HolLight2Isabelle.hs revision e9458b1a7a19a63aa4c179f9ab20f4d50681c168
{-# 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 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 () ()
IsabelleMorphism () () () where
sourceLogic _ = HolLight
sourceSublogic _ = Top
targetLogic _ = Isabelle
mapSublogic _ _ = Just ()
map_theory HolLight2Isabelle = mapTheory
map_sentence HolLight2Isabelle = mapSentence
-- mapping sentences
mapSentence :: Sign -> Sentence -> Result IsaSign.Sentence
mapSentence _ s = return $ mapHolSen s
mapHolSen :: Sentence -> IsaSign.Sentence
mapHolSen (Sentence t _) = IsaSign.Sentence {
IsaSign.isSimp = False
, IsaSign.isRefuteAux = False
, IsaSign.metaTerm =
IsaSign.Term $ translateTerm t (allVars t)
, IsaSign.thmProof = Nothing
}
tp2DTyp :: HolType -> IsaSign.DTyp
tp2DTyp tp = IsaSign.Hide {
IsaSign.typ = tp2Typ tp,
IsaSign.arit = Nothing
}
constMap :: Map.Map String IsaSign.VName
constMap = Map.fromList [("+", IsaConsts.plusV)
, ("-", IsaConsts.minusV)
, ("*", IsaConsts.timesV)
, ("!", IsaConsts.mkVName IsaConsts.allS)
, ("?", IsaConsts.mkVName IsaConsts.exS)
, ("?!", IsaConsts.mkVName IsaConsts.ex1S)
, ("=", IsaConsts.eqV)
, ("<=>", IsaConsts.eqV)
, ("/\\", IsaConsts.conjV)
, ("\\/", IsaConsts.disjV)
, ("==>", IsaConsts.implV)
, ("~", IsaConsts.notV)
, ("T", IsaConsts.mkVName IsaConsts.cTrue)
, ("F", IsaConsts.mkVName IsaConsts.cFalse)
]
notIgnore :: [String]
notIgnore = ["+", "-", "*"]
ignore :: [String]
ignore = map fst (Map.toList constMap) \\ notIgnore
transConstS :: String -> HolType -> IsaSign.VName
transConstS s t = case (Map.lookup s constMap, elem s notIgnore) of
(Just v, False) -> v
(_, _) -> IsaConsts.mkVName $ typedName s t
typedName :: String -> HolType -> String
typedName s _t = transConstStringT bs s -- ++ "_" ++ (show $ pp_print_type t)
unpack_gabs t vs = case unpack_gabs' t vs [] of
Just (q, vars, tm) ->
let (pat, res) = case tm of
Comb (Comb (Const "GEQ" _ _)
(Comb (Var "f" _ _) pat1)) res1 -> (pat1, res1)
_ -> error "unpack_gabs failed"
in (q, vars, translateTerm pat vs, translateTerm res vs)
Nothing -> error "unpack_gabs' failed"
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 _ [] t = t
makeForAll q (v : vs) t = IsaSign.App q
(IsaSign.Abs v
(makeForAll q vs t)
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)])
in if b then makeForAll q vars (IsaSign.App q t1
else t1
_ -> error "handleGabs failed"
mkAbs :: Term -> [String] -> IsaSign.Term
mkAbs t vs = let name = freeName vs in
(IsaSign.Free (IsaConsts.mkVName name))
(IsaSign.App (translateTerm t (name : vs))
(IsaSign.Free (IsaConsts.mkVName name))
mkQuantifier :: Term -> [String] -> IsaSign.Term
mkQuantifier t vs = let name = freeName vs in
(IsaSign.Free (IsaConsts.mkVName name))
(IsaSign.App (translateTerm t (name : vs))
(IsaSign.Free (IsaConsts.mkVName name))
(IsaSign.Free (IsaConsts.mkVName name))
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)
else IsaSign.App (translateTerm c1 vs)
(if isQuantifier t
then mkQuantifier t vs
else mkAbs t vs)
translateTerm (Comb tm1 tm2) vs = IsaSign.App (translateTerm tm1 vs)
(translateTerm tm2 vs)
translateTerm (Abs tm1 tm2) vs = IsaSign.Abs (translateTerm tm1 vs)
(translateTerm tm2 vs)
-- 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.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 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}