{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}

{- |

Module : $Header$

Description : Comorphism from CommonLogic to CommonLogic

Copyright : (c) Eugen Kuksa, Uni Bremen 2011

License : GPLv2 or higher, see LICENSE.txt

Maintainer : eugenk@informatik.uni-bremen.de

Stability : experimental (not complete: typleclass-instances missing)

Portability : non-portable (via Logic.Logic)

Translating comorphism from CommonLogic to CommonLogic in order to eliminate

modules.

-}

module Comorphisms.CommonLogic2CommonLogic (

CommonLogic2CommonLogic (..)

, eliminateModules

)

where

import qualified Data.Set as Set

import CommonLogic.Tools

import Common.Id

import Logic.Logic as Logic

import Logic.Comorphism

import Common.ProofTree

import Common.Result

import qualified Common.AS_Annotation as AS_Anno

-- Common Logic

import CommonLogic.AS_CommonLogic

import qualified CommonLogic.Logic_CommonLogic as Logic

import qualified CommonLogic.Sign as Sign

import qualified CommonLogic.Symbol as Symbol

import qualified CommonLogic.Morphism as Mor

import qualified CommonLogic.Sublogic as Sl

data CommonLogic2CommonLogic = CommonLogic2CommonLogic deriving Show

instance Language CommonLogic2CommonLogic where

language_name CommonLogic2CommonLogic = "CommonLogic2CommonLogic"

instance Comorphism

CommonLogic2CommonLogic -- comorphism

Logic.CommonLogic -- lid domain

Sl.CommonLogicSL -- sublogics codomain

BASIC_SPEC -- Basic spec domain

TEXT_MRS -- sentence domain

SYMB_ITEMS -- symb_items

SYMB_MAP_ITEMS -- symbol map items domain

Sign.Sign -- signature domain

Mor.Morphism -- morphism domain

Symbol.Symbol -- symbol domain

Symbol.Symbol -- rawsymbol domain

ProofTree -- proof tree codomain

Logic.CommonLogic -- lid domain

Sl.CommonLogicSL -- sublogics codomain

BASIC_SPEC -- Basic spec domain

TEXT_MRS -- sentence domain

SYMB_ITEMS -- symb_items

SYMB_MAP_ITEMS -- symbol map items domain

Sign.Sign -- signature domain

Mor.Morphism -- morphism domain

Symbol.Symbol -- symbol domain

Symbol.Symbol -- rawsymbol domain

ProofTree -- proof tree codomain

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 (Text_mrs (txt,mrs)) =

Text_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?