HaskHOL.Core.State.Monad

This module exports the primitive types and combinators for the HOL computational monad. At a high level this monad is a flattened stack of a State monad transformer and a limited IO monad.

For higher level monadic combinators see the HaskHOL.Core.State and HaskHOL.Core.Basics modules.

The HOL Monad

data HOL cls thry a

The HOL monad structures computations in the HaskHOL system at the stateful layer and above. The type parameters are used as such:

• cls - HOL computations are split into two classes, those that extend the current working theory and those that are "pure"-ly used for proof. The cls parameter is used to indicate the classification of a computation. It is a phantom type variable that is inhabited by one of two empty data types, Theory and Proof.
• thry - Carries a tag indicating the most recent checkpoint of the current working theory, i.e. the last library loaded. Again, it is phantom type variable that is inhabited by an empty data type. A unique tag is created for each library by linerearly extending the tag starting from a base value. For example, the tag ExtThry EqualThry BaseThry would indicate a current working theory consisting of the base and equality logic theories.

Note that typically this value is left polymorphic and is constrained by a class related to a library. For example, the following type indicates a computation that can only be ran by using a theory context value that has the equality logic library loaded: EqualCtxt thry => HOL cls thry a

• a - The return type of a HOL computation.

Note that the HOL monad is effectively a flattened stack of a limited IO monad and a State monad. We say limited as we restrict the possible IO-like computations to the ones shown in this module, rather than allowing arbitrary computations through a mechanism like MonadIO. This prevents a number of soundness issues.

For more information regarding the contents of a theory context see the documentation for HOLContext.

Instances

Monad (HOL cls thry)

Functor (HOL cls thry)

MonadPlus (HOL cls thry)

Applicative (HOL cls thry)

Alternative (HOL cls thry)

Note (HOL cls thry)

data Theory

The classification tag for theory extension computations.

data Proof

The classification tag for proof computations.

runHOLCtxt :: HOL cls thry a -> HOLContext thry -> IO (a, HOLContext thry)

Evaluates a HOL computation with a provided theory context. Returns the result paired with an updated theory context.

evalHOLCtxt :: HOL cls thry a -> HOLContext thry -> IO a

A version of runHOLCtxt that returns only the resultant value.

execHOLCtxt :: HOL cls thry a -> HOLContext thry -> IO (HOLContext thry)

A version of runHOLCtxt that returns only the theory context.

State Methods

get :: HOL cls thry (HOLContext thry)

Equivalent to get for the HOL monad. Note that we define our own version of this function, rather than define an instance of MonadState so that we can control where the morphisms are exported.

This is done in the name of soundness given that a user can inject an unsound theory context into a proof using a put morphism. This is analogous to the issue behind defining an instance of MonadIO given liftIO can be used to inject arbitrary computations into the HOL monad, including ones containing unsound contexts.

gets :: (HOLContext thry -> a) -> HOL cls thry a

A version of get that applies a function to the state before returning the result.

Text Output Methods

putStrHOL :: String -> HOL cls thry ()

A version of putStr lifted to the HOL monad.

putStrLnHOL :: String -> HOL cls thry ()

A version of putStrLn lifted to the HOL monad.

Exception Handling Methods

newtype HOLException

The data type for generic errors in HaskHOL. Carries a String message.

Constructors

HOLException String

Instances

Show HOLException

Typeable HOLException

Exception HOLException

throwHOL :: Exception e => e -> HOL cls thry a

A version of throwIO lifted to the HOL monad.

Note that the following functions for the HOL type rely on throwHOL:

• fail - Equivalent to

 throwHOL . HOLException

• mzero - Equivalent to

 fail "mzero - HOL"

• empty - Equivalent to

 fail "empty - HOL"

catchHOL :: Exception e => HOL cls thry a -> (e -> HOL cls thry a) -> HOL cls thry a

A version of catch lifted to the HOL monad.

Note that mplus and <|> are defined in terms of catching a SomeException with catchHOL and then ignoring it to run an alternative computation instead.

liftMaybe :: String -> Maybe a -> HOL cls thry a

Lifts a Maybe value into the HOL monad mapping Justs to returns and Nothings to fails with the provided String.

liftEither :: Show err => String -> Either err a -> HOL cls thry a

Lifts an Either value into the HOL monad mapping Rights to returns and Lefts to fails.

Note that the value inside the Left must have an instance of the Show class such that show can be used to construct a string to be used with fail.

Local Reference Methods

type HOLRef = IORef

A type synonym for IORef.

newHOLRef :: a -> HOL cls thry (HOLRef a)

Creates a new HOLRef from a given starting value. Functionally equivalent to newIORef lifted to the HOL monad.

readHOLRef :: IORef a -> HOL cls thry a

Reads a HOLRef returning the stored value. Functionally equivalent to readIORef lifted to the HOL monad.

writeHOLRef :: IORef a -> a -> HOL cls thry ()

Writes a value to a HOLRef. Functionally equivalent to writeHOLRef lifted to the HOL monad.

modifyHOLRef :: IORef a -> (a -> a) -> HOL cls thry ()

Applies a given function to a HOLRef, modifying the stored value. Functionally equivalent to modifyHOLRef lifted to the HOL monad.

Benign Flag Methods

class Typeable a => BenignFlag a where

HOL systems typically use a large number of boolean flags in order to direct system behavior, i.e. debug flags, warning flags, parser/printer flags, etc. These flags don't affect the underlying proof computations, hence their classification as benign, so we'd like to be able to toggle them on and off at will. Unfortunately, if we store them in the extensible state and use putExt or modifyExt we're limited to only being able to change them in Theory computations.

Instead, we include them in a separate part of the theory context where we can interact with them in any way we want without sacrificing the safety of the extensible state portion of the context.

The BenignFlag class works very similarly to the ExtClass class with the obvious exception that initial values are restricted to boolean values.

See HOLContext, getBenignFlagCtxt, and setBenignFlag for more details.

Methods

initFlagValue :: a -> Bool

The intial value for a benign flag. The value returned when attempting to retrieve a flag that is not yet defined in the context.

Instances

BenignFlag FlagDebug

BenignFlag FlagIgnoreConstVarstruct

BenignFlag FlagTyInvWarning

BenignFlag FlagTyOpInvWarning

BenignFlag FlagAddTyAppsAuto

BenignFlag FlagRevInterface

BenignFlag FlagPrintAllThm

setBenignFlag :: BenignFlag a => a -> HOL cls thry ()

Adds a new, or modifies an existing, benign flag to be True. Benign flags in the context are stored as a list of (String, Bool) pairs. The first field in this pair is a term-level reificatino of a benign flag's type, produced via a composition of show and typeOf. The second field is simply the current boolean value of the flag.

Numerous usage examples can be found in both the HaskHOL.Core.Parser.Lib and HaskHOL.Core.Printer modules where flags are used to direct the behavior of the parsers and printers accordingly.

Note that since the retrieval and storage of benign flags are driven by types, it is in the best interest of library implementors to guarantee that the types of their flags are unique. The easiest way to do this is to create a unique data type for each flag. The type doesn't need to carry a payload, but it does need to provide a witness to the flag type. As such, it can either be a nullary, punned data declaration, i.e. data X = X, or an empty data declaration with a type annotated instance of undefined acting as the ness, i.e. undefined :: X.

Example:

 setBenignFlag FlagDebug

would set the debugging flag equal to True.

Alternatively, the newFlag splice can be used to automatically construct a new extension given a name and initial value. See that function's documentation for more information.

unsetBenignFlag :: BenignFlag a => a -> HOL cls thry ()

Unsets a benign flag making it False.

getBenignFlagCtxt :: forall a thry. BenignFlag a => a -> HOLContext thry -> Bool

Retrieves the value of a benign flag from a theory context. This function is typically used external to HOL computations, such as in the parser and printer.

Note that retrieval of the value requires a witness to the desired flag's type, i.e.

 getBenignFlag FlagDebug

or

 getBenignFlag (undefined :: FlagDebug)

In the event that the flag is not found then the initFlagValue for that type is returned. Thus, this function never fails.

getBenignFlag :: BenignFlag a => a -> HOL cls thry Bool

A version of getBenignFlagCtxt that can be used with theory contexts passed implicitly as part of a HOL computation.

Never fails.

Methods Related to Fresh Name Generation

tickTermCounter :: HOL cls thry Int

Increments the term counter stored in the context, returning the new value. Can be used to guarantee the freshness of term names within a single computation.

tickTypeCounter :: HOL cls thry Int

Increments the type counter stored in the context, returning the new value. Can be used to gurantee the freshness of type names within a single computation.

Extensible State Methods

HaskHOL's extensible state mechanism is based closely on the implementation of extensible state found in XMonad.

In the event that the relevant documentation from ExtClass, putExt, and getExtCtxt is confusing or not sufficient, it may be helpful to review the documentation contained in the XMonad.Util.ExtensibleState module.

class (Lift a, Typeable a) => ExtClass a where

The ExtClass type class is the heart of HaskHOL's extensible state mechanism. It serves a number of purposes:

• It provides the polymorphic type for heterogenous structures of type ExtState.
• It introduces the Typeable constraint that enables the mechanism for selecting specific state extensions based on their type. See getExt for more details.
• It defines an initial value for state extensions to use if they have not been introduced to the context by a computation yet.

For more information see the documentation for HOLContext, getExtCtxt, and putExt.

Methods

initValue :: a

The intial value for an extensible state type. The value returned when attempting to retrieve a type that is not yet defined in the context.

data ExtState

Used to build heterogenous structures that hold state extensions. See ExtClass for more details.

Instances

Lift ExtState

putExt :: ExtClass a => a -> HOL Theory thry ()

Adds a new, or modifies an existing, state extension. State extensions in the context are stored as a list of (String, ExtState) pairs. The first field in this pair is a term-level reification of a state extension's type, produced via a composition of show and typeOf. The second field is simply a wrapping of the extension's value with ExtState to facilitate heterogeneous structures.

Numerous usage examples can be found in the HaskHOL.Core.Parser.Lib module where extensible state is used to store the list of operators, as well as other information, required by the parser.

Note that since the retrieval and storage of state extensions are driven by types, it is in the best interest of library implementors to guarantee that the type of their extensions are unique. The easiest way to do this is to create a newtype wrapper for your extension and hide the internal constructor to prevent unintended modification. Again, see HaskHOL.Core.Parser.Lib for usage examples.

Alternatively, the newExtension splice can be used to automatically construct a new extension given a name and initial value. See that function's documentation for more information.

getExtCtxt :: forall a thry. ExtClass a => HOLContext thry -> a

Retrives a state extension from a theory context. This function is typically used external to HOL computations, such as in the parser, where a theory context is passed explicitly as a value.

Note that the selection of the extension is driven by the return type of this function. Thus when binding the result of this function, the type must be fixed either via explicit type annotation or through the presence of a unique constructor.

In order to provide the correct result type, this function relies on the type-safe cast operation. In the event that either this cast fails or the state extension is not found then the initValue for that type is returned. Thus, this function never fails.

getExt :: ExtClass a => HOL cls thry a

A version of getExtCtxt that can be used with theory contexts passed implicitly as part of a HOL computation.

Never fails.

modifyExt :: ExtClass a => (a -> a) -> HOL Theory thry ()

Modifies the value of a state extension. Functionally equivalent to the composition

 \ f -> putExt . f =<< getExt

Implementation of Theory Contexts

data HOLContext thry

The state type for the HOL monad. A newtype wrapper to the following quad:

• An association List of (String, Bool) pairs that models HaskHOL's extensible benign flag system. The first field is a String representation of the type of a benign flag and the second field is that flag's current value.
• An Int counter that is used for fresh name generation for type variables.
• An Int counter that is used for fresh name generation for term variables.
• An association List of (String, ExtState) pairs that models HaskHOL's extensible state. The first field is a String representation of the type of a state extension and the second field is a wrapping of that type that has an instance of the ExtClass class.

See putExt and getExtCtxt for more details on how to interact with the extensible state and see setBenignFlag and getBenignFlag for more details on how to interact with benign flags.

Instances

Typeable1 HOLContext

Show (HOLContext thry)

Lift (HOLContext thry)

ctxtBase :: HOLContext BaseThry

The initial working theory value: debugging is on, the counters are at zero and the extensible state is empty.

data ExtThry a b

The ExtThry type is the type of a linear theory extension, i.e. a cons-like operation for theory types. See the module HaskHOL.Lib.Equal.Context for an example of how to correctly define theory types and contexts for a library.

Constructors

ExtThry a b

Instances

Typeable2 ExtThry

BaseCtxt b => BaseCtxt (ExtThry a b)

data BaseThry

The BaseThry type is the type of the initial working theory.

Constructors

BaseThry

Instances

Typeable BaseThry

BaseCtxt BaseThry

class BaseCtxt a

The BaseCtxt class is the context name associated with the BaseThry type, i.e. the constraint to be used to guarantee that the stateful kernel has been loaded. This should always be true.

Instances

BaseCtxt BaseThry

BaseCtxt b => BaseCtxt (ExtThry a b)

Template Haskell Assistance for Flags/Extensions

newFlag :: String -> Bool -> Q [Dec]

The newFlag splice can be used to automatically construct a new benign flag given a name and an initial flag value.

Example:

 newFlag "FlagDebug" True

will construct the following Haskell code:

 data FlagDebug = FlagDebug deriving Typeable
 instance BenignFlag FlagDebug where
     initFlagValue _ = True

newExtension :: String -> ExpQ -> Q [Dec]

The newExtension splice can be used to automatically construct a new state extension given a name and a quoted, type annotated, initial value. The type annotation is required as many initial values, such as an empty list, are too polymorphic to infer the correct type on its own.

Example:

 newExtension "TheCoreDefinitions" [| [] :: [HOLThm] |]

will construct the following Haskell code:

 newtype TheCoreDefinitions = TheCoreDefinitions [HOLThm] deriving Typeable
 instance ExtClass TheCoreDefinitions where
     initValue = TheCoreDefinitions []

Note that, due to limitations with the current version of Template Haskell, Lift instances should be derived external to this splice via deriveLift or deriveLiftMany.

Re-export for Extensible Exceptions

class (Typeable e, Show e) => Exception e

Any type that you wish to throw or catch as an exception must be an instance of the Exception class. The simplest case is a new exception type directly below the root:

 data MyException = ThisException | ThatException
     deriving (Show, Typeable)

 instance Exception MyException

The default method definitions in the Exception class do what we need in this case. You can now throw and catch ThisException and ThatException as exceptions:

*Main> throw ThisException `catch` \e -> putStrLn ("Caught " ++ show (e :: MyException))
Caught ThisException

In more complicated examples, you may wish to define a whole hierarchy of exceptions:

 ---------------------------------------------------------------------
 -- Make the root exception type for all the exceptions in a compiler

 data SomeCompilerException = forall e . Exception e => SomeCompilerException e
     deriving Typeable

 instance Show SomeCompilerException where
     show (SomeCompilerException e) = show e

 instance Exception SomeCompilerException

 compilerExceptionToException :: Exception e => e -> SomeException
 compilerExceptionToException = toException . SomeCompilerException

 compilerExceptionFromException :: Exception e => SomeException -> Maybe e
 compilerExceptionFromException x = do
     SomeCompilerException a <- fromException x
     cast a

 ---------------------------------------------------------------------
 -- Make a subhierarchy for exceptions in the frontend of the compiler

 data SomeFrontendException = forall e . Exception e => SomeFrontendException e
     deriving Typeable

 instance Show SomeFrontendException where
     show (SomeFrontendException e) = show e

 instance Exception SomeFrontendException where
     toException = compilerExceptionToException
     fromException = compilerExceptionFromException

 frontendExceptionToException :: Exception e => e -> SomeException
 frontendExceptionToException = toException . SomeFrontendException

 frontendExceptionFromException :: Exception e => SomeException -> Maybe e
 frontendExceptionFromException x = do
     SomeFrontendException a <- fromException x
     cast a

 ---------------------------------------------------------------------
 -- Make an exception type for a particular frontend compiler exception

 data MismatchedParentheses = MismatchedParentheses
     deriving (Typeable, Show)

 instance Exception MismatchedParentheses where
     toException   = frontendExceptionToException
     fromException = frontendExceptionFromException

We can now catch a MismatchedParentheses exception as MismatchedParentheses, SomeFrontendException or SomeCompilerException, but not other types, e.g. IOException:

*Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: MismatchedParentheses))
Caught MismatchedParentheses
*Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeFrontendException))
Caught MismatchedParentheses
*Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeCompilerException))
Caught MismatchedParentheses
*Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: IOException))
*** Exception: MismatchedParentheses

Instances

Exception PatternMatchFail

Exception RecSelError

Exception RecConError

Exception RecUpdError

Exception NoMethodError

Exception NonTermination

Exception NestedAtomically

Exception SomeException

Exception ErrorCall

Exception ArithException

Exception HOLException