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