967e5f3c25249c779575864692935627004d3f9eChristian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder{- |

650bafe7709533bc5f82bb9daf8fa06f431cd963Christian MaederModule : $Header$

97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : translating from HolLight to Isabelle

967e5f3c25249c779575864692935627004d3f9eChristian MaederCopyright : (c) Jonathan von Schroeder and M. Codescu, DFKI 2010

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederLicense : GPLv2 or higher, see LICENSE.txt

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

89054b2b95a3f92e78324dc852f3d34704e2ca49Christian MaederMaintainer : jonathan.von_schroeder@dfki.de

f3a94a197960e548ecd6520bb768cb0d547457bbChristian MaederStability : provisional

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaederPortability : non-portable (imports Logic.Logic)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maeder-}

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maedermodule Comorphisms.HolLight2Isabelle where

967e5f3c25249c779575864692935627004d3f9eChristian Maeder

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Logic.Comorphism

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Logic.Logic

650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder

9cb4aa4ea6685489a38f9b609f5dbe5d37f25bc7Christian Maederimport qualified Isabelle.IsaSign as IsaSign

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maederimport Isabelle.Logic_Isabelle

ac19f8695aa1b2d2d1cd1319da2530edd8f46a96Christian Maederimport Isabelle.IsaConsts as IsaConsts

8b9fda012e5ee53b7b2320c0638896a0ff6e99f3Christian Maederimport Isabelle.Translate

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport Common.Result

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport Common.AS_Annotation

9744c7d9fa61d255d5e73beec7edc3499522e9e2Till Mossakowski

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maederimport qualified Data.Map as Map

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maederimport Data.List ((\\))

fd896e2068ad7e50aed66ac18c3720ea7ff2619fChristian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport HolLight.Sign

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport HolLight.Sentence

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maederimport HolLight.Term

967e5f3c25249c779575864692935627004d3f9eChristian Maederimport HolLight.Logic_HolLight

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maederimport HolLight.Sublogic

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederimport HolLight.Helper

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maederdata HolLight2Isabelle = HolLight2Isabelle deriving Show

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maederinstance Language HolLight2Isabelle

7a879b08ae0ca30006f9be887a73212b07f10204Christian Maeder

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maederinstance Comorphism HolLight2Isabelle

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder HolLight

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder HolLightSL -- sublogic

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder () -- basic_spec

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Sentence -- sentence

6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder () -- symb_items

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder () -- symb_map_items

62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian Maeder Sign -- sign

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder HolLightMorphism -- morphism

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder () -- symbol

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder () -- raw_symbol

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder () -- proof_tree

d5c415f6373274fed04d83b9322891f3b82e9c26Christian Maeder Isabelle () () IsaSign.Sentence () ()

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.Sign

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsabelleMorphism () () () where

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder sourceLogic _ = HolLight

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder sourceSublogic _ = Top

5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder targetLogic _ = Isabelle

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder mapSublogic _ _ = Just ()

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder map_theory HolLight2Isabelle = mapTheory

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder map_sentence HolLight2Isabelle = mapSentence

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder-- mapping sentences

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapSentence :: Sign -> Sentence -> Result IsaSign.Sentence

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapSentence _ s = return $ mapHolSen s

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapHolSen :: Sentence -> IsaSign.Sentence

717686b54b9650402e2ebfbaadf433eab8ba5171Christian MaedermapHolSen (Sentence t _) = IsaSign.Sentence {

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder IsaSign.isSimp = False

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder , IsaSign.isRefuteAux = False

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder , IsaSign.metaTerm =

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder IsaSign.Term $ translateTerm t (allVars t)

717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder , IsaSign.thmProof = Nothing

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder }

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maedertp2DTyp :: HolType -> IsaSign.DTyp

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maedertp2DTyp tp = IsaSign.Hide {

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder IsaSign.typ = tp2Typ tp,

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder IsaSign.kon = IsaSign.TCon,

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.arit = Nothing

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder }

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederconstMap :: Map.Map String IsaSign.VName

e7ce154edb906685b3fa7f6c0a764e18a4658068Christian MaederconstMap = Map.fromList [("+", IsaConsts.plusV)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , ("-", IsaConsts.minusV)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder , ("*", IsaConsts.timesV)

c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder , ("!", IsaSign.mkVName IsaConsts.allS)

c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder , ("?", IsaSign.mkVName IsaConsts.exS)

c66a930944d9e4d64a8f0f38c748fdad0831ff87Christian Maeder , ("?!", IsaSign.mkVName IsaConsts.ex1S)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder , ("=", IsaConsts.eqV)

0a8ea95bcf0e3f84fed0b725c049ec2a956a4a28Christian Maeder , ("<=>", IsaConsts.eqV)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , ("/\\", IsaConsts.conjV)

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian Maeder , ("\\/", IsaConsts.disjV)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , ("==>", IsaConsts.implV)

967e5f3c25249c779575864692935627004d3f9eChristian Maeder , ("~", IsaConsts.notV)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder , ("T", IsaSign.mkVName IsaConsts.cTrue)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder , ("F", IsaSign.mkVName IsaConsts.cFalse)

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder ]

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedernotIgnore :: [String]

20e16bdd7481741d0b6b14f952aea42ee7a65efbChristian MaedernotIgnore = ["+", "-", "*"]

e1839fb37a3a2ccd457464cb0dcc5efd466dbe22Christian Maeder

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederignore :: [String]

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maederignore = (map fst $ Map.toList constMap) \\ notIgnore

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertransConstS :: String -> HolType -> IsaSign.VName

a578ec30cded5e396a7ce9a3b469e8cd3a88246aChristian MaedertransConstS s t = case (Map.lookup s constMap, elem s notIgnore) of

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maeder (Just v, False) -> v

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (_, _) -> IsaSign.mkVName $ typedName s t

650bafe7709533bc5f82bb9daf8fa06f431cd963Christian Maeder

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian MaedertypedName :: String -> HolType -> String

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedertypedName s _t = transConstStringT bs $ s -- ++ "_" ++ (show $ pp_print_type t)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maederunpack_gabs :: Term -> [String] -> (IsaSign.Term, [IsaSign.Term], IsaSign.Term, IsaSign.Term)

a89e661aad28f1b39f4fc9f9f9a4d46074234123Christian Maederunpack_gabs t vs = case unpack_gabs' t vs [] of

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder Just (q, vars, tm) ->

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski let (pat, res) = case tm of

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder Comb (Comb (Const "GEQ" _ _)

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder (Comb (Var "f" _ _) pat1)) res1 -> (pat1, res1)

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder _ -> error "unpack_gabs failed"

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder in (q, vars, translateTerm pat vs, translateTerm res vs)

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder Nothing -> error "unpack_gabs' failed"

42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski

842eedc62639561781b6c33533d1949693ef6cc5Christian Maederunpack_gabs' :: Term -> [String] -> [IsaSign.Term] -> Maybe (IsaSign.Term, [IsaSign.Term], Term)

842eedc62639561781b6c33533d1949693ef6cc5Christian Maederunpack_gabs' (Comb c@(Const "!" _ _) (Abs v@(Var _ _ _) tm)) vs vars =

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder case unpack_gabs' tm vs ((translateTerm v vs) : vars) of

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder Just r -> Just r

842eedc62639561781b6c33533d1949693ef6cc5Christian Maeder Nothing -> Just (translateTerm c vs, (translateTerm v vs) : vars, tm)

842eedc62639561781b6c33533d1949693ef6cc5Christian Maederunpack_gabs' _ _ _ = Nothing

bfa9e03532243ceb487f0384d0f6a447f1ce7670Till Mossakowski

967e5f3c25249c779575864692935627004d3f9eChristian MaedermakeForAll :: IsaSign.Term -> [IsaSign.Term] -> IsaSign.Term -> IsaSign.Term

967e5f3c25249c779575864692935627004d3f9eChristian MaedermakeForAll _ [] t = t

967e5f3c25249c779575864692935627004d3f9eChristian MaedermakeForAll q (v : vs) t = IsaSign.App q

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (IsaSign.Abs v

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (makeForAll q vs t)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.NotCont)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.NotCont

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederhandleGabs :: Bool -> Term -> [String] -> IsaSign.Term

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederhandleGabs b t vs = case t of

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (Comb (Const "GABS" _ _) (Abs (Var "f" _ _) tm)) ->

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let (q, vars, pat, res) = unpack_gabs tm vs in

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let n = IsaSign.Free $ IsaSign.mkVName (freeName ((varNames vars)++vs)) in

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder let t1 = IsaSign.Abs n

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (IsaSign.Case n [(pat, res)])

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.NotCont

967e5f3c25249c779575864692935627004d3f9eChristian Maeder in if b then makeForAll q vars (IsaSign.App q t1

967e5f3c25249c779575864692935627004d3f9eChristian Maeder IsaSign.NotCont)

7221c71b38c871ce66eee4537cb681d468308dfbChristian Maeder else t1

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder _ -> error "handleGabs failed"

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkAbs :: Term -> [String] -> IsaSign.Term

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkAbs t vs = let name = freeName vs in

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder IsaSign.Abs

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Free (IsaSign.mkVName name))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.App (translateTerm t (name:vs))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Free (IsaSign.mkVName name))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder IsaSign.NotCont)

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder IsaSign.NotCont

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkQuantifier :: Term -> [String] -> IsaSign.Term

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedermkQuantifier t vs = let name = freeName vs in

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder IsaSign.Abs

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Free (IsaSign.mkVName name))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.App (translateTerm t (name:vs))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Abs

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Free (IsaSign.mkVName name))

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder (IsaSign.Free (IsaSign.mkVName name))

ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian Maeder IsaSign.NotCont)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder IsaSign.NotCont)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder IsaSign.NotCont

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederisAppT :: HolType -> Bool

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederisAppT (TyApp _ _) = True

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederisAppT _ = False

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederisQuantifier :: Term -> Bool

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederisQuantifier (Const c _ _) = elem c ["!", "?", "?!"]

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaederisQuantifier _ = False

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedervarNames :: [IsaSign.Term] -> [String]

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedervarNames [] = []

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedervarNames ((IsaSign.Free s):vs) = (IsaSign.orig s):(varNames vs)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedervarNames (_:vs) = varNames vs

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederallVars :: Term -> [String]

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederallVars (Comb a b) = (allVars a) ++ (allVars b)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederallVars (Abs a b) = (allVars a) ++ (allVars b)

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaederallVars (Const _ _ _) = []

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaederallVars (Var s _ _) = [s]

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian Maeder

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedertranslateTerm :: Term -> [String] -> IsaSign.Term

7221c71b38c871ce66eee4537cb681d468308dfbChristian MaedertranslateTerm (Comb (Comb (Const "," _ _) a) b) vs = IsaSign.Tuplex [translateTerm a vs, translateTerm b vs] IsaSign.NotCont

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedertranslateTerm (Var s tp _) _ = IsaSign.Free $ (transConstS s tp)

deb7bff126ec547bd812d0c8683ad6e785a45abbChristian MaedertranslateTerm (Const s tp _) _ = IsaSign.Const (transConstS s tp) $ tp2DTyp tp

967e5f3c25249c779575864692935627004d3f9eChristian MaedertranslateTerm (Comb (Const "!" _ _) t@(Comb (Const "GABS" _ _) _)) vs = handleGabs True t vs

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertranslateTerm t@(Comb (Const "GABS" _ _) (Abs (Var "f" _ _) _)) vs = handleGabs False t vs

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian MaedertranslateTerm (Comb (Comb (Comb (Const "COND" _ _) i) t) e) vs = IsaSign.If

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (translateTerm i vs)

83814002b4922114cbe7e9ba728472a0bf44aac5Christian Maeder (translateTerm t vs)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder (translateTerm e vs)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder IsaSign.NotCont

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian MaedertranslateTerm (Comb c1@(Const c tp _) t) vs = if (isAbs t) || ((isAppT tp) && not (isQuantifier t) && not (isQuantifier c1) && c /= "@")

97ee7048e63953c5617342ce38c30cbcb35cc0beChristian Maeder then IsaSign.App

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (translateTerm c1 vs)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder (translateTerm t vs)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder IsaSign.NotCont

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder else IsaSign.App (translateTerm c1 vs)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (if isQuantifier t

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder then (mkQuantifier t vs)

dedabc954aa15f6ad0764472a9434dc6dafe3db2Christian Maeder else (mkAbs t vs))

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder IsaSign.NotCont

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedertranslateTerm (Comb tm1 tm2) vs = IsaSign.App (translateTerm tm1 vs)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (translateTerm tm2 vs)

4fb19f237193a3bd6778f8aee3b6dd8da5856665Christian Maeder IsaSign.NotCont

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian MaedertranslateTerm (Abs tm1 tm2) vs = IsaSign.Abs (translateTerm tm1 vs)

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder (translateTerm tm2 vs)

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder IsaSign.NotCont

07b72edb610ee53b4832d132e96b0a3d8423f8ebChristian Maeder

-- mapping theories

mapTheory :: (Sign, [Named Sentence]) ->

Result (IsaSign.Sign, [Named IsaSign.Sentence])

mapTheory (sig, n_sens) = let

sig' = mapSign sig

n_sens' = map mapNamedSen n_sens

in return (sig', n_sens')

bs :: IsaSign.BaseSig

bs = IsaSign.MainHC_thy

mapSign :: Sign -> IsaSign.Sign

mapSign (Sign t o) = IsaSign.emptySign {

IsaSign.baseSig = IsaSign.MainHC_thy,

IsaSign.constTab = mapOps o,

IsaSign.tsig = mapTypes t

}

mapOps :: Map.Map String HolType -> IsaSign.ConstTab

mapOps f = Map.fromList

$ map (\ (x, y) -> (transConstS x y, tp2Typ y))

$ Map.toList (foldl (\ m i -> Map.delete i m) f ignore)

tp2Typ :: HolType -> IsaSign.Typ

tp2Typ (TyVar ('\'':s')) =IsaSign.TFree ('\'':(transTypeStringT bs s')) holType

tp2Typ (TyVar s) = IsaSign.Type (transTypeStringT bs s) holType []

tp2Typ (TyApp s tps) = case tps of

[a1, a2] | s == "fun" -> mkFunType (tp2Typ a1) (tp2Typ a2)

[] | s == "bool" -> boolType

_ -> IsaSign.Type (transTypeStringT bs s) holType $ map tp2Typ tps

arity2tp :: Int -> [(IsaSign.IsaClass, [(IsaSign.Typ, IsaSign.Sort)])]

arity2tp i = [(isaTerm, map (\ k -> (IsaSign.TFree ("'a" ++ show (k)) [], [isaTerm]))

[1 .. i])]

mapTypes :: Map.Map String Int -> IsaSign.TypeSig

mapTypes tps = IsaSign.emptyTypeSig {

IsaSign.arities = Map.fromList $ map extractTypeName

$ Map.toList $ foldr Map.delete tps

["bool", "fun", "prod"] }

where

extractTypeName (s, arity) = (transTypeStringT bs s, arity2tp arity)

mapNamedSen :: Named Sentence -> Named IsaSign.Sentence

mapNamedSen n_sen = let

sen = sentence n_sen

trans = mapHolSen sen

in

n_sen {sentence = trans}