haskhol-core-1.1.0: src/HaskHOL/Core/State/Monad.hs
{-# LANGUAGE ConstraintKinds, DataKinds, EmptyDataDecls, ScopedTypeVariables,
TypeFamilies, TypeOperators, UndecidableInstances #-}
{-|
Module: HaskHOL.Core.State.Monad
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module exports the primitive types and combinators for the 'HOL'
computational monad. At a high level this monad is a newtype wrapper for a
limited 'IO' monad.
For higher level monadic combinators see the "HaskHOL.Core.State" and
"HaskHOL.Core.Basics" modules.
-}
module HaskHOL.Core.State.Monad
( -- * The 'HOL' Monad
HOL
, Theory
, Proof
, runHOLProof
, runHOL
-- * Theory Contexts
, TheoryPath
, mkTheoryPath
, destTheoryPath
, BaseThry(..)
, ExtThry(..)
, CtxtName(..)
, PolyTheory
, BaseCtxt
, ctxtBase
-- * Text Output Methods
, putStrHOL
, putStrLnHOL
-- * Exception Handling Methods
, HOLException(..)
, throwHOL
, catchHOL
, noteHOL
, liftMaybe
, liftEither
, finallyHOL
-- * Local Reference Methods
, HOLRef
, newHOLRef
, readHOLRef
, writeHOLRef
, modifyHOLRef
-- * Acid State Primitives
, openLocalStateHOL
, openLocalStateHOLBase
, closeAcidStateHOL
, createCheckpointAndCloseHOL
, cleanArchives
, updateHOL
, updateHOLUnsafe
, queryHOL
-- * Benign Flag Methods
, setBenignFlag
, unsetBenignFlag
, getBenignFlag
, newFlag
-- * Methods Related to Fresh Name Generation
, tickTermCounter
, tickTypeCounter
-- * Proof Caching
, cacheProof
, cacheProofs
, checkpointProofs
, cleanArchiveProofs
-- * Re-export for Extensible Exceptions
, Exception
) where
import HaskHOL.Core.Lib hiding (combine)
import HaskHOL.Core.Kernel.Prims
-- HOL Monad imports
import Data.Typeable
import Control.Exception (Exception)
import qualified Control.Exception as E
import Data.IORef
import GHC.Prim (Constraint)
import qualified Data.HashMap.Strict as Hash
import Data.Hashable
import Data.Acid hiding (makeAcidic, Query, Update)
-- TH imports
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (lift)
-- Path Handling imports
import Prelude hiding (FilePath)
import Paths_haskhol_core
import Shelly hiding (put, get)
import System.FilePath (combine)
-- Messy Template Haskell stuff
-- Proofs
data Proofs = Proofs !(Hash.HashMap String HOLThm) deriving Typeable
instance (SafeCopy a, SafeCopy b, Hashable a, Eq a) =>
SafeCopy (Hash.HashMap a b) where
getCopy = contain $ fmap Hash.fromList safeGet
putCopy = contain . safePut . Hash.toList
deriveSafeCopy 0 'base ''Proofs
insertProof :: String -> HOLThm -> Update Proofs ()
insertProof lbl thm =
do (Proofs m) <- get
put (Proofs (Hash.insert lbl thm m))
getProof :: String -> Query Proofs (Maybe HOLThm)
getProof lbl =
do (Proofs m) <- ask
return $! Hash.lookup lbl m
makeAcidic ''Proofs ['insertProof, 'getProof]
--
-- Types
data TyCounter = TyCounter !Integer deriving Typeable
deriveSafeCopy 0 'base ''TyCounter
updateTyCounter :: Update TyCounter Integer
updateTyCounter =
do TyCounter n <- get
let n' = succ n
put (TyCounter n')
return n'
queryTyCounter :: Query TyCounter Integer
queryTyCounter =
do TyCounter n <- ask
return n
makeAcidic ''TyCounter ['updateTyCounter, 'queryTyCounter]
--
-- Terms
data TmCounter = TmCounter !Integer deriving Typeable
deriveSafeCopy 0 'base ''TmCounter
updateTmCounter :: Update TmCounter Integer
updateTmCounter =
do TmCounter n <- get
let n' = succ n
put (TmCounter n')
return n'
queryTmCounter :: Query TmCounter Integer
queryTmCounter =
do TmCounter n <- ask
return n
makeAcidic ''TmCounter ['updateTmCounter, 'queryTmCounter]
--
-- Flags
data BenignFlags = BenignFlags !(Map String Bool) deriving Typeable
deriveSafeCopy 0 'base ''BenignFlags
insertFlag :: String -> Bool -> Update BenignFlags ()
insertFlag ty flag =
do BenignFlags m <- get
put (BenignFlags (mapInsert ty flag m))
lookupFlag :: String -> Query BenignFlags (Maybe Bool)
lookupFlag ty =
do BenignFlags m <- ask
return (mapLookup ty m)
makeAcidic ''BenignFlags ['insertFlag, 'lookupFlag]
--
--
-- Monad
-- HOL method types
{-|
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 a
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 type 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 essentially a newtype wrapper to a limited
'IO' monad. We say limited as we restrict the possible
IO-like computations to the ones exported in this module, rather than allowing
arbitrary computations through a mechanism like 'MonadIO'. This prevents a
number of soundness issues.
-}
newtype HOL cls thry a =
HOL { -- not exposed to the user
runHOLUnsafe :: AcidState Proofs -> String -> IO a
}
-- | The classification tag for theory extension computations.
data Theory
-- | The classification tag for proof computations.
data Proof
-- used internally by runHOLProof and runHOL
runHOLUnsafe' :: HOL cls thry a -> String -> IO a
runHOLUnsafe' m fp =
do dir <- getDataDir
acid <- openLocalStateFrom (dir `combine` "Proofs") (Proofs Hash.empty)
runHOLUnsafe m acid fp `E.finally` closeAcidState acid
{-|
Runs a 'HOL' 'Proof' computation using a provided 'TheoryPath' with access to
the proof cache. Other state values, e.g. type and term constants, may be
accessed but not modified.
-}
runHOLProof :: HOL Proof thry a -> TheoryPath thry -> IO a
runHOLProof m (TheoryPath fp) = runHOLUnsafe' m fp
{-|
Evaluates a 'HOL' computation by copying the contents of a provided
'TheoryPath' to a new directory where destructive updates will occur.
This is used primarily by 'extendTheory', but is also useful for testing
'Theory' computations in temporary directories.
-}
runHOL :: HOL cls thry a -> TheoryPath thry -> String -> IO a
runHOL m (TheoryPath old) new =
do dir <- getDataDir
let old' = mkFilePath $ dir `combine` old
new' = mkFilePath $ dir `combine` new
shelly $ do unlessM (test_d old') . fail $
"runHOL: acid-state directory, " ++
old ++ ", does not exist."
whenM (test_d new') . echo . pack $
"runHOL: acid-state directory, " ++
new ++ ", already exists. Overwriting."
rm_rf new'
cp_r old' new'
runHOLUnsafe' m new
instance Functor (HOL cls thry) where
fmap = liftM
instance Monad (HOL cls thry) where
return x = HOL $ \ _ _ -> return x
m >>= k = HOL $ \ acid st ->
do b <- runHOLUnsafe m acid st
runHOLUnsafe (k b) acid st
fail = throwHOL . HOLException
instance MonadPlus (HOL cls thry) where
mzero = fail "mzero - HOL"
mplus = (<||>)
instance Applicative (HOL cls thry) where
pure = return
(<*>) = ap
instance Alternative (HOL cls thry) where
empty = fail "empty - HOL"
(<|>) = (<||>)
instance Note (HOL cls thry) where
job <?> str = job <|> throwHOL (HOLException str)
-- Theory Contexts
{-|
A @newtype@ wrapper for the filepath to a theory context that uses a phantom
type variable to capture the theory context type. See 'HOL' for more
information.
-}
newtype TheoryPath thry = TheoryPath String
{-| Constructs a 'TheoryPath' for a provided theory context type using
'ctxtName'.
-}
mkTheoryPath :: forall thry. CtxtName thry => TheoryPath thry
mkTheoryPath = TheoryPath $ ctxtName (undefined :: thry)
-- | Destructs a 'TheoryPath', returning its internal 'String'.
destTheoryPath :: TheoryPath thry -> String
destTheoryPath (TheoryPath x) = x
-- converts TheoryPath strings to FilePaths for shelly
mkFilePath :: String -> FilePath
mkFilePath = fromText . pack
-- | The 'BaseThry' type is the type of the initial working theory.
data BaseThry = BaseThry
{-|
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.
-}
data ExtThry a b = ExtThry a b
{-|
The 'CtxtName' class associates a 'String' representation of context names
with context types. It's used internally for most Template Haskell primitives
defined in @HaskHOL.Core.Ext@ and its submodules.
-}
class CtxtName a where
-- | Returns the name of a context type.
ctxtName :: a -> String
{-|
The 'PolyTheory' type family is used to build a polymorphic theory context
constraint from a monomorphic theory context type. For example:
> type instance PolyTheory BoolType b = BaseCtxt b
Note: This will be automated and appropriately hidden in the future, but for
now it must be manually defined.
Be extra careful not to define incorrect instances as they can be used to
bypass the safety mechanisms of 'cacheProof' and 'cacheProofs'.
-}
type family PolyTheory a b :: Constraint
instance CtxtName BaseThry where
ctxtName _ = "BaseCtxt"
instance CtxtName a => CtxtName (ExtThry a b) where
ctxtName _ = ctxtName (undefined::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.
-}
type family BaseCtxt a :: Constraint where
BaseCtxt BaseThry = ()
BaseCtxt (ExtThry a b) = BaseCtxt b
-- type family stuff for base contexts
type instance PolyTheory BaseThry b = BaseCtxt b
type instance BaseThry == BaseThry = 'True
type instance ExtThry a b == ExtThry a' b' = (a == a') && (b == b')
-- | The 'TheoryPath' for the base theory context.
ctxtBase :: TheoryPath BaseThry
ctxtBase = mkTheoryPath
-- define own versions of IO functions so they can be used external to kernel
-- | A version of 'putStr' lifted to the 'HOL' monad.
putStrHOL :: String -> HOL cls thry ()
putStrHOL x = HOL $ \ _ _ -> putStr x
-- | A version of 'putStrLn' lifted to the 'HOL' monad.
putStrLnHOL :: String -> HOL cls thry ()
putStrLnHOL x = HOL $ \ _ _ -> putStrLn x
-- Errors
-- the basic HOL exception type
-- | The data type for generic errors in HaskHOL. Carries a 'String' message.
newtype HOLException = HOLException String deriving Typeable
instance Show HOLException where show (HOLException str) = str
instance Exception HOLException
{-|
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"
-}
throwHOL :: Exception e => e -> HOL cls thry a
throwHOL x = HOL $ \ _ _ -> E.throwIO x
{-|
A version of 'E.catch' lifted to the 'HOL' monad.
Note that 'mplus' and '<|>' are defined in terms of catching a
'E.SomeException' with 'catchHOL' and then ignoring it to run an alternative
computation instead.
-}
catchHOL :: Exception e => HOL cls thry a -> (e -> HOL cls thry a) ->
HOL cls thry a
catchHOL job errcase = HOL $ \ acid st ->
runHOLUnsafe job acid st `E.catch` \ e -> runHOLUnsafe (errcase e) acid st
-- Used to define mplus and (<|>) for the HOL monad. Not exposed to the user.
(<||>) :: HOL cls thry a -> HOL cls thry a -> HOL cls thry a
job <||> alt = HOL $ \ acid st ->
runHOLUnsafe job acid st `E.catch`
\ (_ :: E.SomeException) -> runHOLUnsafe alt acid st
-- | A version of 'note' specific to 'HOL' computations.
noteHOL :: String -> HOL cls thry a -> HOL cls thry a
noteHOL str m = HOL $ \ acid st ->
runHOLUnsafe m acid st `E.catch` \ (e :: E.SomeException) ->
case E.fromException e of
Just (HOLException str2) ->
E.throwIO . HOLException $ str ++ ": " ++ str2
_ -> E.throwIO . HOLException $ str ++ ": " ++ show e
{-|
Lifts a 'Maybe' value into the 'HOL' monad mapping 'Just's to 'return's and
'Nothing's to 'fail's with the provided 'String'.
-}
liftMaybe :: String -> Maybe a -> HOL cls thry a
liftMaybe _ (Just x) = return x
liftMaybe str _ = fail str
{-|
Lifts an 'Either' value into the 'HOL' monad mapping 'Right's to 'return's
and 'Left's to 'fail's.
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'.
-}
liftEither :: Show err => String -> Either err a -> HOL cls thry a
liftEither _ (Right res) = return res
liftEither str1 (Left str2) = fail $ str1 ++ ": " ++ show str2
-- | A version of 'E.finally' lifted to the 'HOL' monad.
finallyHOL :: HOL cls thry a -> HOL cls thry b -> HOL cls thry a
finallyHOL a b = HOL $ \ acid st ->
runHOLUnsafe a acid st `E.finally` runHOLUnsafe b acid st
-- Local vars
-- | A type synonym for 'IORef'.
type HOLRef = IORef
{-|
Creates a new 'HOLRef' from a given starting value. Functionally equivalent
to 'newIORef' lifted to the 'HOL' monad.
-}
newHOLRef :: a -> HOL cls thry (HOLRef a)
newHOLRef ref = HOL $ \ _ _ -> newIORef ref
{-|
Reads a 'HOLRef' returning the stored value. Functionally equivalent to
'readIORef' lifted to the 'HOL' monad.
-}
readHOLRef :: IORef a -> HOL cls thry a
readHOLRef ref = HOL $ \ _ _ -> readIORef ref
{-|
Writes a value to a 'HOLRef'. Functionally equivalent to 'writeHOLRef' lifted
to the 'HOL' monad.
-}
writeHOLRef :: IORef a -> a -> HOL cls thry ()
writeHOLRef ref x = HOL $ \ _ _ -> writeIORef ref x
{-|
Applies a given function to a 'HOLRef', modifying the stored value.
Functionally equivalent to 'modifyHOLRef' lifted to the 'HOL' monad.
-}
modifyHOLRef :: IORef a -> (a -> a) -> HOL cls thry ()
modifyHOLRef ref f = HOL $ \ _ _ -> modifyIORef ref f
-- acid primitives
-- used internally by openLocalStateHOL and openLocalStateHOLBase
openLocalState' :: (Typeable st, IsAcidic st)
=> st -> String -> IO (AcidState st)
openLocalState' ast suf =
do dir <- getDataDir
let dir' = dir `combine` suf `combine` show (typeOf ast)
openLocalStateFrom dir' ast
{-|
Creates an 'AcidState' value from a 'HOL' computation's theory context using
a default value.
This is a wrapper to 'openLocalStateFrom' using @HaskHOL.Core@'s
shared data directory appended with the 'ctxtName' of the theory context.
-}
openLocalStateHOL :: (Typeable st, IsAcidic st) => st
-> HOL cls thry (AcidState st)
openLocalStateHOL ast = HOL $ \ _ st -> openLocalState' ast st
{-|
A version of 'openLocalStateHOL' that uses just @HaskHOL.Core@'s shared data
directory.
-}
openLocalStateHOLBase :: (Typeable st, IsAcidic st) => st
-> HOL cls thry (AcidState st)
openLocalStateHOLBase ast = HOL $ \ _ _ -> openLocalState' ast ""
-- | A wrapper to 'closeAcidState' for the 'HOL' monad.
closeAcidStateHOL :: (SafeCopy st, Typeable st) => AcidState st
-> HOL cls thry ()
closeAcidStateHOL ast = HOL $ \ _ _ -> closeAcidState ast
{-|
A version of 'closeAcidStateHOL' that calls 'createCheckpoint' and
'createArchive' first. -}
createCheckpointAndCloseHOL :: (SafeCopy st, Typeable st) => AcidState st
-> HOL cls thry ()
createCheckpointAndCloseHOL ast = HOL $ \ _ _ ->
do createCheckpoint ast
createArchive ast
closeAcidState ast
{-|
The 'cleanArchives' method removes all of the "Archive" sub-directories
in a theory context that were created by 'createCheckpointAndCloseHOL'.
-}
cleanArchives :: HOL cls thry ()
cleanArchives = HOL $ \ _ st ->
do dir <- getDataDir
let dir' = mkFilePath $ dir `combine` st
shelly $ do archvs <- findWhen (\ x -> return $! x == "Archive") dir'
mapM_ rm_rf archvs
{-|
A wrapper to 'update' for the 'HOL' monad. Note that the classification of
the provided 'HOL' computation is unrestricted, such that it can be used in
'Proof' computations to update benign state values.
If you want the state modification to be captured by the type, make sure to
use 'updateHOL' instead.
-}
updateHOLUnsafe :: UpdateEvent event => AcidState (EventState event) -> event
-> HOL cls thry (EventResult event)
updateHOLUnsafe ast e = HOL $ \ _ _ -> update ast e
{-|
A version of 'updateHOLUnsafe' that restricts the classification of the
provided 'HOL' computation to be of a 'Theory' type.
-}
updateHOL :: UpdateEvent event => AcidState (EventState event) -> event
-> HOL Theory thry (EventResult event)
updateHOL = updateHOLUnsafe
-- | A wrapper to 'query' for the 'HOL' monad.
queryHOL :: QueryEvent event => AcidState (EventState event) -> event
-> HOL cls thry (EventResult event)
queryHOL ast e = HOL $ \ _ _ -> query ast e
-- Flag Methods
{-|
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 'getBenignFlagCtxt' and 'setBenignFlag' for more details.
-}
class Typeable a => BenignFlag a where
{-|
The intial value for a benign flag. The value returned when attempting to
retrieve a flag that is not yet defined in the context.
-}
initFlagValue :: a -> Bool
-- Benign Flag methods
-- Converts a flag's type to the string representation of its full name
tyToIndex :: forall a. Typeable a => a -> String
tyToIndex _ =
let con = typeRepTyCon $ typeOf (undefined::a) in
tyConPackage con ++ tyConModule con ++ tyConName con
-- used internally by set/unsetBenignFlag
modBenignFlag :: BenignFlag a => Bool -> a -> HOL cls thry ()
modBenignFlag val flag =
do acid <- openLocalStateHOL (BenignFlags mapEmpty)
updateHOLUnsafe acid (InsertFlag (tyToIndex flag) val)
closeAcidStateHOL acid
{-|
Adds a new, or modifies an existing, benign flag to be 'True'. Benign flags
in the context are stored as a 'Map' of 'Bool' values with 'String' keys.
The key is a term-level reificatino of a benign flag's type,
produced via a composition of 'show' and 'typeOf'.
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
witness, i.e. @undefined :: X@.
Example:
> setBenignFlag FlagDebug
would set the debugging flag equal to 'True'.
-}
setBenignFlag :: BenignFlag a => a -> HOL cls thry ()
setBenignFlag = modBenignFlag True
-- | Unsets a benign flag making it 'False'.
unsetBenignFlag :: BenignFlag a => a -> HOL cls thry ()
unsetBenignFlag = modBenignFlag False
{-|
Retrieves the value of a benign flag from a theory context.
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
getBenignFlag flag =
do acid <- openLocalStateHOL (BenignFlags mapEmpty)
val <- queryHOL acid (LookupFlag (tyToIndex flag))
closeAcidStateHOL acid
return $! fromMaybe (initFlagValue flag) val
-- Fresh Name Generation
{-|
Increments the term counter stored in the context, returning the new value.
-}
tickTermCounter :: HOL cls thry Integer
tickTermCounter =
do acid <- openLocalStateHOL (TmCounter 0)
n <- updateHOLUnsafe acid UpdateTmCounter
closeAcidStateHOL acid
return n
{-|
Increments the type counter stored in the context, returning the new value.
-}
tickTypeCounter :: HOL cls thry Integer
tickTypeCounter =
do acid <- openLocalStateHOL (TyCounter 0)
n <- updateHOLUnsafe acid UpdateTyCounter
closeAcidStateHOL acid
return n
{-|
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
-}
newFlag :: String -> Bool -> Q [Dec]
newFlag flag val =
do val' <- lift val
let name = mkName flag
ty = DataD [] name [] [NormalC name []] [''Typeable]
cls = InstanceD [] (AppT (ConT ''BenignFlag) (ConT name))
[FunD 'initFlagValue [Clause [WildP] (NormalB val') []]]
return [ty, cls]
-- Proof Caching
{-|
The 'cacheProof' method stores or retrieves a theorem from the proof
cache. For example:
> thmTRUTH :: BoolCtxt thry => HOL cls thry HOLThm
> thmTRUTH = cacheProof "thmTRUTH" ctxtBool $
> do tm <- toHTm [str| \p:bool. p |]
> tdef <- defT
> liftO . liftM1 primEQ_MP (ruleSYM tdef) $ primREFL tm
Note that 'cacheProof' takes three arguments:
* The label for the theorem. Note that these labels must be unique, such that
an attempt to store a theorem with a duplicate label will instead retrieve
the existing theorem. In the event that the existing theorem requires a
theory context that is not satisfied by the provided context, the
appropriate error will be thrown.
* The theory context required to successfully evaluate the proof of the
theorem. Note that this context only needs to satisfy the ascribed type
constraint, not "match" it. For example, one could define a set of contexts
that are identical modulo overload priorities. Selecting from this set on a
case by case basis can be used to eliminate a large number of type
annotations.
* The proof computation itself. Regardless of how the proof is provided as
an argument, be sure that it's type matches that of the type ascribed to
the call to 'cacheProof'.
-}
cacheProof :: PolyTheory thry thry' => String -> TheoryPath thry
-> HOL Proof thry HOLThm
-> HOL cls thry' HOLThm
cacheProof lbl (TheoryPath fp) prf = HOL $ \ acid _ ->
do qth <- query acid (GetProof lbl)
case qth of
Just th ->
return th
Nothing ->
do putStrLn ("proving: " ++ lbl)
th <- runHOLUnsafe prf acid fp
putStrLn (lbl ++ " proved.")
update acid (InsertProof lbl th)
return th
{-|
This is a version of 'cacheProof' that handles proof computations that return
multiple theorems. Essentially, it maps 'cacheProof' over
the list of labels, where each resultant computation retrieves only a single
theorem, but can store them all.
The decision to return a list of computations was inherited from a previous
implementation technique. It can result in some messy code when you want to
provide top-level names for each computation, but works fairly well otherwise.
-}
cacheProofs :: forall cls thry thry'. PolyTheory thry thry' => [String]
-> TheoryPath thry
-> HOL Proof thry [HOLThm]
-> [HOL cls thry' HOLThm]
cacheProofs lbls (TheoryPath fp) prf = map cacheProofs' lbls
where cacheProofs' :: String -> HOL cls thry' HOLThm
cacheProofs' lbl = HOL $ \ acid _ ->
do qth <- query acid (GetProof lbl)
case qth of
Just th ->
return th
Nothing ->
do qths <- liftM catMaybes $
mapM (query acid . GetProof) lbls
unless (null qths) . fail $
"cacheProofs: some provided labels clas with " ++
"existing theorems."
putStrLn ("proving: " ++ unwords lbls)
ths <- runHOLUnsafe prf acid fp
putStrLn (unwords lbls ++ " proved.")
when (length lbls /= length ths) . fail $
"cacheProofs: number of labels does not match " ++
"number of theorems."
mapM_ (\ (x, y) -> update acid (InsertProof x y)) $
zip lbls ths
let n = fromJust $ elemIndex lbl lbls
th = ths !! n
return th
{-|
Similar to 'createCheckpointAndCloseHOL', this method creates a checkpoint
and archive for the proofs cache specifically.
-}
checkpointProofs :: HOL cls thry ()
checkpointProofs = HOL $ \ acid _ ->
do createCheckpoint acid
createArchive acid
{-|
A version of 'cleanArchives' for the proofs cache specifically.
-}
cleanArchiveProofs :: HOL cls thry ()
cleanArchiveProofs = HOL $ \ _ _ ->
do dir <- liftM mkFilePath getDataDir
let dir' = dir </> ("Proofs" :: FilePath) </> ("Archive" :: FilePath)
shelly $ rm_rf dir'