content: {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/Hs2HOLCFaux.hs
  Copyright   :  (c) Paolo Torrini and Till Mossakowski and Uni Bremen 2004-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  paolot@informatik.uni-bremen.de
  Stability   :  provisional
  Portability :  non-portable (depends on programatica using MPTC)
  
  auxiliary functions for the embedding comorphism from Haskell to Isabelle
  -}
  
  module Comorphisms.Hs2HOLCFaux
      ( PrDecl
      , aweLits
      , mthEq
      , removeEL
      , extAxType
      , extTBody
      , fixMRec
      , newConstTab
      , getTermName
      , extRightH
      , ExpRole (..)
      , ISign
      , IsaSort
      , IsaType
      , IsaPattern
      , IsaTerm
      , IsaName (..)
      , xDummy
      , termMAbs
      , termMAppl
      , termBAppl
      , PrExp
      , PrPat
      , renVars
      , remove_duplicates
      , HsType
      , HsScheme
      , HsId
      , getInstClass
      , getInstType
      , repVarClass
      , constrVarClass
      , getLitName
      , transTN
      , transPath
      , showIsaS
      , funFliftbin
      , funFlift2
      , VaMap
      , AConstTab
      , liftMapByListD
      , nothingFiOut
      , IsaTypeInsts
      , IsaVT (..)
      , TyMap
      , liftMapByList
      , HsTypeInfo
      , HsInstance
      , HsInstances
      , extClassInfo
      , extAbbrsInfo
      , groupInst
      , getMainInstType
      , prepInst
      , checkTyCons
      , getDepDoms
      , getDomType
      , getFieldTypes
      , isCont
      , replaceTyVar
      , varDouble
      , mthTy
      , mthAll
      , enElem
      , getContinuity
      ) where
  
  import Data.List
  import qualified Data.Map as Map
  import Data.Maybe (fromMaybe)
  
  import Common.AS_Annotation
  import Common.Utils (number, nubOrd)
  
  -- Haskell (Programatica)
  import SourceNames
  import TiTypes
  import TiInstanceDB
  
  import PNT
  import PosName
  import UniqueNames
  
  import TiPropDecorate
  import PropSyntaxStruct as HsName
  
  import TiDecorate
  
  -- Isabelle
  import Isabelle.IsaSign as IsaSign
  import Isabelle.IsaConsts as IsaConsts
  import Isabelle.Translate as Translate
  
  import Debug.Trace
  
  {- ----------------------------- TYPE synonyms --------------------------
  ---------------- Haskell --------------------------------------------- -}
  
  type HsInstance = TiInstanceDB.Instance PNT
  type HsInstances = [TiInstanceDB.Instance PNT]
  type HsPred = TiTypes.Pred PNT
  type HsType = TiTypes.Type PNT -- same as HsPred
  type HsClass = TiTypes.Type PNT
  type HsScheme = TiTypes.Scheme PNT
  type HsId = HsIdentI PNT
  type HsTypeInfo = TiTypes.TypeInfo PNT
  type PrDecl = TiPropDecorate.TiDecl PNT
  type PrExp = TiPropDecorate.TiExp PNT
  type PrPat = TiDecorate.TiPat PNT
  
  type HId i = HsIdentI i
  
  type VaMap = Map.Map HsId HsScheme
  type TyMap = Map.Map HsId (Kind, HsTypeInfo)
  
  -- ---------------- Isabelle --------------------------------------------
  
  type ISign = IsaSign.Sign
  type IsaSort = IsaSign.Sort
  type IsaType = IsaSign.Typ
  type IsaTerm = IsaSign.Term
  type IsaPattern = IsaSign.Term
  type IsaTypeInsts = (TName, [(IsaClass, [(IsaType, [IsaClass])])])
  
  -- ------------------------ list functions ------------------------------
  
  removeEL :: [[a]] -> [[a]]
  removeEL = filter (not . null)
  
  remove_duplicates :: Ord a => [a] -> [a]
  remove_duplicates = nubOrd
  
  -- ------------------------- 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 ----------
  
  getDepDoms :: IsaSign.DomainTab -> IsaSign.DomainTab
  getDepDoms = abGetDep deDepOn
  
  abGetDep :: Ord a => (a -> a -> Bool) -> [[a]] -> [[a]]
  abGetDep f ls = case ls of
   x : xs ->
     remove_duplicates $
        removeEL (map remove_duplicates
                     (checkDep (liftDep (mutRel f)) xs [x] []))
   [] -> []
  
  checkDep :: ([x] -> [x] -> Bool) -> [[x]] -> [[x]] -> [[x]] -> [[x]]
  checkDep f ls ms cs = case ls of
    a : as -> case ms of
       b : bs ->
          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) []
    [] -> ms
  
  -- mutual dependence
  mutRel :: (a -> a -> Bool) -> a -> a -> Bool
  mutRel f x y = f x y && f y x
  
  {- ------------------ HASKELL representation -------------------------------
  --------------------- check functions ----------------------------------- -}
  
  checkTyCons :: HsId -> Bool
  checkTyCons d = case d of
    HsCon _ -> True
    _ -> False
  
  {- -------------------------- get functions -------------------------------
  ----------------- getting info from Haskell types ---------------------- -}
  
  getLitName :: HsType -> PNT
  getLitName (Typ t) = case t of
     HsTyVar x -> x
     HsTyCon x -> x
     _ -> error "Hs2HOLCFaux.getLitName"
  
  -- ---------------- getting class and type ouf of predicate --------------
  
  getInstType :: HsPred -> HsType
  getInstType x = case x of (Typ (HsTyApp _ t)) -> t
                            _ -> trace ("\n TYPE: " ++ show x) $
                                 error "Hs2HOLCFaux.getInstType"
  
  getInstClass :: HsPred -> HsType
  getInstClass x = case x of (Typ (HsTyApp c _)) -> c
                             _ -> trace ("\n CLASS: " ++ show x) $
                                  error "Hs2HOLCFaux.getInstClass"
  
  -- --------------------- getting class information -----------------------
  
  extClassInfo :: HsTypeInfo -> [HsClass]
  extClassInfo p = case p of
          TiTypes.Class a _ _ _ -> map getInstClass a
          _ -> error "Hs2HOLCFaux.extClassInfo"
  
  -- ------------------------- getting info on type syns -------------------
  
  extAbbrsInfo :: HsTypeInfo -> ([PNT], HsType)
  extAbbrsInfo p = case p of
             TiTypes.Synonym ls t -> (ls, t)
             _ -> error "Hs2HOLCFaux.extAbbrsInfo"
  
  -- ------------ get 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])]
  prepInst1 i =
    [(x, [getInstClass y | y <-
            getInstPrems i, showIsaHsTypeString (getInstType y)
                             == showIsaHsTypeString x])
               | x <- nub $ map getInstType (getInstPrems i)]
  
  -- ------------------- ISABELLE representation ---------------------------
  
  data ExpRole = FunDef | InstDef  -- no PLogic yet
    deriving (Ord, Eq, Show)
  
  -- --------------------------- constants ---------------------------------
  
  xDummy :: IsaTerm
  xDummy = conDouble "dummy"
  
  holEq :: IsaTerm -> IsaTerm -> IsaTerm
  holEq t1 t2 = termMAppl NotCont (con eqV) [t1, t2]
  
  getTermName :: Term -> Maybe String
  getTermName a = case a of
    Const x _ -> Just $ new x
    Free x -> Just $ new x
    _ -> Nothing -- "_"
  
  -- ---------------------- Haskell names --------------------------------
  
  enElem :: String -> [String] -> Bool
  enElem s ls = let
              ks = map showIsaName ls
              hs = map (++ "DF") ks
              js = map (++ "I") hs
      in elem s $ ks ++ hs ++ js
  
  mthTy :: Continuity -> String -> String -> IsaType
  mthTy c k p
   | enElem p ["==", "/=", "<", "<=", ">", ">="] = aaT c k (boolT c)
   | enElem p (["min", "max", "+", "-", "*", "quot", "rem"]
               ++ ["div", "mod", "\\"]) = aaA c k
   | enElem p ["succ", "pred", "negate", "abs", "signum", "recip"] = aA c k
   | enElem p ["enumFromThen", "enumFromTo"] = aaL c k
   | enElem p ["minBound", "maxBound"] = TFree "a" (IsaClass k : sortT c)
   | enElem p ["quotRem", "divMod"] = aaP c k
   | enElem p ["toEnum"] = aT c k (intT c)
   | enElem p ["enumFrom"] = aL c k
   | enElem p ["enumFromThenTo"] = aaaL c k
   | enElem p ["fromEnum"] = tA c k (intT c)
   | enElem p ["fromInteger"] = tA c k (integerT c)
   | enElem p ["fromFractional"] = tA c k (fracT c)
   | enElem p ["toInteger"] = aT c k (integerT c)
   | enElem p ["compare"] = aaT c k (orderingT c)
   | otherwise = trace (show p) $ error "HsHOLCFaux, mthTy"
  
  aaT :: Continuity -> String -> IsaType -> IsaType
  aaT c k h = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w, w] h
  
  aaA :: Continuity -> String -> IsaType
  aaA c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w, w] w
  
  aL :: Continuity -> String -> IsaType
  aL c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w] $ listT c w
  
  aaL :: Continuity -> String -> IsaType
  aaL c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w, w] $ listT c w
  
  aaaL :: Continuity -> String -> IsaType
  aaaL c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w, w, w] $ listT c w
  
  aaP :: Continuity -> String -> IsaType
  aaP c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w, w] $ prodT c w w
  
  tA :: Continuity -> String -> IsaType -> IsaType
  tA c k h = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [h] w
  
  aT :: Continuity -> String -> IsaType -> IsaType
  aT c k h = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w] h
  
  aA :: Continuity -> String -> IsaType
  aA c k = let w = TFree "a" (IsaClass k : sortT c)
     in curryFunT c [w] w
  
  -- method names
  mthEq, mthOrd, mthEnum, mthBounded, mthNum, mthIntegral :: [String]
  mthMonad, mthFunctor, mthAll, aweLits, mthFractional :: [String]
  
  mthEq = ["==", "/="]
  mthOrd = ["compare", "<", "<=", ">", ">=", "max", "min"]
  mthEnum = ["succ", "pred", "toEnum", "fromEnum", "enumFrom",
                 "enumFromThen", "enumFromTo", "enumFromThenTo"]
  mthBounded = ["minBound", "maxBound"]
  mthNum = ["+", "-", "*", "negate", "abs", "signum", "fromInteger"]
  mthIntegral = ["quot", "rem", "div", "mod", "quotRem", "divMod", "toInteger"]
  mthMonad = ["return", ">>=", ">>", "fail"]
  mthFunctor = ["fmap"]
  mthFractional = ["/", "recip", "fromRational"]
  mthAll = mthEq ++ mthOrd ++ mthEnum ++ mthNum
                ++ mthIntegral ++ mthFractional ++ mthBounded
  aweLits = mthMonad ++ mthFunctor ++ mthEq ++ ["+", "-", "*"]
  
  nameListA, nameListB, nameListC, nameListD :: [String]
  nameListE, nameListF, nameListH :: [String]
  
  -- Special translation - operators
  nameListA = ["&&", "||", "==", "/=", "<", "<=", ">", ">=", "+",
    "*", "-", "^",
    "^^", "++", "!!", "/", ".", "$", "$!", ">>=", ">>"]
  
  -- dual translation - constructors
  nameListB = ["()", "(,)", "True", "False", ":", "[]", "Just", "Nothing"]
  
  -- dual translation operators
  nameListC = ["primError", "return"]
  
  -- other constructors
  nameListD = ["ET", "EQ", "GT", "Left", "Right"]
  
  -- Prelude functions
  nameListE = -- map (\x -> x ++ "'")
    ["not", "min", "max", "negate", "abs", "signum",
    "fromInteger", "succ", "pred", "fromEnum", "toEnum", "enumFrom",
    "enumFromThen", "enumFromTo", "enumFromThenTo",
    "minBound", "maxBound", "toRational", "quot", "rem", "div", "mod",
    "quotRem", "divMod", "toInteger", "otherwise", "either", "maybe",
    "fst", "snd", "id", "curry", "uncurry", "const", "until", "asTypeOf",
    "odd", "even", "subtract", "flip", "gcd", "lcm", "seq", "error",
    "undefined", "fromRational", "recip", "powAux", "powBux"]
  
  -- Prelude list functions
  nameListF = -- map (\x -> x ++ "'")
    ["map", "filter", "concat", "concatMap", "head", "last", "tail",
    "init", "null", "length", "foldl", "foldl1", "scanl", "scanl1",
    "foldr", "foldr1", "scanr", "scanr1", "iterate", "repeat",
    "replicate", "cycle", "take", "drop", "splitAt", "takeWhile",
    "dropWhile", "span", "break", "lines", "words", "unlines",
    "unwords", "reverse", "and", "or", "any", "all", "elem", "notElem",
    "lookup", "sum", "product", "maximum", "minimum", "zip", "zip3",
    "zipWith", "zipWith3", "unzip", "unzip3"]
  
  -- hidden
  nameListH = ["flip", "&&", "||", "conj", "disj", "error", "otherwise",
               "comp", "subtract", "map", ".", "not", "break", "fst", "snd"]
  
  primedS :: String -> String
  primedS s = s ++ "'"
  
  trOSym :: String -> String
  trOSym s = case s of
       "&&" -> "conj"
       "||" -> "disj"
       "==" -> "="
       "/=" -> "~="
       "<" -> "less"
       "<=" -> "leq"
       ">" -> "more"
       ">=" -> "meq"
       "+" -> "+"
       "*" -> "*"
       "-" -> "-"
       "^" -> "pow"
       "^^" -> "fpow"
       "++" -> "bconcat"
       "!!" -> "nth"
       "/" -> "frac"
       "." -> "comp"
       "$" -> "apply"
       "$!" -> "sapply"
       ">>=" -> "mbind"
       ">>" -> "mbbind"
       _ -> error "Hs2HOLCFaux,trOSym"
  
  transPrelude :: (String -> String) -> String -> String
  transPrelude f s = let ns = init s
    in if elem s (nameListB ++ nameListC ++ nameListD) then s
       else if elem s (nameListE ++ nameListF)
       then s ++ (if elem s (mthAll ++ nameListH ++ ["tail", "head"])
                   then "H" else "U")
       else if elem s (map primedS (nameListE ++ nameListF))
       then ns ++ (if elem ns (mthAll ++ nameListH)
                    then "H" else "U")
       else if elem s nameListA
       then if elem s aweLits then trOSym s
            else trOSym s ++ (if elem s (mthAll ++ nameListH)
                          then "H" else "U")
       else if elem ns nameListA && last s == '#'
       then if elem ns aweLits then trOSym ns
            else trOSym ns ++ (if elem ns (mthAll ++ nameListH)
                           then "H" else "U")
       else if take 9 s == "default__"
       then transPrelude f (drop 9 s) ++ "DF"
       else if take 3 s == "$--"
       then transPrelude f (drop 3 s) ++ "I"
       else f s
  
  {- ------------------------- Name translation ----------------------------
  Translating to strings compatible with Isabelle -}
  
  class IsaName a where
   showIsaName :: a -> String
   showIsaString :: a -> String
  
  showIsaS :: String -> String
  showIsaS = transPrelude (transConstStringT HOLCF_thy)
  
  instance IsaName String where
    showIsaName = showIsaS
    showIsaString = id
  
  showIsaHsN :: Show a => (String -> a) -> HsName.HsName -> a
  showIsaHsN f t = case t of
         Qual _ y -> f y
         UnQual w -> f w
  
  instance IsaName PNT.PId where
    showIsaName (PN x _) = showIsaS x
    showIsaString (PN x _) = x
  
  instance IsaName HsName.HsName where
    showIsaName = showIsaHsN showIsaS
    showIsaString = showIsaHsN id
  
  instance IsaName PosName.HsName where
    showIsaName (SN x _) = showIsaName x
    showIsaString (SN x _) = showIsaString x
  
  instance IsaName PNT.PName where
    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
                   HsVar x -> showIsaName x
                   HsCon x -> showIsaName x
    showIsaString t = case t of
                   HsVar x -> showIsaString x
                   HsCon x -> showIsaString x
  
  showIsaHsTypeString :: HsType -> String
  showIsaHsTypeString (Typ t) = case t of
      HsTyFun _ _ -> "Fun"
      HsTyApp _ _ -> "App"
      HsTyVar x -> showIsaString x
      HsTyCon x -> showIsaString x
      HsTyForall _ _ x -> showIsaHsTypeString x
  
  -- ------ auxiliary name functions depending on IsaSign -----------------
  joinNames :: [String] -> String
  joinNames = concatMap (++ "_X")
  
  isCont :: Continuity -> Bool
  isCont x = x == IsCont True || x == IsCont False
  
  getContinuity :: Continuity -> IsaTerm -> Continuity
  getContinuity c t = case t of
    IsaSign.Const _ w -> case (kon w, c) of
          (_, NotCont) -> c
          (TCon, IsCont _) -> IsCont False  -- unlifted for constructors
          (_, IsCont _) -> IsCont True   -- lifted for the rest
    IsaSign.App {} -> continuity t
    IsaSign.Abs {} -> continuity t
    IsaSign.If {} -> continuity t
    IsaSign.Tuplex _ _ -> continuity t
    _ -> c
  
  transTN :: Continuity -> String -> String -> String
  transTN c s1 s2 = let d = transPath s1 s2
                        ic = isCont c
      in if s1 == "Prelude" then case s2 of
          "()" -> if ic then "unitT"
                        else "unit"
          "Int" -> if ic then "intT"
                        else "int"
          "Integer" -> if ic then "integerT"
                        else "int"
          "Char" -> if ic then "charT"
                        else "char"
          "Bool" -> if ic then "lBool"
                        else "bool"
          "[]" -> if ic then "llist"
                        else "list"
          "Either" -> if ic then "lEither"
                        else "either"
          "Ordering" -> if ic then "lOrdering"
                        else "sOrdering"
          "String" -> if ic then "lString"
                        else "string"
          "Maybe" -> if ic then "lMaybe"
                        else "option"
          "(,)" -> if ic then "lprod" else "*"
          "Rational" -> if ic then "ratT" else "rat"
          _ -> d
      else d
  
  transPath :: String -> String -> String
  transPath s1 s2 = showIsaName s1 ++ "_" ++ showIsaName s2
  
  -- --------------- getting info about domaintab -------------------------
  
  type AConstTab = Map.Map VName (Typ, IsaVT)
  data IsaVT = IsaConst | IsaVal deriving (Eq, Show)
  
  getDomType :: AConstTab -> VName -> IsaType
  getDomType ctab c = maybe (error "Hs2HOLCFaux.getDomType")
      (getHeadType . fst) $ Map.lookup c ctab
  
  isFunArrow :: String -> Bool
  isFunArrow name = elem name [funS, cFunS, lFunS]
  
  getHeadType :: IsaType -> IsaType
  getHeadType t = case t of
    IsaSign.Type name _ [_, t2] | isFunArrow name -> getHeadType t2
    _ -> t
  
  getFieldTypes :: AConstTab -> VName -> [IsaType]
  getFieldTypes ctab c = maybe [] (argTypes . fst) $ Map.lookup c ctab
  
  argTypes :: IsaType -> [IsaType]
  argTypes a = case a of
      IsaSign.Type name _ [b, c] | isFunArrow name -> b : argTypes c
      _ -> []
  
  -- ----------------------- Instances ------------------------------------
  
  groupInst :: [IsaTypeInsts] -> [IsaTypeInsts]
  groupInst db =
    remove_duplicates [(y,
          remove_duplicates $ concat
                        [b | (a, b) <- db, a == y]) | (y, _) <- db]
  
  {- --------------------- TERMS ------------------------------------------
  lifting, tuples, multiple abstractions and applications, fixpoints -- -}
  
  funFliftbin :: Term -> Term
  funFliftbin f = termMAppl NotCont (conDouble lliftbinS) [f]
  
  funFlift2 :: Term -> Term
  funFlift2 f = termMAppl NotCont (conDouble flift2S) [f]
  
  varDouble :: String -> Term
  varDouble = Free . mkVName
  
  termMAbs :: Continuity -> [Term] -> Term -> Term
  termMAbs c ts t =
   case ts of
     [] -> t
     v : vs -> if isDicConst v then termMAbs c vs t else
        IsaSign.Abs v (termMAbs c vs t) c
  
  termMAppl :: Continuity -> Term -> [Term] -> Term
  termMAppl c t ts =
    let prelTest vn = any (\ x -> isPrefixOf x $ IsaSign.orig vn)
                 [ "inst__Prelude_"
                 , "derived__Prelude_"]
   in case (t, ts) of
     (Const vn _, [a]) | isDicConst t || prelTest vn -> a
     (_, []) -> t
     (_, v : vs) -> case v of
           Const vn _ | isDicConst v || prelTest vn -> termMAppl c t vs
           _ -> termMAppl c (App t v $ getContinuity c t) vs
  
  termBAppl :: Continuity -> Term -> Term -> Term -> Term
  termBAppl c t1 t2 t3 = termMAppl c t1 [t2, t3]
  
  termSAppl :: Continuity -> Term -> Term -> Term
  termSAppl c t1 t2 = termMAppl c t1 [t2]
  
  -- --------------------- connectives ------------------------------------
  
  tupleSelector :: Int -> Int -> Term -> Continuity -> Term
  tupleSelector mx n t c
    | mx < 2 = error "Hs2HOLCFaux.tupleSelector1"
    | n == 0 = error "Hs2HOLCFaux.tupleSelector2"
    | mx < n = error "Hs2HOLCFaux.tupleSelector3"
    | n == mx = tupleSelect (n - 1) t c
    | otherwise = termMAppl c (fstPT c) [tupleSelect (n - 1) t c]
  
  tupleSelect :: Int -> Term -> Continuity -> Term
  tupleSelect n t c = case n of
    0 -> t
    _ -> tupleSelect (n - 1)
       (termMAppl c (sndPT c) [t]) c
  
  -- ---------------------------- term filters ----------------------------
  
  isDicConst :: Term -> Bool
  isDicConst t = case t of
      Const vn _ | IsaSign.orig vn == "DIC" -> True
      Free vn | IsaSign.orig vn == "DIC" -> True
      _ -> False
  
  constFilter :: Term -> [Term]
  constFilter t = case t of
   IsaSign.Const _ _ -> [t]
   IsaSign.Abs _ x _ -> constFilter x
   IsaSign.App x y _ -> concatMap constFilter [x, y]
   IsaSign.If x y z _ -> concatMap constFilter [x, y, z]
   IsaSign.Case x ys -> concatMap constFilter $ x : map snd ys
   IsaSign.Let xs y -> concatMap constFilter $ y : map snd xs
   IsaSign.IsaEq x y -> concatMap constFilter [x, y]
   IsaSign.Tuplex xs _ -> concatMap constFilter xs
   _ -> [t]
  
  elPos :: [Term] -> Term -> Maybe Int
  elPos ls x = fmap (+ 1) $ findIndex (constEq x) ls
  
  -- ---------------- subterm extraction ----------------------------------
  
  extFBody :: Term -> (Term, [Term])
  extFBody t' = extFB t' []
   where
    extFB t as = case t of
       IsaSign.Abs x b _ -> extFB b (x : as)
       _ -> (t, reverse as)
  
  extTBody :: Term -> (Term, [Term])
  extTBody t' = extTB t' []
   where
    extTB t as = case t of
       IsaSign.App a x _ -> extTB a (x : as)
       _ -> (t, reverse as)
  
  -- ------------- eliminating case expressions ---------------------------
  
  destCaseS :: Continuity -> IsaTerm -> IsaTerm -> [IsaTerm]
  destCaseS c d t =
      [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])
      _ -> error "Hs2HOLCFaux.destCaseU"
  
  destCase :: IsaTerm -> (VName -> VName) -> [(IsaPattern, IsaTerm)]
  destCase t f = let w = extFBody t in case w of
      (Case v ls, _ : vs) -> case v of
            Free n ->
                  [(renVars (Free (f n)) [l] l, -- repl. l if l is a var.
                    renVars (Free (f n))
                           [l] (termMAbs NotCont vs m)) | (l, m) <- ls]
            _ -> [(l, termMAbs NotCont vs m) | (l, m) <- ls]
      _ -> error "Hs2HOLCFaux.destCase"
  
  -- --------------------- equivalence on terms ---------------------------
  
  constEq :: Term -> Term -> Bool
  constEq t1 t2 = case (t1, t2) of
    (Const m x, Const n y) -> n == m && typEq (typ x) (typ y)
    _ -> False
  
  simTerms :: Term -> Term -> Bool
  simTerms t1 t2 = case (t1, t2) of
   (IsaSign.Const x w, IsaSign.Const y z) ->
          x == y && (if take 6 (new x) == "mbind_" ||
                        take 7 (new x) == "return_"
              then typ w == noTypeT || typ z == noTypeT ||
                                       typSim (typ w) (typ z)
              else typSim (typ w) (typ z))
   (IsaSign.Free _, IsaSign.Free _) -> True
   (IsaSign.Abs _ _ c, IsaSign.Abs _ _ d) -> c == d
   (If _ _ _ c, If _ _ _ d) -> c == d
   (Case _ _, Case _ _) -> True
   (Let _ _, Let _ _) -> True
   (IsaEq _ _, IsaEq _ _) -> True
   (Tuplex _ _, Tuplex _ _) -> True
   _ -> False
  
  -- ------------------ 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.Free _ -> if elem t ls then f else t
   IsaSign.Abs v x c -> IsaSign.Abs v (renVars f ls x) c
   IsaSign.App x y c -> termSAppl c (renVars f ls x) (renVars f ls y)
   IsaSign.If x y z c ->
       IsaSign.If (renVars f ls x) (renVars f ls y) (renVars f ls z) c
   IsaSign.Case x ys ->
       IsaSign.Case (renVars f ls x) [(a, renVars f ls b) | (a, b) <- ys]
   IsaSign.Let xs y ->
       IsaSign.Let [(a, renVars f ls b) | (a, b) <- xs] (renVars f ls y)
   IsaSign.IsaEq x y -> IsaSign.IsaEq (renVars f ls x) (renVars f ls y)
   IsaSign.Tuplex xs c -> IsaSign.Tuplex (map (renVars f ls) xs) c
   _ -> t
  
  renFuns :: (Term -> Maybe Term) -> Term -> Term
  renFuns f t = case t of
   IsaSign.Abs v x c -> IsaSign.Abs v (renFuns f x) c
   IsaSign.App x y c -> fromMaybe (termSAppl c (renFuns f x) (renFuns f y)) $ f t
   IsaSign.If x y z c ->
       IsaSign.If (renFuns f x) (renFuns f y) (renFuns f z) c
   IsaSign.Case x ys ->
       IsaSign.Case (renFuns f x) [(a, renFuns f b) | (a, b) <- ys]
   IsaSign.Let xs y ->
       IsaSign.Let [(a, renFuns f b) | (a, b) <- xs] (renFuns f y)
   IsaSign.IsaEq x y -> IsaSign.IsaEq (renFuns f x) (renFuns f y)
   IsaSign.Tuplex xs c -> IsaSign.Tuplex (map (renFuns f) xs) c
   _ -> t
  
  {- -------------------- SENTENCES ----------------------------------------
  ------------------- getting info from sentences ----------------------- -}
  
  newConstTab :: Continuity -> [Named IsaSign.Sentence] -> ConstTab
  newConstTab c ls = if isCont c then Map.empty else
      Map.fromList [(mkVName $ extAxName x, extAxType x) | x <- ls]
  
  extAxName :: Named Sentence -> String
  extAxName = senAttr
  
  extAxType :: Named Sentence -> Typ
  extAxType s = case extFunTerm s of
    Const _ t | isAxiom s -> typ t
    _ -> noTypeT
  
  {-
  extAxType :: Named Sentence -> Typ
  extAxType s = case sentence s of
    ConstDef (IsaEq (Const _ t) _) | isAxiom s -> (typ t)
    RecDef _ ((App (App _ (App (Const _ t) _ _) _) _ _ : _) : _)
                                                  | isAxiom s -> (typ t)
    _ -> noTypeT
  -}
  extFunTerm :: Named Sentence -> Term
  extFunTerm s = case sentence s of
    ConstDef (IsaEq t _) -> fst $ extTBody t
    RecDef _ _ _ (App (App _ x _) _ _ : _) -> fst $ extTBody x
    _ -> error "Hs2HOLCFaux.extFunTerm"
  
  extLeftH :: Named Sentence -> Term
  extLeftH s = case sentence s of
    ConstDef (IsaEq t _) -> t
    _ -> error "Hs2HOLCFaux.extLeftH"
  
  extRightH :: Named Sentence -> Term
  extRightH s = case sentence s of
    ConstDef (IsaEq _ t) -> t
    _ -> error "Hs2HOLCFaux.extRightH"
  
  -- left comp is def name, right comp are constants in the def
  sentAna :: Named Sentence -> (Term, [Term])
  sentAna s = case sentence s of
    ConstDef (IsaEq l r) | isAxiom s -> (l, constFilter r)
    _ -> error "Hs2HOLCFaux.sentAna"
  
  -- ------------ checking for mutually recursive function defs ----------
  
  getDepSent :: [[Named Sentence]] -> [[Named Sentence]]
  getDepSent = abGetDep sentDepOn
  
  getExpRole :: Named Sentence -> ExpRole
  getExpRole n = case extFunTerm n of
     Const _ x -> case kon x of
          TMet -> InstDef
          _ -> FunDef
     _ -> error "Hs2HOLCFaux, getExpRole"
  
  depOn :: (a -> b -> Bool) -> (c -> a) -> (c -> [b]) -> c -> c -> Bool
  depOn f g h x y = any (f (g x)) (h y)
  
  sentDepOn :: Named Sentence -> Named Sentence -> Bool
  sentDepOn x y = case getExpRole x of
     InstDef ->
          depOn (\ u v -> simTerms u v
                 && typEq (typ $ termType u) (typ $ termType v))
              (fst . sentAna) (snd . sentAna) x y
     FunDef -> depOn simTerms (fst . sentAna) (snd . sentAna) x y
  
  -- ----------------- adding fixpoints ------------------------------------
  
  fixMRec :: Continuity -> [[Named Sentence]] -> [Named Sentence]
  fixMRec c ls = let xs = getDepSent ls
      in addFixPoints c xs
  
  addFixPoints :: Continuity -> [[Named Sentence]] -> [Named Sentence]
  addFixPoints c = concatMap (fixPoint c)
  
  fixPoint :: Continuity -> [Named Sentence] -> [Named Sentence]
  fixPoint c xs = case xs of
    [a] -> if sentDepOn a a then [mapNamed ( \ s -> case s of
             ConstDef (IsaEq lh rh) -> case c of
               IsCont _ -> RecDef (Just fixrecS) (mkVName . senAttr $ a)
                Nothing [holEq lh rh]
               NotCont -> RecDef Nothing (mkVName . senAttr $ a)
                Nothing (destCaseS c lh rh)
             _ -> error "Hs2HOLCFaux.fixPoint") a]
           else xs
    _ : _ -> case c of
      IsCont _ -> let
           jn = joinNames (map extAxName xs) -- name is ininfluential here
           ys = map (\ x -> [holEq (extLeftH x) $ extRightH x]) xs
           ps = [makeNamed jn $ RecDef (Just fixrecS) (mkVName jn)
            Nothing (concat ys)]
        in ps
      NotCont -> let
           jj = joinNames (map extAxName xs)
           jn = mkVName jj
           jt1 = headTailsType (map extAxType xs)
           (jta, jts) = headTailsMT jt1
           jt = mkFunType jta (typTuple NotCont jts)
           jl = Const jn $ hideNN jt
           n = length xs
           rs = map extRightH xs
           ls = map extFunTerm xs
           yys = map (\ x -> destCase x (const jn)) rs
           yyys = reassemble yys
           zs = map (\ (p, ts) -> (p, Tuplex
                        (map (renFuns (newFCons (Const jn noType) ls)) ts)
                        NotCont)) $ Map.toList yyys
           os = map (\ (x, m) -> mkNewDef x jj n m jt1) $ number xs
           ps = makeNamed jj (makeRecDef jj jl zs) : os
        in ps
    [] -> []
  
  mkNewDef :: Named Sentence -> String ->
                      Int -> Int -> [(Typ, Typ)] -> Named Sentence
  mkNewDef s z x y t = let      -- x is the max
         a = NotCont
         zy = uncurry mkFunType (t !! (y - 1))
    in mapNamed ( \ sen -> case sen of
      ConstDef (IsaEq lh rh) -> case (lh, extFBody rh) of
        (Const nam _, (_, w : ws)) ->
           ConstDef $ IsaEq (Const nam $ hideNN zy) $
              termMAbs a (w : ws) $ termMAppl a (tupleSelector x y
                    (termSAppl a (Const (mkVName z) noType) w) a) ws
        _ -> error "Hs2HOLCFaux.mkNewDef1"
      _ -> error "Hs2HOLCFaux.mkNewDef2") s
  
  makeRecDef :: String -> Term -> [(Term, Term)] -> Sentence
  makeRecDef n t ls =
   RecDef Nothing (mkVName n)
    Nothing (map (\ (a, b) -> holEq (App t a NotCont) b) ls)
  
  reassemble :: [[(Term, Term)]] -> Map.Map Term [Term]
  reassemble ls = foldr
   (\ (ft, sd) ms ->
       Map.insert ft (sd : Map.findWithDefault [] ft ms) ms)
     Map.empty (concat ls)
  
  newFCons :: Term -> [Term] -> Term -> Maybe Term
  newFCons t ls k = case k of
   App n w NotCont -> case elPos ls n of
     Nothing -> Nothing
     Just i ->
        Just $ tupleSelector (length ls) i (IsaSign.App t w NotCont) NotCont
   _ -> Nothing
  
  {- ------------------------ TYPES -----------------------------------------
  ---------------------- tuples, lifting --------------------------------- -}
  
  typTuple :: Continuity -> [Typ] -> Typ
  typTuple c ts = case ts of
    [] -> noTypeT
    [a] -> a
    a : as ->
        (if isCont c then mkContProduct else prodType) a (typTuple c as)
  
  -- ------------------ function types -----------------------------------
  
  headTailsType :: [Typ] -> [(Typ, Typ)]
  headTailsType ls = if chkTHead ls then map splitFunT ls
                     else error "Hs2HOLCFaux.headTailsType"
  
  splitFunT :: Typ -> (Typ, Typ)
  splitFunT x = case x of
    IsaSign.Type "=>" _ [i, b] -> (i, b)
    _ -> error "Hs2HOLCF, headTail"
  
  {- checks that all types in the list are equivalent in the first argument
  and that all variables occur in that argument -}
  chkTHead :: [IsaType] -> Bool
  chkTHead ls = case ls of
     IsaSign.Type "=>" _ [x, n] : IsaSign.Type "=>" s [y, m] : ns ->
        (typEq x y && mkTVarMap id x == mkTVarMap id n) &&
         chkTHead (IsaSign.Type "=>" s [y, m] : ns)
     [IsaSign.Type "=>" _ [x, n]] -> mkTVarMap id x == mkTVarMap id n
     _ -> False
  
  -- -------------------- equivalence of types modulo variables name ------
  
  typSim :: Typ -> Typ -> Bool
  typSim t1 t2 = case (t1, t2) of
    (IsaSign.Type _ _ ls1, IsaSign.Type _ _ ls2) ->
                     typeId t1 == typeId t2 && typLSim ls1 ls2
    (TFree _ _, TFree _ _) -> True
    _ -> False
  
  typLSim :: [Typ] -> [Typ] -> Bool
  typLSim ls1 ls2 = case (ls1, ls2) of
       ([], []) -> True
       (a : as, b : bs) -> typSim a b && typLSim as bs
       _ -> False
  
  typEq :: Typ -> Typ -> Bool     -- make some distinction for case noType?
  typEq t1 t2 = t1 == noTypeT || t2 == noTypeT || case (t1, t2) of
    (IsaSign.Type _ _ ls1, IsaSign.Type _ _ ls2) ->
        typeId t1 == typeId t2
            && typeSort t1 == typeSort t2 && typLEq ls1 ls2
    (TFree _ _, TFree _ _) -> typeSort t1 == typeSort t2
    _ -> False
  
  typLEq :: [Typ] -> [Typ] -> Bool
  typLEq ls1 ls2 = case (ls1, ls2) of
       ([], []) -> True
       (a : as, b : bs) -> typEq a b && typLEq as bs
       _ -> False
  
  -- --------------------- type renaming -----------------------------------
  
  applyTyRen :: Int -> Typ -> Typ
  applyTyRen n t = case t of
        TFree x s -> TFree (x ++ "XX" ++ show n) s
        TVar _ _ -> t
        IsaSign.Type a b cs -> IsaSign.Type a b $ map (applyTyRen n) cs
  
  -- ----------------------- type var maps ---------------------------------
  
  headTailsMT :: [(Typ, Typ)] -> (Typ, [Typ])
  headTailsMT ls = let
           ks = [(mkTVarMap (applyTyRen 0) i, (i, b)) | (i, b) <- ls]
        in case ks of
           [] -> error "Hs2HOLCFaux, headTailsType"
           (f, (x, _)) : _ -> let
                     zs = [(renMap f g, y) | (g, (_, y)) <- ks]
                     zz = [applyTVM h y | (h, y) <- zs]
                     w = applyTyRen 0 x
                 in (w, zz)
  
  -- !!!!!!!!!!!!
  renMap :: Map.Map Typ Typ -> Map.Map Typ Typ -> Map.Map Typ Typ
  renMap f g = if Map.size f == Map.size g then
       Map.fromList [(fst $ Map.elemAt n g, snd $ Map.elemAt n f)
                                       | n <- [0 .. (Map.size f - 1)]]
    else error "HsHOLCFaux, renMap"
  -- !!!!!!!!!!!!
  
  mkTVarMap :: (Typ -> Typ) -> Typ -> Map.Map Typ Typ
  mkTVarMap f t = case t of
     Type _ _ xs -> Map.unions [mkTVarMap f y | y <- xs]
     _ -> Map.singleton t (f t)
  
  applyTVM :: Map.Map Typ Typ -> Typ -> Typ
  applyTVM f t = case t of
      IsaSign.Type n s vs -> IsaSign.Type n s (map (applyTVM f) vs)
      _ -> fromMaybe t $ Map.lookup t f
  
  {- ---------------------- 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
  addSort cs n s = do
       as <- Map.lookup n (Map.fromList cs)
       return $ TFree n $ remove_duplicates $ s ++ as
  
  -- replaces in t variables 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
      IsaSign.Type n s vs -> IsaSign.Type n s (map (typeVarsRep f ls) vs)
      IsaSign.TFree n s -> fromMaybe t $ f ls n s
      _ -> t
  
  {- replace type var in t with type x; used in instantiation; assumed
  that t has just one variable -}
  replaceTyVar :: IsaType -> IsaType -> IsaType
  replaceTyVar x t = if x == noTypeT then t else case t of
      IsaSign.Type n s vs -> IsaSign.Type n s (map (replaceTyVar x) vs)
      IsaSign.TFree _ _ -> x
      IsaSign.TVar _ _ -> x
  