707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{- |

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederModule : $Header$

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederDescription : Comorphism from CommonLogic to CommonLogic

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederCopyright : (c) Eugen Kuksa, Uni Bremen 2011

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederMaintainer : eugenk@informatik.uni-bremen.de

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederStability : experimental (not complete: typleclass-instances missing)

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederPortability : non-portable (via Logic.Logic)

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian MaederTranslating comorphism from CommonLogic to CommonLogic in order to eliminate

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maedermodules.

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder-}

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maedermodule Comorphisms.CommonLogic2CommonLogic (

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder CommonLogic2CommonLogic (..)

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder , eliminateModules

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder )

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder where

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport qualified Data.Set as Set

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport CommonLogic.Tools

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport Common.Id

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport Logic.Logic as Logic

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport Logic.Comorphism

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport Common.ProofTree

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport Common.Result

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport qualified Common.AS_Annotation as AS_Anno

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder-- Common Logic

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport CommonLogic.AS_CommonLogic

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport qualified CommonLogic.Logic_CommonLogic as Logic

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maederimport qualified CommonLogic.Sign as Sign

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport qualified CommonLogic.Symbol as Symbol

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederimport qualified CommonLogic.Morphism as Mor

bb5022629cd054caa569bf15e366a9977ab011ceChristian Maederimport qualified CommonLogic.Sublogic as Sl

4cc271fa22221d0d20cf303553f86c4e3b1a56e4Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederdata CommonLogic2CommonLogic = CommonLogic2CommonLogic deriving Show

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederinstance Language CommonLogic2CommonLogic where

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder language_name CommonLogic2CommonLogic = "CommonLogic2CommonLogic"

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maederinstance Comorphism

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder CommonLogic2CommonLogic -- comorphism

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Logic.CommonLogic -- lid domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Sl.CommonLogicSL -- sublogics codomain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder BASIC_SPEC -- Basic spec domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder TEXT_MRS -- sentence domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder SYMB_ITEMS -- symb_items

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder SYMB_MAP_ITEMS -- symbol map items domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Sign.Sign -- signature domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Mor.Morphism -- morphism domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Symbol.Symbol -- symbol domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Symbol.Symbol -- rawsymbol domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder ProofTree -- proof tree codomain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Logic.CommonLogic -- lid domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Sl.CommonLogicSL -- sublogics codomain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder BASIC_SPEC -- Basic spec domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder TEXT_MRS -- sentence domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder SYMB_ITEMS -- symb_items

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder SYMB_MAP_ITEMS -- symbol map items domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Sign.Sign -- signature domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Mor.Morphism -- morphism domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Symbol.Symbol -- symbol domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder Symbol.Symbol -- rawsymbol domain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder ProofTree -- proof tree codomain

707a4b48578109589b887a7a1ae0bf079d2ce684Christian Maeder where

sourceLogic CommonLogic2CommonLogic = Logic.CommonLogic

sourceSublogic CommonLogic2CommonLogic = Sl.top

targetLogic CommonLogic2CommonLogic = Logic.CommonLogic

mapSublogic CommonLogic2CommonLogic = Just . mapSub

map_theory CommonLogic2CommonLogic = mapTheory

map_morphism CommonLogic2CommonLogic = mapMor

map_sentence CommonLogic2CommonLogic = mapSentence

--hasCommonLogic2CommonLogic_model_expansion = True -- TODO: check if it is really True

mapSub :: Sl.CommonLogicSL -> Sl.CommonLogicSL

mapSub = id

mapMor :: Mor.Morphism -> Result Mor.Morphism

mapMor mor = return mor

mapSentence :: Sign.Sign -> TEXT_MRS -> Result TEXT_MRS

mapSentence _ txt = return $ eliminateModules txt

-------------------------------------------------------------------------------

-- MODULE ELIMINATION --

-------------------------------------------------------------------------------

mapTheory :: (Sign.Sign, [AS_Anno.Named TEXT_MRS])

-> Result (Sign.Sign, [AS_Anno.Named TEXT_MRS])

mapTheory (srcSign, srcTexts) =

return (srcSign,

map ((uncurry AS_Anno.makeNamed) . elimModSnd . senAndName) srcTexts)

where senAndName :: AS_Anno.Named TEXT_MRS -> (String, TEXT_MRS)

senAndName t = (AS_Anno.senAttr t, AS_Anno.sentence t)

elimModSnd :: (String, TEXT_MRS) -> (String, TEXT_MRS)

elimModSnd (s, t) = (s, eliminateModules t)

-- | Result is a CL-equivalent text without modules

eliminateModules :: TEXT_MRS -> TEXT_MRS

eliminateModules (txt,mrs) =

(Text [Sentence (me_text newName [] txt)] nullRange, mrs)

where (newName, _) = freeName ("x", 0) (indvC_text txt)

-- 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 (

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 qs _ -> Quant_sent (me_quantsent newName modules qs) 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

Conjunction sens -> Conjunction $ map me_sen_mod sens

Disjunction sens -> Disjunction $ map me_sen_mod sens

Negation sen -> Negation $ me_sen_mod sen

Implication s1 s2 -> Implication (me_sen_mod s1) (me_sen_mod s2)

Biconditional s1 s2 -> Biconditional (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_SENT -> QUANT_SENT

me_quantsent newName modules qs =

case qs of

Universal noss sen -> Universal noss (

Bool_sent (Implication

(anticedent modules noss)

(me_sentence newName modules sen)

) nullRange)

Existential noss sen -> Existential noss (

Bool_sent (Implication

(anticedent modules noss)

(me_sentence newName modules sen)

) nullRange)

anticedent :: [NAME] -> [NAME_OR_SEQMARK] -> SENTENCE

anticedent modules noss =

case length modules of

1 -> anticedent1 (head modules) noss

_ -> Bool_sent (Conjunction (map (flip anticedent1 noss) modules)) nullRange

anticedent1 :: NAME -> [NAME_OR_SEQMARK] -> SENTENCE

anticedent1 m noss =

Atom_sent (Atom (Name_term m) (map nos2termseq 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 (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 (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 ( 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 ( 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?