HaskHOL.Core.State

This module exports the stateful layer of HaskHOL. It consists of:

• Stateful type primitives not found in HaskHOL.Core.Types.
• Stateful term primitives not found in HaskHOL.Core.Terms.
• Stateful theory extension primitives not found in HaskHOL.Core.Kernel.
• A very primitive debugging system.

Stateful Type Primitives

types :: HOL cls thry [(String, TypeOp)]

Retrieves the list of type constants from the current working theory. The list contains pairs of strings recognized by the parser and the associated type operator value, i.e.

 ("bool", tyOpBool)

getTypeArityCtxt :: HOLContext thry -> String -> Maybe Int

Retrieves the arity of a given type constant. Fails with Nothing if the provided type constant name is not defined in the provided context.

Note that this function takes a HOLContext argument such that it can be used outside of HOL computations; for example, in the parser.

getTypeArity :: String -> HOL cls thry Int

A version of getTypeArityCtxt that operates over the current working theory of a HOL computation. Throws a HOLException if the provided type constant name is not defined.

newType :: String -> Int -> HOL Theory thry ()

Constructs a new primitve type constant of a given name and arity. Also adds this new type to the current working theory. Throws a HOLException when a type of the same name has already been declared.

mkType :: String -> [HOLType] -> HOL cls thry HOLType

Constructs a type application given an operator name and a list of argument types. If the provided name is not a currently defined type constant then this function defaults it to a type operator variable. Throws a HOLException in the following cases:

• A type operator's arity disagrees with the length of the argument list.
• A type operator is applied to zero arguments.

mkFunTy :: HOLType -> HOLType -> HOL cls thry HOLType

Constructs a function type safely using mkType. Should never fail provided that the initial value for type constants has not been modified.

Stateful Term Primitives

constants :: HOL cls thry [(String, HOLTerm)]

Retrieves the list of term constants from the current working theory. The list contains pairs of strings recognized by the parser and the associated term constant value, i.e.

 ("=", tmEq tyA)

getConstType :: String -> HOL cls thry HOLType

Retrieves the type of a given term constant. Throws a HOLException if the provided term constant name is not defined.

newConstant :: String -> HOLType -> HOL Theory thry ()

Constructs a new primitive term constant of a given name and type. Also adds this new term to the current working theory. Throws a HOLException when a term of the same name has already been declared.

mkConst :: TypeSubst l r => String -> [(l, r)] -> HOL cls thry HOLTerm

Constructs a specific instance of a term constant when provided with its name and a type substition environment. Throws a HOLException in the following cases:

• The instantiation as performed by instConst fails.
• The provided name is not a currently defined constant.

mkConstFull :: String -> SubstTrip -> HOL cls thry HOLTerm

A version of mkConst that accepts a triplet of type substitition environments. Frequently used with the typeMatch function.

mkEq :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm

Safely creates an equality between two terms using mkConst using the type of the left hand side argument to perform the required instantiation. Throws a HOLException in the case when the types of the two terms do not agree.

Stateful Theory Extension Primitives

axioms :: HOL cls thry [(String, HOLThm)]

Retrieves the list of axioms from the current working theory. The list contains pairs of string names and the axioms. This names exists such that compile time operations have a tag with which they can use to extract axioms from saved theories. See extractAxiom for more details.

getAxiom :: String -> HOL cls thry HOLThm

Retrieves a specific axiom by name. Throws a HOLException if there is no axiom with the provided name in the current working theory.

newAxiom :: String -> HOLTerm -> HOL Theory thry HOLThm

Constructs a new axiom of a given name and conclusion term. Also adds this new axiom to the current working theory. Throws a HOLException in the following cases:

• The provided term is not a proposition.
• An axiom with the provided name has already been declared.

definitions :: HOL cls thry [HOLThm]

Retrieves the list of definitions from the current working theory. See newBasicDefinition for more details.

newBasicDefinition :: HOLTerm -> HOL Theory thry HOLThm

Introduces a definition of the form c = t into the current working theory. Throws a HOLException when the definitional term is ill-formed. See newDefinedConst for more details.

newBasicTypeDefinition :: String -> String -> String -> HOLThm -> HOL Theory thry (HOLThm, HOLThm)

Introduces a new type constant, and two associated term constants, into the current working theory that is defined as an inhabited subset of an existing type constant. Takes the following arguments:

• The name of the new type constant.
• The name of the new term constant that will be used to construct the type.
• The name of the new term constant that will be used to desctruct the type.
• A theorem that proves that the defining predicate has at least one satisfying value.

Throws a HOLException in the following cases:

• A term constant of either of the provided names has already been defined.
• A type constant of the provided name has already been defined.

See newDefinedTypeOp for more details.

Primitive Debugging System

data FlagDebug

Flag states whether or not to print debug statements.

Constructors

FlagDebug

Instances

Typeable FlagDebug

BenignFlag FlagDebug

warn :: Bool -> String -> HOL cls thry ()

Prints the provided string, with a new line, when the given boolean value is true.

printDebugLn :: String -> HOL cls thry a -> HOL cls thry a

Prints the provided string, with a new line, when debugging is turned on, then returns the given HOL computation. A version of trace for the HOL monad that is referentially transparent.

printDebug :: String -> HOL cls thry a -> HOL cls thry a

A version of printDebug that does not print a new line.

Monad Re-Export

module HaskHOL.Core.State.Monad