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
- 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
The Protected class is the associated type class that facilitates our protect/serve protection mechanism.
- A data wrapper for our protected type.
- Conversions to/from this new type, protect and serve.
- Some boilerplate code to enable template haskell lifting.
Protects a value by sealing it against a provided context.
Unseals a protected value, returning it in a monadic computation whose current working theory satisfies the context that the value was originally sealed with.
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 |]
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 |] ]
extractAxiom for a basic example of how this function may be used.
A version of
proveCompileTime that works for a proof computation returning
Note that each resultant theorem must have a unique, provided name.
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.
extractBasicDefinition ctxtBool "defT" "T"
will return the spliceable list of declarations for the following theorem
|- T = ( p:bool . p) = ( p:bool . p)
Quasi-quoting provides a way to parse
HOLTerms at compile time safely.
Just as with proofs, we seal these terms against the theory context used to
parse them with
serve to preserve soundness. See the
base for a brief discussion on when quasi-quoting should
be used vs.
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
String as a term, protecting and lifting the result.
Note that, at this point in time, we only allowing quoting at the expression level.
[base| x = y |]
will parse the provided string and construct the
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,
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
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
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
DerivedCtxtalong 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.
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
QuasiQuoter for the purpose of writing type signatures
external to this module.