CASL2HasCASL.hs revision 97018cf5fa25b494adffd7e9b4e87320dae6bf47
Portability : non-portable (imports Logic.Logic)
module Comorphisms.CASL2HasCASL where
import Logic.Logic
import Logic.Comorphism
import Common.Id
import Common.Lib.State
import Common.AS_Annotation
import qualified Common.Lib.Map as Map
import qualified Common.Lib.Set as Set
import CASL.Logic_CASL
import CASL.Sublogic as CasSub
import CASL.Sign
import qualified CASL.AS_Basic_CASL as Cas
import qualified CASL.Morphism as CasM
import HasCASL.Logic_HasCASL
import HasCASL.As
import HasCASL.Le
import HasCASL.Builtin
import HasCASL.VarDecl
import HasCASL.AsUtils
import HasCASL.Morphism
import HasCASL.Sublogic as HasSub
{ CasSub.has_sub = True, -- simple subsorting in HasCASL
CasSub.has_part = True,
CasSub.has_cons = True,
CasSub.has_eq = True,
CasSub.has_pred = True,
targetSublogic CASL2HasCASL = HasSub.top
map_symbol CASL2HasCASL = Set.singleton . mapSym
fromOpType :: OpType -> Cas.FunKind -> TypeScheme
Cas.Total -> FunArr
Cas.Partial -> PFunArr
mapTheory :: (Sign f e, [Named (Cas.FORMULA f)]) -> (Env, [Named Sentence])
let j = Map.findWithDefault i i im in
initialEnv { classMap = Map.empty,
typeMap = Map.fromList $ map
$ Set.toList $ supersortsOf s sign
})) $ Set.toList $ sortSet sign }
mapMor :: CasM.Morphism f e m -> Morphism
mapMor m = let tm = CasM.sort_map m
{ typeIdMap = tm , funMap = Map.fromList (f2 ++ f1) }
mapSym :: CasM.Symbol -> Symbol
mapSym s = let i = CasM.symName s in
case CasM.symbType s of
CasM.OpAsItemType ot ->
CasM.PredAsItemType pt -> idToOpSymbol initialEnv i $ fromPredType pt
CasM.SortAsItemType -> idToTypeSymbol initialEnv i star
toQuant :: Cas.QUANTIFIER -> Quantifier
toQuant Cas.Universal = Universal
toQuant Cas.Existential = Existential
toQuant Cas.Unique_existential = Unique
toVarDecl :: Cas.VAR_DECL -> [GenVarDecl]
toVarDecl (Cas.Var_decl vs s ps) =
toSentence :: Sign f e -> Cas.FORMULA f -> Sentence
Cas.Sort_gen_ax cs b -> let
(sorts, ops, smap) = Cas.recover_Sort_gen_ax cs
mapPart :: Cas.FunKind -> Partiality
$ map ( \ s -> DataEntry (Map.fromList smap) s genKind []
$ map ( \ (Cas.Qual_op_name i t ps) ->
toTerm :: Sign f e -> Cas.FORMULA f -> Term
Cas.Quantification q vs frm ps ->
Cas.Conjunction fs ps ->
Cas.Disjunction fs ps ->
Cas.Implication f1 f2 b ps ->
Cas.Equivalence f1 f2 ps ->
Cas.Negation frm ps -> mkTerm notId notType ps $ toTerm s frm
Cas.True_atom ps -> unitTerm trueId ps
Cas.False_atom ps -> unitTerm falseId ps
Cas.Existl_equation t1 t2 ps ->
Cas.Strong_equation t1 t2 ps ->
Cas.Definedness t ps -> mkTerm defId defType ps $ fromTERM s t
Cas.Membership t ty ps -> TypedTerm (fromTERM s t) InType (toType ty) ps
fromOP_TYPE :: Cas.OP_TYPE -> TypeScheme
fromTERM :: Sign f e -> Cas.TERM f -> Term
Cas.Qual_var v ty ps ->
Cas.Sorted_term trm ty ps ->
Cas.Cast trm ty ps -> TypedTerm (fromTERM s trm) AsType (toType ty) ps
Cas.Conditional t1 f t2 ps -> mkTerm whenElse whenType ps $