1a38107941725211e7c3f051f7a8f5e12199f03acmaeder{- |

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : embedding from CASL to ModalCASL

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis TsogiasCopyright : (c) Till Mossakowski and Uni Bremen 2004

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis TsogiasLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasMaintainer : luecke@informatik.uni-bremen.de

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis TsogiasStability : provisional

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis TsogiasPortability : non-portable (imports Logic.Logic)

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis TsogiasThe embedding comorphism from CASL to ModalCASL.

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias-}

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogiasmodule Comorphisms.CASL2Modal (CASL2Modal(..)) where

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasimport Logic.Logic

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasimport Logic.Comorphism

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogiasimport qualified Data.Set as Set

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias-- CASL

4e95ffc23b9c5f0b5980ab6f1cacbe7bd9789851Alexis Tsogiasimport CASL.Logic_CASL

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport CASL.Sublogic as SL

1a38107941725211e7c3f051f7a8f5e12199f03acmaederimport CASL.Sign

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogiasimport CASL.AS_Basic_CASL

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogiasimport CASL.Morphism

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder-- ModalCASL

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroederimport Modal.Logic_Modal

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogiasimport Modal.AS_Modal

4e95ffc23b9c5f0b5980ab6f1cacbe7bd9789851Alexis Tsogiasimport Modal.ModalSign

8394b397aadaf0c2bfc19c0628f17f83f031a759Jonathan von Schroeder

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder-- | The identity of the comorphism

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogiasdata CASL2Modal = CASL2Modal deriving (Show)

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogiasinstance Language CASL2Modal -- default definition is okay

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroederinstance Comorphism CASL2Modal

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder CASL CASL_Sublogics

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias CASLSign

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder CASLMor

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Symbol RawSymbol Q_ProofTree

87d946b3c13ffd7f6391aa796e786c2b31b122b1Jonathan von Schroeder Modal ()

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder M_BASIC_SPEC ModalFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias MSign

1e622ddf5a057555db1924ddc88475c695c6f7f2Alexis Tsogias ModalMor

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias Symbol RawSymbol () where

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias sourceLogic CASL2Modal = CASL

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias sourceSublogic CASL2Modal = SL.top

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias targetLogic CASL2Modal = Modal

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder mapSublogic CASL2Modal _ = Just ()

fc09e0a6af734edbd944dd8082bb51985c233b43Alexis Tsogias map_theory CASL2Modal = return . simpleTheoryMapping mapSig mapSen

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias map_morphism CASL2Modal = return . mapMor

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias map_sentence CASL2Modal _ = return . mapSen

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias map_symbol CASL2Modal = Set.singleton . mapSym

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias has_model_expansion CASL2Modal = True

7dc37844730a8b23973139e9720574382de109e7Alexis Tsogias is_weakly_amalgamable CASL2Modal = True

34f39ea74476d1637e9b21f5c8d18a4c26a6671bJonathan von Schroeder

7dc37844730a8b23973139e9720574382de109e7Alexis TsogiasmapSig :: CASLSign -> MSign

8fb127028cb7dd361e348a3252e33487f73428bcJonathan von SchroedermapSig sign =

8fb127028cb7dd361e348a3252e33487f73428bcJonathan von Schroeder (emptySign emptyModalSign) {sortSet = sortSet sign

409eb8adf8c7ee0609aef256b67f5dfad2fb6386Alexis Tsogias , sortRel = sortRel sign

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , opMap = opMap sign

e21e5f0fa66bf80e14cfd3f571e09b3952e46ad9Alexis Tsogias , assocOps = assocOps sign

81e71677da25aee1caa7fef177c45ddd69bbf22eJonathan von Schroeder , predMap = predMap sign }

1a38107941725211e7c3f051f7a8f5e12199f03acmaeder

mapMor :: CASLMor -> ModalMor

mapMor m = (embedMorphism () (mapSig $ msource m) $ mapSig $ mtarget m)

{ sort_map = sort_map m

, fun_map = fun_map m

, pred_map = pred_map m }

mapSym :: Symbol -> Symbol

mapSym = id -- needs to be changed once modal symbols are added

mapSen :: CASLFORMULA -> ModalFORMULA

mapSen f = case f of

Quantification q vs frm ps ->

Quantification q vs (mapSen frm) ps

Conjunction fs ps ->

Conjunction (map mapSen fs) ps

Disjunction fs ps ->

Disjunction (map mapSen fs) ps

Implication f1 f2 b ps ->

Implication (mapSen f1) (mapSen f2) b ps

Equivalence f1 f2 ps ->

Equivalence (mapSen f1) (mapSen f2) ps

Negation frm ps -> Negation (mapSen frm) ps

True_atom ps -> True_atom ps

False_atom ps -> False_atom ps

Existl_equation t1 t2 ps ->

Existl_equation (mapTERM t1) (mapTERM t2) ps

Strong_equation t1 t2 ps ->

Strong_equation (mapTERM t1) (mapTERM t2) ps

Predication pn as qs ->

Predication pn (map mapTERM as) qs

Definedness t ps -> Definedness (mapTERM t) ps

Membership t ty ps -> Membership (mapTERM t) ty ps

Sort_gen_ax constrs isFree -> Sort_gen_ax constrs isFree

_ -> error "CASL2Modal.mapSen"

mapTERM :: TERM () -> TERM M_FORMULA

mapTERM t = case t of

Qual_var v ty ps -> Qual_var v ty ps

Application opsym as qs -> Application opsym (map mapTERM as) qs

Sorted_term trm ty ps -> Sorted_term (mapTERM trm) ty ps

Cast trm ty ps -> Cast (mapTERM trm) ty ps

Conditional t1 f t2 ps ->

Conditional (mapTERM t1) (mapSen f) (mapTERM t2) ps

_ -> error "CASL2Modal.mapTERM"