haskhol-core-1.0.0: src/HaskHOL/Core/Ext/Protected.hs
{-# LANGUAGE ExistentialQuantification, FlexibleInstances,
FunctionalDependencies, MultiParamTypeClasses, ScopedTypeVariables,
TemplateHaskell, TypeFamilies, TypeSynonymInstances,
UndecidableInstances, ViewPatterns #-}
{-|
Module: HaskHOL.Core.Ext.Protected
Copyright: (c) The University of Kansas 2013
LICENSE: BSD3
Maintainer: ecaustin@ittc.ku.edu
Stability: unstable
Portability: unknown
This module defines a mechanism for sealing and unsealing values against a
given context. Additionally, a number of compile time operations are
provided that leverage this technique as an example of how it can be used.
The basic goal behind the content of this module 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.
-}
module HaskHOL.Core.Ext.Protected
( Protected(protect, serve)
, PData
, PType
, PTerm
, PThm
, 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]
) where
import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel hiding (typeOf)
import HaskHOL.Core.State
import HaskHOL.Core.Parser
import Data.Typeable (typeOf, typeRepArgs)
import Language.Haskell.TH
import Language.Haskell.TH.Syntax (Lift(..))
-- protected values
{-|
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.
-}
class Lift a => Protected a where
data PData a thry
-- | Protects a value by sealing it against a provided context.
protect :: HOLContext thry -> a -> PData a thry
{-|
Unseals a protected value, returning it in a monadic computation whose
current working theory satisfies the context that the value was originally
sealed with.
-}
serve :: PData a thry -> HOL cls thry a
liftTy :: a -> Name
protLift :: PData a thry -> Q Exp
instance Protected HOLThm where
data PData HOLThm thry = PThm HOLThm
protect _ = PThm
serve (PThm thm) = return thm
liftTy _ = ''HOLThm
protLift (PThm thm) = conE 'PThm `appE` lift thm
-- | Type synonym for protected 'HOLThm's.
type PThm thry = PData HOLThm thry
instance Protected HOLTerm where
data PData HOLTerm thry = PTm HOLTerm
protect _ = PTm
serve (PTm tm) = return tm
liftTy _ = ''HOLTerm
protLift (PTm tm) = conE 'PTm `appE` lift tm
-- | Type synonym for protected 'HOLTerm's.
type PTerm thry = PData HOLTerm thry
instance Protected HOLType where
data PData HOLType thry = PTy HOLType
protect _ = PTy
serve (PTy ty) = return ty
liftTy _ = ''HOLType
protLift (PTy ty) = conE 'PTy `appE` lift ty
-- | Type synonym for protected 'HOLType's.
type PType thry = PData HOLType thry
instance HOLTermRep (PTerm thry) thry where
toHTm = serve
instance HOLTypeRep (PType thry) thry where
toHTy = serve
{-
Builds the theory contrainst for a lifted, protected value.
For example:
> buildThryType (x::PData a Bool)
builds the context
> forall thry. BoolCtxt thry => PData a thry
-}
buildThryType :: forall a thry. (Protected a, Typeable thry) =>
PData a thry -> Type
buildThryType _ =
let tyname = mkName "thry"
ctxtName = mkName $ topTheory ++ "Ctxt"
cls = ClassP ctxtName [VarT tyname] in
ForallT [PlainTV tyname] [cls] .
AppT (AppT (ConT ''PData) . ConT $ liftTy (undefined :: a)) $
VarT tyname
where topTheory :: String
topTheory =
let base = show . head . typeRepArgs $ typeOf (undefined :: thry) in
take (length base - 4) base
{-|
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 |]
-}
liftProtectedExp :: (Protected a, Typeable thry) =>
PData a thry -> Q Exp
liftProtectedExp pdata =
do pdata' <- protLift pdata
let ty = buildThryType pdata
return $! SigE pdata' ty
{-|
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.
-}
liftProtected :: (Protected a, Typeable thry) =>
String -> PData a thry -> Q [Dec]
liftProtected lbl pdata =
do pdata' <- protLift pdata
let ty = buildThryType pdata
name = mkName lbl
tysig = SigD name ty
dec = ValD (VarP name) (NormalB pdata') []
return [tysig, dec]
-- Compile Time Proof
--EvNote: long-term idea: change debuging printing to be based on cabal flag
{-|
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.
-}
proveCompileTime :: Typeable thry => HOLContext thry -> String ->
HOL Proof thry HOLThm -> Q [Dec]
proveCompileTime ctx lbl th =
do thm <- runIO $
do putStr $ "proving: " ++ lbl ++ "..."
thm <- evalHOLCtxt (setBenignFlag FlagDebug >> th) ctx
putStrLn "...proved."
return thm
liftProtected lbl $ protect ctx thm
{-|
A version of 'proveCompileTime' that works for a proof computation returning
multiple theorems.
Note that each resultant theorem must have a unique, provided name.
-}
proveCompileTimeMany :: Typeable thry => HOLContext thry -> [String] ->
HOL Proof thry [HOLThm] -> Q [Dec]
proveCompileTimeMany ctx lbls ths =
let n = length lbls in
do thms <- runIO $
do putStrLn $ "proving " ++ show n ++ " theorems"
thms <- evalHOLCtxt (setBenignFlag FlagDebug >> ths) ctx
if length thms /= n
then fail $ "proveCompileTimeMany: number of " ++
"theorems and labels does not agree."
else do putStrLn $ unwords lbls ++ " proved."
return thms
liftM concat . mapM (\ (lbl, thm) -> liftProtected lbl $
protect ctx thm) $ zip lbls thms
-- Extraction functions for Core State values
{-|
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) @
-}
extractBasicDefinition :: Typeable thry =>
HOLContext thry -> String -> String -> Q [Dec]
extractBasicDefinition ctx lbl name =
do defns <- runIO $ evalHOLCtxt definitions ctx
let mb = find (\ x -> case destEq $ concl x of
Just (view -> Const l _ _, _) -> l == name
_ -> False) defns
case mb of
Nothing -> fail "extractBasicDefinition: definition not found"
Just th -> liftProtected lbl $ protect ctx th
{-|
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'.
-}
extractAxiom :: Typeable thry => HOLContext thry -> String -> Q [Dec]
extractAxiom ctx lbl =
do ax <- runIO $ evalHOLCtxt
(getAxiom lbl <?> "extractAxiom: axiom not found") ctx
liftProtected lbl $ protect ctx ax