module HOL.Term
where
import Data.Maybe (isJust)
import qualified Data.Map as Map
import System.IO.Unsafe (unsafePerformIO)
import System.Mem.StableName (makeStableName)
import qualified HOL.Const as Const
import HOL.Data
import qualified HOL.TermData as TermData
import qualified HOL.Type as Type
import qualified HOL.TypeVar as TypeVar
import HOL.Util
import qualified HOL.Var as Var
dest :: Term -> TermData
dest (Term d _ _ _ _ _) = d
mk :: TermData -> Term
mk d =
Term d i sz ty tvs fvs
where
i = unsafePerformIO (makeStableName $! d)
sz = TermData.size d
ty = TermData.typeOf d
tvs = TypeVar.vars d
fvs = Var.free d
mkConst :: Const -> Type -> Term
mkConst c = mk . TermData.mkConst c
destConst :: Term -> Maybe (Const,Type)
destConst = TermData.destConst . dest
isConst :: Term -> Bool
isConst = isJust . destConst
destGivenConst :: Const -> Term -> Maybe Type
destGivenConst c = TermData.destGivenConst c . dest
isGivenConst :: Const -> Term -> Bool
isGivenConst c = isJust . destGivenConst c
mkVar :: Var -> Term
mkVar = mk . TermData.mkVar
destVar :: Term -> Maybe Var
destVar = TermData.destVar . dest
isVar :: Term -> Bool
isVar = isJust . destVar
eqVar :: Var -> Term -> Bool
eqVar v = TermData.eqVar v . dest
mkApp :: Term -> Term -> Maybe Term
mkApp f x = fmap mk $ TermData.mkApp f x
mkAppUnsafe :: Term -> Term -> Term
mkAppUnsafe = mkUnsafe2 "HOL.Term.mkApp" mkApp
destApp :: Term -> Maybe (Term,Term)
destApp = TermData.destApp . dest
isApp :: Term -> Bool
isApp = isJust . destApp
rator :: Term -> Maybe Term
rator = fmap fst . destApp
rand :: Term -> Maybe Term
rand = fmap snd . destApp
land :: Term -> Maybe Term
land tm = do
f <- rator tm
rand f
listMkApp :: Term -> [Term] -> Maybe Term
listMkApp tm [] = Just tm
listMkApp f (x : xs) = do
fx <- mkApp f x
listMkApp fx xs
listMkAppUnsafe :: Term -> [Term] -> Term
listMkAppUnsafe = mkUnsafe2 "HOL.Term.listMkApp" listMkApp
stripApp :: Term -> (Term,[Term])
stripApp =
go []
where
go xs tm =
case destApp tm of
Nothing -> (tm,xs)
Just (f,x) -> go (x : xs) f
mkAbs :: Var -> Term -> Term
mkAbs v b = mk $ TermData.mkAbs v b
destAbs :: Term -> Maybe (Var,Term)
destAbs = TermData.destAbs . dest
isAbs :: Term -> Bool
isAbs = isJust . destAbs
listMkAbs :: [Var] -> Term -> Term
listMkAbs [] tm = tm
listMkAbs (v : vs) b = mkAbs v $ listMkAbs vs b
stripAbs :: Term -> ([Var],Term)
stripAbs tm =
case destAbs tm of
Nothing -> ([],tm)
Just (v,t) -> (v : vs, b) where (vs,b) = stripAbs t
size :: Term -> Size
size (Term _ _ s _ _ _) = s
typeOf :: Term -> Type
typeOf (Term _ _ _ ty _ _) = ty
isBool :: Term -> Bool
isBool = Type.isBool . typeOf
sameType :: Term -> Term -> Bool
sameType tm1 tm2 = typeOf tm1 == typeOf tm2
sameTypeVar :: Var -> Term -> Bool
sameTypeVar v tm = Var.typeOf v == typeOf tm
alphaCompare :: Term -> Term -> Ordering
alphaCompare =
tcmp 0 True bvEmpty bvEmpty
where
bvEmpty :: Map.Map Var Int
bvEmpty = Map.empty
tcmp n bvEq bv1 bv2 tm1 tm2 =
if bvEq && iEq tm1 tm2 then EQ
else case compare (size tm1) (size tm2) of
LT -> LT
EQ -> dcmp n bvEq bv1 bv2 (dest tm1) (dest tm2)
GT -> GT
iEq (Term _ i1 _ _ _ _) (Term _ i2 _ _ _ _) = i1 == i2
dcmp _ _ bv1 bv2 (VarTerm v1) (VarTerm v2) =
case (Map.lookup v1 bv1, Map.lookup v2 bv2) of
(Nothing,Nothing) -> compare v1 v2
(Just _, Nothing) -> LT
(Nothing, Just _) -> GT
(Just i1, Just i2) -> compare i1 i2
dcmp n bvEq bv1 bv2 (AbsTerm v1 b1) (AbsTerm v2 b2) =
case compare ty1 ty2 of
LT -> LT
EQ -> tcmp n' bvEq' bv1' bv2' b1 b2
GT -> GT
where
(n1,ty1) = Var.dest v1
(n2,ty2) = Var.dest v2
n' = n + 1
bvEq' = bvEq && n1 == n2
bv1' = Map.insert v1 n bv1
bv2' = if bvEq' then bv1' else Map.insert v2 n bv2
dcmp n bvEq bv1 bv2 (AppTerm f1 x1) (AppTerm f2 x2) =
case tcmp n bvEq bv1 bv2 f1 f2 of
LT -> LT
EQ -> tcmp n bvEq bv1 bv2 x1 x2
GT -> GT
dcmp _ _ _ _ d1 d2 = compare d1 d2
alphaEqual :: Term -> Term -> Bool
alphaEqual tm1 tm2 = alphaCompare tm1 tm2 == EQ
mkEqConst :: Type -> Term
mkEqConst a = mkConst Const.eq $ Type.mkEq a
destEqConst :: Term -> Maybe Type
destEqConst tm = do
ty <- destGivenConst Const.eq tm
Type.destEq ty
isEqConst :: Term -> Bool
isEqConst = isJust . destEqConst
mkEq :: Term -> Term -> Maybe Term
mkEq l r = listMkApp c [l,r] where c = mkEqConst (typeOf l)
mkEqUnsafe :: Term -> Term -> Term
mkEqUnsafe = mkUnsafe2 "HOL.Term.mkEq" mkEq
destEq :: Term -> Maybe (Term,Term)
destEq tm = do
(el,r) <- destApp tm
(e,l) <- destApp el
if isEqConst e then Just (l,r) else Nothing
isEq :: Term -> Bool
isEq = isJust . destEq
lhs :: Term -> Maybe Term
lhs = fmap fst . destEq
rhs :: Term -> Maybe Term
rhs = fmap snd . destEq
rhsUnsafe :: Term -> Term
rhsUnsafe = mkUnsafe1 "HOL.Term.rhs" rhs
mkRefl :: Term -> Term
mkRefl tm = mkEqUnsafe tm tm
destRefl :: Term -> Maybe Term
destRefl tm = do
(l,r) <- destEq tm
if l == r then Just l else Nothing
isRefl :: Term -> Bool
isRefl = isJust . destRefl
mkSelectConst :: Type -> Term
mkSelectConst a = mkConst Const.select $ Type.mkSelect a
destSelectConst :: Term -> Maybe Type
destSelectConst tm = do
ty <- destGivenConst Const.select tm
Type.destSelect ty
isSelectConst :: Term -> Bool
isSelectConst = isJust . destSelectConst
mkSelect :: Var -> Term -> Term
mkSelect v b =
mkAppUnsafe c (mkAbs v b)
where
c = mkSelectConst $ Var.typeOf v
destSelect :: Term -> Maybe (Var,Term)
destSelect tm = do
(c,vb) <- destApp tm
if isSelectConst c then destAbs vb else Nothing
isSelect :: Term -> Bool
isSelect = isJust . destSelect