module HaskHOL.Core.Kernel.Terms
(
HOLTerm
, HOLTermView(..)
, ConstTag
, HOLTermEnv
, alphaOrder
, aConv
, isVar
, isConst
, isAbs
, isComb
, mkVar
, mkAbs
, mkComb
, destVar
, destConst
, destComb
, destAbs
, frees
, catFrees
, freesIn
, varFreeIn
, typeVarsInTerm
, typeVarsInTerms
, varSubst
, Inst
, inst
, instFull
, instConst
, instConstFull
, tmEq
, isEq
, primMkEq
, destEq
, variant
, variants
, newPrimConst
, typeOpVarsInTerm
, typeOpVarsInTerms
, isTyAbs
, isTyComb
, mkTyAbs
, mkTyComb
, destTyAbs
, destTyComb
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel.Prims
import HaskHOL.Core.Kernel.Types
alphaOrder :: HOLTerm -> HOLTerm -> Ordering
alphaOrder = orda []
where orda :: HOLTermEnv -> HOLTerm -> HOLTerm -> Ordering
orda env tm1 tm2
| tm1 == tm2 && all (uncurry (==)) env = EQ
| otherwise =
case (tm1, tm2) of
(VarIn{}, VarIn{}) -> ordav env tm1 tm2
(ConstIn{}, ConstIn{}) -> tm1 `aorder` tm2
(CombIn s1 t1, CombIn s2 t2) ->
case orda env s1 s2 of
EQ -> orda env t1 t2
res -> res
(AbsIn x1@(VarIn _ ty1) t1, AbsIn x2@(VarIn _ ty2) t2) ->
case tyAlphaOrder ty1 ty2 of
EQ -> orda ((x1, x2):env) t1 t2
res -> res
(AbsIn{}, AbsIn{}) -> compare tm1 tm2
(TyAbsIn tv1@(TyVarIn True _) tb1,
TyAbsIn tv2@(TyVarIn True _) tb2) ->
orda env tb1 $ inst [(tv2, tv1)] tb2
(TyAbsIn{}, TyAbsIn{}) -> compare tm1 tm2
(TyCombIn t1 ty1, TyCombIn t2 ty2) ->
case orda env t1 t2 of
EQ -> tyAlphaOrder ty1 ty2
res -> res
(ConstIn{}, _) -> LT
(_, ConstIn{}) -> GT
(VarIn{}, _) -> LT
(_, VarIn{}) -> GT
(CombIn{}, _) -> LT
(_, CombIn{}) -> GT
(AbsIn{}, _) -> LT
(_, AbsIn{}) -> GT
(TyAbsIn{}, _) -> LT
(_, TyAbsIn{}) -> GT
ordav :: HOLTermEnv -> HOLTerm -> HOLTerm -> Ordering
ordav [] x1 x2 = x1 `aorder` x2
ordav ((t1, t2):oenv) x1 x2
| x1 == t1 = if x2 == x2 then EQ else LT
| otherwise = if x2 == t2 then GT else ordav oenv x1 x2
aorder :: HOLTerm -> HOLTerm -> Ordering
aorder tm1@(VarIn s1 ty1) tm2@(VarIn s2 ty2)
| s1 == s2 = tyAlphaOrder ty1 ty2
| otherwise = compare tm1 tm2
aorder tm1@(ConstIn s1 ty1 d1) tm2@(ConstIn s2 ty2 d2)
| s1 == s2 && d1 == d2 = tyAlphaOrder ty1 ty2
| otherwise = compare tm1 tm2
aorder tm1 tm2 = compare tm1 tm2
aConv :: HOLTerm -> HOLTerm -> Bool
aConv tm1 tm2 = alphaOrder tm1 tm2 == EQ
isVar :: HOLTerm -> Bool
isVar VarIn{} = True
isVar _ = False
isConst :: HOLTerm -> Bool
isConst ConstIn{} = True
isConst _ = False
isAbs :: HOLTerm -> Bool
isAbs AbsIn{} = True
isAbs _ = False
isComb :: HOLTerm -> Bool
isComb CombIn{} = True
isComb _ = False
mkVar :: String -> HOLType -> HOLTerm
mkVar = VarIn
mkAbs :: HOLTerm -> HOLTerm -> Either String HOLTerm
mkAbs bv@VarIn{} bod = Right $ AbsIn bv bod
mkAbs _ _ = Left "mkAbs"
mkComb :: HOLTerm -> HOLTerm -> Either String HOLTerm
mkComb f a =
case typeOf f of
(TyAppIn (TyPrim "fun" _) (ty:_)) ->
if typeOf a `tyAConv` ty then Right $ CombIn f a
else Left "mkComb: argument type mismatch."
_ -> Left "mkComb: argument not of function type."
destVar :: HOLTerm -> Maybe (String, HOLType)
destVar (VarIn s ty) = Just (s, ty)
destVar _ = Nothing
destConst :: HOLTerm -> Maybe (String, HOLType)
destConst (ConstIn s ty _) = Just (s, ty)
destConst _ = Nothing
destComb :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
destComb (CombIn f x) = Just (f, x)
destComb _ = Nothing
destAbs :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
destAbs (AbsIn v b) = Just (v, b)
destAbs _ = Nothing
frees :: HOLTerm -> [HOLTerm]
frees tm@VarIn{} = [tm]
frees ConstIn{} = []
frees (AbsIn bv bod) = frees bod \\ [bv]
frees (CombIn s t) = frees s `union` frees t
frees (TyAbsIn _ tm) = frees tm
frees (TyCombIn tm _) = frees tm
catFrees :: [HOLTerm] -> [HOLTerm]
catFrees = foldr (union . frees) []
freesIn :: [HOLTerm] -> HOLTerm -> Bool
freesIn acc tm@VarIn{} = tm `elem` acc
freesIn _ ConstIn{} = True
freesIn acc (AbsIn bv bod) = freesIn (bv:acc) bod
freesIn acc (CombIn s t) = freesIn acc s && freesIn acc t
freesIn acc (TyAbsIn _ t) = freesIn acc t
freesIn acc (TyCombIn t _) = freesIn acc t
varFreeIn :: HOLTerm -> HOLTerm -> Bool
varFreeIn v (AbsIn bv bod) = v /= bv && varFreeIn v bod
varFreeIn v (CombIn s t) = varFreeIn v s || varFreeIn v t
varFreeIn v (TyAbsIn _ t) = varFreeIn v t
varFreeIn v (TyCombIn t _) = varFreeIn v t
varFreeIn v tm = v == tm
typeVarsInTerm :: HOLTerm -> [HOLType]
typeVarsInTerm (VarIn _ ty) = tyVars ty
typeVarsInTerm (ConstIn _ ty _) = tyVars ty
typeVarsInTerm (CombIn s t) = typeVarsInTerm s `union` typeVarsInTerm t
typeVarsInTerm (AbsIn bv t) = typeVarsInTerm bv `union` typeVarsInTerm t
typeVarsInTerm (TyAbsIn tv tm) = typeVarsInTerm tm \\ [tv]
typeVarsInTerm (TyCombIn tm ty) = typeVarsInTerm tm `union` tyVars ty
typeVarsInTerms :: [HOLTerm] -> [HOLType]
typeVarsInTerms =
foldr (\ tm tvs -> typeVarsInTerm tm `union` tvs) []
varSubst :: HOLTermEnv -> HOLTerm -> HOLTerm
varSubst [] term = term
varSubst theta term =
varSubstRec (filter validPair theta) term
where validPair :: (HOLTerm, HOLTerm) -> Bool
validPair (VarIn _ ty, t) = ty `tyAConv` typeOf t
validPair _ = False
varSubstRec :: HOLTermEnv -> HOLTerm -> HOLTerm
varSubstRec env tm@VarIn{} = lookupd tm env tm
varSubstRec _ tm@ConstIn{} = tm
varSubstRec env (CombIn s t) =
CombIn (varSubstRec env s) $ varSubstRec env t
varSubstRec env tm@(AbsIn v s) =
let env' = filter (\ (x, _) -> x /= v) env in
if null env' then tm
else let s' = varSubstRec env' s in
if s' == s then tm
else if any (\ (x, t) -> varFreeIn v t &&
varFreeIn x s) env'
then let v' = variant [s'] v in
AbsIn v' $ varSubstRec ((v, v'):env') s
else AbsIn v $ varSubstRec env' s
varSubstRec env (TyAbsIn tv t) = TyAbsIn tv $ varSubstRec env t
varSubstRec env (TyCombIn t ty) = TyCombIn (varSubstRec env t) ty
class TypeSubst a b => Inst a b where
instTyAbs :: HOLTermEnv -> [(a, b)] -> HOLTerm -> Either HOLTerm HOLTerm
instance Inst HOLType HOLType where
instTyAbs env tyenv tm@(TyAbsIn tv t) =
let tyenv' = filter (\ (x, _) -> x /= tv) tyenv in
if null tyenv' then Right tm
else if any (\ (x, r) -> tv `elem` tyVars r &&
x `elem` typeVarsInTerm t) tyenv'
then let tvt = typeVarsInTerm t
tvpatts = map fst tyenv'
tvrepls = catTyVars . mapMaybe (`lookup` tyenv') $
tvt `intersect` tvpatts
tv' = variantTyVar ((tvt \\ tvpatts) `union` tvrepls) tv in
liftM (TyAbsIn tv') $ instRec env ((tv, tv'):tyenv') t
else liftM (TyAbsIn tv) $ instRec env tyenv' t
instTyAbs _ _ tm = Right tm
instance Inst TypeOp TypeOp where
instTyAbs env tyenv (TyAbsIn tv t) =
liftM (TyAbsIn tv) $ instRec env tyenv t
instTyAbs _ _ tm = Right tm
instance Inst TypeOp HOLType where
instTyAbs env tyenv (TyAbsIn tv t) =
if any (\ (x, ty) -> tv `elem` tyVars ty &&
x `elem` typeOpVarsInTerm t) tyenv
then let tvbs = typeOpVarsInTerm t
tvpatts = map fst tyenv
tvrepls = catTyVars . mapMaybe (`lookup` tyenv) $
tvbs `intersect` tvpatts
tv' = variantTyVar tvrepls tv in
liftM (TyAbsIn tv') . instRec env tyenv $ inst [(tv, tv')] t
else liftM (TyAbsIn tv) $ instRec env tyenv t
instTyAbs _ _ tm = Right tm
inst :: Inst a b => [(a, b)] -> HOLTerm -> HOLTerm
inst [] tm = tm
inst theta tm =
case instRec [] theta tm of
Right res -> res
Left _ -> tm
instRec :: Inst a b => HOLTermEnv -> [(a, b)] -> HOLTerm ->
Either HOLTerm HOLTerm
instRec env tyenv tm@(VarIn n ty) =
let ty' = typeSubst tyenv ty
tm' = VarIn n ty' in
if lookupd tm' env tm == tm then Right tm'
else Left tm'
instRec _ tyenv (ConstIn c ty tag) =
let ty' = typeSubst tyenv ty in
Right $ ConstIn c ty' tag
instRec env tyenv (CombIn f x) =
return CombIn <*> instRec env tyenv f <*> instRec env tyenv x
instRec env tyenv (AbsIn y@(VarIn _ ty) t) =
do y' <- instRec [] tyenv y
case instRec ((y', y):env) tyenv t of
Right t' -> Right $ AbsIn y' t'
e@(Left w') ->
if w' /= y' then e
else do ifrees <- mapM (instRec [] tyenv) $ frees t
case variant ifrees y' of
VarIn x _ ->
let z = VarIn x ty in
instRec env tyenv . AbsIn z $ varSubst [(y, z)] t
_ -> e
instRec env tyenv tm@TyAbsIn{} = instTyAbs env tyenv tm
instRec env tyenv (TyCombIn tm ty) =
do tm' <- instRec env tyenv tm
return . TyCombIn tm' $ typeSubst tyenv ty
instRec _ _ _ = Left undefined
instFull :: SubstTrip -> HOLTerm -> HOLTerm
instFull (tyenv, tyOps, opOps) = inst opOps . inst tyOps . inst tyenv
instConst :: TypeSubst a b => HOLTerm -> [(a, b)] -> Maybe HOLTerm
instConst (ConstIn name uty tag) tyenv =
Just $ ConstIn name (typeSubst tyenv uty) tag
instConst _ _ = Nothing
instConstFull :: HOLTerm -> SubstTrip -> Maybe HOLTerm
instConstFull (ConstIn name uty tag) tyenv =
Just $ ConstIn name (typeSubstFull tyenv uty) tag
instConstFull _ _ = Nothing
tmEq :: HOLType -> HOLTerm
tmEq ty =
ConstIn "=" (TyAppIn tyOpFun [ty, TyAppIn tyOpFun [ty, tyBool]]) Prim
isEq :: HOLTerm -> Bool
isEq (CombIn (CombIn (ConstIn "=" _ Prim) _) _) = True
isEq _ = False
primMkEq :: HOLTerm -> HOLTerm -> Either String HOLTerm
primMkEq l r
| typeOf l `tyAConv` typeOf r =
Right $ CombIn (CombIn (tmEq $ typeOf l) l) r
| otherwise = Left "primMkEq"
destEq :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
destEq (CombIn (CombIn (ConstIn "=" _ Prim) l) r) =
Just (l, r)
destEq _ = Nothing
variant :: [HOLTerm] -> HOLTerm -> HOLTerm
variant avoid v@(VarIn s ty)
| any (varFreeIn v) avoid = variant avoid $ VarIn (s++"'") ty
| otherwise = v
variant _ tm = tm
variants :: [HOLTerm] -> [HOLTerm] -> [HOLTerm]
variants _ [] = []
variants avoid (v:vs) =
let vh = variant avoid v in
vh : variants (vh:avoid) vs
newPrimConst :: String -> HOLType -> HOLTerm
newPrimConst name ty = ConstIn name ty Prim
typeOpVarsInTerm :: HOLTerm -> [TypeOp]
typeOpVarsInTerm (VarIn _ ty) = typeOpVars ty
typeOpVarsInTerm (ConstIn _ ty _) = typeOpVars ty
typeOpVarsInTerm (CombIn s t) = typeOpVarsInTerm s `union` typeOpVarsInTerm t
typeOpVarsInTerm (AbsIn bv t) = typeOpVarsInTerm bv `union` typeOpVarsInTerm t
typeOpVarsInTerm (TyAbsIn _ tm) = typeOpVarsInTerm tm
typeOpVarsInTerm (TyCombIn tm ty) = typeOpVarsInTerm tm `union` typeOpVars ty
typeOpVarsInTerms :: [HOLTerm] -> [TypeOp]
typeOpVarsInTerms =
foldr (\ tm topvs -> typeOpVarsInTerm tm `union` topvs) []
isTyAbs :: HOLTerm -> Bool
isTyAbs TyAbsIn{} = True
isTyAbs _ = False
isTyComb :: HOLTerm -> Bool
isTyComb TyCombIn{} = True
isTyComb _ = False
mkTyAbs :: HOLType -> HOLTerm -> Either String HOLTerm
mkTyAbs tv@(TyVarIn True s) bod
| not . any (\ x -> tv `elem` tyVars (typeOf x)) $ frees bod =
Right $ TyAbsIn tv bod
| otherwise =
Left $ "mkTyAbs: tyvar " ++ s ++ " occurs in type of free variable in body term."
mkTyAbs _ _ = Left "mkTyAbs: first argument not a small type variable."
mkTyComb :: HOLTerm -> HOLType -> Either String HOLTerm
mkTyComb tm ty
| isSmall ty =
case typeOf tm of
UTypeIn{} -> Right $ TyCombIn tm ty
_ -> Left "mkTyComb: term must have universal type."
| otherwise =
Left "mkTyComb: type argument not small."
destTyAbs :: HOLTerm -> Maybe (HOLType, HOLTerm)
destTyAbs (TyAbsIn tv bod) = Just (tv, bod)
destTyAbs _ = Nothing
destTyComb :: HOLTerm -> Maybe (HOLTerm, HOLType)
destTyComb (TyCombIn tm ty) = Just (tm, ty)
destTyComb _ = Nothing