{-# 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