HaskHOL.Core.Basics

This module defines common utility functions that depend on data types introduced by HaskHOL. See the HaskHOL.Core.Lib module for utility functions that do not have this dependence.

Variable Term Generation

genVarWithName :: String -> HOLType -> HOL cls thry HOLTerm

Generates a new term variable consisting of a given prefix and the next value in the fresh term counter.

genVar :: HOLType -> HOL cls thry HOLTerm

A version of genVarWithName that defaults to the prefix "_".

Common Type Functions

occursIn :: HOLType -> HOLType -> Bool

Checks to see if the first type occurs in the second type. Note that the predicate is also satisfied if the two types are equal.

tysubst :: HOLTypeEnv -> HOLType -> Either String HOLType

Basic type substitution that ignores type operators and prunes the substitution environment of bound variables rather than handle renaming. Works for all types, variable and non-variable alike. Fails with Left when the substitution would result in an invalid type construction.

Note that the order of the elements of the substitution pairs matches other environments in the systems, such that for the pair (A, B) B will be substituted for all instances of A.

alphaUtype :: HOLType -> HOLType -> Either String HOLType

Alpha conversion for universal types. Renames a bound type variable to match the name of a provided type variable. Fails with Left in the following cases:

• First type is not a small type variable.
• Second type is not a universal type.
• The type variable is free in the body of the universal type.

Common Term Functions

freeIn :: HOLTerm -> HOLTerm -> Bool

Predicate to check if the first term is free in the second modulo alpha-equivalence.

subst :: HOLTermEnv -> HOLTerm -> HOL cls thry HOLTerm

Basic term substitution. Throws a HOLException when the substitution would result in an invalid term construction.

Note that the order of the elements of the substitution pairs matches other environments in the systems, such that for the pair (A, B) B will be substituted for all instances of A.

alpha :: HOLTerm -> HOLTerm -> Either String HOLTerm

Alpha conversion for term abstractions. Renames a bound variable to match the name of a provided variable. Fails with Left in the following cases:

• First term is not a variable.
• Second term is not an abstraction.
• The types of the variable and bound variable do no agree.
• The variable is free in the body of the abstraction.

alphaTyabs :: HOLType -> HOLTerm -> Either String HOLTerm

Alpha conversion for type abstractions. Renames a bound type variable to match the name of a provided type variable. Fails with Left in the following cases:

• The provided type is not a small type variable.
• The provided term is not a type abstraction.
• The type is free in the body of the type abstraction.

findTerm :: (HOLTerm -> Bool) -> HOLTerm -> Maybe HOLTerm

Searches a term for a subterm that satisfies a given predicate. Fails with Nothing if no such term is found.

findTerms :: (HOLTerm -> Bool) -> HOLTerm -> [HOLTerm]

Searches a term for all unique subterms that satisfy a given predicate.

findPath :: (HOLTerm -> Bool) -> HOLTerm -> Maybe String

Searches a term for a subterm that satisfies a given predicate, returning a string that indicates the path to that subterm:

• 'b' - Take the body of an abstraction.
• 't' - Take the body of a type abstraction.
• 'l' - Take the left path in a term combination.
• 'r' - Take the right path in a term combination.
• 'c' - Take the body in a type combination.

Fails with Nothing if there is no satisfying subterm.

followPath :: String -> HOLTerm -> Maybe HOLTerm

Returns the subterm found by following a String path as produced by findPath. Fails with Nothing if the provided term does not a suitable subterm for the given path.

Common Theorem Functions

typeVarsInThm :: HOLThm -> [HOLType]

Returns the list of all free type variables in a theorem.

thmFrees :: HOLThm -> [HOLTerm]

Returns the list of all free term variables in a theorem.

Derived Destructors and Constructors for Basic Terms

listMkComb :: HOLTerm -> [HOLTerm] -> Either String HOLTerm

Constructs a complex combination that represents the application of a function to a list of arguments. Fails with Left if any internal call to mkComb fails.

listMkAbs :: [HOLTerm] -> HOLTerm -> Either String HOLTerm

Constructs a complex abstraction that represents a term with multiple bound variables. Fails with Left if any internal call to mkAbs fails.

mkArgs :: String -> [HOLTerm] -> [HOLType] -> [HOLTerm]

Constructs a list of term variables of a given prefix. Names are adjusted as necessary with variant to avoid clashing with the provided list of term variables. The number and types of the resultant variables is directed by the provided list of types, i.e.

 mkArgs "x" avoids [ty1, ... tyn] === [x1:ty1, ..., xn:tyn] where {x1, ..., xn} are not elements of avoids

rator :: HOLTerm -> Maybe HOLTerm

Returns the left term of a combination. Fails with Nothing if the provided term is not a combination.

rand :: HOLTerm -> Maybe HOLTerm

Returns the right term of a combination. Fails with Nothing if the provided term is not a combination.

bndvar :: HOLTerm -> Maybe HOLTerm

Returns the bound term of an abstraction. Fails with Nothing if the provided term is not an abstraction.

body :: HOLTerm -> Maybe HOLTerm

Returns the body term of an abstraction. Fails with Nothing if the provided term is not an abstraction.

bndvarTyabs :: HOLTerm -> Maybe HOLType

Returns the bound type of a type abstraction. Fails with Nothing if the provided term is not a type abstraction.

bodyTyabs :: HOLTerm -> Maybe HOLTerm

Returns the body term of a type abstraction. Fails with Nothing if the provided term is not a type abstraction.

stripComb :: HOLTerm -> (HOLTerm, [HOLTerm])

Destructs a complex combination returning its function term and its list of argument terms.

stripAbs :: HOLTerm -> ([HOLTerm], HOLTerm)

Destructs a complex abstraction returning its list of bound variables and its body term.

Type Matching Functions

typeMatch :: HOLType -> HOLType -> SubstTrip -> Maybe SubstTrip

Computes a tiplet of substitution environments that can be used to make two types match. The triplet argument can be used to constrain the match, or its three environments can be left empty to find the most general match. Fails with Nothing in the event that a match cannot be found that satisfies the provided constraint.

mkMConst :: String -> HOLType -> HOL cls thry HOLTerm

Constructs an instance of a constant of the provided name and type. Relies internally on typeMatch in order to provide a match between the most general type of the constant and the provided type. Throws a HOLException in the following cases:

• The provided string is not the name of a defined constant.
• Type matching fails.

mkIComb :: HOLTerm -> HOLTerm -> Maybe HOLTerm

A version of mkComb that instantiates the type variables in the left hand argument. Relies internally on typeMatch in order to provide a match between the domain type of the function and the type of the argument. Fails with Nothing if instantiation is impossible.

listMkIComb :: String -> [HOLTerm] -> HOL cls thry HOLTerm

An iterative version of mkIComb that builds a complex combination given a constant name and a list of arguments, attempting to find a correct instantiation at every step. Throws a HOLException in the following cases:

• The provided name is not a currently defiend constant.
• Any internal call to mkIComb fails.

Predicates, Constructors, and Destructors for Binary Terms

isBinary :: String -> HOLTerm -> Bool

Predicate that tests if a term is a binary application whose operator has the given name.

isBinop :: HOLTerm -> HOLTerm -> Bool

A version of isBinary that tests for operator terms, not strings.

destBinary :: String -> HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructs a binary application returning its left and right arguments. Fails with Nothing if the provided term is not a binary application with the specified operator name.

destBinop :: HOLTerm -> HOLTerm -> Maybe (HOLTerm, HOLTerm)

A version of destBinary that tests for operator terms, not strings.

mkBinary :: String -> HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructs a binary application given a constant name and two argument terms. Note that no instantiation is performed, thus the constant must be monomorphic or the provided arguments must match the constant's general type. Throws a HOLException if any of the internal calls to mkConst or mkComb fail.

mkBinop :: HOLTerm -> HOLTerm -> HOLTerm -> Either String HOLTerm

A version of mkBinary that accepts the operator as a pre-constructed term.

listMkBinop :: HOLTerm -> [HOLTerm] -> Either String HOLTerm

Iteratively builds a complex combination using mkBinop, i.e.

 listMkBinop (/\) [T, F, T] === T /\ F /\ T

binops :: HOLTerm -> HOLTerm -> [HOLTerm]

The inverse of listMkBinop. Destructs a complex combination built with a binary operator into its list of arguments.

Predicates, Constructors, and Destructors for Complex Abstractions

isGAbs :: HOLTerm -> Bool

Predicate for generalized abstractions. See mkGAbs for more details.

isBinder :: String -> HOLTerm -> Bool

Predicate that tests if a term is an abstraction of specified binder name.

isTyBinder :: String -> HOLTerm -> Bool

Predicate that tests if a term is an abtraction of a specified type binder name.

destGAbs :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for generalized abstractions. Fails with Nothing if the provided term is not an abstraction or generalized abstraction. See mkGAbs for more details.

destBinder :: String -> HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructs an abstraction of specified binder name into its bound variable and its body term. Fails with Nothing if the provided term is not an abstraction with the specified binder name.

destTyBinder :: String -> HOLTerm -> Maybe (HOLType, HOLTerm)

Destructs a type abstraction of specified binder name into its bound type variable and its body term. Fails with Nothing if the provided term is not a type abstraction with the specified type binder name.

mkGAbs :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for generalized abstractions. Generalized abstractions extend term abstractions to the more general of notion of a function mapping some structure to some term. This allows us to bind patterns more complicated than a variable, i.e. binding pairs

 \ (x:num, y:num) -> x + y

or lists

 \ CONS x xs -> x

Note that in the case where the pattern to bind is simply a variable mkGAbs just calls mkAbs.

mkBinder :: String -> HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructs an abstraction given a binder name and two argument terms. Throws a HOLException if any of the internal calls to mkConst, mkAbs, or mkComb fail.

Note that the given string can actually be any constant name of type (A -> *) -> *, such that a well-typed term of the form c (\x . t) can be produced.

mkTyBinder :: String -> HOLType -> HOLTerm -> HOL cls thry HOLTerm

Constructs a type abstraction given a type binder name, a type variable to find, and a body term. Throws a HOLException if any of the internal calls to mkConst, mkTyAbs, or mkComb fail.

Note that the given string can actually be any constant name of type (% 'a . *) -> *, such that a well-typed term of the form c (\\x . t) can be produced.

listMkGAbs :: [HOLTerm] -> HOLTerm -> HOL cls thry HOLTerm

A specific version of listMkAbs for general abstractions.

stripGAbs :: HOLTerm -> ([HOLTerm], HOLTerm)

A specific version of stripAbs for general abstractions.

Predicates, Constructors, and Destructors for Propositions

isConj :: HOLTerm -> Bool

Predicate for boolean conjunctions.

isImp :: HOLTerm -> Bool

Predicate for boolean implications.

isForall :: HOLTerm -> Bool

Predicate for universal term quantification.

isExists :: HOLTerm -> Bool

Predicate for existential term quantification.

isDisj :: HOLTerm -> Bool

Predicate for boolean disjunctions.

isNeg :: HOLTerm -> Bool

Predicate for boolean negations.

isUExists :: HOLTerm -> Bool

Predicate for unique, existential quantification.

isTyAll :: HOLTerm -> Bool

Predicate for term-level universal type quantification.

isTyEx :: HOLTerm -> Bool

Predicate for term-level existential type quantification.

destConj :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for boolean conjunctions.

destImp :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for boolean implications.

destForall :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for universal term quantification.

destExists :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for existential term quantification.

destDisj :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for boolean disjunctions.

destNeg :: HOLTerm -> Maybe HOLTerm

Destructor for boolean negations.

destUExists :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for unique, existential quantification.

destTyAll :: HOLTerm -> Maybe (HOLType, HOLTerm)

Destructor for term-level universal type quantification.

destTyEx :: HOLTerm -> Maybe (HOLType, HOLTerm)

Destructor for term-level existential type quantification.

mkConj :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for boolean conjunctions. Throws a HOLException if the internal call to mkBinary fails.

mkImp :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for boolean implications. Throws a HOLException if the internal call to mkBinary fails.

mkForall :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for universal term quantification. Throws a HOLException if the internal call to mkBinder fails.

mkExists :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for existential term quantification. Throws a HOLException if the internal call to mkBinder fails.

mkDisj :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for boolean disjunctions. Throws a HOLException if the internal call to mkBinary fails.

mkNeg :: HOLTerm -> HOL cls thry HOLTerm

Constructor for boolean negations. Throws a HOLException if any of the internal calls to mkConst or mkComb fail.

mkUExists :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Constructor for unique, existential term quantification. Throws a HOLException if the internal call to mkBinder fails.

mkTyAll :: HOLType -> HOLTerm -> HOL cls thry HOLTerm

Constructor for term-level universal type quantification. Throws a HOLException if the internal call to mkTyBinder fails.

mkTyEx :: HOLType -> HOLTerm -> HOL cls thry HOLTerm

Constructor for term-level existential type quantification. Throws a HOLException if the internal call to mkTyBinder fails.

listMkConj :: [HOLTerm] -> HOL cls thry HOLTerm

Constructs a complex conjunction from a given list of propositions.

listMkDisj :: [HOLTerm] -> HOL cls thry HOLTerm

Constructs a complex disjunction from a given list of propositions.

listMkForall :: [HOLTerm] -> HOLTerm -> HOL cls thry HOLTerm

A specific version of listMkAbs for universal term quantification.

listMkExists :: [HOLTerm] -> HOLTerm -> HOL cls thry HOLTerm

A specific version of listMkAbs for existential term quantification.

conjuncts :: HOLTerm -> [HOLTerm]

Returns the list of propositions in a complex conjunction.

disjuncts :: HOLTerm -> [HOLTerm]

Returns the list of propositions in a complex disjunction.

stripForall :: HOLTerm -> ([HOLTerm], HOLTerm)

A specific version of stripAbs for universal term quantification.

stripExists :: HOLTerm -> ([HOLTerm], HOLTerm)

A specific version of stripAbs for existential term quantification.

stripTyAll :: HOLTerm -> ([HOLType], HOLTerm)

A specific version of stripAbs for term-level universal type quantification.

stripTyEx :: HOLTerm -> ([HOLType], HOLTerm)

A specific version of stripAbs for term-level existential type quantification.

Predicates, Constructors, and Destructors for Other Terms

isCons :: HOLTerm -> Bool

Predicate for list CONS.

isList :: HOLTerm -> Bool

Predicate for list terms.

isLet :: HOLTerm -> Bool

Predicate for let binding terms.

destCons :: HOLTerm -> Maybe (HOLTerm, HOLTerm)

Destructor for list CONS.

destList :: HOLTerm -> Maybe [HOLTerm]

Destructor for list terms. Returns a list of the elements in the term. Fails with Nothing if internall the term is not of the form

 x1 `CONS` .... xn `CONS` NIL

destLet :: HOLTerm -> Maybe ([(HOLTerm, HOLTerm)], HOLTerm)

Destructs a let binding term into a list of its name and value pairs and its body term. Fails with Nothing if internally the term is not of the form

 LET (x1, v1) ... (xn, vn) LET_END

destNumeral :: HOLTerm -> Maybe Integer

Converts a numeral term to an Integer. Fails with Nothing if internally the term is not of the form

 NUMERAL bits _0, where bits is a series of BIT0 and BIT1 terms  

Term Nets

data Net a

Internally, Nets are represented with a tree structure; each node has a list of labeled branches and a list of values. The node labels are generated via the following guidelines:

• Flattening of combinations favors the left hand side such that the head of an application is looked at first.
• If the head of an application is variable, the whole term is considered variable.
• Type abstractions and type combinations are effectively treated as local constants, though they do have their own node lable representations to avoid any potential issues with user provided variable lists for enter.
• Matching is conservative, such that all matching values will be returned, but some non-matching values may be returned. For example, a pattern term of the form x `op` x will match any term of the form a `op` b regardless of the values of a and b.

Instances

Show a => Show (Net a)

Lift a0 => Lift (Net a0)

netEmpty :: Net a

The empty Net.

netEnter :: Ord a => [HOLTerm] -> (HOLTerm, a) -> Net a -> HOL cls thry (Net a)

Inserts a new element, paired with a pattern term, into a provided net. The first argument is a list of variables that should be treated as local constants, such that only patterns with those variables at the exact same position will match. See the documentation for Net for more details.

Never fails.

netLookup :: HOLTerm -> Net a -> [a]

Returns the list of all values stored in a term net that satisfy a provided pattern term. See the documentation for Net for more details.

netMerge :: Ord a => Net a -> Net a -> Net a

Merges two term nets together. The values for the two nets are merged, maintaining order and uniqueness, with the term labels adjusted appropriately. The algorithm to do so is courtesy of Don Syme via John Harrison's implementation in HOL Light.