0f081398cf0eef8cc7c66a535d450110a92dc8aefielding{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding{- |

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingModule : $Header$

bc8fd1b0b1afdf89b8d28eefa8cd74e26ba97986fieldingCopyright : (c) Christian Maeder, DFKI 2012

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingLicense : GPLv2 or higher, see LICENSE.txt

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingMaintainer : Christian.Maeder@dfki.de

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingStability : provisional

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingPortability : non-portable (MPTC-FD)

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-}

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingmodule Comorphisms.ExtModal2CASL where

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport Logic.Logic

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport Logic.Comorphism

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport Common.AS_Annotation

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport Common.Id

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport Common.ProofTree

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Common.Lib.Rel as Rel

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Common.Lib.MapSet as MapSet

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport qualified Data.Set as Set

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.Fold

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.Logic_CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.Sublogic as SL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.Sign

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingimport CASL.AS_Basic_CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.Morphism

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport CASL.World

64185f9824e42f21ca7b9ae6c004484215c031a7rbb

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding-- ExtModalCASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport ExtModal.Logic_ExtModal

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport ExtModal.AS_ExtModal

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport ExtModal.ExtModalSign

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingimport ExtModal.Sublogic

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldingdata ExtModal2CASL = ExtModal2CASL deriving (Show)

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldinginstance Language ExtModal2CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fieldinginstance Comorphism ExtModal2CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding ExtModal Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding SYMB_MAP_ITEMS ExtModalSign ExtModalMorph

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding Symbol RawSymbol ()

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding CASL CASL_Sublogics

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding CASLSign

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding CASLMor

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding Symbol RawSymbol ProofTree where

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding sourceLogic ExtModal2CASL = ExtModal

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding sourceSublogic ExtModal2CASL = maxSublogic

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding targetLogic ExtModal2CASL = CASL

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding mapSublogic ExtModal2CASL _ = Just SL.caslTop

ab2c1c1c83ec91415565da5a71fbc15d9685caa6fielding map_theory ExtModal2CASL (sig, sens) = case transSig sig of

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding mme -> return (mme, map (mapNamed $ transTop sig) sens)

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding {-

3568de757bac0b47256647504c186d17ca272f85rbb map_morphism ExtModal2CASL = return . mapMor

3568de757bac0b47256647504c186d17ca272f85rbb map_sentence ExtModal2CASL sig = return . transSen sig

3568de757bac0b47256647504c186d17ca272f85rbb map_symbol ExtModal2CASL _ = Set.singleton . mapSym

3568de757bac0b47256647504c186d17ca272f85rbb -}

3568de757bac0b47256647504c186d17ca272f85rbb has_model_expansion ExtModal2CASL = True

3568de757bac0b47256647504c186d17ca272f85rbb is_weakly_amalgamable ExtModal2CASL = True

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbbnomName :: Token -> Id

3568de757bac0b47256647504c186d17ca272f85rbbnomName t = Id [genToken "N"] [mkId [t]] $ tokPos t

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbbnomOpType :: OpType

3568de757bac0b47256647504c186d17ca272f85rbbnomOpType = mkTotOpType [] world

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbb-- | add world arguments to flexible ops and preds; and add relations

3568de757bac0b47256647504c186d17ca272f85rbbtransSig :: ExtModalSign -> CASLSign

3568de757bac0b47256647504c186d17ca272f85rbbtransSig sign = let

3568de757bac0b47256647504c186d17ca272f85rbb s1 = embedSign () sign

3568de757bac0b47256647504c186d17ca272f85rbb extInf = extendedInfo sign

3568de757bac0b47256647504c186d17ca272f85rbb flexibleOps = flexOps extInf

3568de757bac0b47256647504c186d17ca272f85rbb flexiblePreds = flexPreds extInf

3568de757bac0b47256647504c186d17ca272f85rbb flexOps' = addWorldOp world addPlace flexibleOps

3568de757bac0b47256647504c186d17ca272f85rbb flexPreds' = addWorldPred world addPlace flexiblePreds

3568de757bac0b47256647504c186d17ca272f85rbb rigOps' = diffOpMapSet (opMap sign) flexibleOps

3568de757bac0b47256647504c186d17ca272f85rbb rigPreds' = diffMapSet (predMap sign) flexiblePreds

3568de757bac0b47256647504c186d17ca272f85rbb noms = nominals extInf

3568de757bac0b47256647504c186d17ca272f85rbb noNomsPreds = Set.fold (\ n -> MapSet.delete (nomPId n) nomPType)

3568de757bac0b47256647504c186d17ca272f85rbb rigPreds' noms

3568de757bac0b47256647504c186d17ca272f85rbb termMs = termMods extInf

3568de757bac0b47256647504c186d17ca272f85rbb timeMs = timeMods extInf

3568de757bac0b47256647504c186d17ca272f85rbb rels = Set.fold (\ m ->

3568de757bac0b47256647504c186d17ca272f85rbb insertModPred world (Set.member m timeMs) (Set.member m termMs) m)

3568de757bac0b47256647504c186d17ca272f85rbb MapSet.empty $ modalities extInf

3568de757bac0b47256647504c186d17ca272f85rbb nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms

3568de757bac0b47256647504c186d17ca272f85rbb in s1

3568de757bac0b47256647504c186d17ca272f85rbb { sortRel = Rel.insertKey world $ sortRel sign

3568de757bac0b47256647504c186d17ca272f85rbb , opMap = addOpMapSet flexOps' nomOps

3568de757bac0b47256647504c186d17ca272f85rbb , assocOps = diffOpMapSet (assocOps sign) flexibleOps

3568de757bac0b47256647504c186d17ca272f85rbb , predMap = addMapSet rels $ addMapSet flexPreds' noNomsPreds}

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbbdata Args = Args

3568de757bac0b47256647504c186d17ca272f85rbb { currentW, futureW :: TERM () -- world variables

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , currentN, futureN :: TERM () -- world numbering

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , transPredName :: Id

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding , signature :: ExtModalSign }

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding

3568de757bac0b47256647504c186d17ca272f85rbbnatSort :: SORT

cd8f8c995d415473f3bfb0b329b2450f2a722c3atrawicknatSort = stringToId "Nat"

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbbtransTop :: ExtModalSign -> FORMULA EM_FORMULA -> FORMULA ()

3568de757bac0b47256647504c186d17ca272f85rbbtransTop sig f = case f of

3568de757bac0b47256647504c186d17ca272f85rbb Sort_gen_ax cs b -> Sort_gen_ax cs b

db12cd62083041bf90945eeb90cc40fbd2340797trawick _ -> let

db12cd62083041bf90945eeb90cc40fbd2340797trawick vd = mkVarDecl (genNumVar "w" 1) world

db12cd62083041bf90945eeb90cc40fbd2340797trawick vt = toQualVar vd

333eac96e4fb7d6901cb75e6ca7bb22b2ccb84cetrawick vn = mkVarDecl (genNumVar "n" 1) natSort

333eac96e4fb7d6901cb75e6ca7bb22b2ccb84cetrawick nt = toQualVar vn

3568de757bac0b47256647504c186d17ca272f85rbb in mkForall [vd] $ transMF (Args vt vt nt nt (stringToId "Z") sig) f

3568de757bac0b47256647504c186d17ca272f85rbb

3568de757bac0b47256647504c186d17ca272f85rbbtransMF :: Args -> FORMULA EM_FORMULA -> FORMULA ()

3568de757bac0b47256647504c186d17ca272f85rbbtransMF as = let

3568de757bac0b47256647504c186d17ca272f85rbb extInf = extendedInfo $ signature as

3568de757bac0b47256647504c186d17ca272f85rbb flexibleOps = flexOps extInf

3568de757bac0b47256647504c186d17ca272f85rbb flexiblePreds = flexPreds extInf

3568de757bac0b47256647504c186d17ca272f85rbb in foldFormula (mapRecord $ const ())

3568de757bac0b47256647504c186d17ca272f85rbb { foldPredication = \ _ ps args r -> case ps of

3568de757bac0b47256647504c186d17ca272f85rbb Qual_pred_name pn pTy@(Pred_type srts q) p

3568de757bac0b47256647504c186d17ca272f85rbb | MapSet.member pn (toPredType pTy) flexiblePreds

3568de757bac0b47256647504c186d17ca272f85rbb -> Predication

3568de757bac0b47256647504c186d17ca272f85rbb (Qual_pred_name (addPlace pn) (Pred_type (world : srts) q) p)

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz (futureW as : args) r

3568de757bac0b47256647504c186d17ca272f85rbb _ -> Predication ps args r

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz , foldExtFORMULA = \ _ f -> transEMF as f

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz , foldApplication = \ _ os args r -> case os of

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz Qual_op_name on oTy@(Op_type ok srts res q) p

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding | MapSet.member on (toOpType oTy) flexibleOps

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz -> Application

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (Qual_op_name (addPlace on) (Op_type ok (world : srts) res q) p)

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding (futureW as : args) r

0f081398cf0eef8cc7c66a535d450110a92dc8aefielding _ -> Application os args r

8f3ec4772d2aeb347cf40e87c77627bb784dd018rbb }

8f3ec4772d2aeb347cf40e87c77627bb784dd018rbb

3d96ee83babeec32482c9082c9426340cee8c44dwrowetransEMF :: Args -> EM_FORMULA -> FORMULA ()

0f081398cf0eef8cc7c66a535d450110a92dc8aefieldingtransEMF as emf = case emf of

cd8f8c995d415473f3bfb0b329b2450f2a722c3atrawick PrefixForm _pf f _ -> transMF as f

cd8f8c995d415473f3bfb0b329b2450f2a722c3atrawick UntilSince _isUntil f1 f2 r -> conjunctRange [transMF as f1, transMF as f2] r

3568de757bac0b47256647504c186d17ca272f85rbb ModForm _ -> trueForm

28c170ac8e99644de58cad454c6e0f9b4b359be6jerenkrantz