Portability | unknown |
---|---|

Stability | unstable |

Maintainer | ecaustin@ittc.ku.edu |

Safe Haskell | None |

This module exports a safe view of HOL terms for HaskHOL. It also defines the primitive functions related to terms. For clarity, these functions have been seperated based on their influential system: HOL Light, Stateless HOL, and HOL2P.

Note that, per the stateless approach, any stateful, but still primitive, functions related to terms have been relocated to the HaskHOL.Core.State module.

- data HOLTerm
- data HOLTermView
- data ConstTag
- type HOLTermEnv = [(HOLTerm, HOLTerm)]
- alphaOrder :: HOLTerm -> HOLTerm -> Ordering
- aConv :: HOLTerm -> HOLTerm -> Bool
- isVar :: HOLTerm -> Bool
- isConst :: HOLTerm -> Bool
- isAbs :: HOLTerm -> Bool
- isComb :: HOLTerm -> Bool
- mkVar :: String -> HOLType -> HOLTerm
- mkAbs :: HOLTerm -> HOLTerm -> Either String HOLTerm
- mkComb :: HOLTerm -> HOLTerm -> Either String HOLTerm
- destVar :: HOLTerm -> Maybe (String, HOLType)
- destConst :: HOLTerm -> Maybe (String, HOLType)
- destComb :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
- destAbs :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
- frees :: HOLTerm -> [HOLTerm]
- catFrees :: [HOLTerm] -> [HOLTerm]
- freesIn :: [HOLTerm] -> HOLTerm -> Bool
- varFreeIn :: HOLTerm -> HOLTerm -> Bool
- typeVarsInTerm :: HOLTerm -> [HOLType]
- typeVarsInTerms :: [HOLTerm] -> [HOLType]
- varSubst :: HOLTermEnv -> HOLTerm -> HOLTerm
- class TypeSubst a b => Inst a b
- inst :: Inst a b => [(a, b)] -> HOLTerm -> HOLTerm
- instFull :: SubstTrip -> HOLTerm -> HOLTerm
- instConst :: TypeSubst a b => HOLTerm -> [(a, b)] -> Maybe HOLTerm
- instConstFull :: HOLTerm -> SubstTrip -> Maybe HOLTerm
- tmEq :: HOLType -> HOLTerm
- isEq :: HOLTerm -> Bool
- primMkEq :: HOLTerm -> HOLTerm -> Either String HOLTerm
- destEq :: HOLTerm -> Maybe (HOLTerm, HOLTerm)
- variant :: [HOLTerm] -> HOLTerm -> HOLTerm
- variants :: [HOLTerm] -> [HOLTerm] -> [HOLTerm]
- newPrimConst :: String -> HOLType -> HOLTerm
- typeOpVarsInTerm :: HOLTerm -> [TypeOp]
- typeOpVarsInTerms :: [HOLTerm] -> [TypeOp]
- isTyAbs :: HOLTerm -> Bool
- isTyComb :: HOLTerm -> Bool
- mkTyAbs :: HOLType -> HOLTerm -> Either String HOLTerm
- mkTyComb :: HOLTerm -> HOLType -> Either String HOLTerm
- destTyAbs :: HOLTerm -> Maybe (HOLType, HOLTerm)
- destTyComb :: HOLTerm -> Maybe (HOLTerm, HOLType)

# A View of HOL Terms

## A Quick Note on View Patterns

The primitive data types of HaskHOL are implemented using view patterns in order to simulate private data types:

- Internal constructors are hidden to prevent manual construction of terms.
- View constructors (those of
`HOLTypeView`

,`HOLTermView`

, and`HOLThmView`

) are exposed to enable pattern matching. - View patterns, as defined by instances of the
`view`

function from the`Viewable`

class, provide a conversion between the two sets of constructors.

The `HOLTerm`

data type defines the internal constructors for HOL terms in
HaskHOL. For more details, see the documentation for its view pattern data
type, `HOLTermView`

.

data HOLTermView Source

The view pattern data type for HOL terms.

Var String HOLType | A term variable consisting of a name and type. |

Const String HOLType ConstTag | A term constant consisting of a name, type, and tag. See |

Comb HOLTerm HOLTerm | A term application consisting of a function term and argument term. |

Abs HOLTerm HOLTerm | A term abstraction consisting of a bound term and a body term. Note that the bound term must be a type variable. |

TyComb HOLTerm HOLType | A term-level, type application consisting of a body term and an argument type. Note that the body term must have a universal type. |

TyAbs HOLType HOLTerm | A term-level, type abstraction consisting of a bound type and a body term. Note that the bound type must be a small, type variable. |

The data type for constant tags, `ConstTag`

, follows identically from the
implementation in Stateless HOL. For more information regarding construction
of the different tags, see the documentation of the following functions:
`newPrimConst`

, `newDefinedConst`

, and `newDefinedTypeOp`

.

type HOLTermEnv = [(HOLTerm, HOLTerm)]Source

Type synonym for the commonly used, list-based, term environment.

# HOL Light Term Primitives

## Alpha-Equivalence of Terms

alphaOrder :: HOLTerm -> HOLTerm -> OrderingSource

Provides an ordering for two terms modulo alpha-equivalence

## Predicates, Constructors, and Destructors for Basic Terms

mkAbs :: HOLTerm -> HOLTerm -> Either String HOLTermSource

Constructs a term abstraction of a given bound term and body term. Fails with
`Left`

if the bound term is not a variable.

mkComb :: HOLTerm -> HOLTerm -> Either String HOLTermSource

Constructs a combination of two given terms. Fails with `Left`

in the
following cases:

- The first term does not have a function type.
- The types of the two terms does not agree.

destVar :: HOLTerm -> Maybe (String, HOLType)Source

Destructs a term variable, returning its name and type. Fails with `Nothing`

if the provided term is not a variable.

destConst :: HOLTerm -> Maybe (String, HOLType)Source

Destructs a term constant, returning its name and type. Note that no constant
tag information is returned. Fails with `Nothing`

if the provided term is
not a constant.

destComb :: HOLTerm -> Maybe (HOLTerm, HOLTerm)Source

Destructs a term combination, returning its function and argument terms.
Fails with `Nothing`

if the provided term is not a combination.

destAbs :: HOLTerm -> Maybe (HOLTerm, HOLTerm)Source

Destructs a term abstraction, returning its bound term and body term. Fails
with `Nothing`

if the provided term is not an abstraction.

## Term and Type Variable Extractors

catFrees :: [HOLTerm] -> [HOLTerm]Source

Returns a list of all free, term variables in a list of terms.

freesIn :: [HOLTerm] -> HOLTerm -> BoolSource

Checks a list of term variables to see if they are all free in a give term.

varFreeIn :: HOLTerm -> HOLTerm -> BoolSource

Checks if a variable or constant term is free in a given term.

typeVarsInTerm :: HOLTerm -> [HOLType]Source

Returns a list of all free, type variables in a term, not including type operator variables.

typeVarsInTerms :: [HOLTerm] -> [HOLType]Source

Returns a list of all free, type variables in a list of terms, not including type operator variables.

## Term Substitution and Instantiation

varSubst :: HOLTermEnv -> HOLTerm -> HOLTermSource

Performs a basic term substitution using a substitution environment containing pairs consisting of a term variable and a term to be substituted for that variable. Note that the order of elements in a substitution pair follows the convention of most Haskell libraries, rather than the traditional HOL convention:

- The second element is substituted for the first, i.e. the substitution pair
`(A, \ x.x)`

indicates that the lambda term`\x.x`

should be substituted for the term variable`A`

.

class TypeSubst a b => Inst a b Source

The `Inst`

class provides the framework for type instantiation in HaskHOL.
Note that in the simplest cases, instantiation is simply a type substitution
for the types of term variables and constants. Therefore, instantiation is
constrained by the `TypeSubst`

class.

The move to a polymorphic type system further complicates things as types can now be bound at the term level, requiring renaming for type instantiation. Since we have three different possible substitution environment types, we have three different possible instantiation environment types and, therefore, three different ways to handle renaming:

- For
`(x::`

substitution pairs we rename in the case where a type abstraction binds a type variable present in`HOLTerm`

, r::`HOLTerm`

)`r`

and`x`

is present in the body of the type abstraction. - For
`(_::`

substitution pairs we can safely ignore renaming as our logic does not permit the binding of type operator variables.`TypeOp`

, _::`TypeOp`

) - For
`(x::`

substitution pairs we rename in the case where a type abstraction binds a type variable present in`TypeOp`

, r::`HOLTerm`

)`r`

and`x`

is present in the body of the type abstraction.

Just as we did for the `TypeSubst`

class, we hide the internals of `Inst`

to
prevent unsound re-definition. The correct functions to call for
type instantiation are `inst`

and `instFull`

.

inst :: Inst a b => [(a, b)] -> HOLTerm -> HOLTermSource

Type instantiation for terms. Accepts the same types of substitution
environments as discussed in the documentation for the `TypeSubst`

class,
with invalid substitution pairs being pruned internally by `typeSubst`

as
necessary.

For more information on why the `Inst`

class constraint is necessary and how
renaming of bound types is performed, see that classes documentation.

instFull :: SubstTrip -> HOLTerm -> HOLTermSource

A version of `inst`

that accepts a triplet of type substitution environments.

instConstFull :: HOLTerm -> SubstTrip -> Maybe HOLTermSource

A version of `instConst`

that accepts a triplet of type substitition
environments.

## Commonly Used Terms and Functions

tmEq :: HOLType -> HOLTermSource

Constructs an instance of the HOL equality constant, `=`

, for a given type.

primMkEq :: HOLTerm -> HOLTerm -> Either String HOLTermSource

Constructs an equation term given the left and right hand side arguments.
Fails with `Left`

if the types of the terms are not alpha-equivalent.

destEq :: HOLTerm -> Maybe (HOLTerm, HOLTerm)Source

Destructs an equation term, returning the left and right hand side arguments.
Fails with `Nothing`

if the term is not an equation, i.e. of the form `l = r`

.

variant :: [HOLTerm] -> HOLTerm -> HOLTermSource

Renames a term variable to avoid sharing a name with any of a given list of term variables. Rreturns the original term if it's not a term variable.

variants :: [HOLTerm] -> [HOLTerm] -> [HOLTerm]Source

Renames a list of term variables to avoid sharing a name with any of a given list of term variables. As each term variable is processed it is added to the list of avoids such that the resultant list of term variables are all uniquely named.

# Stateless HOL Term Primitives

## Constructors for Constant Tags

newPrimConst :: String -> HOLType -> HOLTermSource

Constructs a primitive constant given a name and type. Note that primitive
constants are tagged with a `Prim`

`ConstTag`

indicating that they have no
definition.

## Type Operator Variable Extractors

typeOpVarsInTerm :: HOLTerm -> [TypeOp]Source

Returns the list of all type operator variables in a term.

typeOpVarsInTerms :: [HOLTerm] -> [TypeOp]Source

Returns the list of all type operator variables in a list of terms.

# HOL2P Term Primitives

## Predicates, Constructors, and Destructors for Term-Level Types

mkTyAbs :: HOLType -> HOLTerm -> Either String HOLTermSource

Constructs a type abstraction term given a bound type and a body term. Fails
with `Left`

in the following cases:

- The bound type is not a small type variable.
- The bound type variable occurs in the type of a free variable in the body term.

mkTyComb :: HOLTerm -> HOLType -> Either String HOLTermSource

Constructs a type combination term given a body term and a type argument to
apply. Fails with `Left`

in the following cases:

- The type argument is not a small type.
- The type of the body term is not a universal type.