HaskHOL.Core.Ext

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 HOLTerms.
• Methods related to compile time extension and caching of theory contexts.

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 where

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.

Associated Types

data PData a thry

Methods

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

Protects a value by sealing it against a provided context.

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

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

Instances

Protected HOLThm

Protected HOLTerm

Protected HOLType

type PType thry = PData HOLType thry

Type synonym for protected HOLTypes.

type PTerm thry = PData HOLTerm thry

Type synonym for protected HOLTerms.

type PThm thry = PData HOLThm thry

Type synonym for protected HOLThms.

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

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]

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]

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]

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]

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]

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 HOLTerms 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 -> QuasiQuoter

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.

base :: QuasiQuoter

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.

str :: QuasiQuoter

This is a specialized quasi-quoter for Strings. It can be used to strip white space and automatically escape special characters. It is typically used in conjunction with toHTm directly or indirectly.

Theory Extension Methods

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

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

Re-exports Q, Dec, and Exp for the purpose of writing type signatures external to this module.

module Language.Haskell.TH.Quote

Re-exports QuasiQuoter for the purpose of writing type signatures external to this module.