HasCASL2IsabelleHOL.hs revision bba825b39570777866d560bfde3807731131097e
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederModule : $Header$
c58a94c44b76b072ace930f2126c889c0b64cb2aChristian MaederCopyright : (c) Sonja Groening, C. Maeder, Uni Bremen 2003-2006
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederMaintainer : maeder@tzi.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : non-portable (imports Logic.Logic)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederThis embedding comorphism from HasCASL to Isabelle-HOL is an old
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maederversion that can be deleted as soon as case terms are implemented by
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian MaederPCoClTyConsHOL2IsabelleHOL.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule Comorphisms.HasCASL2IsabelleHOL where
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Isabelle.IsaSign as IsaSign
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport qualified Data.Map as Map
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Data.List (elemIndex, nub)
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Data.Maybe (catMaybes)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | The identity of the comorphism
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederdata HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederinstance Language HasCASL2IsabelleHOL -- default definition is okay
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinstance Comorphism HasCASL2IsabelleHOL
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder HasCASL Sublogic
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder BasicSpec Le.Sentence SymbItems SymbMapItems
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Symbol RawSymbol ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Isabelle () () IsaSign.Sentence () ()
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder IsabelleMorphism () () () where
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder sourceLogic HasCASL2IsabelleHOL = HasCASL
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder sourceSublogic HasCASL2IsabelleHOL = sublogic_min noSubtypes noClasses
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder targetLogic HasCASL2IsabelleHOL = Isabelle
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid
836e72a3c413366ba9801726f3b249c7791cb9caChristian Maeder then Just () else Nothing
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder map_theory HasCASL2IsabelleHOL = mkTheoryMapping transSignature
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder (map_sentence HasCASL2IsabelleHOL)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder map_morphism = mapDefaultMorphism
cf3232cec840a6945667bdb06f5b47b22243bc8fChristian Maeder map_sentence HasCASL2IsabelleHOL sign phi =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder case transSentence sign phi of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> warning (mkSen true)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder "translation of sentence not implemented" nullRange
975642b989852fc24119c59cf40bc1af653608ffChristian Maeder Just (ts) -> return $ mkSen ts
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder map_symbol = errMapSymbol
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- * Signature
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederbaseSign :: BaseSig
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederbaseSign = MainHC_thy
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedertransSignature :: Env -> Result (IsaSign.Sign,[Named IsaSign.Sentence])
975642b989852fc24119c59cf40bc1af653608ffChristian MaedertransSignature sign =
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder baseSig = baseSign,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- translation of typeconstructors
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder tsig = emptyTypeSig
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder { arities = Map.foldWithKey extractTypeName
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (typeMap sign) },
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- translation of operation declarations
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder constTab = Map.foldWithKey insertOps
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (assumps sign),
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- translation of datatype declarations
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder domainTab = transDatatype (typeMap sign),
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder showLemmas = True },
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder extractTypeName tyId typeInfo m =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder if isDatatypeDefn typeInfo then m
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else Map.insert (showIsaTypeT tyId baseSign) [(isaTerm, [])] m
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- translate the kind here!
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder isDatatypeDefn t = case typeDefn t of
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder DatatypeDefn _ -> True
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder insertOps name ops m =
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder let infos = opInfos ops
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder in if isSingle infos then
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder let transOp = transOpInfo (head infos)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder in case transOp of
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder Map.insert (mkVName $ showIsaConstT name baseSign) op m
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let transOps = map transOpInfo infos
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder in foldl (\ m' (transOp,i) ->
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder case transOp of
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (mkVName $ showIsaConstIT name i baseSign)
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> m')
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder m (zip transOps [1::Int ..])
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * translation of a type in an operation declaration
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- extract type from OpInfo
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder-- omit datatype constructors
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedertransOpInfo :: OpInfo -> Maybe Typ
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian MaedertransOpInfo (OpInfo t _ opDef) =
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder case opDef of
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder ConstructData _ -> Nothing
31242f7541fd6ef179e4eb5be7522ddf54ae397bChristian Maeder _ -> Just (transOpType t)
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder-- operation type
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedertransOpType :: TypeScheme -> Typ
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedertransOpType (TypeScheme _ op _) = transType op
628310b42327ad76ce471caf0dde6563d6fa6307Christian MaedertransType :: Type -> Typ
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaedertransType t = case getTypeAppl t of
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (TypeName tid _ n, tyArgs) -> let num = length tyArgs in
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder if n == 0 then
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder if tid == unitTypeId && null tyArgs then boolType
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else if tid == lazyTypeId && num == 1 then
628310b42327ad76ce471caf0dde6563d6fa6307Christian Maeder transType $ head tyArgs
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else if isArrow tid && num == 2 then
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let [t1, t2] = tyArgs
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder tr = transType t2
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder in mkFunType (transType t1) $
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder if isPartialArrow tid && not (isPredType t)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder then mkOptionType tr else tr
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder else if isProductId tid && num > 1 then
cbbb99ab370e6ad265b14a37e7d35b7f08a50d43Christian Maeder foldl1 prodType $ map transType tyArgs
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian Maeder else Type (showIsaTypeT tid baseSign) [] $ map transType tyArgs
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maeder else TFree (showIsaTypeT tid baseSign) []
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder -- type arguments are not allowed here!
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> error $ "transType " ++ showDoc t "\n" ++ show t
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * translation of a datatype declaration
ac07a6558423dae7adc488ed9092cd8e9450a29dChristian MaedertransDatatype :: TypeMap -> DomainTab
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedertransDatatype tm = map transDataEntry (Map.fold extractDataypes [] tm)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder where extractDataypes ti des = case typeDefn ti of
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder DatatypeDefn de -> des++[de]
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder-- datatype with name (tyId) + args (tyArgs) and alternatives
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian MaedertransDataEntry :: DataEntry -> [DomainEntry]
154d4152b38c55c3c4ab8f35578669a65fc04df9Christian MaedertransDataEntry (DataEntry _ tyId Le.Free tyArgs _ alts) =
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder [(transDName tyId tyArgs, map transAltDefn alts)]
b49276c9f50038e0bd499ad49f7bd6444566a834Christian Maeder where transDName ti ta = Type (showIsaTypeT ti baseSign) []
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder $ map transTypeArg ta
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedertransDataEntry _ = error "HasCASL2IsabelleHOL.transDataEntry"
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder-- arguments of datatype's typeconstructor
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedertransTypeArg :: TypeArg -> Typ
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransAltDefn :: AltDefn -> (VName, [Typ])
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransAltDefn (Construct opId ts Total _) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder let ts' = map transType ts
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder in case opId of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Just opId' -> (mkVName $ showIsaConstT opId' baseSign, ts')
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> (mkVName "", ts')
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransAltDefn _ = error "HasCASL2IsabelleHOL.transAltDefn"
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- simple variables
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransVar :: Var -> VName
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransVar v = mkVName $ showIsaConstT v baseSign
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedertransSentence :: Env -> Le.Sentence -> Maybe IsaSign.Term
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransSentence sign s = case s of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Le.Formula t -> Just (transTerm sign t)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder DatatypeSen _ -> Nothing
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder ProgEqSen _ _ _pe -> Nothing
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- disambiguate operation names
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransOpId :: Env -> UninstOpId -> TypeScheme -> String
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransOpId sign op ts =
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder case (do ops <- Map.lookup op (assumps sign)
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if isSingle (opInfos ops) then return $ showIsaConstT op baseSign
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder else do i <- elemIndex ts (map opType (opInfos ops))
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder return $ showIsaConstIT op (i+1) baseSign) of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Just str -> str
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder Nothing -> showIsaConstT op baseSign
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransProgEq :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransProgEq sign (ProgEq pat t _) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (transPattern sign pat, transPattern sign t)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransTerm sign trm = case trm of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder QualVar (VarDecl var _ _ _) ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder termAppl conSome $ IsaSign.Free (transVar var)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder QualOp _ (InstOpId opId _ _) ts _ ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder if opId == trueId then true
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else if opId == falseId then false
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder else termAppl conSome (conDouble (transOpId sign opId ts))
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder QuantifiedTerm quan varDecls phi _ ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder let quantify q gvd phi' = case gvd of
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder GenVarDecl (VarDecl var _ _ _) ->
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder termAppl (conDouble $ qname q)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder $ Abs (IsaSign.Free $ transVar var) phi' NotCont
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder GenTypeVarDecl _ -> phi'
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder qname Universal = allS
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder qname Existential = exS
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder qname Unique = ex1S
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder in foldr (quantify quan) (transTerm sign phi) varDecls
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder TypedTerm t _ _ _ -> transTerm sign t
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder LambdaTerm pats p body _ ->
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder let lambdaAbs f = if null pats then termAppl conSome
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (Abs (IsaSign.Free $ mkVName "dummyVar")
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (f sign body) NotCont)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder else termAppl conSome (foldr (abstraction sign)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder (f sign body)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- distinguishes between partial and total lambda abstraction
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder -- total lambda bodies are of type 'a' instead of type 'a option'
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Partial -> lambdaAbs transTerm
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder Total -> lambdaAbs transTotalLambda
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder LetTerm As.Let peqs body _ ->
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder IsaSign.Let (map (transProgEq sign) peqs) $ transTerm sign body
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder TupleTerm ts@(_ : _) _ ->
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder foldl1 (binConst pairC) (map (transTerm sign) ts)
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder ApplTerm t1 t2 _ -> transAppl sign Nothing t1 t2
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder CaseTerm t peqs _ ->
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- flatten case alternatives
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder let alts = arangeCaseAlts sign peqs
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- introduces new case statement if case variable is
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder -- a term application that may evaluate to 'Some x' or 'None'
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder QualVar (VarDecl decl _ _ _) ->
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Case (IsaSign.Free (transVar decl)) alts
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> Case (transTerm sign t)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder [(conDouble "None", conDouble "None"),
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (App conSome (IsaSign.Free (mkVName "caseVar")) NotCont,
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder Case (IsaSign.Free (mkVName "caseVar")) alts)]
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder _ -> error $ "HasCASL2IsabelleHOL.transTerm " ++ showDoc trm "\n"
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertransAppl :: Env -> Maybe As.Type -> As.Term -> As.Term -> IsaSign.Term
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertransAppl s typ t' t'' = case t'' of
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder TupleTerm [] _ -> transTerm s t'
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> case t' of
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder QualVar (VarDecl _ ty _ _) -> transApplOp s ty t' t''
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder QualOp _ (InstOpId opId _ _) (TypeScheme _ ty _) _ ->
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder if elem opId $ map fst bList then
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -- logical formulas are translated seperatly (transLog)
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder if opId == whenElse then transWhenElse s t''
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder else transLog s opId t' t''
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder else transApplOp s ty t' t''
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder -- distinguishes between partial and total term application
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder TypedTerm tt' _ typ' _ -> transAppl s (Just typ') tt' t''
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ -> maybe (mkApp "app" s t' t'')
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder ( \ ty -> transApplOp s ty t' t'') typ
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaedermkApp :: String -> Env -> As.Term -> As.Term -> IsaSign.Term
81946e2b3f6dde6167f48769bd02c7a634736856Christian MaedermkApp s sg tt tt' = termAppl (termAppl (conDouble s) (transTerm sg tt))
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder (transTerm sg tt')
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertransApplOp :: Env -> As.Type -> As.Term -> As.Term -> IsaSign.Term
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertransApplOp s typ tt tt' = if isPredType typ then mkApp "pApp" s tt tt'
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder else case getTypeAppl typ of
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder (TypeName tid _ 0, [_, _]) | isArrow tid ->
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder if isPartialArrow tid then mkApp "app" s tt tt'
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder else mkApp "apt" s tt tt'
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder _ -> mkApp "app" s tt tt'
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder-- translation formulas with logical connectives
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaedertransLog :: Env -> Id -> As.Term -> As.Term -> IsaSign.Term
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertransLog sign opId opTerm t = case t of
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder TupleTerm [l' , r'] _
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder | opId == andId -> binConj l r
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == orId -> binDisj l r
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == implId -> binImpl l r
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == infixIf -> binImpl r l
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == eqvId -> binEq l r
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == exEq -> binConj (binEq l r) $
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder binConj (termAppl defOp l) $
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder termAppl defOp r
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder | opId == eqId -> binEq l r
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder where l = transTerm sign l'
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder r = transTerm sign r'
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder _ | opId == notId -> termAppl notOp (transTerm sign t)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | opId == defId -> termAppl defOp (transTerm sign t)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder | otherwise -> termAppl (transTerm sign opTerm) (transTerm sign t)
_ -> error "HasCASL2IsabelleHOL.transWhenElse.tuple"
_ -> error "HasCASL2IsabelleHOL.transWhenElse"
error "HasCASL2IsabelleHOL.abstraction"
IsaSign.Free (transVar var)
IsaSign.Free (transVar var)
if (null pats) then Abs (IsaSign.Free (mkVName "dummyVar"))
from HasCASL to Isabelle/HOL patterns may take the form:
extractIds _ = error "HasCASL2Isabelle.extractIds"
findInMap :: Ord k => k -> Map.Map k a -> a
findInMap k m = maybe (error "HasCASL2isabelleHOL.findInMap") id $
Map.lookup k m
_ -> error "HasCASL2IsabelleHOL.getTypeName"
_ -> error "HasCASL2IsabelleHOL.name (of type)"
cons :: Maybe As.Term,
term :: As.Term } deriving (Show)
matriArg :: Pattern -> As.Term -> CaseMatrix
_ -> error "HasCASL2IsabelleHOL.matriArg"
| null peqs = error "HasCASL2IsabelleHOL.testPEQs"
shrinkPat :: CaseMatrix -> As.Term
Nothing -> error "HasCASL2IsabelleHOL.shrinkPat"
termIsVar :: As.Term -> Bool
termHasNoArg :: As.Term -> Bool
IsaSign.Free (transVar var)
transPat _ _ = error "HasCASL2IsabelleHOL.transPat"