{- |
Module      :  ./CommonLogic/ModuleElimination.hs
Description :  Module elimination in CommonLogic
Copyright   :  (c) Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  portable

Used by Comorphisms.CommonLogicModuleElimination and Print_KIF.
-}

module CommonLogic.ModuleElimination (eliminateModules) where

import qualified Data.Set as Set
import CommonLogic.Tools
import Common.Id

import CommonLogic.AS_CommonLogic

-- | Result is a CL-equivalent text without modules
eliminateModules :: TEXT_META -> TEXT_META
eliminateModules :: TEXT_META -> TEXT_META
eliminateModules tm :: TEXT_META
tm =
  TEXT_META
tm { getText :: TEXT
getText = [PHRASE] -> Range -> TEXT
Text [SENTENCE -> PHRASE
Sentence (NAME -> [NAME] -> TEXT -> SENTENCE
me_text NAME
newName [] (TEXT -> SENTENCE) -> TEXT -> SENTENCE
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
getText TEXT_META
tm)] Range
nullRange }
  where (newName :: NAME
newName, _) = (String, Int) -> Set NAME -> (NAME, Int)
freeName ("item", 0) (TEXT -> Set NAME
indvC_text (TEXT -> Set NAME) -> TEXT -> Set NAME
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
getText TEXT_META
tm)

-- NOTE: ignores importations
me_text :: NAME -> [NAME] -> TEXT -> SENTENCE
me_text :: NAME -> [NAME] -> TEXT -> SENTENCE
me_text newName :: NAME
newName modules :: [NAME]
modules txt :: TEXT
txt =
    case TEXT
txt of
        Text phrs :: [PHRASE]
phrs _ -> NAME -> [NAME] -> [PHRASE] -> SENTENCE
me_phrases NAME
newName [NAME]
modules ([PHRASE] -> SENTENCE) -> [PHRASE] -> SENTENCE
forall a b. (a -> b) -> a -> b
$ (PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
nonImportation [PHRASE]
phrs
        Named_text _ t :: TEXT
t _ -> NAME -> [NAME] -> TEXT -> SENTENCE
me_text NAME
newName [NAME]
modules TEXT
t
  where nonImportation :: PHRASE -> Bool
nonImportation p :: PHRASE
p = case PHRASE
p of
          Importation _ -> Bool
False
          _ -> Bool
True

-- Table 2: R5a - R5b, ignoring importations and comments
me_phrases :: NAME -> [NAME] -> [PHRASE] -> SENTENCE
me_phrases :: NAME -> [NAME] -> [PHRASE] -> SENTENCE
me_phrases newName :: NAME
newName modules :: [NAME]
modules phrs :: [PHRASE]
phrs =
    case [PHRASE] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [PHRASE]
phrs of
         1 -> NAME -> [NAME] -> PHRASE -> SENTENCE
me_phrase NAME
newName [NAME]
modules (PHRASE -> SENTENCE) -> PHRASE -> SENTENCE
forall a b. (a -> b) -> a -> b
$ [PHRASE] -> PHRASE
forall a. [a] -> a
head [PHRASE]
phrs
         _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (
                AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction (
                    (PHRASE -> SENTENCE) -> [PHRASE] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> [NAME] -> PHRASE -> SENTENCE
me_phrase NAME
newName [NAME]
modules) ((PHRASE -> Bool) -> [PHRASE] -> [PHRASE]
forall a. (a -> Bool) -> [a] -> [a]
filter PHRASE -> Bool
mod_sen [PHRASE]
phrs)
                )
            ) Range
nullRange
    where mod_sen :: PHRASE -> Bool
mod_sen p :: PHRASE
p = case PHRASE
p of
            Module _ -> Bool
True
            Sentence _ -> Bool
True
            _ -> Bool
False


-- | converts comment-texts to comment-sentences
me_phrase :: NAME -> [NAME] -> PHRASE -> SENTENCE
me_phrase :: NAME -> [NAME] -> PHRASE -> SENTENCE
me_phrase newName :: NAME
newName modules :: [NAME]
modules p :: PHRASE
p =
    case PHRASE
p of
        Module m :: MODULE
m -> NAME -> [NAME] -> MODULE -> SENTENCE
me_module NAME
newName [NAME]
modules MODULE
m
        Sentence s :: SENTENCE
s -> NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence NAME
newName [NAME]
modules SENTENCE
s
        Comment_text c :: COMMENT
c txt :: TEXT
txt r :: Range
r -> COMMENT -> SENTENCE -> Range -> SENTENCE
Comment_sent COMMENT
c (NAME -> [NAME] -> TEXT -> SENTENCE
me_text NAME
newName [NAME]
modules TEXT
txt) Range
r
        Importation _ -> SENTENCE
forall a. HasCallStack => a
undefined

me_sentence :: NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence :: NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence newName :: NAME
newName modules :: [NAME]
modules sen :: SENTENCE
sen =
    if [NAME] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [NAME]
modules then SENTENCE
sen else -- this keeps the sentence simple
    case SENTENCE
sen of
        Bool_sent bs :: BOOL_SENT
bs _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (NAME -> [NAME] -> BOOL_SENT -> BOOL_SENT
me_boolsent NAME
newName [NAME]
modules BOOL_SENT
bs) Range
nullRange
        Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is _ ->
          QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
q [NAME_OR_SEQMARK]
vs (NAME
-> [NAME] -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
me_quantsent NAME
newName [NAME]
modules QUANT
q [NAME_OR_SEQMARK]
vs SENTENCE
is) Range
nullRange
        x :: SENTENCE
x -> SENTENCE
x                              -- Table 2: R1a - R2b

-- Table 2: R2a - R2e
me_boolsent :: NAME -> [NAME] -> BOOL_SENT -> BOOL_SENT
me_boolsent :: NAME -> [NAME] -> BOOL_SENT -> BOOL_SENT
me_boolsent newName :: NAME
newName modules :: [NAME]
modules bs :: BOOL_SENT
bs =
    case BOOL_SENT
bs of
         Junction j :: AndOr
j sens :: [SENTENCE]
sens -> AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
j ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$ (SENTENCE -> SENTENCE) -> [SENTENCE] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map SENTENCE -> SENTENCE
me_sen_mod [SENTENCE]
sens
         Negation sen :: SENTENCE
sen -> SENTENCE -> BOOL_SENT
Negation (SENTENCE -> BOOL_SENT) -> SENTENCE -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$ SENTENCE -> SENTENCE
me_sen_mod SENTENCE
sen
         BinOp op :: ImplEq
op s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 -> ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
op (SENTENCE -> SENTENCE
me_sen_mod SENTENCE
s1) (SENTENCE -> SENTENCE
me_sen_mod SENTENCE
s2)
    where me_sen_mod :: SENTENCE -> SENTENCE
me_sen_mod = NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence NAME
newName [NAME]
modules -- TODO: check whether dn stays the same

-- Table 2: R3a - R3b
me_quantsent :: NAME -> [NAME] -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE
                -> SENTENCE
me_quantsent :: NAME
-> [NAME] -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> SENTENCE
me_quantsent newName :: NAME
newName modules :: [NAME]
modules _ noss :: [NAME_OR_SEQMARK]
noss sen :: SENTENCE
sen =
  BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication
             ([NAME] -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent [NAME]
modules [NAME_OR_SEQMARK]
noss)
             (NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence NAME
newName [NAME]
modules SENTENCE
sen)) Range
nullRange

anticedent :: [NAME] -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent :: [NAME] -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent modules :: [NAME]
modules noss :: [NAME_OR_SEQMARK]
noss =
    case [NAME]
modules of
         [m :: NAME
m] -> NAME -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent1 NAME
m [NAME_OR_SEQMARK]
noss
         _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ((NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> [NAME_OR_SEQMARK] -> SENTENCE
`anticedent1` [NAME_OR_SEQMARK]
noss) [NAME]
modules)) Range
nullRange

anticedent1 :: NAME -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent1 :: NAME -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent1 m :: NAME
m noss :: [NAME_OR_SEQMARK]
noss = case [NAME_OR_SEQMARK]
noss of
  [nos :: NAME_OR_SEQMARK
nos] -> ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (NAME -> TERM
Name_term NAME
m) [NAME_OR_SEQMARK -> TERM_SEQ
nos2termseq NAME_OR_SEQMARK
nos]) Range
nullRange
  _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$
                  (NAME_OR_SEQMARK -> SENTENCE) -> [NAME_OR_SEQMARK] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (\ nos :: NAME_OR_SEQMARK
nos -> NAME -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent1 NAME
m [NAME_OR_SEQMARK
nos]) [NAME_OR_SEQMARK]
noss) Range
nullRange

nos2termseq :: NAME_OR_SEQMARK -> TERM_SEQ
nos2termseq :: NAME_OR_SEQMARK -> TERM_SEQ
nos2termseq nos :: NAME_OR_SEQMARK
nos = case NAME_OR_SEQMARK
nos of
                    Name n :: NAME
n -> TERM -> TERM_SEQ
Term_seq (TERM -> TERM_SEQ) -> TERM -> TERM_SEQ
forall a b. (a -> b) -> a -> b
$ NAME -> TERM
Name_term NAME
n
                    SeqMark s :: NAME
s -> NAME -> TERM_SEQ
Seq_marks NAME
s

-- Table 2 R4
me_module :: NAME -> [NAME] -> MODULE -> SENTENCE
me_module :: NAME -> [NAME] -> MODULE -> SENTENCE
me_module newName :: NAME
newName modules :: [NAME]
modules m :: MODULE
m =
    case MODULE
m of
        Mod n :: NAME
n t :: TEXT
t _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction (
              NAME -> [NAME] -> TEXT -> SENTENCE
me_text NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules) TEXT
t
            SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: NAME -> [NAME] -> SENTENCE
ex_conj NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules)
            SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: (NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules)) (Set NAME -> [NAME]
forall a. Set a -> [a]
Set.elems (Set NAME -> [NAME]) -> Set NAME -> [NAME]
forall a b. (a -> b) -> a -> b
$ TEXT -> Set NAME
indvC_text TEXT
t)
          )) Range
nullRange
        Mod_ex n :: NAME
n excl :: [NAME]
excl t :: TEXT
t _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction (
              NAME -> [NAME] -> TEXT -> SENTENCE
me_text NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules) TEXT
t
            SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: NAME -> [NAME] -> SENTENCE
ex_conj NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules)
            SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: (NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules)) (Set NAME -> [NAME]
forall a. Set a -> [a]
Set.elems (Set NAME -> [NAME]) -> Set NAME -> [NAME]
forall a b. (a -> b) -> a -> b
$ TEXT -> Set NAME
indvC_text TEXT
t)
            [SENTENCE] -> [SENTENCE] -> [SENTENCE]
forall a. [a] -> [a] -> [a]
++ (NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> [NAME] -> NAME -> SENTENCE
not_ex_conj_excl NAME
newName (NAME
n NAME -> [NAME] -> [NAME]
forall a. a -> [a] -> [a]
: [NAME]
modules)) [NAME]
excl
          )) Range
nullRange

-- Table 2 R4: each line in the conjunction
ex_conj :: NAME -> [NAME] -> SENTENCE
ex_conj :: NAME -> [NAME] -> SENTENCE
ex_conj n :: NAME
n modules :: [NAME]
modules =
  QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Existential [NAME -> NAME_OR_SEQMARK
Name NAME
n] (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction (
        (NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> NAME -> SENTENCE
modNameToPredicate NAME
n) [NAME]
modules
    )) Range
nullRange) Range
nullRange

-- Table 2 R4: each line with indvC-elements in the conjunction
ex_conj_indvC :: NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC :: NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC n :: NAME
n modules :: [NAME]
modules c :: NAME
c =
    QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Existential [NAME -> NAME_OR_SEQMARK
Name NAME
n] (BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction (
            ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation (NAME -> TERM
Name_term NAME
n) (NAME -> TERM
Name_term NAME
c)) Range
nullRange
            SENTENCE -> [SENTENCE] -> [SENTENCE]
forall a. a -> [a] -> [a]
: (NAME -> SENTENCE) -> [NAME] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map (NAME -> NAME -> SENTENCE
modNameToPredicate NAME
n) [NAME]
modules
        )) Range
nullRange) Range
nullRange

-- Table 2 R4: each line with excluded elements in the conjunction
not_ex_conj_excl :: NAME -> [NAME] -> NAME -> SENTENCE
not_ex_conj_excl :: NAME -> [NAME] -> NAME -> SENTENCE
not_ex_conj_excl n :: NAME
n modules :: [NAME]
modules c :: NAME
c =
    BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation (NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC NAME
n [NAME]
modules NAME
c)) Range
nullRange

-- Table 2 R4: makes a Predicate out of the module name
modNameToPredicate :: NAME -> NAME -> SENTENCE
modNameToPredicate :: NAME -> NAME -> SENTENCE
modNameToPredicate n :: NAME
n m :: NAME
m =
    ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (NAME -> TERM
Name_term NAME
m) [TERM -> TERM_SEQ
Term_seq (NAME -> TERM
Name_term NAME
n)]) Range
nullRange
-- what if the module name already occurs as a predicate?