hets/CommonLogic/ModuleElimination.hs

{- |
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 tm =
  tm { getText = Text [Sentence (me_text newName [] $ getText tm)] nullRange }
  where (newName, _) = freeName ("item", 0) (indvC_text $ getText tm)

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

-- Table 2: R5a - R5b, ignoring importations and comments
me_phrases :: NAME -> [NAME] -> [PHRASE] -> SENTENCE
me_phrases newName modules phrs =
    case length phrs of
         1 -> me_phrase newName modules $ head phrs
         _ -> Bool_sent (
                Junction Conjunction (
                    map (me_phrase newName modules) (filter mod_sen phrs)
                )
            ) nullRange
    where mod_sen p = case p of
            Module _ -> True
            Sentence _ -> True
            _ -> False


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

me_sentence :: NAME -> [NAME] -> SENTENCE -> SENTENCE
me_sentence newName modules sen =
    if null modules then sen else -- this keeps the sentence simple
    case sen of
        Bool_sent bs _ -> Bool_sent (me_boolsent newName modules bs) nullRange
        Quant_sent q vs is _ ->
          Quant_sent q vs (me_quantsent newName modules q vs is) nullRange
        x -> x                              -- Table 2: R1a - R2b

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

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

anticedent :: [NAME] -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent modules noss =
    case modules of
         [m] -> anticedent1 m noss
         _ -> Bool_sent (Junction Conjunction (map (`anticedent1` noss) modules)) nullRange

anticedent1 :: NAME -> [NAME_OR_SEQMARK] -> SENTENCE
anticedent1 m noss = case noss of
  [nos] -> Atom_sent (Atom (Name_term m) [nos2termseq nos]) nullRange
  _ -> Bool_sent (Junction Conjunction $
                  map (\ nos -> anticedent1 m [nos]) noss) nullRange

nos2termseq :: NAME_OR_SEQMARK -> TERM_SEQ
nos2termseq nos = case nos of
                    Name n -> Term_seq $ Name_term n
                    SeqMark s -> Seq_marks s

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

-- Table 2 R4: each line in the conjunction
ex_conj :: NAME -> [NAME] -> SENTENCE
ex_conj n modules =
  Quant_sent Existential [Name n] (Bool_sent (Junction Conjunction (
        map (modNameToPredicate n) modules
    )) nullRange) nullRange

-- Table 2 R4: each line with indvC-elements in the conjunction
ex_conj_indvC :: NAME -> [NAME] -> NAME -> SENTENCE
ex_conj_indvC n modules c =
    Quant_sent Existential [Name n] (Bool_sent (Junction Conjunction (
            Atom_sent (Equation (Name_term n) (Name_term c)) nullRange
            : map (modNameToPredicate n) modules
        )) nullRange) nullRange

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

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