01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder{- |

e6d40133bc9f858308654afb1262b8b483ec5922Till MossakowskiModule : $Header$

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiDescription : embedding CASL into HasCASL

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederCopyright : (c) Till Mossakowski, Christian Maeder and Uni Bremen 2003-2005

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederMaintainer : Christian.Maeder@dfki.de

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaederStability : provisional

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederPortability : non-portable (imports Logic.Logic)

e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till MossakowskiThe embedding comorphism from CASL to HasCASL.

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder-}

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskimodule Comorphisms.CASL2HasCASL where

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowski

1549f3abf73c1122acff724f718b615c82fa3648Till Mossakowskiimport Logic.Logic

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport Logic.Comorphism

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.AS_Annotation

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.Id

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.ProofTree

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport Common.DocUtils

f8b715ab2993083761c0aedb78f1819bcf67b6ccChristian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport qualified Data.Map as Map

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified Data.Set as Set

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder-- CASL

5e46b572ed576c0494768998b043d9d340594122Till Mossakowskiimport CASL.Logic_CASL

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport CASL.Sublogic as CasSub

23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maederimport CASL.ToDoc

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport CASL.Fold

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified CASL.AS_Basic_CASL as Cas

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport qualified CASL.Sign as CasS

db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wangimport qualified CASL.Morphism as CasM

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maederimport HasCASL.Logic_HasCASL

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport HasCASL.As

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederimport HasCASL.AsUtils

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowskiimport HasCASL.Le

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport HasCASL.Builtin

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maederimport HasCASL.Sublogic as HasSub

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maederimport HasCASL.FoldTerm as HasFold

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder-- | The identity of the comorphism

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichdata CASL2HasCASL = CASL2HasCASL deriving (Show)

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettichinstance Language CASL2HasCASL -- default definition is okay

ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maederinstance Comorphism CASL2HasCASL

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder CASL CASL_Sublogics

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski CASLBasicSpec Cas.CASLFORMULA Cas.SYMB_ITEMS

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Cas.SYMB_MAP_ITEMS

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CasS.CASLSign

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder CasM.CASLMor

c7e03d0708369f944b6f235057b39142a21599f2Mihai Codescu CasS.Symbol CasM.RawSymbol ProofTree

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder HasCASL Sublogic

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder BasicSpec Sentence SymbItems SymbMapItems

986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder Env Morphism Symbol RawSymbol () where

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sourceLogic CASL2HasCASL = CASL

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder sourceSublogic CASL2HasCASL = CasSub.top

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder targetLogic CASL2HasCASL = HasCASL

8e80792f474d154ff11762fac081a422e34f1accChristian Maeder mapSublogic CASL2HasCASL sl = Just $ sublogicUp $

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (if has_cons sl then sublogic_max need_hol else id)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder caslLogic

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder { HasSub.has_sub = CasSub.has_sub sl

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , HasSub.has_part = CasSub.has_part sl

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , HasSub.has_eq = CasSub.has_eq sl

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , HasSub.has_pred = CasSub.has_pred sl

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , HasSub.which_logic = case CasSub.which_logic sl of

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder CasSub.Atomic -> HasSub.Atomic

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder CasSub.Horn -> HasSub.Horn

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder CasSub.GHorn -> HasSub.GHorn

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder CasSub.Prenex -> HasSub.FOL -- at least for now

4c7f058cdd19ce67b2b5d4b7f69703d0f8a21e38Christian Maeder CasSub.FOL -> HasSub.FOL

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder CasSub.SOL -> HasSub.HOL

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder }

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder map_morphism CASL2HasCASL = return . mapMor

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder map_sentence CASL2HasCASL _ = return . toSentence

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder map_symbol CASL2HasCASL _ = Set.singleton . mapSym

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder map_theory CASL2HasCASL = return . mapTheory

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder has_model_expansion CASL2HasCASL = True

d79e02625778d20a5458078f979ff74aac67db61Christian Maeder is_weakly_amalgamable CASL2HasCASL = True

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder isInclusionComorphism CASL2HasCASL = True

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederfromOPTYPE :: Cas.OP_TYPE -> Type

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederfromOPTYPE (Cas.Op_type ok args res ps) = let

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder (total, arr) = case ok of

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Cas.Total -> (True, FunArr)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Cas.Partial -> (False, PFunArr)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder resTy = toType res

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder in if null args then if total then resTy else mkLazyType resTy

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski else mkFunArrType (mkProductTypeWithRange (map toType args) ps) arr resTy

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski

5e46b572ed576c0494768998b043d9d340594122Till MossakowskifromOpType :: CasS.OpType -> Type

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaederfromOpType = fromOPTYPE . CasS.toOP_TYPE

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederfromPREDTYPE :: Cas.PRED_TYPE -> Type

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederfromPREDTYPE (Cas.Pred_type args ps) =

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder if null args then mkLazyType $ unitTypeWithRange ps

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder else predType ps $ mkProductTypeWithRange (map toType args) ps

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaederfromPredType :: CasS.PredType -> Type

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaederfromPredType = fromPREDTYPE . CasS.toPRED_TYPE

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapTheory :: (CasS.TermExtension f, FormExtension f) =>

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (CasS.Sign f e, [Named (Cas.FORMULA f)]) -> (Env, [Named Sentence])

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapTheory (sig, sents) =

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski (mapSig (CasS.getConstructors sents) sig, map (mapNamed toSentence) sents)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian MaedermapSig :: Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian MaedermapSig = mapSigAux trId fromOpType fromPredType

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder-- | sort names or not translated

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapSigAux :: (Id -> Id) -> (CasS.OpType -> Type) -> (CasS.PredType -> Type)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder -> Set.Set (Id, CasS.OpType) -> CasS.Sign f e -> Env

68138d26bcddf5e89c30206aa83ab5ec006d170dChristian MaedermapSigAux trI trO trP constr sign =

4601edb679f0ba530bbb085b25d82a411cd070aaChristian Maeder let f1 = map ( \ (i, ty) ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (trI i, trO ty,

26d11a256b1433604a3dbc69913b520fff7586acChristian Maeder if Set.member (i, CasS.mkPartial ty)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder constr then ConstructData $ CasS.opRes ty

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder else NoOpDefn Op))

2b2f3b72e82e28b34db9c69af2d1ec38f228272eChristian Maeder $ CasS.mapSetToList $ CasS.opMap sign

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder f2 = map ( \ (i, ty) -> let pTy = trP ty in

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (trI i, pTy, NoOpDefn

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ if isPredType pTy then Pred else Fun))

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ CasS.mapSetToList $ CasS.predMap sign

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder insF (i, ty, defn) m =

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder let os = Map.findWithDefault Set.empty i m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in Map.insert i (Set.insert

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (OpInfo (simpleTypeScheme ty) Set.empty defn) os) m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in initialEnv

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { classMap = Map.empty,

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder typeMap = Map.fromList $ map

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder ( \ s -> (s, starTypeInfo

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski { superTypes = Set.delete s $

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder CasS.supersortsOf s sign

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder })) $ Set.toList $ CasS.sortSet sign,

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder assumps = foldr insF Map.empty (f1 ++ f2)}

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian MaedermapMor :: CasM.Morphism f e m -> Morphism

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedermapMor m = let tm = CasM.sort_map m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder f1 = map ( \ ((i, ot), (j, t)) ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder ((trId i, simpleTypeScheme $ fromOpType ot),

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (trId j, simpleTypeScheme $ mapType tm

5e46b572ed576c0494768998b043d9d340594122Till Mossakowski $ fromOpType ot { CasS.opKind = t })))

1f086d5155f47fdad9a0de4e46bbebb2c4b33d30Christian Maeder $ Map.toList $ CasM.op_map m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder f2 = map ( \ ((i, pt), j) ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder let ty = fromPredType pt

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in ( (trId i, simpleTypeScheme ty)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , (trId j, simpleTypeScheme $ mapType tm ty)))

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ Map.toList $ CasM.pred_map m

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in (mkMorphism (mapSig Set.empty $ CasM.msource m)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (mapSig Set.empty $ CasM.mtarget m))

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder { typeIdMap = tm , funMap = Map.fromList $ f2 ++ f1 }

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapSym :: CasS.Symbol -> Symbol

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapSym = mapSymAux trId fromOpType fromPredType

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskimapSymAux :: (Id -> Id) -> (CasS.OpType -> Type)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski -> (CasS.PredType -> Type) -> CasS.Symbol -> Symbol

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedermapSymAux trI trO trP s = let

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski n = CasS.symName s

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski i = trI n

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski in case CasS.symbType s of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski CasS.OpAsItemType ot -> idToOpSymbol i . simpleTypeScheme $ trO ot

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski CasS.PredAsItemType pt -> idToOpSymbol i . simpleTypeScheme $ trP pt

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder CasS.SortAsItemType -> idToTypeSymbol n rStar

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder CasS.SubsortAsItemType _ -> idToTypeSymbol n rStar

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitoQuant :: Cas.QUANTIFIER -> Quantifier

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoQuant Cas.Universal = Universal

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoQuant Cas.Existential = Existential

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoQuant Cas.Unique_existential = Unique

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoVarDecl :: Cas.VAR_DECL -> [GenVarDecl]

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoVarDecl (Cas.Var_decl vs s ps) =

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder map ( \ i -> GenVarDecl $

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder VarDecl (simpleIdToId i) (toType s) Other ps) vs

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian MaedertoSentence :: (CasS.TermExtension f, FormExtension f)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder => Cas.FORMULA f -> Sentence

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill MossakowskitoSentence f = case f of

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Cas.Sort_gen_ax cs b -> let

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (sorts, ops, smap) = Cas.recover_Sort_gen_ax cs

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski genKind = if b then Free else Generated

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapPart :: Cas.OpKind -> Partiality

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder mapPart cp = case cp of

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Cas.Total -> HasCASL.As.Total

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Cas.Partial -> HasCASL.As.Partial

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in DatatypeSen $ map ( \ s ->

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder DataEntry (Map.fromList smap) s genKind [] rStar

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder $ Set.fromList $ map ( \ (i, t) ->

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let args = map toType $ CasS.opArgs t in

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Construct (if isInjName i then Nothing else Just i)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (if null args then [] else [mkProductType args])

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (mapPart $ CasS.opKind t)

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski $ if null args then [] else

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski [map (\ a -> Select Nothing a HasCASL.As.Total) args])

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ filter ( \ (_, t) -> CasS.opRes t == s)

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder $ map ( \ o -> case o of

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Cas.Qual_op_name i t _ -> (trId i, CasS.toOpType t)

575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder _ -> error "CASL2HasCASL.toSentence") ops) sorts

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder _ -> Formula $ toTerm f

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertoTerm :: (CasS.TermExtension f, FormExtension f) => Cas.FORMULA f -> Term

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertoTerm f = foldFormula (transRecord $ showDoc f "") f

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertransRecord :: CasS.TermExtension f => String -> Record f Term Term

03136b84a0c70d877e227444f0875e209506b9e4Christian MaedertransRecord str = let err = error $ "CASL2HasCASL.unexpected formula: " ++ str

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder in (constRecord err err err)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder { foldQuantification = \ _ q -> QuantifiedTerm (toQuant q)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder . concatMap toVarDecl

3df765bba27034f17ba60ee9b90d7dbd3643ea9eChristian Maeder , foldJunction = \ _ j fs ps -> let

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder (n, op) = case j of

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Cas.Con -> (trueId, andId)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Cas.Dis -> (falseId, orId)

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder in case fs of

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder [] -> unitTerm n ps

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder _ -> toBinJunctor op fs ps

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder , foldRelation = \ _ f1 c f2 ps -> case c of

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Cas.Implication -> mkLogTerm implId ps f1 f2

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Cas.RevImpl -> mkLogTerm infixIf ps f2 f1

58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Cas.Equivalence -> mkLogTerm eqvId ps f1 f2

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , foldNegation = \ _ frm ps -> mkTerm notId notType [] ps frm

0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder , foldAtom = \ _ b -> unitTerm $ if b then trueId else falseId

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldEquation = \ o t1 e t2 ps ->

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let Cas.Equation c1 _ _ _ = o in

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder mkEqTerm (if e == Cas.Existl then exEq else eqId)

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (typeOfTerm c1) ps t1 t2

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldPredication = \ _ qpn args qs ->

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder let Cas.Qual_pred_name ui pty@(Cas.Pred_type ts _) ps = qpn

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder i = trId ui

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder sc = simpleTypeScheme $ fromPREDTYPE pty

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder p = QualOp Pred (PolyId i [] ps) sc [] Infer ps

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder in if null args then p else TypedTerm

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (ApplTerm p (mkTupleTerm (zipWith

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (\ tr ty -> TypedTerm tr Inferred (toType ty) ps)

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder args ts) qs) qs)

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder Inferred unitType ps

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldDefinedness = \ o t ps ->

0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder let Cas.Definedness c _ = o in

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder mkTerm defId defType [typeOfTerm c] ps t

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldMembership = \ _ t -> TypedTerm t InType . toType

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder , foldQuantOp = \ _ uo ty frm -> let o = trId uo in

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder QuantifiedTerm Universal

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder [GenVarDecl $ VarDecl o (fromOPTYPE ty) Other nullRange]

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder (qualName2var o frm) nullRange

0b6f6d3eeb7b3b36292e60f1b3da5a5ce42eef1aChristian Maeder , foldQuantPred = \ _ up ty frm -> let p = trId up in

200849122a9c65773e5b2ba8084ac3490d0490b5Christian Maeder QuantifiedTerm Universal

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder [GenVarDecl $ VarDecl p (fromPREDTYPE ty) Other nullRange]

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder (qualName2var p frm) nullRange

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , foldQual_var = \ _ v ty ->

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder QualVar . VarDecl (simpleIdToId v) (toType ty) Other

03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder , foldApplication = \ _ qon args qs ->

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder let Cas.Qual_op_name ui ot ps = qon

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder i = trId ui

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder sc = simpleTypeScheme $ fromOPTYPE ot

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder o = QualOp Op (PolyId i [] ps) sc [] Infer ps

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder at = CasS.toOpType ot

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder in if null args then o else TypedTerm

a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (ApplTerm o (mkTupleTerm (zipWith

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder (\ tr ty -> TypedTerm tr Inferred (toType ty) ps)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder args $ CasS.opArgs at) qs) qs)

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder Inferred (toType $ CasS.opRes at) ps

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldSorted_term = \ _ trm -> TypedTerm trm OfType . toType

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldCast = \ _ trm -> TypedTerm trm AsType . toType

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldConditional = \ o t1 f t2 ps ->

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder let Cas.Conditional c1 _ _ _ = o in

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder mkTerm whenElse whenType [typeOfTerm c1] ps

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder $ TupleTerm [t1, f, t2] ps

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder , foldSort_gen_ax = \ _ cs _ ->

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder error $ "unexpected sort generation constraint: "

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ++ unlines (map (`showDoc` "") $ recoverType cs)

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder ++ "in: " ++ str

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder }

7a47fbe6b987bd69a5056ce5d00fc8710f6c5e8aChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedertypeOfTerm :: CasS.TermExtension f => Cas.TERM f -> Type

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaedertypeOfTerm = toType . CasS.sortOfTerm

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian Maeder-- | replace qualified names by variables in second order formulas

e82587ca2892d246aa4405c2f5b9f30f287f9ebfChristian MaederqualName2var :: Id -> Term -> Term

2561b4bfc45d280ee2be8a7870314670e4e682e4Christian MaederqualName2var i = HasFold.foldTerm mapRec

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder { foldQualOp = \ t _ (PolyId j _ _) (TypeScheme _ ty _) _ _ ps ->

01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder if i == j then QualVar $ VarDecl i ty Other ps else t }

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder-- | the invisible identifier is reserved for application

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertrId :: Id -> Id

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian MaedertrId i@(Id ts cs ps) = if null cs && all isPlace ts then

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder Id [genNumVar "empty" $ length ts] cs ps else i

e01299e9b22b96b31b720ca1e9f9f5f25af9b024Christian Maeder