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

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

module HOL.TermData
where

import Data.Maybe (isJust)
import HOL.Data
import qualified HOL.Type as Type
import qualified HOL.Var as Var

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

-- Constants

mkConst :: Const -> Type -> TermData
mkConst :: Const -> Type -> TermData
mkConst = Const -> Type -> TermData
ConstTerm

destConst :: TermData -> Maybe (Const,Type)
destConst :: TermData -> Maybe (Const, Type)
destConst (ConstTerm Const
c Type
ty) = (Const, Type) -> Maybe (Const, Type)
forall a. a -> Maybe a
Just (Const
c,Type
ty)
destConst TermData
_ = Maybe (Const, Type)
forall a. Maybe a
Nothing

isConst :: TermData -> Bool
isConst :: TermData -> Bool
isConst = Maybe (Const, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Const, Type) -> Bool)
-> (TermData -> Maybe (Const, Type)) -> TermData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermData -> Maybe (Const, Type)
destConst

destGivenConst :: Const -> TermData -> Maybe Type
destGivenConst :: Const -> TermData -> Maybe Type
destGivenConst Const
c TermData
d =
    case TermData -> Maybe (Const, Type)
destConst TermData
d of
      Just (Const
c',Type
ty) -> if Const
c' Const -> Const -> Bool
forall a. Eq a => a -> a -> Bool
== Const
c then Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty else Maybe Type
forall a. Maybe a
Nothing
      Maybe (Const, Type)
Nothing -> Maybe Type
forall a. Maybe a
Nothing

isGivenConst :: Const -> TermData -> Bool
isGivenConst :: Const -> TermData -> Bool
isGivenConst Const
c = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool)
-> (TermData -> Maybe Type) -> TermData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const -> TermData -> Maybe Type
destGivenConst Const
c

-- Variables

mkVar :: Var -> TermData
mkVar :: Var -> TermData
mkVar = Var -> TermData
VarTerm

destVar :: TermData -> Maybe Var
destVar :: TermData -> Maybe Var
destVar (VarTerm Var
v) = Var -> Maybe Var
forall a. a -> Maybe a
Just Var
v
destVar TermData
_ = Maybe Var
forall a. Maybe a
Nothing

isVar :: TermData -> Bool
isVar :: TermData -> Bool
isVar = Maybe Var -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Var -> Bool) -> (TermData -> Maybe Var) -> TermData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermData -> Maybe Var
destVar

eqVar :: Var -> TermData -> Bool
eqVar :: Var -> TermData -> Bool
eqVar Var
v TermData
d =
    case TermData -> Maybe Var
destVar TermData
d of
      Just Var
w -> Var
w Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
== Var
v
      Maybe Var
Nothing -> Bool
False

-- Function application

mkApp :: Term -> Term -> Maybe TermData
mkApp :: Term -> Term -> Maybe TermData
mkApp Term
f Term
x = do
    Type
ty <- Type -> Maybe Type
Type.domain Type
fty
    if Type
xty Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
ty then TermData -> Maybe TermData
forall a. a -> Maybe a
Just (TermData -> Maybe TermData) -> TermData -> Maybe TermData
forall a b. (a -> b) -> a -> b
$ Term -> Term -> TermData
AppTerm Term
f Term
x else Maybe TermData
forall a. Maybe a
Nothing
  where
    Term TermData
_ TermId
_ Size
_ Type
fty Set TypeVar
_ Set Var
_ = Term
f
    Term TermData
_ TermId
_ Size
_ Type
xty Set TypeVar
_ Set Var
_ = Term
x

destApp :: TermData -> Maybe (Term,Term)
destApp :: TermData -> Maybe (Term, Term)
destApp (AppTerm Term
f Term
x) = (Term, Term) -> Maybe (Term, Term)
forall a. a -> Maybe a
Just (Term
f,Term
x)
destApp TermData
_ = Maybe (Term, Term)
forall a. Maybe a
Nothing

isApp :: TermData -> Bool
isApp :: TermData -> Bool
isApp = Maybe (Term, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Term, Term) -> Bool)
-> (TermData -> Maybe (Term, Term)) -> TermData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermData -> Maybe (Term, Term)
destApp

-- Lambda abstraction

mkAbs :: Var -> Term -> TermData
mkAbs :: Var -> Term -> TermData
mkAbs = Var -> Term -> TermData
AbsTerm

destAbs :: TermData -> Maybe (Var,Term)
destAbs :: TermData -> Maybe (Var, Term)
destAbs (AbsTerm Var
v Term
b) = (Var, Term) -> Maybe (Var, Term)
forall a. a -> Maybe a
Just (Var
v,Term
b)
destAbs TermData
_ = Maybe (Var, Term)
forall a. Maybe a
Nothing

isAbs :: TermData -> Bool
isAbs :: TermData -> Bool
isAbs = Maybe (Var, Term) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Var, Term) -> Bool)
-> (TermData -> Maybe (Var, Term)) -> TermData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TermData -> Maybe (Var, Term)
destAbs

-------------------------------------------------------------------------------
-- Size is measured as the number of TermData constructors
-------------------------------------------------------------------------------

size :: TermData -> Size
size :: TermData -> Size
size (ConstTerm Const
_ Type
_) = Size
1
size (VarTerm Var
_) = Size
1
size (AppTerm Term
f Term
x) =
    Size
fsz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
xsz
  where
    Term TermData
_ TermId
_ Size
fsz Type
_ Set TypeVar
_ Set Var
_ = Term
f
    Term TermData
_ TermId
_ Size
xsz Type
_ Set TypeVar
_ Set Var
_ = Term
x
size (AbsTerm Var
_ Term
b) =
    Size
bsz Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1
  where
    Term TermData
_ TermId
_ Size
bsz Type
_ Set TypeVar
_ Set Var
_ = Term
b

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

typeOf :: TermData -> Type
typeOf :: TermData -> Type
typeOf (ConstTerm Const
_ Type
ty) = Type
ty
typeOf (VarTerm Var
v) = Var -> Type
Var.typeOf Var
v
typeOf (AppTerm Term
f Term
_) =
    case Type -> Maybe Type
Type.range Type
fty of
      Just Type
ty -> Type
ty
      Maybe Type
Nothing -> [Char] -> Type
forall a. HasCallStack => [Char] -> a
error [Char]
"HOL.TermData.typeOf: bad types in AppTerm"
  where
    Term TermData
_ TermId
_ Size
_ Type
fty Set TypeVar
_ Set Var
_ = Term
f
typeOf (AbsTerm Var
v Term
b) =
    Type -> Type -> Type
Type.mkFun (Var -> Type
Var.typeOf Var
v) Type
bty
  where
    Term TermData
_ TermId
_ Size
_ Type
bty Set TypeVar
_ Set Var
_ = Term
b

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

freeInMultiple :: Var -> TermData -> Bool
freeInMultiple :: Var -> TermData -> Bool
freeInMultiple Var
v = TermData -> Bool
go
  where
    go :: TermData -> Bool
go (ConstTerm Const
_ Type
_) = Bool
False
    go (VarTerm Var
_) = Bool
False
    go (AppTerm Term
f Term
x) =
        case (Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.freeIn Var
v Term
f, Var -> Term -> Bool
forall a. HasFree a => Var -> a -> Bool
Var.freeIn Var
v Term
x) of
          (Bool
True,Bool
True) -> Bool
True
          (Bool
True,Bool
False) -> TermData -> Bool
go TermData
fd
          (Bool
False,Bool
True) -> TermData -> Bool
go TermData
xd
          (Bool
False,Bool
False) -> Bool
False
      where
        Term TermData
fd TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
_ = Term
f
        Term TermData
xd TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
_ = Term
x
    go (AbsTerm Var
w Term
b) = Var
w Var -> Var -> Bool
forall a. Eq a => a -> a -> Bool
/= Var
v Bool -> Bool -> Bool
&& TermData -> Bool
go TermData
bd
      where
        Term TermData
bd TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
_ = Term
b