HasCASL2IsabelleHOL.hs revision bba825b39570777866d560bfde3807731131097e
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder{- |
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
ea03c5d09694b4a966fbd19d46cfa5772648d95fChristian Maeder
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederMaintainer : maeder@tzi.de
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian MaederStability : provisional
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian MaederPortability : non-portable (imports Logic.Logic)
4b0a4c7dea0f67a233dcc42ce9bb18d36de109aeChristian Maeder
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 Maeder-}
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule Comorphisms.HasCASL2IsabelleHOL where
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maederimport Logic.Logic as Logic
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maederimport Logic.Comorphism
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maederimport HasCASL.Logic_HasCASL
dc6b48bb46df8e56da3491c98476e6da0d1d5d1dChristian Maederimport HasCASL.Sublogic
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport HasCASL.Le as Le
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maederimport HasCASL.As as As
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport HasCASL.AsUtils
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport HasCASL.Builtin
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Isabelle.IsaSign as IsaSign
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Isabelle.IsaConsts
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maederimport Isabelle.Logic_Isabelle
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport Isabelle.Translate
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Common.DocUtils
0a85c4dc6f4bba88e1994e8f1cd3657b6503b220Christian Maederimport Common.Id
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maederimport Common.Result
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maederimport qualified Data.Map as Map
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maederimport Common.AS_Annotation
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maederimport Data.List (elemIndex, nub)
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maederimport Data.Maybe (catMaybes)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- | The identity of the comorphism
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederdata HasCASL2IsabelleHOL = HasCASL2IsabelleHOL deriving Show
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maederinstance Language HasCASL2IsabelleHOL -- default definition is okay
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maederinstance Comorphism HasCASL2IsabelleHOL
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder HasCASL Sublogic
23f8d286586ff38a9e73052b2c7c04c62c5c638fChristian Maeder BasicSpec Le.Sentence SymbItems SymbMapItems
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder Env Morphism
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Symbol RawSymbol ()
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder Isabelle () () IsaSign.Sentence () ()
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder IsaSign.Sign
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
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
e8a2ca3a7b3e9a19ef03b6b1c0b5d03dbad6463cChristian Maeder-- * Signature
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederbaseSign :: BaseSig
9348e8460498ddfcd9da11cd8b5794c06023e004Christian MaederbaseSign = MainHC_thy
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedertransSignature :: Env -> Result (IsaSign.Sign,[Named IsaSign.Sentence])
975642b989852fc24119c59cf40bc1af653608ffChristian MaedertransSignature sign =
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder return (IsaSign.emptySign {
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder baseSig = baseSign,
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder -- translation of typeconstructors
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder tsig = emptyTypeSig
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder { arities = Map.foldWithKey extractTypeName
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Map.empty
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder (typeMap sign) },
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- translation of operation declarations
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder constTab = Map.foldWithKey insertOps
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Map.empty
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder (assumps sign),
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder -- translation of datatype declarations
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder domainTab = transDatatype (typeMap sign),
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder showLemmas = True },
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder [] )
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder where
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 _ -> False
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
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Just op ->
e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder Map.insert (mkVName $ showIsaConstT name baseSign) op m
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder Nothing -> m
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder else
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder let transOps = map transOpInfo infos
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder in foldl (\ m' (transOp,i) ->
502ed7ed7fecd10b6d0c83cdd48a244ec45e840aChristian Maeder case transOp of
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder Just typ -> Map.insert
81946e2b3f6dde6167f48769bd02c7a634736856Christian Maeder (mkVName $ showIsaConstIT name i baseSign)
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder typ m'
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder Nothing -> m')
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder m (zip transOps [1::Int ..])
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * translation of a type in an operation declaration
fd5d3885a092ac0727fa2436cdfc3b248318ebd8Christian Maeder
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)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
76fa667489c5e0868ac68de9f0253ac10f73d0b5Christian Maeder-- operation type
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedertransOpType :: TypeScheme -> Typ
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaedertransOpType (TypeScheme _ op _) = transType op
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- types
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
c9892acbf03a509d874ac6d79b9a2cb09042e0dcChristian Maeder
9348e8460498ddfcd9da11cd8b5794c06023e004Christian Maeder-- * translation of a datatype declaration
7c57322afb6342e5cc8b1fdc96050b707407fc61Christian Maeder
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]
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder _ -> des
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
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"
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
b603f34b79bc0992e5d74f484e5bdc9f9c2346c6Christian Maeder-- arguments of datatype's typeconstructor
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaedertransTypeArg :: TypeArg -> Typ
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransTypeArg ta = TFree (showIsaTypeT (getTypeVar ta) baseSign) []
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- datatype alternatives/constructors
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
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder-- * Formulas
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder-- simple variables
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransVar :: Var -> VName
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransVar v = mkVName $ showIsaConstT v baseSign
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
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
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 Maeder
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransProgEq :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransProgEq sign (ProgEq pat t _) =
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder (transPattern sign pat, transPattern sign t)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder-- terms
f8c07dc6526e0134d66885d461a30abadc2c6038Christian MaedertransTerm :: Env -> As.Term -> IsaSign.Term
afa6848d579d235c9677e1ab477916df8e5ae11aChristian MaedertransTerm sign trm = case trm of
afa6848d579d235c9677e1ab477916df8e5ae11aChristian Maeder QualVar (VarDecl var _ _ _) ->
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder termAppl conSome $ IsaSign.Free (transVar var)
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder
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))
f8c07dc6526e0134d66885d461a30abadc2c6038Christian Maeder
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)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder pats)
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder in case p of
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 in case t of
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 Maeder ++ show trm
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
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
4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder
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')
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
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
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)
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder
-- | when else statement
transWhenElse :: Env -> As.Term -> IsaSign.Term
transWhenElse sign t =
case t of
TupleTerm terms _ ->
let ts = (map (transTerm sign) terms)
in case ts of
[i, c, e] -> If c i e NotCont
_ -> error "HasCASL2IsabelleHOL.transWhenElse.tuple"
_ -> error "HasCASL2IsabelleHOL.transWhenElse"
-- * translation of lambda abstractions
-- form Abs(pattern term)
abstraction :: Env -> As.Term -> IsaSign.Term -> IsaSign.Term
abstraction sign pat body =
Abs (transPattern sign pat) body NotCont where
-- Abs (transPattern sign pat) body NotCont where
getType t =
case t of
QualVar (VarDecl _ typ _ _) -> transType typ
TypedTerm _ _ typ _ -> transType typ
TupleTerm terms _ -> evalTupleType terms
_ ->
error "HasCASL2IsabelleHOL.abstraction"
evalTupleType t = foldr1 prodType (map getType t)
-- translation of lambda patterns
-- a pattern keeps his type 't', isn't translated to 't option'
transPattern :: Env -> As.Term -> IsaSign.Term
transPattern _ (QualVar (VarDecl var _ _ _)) =
IsaSign.Free (transVar var)
transPattern sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) $ map (transPattern sign) terms
transPattern _ (QualOp _ (InstOpId opId _ _) _ _) =
conDouble $ showIsaConstT opId baseSign
transPattern sign (TypedTerm t _ _ _) = transPattern sign t
transPattern sign (ApplTerm t1 t2 _) =
App (transPattern sign t1) (transPattern sign t2) NotCont
transPattern sign t = transTerm sign t
-- translation of total lambda abstraction bodies
transTotalLambda :: Env -> As.Term -> IsaSign.Term
transTotalLambda _ (QualVar (VarDecl var _ _ _)) =
IsaSign.Free (transVar var)
transTotalLambda sign t@(QualOp _ (InstOpId opId _ _) _ _) =
if opId == trueId || opId == falseId then transTerm sign t
else conDouble $ showIsaConstT opId baseSign
transTotalLambda sign (ApplTerm term1 term2 _) =
termAppl (transTotalLambda sign term1) $ transTotalLambda sign term2
transTotalLambda sign (TypedTerm t _ _ _) = transTotalLambda sign t
transTotalLambda sign (LambdaTerm pats part body _) =
case part of
Partial -> lambdaAbs transTerm
Total -> lambdaAbs transTotalLambda
where
lambdaAbs f =
if (null pats) then Abs (IsaSign.Free (mkVName "dummyVar"))
(f sign body) NotCont
-- if (null pats) then Abs [("dummyVar", noType)]
else foldr (abstraction sign) (f sign body) pats
transTotalLambda sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) $ map (transTotalLambda sign) terms
transTotalLambda sign (CaseTerm t pEqs _) =
Case (transTotalLambda sign t) $ map transCaseAltTotal pEqs
where transCaseAltTotal (ProgEq pat trm _) =
(transPat sign pat, transTotalLambda sign trm)
transTotalLambda sign t = transTerm sign t
-- * translation of case alternatives
{- Annotation concerning Patterns:
Following the HasCASL-Summary and the limits of the encoding
from HasCASL to Isabelle/HOL patterns may take the form:
QualVar, QualOp, ApplTerm, TupleTerm and TypedTerm
-}
-- Input: List of case alternative (one pattern per term)
-- Functionality: Tests wheter pattern is a variable -> case alternative is
-- translated
arangeCaseAlts :: Env -> [ProgEq]-> [(IsaSign.Term, IsaSign.Term)]
arangeCaseAlts sign peqs
| and (map patIsVar peqs) = map (transCaseAlt sign) peqs
| otherwise = sortCaseAlts sign peqs
{- Input: List of case alternatives, that patterns does consist of
datatype constructors (with arguments) or tupels
Functionality: Groups case alternatives by leading
pattern-constructor each pattern group is flattened
-}
sortCaseAlts :: Env -> [ProgEq]-> [(IsaSign.Term, IsaSign.Term)]
sortCaseAlts sign peqs =
let consList
| null peqs = error "No case alternatives."
| otherwise = getCons sign (getName (head peqs))
groupedByCons = nub (map (groupCons peqs) consList)
in map (flattenPattern sign) groupedByCons
-- Returns a list of the constructors of the used datatype
getCons :: Env -> TypeId -> [UninstOpId]
getCons sign tyId =
extractIds (typeDefn (findInMap tyId (typeMap sign)))
where extractIds (DatatypeDefn (DataEntry _ _ _ _ _ altDefns)) =
catMaybes (map stripConstruct altDefns)
extractIds _ = error "HasCASL2Isabelle.extractIds"
stripConstruct (Construct i _ _ _) = i
findInMap :: Ord k => k -> Map.Map k a -> a
findInMap k m = maybe (error "HasCASL2isabelleHOL.findInMap") id $
Map.lookup k m
-- Extracts the type of the used datatype in case patterns
getName :: ProgEq -> TypeId
getName (ProgEq pat _ _) = (getTypeName pat)
getTypeName :: Pattern -> TypeId
getTypeName p =
case p of
QualVar (VarDecl _ typ _ _) -> name typ
QualOp _ _ (TypeScheme _ typ _) _ -> name typ
TypedTerm _ _ typ _ -> name typ
ApplTerm t _ _ -> getTypeName t
TupleTerm ts _ -> getTypeName (head ts)
_ -> error "HasCASL2IsabelleHOL.getTypeName"
where name tp = case getTypeAppl tp of
(TypeName tyId _ 0, tyArgs) -> let num = length tyArgs in
if isArrow tyId && num == 2 then
name $ head $ tail tyArgs
else if isProductId tyId && num > 1 then
name $ head tyArgs
else tyId
_ -> error "HasCASL2IsabelleHOL.name (of type)"
-- Input: Case alternatives and name of one constructor
-- Functionality: Filters case alternatives by constructor's name
groupCons :: [ProgEq] -> UninstOpId -> [ProgEq]
groupCons peqs name = filter hasSameName peqs
where hasSameName (ProgEq pat _ _) =
hsn pat
hsn pat =
case pat of
QualOp _ (InstOpId n _ _) _ _ -> n == name
ApplTerm t1 _ _ -> hsn t1
TypedTerm t _ _ _ -> hsn t
TupleTerm _ _ -> True
_ -> False
-- Input: List of case alternatives with same leading constructor
-- Functionality: Tests whether the constructor has no arguments, if so
-- translates case alternatives
flattenPattern :: Env -> [ProgEq] -> (IsaSign.Term, IsaSign.Term)
flattenPattern sign peqs = case peqs of
[] -> error "Missing constructor alternative in case pattern."
[h] -> transCaseAlt sign h
-- at this stage there are patterns left which use 'ApplTerm' or 'TupleTerm'
-- or the 'TypedTerm' variant of one of them
_ -> let m = concentrate (matricize peqs) sign in
transCaseAlt sign (ProgEq (shrinkPat m) (term m) nullRange)
data CaseMatrix = CaseMatrix { patBrand :: PatBrand,
cons :: Maybe As.Term,
args :: [Pattern],
newArgs :: [Pattern],
term :: As.Term } deriving (Show)
data PatBrand = Appl | Tuple | QuOp | QuVar deriving (Eq, Show)
instance Eq CaseMatrix where
(==) cmx cmx' = (patBrand cmx == patBrand cmx')
&& (args cmx == args cmx')
&& (term cmx == term cmx')
&& (cons cmx == cons cmx')
&& (newArgs cmx == newArgs cmx')
{- First of all a matrix is allocated (matriArg) with the arguments of a
constructor resp. of a tuple. They're binded with the term, that would
be executed if the pattern matched. Then the resulting list of
matrices is grouped by the leading argument. (groupArgs) Afterwards -
if a list of grouped arguments has more than one element - the last
pattern argument (in the list 'patterns') is replaced by a new variable.
n patterns are reduced to one pattern.
This procedure is repeated until there's only one case alternative
for each constructor.
-}
-- Functionality: turns ProgEq into CaseMatrix
matricize :: [ProgEq] -> [CaseMatrix]
matricize = map matriPEq
matriPEq :: ProgEq -> CaseMatrix
matriPEq (ProgEq pat altTerm _) = matriArg pat altTerm
matriArg :: Pattern -> As.Term -> CaseMatrix
matriArg pat cTerm =
case pat of
ApplTerm t1 t2 _ -> let (c, p) = stripAppl t1 (Nothing, [])
in
CaseMatrix { patBrand = Appl,
cons = c,
args = p ++ [t2],
newArgs = [],
term = cTerm }
TupleTerm ts _ -> CaseMatrix { patBrand = Tuple,
cons = Nothing,
args = ts,
newArgs = [],
term = cTerm }
TypedTerm t _ _ _ -> matriArg t cTerm
qv@(QualVar _) -> CaseMatrix { patBrand = QuVar,
cons = Nothing,
args = [qv],
newArgs = [],
term = cTerm }
qo@(QualOp _ _ _ _) -> CaseMatrix { patBrand = QuOp,
cons = Nothing,
args = [qo],
newArgs = [],
term = cTerm }
_ -> error "HasCASL2IsabelleHOL.matriArg"
-- Assumption: The innermost term of a case-pattern consisting of a ApplTerm
-- is a QualOp, that is a datatype constructor
where stripAppl ct tp = case ct of
TypedTerm (ApplTerm q@(QualOp _ _ _ _) t' _) _ _ _ ->
(Just q, [t'] ++ snd tp)
TypedTerm (ApplTerm (TypedTerm
q@(QualOp _ _ _ _) _ _ _) t' _) _ _ _ -> (Just q, [t'] ++ snd tp)
TypedTerm (ApplTerm t' t'' _) _ _ _ ->
stripAppl t' (fst tp, [t''] ++ snd tp)
ApplTerm q@(QualOp _ _ _ _) t' _ -> (Just q, [t'] ++ snd tp)
ApplTerm (TypedTerm
q@(QualOp _ _ _ _) _ _ _) t' _ -> (Just q, [t'])
ApplTerm t' t'' _ ->
stripAppl t' (fst tp, [t''] ++ snd tp)
-- TypedTerm t' _ _ _ -> stripAppl t' tp
q@(QualOp _ _ _ _) -> (Just q, snd tp)
_ -> (Nothing, [ct] ++ snd tp)
-- Input: List with CaseMatrix of same leading constructor pattern
-- Functionality: First: Groups CMs so that these CMs are in one list
-- that only differ in their last argument
-- then: reduces list of every CMslist to one CM
concentrate :: [CaseMatrix] -> Env -> CaseMatrix
concentrate cmxs sign = case map (redArgs sign) $
nub $ map (groupByArgs cmxs) [0..(length cmxs-1)] of
[h] -> h
l -> concentrate l sign
groupByArgs :: [CaseMatrix] -> Int -> [CaseMatrix]
groupByArgs cmxs i
| and (map null (map args cmxs)) = cmxs
| otherwise = (filter equalPat cmxs)
where patE = init (args (cmxs !! i))
equalPat cmx = isSingle (args cmx) || init (args cmx) == patE
redArgs :: Env -> [CaseMatrix] -> CaseMatrix
redArgs sign cmxs
| and (map (testPatBrand Appl) cmxs) = redAppl cmxs sign
| and (map (testPatBrand Tuple) cmxs) = redAppl cmxs sign
| isSingle cmxs = head cmxs
| otherwise = head cmxs
where testPatBrand pb cmx = pb == patBrand cmx
{- Input: List of CMs thats leading constructor and arguments except
the last one are equal
Functionality: Reduces n CMs to one with same last argument in
pattern (perhaps a new variable
-}
redAppl :: [CaseMatrix] -> Env -> CaseMatrix
redAppl cmxs sign
| and (map null (map args cmxs)) = head cmxs
| isSingle cmxs =
(head cmxs) { args = init $ args $ head cmxs,
newArgs = last (args $ head cmxs) : newArgs (head cmxs) }
| and (map termIsVar lastArgs) = substVar (head cmxs)
| otherwise = substTerm (head cmxs)
where terms = map term cmxs
lastArgs = map last (map args cmxs)
varName = "caseVar" ++ show (length (args (head cmxs)))
varId = (mkId [(mkSimpleId varName)])
newVar = QualVar (VarDecl varId (TypeName varId rStar 1)
Other nullRange)
newPeqs = (map newProgEq (zip lastArgs terms))
newPeqs' = recArgs sign newPeqs
substVar cmx
| null (args cmx) = cmx
| isSingle (args cmx) =
cmx { args = [],
newArgs = last(args cmx) : (newArgs cmx) }
| otherwise =
cmx { args = init (args cmx),
newArgs = last(args cmx) : (newArgs cmx) }
substTerm cmx
| null (args cmx) = cmx
| isSingle (args cmx) =
cmx { args = [],
newArgs = newVar : (newArgs cmx),
term = CaseTerm newVar newPeqs' nullRange }
| otherwise =
cmx { args = init(args cmx),
newArgs = newVar : (newArgs cmx),
term = CaseTerm newVar newPeqs' nullRange }
newProgEq (p, t) = ProgEq p t nullRange
-- Input: ProgEqs that were build to replace an argument
-- with a case statement
-- Functionality:
recArgs :: Env -> [ProgEq] -> [ProgEq]
recArgs sign peqs
| isSingle groupedByCons
|| null groupedByCons = []
| otherwise = doPEQ groupedByCons []
where consList
| null peqs = error "No case alternatives."
| otherwise = getCons sign (getName (head peqs))
groupedByCons = map (groupCons peqs) consList
doPEQ [] res = res
doPEQ (g:gByCs) res
| isSingle g = doPEQ gByCs (res ++ g)
| otherwise = doPEQ gByCs (res ++ [(toPEQ (testPEQs sign g))])
toPEQ cmx = ProgEq (shrinkPat cmx) (term cmx) nullRange
testPEQs sig ps
| null peqs = error "HasCASL2IsabelleHOL.testPEQs"
| otherwise = concentrate (matricize ps) sig
-- accumulates arguments of caseMatrix to one pattern
shrinkPat :: CaseMatrix -> As.Term
shrinkPat cmx =
case patBrand cmx of
Appl -> case cons cmx of
Just c -> foldl mkApplT c ((args cmx) ++ (newArgs cmx))
Nothing -> error "HasCASL2IsabelleHOL.shrinkPat"
Tuple -> TupleTerm ((args cmx) ++ (newArgs cmx)) nullRange
QuOp -> head (args cmx)
_ -> head (newArgs cmx)
where mkApplT t1 t2 = ApplTerm t1 t2 nullRange
patIsVar :: ProgEq -> Bool
patIsVar (ProgEq pat _ _) = termIsVar pat
termIsVar :: As.Term -> Bool
termIsVar t = case t of
QualVar _ -> True
TypedTerm tr _ _ _ -> termIsVar tr
TupleTerm ts _ -> and (map termIsVar ts)
_ -> False
patHasNoArg :: ProgEq -> Bool
patHasNoArg (ProgEq pat _ _) = termHasNoArg pat
termHasNoArg :: As.Term -> Bool
termHasNoArg t = case t of
QualOp _ _ _ _ -> True
TypedTerm tr _ _ _ -> termHasNoArg tr
_ -> False
transCaseAlt :: Env -> ProgEq -> (IsaSign.Term, IsaSign.Term)
transCaseAlt sign (ProgEq pat trm _) =
(transPat sign pat, (transTerm sign trm))
transPat :: Env -> As.Term -> IsaSign.Term
transPat _ (QualVar (VarDecl var _ _ _)) =
IsaSign.Free (transVar var)
transPat sign (ApplTerm term1 term2 _) =
termAppl (transPat sign term1) (transPat sign term2)
transPat sign (TypedTerm trm _ _ _) = transPat sign trm
transPat sign (TupleTerm terms@(_ : _) _) =
foldl1 (binConst isaPair) (map (transPat sign) terms)
transPat _ (QualOp _ (InstOpId i _ _) _ _) =
conDouble (showIsaConstT i baseSign)
transPat _ _ = error "HasCASL2IsabelleHOL.transPat"
-- | apply binary operation to arguments
binConst :: String -> IsaSign.Term -> IsaSign.Term -> IsaSign.Term
binConst s = binVNameAppl $ mkVName s
-- | upper case curried pair constructor
isaPair :: String
isaPair = "Pair"