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

Stability | unstable |

Maintainer | ecaustin@ittc.ku.edu |

Safe Haskell | None |

This module exports HaskHOL's non-trivial extensions to the underlying HOL system, i.e. the compile time operations. These operations are split into three categories:

- Methods related to the Protect and Serve Mechanism for sealing and unsealing data against a provided theory context.
- Methods related to quasi-quoting of
`HOLTerm`

s. - Methods related to compile time extension and caching of theory contexts.

- class Lift a => Protected a where
- type PType thry = PData HOLType thry
- type PTerm thry = PData HOLTerm thry
- type PThm thry = PData HOLThm thry
- liftProtectedExp :: (Protected a, Typeable thry) => PData a thry -> Q Exp
- liftProtected :: (Protected a, Typeable thry) => String -> PData a thry -> Q [Dec]
- proveCompileTime :: Typeable thry => HOLContext thry -> String -> HOL Proof thry HOLThm -> Q [Dec]
- proveCompileTimeMany :: Typeable thry => HOLContext thry -> [String] -> HOL Proof thry [HOLThm] -> Q [Dec]
- extractBasicDefinition :: Typeable thry => HOLContext thry -> String -> String -> Q [Dec]
- extractAxiom :: Typeable thry => HOLContext thry -> String -> Q [Dec]
- baseQuoter :: Typeable thry => HOLContext thry -> QuasiQuoter
- base :: QuasiQuoter
- str :: QuasiQuoter
- extendCtxt :: Typeable thry => HOLContext thry -> HOL cls thry () -> String -> Q [Dec]
- module Language.Haskell.TH
- module Language.Haskell.TH.Quote

# Protected Data Methods

The basic goal behind the Protect and Serve mechanism is to recapture some of
the efficiency lost as a result of moving from an impure, interpretted host
language to a pure, compiled one. We do this by forcing the evaluation of
large computations, usually proofs, such that they are only run once. To
maintain soundness of our proof system, we must track what information
was used to force the computation and guarantee that information is present
in all cases where this new value is to be used. This is the purpose of the
`Protected`

class and the `liftProtectedExp`

and `liftProtected`

methods.

class Lift a => Protected a whereSource

The Protected class is the associated type class that facilitates our protect/serve protection mechanism.

It defines:

- A data wrapper for our protected type.
- Conversions to/from this new type, protect and serve.
- Some boilerplate code to enable template haskell lifting.

protect :: HOLContext thry -> a -> PData a thrySource

Protects a value by sealing it against a provided context.

serve :: PData a thry -> HOL cls thry aSource

Unseals a protected value, returning it in a monadic computation whose current working theory satisfies the context that the value was originally sealed with.

liftProtectedExp :: (Protected a, Typeable thry) => PData a thry -> Q ExpSource

Lifts a protected data value as an expression using an ascribed type. For example:

liftProtectedExp (x::PData a Bool)

produces the following spliceable expression

[| x :: forall thry. BoolCtxt thry => PData a Bool |]

liftProtected :: (Protected a, Typeable thry) => String -> PData a thry -> Q [Dec]Source

Lifts a protected data value as a declaration of a given name with an ascribed type signature. For example:

liftProtected "protX" (x::PData a Bool)

produces the following list of spliceable declarations

[ [d| protX :: forall thry. BoolCtxt thry => PData a Bool |] , [d| protX = x |] ]

See `extractAxiom`

for a basic example of how this function may be used.

proveCompileTime :: Typeable thry => HOLContext thry -> String -> HOL Proof thry HOLThm -> Q [Dec]Source

Evaluates a proof compilation, protects it with the theory used to evaluate it, and then lifts it as a declaration of a given name with an ascribed type signature.

Relies internally on `protect`

and `liftProtected`

to guarantee that the
resultant theorem is sealed with the right type.

proveCompileTimeMany :: Typeable thry => HOLContext thry -> [String] -> HOL Proof thry [HOLThm] -> Q [Dec]Source

A version of `proveCompileTime`

that works for a proof computation returning
multiple theorems.

Note that each resultant theorem must have a unique, provided name.

extractBasicDefinition :: Typeable thry => HOLContext thry -> String -> String -> Q [Dec]Source

Extracts a basic term definition from a provided context, protecting and
lifting it with `liftProtected`

. The extraction is performed by looking for
a definition whose left hand side matches a provided constant name.
For example:

extractBasicDefinition ctxtBool "defT" "T"

will return the spliceable list of declarations for the following theorem

|- T = ( p:bool . p) = ( p:bool . p)

extractAxiom :: Typeable thry => HOLContext thry -> String -> Q [Dec]Source

Extracts an axiom from a provided context, protecting and lifting it with
`liftProtected`

. The extraction is performed by looking for an axioms of
a given name, as specified when the axiom was created with `newAxiom`

.

# Quasi-Quoter Methods

Quasi-quoting provides a way to parse `HOLTerm`

s at compile time safely.
Just as with proofs, we seal these terms against the theory context used to
parse them with `protect`

and `serve`

to preserve soundness. See the
documentation for `base`

for a brief discussion on when quasi-quoting should
be used vs. `toHTm`

.

baseQuoter :: Typeable thry => HOLContext thry -> QuasiQuoterSource

This is the base quasi-quoter for the HaskHOL system. When provided with a
theory context value, it constucts a theory specific quasi-quoter that parses
a `String`

as a term, protecting and lifting the result.

Note that, at this point in time, we only allowing quoting at the expression level.

An instance of `baseQuoter`

for the core theory context, `ctxtBase`

.
Example:

[base| x = y |]

will parse the provided string and construct the `HOLTerm`

`x = y`

at compile
time. Note that this term is protected, such that it has to be accessed via
`serve`

. This is advantageous in computations that may be run many times,
for example:

do tm <- serve [base| x = y |] ...

will parse the term exactly once, only checking the `thry`

tag of the
computation for each evaluation. Conversely,

do tm <- toHTm "x = y" ...

will parse the term for every evaluation of that computation. Generally, the
use of `toHTm`

is reserved for run time parsing and in larger computations
that themselves are evaluated at copmile time to minimize the amount of work
Template Haskell has to do.

# Theory Extension Methods

extendCtxt :: Typeable thry => HOLContext thry -> HOL cls thry () -> String -> Q [Dec]Source

Extends a theory by evaluating a provided computation, returning a list of declarations containing:

- A new empty data declaration associated with the new theory.
- A new type class associated with the new theory to be used with
`DerivedCtxt`

along with the appropriate instances. - The context value for the new theory.
- A class constraint alias that can be safely exported for use in type signatures external to the library where it was defined.
- A quasiquoter for the new theory.
- A compile-time proof function for the new theory.

For example:

extendCtxt ctxtBase loadBoolLib "bool"

will produce the following code

data BoolThry deriving Typeable type BoolType = ExtThry BoolThry BaseThry class BaseCtxt a => BoolContext a instance BaseCtxt b => BoolContext (ExtThry BoolThry b) instance BoolContext b => BoolContext (ExtThry a b) class BoolContext a => BoolCtxt a instance BoolContext a => BoolCtxt a ctxtBool :: HOLContext BoolType ctxtBool = ... bool :: QuasiQuoter bool = baseQuoter ctxtBool proveBool :: String -> HOL Proof BoolType HOLThm -> Q [Dec] proveBool = proveCompileTime ctxtBool proveBoolMany :: [String] -> HOL Proof BoolType [HOLThm] -> Q [Dec] proveBoolMany = proveCompileTimeMany ctxtBool

# Template Haskell Re-Exports

module Language.Haskell.TH

module Language.Haskell.TH.Quote

Re-exports `QuasiQuoter`

for the purpose of writing type signatures
external to this module.