State.hs

{-# LANGUAGE PatternSynonyms, TypeFamilies #-}

{-|
  Module:    HaskHOL.Core.State
  Copyright: (c) The University of Kansas 2013
  LICENSE:   BSD3

  Maintainer:  ecaustin@ittc.ku.edu
  Stability:   unstable
  Portability: unknown

  This module exports the stateful layer of HaskHOL.  It consists of:

  * Stateful type primitives not found in "HaskHOL.Core.Types".

  * Stateful term primitives not found in "HaskHOL.Core.Terms".

  * Stateful theory extension primitives not found in "HaskHOL.Core.Kernel".

  * A very primitive debugging system.
-}
module HaskHOL.Core.State
    ( -- * Stateful Type Primitives
      types
    , tyDefinitions
    , getTypeArity
    , newType
    , mkType
    , mkFunTy
    -- * Stateful Term Primitives
    , constants
    , getConstType
    , newConstant
    , mkConst
    , mkConstFull
    , mkEq
    -- * Stateful Theory Extension Primitives
    , axioms
    , newAxiom
    , getAxiom
    , definitions
    , newBasicDefinition
    , getBasicDefinition
    , newBasicTypeDefinition
    , getBasicTypeDefinition
    -- * Primitive Debugging System
    , FlagDebug(..)
    , warn
    , printDebugLn
    , printDebug
      -- * Monad Re-Export
    , module HaskHOL.Core.State.Monad
    ) where

import HaskHOL.Core.Lib
import HaskHOL.Core.Kernel
import HaskHOL.Core.State.Monad

-- New flags and extensions
-- | Flag states whether or not to print debug statements.
newFlag "FlagDebug" True


data TypeConstants = TypeConstants !(Map Text TypeOp) deriving Typeable

deriveSafeCopy 0 'base ''TypeConstants

insertTypeConstant :: Text -> TypeOp -> Update TypeConstants ()
insertTypeConstant ty op =
    do TypeConstants m <- get
       put (TypeConstants (mapInsert ty op m))

getTypeConstants ::  Query TypeConstants (Map Text TypeOp)
getTypeConstants =
    do TypeConstants m <- ask
       return m

makeAcidic ''TypeConstants 
    ['insertTypeConstant, 'getTypeConstants]

initTypeConstants :: Map Text TypeOp
initTypeConstants = mapFromList [("bool", tyOpBool), ("fun", tyOpFun)]


data TypeDefinitions = TypeDefinitions !(Map Text (HOLThm, HOLThm)) 
    deriving Typeable

deriveSafeCopy 0 'base ''TypeDefinitions

insertTypeDefinition :: Text -> (HOLThm, HOLThm) -> Update TypeDefinitions ()
insertTypeDefinition ty defs =
    do TypeDefinitions m <- get
       put (TypeDefinitions (mapInsert ty defs m))

getTypeDefinitions :: Query TypeDefinitions (Map Text (HOLThm, HOLThm))
getTypeDefinitions  =
    do TypeDefinitions m <- ask
       return m

getTypeDefinition :: Text -> Query TypeDefinitions (Maybe (HOLThm, HOLThm))
getTypeDefinition lbl =
    do (TypeDefinitions m) <- ask
       return $! mapLookup lbl m 

makeAcidic ''TypeDefinitions 
    ['insertTypeDefinition, 'getTypeDefinitions, 'getTypeDefinition]


data TermConstants = TermConstants !(Map Text HOLTerm) deriving Typeable

deriveSafeCopy 0 'base ''TermConstants

insertTermConstant :: Text -> HOLTerm -> Update TermConstants ()
insertTermConstant tm op =
    do TermConstants m <- get
       put (TermConstants (mapInsert tm op m))

getTermConstants :: Query TermConstants (Map Text HOLTerm)
getTermConstants =
    do TermConstants m <- ask
       return m

makeAcidic ''TermConstants 
    ['insertTermConstant, 'getTermConstants]

initTermConstants :: Map Text HOLTerm
initTermConstants = mapFromList [("=", tmEq tyA)]

data TheAxioms = TheAxioms !(Map Text HOLThm) deriving Typeable

deriveSafeCopy 0 'base ''TheAxioms

insertAxiom :: Text -> HOLThm -> Update TheAxioms ()
insertAxiom lbl thm =
    do TheAxioms m <- get
       put (TheAxioms (mapInsert lbl thm m))

getAxioms :: Query TheAxioms (Map Text HOLThm)
getAxioms =
    do TheAxioms m <- ask
       return m

getAxiom' :: Text -> Query TheAxioms (Maybe HOLThm)
getAxiom' lbl =
    do TheAxioms m <- ask
       return $! mapLookup lbl m

makeAcidic ''TheAxioms ['insertAxiom, 'getAxioms, 'getAxiom']


data TheCoreDefinitions = 
    TheCoreDefinitions !(Map Text HOLThm) deriving Typeable

deriveSafeCopy 0 'base ''TheCoreDefinitions

insertCoreDefinition :: Text -> HOLThm -> Update TheCoreDefinitions ()
insertCoreDefinition lbl thm =
    do TheCoreDefinitions defs <- get
       put (TheCoreDefinitions (mapInsert lbl thm defs))

getCoreDefinitions :: Query TheCoreDefinitions [HOLThm]
getCoreDefinitions =
    do TheCoreDefinitions defs <- ask
       return $! mapElems defs

getCoreDefinition :: Text -> Query TheCoreDefinitions (Maybe HOLThm)
getCoreDefinition name =
    do (TheCoreDefinitions defs) <- ask
       return $! name `mapLookup` defs

makeAcidic ''TheCoreDefinitions 
    ['insertCoreDefinition, 'getCoreDefinitions, 'getCoreDefinition]


-- Stateful HOL Light Type Primitives
{-|
  Retrieves the 'Map' of type constants from the current working theory.  The
  mapping pairs strings recognized by the parser with the associated
  type operator value, i.e. 

  > ("bool", tyOpBool)
-}
types :: HOL cls thry (Map Text TypeOp)
types =
    do acid <- openLocalStateHOL (TypeConstants initTypeConstants)
       m <- queryHOL acid GetTypeConstants
       closeAcidStateHOL acid
       return m

-- | Retrieves the 'Map' of type definitions from the current working theory.
tyDefinitions :: HOL cls thry (Map Text (HOLThm, HOLThm))
tyDefinitions =
    do acid <- openLocalStateHOL (TypeDefinitions mapEmpty)
       m <- queryHOL acid GetTypeDefinitions
       closeAcidStateHOL acid
       return m

{-|
  Returns the arity associated with a type constant.
  Throws a 'HOLException' if the provided type constant
  name is not defined.
-}
getTypeArity :: Text -> HOL cls thry Int
getTypeArity name =
    do tys <- types
       liftMaybe ("getTypeArity: type " ++ show name ++ 
                  " has not been defined.") .
         liftM (snd . destTypeOp) $ mapLookup name tys

{- 
  Primitive type constant construction function.  Used by newType and 
  newBasicTypeDefinition.  Not exposed to the user.
-}
newType' :: Text -> TypeOp -> HOL Theory thry ()
newType' name tyop =
    do failWhen (can getTypeArity name) $
         "newType: type " ++ show name ++ " has already been declared."
       acid <- openLocalStateHOL (TypeConstants initTypeConstants)
       updateHOL acid (InsertTypeConstant name tyop)
       createCheckpointAndCloseHOL acid

{-| 
  Constructs a new primitve type constant of a given name and arity.  Also adds
  this new type to the current working theory.  Throws a 'HOLException' when a 
  type of the same name has already been declared.
-}
newType :: Text -> Int -> HOL Theory thry ()
newType name arity = 
    newType' name $ newPrimitiveTypeOp name arity

{-|
  Constructs a type application given an operator name and a list of argument
  types.  If the provided name is not a currently defined type constant then
  this function defaults it to a type operator variable.  Throws a 
  'HOLException' in the following cases:

  * A type operator's arity disagrees with the length of the argument list.

  * A type operator is applied to zero arguments.
-}
mkType :: Text -> [HOLType] -> HOL cls thry HOLType
mkType name args =
    do consts <- types
       case mapLookup name consts of
         Just tyOp -> tyApp tyOp args <#?> 
                        "mkType: type constructor application failed"
         Nothing -> 
           {- This seemed to be the easiest way to supress superfluous warnings
              when parsing type operators. -}
           do name' <- if textHead name == '_'
                       then return $! textTail name
                       else printDebugLn 
                              ("warning - mkType: type " ++ show name ++ 
                               " has not been defined.  Defaulting to type " ++ 
                               "operator variable.") $ 
                              return name
              failWhen (return $ null args)
                "mkType: type operator applied to zero args."
              tyApp (mkTypeOpVar name') args <#?> 
                "mkType: type operator variable application failed"

{-|
  Constructs a function type safely using 'mkType'.  Should never fail provided
  that the initial value for type constants has not been modified.
-}
mkFunTy :: HOLType -> HOLType -> HOL cls thry HOLType
mkFunTy ty1 ty2 = mkType "fun" [ty1, ty2]

-- State for Constants
{-|
  Retrieves the 'Map' of term constants from the current working theory.  The
  mapping pairs strings recognized by the parser and the associated
  term constant value, i.e. 

  > ("=", tmEq tyA)
-}
constants :: HOL cls thry (Map Text HOLTerm)
constants =
    do acid <- openLocalStateHOL (TermConstants initTermConstants)
       m <- queryHOL acid GetTermConstants
       closeAcidStateHOL acid
       return m

{-|
  Retrieves the type of a given term constant.  Throws a 'HOLException' if the
  provided term constant name is not defined.
-}
getConstType :: Text -> HOL cls thry HOLType
getConstType name =
    do consts <- constants
       liftMaybe "getConstType: not a constant name" .
         liftM typeOf $ mapLookup name consts

{-
  Primitive term constant construction function.  Used by newConstant,
  newBasicDefinition, and newBasicTypeDefinition.
-}
newConstant' :: Text -> HOLTerm -> HOL Theory thry ()
newConstant' name c =
    do failWhen (can getConstType name) $
         "newConstant: constant " ++ show name ++ " has already been declared."
       acid <- openLocalStateHOL (TermConstants initTermConstants)
       updateHOL acid (InsertTermConstant name c)
       createCheckpointAndCloseHOL acid

{-|
  Constructs a new primitive term constant of a given name and type.  Also adds
  this new term to the current working theory.  Throws a 'HOLException' when a
  term of the same name has already been declared.
-}
newConstant :: Text -> HOLType -> HOL Theory thry ()
newConstant name ty =
    do cond <- can getConstType name
       if cond
          then printDebugLn ("newConstant: ignoring redefintion of " ++ 
                             show name) $ return ()
          else newConstant' name $ newPrimitiveConst name ty

{-|
  Constructs a specific instance of a term constant when provided with its name
  and a type substition environment.  Throws a 'HOLException' in the 
  following cases:

  * The instantiation as performed by 'instConst' fails.

  * The provided name is not a currently defined constant.
-}
mkConst :: TypeSubst l r => Text -> [(l, r)] -> HOL cls thry HOLTerm
mkConst name tyenv =
    do consts <- constants
       tm <- liftMaybe "mkConst: not a constant name" $ 
               mapLookup name consts
       liftMaybe "mkConst: instantiation failed" $ 
         instConst tm tyenv

{-| 
  A version of 'mkConst' that accepts a triplet of type substitition 
  environments.  Frequently used with the 'typeMatch' function.
-}
mkConstFull :: Text -> SubstTrip -> HOL cls thry HOLTerm
mkConstFull name pat =
    do consts <- constants
       tm <- liftMaybe "mkConstFull: not a constant name" $
               mapLookup name consts
       liftMaybe "mkConstFull: instantiation failed" $ 
         instConstFull tm pat
                                    
{-| 
  Safely creates an equality between two terms using 'mkConst' using the type of
  the left hand side argument to perform the required instantiation.  Throws a
  'HOLException' in the case when the types of the two terms do not agree.
-}
mkEq :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm
mkEq l r =
    let ty = typeOf l in
      do eq <- mkConst "=" [(tyA, ty)]
         liftM1 mkComb (mkComb eq l) r <#?> "mkEq"

-- State for Axioms     

{-|
  Retrieves the list of axioms from the current working theory.  The list
  contains pairs of string names and the axioms.  This names exists such that
  compile time operations have a tag with which they can use to extract axioms 
  from saved theories.  See 'extractAxiom' for more details.
-}
axioms :: HOL cls thry (Map Text HOLThm)
axioms =        
    do acid <- openLocalStateHOL (TheAxioms mapEmpty)
       m <- queryHOL acid GetAxioms
       closeAcidStateHOL acid
       return m

{-| 
  Constructs a new axiom of a given name and conclusion term.  Also adds this
  new axiom to the current working theory.  Throws a 'HOLException' in the 
  following cases:

  * The provided term is not a proposition.

  * An axiom with the provided name has already been declared.
-}
newAxiom :: Text -> HOLTerm -> HOL Theory thry HOLThm
newAxiom name tm =
    do acid <- openLocalStateHOL (TheAxioms mapEmpty)
       qth <- queryHOL acid (GetAxiom' name)
       closeAcidStateHOL acid
       case qth of
         Just th -> 
             return th
         Nothing
             | typeOf tm /= tyBool -> 
                   fail "newAxiom: Not a proposition."
             | otherwise ->
                   let th = axiomThm tm in
                     do acid' <- openLocalStateHOL (TheAxioms mapEmpty)
                        updateHOL acid' (InsertAxiom name th)
                        createCheckpointAndCloseHOL acid'
                        return th
                   
 -- | Retrieves an axiom by label from the theory context.
getAxiom :: Text -> HOL cls thry HOLThm
getAxiom lbl =
    do acid <- openLocalStateHOL (TheAxioms mapEmpty)
       qth <- queryHOL acid (GetAxiom' lbl)
       closeAcidStateHOL acid
       liftMaybe ("getAxiom: axiom " ++ show lbl ++ " not found.") qth

-- State for Definitions
{-|
  Retrieves the list of definitions from the current working theory.  See
  'newBasicDefinition' for more details.
-}
definitions :: HOL cls thry [HOLThm]
definitions =
    do acid <- openLocalStateHOL (TheCoreDefinitions mapEmpty)
       m <- queryHOL acid GetCoreDefinitions
       closeAcidStateHOL acid
       return m

{-|
  Introduces a definition of the form @c = t@ into the current working theory.
  Throws a 'HOLException' when the definitional term is ill-formed.  See
  'newDefinedConst' for more details.
-}
newBasicDefinition :: Text -> HOLTerm -> HOL Theory thry HOLThm
newBasicDefinition lbl tm =
    getBasicDefinition lbl
    <|> case destEq tm of
          Just (Const _ _, _) ->
            fail "newBasicDefinition: constant already defined."
          Just (Var name _, _)
            | name /= lbl ->
                  fail $ "newBasicDefinition: provided label does not " ++
                         "match provided term."
            | otherwise ->
                  do (c@(Const x _), dth) <- liftEither "newBasicDefinition" $ 
                                               newDefinedConst tm
                     newConstant' x c
                     acid <- openLocalStateHOL (TheCoreDefinitions mapEmpty)
                     updateHOL acid (InsertCoreDefinition lbl dth)
                     createCheckpointAndCloseHOL acid
                     return dth
          _ -> fail "newBasicDefinition: provided term not an equation."
                    
-- | Retrieves a basic term definition by label from the theory context.
getBasicDefinition :: Text -> HOL cls thry HOLThm
getBasicDefinition lbl =
    do acid <- openLocalStateHOL (TheCoreDefinitions mapEmpty)
       qth <- queryHOL acid (GetCoreDefinition lbl)
       closeAcidStateHOL acid
       liftMaybe ("getBasicDefinition: definition for " ++ show lbl ++
                  " not found.") qth

{-|
  Introduces a new type constant, and two associated term constants, into the 
  current working theory that is defined as an inhabited subset of an existing 
  type constant.  Takes the following arguments:
  
  *  The name of the new type constant.

  *  The name of the new term constant that will be used to construct the type.

  *  The name of the new term constant that will be used to desctruct the type.

  *  A theorem that proves that the defining predicate has at least one
     satisfying value.

  Throws a 'HOLException' in the following cases:

  *  A term constant of either of the provided names has already been defined.

  *  A type constant of the provided name has already been defined.

  See 'newDefinedTypeOp' for more details.
-}
newBasicTypeDefinition :: Text -> Text -> Text -> HOLThm -> 
                          HOL Theory thry (HOLThm, HOLThm)
newBasicTypeDefinition tyname absname repname dth =
  do failWhen (return or <*> mapM (can getConstType) [absname, repname]) $
       "newBasicTypeDefinition: Constant(s) " ++ show absname ++ ", " ++ 
       show repname ++ " already in use."
     (atyop, a, r, dth1, dth2) <- liftEither "newBasicTypeDefinition" $
                                    newDefinedTypeOp tyname absname repname dth
     failWhen (canNot (newType' tyname) atyop) $
       "newBasicTypeDefinition: Type " ++ show tyname ++ " already defined."
     newConstant' absname a
     newConstant' repname r
     acid <- openLocalStateHOL (TypeDefinitions mapEmpty)
     updateHOL acid (InsertTypeDefinition tyname (dth1, dth2))
     createCheckpointAndCloseHOL acid
     return (dth1, dth2)

-- | Retrieves a basic type definition by label from the theory context.
getBasicTypeDefinition :: Text -> HOL cls thry (HOLThm, HOLThm)
getBasicTypeDefinition lbl =
    do acid <- openLocalStateHOL (TypeDefinitions mapEmpty)
       qth <- queryHOL acid (GetTypeDefinition lbl)
       closeAcidStateHOL acid
       liftMaybe ("getBasicTypeDefinition: definition for " ++ show lbl ++
                  " not found.") qth


-- Primitive Debugging Functions
{-| 
  Prints the provided string, with a new line, when the given boolean value is
  true.
-}
warn :: Bool -> String -> HOL cls thry ()
warn flag str = when flag $ putStrLnHOL str

{-|
  Prints the provided string, with a new line, when debugging is turned on, then
  returns the given 'HOL' computation.  A version of 'trace' for the 'HOL' monad
  that is referentially transparent.
-}
printDebugLn :: String -> HOL cls thry a -> HOL cls thry a
printDebugLn = printDebugBase putStrLnHOL

-- | A version of printDebug that does not print a new line.
printDebug :: String -> HOL cls thry a -> HOL cls thry a
printDebug = printDebugBase putStrHOL

-- Abstracted out for future flexibility.  Not exported.
printDebugBase :: (String -> HOL cls thry ()) -> String -> HOL cls thry a -> 
                  HOL cls thry a
printDebugBase fn str x =
    do debug <- getBenignFlag FlagDebug
       if debug
          then fn str >> x
          else x