ExtModal2HasCASL.hs revision 7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder{- |
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederModule : $Header$
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederCopyright : (c) Christian Maeder, DFKI 2012
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederMaintainer : Christian.Maeder@dfki.de
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederStability : provisional
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaederPortability : non-portable (MPTC-FD)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-}
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maedermodule Comorphisms.ExtModal2HasCASL where
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport Logic.Logic
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport Logic.Comorphism
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport Common.AS_Annotation
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport Common.Id
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.Rel as Rel
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Common.Lib.MapSet as MapSet
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport Comorphisms.CASL2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport qualified Data.Set as Set
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- CASL
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maederimport CASL.AS_Basic_CASL as CASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport CASL.Morphism as CASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport CASL.Sign as CASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport CASL.World
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- ExtModalCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport ExtModal.Logic_ExtModal
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport ExtModal.AS_ExtModal
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport ExtModal.ExtModalSign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport ExtModal.Sublogic as EM
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport HasCASL.Logic_HasCASL
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maederimport HasCASL.As as HC
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport HasCASL.AsUtils
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport HasCASL.Le as HC
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederimport HasCASL.Sublogic as HC
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederdata ExtModal2HasCASL = ExtModal2HasCASL deriving (Show)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Language ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maederinstance Comorphism ExtModal2HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder ExtModal EM.Sublogic EM_BASIC_SPEC ExtModalFORMULA SYMB_ITEMS
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder SYMB_MAP_ITEMS ExtModalSign ExtModalMorph
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder CASL.Symbol CASL.RawSymbol ()
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder HasCASL HC.Sublogic
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder BasicSpec Sentence SymbItems SymbMapItems
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder Env HC.Morphism HC.Symbol HC.RawSymbol () where
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceLogic ExtModal2HasCASL = ExtModal
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder sourceSublogic ExtModal2HasCASL = maxSublogic
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder targetLogic ExtModal2HasCASL = HasCASL
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder mapSublogic ExtModal2HasCASL _ = Just HC.caslLogic { which_logic = HOL }
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder map_theory ExtModal2HasCASL (sig, sens) = case transSig sig sens of
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder mme -> return (mme, [])
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder {-
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_morphism ExtModal2HasCASL = return . mapMor
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_sentence ExtModal2HasCASL sig = return . transSen sig
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder map_symbol ExtModal2HasCASL _ = Set.singleton . mapSym
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder -}
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder has_model_expansion ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder is_weakly_amalgamable ExtModal2HasCASL = True
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName :: Id -> Id
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomName t = Id [genToken "N"] [t] $ rangeOfId t
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType :: OpType
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian MaedernomOpType = mkTotOpType [] world
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauId :: Id
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauId = genName "Tau"
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauTy :: PredType
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertauTy = PredType [world, world]
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder-- | mixfix names work for tuples and are lost after currying
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrI :: Id -> Id
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrI i = if isMixfix i then Id [genToken "C"] [i] $ rangeOfId i else i
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOpSyn :: OP_TYPE -> Type
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOpSyn (Op_type ok args res _) = let
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder (partial, total) = case ok of
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder CASL.Total -> (HC.Total, True)
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder CASL.Partial -> (HC.Partial, False)
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder resTy = toType res
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder in if null args then if total then resTy else mkLazyType resTy
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder else getFunType resTy partial $ map toType args
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOp :: OpType -> TypeScheme
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrOp = simpleTypeScheme . trOpSyn . toOP_TYPE
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPrSyn :: PRED_TYPE -> Type
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPrSyn (Pred_type args ps) = let u = unitTypeWithRange ps in
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder if null args then mkLazyType u else
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder getFunType u HC.Partial $ map toType args
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPr :: PredType -> TypeScheme
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertrPr = simpleTypeScheme . trPrSyn . toPRED_TYPE
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder-- | add world arguments to flexible ops and preds; and add relations
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertransSig :: ExtModalSign -> [Named (FORMULA EM_FORMULA)] -> Env
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian MaedertransSig sign sens = let
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder s1 = embedSign () sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder extInf = extendedInfo sign
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexibleOps = flexOps extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder flexiblePreds = flexPreds extInf
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder flexOps' = addWorldOp world id flexibleOps
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder flexPreds' = addWorldPred world id flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigOps' = diffOpMapSet (opMap sign) flexibleOps
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rigPreds' = diffMapSet (predMap sign) flexiblePreds
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noms = nominals extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder noNomsPreds = Set.fold (`MapSet.delete` nomPType) rigPreds' noms
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder termMs = termMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder timeMs = timeMods extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder rels = Set.fold (\ m ->
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder insertModPred world (Set.member m timeMs) (Set.member m termMs) m)
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder MapSet.empty $ modalities extInf
1c3705f7c752c85afabf3e37a93a3ca9bd614df8Christian Maeder nomOps = Set.fold (\ n -> addOpTo (nomName n) nomOpType) rigOps' noms
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder s2 = s1
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder { sortRel = Rel.insertKey world $ sortRel sign
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder , opMap = addOpMapSet flexOps' nomOps
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder , predMap = (if Set.null timeMs then id else MapSet.insert tauId tauTy)
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder . addMapSet rels $ addMapSet flexPreds' noNomsPreds
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder }
7c44d0c6ca67c2e2f7bb3b95dbc2e8cf7aa20e11Christian Maeder in mapSigAux trI trOp trPr (getConstructors sens) s2