-- Haskell (Programatica)
import TiInstanceDB -- as TiInst
import PropSyntaxStruct as HsName
------------------------------- TYPE synonyms ---------------------------------
------------------ Haskell ----------------------------------------------------
type TyMap =
Map.Map HsId (Kind, HsTypeInfo)
------------------ Isabelle ---------------------------------------------------
type IsaTypeInsts = (TName, [(IsaClass, [(IsaType, [IsaClass])])])
----------------------------- list functions ----------------------------------
removeEL :: [[a]] -> [[a]]
removeEL = filter (not . null)
remove_duplicates :: Eq a => [a] -> [a]
remove_duplicates = nub . reverse
listEnum :: [a] -> [(a, Int)]
---------------------------------- filters -----------------------------------
nothingFiOut :: [(a, (Maybe b, c))] -> [(a, (b, c))]
nothingFiOut ls = [(x, (y, w)) | (x, (Just y, w)) <- ls]
--------------------------------- lifting function ---------------------------
liftMapByList :: (x -> [(a, b)]) -> ([(c, d)] -> y)
-> (a -> c) -> (b -> d) -> x -> y
liftMapByList ma mb h k f = mb [(h a, k b) | (a, b) <- ma f]
liftMapByListD :: (x -> [a]) -> ([c] -> y) -> (a -> b1)
-> (a -> b2) -> ([(b1, b2)] -> [c]) -> x -> y
liftMapByListD l1 l2 h k g f = l2 $ g [ (h a, k a) | a <- l1 f]
--------------------------- generic checking of mutual dependencies ----------
abGetDep :: Eq a => (a -> a -> Bool) -> [[a]] -> [[a]]
abGetDep f ls = case ls of
removeEL (map remove_duplicates (checkDep (abCheckDep (mutRel f))
{- called to check whether, given two lists of elements, one depends
abCheckDep :: (a -> a -> Bool) -> [a] -> [a] -> Bool
abCheckDep f as bs = any (\x -> any (f x) bs) as
checkDep :: ([x] -> [x] -> Bool) -> [[x]] -> [[x]] -> [[x]] -> [[x]]
checkDep f ls ms cs = case ls of
if (f a b) then checkDep f ((a ++ b):as) bs cs else
checkDep f (a:as) bs (b:cs)
[] -> checkDep f as (a:cs) []
mutRel :: (a -> a -> Bool) -> a -> a -> Bool
mutRel f x y = f x y && f y x
depOn :: (a -> b -> Bool) -> (c -> a) -> (c -> [b]) -> c -> c -> Bool
depOn f g h x y = any (f (g x)) (h y)
------------------------ HASKELL representation -------------------------------
--------------------------- check functions -----------------------------------
checkTyCons :: HsId -> Bool
checkTyCons d = case d of
------------------------------ get functions -------------------------------
------------------------ getting info from Haskell types ----------------------
getLitName :: HsType -> PNT
getLitName (Typ t) = case t of
------------------------ getting class and type ouf of predicate --------------
getInstType :: HsPred -> HsType
getInstType x = case x of (Typ (HsTyApp _ t)) -> t
getInstClass :: HsPred -> HsType
getInstClass x = case x of (Typ (HsTyApp c _)) -> c
---------------------------- getting class information -----------------------
extClassInfo :: HsTypeInfo -> [HsClass]
extClassInfo p = case p of
--------------------------- getting info on type syns ------------------------
extAbbrsInfo :: HsTypeInfo -> ([PNT], HsType)
extAbbrsInfo p = case p of
----------- getting arity information from Haskell instances -----------------
getInstPrems :: HsInstance -> [HsPred]
getInstPrems (_, IE _ _ ps) = ps
getMainInstType :: HsInstance -> HsType
getMainInstType (i, _) = getInstType i
getMainInstClass :: HsInstance -> HsClass
getMainInstClass (i, _) = getInstClass i
prepInst :: HsInstance -> (HsClass, [(HsType, [HsClass])])
prepInst i = (getMainInstClass i, prepInst1 i)
prepInst1 :: HsInstance -> [(HsType, [HsClass])]
[(x, [getInstClass y | y <-
getInstPrems i, showIsaHsTypeString (getInstType y)
== showIsaHsTypeString x])
| x <- remove_duplicates $ map getInstType (getInstPrems i)]
-------------------------- ISABELLE representation ---------------------------
-------------------------------- constants -----------------------------------
xDummy = conDouble "dummy"
holEq :: IsaTerm -> IsaTerm -> IsaTerm
holEq t1 t2 = termMAppl NotCont (con eqV) [t1, t2]
getTermName :: Term -> String
getTermName a = case a of
-------------------------------- Name translation ----------------------------
-- Translating to strings compatible with Isabelle
showIsaName :: a -> String
showIsaString :: a -> String
showIsaS :: String -> String
showIsaS = transConstStringT HOLCF_thy
instance IsaName String where
showIsaName x = showIsaS x
showIsaHsN f t = case t of
showIsaName (PN x _) = showIsaS x
showIsaString (PN x _) = x
showIsaName = showIsaHsN showIsaS
showIsaString = showIsaHsN id
showIsaName (SN x _) = showIsaName x
showIsaString (SN x _) = showIsaString x
showIsaName (PN x _) = showIsaName x
showIsaString (PN x _) = showIsaString x
instance IsaName PNT where
showIsaName (PNT x _ _) = showIsaName x
showIsaString (PNT x _ _) = showIsaString x
instance IsaName a => IsaName (HId a) where
showIsaName t = case t of
showIsaString t = case t of
HsVar x -> showIsaString x
HsCon x -> showIsaString x
showIsaHsTypeString :: HsType -> String
showIsaHsTypeString (Typ t) = case t of
HsTyVar x -> showIsaString x
HsTyCon x -> showIsaString x
HsTyForall _ _ x -> showIsaHsTypeString x
----------- auxiliary name functions (inessentially) depending on IsaSign ----
joinNames :: [String] -> String
joinNames = concatMap (++ "_X")
isCont :: Continuity -> Bool
transTN :: Continuity -> String -> String -> String
transTN c s1 s2 = let d = transPath s1 s2
in if s1 == "Prelude" then case s2 of
"Bool" -> if ic then "tr" else "bool"
"Int" -> if ic then "dInt" else "int"
"Integer" -> if ic then "dInt" else "int"
"Rational" -> if ic then "dRat" else "Rat"
"[]" -> if ic then "llist" else "list"
transPath :: String -> String -> String
transPath s1 s2 = showIsaName s1 ++ "_" ++ showIsaName s2
-------------------------- TYPES ----------------------------------------------
------------------------ tuples, lifting --------------------------------------
typTuple :: Continuity -> [Typ] -> Typ
typTuple c ts = case ts of
a : as -> (if isCont c then mkContProduct else prodType) a (typTuple c as)
----------------------------- equivalence of types modulo variables name ------
typEq :: Typ -> Typ -> Bool --make some distinction for case noType??
typEq t1 t2 = t1 == noType || t2 == noType || case (t1, t2) of
typeId t1 == typeId t2 && typeSort t1 == typeSort t2 && typLEq ls1 ls2
(TFree _ _, TFree _ _) -> typeSort t1 == typeSort t2
(TVar _ _, TVar _ _) -> typeSort t1 == typeSort t2
typLEq :: [Typ] -> [Typ] -> Bool
typLEq ls1 ls2 = case (ls1, ls2) of
(a : as, b : bs) -> typEq a b && typLEq as bs
------------------------------- replacement functions -------------------------
-- constrains variables in t with sort constraints in cs
constrVarClass :: IsaType -> [(IsaType,Sort)] -> IsaType
constrVarClass t cs = typeVarsRep addSort [(typeId x,y) | (x,y) <- cs] t
addSort :: [(TName,Sort)] -> TName -> Sort -> Maybe Typ
return $ TFree n $ remove_duplicates $ s ++ as
-- replaces in t varibles of class c with nt
repVarClass :: IsaType -> IsaClass -> IsaType -> IsaType
repVarClass t c nt = typeVarsRep repVC (c,nt) t
repVC :: (IsaClass, IsaType) -> TName -> IsaSort -> Maybe IsaType
repVC (c, t) _ s = if elem c s then return t else Nothing
typeVarsRep :: (a -> TName -> Sort -> Maybe IsaType) -> a -> IsaType -> IsaType
typeVarsRep f ls t = case t of
------------------ more extraction and replacement functions ------------------
unifyTVars :: [IsaType] -> (IsaType,[IsaType])
unifyTVars ls = case chkTHead ls of
chkTHead :: [IsaType] -> Bool
renTVars :: [Typ] -> [Typ]
renTVars ls = [renTVar b a | (a, b) <- listEnum ls]
TFree x s -> if take 2 x == "vX" then t else
TFree (x ++ "XX" ++ show n) s
---------------------------- Instances ----------------------------------------
groupInst :: [IsaTypeInsts] -> [IsaTypeInsts]
remove_duplicates $ concat
[b | (a, b) <- db, a == y]) | (y, _) <- db]
------------------------- DATATYPES -------------------------------------------
----------------------- getting mutually recursive domains in Isabelle --------
getDepDoms ls = ordDoms $ abGetDep deDepOn ls
ordDoms ls = quickSort (orLLift deDepOn) ls
quickSort :: (a -> a-> Bool) -> [a] -> [a]
quickSort f ls = case ls of
([ b | b <- bs, g c b == True],[ b | b <- bs, g c b == False])
orLLift :: (a -> a -> Bool) -> [a] -> [a] -> Bool
orLLift f as bs = case as of
x:xs -> if genOr (f x) bs == True then True
genOr :: (a -> Bool) -> [a] -> Bool
x:xs -> if (f x) then True
deDepOn :: DomainEntry -> DomainEntry -> Bool
deDepOn x y = depOn subTypForm fst (concatMap snd . snd) x y
subTypForm :: Typ -> Typ -> Bool
subTypForm t1 t2 = case t2 of
else any (subTypForm t1) cs
------------------------ getting info about domaintab -------------------------
type AConstTab =
Map.Map VName (Typ,IsaVT)
data IsaVT = IsaConst | IsaVal deriving (Eq, Show)
getDomType :: AConstTab -> VName -> IsaType
isFunArrow :: String -> Bool
isFunArrow name = elem name [funS, cFunS]
getHeadType :: IsaType -> IsaType
getHeadType t = case t of
IsaSign.Type name _ [_, t2] | isFunArrow name -> getHeadType t2
getFieldTypes :: AConstTab -> VName -> [IsaType]
getFieldTypes ctab c = maybe [] (argTypes . fst) $
Map.lookup c ctab
argTypes :: IsaType -> [IsaType]
IsaSign.Type name _ [b, c] | isFunArrow name -> b : argTypes c
-------------------------- TERMS ----------------------------------------------
-------- lifting, tuples, multiple abstractions and applications, fixpoints ---
funFliftbin :: Term -> Term
funFliftbin f = termMAppl NotCont (conDouble fliftbinS) [f]
termMAbs :: Continuity -> [Term] -> Term -> Term
v:vs -> if isDicConst v then (termMAbs c vs t) else
termMAppl :: Continuity -> Term -> [Term] -> Term
let prelTest vn = any (\x -> isPrefixOf x $
IsaSign.orig vn)
(Const vn _, [a]) | isDicConst t || prelTest vn -> a
Const vn _ | isDicConst v || prelTest vn -> termMAppl c t vs
_ -> termMAppl c (App t v c) vs
----------------------- connectives -------------------------------------------
tupleSelector :: Int -> Int -> Term -> Continuity -> Term
| n == mx = tupleSelect (n - 1) t c
| True = termMAppl c (conDouble (if isCont c then "cfst" else "fst"))
$ [tupleSelect (n - 1) t c]
tupleSelect :: Int -> Term -> Continuity -> Term
tupleSelect n t c = case n of
(termMAppl c (conDouble $ if isCont c then "csnd" else "snd") [t]) c
------------------------------------- term filters ----------------------------
isDicConst :: Term -> Bool
constFilter :: Term -> [Term]
constFilter t = case t of
IsaSign.If x y z _ -> concatMap constFilter [x, y, z]
IsaSign.Let xs y -> concatMap constFilter $ y : map snd xs
elPos :: [Term] -> Term -> Maybe Int
elPos ls x = fmap (+ 1) $ findIndex (constEq x) ls
-------------------- subterm extraction -------------------------------------
extFBody :: Term -> (Term, [Term])
extFBody t' = extFB t' []
extTBody :: Term -> (Term, [Term])
extTBody t' = extTB t' []
------------------- eliminating case expressions ---------------------------
destCaseS :: Continuity -> IsaTerm -> IsaTerm -> [IsaTerm] -- t is def rh
[holEq (termMAppl c d xs) y | (xs,y) <- destCaseU (extFBody t,[])]
destCaseU :: ((IsaTerm,[IsaPattern]),[IsaPattern]) -> [([IsaPattern],IsaTerm)]
destCaseU ((t,rs),ks) = case (t,rs) of
(Case v ls, vv : vs) -> if v == vv
then [(ks ++ [l], termMAbs NotCont vs m) | (l,m) <- ls]
else destCaseU ((t,vs), ks ++ [vv])
destCase :: IsaTerm -> (VName -> VName) -> [(IsaPattern,IsaTerm)]
destCase t f = let w = extFBody t in case w of
(Case v ls, _ : vs) -> case v of
[(renVars (Free (f n)) [l] l,
-- repl. l if l is a var.
[l] (termMAbs NotCont vs m)) | (l, m) <- ls]
_ -> [(l,termMAbs NotCont vs m) | (l, m) <- ls]
----------------------------- equivalence on terms ---------------------------
constEq :: Term -> Term -> Bool
constEq t1 t2 = case (t1,t2) of
(Const m x, Const n y) -> n == m && typEq x y
{- this functions was actually meant to compare only constructors -
check out, there might be bugs -}
simTerms :: Term -> Term -> Bool
simTerms t1 t2 = case (t1, t2) of
(If _ _ _ c, If _ _ _ d) -> c == d
(Case _ _, Case _ _) -> True
(Let _ _, Let _ _) -> True
(IsaEq _ _, IsaEq _ _) -> True
(Tuplex _ _, Tuplex _ _) -> True
------------------------ replacement functions -------------------------------
{- in term t, replaces variable f for variables in ls -}
renVars :: Term -> [Term] -> Term -> Term
renVars f ls t = case t of
IsaSign.If (renVars f ls x) (renVars f ls y) (renVars f ls z) c
IsaSign.Case (renVars f ls x) [(a,renVars f ls b) | (a,b) <- ys]
IsaSign.Let [(a,renVars f ls b) | (a,b) <- xs] (renVars f ls y)
renFuns :: (Term -> Maybe Term) -> Term -> Term
IsaSign.If (renFuns f x) (renFuns f y) (renFuns f z) c
IsaSign.Let [(a,renFuns f b) | (a,b) <- xs] (renFuns f y)
---------------------- SENTENCES ---------------------------------------------
--------------------- getting info from sentences ----------------------------
newConstTab c ls = if isCont c then
Map.empty else
Map.fromList [(mkVName $ extAxName x, extAxType x) | x <- ls]
extAxName :: Named Sentence -> String
extAxType :: Named Sentence -> Typ
NamedSen _ True _ (ConstDef (IsaEq (Const _ t) _)) -> t
(RecDef _ ((App (App _ (App (Const _ t) _ _) _) _ _ : _) : _)) -> t
extFunTerm :: Named Sentence -> Term
NamedSen _ _ _ (ConstDef (IsaEq t _)) -> fst $ extTBody t
extLeftH :: Named Sentence -> Term
NamedSen _ _ _ (ConstDef (IsaEq t _)) -> t
extRightH :: Named Sentence -> Term
NamedSen _ _ _ (ConstDef (IsaEq _ t)) -> t
{- left comp is the def name, right comp are the constants in the def -}
sentAna :: Named Sentence -> (Term, [Term])
NamedSen _ True _ (ConstDef (IsaEq l r)) -> (l, constFilter r)
------------------ checking for mutually recursive function defs -------------
getDepSent :: [[Named Sentence]] -> [[Named Sentence]]
getDepSent ls = abGetDep sentDepOn ls
sentDepOn :: Named Sentence -> Named Sentence -> Bool
depOn (\ u v -> simTerms u v && typEq (termType u) (termType v))
(fst . sentAna) (snd . sentAna) x y
------------------- adding fixpoints ---------------------------------------
fixMRec :: Continuity -> [[Named Sentence]] -> [Named Sentence]
fixMRec c ls = addFixPoints c $ getDepSent ls
addFixPoints :: Continuity -> [[Named Sentence]] -> [Named Sentence]
addFixPoints c xs = concatMap (fixPoint c) xs
fixPoint :: Continuity -> [Named Sentence] -> [Named Sentence]
fixPoint c xs = case xs of
NamedSen l m n (ConstDef (IsaEq lh rh)) -> case c of
[NamedSen l m n $ RecDef fixrecS [[holEq lh rh]]]
NotCont -> [NamedSen l m n $ RecDef primrecS
jn = joinNames (map extAxName xs) -- name is ininfluential here
ys = [[holEq (extLeftH x) $ extRightH x] | x <- xs]
in [NamedSen jn True False $ RecDef fixrecS ys]
jj = joinNames (map extAxName xs)
jt1 = unifyTVars (map extAxType xs)
(typTuple NotCont (renTVars jtls))
yys = [destCase x (\ _ -> jn) | x <- rs]
zs = [(p,Tuplex (map (renFuns (newFCons (Const jn noType) ls)) ts)
os = [mkNewDef x jj n m jtls jta | (x,m) <- listEnum xs]
ps = (NamedSen jj True False $ makeRecDef jl zs):os
typeTupleTrivInst :: Int -> [Typ] -> Typ -> Typ
typeTupleTrivInst n tls t = mkFunType t
(typTuple NotCont (renTrivTVars n tls))
renTrivTVars :: Int -> [Typ] -> [Typ]
renTrivTVars m tls = [renTVar m b a | (a, b) <- listEnum tls]
renTVar x n t = if x == n then t else
TFree y s -> if (take 2 y == "vX") then t else
mkNewDef :: Named Sentence -> String -> Int -> Int -> [Typ] -> Typ
mkNewDef s z x y tls t = let -- x is the max
NamedSen l m n (ConstDef (IsaEq lh rh)) -> case (lh, extFBody rh) of
(Const _ _, (_, w : ws)) ->
NamedSen l m n (ConstDef (IsaEq lh $
termMAbs a (w:ws) $ termMAppl a (tupleSelector x y
(App (Const (mkVName z) zt) w a) a) ws))
makeRecDef :: Term -> [(Term,Term)] -> Sentence
RecDef primrecS [map (\ (a, b) -> holEq (App t a NotCont) b) ls]
reassemble :: [[(Term,Term)]] ->
Map.Map Term [Term] -- [(b, [c])]
newFCons :: Term -> [Term] -> Term -> Maybe Term
newFCons t ls k = case k of
App n w NotCont -> case elPos ls n of
Just $ tupleSelector (length ls) i (
IsaSign.App t w NotCont) NotCont