566d6a1a29233cfc27c489b14fd2b3ce6ce3ec9fChristian Maeder{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniCopyright : (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian MaederMaintainer : paolot@informatik.uni-bremen.de
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniStability : provisional
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederPortability : non-portable (depends on programatica using MPTC)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederauxiliary functions for the embedding comorphism from Haskell to Isabelle
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , newConstTab
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , getTermName
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , remove_duplicates
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , getInstClass
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , getInstType
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , repVarClass
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , constrVarClass
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , funFliftbin
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , liftMapByListD
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , nothingFiOut
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , IsaTypeInsts
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , liftMapByList
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , HsInstances
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , extClassInfo
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , extAbbrsInfo
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , getMainInstType
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , checkTyCons
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , getFieldTypes
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini , replaceTyVar
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini , getContinuity
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport qualified Data.Map as Map
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe (fromMaybe)
d4655008a003ed9717ba0bb0d7022e166006fca0Christian Maederimport Common.Utils (number, nubOrd)
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maeder-- Haskell (Programatica)
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maederimport SourceNames
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport TiTypes
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maederimport TiInstanceDB
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport PosName
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport UniqueNames
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport TiPropDecorate
2b827e8e9d6a1196ffaf263dcc991779e5f9c0e9Christian Maederimport PropSyntaxStruct as HsName
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport TiDecorate
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport Isabelle.IsaSign as IsaSign
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport Isabelle.IsaConsts as IsaConsts
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniimport Isabelle.Translate as Translate
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ----------------------------- TYPE synonyms --------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------- Haskell --------------------------------------------- -}
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsInstance = TiInstanceDB.Instance PNT
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsInstances = [TiInstanceDB.Instance PNT]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsPred = TiTypes.Pred PNT
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrinitype HsType = TiTypes.Type PNT -- same as HsPred
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsClass = TiTypes.Type PNT
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsScheme = TiTypes.Scheme PNT
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsId = HsIdentI PNT
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HsTypeInfo = TiTypes.TypeInfo PNT
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype HId i = HsIdentI i
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maedertype VaMap = Map.Map HsId HsScheme
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype TyMap = Map.Map HsId (Kind, HsTypeInfo)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ---------------- Isabelle --------------------------------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype IsaPattern = IsaSign.Term
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinitype IsaTypeInsts = (TName, [(IsaClass, [(IsaType, [IsaClass])])])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------ list functions ------------------------------
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederremoveEL :: [[a]] -> [[a]]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederremoveEL = filter (not . null)
d4655008a003ed9717ba0bb0d7022e166006fca0Christian Maederremove_duplicates :: Ord a => [a] -> [a]
d4655008a003ed9717ba0bb0d7022e166006fca0Christian Maederremove_duplicates = nubOrd
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------- filters -----------------------------------
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedernothingFiOut :: [(a, (Maybe b, c))] -> [(a, (b, c))]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedernothingFiOut ls = [(x, (y, w)) | (x, (Just y, w)) <- ls]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------- lifting function ---------------------------
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederliftMapByList :: (x -> [(a, b)]) -> ([(c, d)] -> y)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder -> (a -> c) -> (b -> d) -> x -> y
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederliftMapByList ma mb h k f = mb [(h a, k b) | (a, b) <- ma f]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederliftMapByListD :: (x -> [a]) -> ([c] -> y) -> (a -> b1)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder -> (a -> b2) -> ([(b1, b2)] -> [c]) -> x -> y
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederliftMapByListD l1 l2 h k g f = l2 $ g [ (h a, k a) | a <- l1 f]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------ generic checking of mutual dependencies ----------
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaedergetDepDoms :: IsaSign.DomainTab -> IsaSign.DomainTab
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetDepDoms = abGetDep deDepOn
d4655008a003ed9717ba0bb0d7022e166006fca0Christian MaederabGetDep :: Ord a => (a -> a -> Bool) -> [[a]] -> [[a]]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederabGetDep f ls = case ls of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder remove_duplicates $
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder removeEL (map remove_duplicates
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (checkDep (liftDep (mutRel f)) xs [x] []))
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrinicheckDep :: ([x] -> [x] -> Bool) -> [[x]] -> [[x]] -> [[x]] -> [[x]]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedercheckDep f ls ms cs = case ls of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder a : as -> case ms of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder if f a b then checkDep f ((a ++ b) : as) bs cs else
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder checkDep f (a : as) bs (b : cs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> checkDep f as (a : cs) []
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder-- mutual dependence
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinimutRel :: (a -> a -> Bool) -> a -> a -> Bool
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinimutRel f x y = f x y && f y x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------ HASKELL representation -------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder--------------------- check functions ----------------------------------- -}
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinicheckTyCons :: HsId -> Bool
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedercheckTyCons d = case d of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder HsCon _ -> True
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- -------------------------- get functions -------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder----------------- getting info from Haskell types ---------------------- -}
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetLitName :: HsType -> PNT
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedergetLitName (Typ t) = case t of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsTyVar x -> x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsTyCon x -> x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ---------------- getting class and type ouf of predicate --------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstType :: HsPred -> HsType
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstType x = case x of (Typ (HsTyApp _ t)) -> t
da955132262baab309a50fdffe228c9efe68251dCui Jian _ -> trace ("\n TYPE: " ++ show x) $
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstClass :: HsPred -> HsType
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstClass x = case x of (Typ (HsTyApp c _)) -> c
da955132262baab309a50fdffe228c9efe68251dCui Jian _ -> trace ("\n CLASS: " ++ show x) $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------- getting class information -----------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniextClassInfo :: HsTypeInfo -> [HsClass]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederextClassInfo p = case p of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini TiTypes.Class a _ _ _ -> map getInstClass a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------------- getting info on type syns -------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniextAbbrsInfo :: HsTypeInfo -> ([PNT], HsType)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederextAbbrsInfo p = case p of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini TiTypes.Synonym ls t -> (ls, t)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------ get arity information from Haskell instances ------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstPrems :: HsInstance -> [HsPred]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetInstPrems (_, IE _ _ ps) = ps
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetMainInstType :: HsInstance -> HsType
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedergetMainInstType (i, _) = getInstType i
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetMainInstClass :: HsInstance -> HsClass
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedergetMainInstClass (i, _) = getInstClass i
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniprepInst :: HsInstance -> (HsClass, [(HsType, [HsClass])])
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniprepInst i = (getMainInstClass i, prepInst1 i)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniprepInst1 :: HsInstance -> [(HsType, [HsClass])]
da955132262baab309a50fdffe228c9efe68251dCui JianprepInst1 i =
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder [(x, [getInstClass y | y <-
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder getInstPrems i, showIsaHsTypeString (getInstType y)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder == showIsaHsTypeString x])
d4655008a003ed9717ba0bb0d7022e166006fca0Christian Maeder | x <- nub $ map getInstType (getInstPrems i)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------- ISABELLE representation ---------------------------
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrinidata ExpRole = FunDef | InstDef -- no PLogic yet
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder deriving (Ord, Eq, Show)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------------- constants ---------------------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinixDummy :: IsaTerm
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederxDummy = conDouble "dummy"
5f47ba5a7151e73f2540d01492b83f7e34605730Christian MaederholEq :: IsaTerm -> IsaTerm -> IsaTerm
bc733f0a76607ee9bba69e5d40784b49c83d7a00Christian MaederholEq t1 t2 = termMAppl NotCont (con eqV) [t1, t2]
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinigetTermName :: Term -> Maybe String
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedergetTermName a = case a of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini Const x _ -> Just $ new x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Free x -> Just $ new x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> Nothing -- "_"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ---------------------- Haskell names --------------------------------
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinienElem :: String -> [String] -> Bool
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederenElem s ls = let
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder ks = map showIsaName ls
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder hs = map (++ "DF") ks
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder js = map (++ "I") hs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in elem s $ ks ++ hs ++ js
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinimthTy :: Continuity -> String -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["==", "/=", "<", "<=", ">", ">="] = aaT c k (boolT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p (["min", "max", "+", "-", "*", "quot", "rem"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ++ ["div", "mod", "\\"]) = aaA c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["succ", "pred", "negate", "abs", "signum", "recip"] = aA c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["enumFromThen", "enumFromTo"] = aaL c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["minBound", "maxBound"] = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["quotRem", "divMod"] = aaP c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["toEnum"] = aT c k (intT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["enumFrom"] = aL c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["enumFromThenTo"] = aaaL c k
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["fromEnum"] = tA c k (intT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["fromInteger"] = tA c k (integerT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["fromFractional"] = tA c k (fracT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["toInteger"] = aT c k (integerT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | enElem p ["compare"] = aaT c k (orderingT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | otherwise = trace (show p) $ error "HsHOLCFaux, mthTy"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaaT :: Continuity -> String -> IsaType -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaaT c k h = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w, w] h
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaaA :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaaA c k = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w, w] w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaL :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaL c k = let w = TFree "a" (IsaClass k : sortT c)
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini in curryFunT c [w] $ listT c w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaaL :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaaL c k = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w, w] $ listT c w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaaaL :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaaaL c k = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w, w, w] $ listT c w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaaP :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaaP c k = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w, w] $ prodT c w w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedertA :: Continuity -> String -> IsaType -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertA c k h = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [h] w
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaT :: Continuity -> String -> IsaType -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaT c k h = let w = TFree "a" (IsaClass k : sortT c)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in curryFunT c [w] h
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederaA :: Continuity -> String -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaA c k = let w = TFree "a" (IsaClass k : sortT c)
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini in curryFunT c [w] w
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini-- method names
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthEq, mthOrd, mthEnum, mthBounded, mthNum, mthIntegral :: [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthMonad, mthFunctor, mthAll, aweLits, mthFractional :: [String]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthEq = ["==", "/="]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthOrd = ["compare", "<", "<=", ">", ">=", "max", "min"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthEnum = ["succ", "pred", "toEnum", "fromEnum", "enumFrom",
da955132262baab309a50fdffe228c9efe68251dCui Jian "enumFromThen", "enumFromTo", "enumFromThenTo"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthBounded = ["minBound", "maxBound"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthNum = ["+", "-", "*", "negate", "abs", "signum", "fromInteger"]
da955132262baab309a50fdffe228c9efe68251dCui JianmthIntegral = ["quot", "rem", "div", "mod", "quotRem", "divMod", "toInteger"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthMonad = ["return", ">>=", ">>", "fail"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthFunctor = ["fmap"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthFractional = ["/", "recip", "fromRational"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermthAll = mthEq ++ mthOrd ++ mthEnum ++ mthNum
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini ++ mthIntegral ++ mthFractional ++ mthBounded
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaweLits = mthMonad ++ mthFunctor ++ mthEq ++ ["+", "-", "*"]
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrininameListA, nameListB, nameListC, nameListD :: [String]
da955132262baab309a50fdffe228c9efe68251dCui JiannameListE, nameListF, nameListH :: [String]
da955132262baab309a50fdffe228c9efe68251dCui Jian-- Special translation - operators
da955132262baab309a50fdffe228c9efe68251dCui JiannameListA = ["&&", "||", "==", "/=", "<", "<=", ">", ">=", "+",
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini "*", "-", "^",
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini "^^", "++", "!!", "/", ".", "$", "$!", ">>=", ">>"]
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini-- dual translation - constructors
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernameListB = ["()", "(,)", "True", "False", ":", "[]", "Just", "Nothing"]
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini-- dual translation operators
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernameListC = ["primError", "return"]
da955132262baab309a50fdffe228c9efe68251dCui Jian-- other constructors
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernameListD = ["ET", "EQ", "GT", "Left", "Right"]
da955132262baab309a50fdffe228c9efe68251dCui Jian-- Prelude functions
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrininameListE = -- map (\x -> x ++ "'")
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ["not", "min", "max", "negate", "abs", "signum",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "fromInteger", "succ", "pred", "fromEnum", "toEnum", "enumFrom",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "enumFromThen", "enumFromTo", "enumFromThenTo",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "minBound", "maxBound", "toRational", "quot", "rem", "div", "mod",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "quotRem", "divMod", "toInteger", "otherwise", "either", "maybe",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "fst", "snd", "id", "curry", "uncurry", "const", "until", "asTypeOf",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "odd", "even", "subtract", "flip", "gcd", "lcm", "seq", "error",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "undefined", "fromRational", "recip", "powAux", "powBux"]
da955132262baab309a50fdffe228c9efe68251dCui Jian-- Prelude list functions
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernameListF = -- map (\x -> x ++ "'")
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ["map", "filter", "concat", "concatMap", "head", "last", "tail",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "init", "null", "length", "foldl", "foldl1", "scanl", "scanl1",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "foldr", "foldr1", "scanr", "scanr1", "iterate", "repeat",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "replicate", "cycle", "take", "drop", "splitAt", "takeWhile",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "dropWhile", "span", "break", "lines", "words", "unlines",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "unwords", "reverse", "and", "or", "any", "all", "elem", "notElem",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "lookup", "sum", "product", "maximum", "minimum", "zip", "zip3",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "zipWith", "zipWith3", "unzip", "unzip3"]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedernameListH = ["flip", "&&", "||", "conj", "disj", "error", "otherwise",
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "comp", "subtract", "map", ".", "not", "break", "fst", "snd"]
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorriniprimedS :: String -> String
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorriniprimedS s = s ++ "'"
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitrOSym :: String -> String
da955132262baab309a50fdffe228c9efe68251dCui JiantrOSym s = case s of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "++" -> "bconcat"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "$!" -> "sapply"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ">>=" -> "mbind"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ">>" -> "mbbind"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> error "Hs2HOLCFaux,trOSym"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaedertransPrelude :: (String -> String) -> String -> String
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinitransPrelude f s = let ns = init s
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder in if elem s (nameListB ++ nameListC ++ nameListD) then s
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else if elem s (nameListE ++ nameListF)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then s ++ (if elem s (mthAll ++ nameListH ++ ["tail", "head"])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then "H" else "U")
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else if elem s (map primedS (nameListE ++ nameListF))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then ns ++ (if elem ns (mthAll ++ nameListH)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then "H" else "U")
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else if elem s nameListA
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder then if elem s aweLits then trOSym s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else trOSym s ++ (if elem s (mthAll ++ nameListH)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then "H" else "U")
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini else if elem ns nameListA && last s == '#'
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder then if elem ns aweLits then trOSym ns
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else trOSym ns ++ (if elem ns (mthAll ++ nameListH)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then "H" else "U")
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini else if take 9 s == "default__"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder then transPrelude f (drop 9 s) ++ "DF"
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else if take 3 s == "$--"
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini then transPrelude f (drop 3 s) ++ "I"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------- Name translation ----------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederTranslating to strings compatible with Isabelle -}
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniclass IsaName a where
14a3cc9512ab27e1f59f01cc23f7d9f97e2e1c4cChristian Maeder showIsaName :: a -> String
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini showIsaString :: a -> String
14a3cc9512ab27e1f59f01cc23f7d9f97e2e1c4cChristian MaedershowIsaS :: String -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedershowIsaS = transPrelude (transConstStringT HOLCF_thy)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName String where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showIsaName = showIsaS
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showIsaString = id
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinishowIsaHsN :: Show a => (String -> a) -> HsName.HsName -> a
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedershowIsaHsN f t = case t of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini Qual _ y -> f y
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini UnQual w -> f w
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torriniinstance IsaName PNT.PId where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaName (PN x _) = showIsaS x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaString (PN x _) = x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName HsName.HsName where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaName = showIsaHsN showIsaS
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaString = showIsaHsN id
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName PosName.HsName where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaName (SN x _) = showIsaName x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaString (SN x _) = showIsaString x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName PNT.PName where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaName (PN x _) = showIsaName x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaString (PN x _) = showIsaString x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName PNT where
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaName (PNT x _ _) = showIsaName x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder showIsaString (PNT x _ _) = showIsaString x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torriniinstance IsaName a => IsaName (HId a) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showIsaName t = case t of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsVar x -> showIsaName x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsCon x -> showIsaName x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder showIsaString t = case t of
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsVar x -> showIsaString x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini HsCon x -> showIsaString x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedershowIsaHsTypeString :: HsType -> String
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedershowIsaHsTypeString (Typ t) = case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder HsTyFun _ _ -> "Fun"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder HsTyApp _ _ -> "App"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder HsTyVar x -> showIsaString x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder HsTyCon x -> showIsaString x
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder HsTyForall _ _ x -> showIsaHsTypeString x
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------ auxiliary name functions depending on IsaSign -----------------
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederjoinNames :: [String] -> String
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederjoinNames = concatMap (++ "_X")
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaederisCont :: Continuity -> Bool
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorriniisCont x = x == IsCont True || x == IsCont False
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinigetContinuity :: Continuity -> IsaTerm -> Continuity
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinigetContinuity c t = case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Const _ w -> case (kon w, c) of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (_, NotCont) -> c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (TCon, IsCont _) -> IsCont False -- unlifted for constructors
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (_, IsCont _) -> IsCont True -- lifted for the rest
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.App {} -> continuity t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Abs {} -> continuity t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.If {} -> continuity t
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini IsaSign.Tuplex _ _ -> continuity t
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaedertransTN :: Continuity -> String -> String -> String
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedertransTN c s1 s2 = let d = transPath s1 s2
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder ic = isCont c
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder in if s1 == "Prelude" then case s2 of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "()" -> if ic then "unitT"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Int" -> if ic then "intT"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Integer" -> if ic then "integerT"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Char" -> if ic then "charT"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Bool" -> if ic then "lBool"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "[]" -> if ic then "llist"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Either" -> if ic then "lEither"
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini else "either"
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini "Ordering" -> if ic then "lOrdering"
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini else "sOrdering"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "String" -> if ic then "lString"
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini else "string"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "Maybe" -> if ic then "lMaybe"
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini else "option"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder "(,)" -> if ic then "lprod" else "*"
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini "Rational" -> if ic then "ratT" else "rat"
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitransPath :: String -> String -> String
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedertransPath s1 s2 = showIsaName s1 ++ "_" ++ showIsaName s2
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------- getting info about domaintab -------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedertype AConstTab = Map.Map VName (Typ, IsaVT)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrinidata IsaVT = IsaConst | IsaVal deriving (Eq, Show)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetDomType :: AConstTab -> VName -> IsaType
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedergetDomType ctab c = maybe (error "Hs2HOLCFaux.getDomType")
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder (getHeadType . fst) $ Map.lookup c ctab
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederisFunArrow :: String -> Bool
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorriniisFunArrow name = elem name [funS, cFunS, lFunS]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetHeadType :: IsaType -> IsaType
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedergetHeadType t = case t of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.Type name _ [_, t2] | isFunArrow name -> getHeadType t2
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetFieldTypes :: AConstTab -> VName -> [IsaType]
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedergetFieldTypes ctab c = maybe [] (argTypes . fst) $ Map.lookup c ctab
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniargTypes :: IsaType -> [IsaType]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniargTypes a = case a of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.Type name _ [b, c] | isFunArrow name -> b : argTypes c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ----------------------- Instances ------------------------------------
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinigroupInst :: [IsaTypeInsts] -> [IsaTypeInsts]
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinigroupInst db =
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini remove_duplicates [(y,
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini remove_duplicates $ concat
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini [b | (a, b) <- db, a == y]) | (y, _) <- db]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- --------------------- TERMS ------------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederlifting, tuples, multiple abstractions and applications, fixpoints -- -}
877dc5b504cce93444f1a85120279f4938e8c5f6Paolo TorrinifunFliftbin :: Term -> Term
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinifunFliftbin f = termMAppl NotCont (conDouble lliftbinS) [f]
5fd8f2cd4cad1d0f623a50c7f01bda4335f4935bPaolo TorrinifunFlift2 :: Term -> Term
5fd8f2cd4cad1d0f623a50c7f01bda4335f4935bPaolo TorrinifunFlift2 f = termMAppl NotCont (conDouble flift2S) [f]
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinivarDouble :: String -> Term
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinivarDouble = Free . mkVName
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitermMAbs :: Continuity -> [Term] -> Term -> Term
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedertermMAbs c ts t =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder v : vs -> if isDicConst v then termMAbs c vs t else
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Abs v (termMAbs c vs t) c
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitermMAppl :: Continuity -> Term -> [Term] -> Term
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaedertermMAppl c t ts =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let prelTest vn = any (\ x -> isPrefixOf x $ IsaSign.orig vn)
ce40e0e7e4e620ae338d9cb1498d9289a17e7132Paolo Torrini [ "inst__Prelude_"
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder , "derived__Prelude_"]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder in case (t, ts) of
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder (Const vn _, [a]) | isDicConst t || prelTest vn -> a
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (_, v : vs) -> case v of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini Const vn _ | isDicConst v || prelTest vn -> termMAppl c t vs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> termMAppl c (App t v $ getContinuity c t) vs
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitermBAppl :: Continuity -> Term -> Term -> Term -> Term
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertermBAppl c t1 t2 t3 = termMAppl c t1 [t2, t3]
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinitermSAppl :: Continuity -> Term -> Term -> Term
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo TorrinitermSAppl c t1 t2 = termMAppl c t1 [t2]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------- connectives ------------------------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitupleSelector :: Int -> Int -> Term -> Continuity -> Term
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitupleSelector mx n t c
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder | mx < 2 = error "Hs2HOLCFaux.tupleSelector1"
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder | n == 0 = error "Hs2HOLCFaux.tupleSelector2"
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder | mx < n = error "Hs2HOLCFaux.tupleSelector3"
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini | n == mx = tupleSelect (n - 1) t c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | otherwise = termMAppl c (fstPT c) [tupleSelect (n - 1) t c]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitupleSelect :: Int -> Term -> Continuity -> Term
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinitupleSelect n t c = case n of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder _ -> tupleSelect (n - 1)
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (termMAppl c (sndPT c) [t]) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ---------------------------- term filters ----------------------------
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorriniisDicConst :: Term -> Bool
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederisDicConst t = case t of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Const vn _ | IsaSign.orig vn == "DIC" -> True
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Free vn | IsaSign.orig vn == "DIC" -> True
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniconstFilter :: Term -> [Term]
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniconstFilter t = case t of
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Abs _ x _ -> constFilter x
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder IsaSign.App x y _ -> concatMap constFilter [x, y]
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder IsaSign.If x y z _ -> concatMap constFilter [x, y, z]
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder IsaSign.Case x ys -> concatMap constFilter $ x : map snd ys
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Let xs y -> concatMap constFilter $ y : map snd xs
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder IsaSign.IsaEq x y -> concatMap constFilter [x, y]
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder IsaSign.Tuplex xs _ -> concatMap constFilter xs
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaederelPos :: [Term] -> Term -> Maybe Int
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaederelPos ls x = fmap (+ 1) $ findIndex (constEq x) ls
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ---------------- subterm extraction ----------------------------------
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederextFBody :: Term -> (Term, [Term])
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaederextFBody t' = extFB t' []
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini extFB t as = case t of
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Abs x b _ -> extFB b (x : as)
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder _ -> (t, reverse as)
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorriniextTBody :: Term -> (Term, [Term])
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaederextTBody t' = extTB t' []
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini extTB t as = case t of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.App a x _ -> extTB a (x : as)
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder _ -> (t, reverse as)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------- eliminating case expressions ---------------------------
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian MaederdestCaseS :: Continuity -> IsaTerm -> IsaTerm -> [IsaTerm]
da955132262baab309a50fdffe228c9efe68251dCui JiandestCaseS c d t =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [holEq (termMAppl c d xs) y | (xs, y) <- destCaseU (extFBody t, [])]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdestCaseU :: ((IsaTerm, [IsaPattern]), [IsaPattern]) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [([IsaPattern], IsaTerm)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdestCaseU ((t, rs), ks) = case (t, rs) of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder (Case v ls, vv : vs) -> if v == vv
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then [(ks ++ [l], termMAbs NotCont vs m) | (l, m) <- ls]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else destCaseU ((t, vs), ks ++ [vv])
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederdestCase :: IsaTerm -> (VName -> VName) -> [(IsaPattern, IsaTerm)]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian MaederdestCase t f = let w = extFBody t in case w of
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder (Case v ls, _ : vs) -> case v of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini [(renVars (Free (f n)) [l] l, -- repl. l if l is a var.
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder renVars (Free (f n))
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder [l] (termMAbs NotCont vs m)) | (l, m) <- ls]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> [(l, termMAbs NotCont vs m) | (l, m) <- ls]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------- equivalence on terms ---------------------------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniconstEq :: Term -> Term -> Bool
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederconstEq t1 t2 = case (t1, t2) of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (Const m x, Const n y) -> n == m && typEq (typ x) (typ y)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinisimTerms :: Term -> Term -> Bool
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinisimTerms t1 t2 = case (t1, t2) of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (IsaSign.Const x w, IsaSign.Const y z) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder x == y && (if take 6 (new x) == "mbind_" ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder take 7 (new x) == "return_"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder then typ w == noTypeT || typ z == noTypeT ||
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder typSim (typ w) (typ z)
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder else typSim (typ w) (typ z))
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder (IsaSign.Abs _ _ c, IsaSign.Abs _ _ d) -> c == d
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder (If _ _ _ c, If _ _ _ d) -> c == d
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini (Case _ _, Case _ _) -> True
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini (Let _ _, Let _ _) -> True
8068f3f49b39b3df074d92823c84be73b125c50aPaolo Torrini (IsaEq _ _, IsaEq _ _) -> True
877dc5b504cce93444f1a85120279f4938e8c5f6Paolo Torrini (Tuplex _ _, Tuplex _ _) -> True
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------ replacement functions ----------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- in term t, replaces variable f for variables in ls
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrenVars :: Term -> [Term] -> Term -> Term
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrinirenVars f ls t = case t of
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Free _ -> if elem t ls then f else t
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Abs v x c -> IsaSign.Abs v (renVars f ls x) c
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini IsaSign.App x y c -> termSAppl c (renVars f ls x) (renVars f ls y)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.If (renVars f ls x) (renVars f ls y) (renVars f ls z) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Case (renVars f ls x) [(a, renVars f ls b) | (a, b) <- ys]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Let [(a, renVars f ls b) | (a, b) <- xs] (renVars f ls y)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.IsaEq x y -> IsaSign.IsaEq (renVars f ls x) (renVars f ls y)
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini IsaSign.Tuplex xs c -> IsaSign.Tuplex (map (renVars f ls) xs) c
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrinirenFuns :: (Term -> Maybe Term) -> Term -> Term
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrinirenFuns f t = case t of
29379037d0a2fc17c96c49bd343a3f276a5b34a6Christian Maeder IsaSign.Abs v x c -> IsaSign.Abs v (renFuns f x) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.App x y c -> fromMaybe (termSAppl c (renFuns f x) (renFuns f y)) $ f t
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.If (renFuns f x) (renFuns f y) (renFuns f z) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Case (renFuns f x) [(a, renFuns f b) | (a, b) <- ys]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Let [(a, renFuns f b) | (a, b) <- xs] (renFuns f y)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder IsaSign.IsaEq x y -> IsaSign.IsaEq (renFuns f x) (renFuns f y)
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini IsaSign.Tuplex xs c -> IsaSign.Tuplex (map (renFuns f) xs) c
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- -------------------- SENTENCES ----------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------- getting info from sentences ----------------------- -}
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaedernewConstTab :: Continuity -> [Named IsaSign.Sentence] -> ConstTab
5109958689fd75b0a42c81e615ee7b270d07bf00Christian MaedernewConstTab c ls = if isCont c then Map.empty else
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder Map.fromList [(mkVName $ extAxName x, extAxType x) | x <- ls]
13ed13e06a5dd4aad12044ed7e7503cbe7f62990Christian MaederextAxName :: Named Sentence -> String
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederextAxName = senAttr
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo TorriniextAxType :: Named Sentence -> Typ
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederextAxType s = case extFunTerm s of
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini Const _ t | isAxiom s -> typ t
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniextAxType :: Named Sentence -> Typ
f358d354ac654d5682743dde5285a4b57af8aa16Christian MaederextAxType s = case sentence s of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini ConstDef (IsaEq (Const _ t) _) | isAxiom s -> (typ t)
da955132262baab309a50fdffe228c9efe68251dCui Jian RecDef _ ((App (App _ (App (Const _ t) _ _) _) _ _ : _) : _)
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini | isAxiom s -> (typ t)
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaederextFunTerm :: Named Sentence -> Term
f358d354ac654d5682743dde5285a4b57af8aa16Christian MaederextFunTerm s = case sentence s of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq t _) -> fst $ extTBody t
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder RecDef _ _ _ (App (App _ x _) _ _ : _) -> fst $ extTBody x
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniextLeftH :: Named Sentence -> Term
f358d354ac654d5682743dde5285a4b57af8aa16Christian MaederextLeftH s = case sentence s of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq t _) -> t
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorriniextRightH :: Named Sentence -> Term
f358d354ac654d5682743dde5285a4b57af8aa16Christian MaederextRightH s = case sentence s of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq _ t) -> t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- left comp is def name, right comp are constants in the def
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinisentAna :: Named Sentence -> (Term, [Term])
f358d354ac654d5682743dde5285a4b57af8aa16Christian MaedersentAna s = case sentence s of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq l r) | isAxiom s -> (l, constFilter r)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------ checking for mutually recursive function defs ----------
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinigetDepSent :: [[Named Sentence]] -> [[Named Sentence]]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetDepSent = abGetDep sentDepOn
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinigetExpRole :: Named Sentence -> ExpRole
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedergetExpRole n = case extFunTerm n of
da955132262baab309a50fdffe228c9efe68251dCui Jian Const _ x -> case kon x of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini TMet -> InstDef
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> error "Hs2HOLCFaux, getExpRole"
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederdepOn :: (a -> b -> Bool) -> (c -> a) -> (c -> [b]) -> c -> c -> Bool
3e603e36c535a7f0c7a6fe1c3f3b5768ab50853bChristian MaederdepOn f g h x y = any (f (g x)) (h y)
8068f3f49b39b3df074d92823c84be73b125c50aPaolo TorrinisentDepOn :: Named Sentence -> Named Sentence -> Bool
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinisentDepOn x y = case getExpRole x of
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder depOn (\ u v -> simTerms u v
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini && typEq (typ $ termType u) (typ $ termType v))
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (fst . sentAna) (snd . sentAna) x y
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder FunDef -> depOn simTerms (fst . sentAna) (snd . sentAna) x y
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ----------------- adding fixpoints ------------------------------------
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaederfixMRec :: Continuity -> [[Named Sentence]] -> [Named Sentence]
da955132262baab309a50fdffe228c9efe68251dCui JianfixMRec c ls = let xs = getDepSent ls
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini in addFixPoints c xs
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaederaddFixPoints :: Continuity -> [[Named Sentence]] -> [Named Sentence]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddFixPoints c = concatMap (fixPoint c)
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaederfixPoint :: Continuity -> [Named Sentence] -> [Named Sentence]
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian MaederfixPoint c xs = case xs of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini [a] -> if sentDepOn a a then [mapNamed ( \ s -> case s of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq lh rh) -> case c of
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder IsCont _ -> RecDef (Just fixrecS) (mkVName . senAttr $ a)
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder Nothing [holEq lh rh]
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder NotCont -> RecDef Nothing (mkVName . senAttr $ a)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing (destCaseS c lh rh)
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder _ : _ -> case c of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini IsCont _ -> let
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder jn = joinNames (map extAxName xs) -- name is ininfluential here
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder ys = map (\ x -> [holEq (extLeftH x) $ extRightH x]) xs
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder ps = [makeNamed jn $ RecDef (Just fixrecS) (mkVName jn)
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder Nothing (concat ys)]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder NotCont -> let
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder jj = joinNames (map extAxName xs)
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder jn = mkVName jj
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini jt1 = headTailsType (map extAxType xs)
d7932c7a4f283f6c339ee4e2cec97840ad6b6735Paolo Torrini (jta, jts) = headTailsMT jt1
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini jt = mkFunType jta (typTuple NotCont jts)
16557bec6cec1ee2c3c4da15a4e8fdadf0b7e7f0Jonathan von Schroeder jl = Const jn $ hideNN jt
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder n = length xs
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder rs = map extRightH xs
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder ls = map extFunTerm xs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder yys = map (\ x -> destCase x (const jn)) rs
8aa7394a1d48cd7c0398ed3b734d148f6f2ea7fcChristian Maeder yyys = reassemble yys
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder zs = map (\ (p, ts) -> (p, Tuplex
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini (map (renFuns (newFCons (Const jn noType) ls)) ts)
8b66de47c89e252c907c8ed3a5ccd16dbccbfb3eChristian Maeder NotCont)) $ Map.toList yyys
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder os = map (\ (x, m) -> mkNewDef x jj n m jt1) $ number xs
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder ps = makeNamed jj (makeRecDef jj jl zs) : os
da955132262baab309a50fdffe228c9efe68251dCui JianmkNewDef :: Named Sentence -> String ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Int -> Int -> [(Typ, Typ)] -> Named Sentence
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinimkNewDef s z x y t = let -- x is the max
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder zy = uncurry mkFunType (t !! (y - 1))
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder in mapNamed ( \ sen -> case sen of
f358d354ac654d5682743dde5285a4b57af8aa16Christian Maeder ConstDef (IsaEq lh rh) -> case (lh, extFBody rh) of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini (Const nam _, (_, w : ws)) ->
16557bec6cec1ee2c3c4da15a4e8fdadf0b7e7f0Jonathan von Schroeder ConstDef $ IsaEq (Const nam $ hideNN zy) $
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder termMAbs a (w : ws) $ termMAppl a (tupleSelector x y
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder (termSAppl a (Const (mkVName z) noType) w) a) ws
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedermakeRecDef :: String -> Term -> [(Term, Term)] -> Sentence
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von SchroedermakeRecDef n t ls =
50ec2512ec38a3a0c793c65583e60ef12beaae33Jonathan von Schroeder RecDef Nothing (mkVName n)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing (map (\ (a, b) -> holEq (App t a NotCont) b) ls)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederreassemble :: [[(Term, Term)]] -> Map.Map Term [Term]
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maederreassemble ls = foldr
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder (\ (ft, sd) ms ->
a5c2cf554caecbeefd0219a8a085329f8fbde094Christian Maeder Map.insert ft (sd : Map.findWithDefault [] ft ms) ms)
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrininewFCons :: Term -> [Term] -> Term -> Maybe Term
ce2b32870d20c444248935aa1ac5317faec2a654Paolo TorrininewFCons t ls k = case k of
5109958689fd75b0a42c81e615ee7b270d07bf00Christian Maeder App n w NotCont -> case elPos ls n of
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini Nothing -> Nothing
ce2b32870d20c444248935aa1ac5317faec2a654Paolo Torrini Just $ tupleSelector (length ls) i (IsaSign.App t w NotCont) NotCont
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------ TYPES -----------------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder---------------------- tuples, lifting --------------------------------- -}
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinitypTuple :: Continuity -> [Typ] -> Typ
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinitypTuple c ts = case ts of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini [] -> noTypeT
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini (if isCont c then mkContProduct else prodType) a (typTuple c as)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ------------------ function types -----------------------------------
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorriniheadTailsType :: [Typ] -> [(Typ, Typ)]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederheadTailsType ls = if chkTHead ls then map splitFunT ls
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder else error "Hs2HOLCFaux.headTailsType"
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinisplitFunT :: Typ -> (Typ, Typ)
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinisplitFunT x = case x of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Type "=>" _ [i, b] -> (i, b)
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini _ -> error "Hs2HOLCF, headTail"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- checks that all types in the list are equivalent in the first argument
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederand that all variables occur in that argument -}
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinichkTHead :: [IsaType] -> Bool
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinichkTHead ls = case ls of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.Type "=>" _ [x, n] : IsaSign.Type "=>" s [y, m] : ns ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (typEq x y && mkTVarMap id x == mkTVarMap id n) &&
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder chkTHead (IsaSign.Type "=>" s [y, m] : ns)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [IsaSign.Type "=>" _ [x, n]] -> mkTVarMap id x == mkTVarMap id n
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- -------------------- equivalence of types modulo variables name ------
da955132262baab309a50fdffe228c9efe68251dCui JiantypSim :: Typ -> Typ -> Bool
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitypSim t1 t2 = case (t1, t2) of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (IsaSign.Type _ _ ls1, IsaSign.Type _ _ ls2) ->
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini typeId t1 == typeId t2 && typLSim ls1 ls2
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (TFree _ _, TFree _ _) -> True
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitypLSim :: [Typ] -> [Typ] -> Bool
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitypLSim ls1 ls2 = case (ls1, ls2) of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini ([], []) -> True
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini (a : as, b : bs) -> typSim a b && typLSim as bs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroedertypEq :: Typ -> Typ -> Bool -- make some distinction for case noType?
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinitypEq t1 t2 = t1 == noTypeT || t2 == noTypeT || case (t1, t2) of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini (IsaSign.Type _ _ ls1, IsaSign.Type _ _ ls2) ->
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder typeId t1 == typeId t2
a1d60ea30abf7e3f514e748a07203d9f336391eaPaolo Torrini && typeSort t1 == typeSort t2 && typLEq ls1 ls2
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini (TFree _ _, TFree _ _) -> typeSort t1 == typeSort t2
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinitypLEq :: [Typ] -> [Typ] -> Bool
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinitypLEq ls1 ls2 = case (ls1, ls2) of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini ([], []) -> True
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini (a : as, b : bs) -> typEq a b && typLEq as bs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- --------------------- type renaming -----------------------------------
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorriniapplyTyRen :: Int -> Typ -> Typ
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorriniapplyTyRen n t = case t of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini TFree x s -> TFree (x ++ "XX" ++ show n) s
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini IsaSign.Type a b cs -> IsaSign.Type a b $ map (applyTyRen n) cs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder-- ----------------------- type var maps ---------------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederheadTailsMT :: [(Typ, Typ)] -> (Typ, [Typ])
da955132262baab309a50fdffe228c9efe68251dCui JianheadTailsMT ls = let
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini ks = [(mkTVarMap (applyTyRen 0) i, (i, b)) | (i, b) <- ls]
da955132262baab309a50fdffe228c9efe68251dCui Jian in case ks of
da955132262baab309a50fdffe228c9efe68251dCui Jian [] -> error "Hs2HOLCFaux, headTailsType"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (f, (x, _)) : _ -> let
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder zs = [(renMap f g, y) | (g, (_, y)) <- ks]
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini zz = [applyTVM h y | (h, y) <- zs]
d7932c7a4f283f6c339ee4e2cec97840ad6b6735Paolo Torrini w = applyTyRen 0 x
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini-- !!!!!!!!!!!!
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinirenMap :: Map.Map Typ Typ -> Map.Map Typ Typ -> Map.Map Typ Typ
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini Map.fromList [(fst $ Map.elemAt n g, snd $ Map.elemAt n f)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder | n <- [0 .. (Map.size f - 1)]]
da955132262baab309a50fdffe228c9efe68251dCui Jian else error "HsHOLCFaux, renMap"
1c0f4f958da0fe26f006c2b867a528aa03e5ae6bPaolo Torrini-- !!!!!!!!!!!!
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinimkTVarMap :: (Typ -> Typ) -> Typ -> Map.Map Typ Typ
da955132262baab309a50fdffe228c9efe68251dCui JianmkTVarMap f t = case t of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini Type _ _ xs -> Map.unions [mkTVarMap f y | y <- xs]
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorriniapplyTVM :: Map.Map Typ Typ -> Typ -> Typ
da955132262baab309a50fdffe228c9efe68251dCui JianapplyTVM f t = case t of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini IsaSign.Type n s vs -> IsaSign.Type n s (map (applyTVM f) vs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> fromMaybe t $ Map.lookup t f
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ---------------------- replacement functions -------------------------
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederconstrains variables in t with sort constraints in cs -}
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederconstrVarClass :: IsaType -> [(IsaType, Sort)] -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederconstrVarClass t cs = typeVarsRep addSort [(typeId x, y) | (x, y) <- cs] t
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederaddSort :: [(TName, Sort)] -> TName -> Sort -> Maybe Typ
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorriniaddSort cs n s = do
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini return $ TFree n $ remove_duplicates $ s ++ as
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini-- replaces in t variables of class c with nt
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinirepVarClass :: IsaType -> IsaClass -> IsaType -> IsaType
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrepVarClass t c nt = typeVarsRep repVC (c, nt) t
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinirepVC :: (IsaClass, IsaType) -> TName -> IsaSort -> Maybe IsaType
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinirepVC (c, t) _ s = if elem c s then return t else Nothing
da955132262baab309a50fdffe228c9efe68251dCui JiantypeVarsRep :: (a -> TName -> Sort -> Maybe IsaType) -> a ->
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini IsaType -> IsaType
1c0d563264ca2179de75ad9556414ce62f42759aPaolo TorrinitypeVarsRep f ls t = case t of
1c0d563264ca2179de75ad9556414ce62f42759aPaolo Torrini IsaSign.Type n s vs -> IsaSign.Type n s (map (typeVarsRep f ls) vs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder IsaSign.TFree n s -> fromMaybe t $ f ls n s
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- replace type var in t with type x; used in instantiation; assumed
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederthat t has just one variable -}
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinireplaceTyVar :: IsaType -> IsaType -> IsaType
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo TorrinireplaceTyVar x t = if x == noTypeT then t else case t of
49c972a61797bb7e9aeeaa6a7ca393b074c3b5f0Paolo Torrini IsaSign.Type n s vs -> IsaSign.Type n s (map (replaceTyVar x) vs)