{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/HolLight2Isabelle.hs
Description :  translating from HolLight to Isabelle
Copyright   :  (c) Jonathan von Schroeder and M. Codescu, DFKI 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

-}

module Comorphisms.HolLight2Isabelle where

import Logic.Comorphism
import Logic.Logic

import qualified Isabelle.IsaSign as IsaSign
import Isabelle.Logic_Isabelle
import Isabelle.IsaConsts as IsaConsts
import Isabelle.Translate

import Common.Result
import Common.AS_Annotation

import qualified Data.Map as Map
import Data.List ((\\))

import HolLight.Sign
import HolLight.Sentence
import HolLight.Term
import HolLight.Logic_HolLight
import HolLight.Sublogic
import HolLight.Helper

data HolLight2Isabelle = HolLight2Isabelle deriving Int -> HolLight2Isabelle -> ShowS
[HolLight2Isabelle] -> ShowS
HolLight2Isabelle -> String
(Int -> HolLight2Isabelle -> ShowS)
-> (HolLight2Isabelle -> String)
-> ([HolLight2Isabelle] -> ShowS)
-> Show HolLight2Isabelle
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HolLight2Isabelle] -> ShowS
$cshowList :: [HolLight2Isabelle] -> ShowS
show :: HolLight2Isabelle -> String
$cshow :: HolLight2Isabelle -> String
showsPrec :: Int -> HolLight2Isabelle -> ShowS
$cshowsPrec :: Int -> HolLight2Isabelle -> ShowS
Show

instance Language HolLight2Isabelle

instance Comorphism HolLight2Isabelle
          HolLight
          HolLightSL                -- sublogic
          ()                        -- basic_spec
          Sentence                  -- sentence
          ()                        -- symb_items
          ()                        -- symb_map_items
          Sign                      -- sign
          HolLightMorphism          -- morphism
          ()                        -- symbol
          ()                        -- raw_symbol
          ()                        -- proof_tree
          Isabelle () () IsaSign.Sentence () ()
          IsaSign.Sign
          IsabelleMorphism () () () where
   sourceLogic :: HolLight2Isabelle -> HolLight
sourceLogic _ = HolLight
HolLight
   sourceSublogic :: HolLight2Isabelle -> HolLightSL
sourceSublogic _ = HolLightSL
Top
   targetLogic :: HolLight2Isabelle -> Isabelle
targetLogic _ = Isabelle
Isabelle
   mapSublogic :: HolLight2Isabelle -> HolLightSL -> Maybe ()
mapSublogic _ _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
   map_theory :: HolLight2Isabelle
-> (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
map_theory HolLight2Isabelle = (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
mapTheory
   map_sentence :: HolLight2Isabelle -> Sign -> Sentence -> Result Sentence
map_sentence HolLight2Isabelle = Sign -> Sentence -> Result Sentence
mapSentence

-- mapping sentences

mapSentence :: Sign -> Sentence -> Result IsaSign.Sentence
mapSentence :: Sign -> Sentence -> Result Sentence
mapSentence _ s :: Sentence
s = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence) -> Sentence -> Result Sentence
forall a b. (a -> b) -> a -> b
$ Sentence -> Sentence
mapHolSen Sentence
s

mapHolSen :: Sentence -> IsaSign.Sentence
mapHolSen :: Sentence -> Sentence
mapHolSen (Sentence t :: Term
t _) = Sentence :: Bool -> Bool -> MetaTerm -> Maybe IsaProof -> Sentence
IsaSign.Sentence {
                                  isSimp :: Bool
IsaSign.isSimp = Bool
False
                                 , isRefuteAux :: Bool
IsaSign.isRefuteAux = Bool
False
                                 , metaTerm :: MetaTerm
IsaSign.metaTerm =
                                    Term -> MetaTerm
IsaSign.Term (Term -> MetaTerm) -> Term -> MetaTerm
forall a b. (a -> b) -> a -> b
$ Term -> [String] -> Term
translateTerm Term
t (Term -> [String]
allVars Term
t)
                                 , thmProof :: Maybe IsaProof
IsaSign.thmProof = Maybe IsaProof
forall a. Maybe a
Nothing
                                      }

tp2DTyp :: HolType -> IsaSign.DTyp
tp2DTyp :: HolType -> DTyp
tp2DTyp tp :: HolType
tp = Hide :: Typ -> TAttr -> Maybe Int -> DTyp
IsaSign.Hide {
                typ :: Typ
IsaSign.typ = HolType -> Typ
tp2Typ HolType
tp,
                kon :: TAttr
IsaSign.kon = TAttr
IsaSign.TCon,
                arit :: Maybe Int
IsaSign.arit = Maybe Int
forall a. Maybe a
Nothing
              }

constMap :: Map.Map String IsaSign.VName
constMap :: Map String VName
constMap = [(String, VName)] -> Map String VName
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList [("+", VName
IsaConsts.plusV)
                        , ("-", VName
IsaConsts.minusV)
                        , ("*", VName
IsaConsts.timesV)
                        , ("!", String -> VName
IsaConsts.mkVName String
IsaConsts.allS)
                        , ("?", String -> VName
IsaConsts.mkVName String
IsaConsts.exS)
                        , ("?!", String -> VName
IsaConsts.mkVName String
IsaConsts.ex1S)
                        , ("=", VName
IsaConsts.eqV)
                        , ("<=>", VName
IsaConsts.eqV)
                        , ("/\\", VName
IsaConsts.conjV)
                        , ("\\/", VName
IsaConsts.disjV)
                        , ("==>", VName
IsaConsts.implV)
                        , ("~", VName
IsaConsts.notV)
                        , ("T", String -> VName
IsaConsts.mkVName String
IsaConsts.cTrue)
                        , ("F", String -> VName
IsaConsts.mkVName String
IsaConsts.cFalse)
                        ]

notIgnore :: [String]
notIgnore :: [String]
notIgnore = ["+", "-", "*"]

ignore :: [String]
ignore :: [String]
ignore = ((String, VName) -> String) -> [(String, VName)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, VName) -> String
forall a b. (a, b) -> a
fst (Map String VName -> [(String, VName)]
forall k a. Map k a -> [(k, a)]
Map.toList Map String VName
constMap) [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
notIgnore

transConstS :: String -> HolType -> IsaSign.VName
transConstS :: String -> HolType -> VName
transConstS s :: String
s t :: HolType
t = case (String -> Map String VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup String
s Map String VName
constMap, String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
s [String]
notIgnore) of
                   (Just v :: VName
v, False) -> VName
v
                   (_, _) -> String -> VName
IsaConsts.mkVName (String -> VName) -> String -> VName
forall a b. (a -> b) -> a -> b
$ String -> HolType -> String
typedName String
s HolType
t

typedName :: String -> HolType -> String
typedName :: String -> HolType -> String
typedName s :: String
s _t :: HolType
_t = BaseSig -> ShowS
transConstStringT BaseSig
bs String
s -- ++ "_" ++ (show $ pp_print_type t)

unpack_gabs :: Term -> [String] -> (IsaSign.Term, [IsaSign.Term], IsaSign.Term, IsaSign.Term)
unpack_gabs :: Term -> [String] -> (Term, [Term], Term, Term)
unpack_gabs t :: Term
t vs :: [String]
vs = case Term -> [String] -> [Term] -> Maybe (Term, [Term], Term)
unpack_gabs' Term
t [String]
vs [] of
                    Just (q :: Term
q, vars :: [Term]
vars, tm :: Term
tm) ->
                     let (pat :: Term
pat, res :: Term
res) = case Term
tm of
                                       Comb (Comb (Const "GEQ" _ _)
                                        (Comb (Var "f" _ _) pat1 :: Term
pat1)) res1 :: Term
res1 -> (Term
pat1, Term
res1)
                                       _ -> String -> (Term, Term)
forall a. HasCallStack => String -> a
error "unpack_gabs failed"
                     in (Term
q, [Term]
vars, Term -> [String] -> Term
translateTerm Term
pat [String]
vs, Term -> [String] -> Term
translateTerm Term
res [String]
vs)
                    Nothing -> String -> (Term, [Term], Term, Term)
forall a. HasCallStack => String -> a
error "unpack_gabs' failed"

unpack_gabs' :: Term -> [String] -> [IsaSign.Term] -> Maybe (IsaSign.Term, [IsaSign.Term], Term)
unpack_gabs' :: Term -> [String] -> [Term] -> Maybe (Term, [Term], Term)
unpack_gabs' (Comb c :: Term
c@(Const "!" _ _) (Abs v :: Term
v@(Var {}) tm :: Term
tm)) vs :: [String]
vs vars :: [Term]
vars =
  case Term -> [String] -> [Term] -> Maybe (Term, [Term], Term)
unpack_gabs' Term
tm [String]
vs (Term -> [String] -> Term
translateTerm Term
v [String]
vs Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vars) of
    Just r :: (Term, [Term], Term)
r -> (Term, [Term], Term) -> Maybe (Term, [Term], Term)
forall a. a -> Maybe a
Just (Term, [Term], Term)
r
    Nothing -> (Term, [Term], Term) -> Maybe (Term, [Term], Term)
forall a. a -> Maybe a
Just (Term -> [String] -> Term
translateTerm Term
c [String]
vs, Term -> [String] -> Term
translateTerm Term
v [String]
vs Term -> [Term] -> [Term]
forall a. a -> [a] -> [a]
: [Term]
vars, Term
tm)
unpack_gabs' _ _ _ = Maybe (Term, [Term], Term)
forall a. Maybe a
Nothing

makeForAll :: IsaSign.Term -> [IsaSign.Term] -> IsaSign.Term -> IsaSign.Term
makeForAll :: Term -> [Term] -> Term -> Term
makeForAll _ [] t :: Term
t = Term
t
makeForAll q :: Term
q (v :: Term
v : vs :: [Term]
vs) t :: Term
t = Term -> Term -> Continuity -> Term
IsaSign.App Term
q
                         (Term -> Term -> Continuity -> Term
IsaSign.Abs Term
v
                           (Term -> [Term] -> Term -> Term
makeForAll Term
q [Term]
vs Term
t)
                           Continuity
IsaSign.NotCont)
                         Continuity
IsaSign.NotCont

handleGabs :: Bool -> Term -> [String] -> IsaSign.Term
handleGabs :: Bool -> Term -> [String] -> Term
handleGabs b :: Bool
b t :: Term
t vs :: [String]
vs = case Term
t of
 (Comb (Const "GABS" _ _) (Abs (Var "f" _ _) tm :: Term
tm)) ->
   let (q :: Term
q, vars :: [Term]
vars, pat :: Term
pat, res :: Term
res) = Term -> [String] -> (Term, [Term], Term, Term)
unpack_gabs Term
tm [String]
vs in
   let n :: Term
n = VName -> Term
IsaSign.Free (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ String -> VName
IsaConsts.mkVName ([String] -> String
freeName ([Term] -> [String]
varNames [Term]
vars [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
vs)) in
   let t1 :: Term
t1 = Term -> Term -> Continuity -> Term
IsaSign.Abs Term
n
             (Term -> [(Term, Term)] -> Term
IsaSign.Case Term
n [(Term
pat, Term
res)])
             Continuity
IsaSign.NotCont
   in if Bool
b then Term -> [Term] -> Term -> Term
makeForAll Term
q [Term]
vars (Term -> Term -> Continuity -> Term
IsaSign.App Term
q Term
t1
                                    Continuity
IsaSign.NotCont)
      else Term
t1
 _ -> String -> Term
forall a. HasCallStack => String -> a
error "handleGabs failed"

mkAbs :: Term -> [String] -> IsaSign.Term
mkAbs :: Term -> [String] -> Term
mkAbs t :: Term
t vs :: [String]
vs = let name :: String
name = [String] -> String
freeName [String]
vs in
             Term -> Term -> Continuity -> Term
IsaSign.Abs
              (VName -> Term
IsaSign.Free (String -> VName
IsaConsts.mkVName String
name))
              (Term -> Term -> Continuity -> Term
IsaSign.App (Term -> [String] -> Term
translateTerm Term
t (String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
vs))
                (VName -> Term
IsaSign.Free (String -> VName
IsaConsts.mkVName String
name))
                Continuity
IsaSign.NotCont)
              Continuity
IsaSign.NotCont

mkQuantifier :: Term -> [String] -> IsaSign.Term
mkQuantifier :: Term -> [String] -> Term
mkQuantifier t :: Term
t vs :: [String]
vs = let name :: String
name = [String] -> String
freeName [String]
vs in
                    Term -> Term -> Continuity -> Term
IsaSign.Abs
                     (VName -> Term
IsaSign.Free (String -> VName
IsaConsts.mkVName String
name))
                     (Term -> Term -> Continuity -> Term
IsaSign.App (Term -> [String] -> Term
translateTerm Term
t (String
name String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [String]
vs))
                       (Term -> Term -> Continuity -> Term
IsaSign.Abs
                        (VName -> Term
IsaSign.Free (String -> VName
IsaConsts.mkVName String
name))
                        (VName -> Term
IsaSign.Free (String -> VName
IsaConsts.mkVName String
name))
                        Continuity
IsaSign.NotCont)
                       Continuity
IsaSign.NotCont)
                     Continuity
IsaSign.NotCont

isAppT :: HolType -> Bool
isAppT :: HolType -> Bool
isAppT (TyApp _ _) = Bool
True
isAppT _ = Bool
False

isQuantifier :: Term -> Bool
isQuantifier :: Term -> Bool
isQuantifier (Const c :: String
c _ _) = String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem String
c ["!", "?", "?!"]
isQuantifier _ = Bool
False

varNames :: [IsaSign.Term] -> [String]
varNames :: [Term] -> [String]
varNames [] = []
varNames (IsaSign.Free s :: VName
s : vs :: [Term]
vs) = VName -> String
IsaSign.orig VName
s String -> [String] -> [String]
forall a. a -> [a] -> [a]
: [Term] -> [String]
varNames [Term]
vs
varNames (_ : vs :: [Term]
vs) = [Term] -> [String]
varNames [Term]
vs

allVars :: Term -> [String]
allVars :: Term -> [String]
allVars (Comb a :: Term
a b :: Term
b) = Term -> [String]
allVars Term
a [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Term -> [String]
allVars Term
b
allVars (Abs a :: Term
a b :: Term
b) = Term -> [String]
allVars Term
a [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ Term -> [String]
allVars Term
b
allVars (Const {}) = []
allVars (Var s :: String
s _ _) = [String
s]

translateTerm :: Term -> [String] -> IsaSign.Term
translateTerm :: Term -> [String] -> Term
translateTerm (Comb (Comb (Const "," _ _) a :: Term
a) b :: Term
b) vs :: [String]
vs =
  [Term] -> Continuity -> Term
IsaSign.Tuplex [Term -> [String] -> Term
translateTerm Term
a [String]
vs, Term -> [String] -> Term
translateTerm Term
b [String]
vs] Continuity
IsaSign.NotCont
translateTerm (Var s :: String
s tp :: HolType
tp _) _ = VName -> Term
IsaSign.Free (VName -> Term) -> VName -> Term
forall a b. (a -> b) -> a -> b
$ String -> HolType -> VName
transConstS String
s HolType
tp
translateTerm (Const s :: String
s tp :: HolType
tp _) _ = VName -> DTyp -> Term
IsaSign.Const (String -> HolType -> VName
transConstS String
s HolType
tp) (DTyp -> Term) -> DTyp -> Term
forall a b. (a -> b) -> a -> b
$ HolType -> DTyp
tp2DTyp HolType
tp
translateTerm (Comb (Const "!" _ _) t :: Term
t@(Comb (Const "GABS" _ _) _)) vs :: [String]
vs =
  Bool -> Term -> [String] -> Term
handleGabs Bool
True Term
t [String]
vs
translateTerm t :: Term
t@(Comb (Const "GABS" _ _) (Abs (Var "f" _ _) _)) vs :: [String]
vs =
  Bool -> Term -> [String] -> Term
handleGabs Bool
False Term
t [String]
vs
translateTerm (Comb (Comb (Comb (Const "COND" _ _) i :: Term
i) t :: Term
t) e :: Term
e) vs :: [String]
vs =
  Term -> Term -> Term -> Continuity -> Term
IsaSign.If (Term -> [String] -> Term
translateTerm Term
i [String]
vs) (Term -> [String] -> Term
translateTerm Term
t [String]
vs)
             (Term -> [String] -> Term
translateTerm Term
e [String]
vs) Continuity
IsaSign.NotCont
translateTerm (Comb c1 :: Term
c1@(Const c :: String
c tp :: HolType
tp _) t :: Term
t) vs :: [String]
vs = if Term -> Bool
isAbs Term
t Bool -> Bool -> Bool
|| (HolType -> Bool
isAppT HolType
tp Bool -> Bool -> Bool
&&
  Bool -> Bool
not (Term -> Bool
isQuantifier Term
t) Bool -> Bool -> Bool
&& Bool -> Bool
not (Term -> Bool
isQuantifier Term
c1) Bool -> Bool -> Bool
&& String
c String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= "@")
                                           then Term -> Term -> Continuity -> Term
IsaSign.App
                                                (Term -> [String] -> Term
translateTerm Term
c1 [String]
vs)
                                                (Term -> [String] -> Term
translateTerm Term
t [String]
vs)
                                                Continuity
IsaSign.NotCont
                                          else Term -> Term -> Continuity -> Term
IsaSign.App (Term -> [String] -> Term
translateTerm Term
c1 [String]
vs)
                                                (if Term -> Bool
isQuantifier Term
t
                                                 then Term -> [String] -> Term
mkQuantifier Term
t [String]
vs
                                                 else Term -> [String] -> Term
mkAbs Term
t [String]
vs)
                                                Continuity
IsaSign.NotCont
translateTerm (Comb tm1 :: Term
tm1 tm2 :: Term
tm2) vs :: [String]
vs = Term -> Term -> Continuity -> Term
IsaSign.App (Term -> [String] -> Term
translateTerm Term
tm1 [String]
vs)
                                (Term -> [String] -> Term
translateTerm Term
tm2 [String]
vs)
                                Continuity
IsaSign.NotCont
translateTerm (Abs tm1 :: Term
tm1 tm2 :: Term
tm2) vs :: [String]
vs = Term -> Term -> Continuity -> Term
IsaSign.Abs (Term -> [String] -> Term
translateTerm Term
tm1 [String]
vs)
                                          (Term -> [String] -> Term
translateTerm Term
tm2 [String]
vs)
                                          Continuity
IsaSign.NotCont

-- mapping theories

mapTheory :: (Sign, [Named Sentence]) ->
             Result (IsaSign.Sign, [Named IsaSign.Sentence])
mapTheory :: (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
mapTheory (sig :: Sign
sig, n_sens :: [Named Sentence]
n_sens) = let
  sig' :: Sign
sig' = Sign -> Sign
mapSign Sign
sig
  n_sens' :: [Named Sentence]
n_sens' = (Named Sentence -> Named Sentence)
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map Named Sentence -> Named Sentence
mapNamedSen [Named Sentence]
n_sens
                          in (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig', [Named Sentence]
n_sens')
bs :: IsaSign.BaseSig
bs :: BaseSig
bs = BaseSig
IsaSign.MainHC_thy

mapSign :: Sign -> IsaSign.Sign
mapSign :: Sign -> Sign
mapSign (Sign t :: Map String Int
t o :: Map String HolType
o) = Sign
IsaSign.emptySign {
                          baseSig :: BaseSig
IsaSign.baseSig = BaseSig
IsaSign.MainHC_thy,
                          constTab :: ConstTab
IsaSign.constTab = Map String HolType -> ConstTab
mapOps Map String HolType
o,
                          tsig :: TypeSig
IsaSign.tsig = Map String Int -> TypeSig
mapTypes Map String Int
t
                         }

mapOps :: Map.Map String HolType -> IsaSign.ConstTab
mapOps :: Map String HolType -> ConstTab
mapOps f :: Map String HolType
f = [(VName, Typ)] -> ConstTab
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
             ([(VName, Typ)] -> ConstTab) -> [(VName, Typ)] -> ConstTab
forall a b. (a -> b) -> a -> b
$ ((String, HolType) -> (VName, Typ))
-> [(String, HolType)] -> [(VName, Typ)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (x :: String
x, y :: HolType
y) -> (String -> HolType -> VName
transConstS String
x HolType
y, HolType -> Typ
tp2Typ HolType
y))
             ([(String, HolType)] -> [(VName, Typ)])
-> [(String, HolType)] -> [(VName, Typ)]
forall a b. (a -> b) -> a -> b
$ Map String HolType -> [(String, HolType)]
forall k a. Map k a -> [(k, a)]
Map.toList ((Map String HolType -> String -> Map String HolType)
-> Map String HolType -> [String] -> Map String HolType
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((String -> Map String HolType -> Map String HolType)
-> Map String HolType -> String -> Map String HolType
forall a b c. (a -> b -> c) -> b -> a -> c
flip String -> Map String HolType -> Map String HolType
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete) Map String HolType
f [String]
ignore)

tp2Typ :: HolType -> IsaSign.Typ
tp2Typ :: HolType -> Typ
tp2Typ (TyVar ('\'' : s' :: String
s')) = String -> Sort -> Typ
IsaSign.TFree ('\'' Char -> ShowS
forall a. a -> [a] -> [a]
: BaseSig -> ShowS
transTypeStringT BaseSig
bs String
s')
                              Sort
holType
tp2Typ (TyVar s :: String
s) = String -> Sort -> [Typ] -> Typ
IsaSign.Type (BaseSig -> ShowS
transTypeStringT BaseSig
bs String
s) Sort
holType []
tp2Typ (TyApp s :: String
s tps :: [HolType]
tps) = case [HolType]
tps of
  [a1 :: HolType
a1, a2 :: HolType
a2] | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "fun" -> Typ -> Typ -> Typ
mkFunType (HolType -> Typ
tp2Typ HolType
a1) (HolType -> Typ
tp2Typ HolType
a2)
  [] | String
s String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== "bool" -> Typ
boolType
  _ -> String -> Sort -> [Typ] -> Typ
IsaSign.Type (BaseSig -> ShowS
transTypeStringT BaseSig
bs String
s) Sort
holType ([Typ] -> Typ) -> [Typ] -> Typ
forall a b. (a -> b) -> a -> b
$ (HolType -> Typ) -> [HolType] -> [Typ]
forall a b. (a -> b) -> [a] -> [b]
map HolType -> Typ
tp2Typ [HolType]
tps

arity2tp :: Int -> [(IsaSign.IsaClass, [(IsaSign.Typ, IsaSign.Sort)])]
arity2tp :: Int -> [(IsaClass, [(Typ, Sort)])]
arity2tp i :: Int
i = [(IsaClass
isaTerm, (Int -> (Typ, Sort)) -> [Int] -> [(Typ, Sort)]
forall a b. (a -> b) -> [a] -> [b]
map (\ k :: Int
k -> (String -> Sort -> Typ
IsaSign.TFree ("'a" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k) [],
  [IsaClass
isaTerm])) [1 .. Int
i])]

mapTypes :: Map.Map String Int -> IsaSign.TypeSig
mapTypes :: Map String Int -> TypeSig
mapTypes tps :: Map String Int
tps = TypeSig
IsaSign.emptyTypeSig {
                    arities :: Arities
IsaSign.arities = [(String, [(IsaClass, [(Typ, Sort)])])] -> Arities
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(String, [(IsaClass, [(Typ, Sort)])])] -> Arities)
-> [(String, [(IsaClass, [(Typ, Sort)])])] -> Arities
forall a b. (a -> b) -> a -> b
$ ((String, Int) -> (String, [(IsaClass, [(Typ, Sort)])]))
-> [(String, Int)] -> [(String, [(IsaClass, [(Typ, Sort)])])]
forall a b. (a -> b) -> [a] -> [b]
map (String, Int) -> (String, [(IsaClass, [(Typ, Sort)])])
extractTypeName
                  ([(String, Int)] -> [(String, [(IsaClass, [(Typ, Sort)])])])
-> [(String, Int)] -> [(String, [(IsaClass, [(Typ, Sort)])])]
forall a b. (a -> b) -> a -> b
$ Map String Int -> [(String, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map String Int -> [(String, Int)])
-> Map String Int -> [(String, Int)]
forall a b. (a -> b) -> a -> b
$ (String -> Map String Int -> Map String Int)
-> Map String Int -> [String] -> Map String Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr String -> Map String Int -> Map String Int
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Map String Int
tps
                       ["bool", "fun", "prod"] }
 where
    extractTypeName :: (String, Int) -> (String, [(IsaClass, [(Typ, Sort)])])
extractTypeName (s :: String
s, arity :: Int
arity) = (BaseSig -> ShowS
transTypeStringT BaseSig
bs String
s, Int -> [(IsaClass, [(Typ, Sort)])]
arity2tp Int
arity)

mapNamedSen :: Named Sentence -> Named IsaSign.Sentence
mapNamedSen :: Named Sentence -> Named Sentence
mapNamedSen n_sen :: Named Sentence
n_sen = let
 sen :: Sentence
sen = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
n_sen
 trans :: Sentence
trans = Sentence -> Sentence
mapHolSen Sentence
sen
                    in
 Named Sentence
n_sen {sentence :: Sentence
sentence = Sentence
trans}