6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann{- |

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannModule : ./Comorphisms/HolLight2Isabelle.hs

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannDescription : translating from HolLight to Isabelle

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannCopyright : (c) Jonathan von Schroeder and M. Codescu, DFKI 2010

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannLicense : GPLv2 or higher, see LICENSE.txt

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannMaintainer : jonathan.von_schroeder@dfki.de

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannStability : provisional

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannPortability : non-portable (imports Logic.Logic)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-}

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannmodule Comorphisms.HolLight2Isabelle where

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Logic.Comorphism

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Logic.Logic

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Isabelle.IsaSign as IsaSign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Isabelle.Logic_Isabelle

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Isabelle.IsaConsts as IsaConsts

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Isabelle.Translate

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.Result

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Common.AS_Annotation

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport qualified Data.Map as Map

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport Data.List ((\\))

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Sign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Sentence

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Term

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Logic_HolLight

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Sublogic

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannimport HolLight.Helper

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanndata HolLight2Isabelle = HolLight2Isabelle deriving Show

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Language HolLight2Isabelle

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanninstance Comorphism HolLight2Isabelle

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann HolLight

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann HolLightSL -- sublogic

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- basic_spec

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Sentence -- sentence

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- symb_items

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- symb_map_items

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Sign -- sign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann HolLightMorphism -- morphism

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- symbol

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- raw_symbol

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann () -- proof_tree

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Isabelle () () IsaSign.Sentence () ()

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.Sign

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsabelleMorphism () () () where

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceLogic _ = HolLight

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann sourceSublogic _ = Top

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann targetLogic _ = Isabelle

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann mapSublogic _ _ = Just ()

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_theory HolLight2Isabelle = mapTheory

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann map_sentence HolLight2Isabelle = mapSentence

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann-- mapping sentences

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannmapSentence :: Sign -> Sentence -> Result IsaSign.Sentence

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannmapSentence _ s = return $ mapHolSen s

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannmapHolSen :: Sentence -> IsaSign.Sentence

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannmapHolSen (Sentence t _) = IsaSign.Sentence {

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.isSimp = False

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , IsaSign.isRefuteAux = False

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , IsaSign.metaTerm =

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.Term $ translateTerm t (allVars t)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , IsaSign.thmProof = Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann }

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanntp2DTyp :: HolType -> IsaSign.DTyp

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmanntp2DTyp tp = IsaSign.Hide {

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.typ = tp2Typ tp,

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.kon = IsaSign.TCon,

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann IsaSign.arit = Nothing

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann }

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannconstMap :: Map.Map String IsaSign.VName

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannconstMap = Map.fromList [("+", IsaConsts.plusV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("-", IsaConsts.minusV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("*", IsaConsts.timesV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("!", IsaConsts.mkVName IsaConsts.allS)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("?", IsaConsts.mkVName IsaConsts.exS)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("?!", IsaConsts.mkVName IsaConsts.ex1S)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("=", IsaConsts.eqV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("<=>", IsaConsts.eqV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("/\\", IsaConsts.conjV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("\\/", IsaConsts.disjV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("==>", IsaConsts.implV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("~", IsaConsts.notV)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("T", IsaConsts.mkVName IsaConsts.cTrue)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann , ("F", IsaConsts.mkVName IsaConsts.cFalse)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann ]

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnotIgnore :: [String]

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmannnotIgnore = ["+", "-", "*"]

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannignore :: [String]

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannignore = map fst (Map.toList constMap) \\ notIgnore

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntransConstS :: String -> HolType -> IsaSign.VName

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntransConstS s t = case (Map.lookup s constMap, elem s notIgnore) of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (Just v, False) -> v

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (_, _) -> IsaConsts.mkVName $ typedName s t

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntypedName :: String -> HolType -> String

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel HausmanntypedName s _t = transConstStringT bs s -- ++ "_" ++ (show $ pp_print_type t)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannunpack_gabs :: Term -> [String] -> (IsaSign.Term, [IsaSign.Term], IsaSign.Term, IsaSign.Term)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmannunpack_gabs t vs = case unpack_gabs' t vs [] of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Just (q, vars, tm) ->

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann let (pat, res) = case tm of

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann Comb (Comb (Const "GEQ" _ _)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann (Comb (Var "f" _ _) pat1)) res1 -> (pat1, res1)

6a4fa2d53294f484fa8788a75656eff4ad1fd703Daniel Hausmann _ -> error "unpack_gabs failed"

in (q, vars, translateTerm pat vs, translateTerm res vs)

Nothing -> error "unpack_gabs' failed"

unpack_gabs' :: Term -> [String] -> [IsaSign.Term] -> Maybe (IsaSign.Term, [IsaSign.Term], Term)

unpack_gabs' (Comb c@(Const "!" _ _) (Abs v@(Var {}) tm)) vs vars =

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

Just r -> Just r

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

unpack_gabs' _ _ _ = Nothing

makeForAll :: IsaSign.Term -> [IsaSign.Term] -> IsaSign.Term -> IsaSign.Term

makeForAll _ [] t = t

makeForAll q (v : vs) t = IsaSign.App q

(IsaSign.Abs v

(makeForAll q vs t)

IsaSign.NotCont)

IsaSign.NotCont

handleGabs :: Bool -> Term -> [String] -> IsaSign.Term

handleGabs b t vs = case t of

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

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

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

let t1 = IsaSign.Abs n

(IsaSign.Case n [(pat, res)])

IsaSign.NotCont

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

IsaSign.NotCont)

else t1

_ -> error "handleGabs failed"

mkAbs :: Term -> [String] -> IsaSign.Term

mkAbs t vs = let name = freeName vs in

IsaSign.Abs

(IsaSign.Free (IsaConsts.mkVName name))

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

(IsaSign.Free (IsaConsts.mkVName name))

IsaSign.NotCont)

IsaSign.NotCont

mkQuantifier :: Term -> [String] -> IsaSign.Term

mkQuantifier t vs = let name = freeName vs in

IsaSign.Abs

(IsaSign.Free (IsaConsts.mkVName name))

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

(IsaSign.Abs

(IsaSign.Free (IsaConsts.mkVName name))

(IsaSign.Free (IsaConsts.mkVName name))

IsaSign.NotCont)

IsaSign.NotCont)

IsaSign.NotCont

isAppT :: HolType -> Bool

isAppT (TyApp _ _) = True

isAppT _ = False

isQuantifier :: Term -> Bool

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

isQuantifier _ = False

varNames :: [IsaSign.Term] -> [String]

varNames [] = []

varNames (IsaSign.Free s : vs) = IsaSign.orig s : varNames vs

varNames (_ : vs) = varNames vs

allVars :: Term -> [String]

allVars (Comb a b) = allVars a ++ allVars b

allVars (Abs a b) = allVars a ++ allVars b

allVars (Const {}) = []

allVars (Var s _ _) = [s]

translateTerm :: Term -> [String] -> IsaSign.Term

translateTerm (Comb (Comb (Const "," _ _) a) b) vs =

IsaSign.Tuplex [translateTerm a vs, translateTerm b vs] IsaSign.NotCont

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

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

translateTerm (Comb (Const "!" _ _) t@(Comb (Const "GABS" _ _) _)) vs =

handleGabs True t vs

translateTerm t@(Comb (Const "GABS" _ _) (Abs (Var "f" _ _) _)) vs =

handleGabs False t vs

translateTerm (Comb (Comb (Comb (Const "COND" _ _) i) t) e) vs =

IsaSign.If (translateTerm i vs) (translateTerm t vs)

(translateTerm e vs) IsaSign.NotCont

translateTerm (Comb c1@(Const c tp _) t) vs = if isAbs t || (isAppT tp &&

not (isQuantifier t) && not (isQuantifier c1) && c /= "@")

then IsaSign.App

(translateTerm c1 vs)

(translateTerm t vs)

IsaSign.NotCont

else IsaSign.App (translateTerm c1 vs)

(if isQuantifier t

then mkQuantifier t vs

else mkAbs t vs)

IsaSign.NotCont

translateTerm (Comb tm1 tm2) vs = IsaSign.App (translateTerm tm1 vs)

(translateTerm tm2 vs)

IsaSign.NotCont

translateTerm (Abs tm1 tm2) vs = IsaSign.Abs (translateTerm tm1 vs)

(translateTerm tm2 vs)

IsaSign.NotCont

-- 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 (flip Map.delete) 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}