{- |
module: $Header$
description: Higher order logic terms
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

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

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

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

-- Constants

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

-- Variables

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

-- Function application

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

-- Lambda abstraction

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 is measured as the number of TermData constructors
-------------------------------------------------------------------------------

size :: Term -> Size
size :: Term -> Size
size (Term TermData
_ TermId
_ Size
s Type
_ Set TypeVar
_ Set Var
_) = Size
s

-------------------------------------------------------------------------------
-- The type of a (well-formed) term
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Free variables in terms
-------------------------------------------------------------------------------

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)

-------------------------------------------------------------------------------
-- A total order on terms modulo alpha-equivalence
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Rename all bound variables to fresh names
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Primitive constants
-------------------------------------------------------------------------------

-- Equality

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

-- Hilbert's choice operator

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