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

Stability | unstable |

Maintainer | ecaustin@ittc.ku.edu |

Safe Haskell | None |

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.

- types :: HOL cls thry [(String, TypeOp)]
- getTypeArityCtxt :: HOLContext thry -> String -> Maybe Int
- getTypeArity :: String -> HOL cls thry Int
- newType :: String -> Int -> HOL Theory thry ()
- mkType :: String -> [HOLType] -> HOL cls thry HOLType
- mkFunTy :: HOLType -> HOLType -> HOL cls thry HOLType
- constants :: HOL cls thry [(String, HOLTerm)]
- getConstType :: String -> HOL cls thry HOLType
- newConstant :: String -> HOLType -> HOL Theory thry ()
- mkConst :: TypeSubst l r => String -> [(l, r)] -> HOL cls thry HOLTerm
- mkConstFull :: String -> SubstTrip -> HOL cls thry HOLTerm
- mkEq :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm
- axioms :: HOL cls thry [(String, HOLThm)]
- getAxiom :: String -> HOL cls thry HOLThm
- newAxiom :: String -> HOLTerm -> HOL Theory thry HOLThm
- definitions :: HOL cls thry [HOLThm]
- newBasicDefinition :: HOLTerm -> HOL Theory thry HOLThm
- newBasicTypeDefinition :: String -> String -> String -> HOLThm -> HOL Theory thry (HOLThm, HOLThm)
- data FlagDebug = FlagDebug
- warn :: Bool -> String -> HOL cls thry ()
- printDebugLn :: String -> HOL cls thry a -> HOL cls thry a
- printDebug :: String -> HOL cls thry a -> HOL cls thry a
- module HaskHOL.Core.State.Monad

# Stateful Type Primitives

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

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 IntSource

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 IntSource

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 ()Source

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 HOLTypeSource

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 HOLTypeSource

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)]Source

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 HOLTypeSource

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 ()Source

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 HOLTermSource

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 HOLTermSource

A version of `mkConst`

that accepts a triplet of type substitition
environments. Frequently used with the `typeMatch`

function.

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

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)]Source

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 HOLThmSource

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 HOLThmSource

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]Source

Retrieves the list of definitions from the current working theory. See
`newBasicDefinition`

for more details.

newBasicDefinition :: HOLTerm -> HOL Theory thry HOLThmSource

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)Source

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

Flag states whether or not to print debug statements.

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

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

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

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

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

# Monad Re-Export

module HaskHOL.Core.State.Monad