State.hs

{-# LANGUAGE DeriveDataTypeable, TemplateHaskell, ViewPatterns #-}

{-|
  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            -- :: HOL cls thry [(String, TypeOp)]
    , getTypeArityCtxt -- :: HOLContext thry -> String -> Maybe Int
    , getTypeArity     -- :: String -> HOL cls thry Int
    , newType          -- :: String -> Int -> HOL Theory thry ()
    , mkType           -- :: String -> [HOLType] -> HOL cls thry HOLType
    , mkFunTy          -- :: HOLType -> HOLType -> HOL cls thry HOLType
    -- * Stateful Term Primitives
    , constants    -- :: HOL cls thry [(String, HOLTerm)]
    , getConstType -- :: String -> HOL cls thry HOLType
    , newConstant  -- :: String -> HOLType -> HOL Theory thry ()
    , mkConst      -- :: TypeSubst l r => 
                   --    String -> [(l, r)] -> HOL cls thry HOLTerm
    , mkConstFull  -- :: String -> SubstTrip -> HOL cls thry HOLTerm
    , mkEq         -- :: HOLTerm -> HOLTerm -> HOL cls thry HOLTerm
    -- * Stateful Theory Extension Primitives
    , axioms                 -- :: HOL cls thry [(String, HOLThm)]
    , getAxiom               -- :: String -> HOL cls thry HOLThm
    , newAxiom               -- :: String -> HOLTerm -> HOL Theory thry HOLThm
    , definitions            -- :: HOL cls thry [HOLThm]
    , newBasicDefinition     -- :: HOLTerm -> HOL Theory thry HOLThm
    , newBasicTypeDefinition -- :: String -> String -> String -> HOLThm -> 
                             --    HOL Theory thry (HOLThm, HOLThm)
    -- * Primitive Debugging System
    , FlagDebug(..)
    , warn         -- :: Bool -> String -> HOL cls thry ()
    , printDebugLn -- :: String -> HOL cls thry a -> HOL cls thry a
    , printDebug   -- :: String -> HOL cls thry a -> HOL cls thry a
      -- * 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

newExtension "TypeConstants" 
  [| [("bool", tyOpBool), ("fun", tyOpFun)] :: [(String, TypeOp)] |]

newExtension "TermConstants" [| [("=", tmEq tyA)] :: [(String, HOLTerm)] |]

newExtension "TheAxioms" [| [] :: [(String, HOLThm)] |]

{- 
  Extensible state type for term definitions introduced via 
  newBasicDefinition.
-}
newExtension "TheCoreDefinitions" [| [] :: [HOLThm] |]

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

  > ("bool", tyOpBool)
-}
types :: HOL cls thry [(String, TypeOp)]
types =
    do (TypeConstants tys) <- getExt
       return tys

-- needed for parser
{-| 
  Retrieves the arity of a given type constant.  Fails with 'Nothing' if the
  provided type constant name is not defined in the provided context.

  Note that this function takes a 'HOLContext' argument such that it can be
  used outside of 'HOL' computations; for example, in the parser.
-}
getTypeArityCtxt :: HOLContext thry -> String -> Maybe Int
getTypeArityCtxt ctx name =
    let (TypeConstants tys) = getExtCtxt ctx in
      do tyOp <- lookup name tys
         return . snd $ destTypeOp tyOp

{-|
  A version of 'getTypeArityCtxt' that operates over the current working theory
  of a 'HOL' computation.  Throws a 'HOLException' if the provided type constant
  name is not defined.
-}
getTypeArity :: String -> HOL cls thry Int
getTypeArity name =
    do ctxt <- get
       liftMaybe ("getTypeArity: type " ++ name ++ " has not been defined.") $
         getTypeArityCtxt ctxt name

{- 
  Primitive type constant construction function.  Used by newType and 
  newBasicTypeDefinition.  Not exposed to the user.
-}
newType' :: String -> TypeOp -> HOL Theory thry ()
newType' name tyop =
    do failWhen (can getTypeArity name) $
         "newType: type " ++ name ++ " has already been declared."
       modifyExt $ \ (TypeConstants consts) -> 
                       TypeConstants $ (name, tyop) : consts

{-| 
  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 :: String -> Int -> HOL Theory thry ()
newType name arity = 
    newType' name $ newPrimTypeOp 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 :: String -> [HOLType] -> HOL cls thry HOLType
mkType name args =
    do (TypeConstants consts) <- getExt
       case lookup name consts of
         Just tyOp -> liftEither "mkType: type constructor application failed" $
                        tyApp tyOp args
         Nothing -> 
           {- This seemed to be the easiest way to supress superfluous warnings
              when parsing type operators. -}
           do name' <- case name of
                         '_':x -> return x
                         _ -> printDebugLn 
                                ("warning - mkType: type " ++ name ++ " has " ++
                                 "not been defined.  Defaulting to type " ++ 
                                 "operator variable.") $ 
                                return name
              failWhen (return $ null args)
                "mkType: type operator applied to zero args."
              liftEither "mkType: type operator variable application failed" $ 
                tyApp (mkTypeOpVar name') args

{-|
  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 list of term constants from the current working theory.  The
  list contains pairs of strings recognized by the parser and the associated
  term constant value, i.e. 

  > ("=", tmEq tyA)
-}
constants :: HOL cls thry [(String, HOLTerm)]
constants =
    do (TermConstants consts) <- getExt
       return consts

{-|
  Retrieves the type of a given term constant.  Throws a 'HOLException' if the
  provided term constant name is not defined.
-}
getConstType :: String -> HOL cls thry HOLType
getConstType name =
    do (TermConstants consts) <- getExt
       tm <- liftMaybe "getConstType: not a constant name" $
               lookup name consts
       return $! typeOf tm

{-
  Primitive term constant construction function.  Used by newConstant,
  newBasicDefinition, and newBasicTypeDefinition.
-}
newConstant' :: String -> HOLTerm -> HOL Theory thry ()
newConstant' name c =
    do failWhen (can getConstType name) $
         "newConstant: constant " ++ name ++ " has already been declared."
       modifyExt $ \ (TermConstants consts) -> 
                       TermConstants $ (name, c) : consts

{-|
  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 :: String -> HOLType -> HOL Theory thry ()
newConstant name ty =
    newConstant' name $ newPrimConst 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 => String -> [(l, r)] -> HOL cls thry HOLTerm
mkConst name tyenv =
    do (TermConstants consts) <- getExt
       tm <- liftMaybe "mkConst: not a constant name" $ 
               lookup 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 :: String -> SubstTrip -> HOL cls thry HOLTerm
mkConstFull name pat =
    do (TermConstants consts) <- getExt
       tm <- liftMaybe "mkConstFull: not a constant name" $
               lookup 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)]
         liftEither "mkEq" $
           liftM1 mkComb (mkComb eq l) r

-- 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 [(String, HOLThm)]
axioms =	
    do (TheAxioms thms) <- getExt
       return thms

{-| 
  Retrieves a specific axiom by name.  Throws a 'HOLException' if there is no
  axiom with the provided name in the current working theory.
-}
getAxiom :: String -> HOL cls thry HOLThm
getAxiom lbl =
    do (TheAxioms thms) <- getExt
       liftMaybe "getAxiom: axiom name not found" $
         lookup lbl thms

{-| 
  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 :: String -> HOLTerm -> HOL Theory thry HOLThm
newAxiom name tm
    | typeOf tm /= tyBool = fail "newAxiom: Not a proposition."
    | otherwise =
        do failWhen (can getAxiom name) $ "newAxiom: axiom with name " ++ 
             name ++ " has already been declared."
           let th = axiomThm tm 
           modifyExt $ \ (TheAxioms axs) -> TheAxioms $ (name, th) : axs
           return th

-- 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 (TheCoreDefinitions defs) <- getExt
       return defs

{-|
  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 :: HOLTerm -> HOL Theory thry HOLThm
newBasicDefinition tm =
    do (c@(view -> Const name _ _), dth) <- liftEither "newBasicDefinition" $
                                              newDefinedConst tm
       newConstant' name c
       modifyExt $ \ (TheCoreDefinitions defs) -> 
                       TheCoreDefinitions $ dth : defs
       return dth

{-|
  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 :: String -> String -> String -> HOLThm -> 
                          HOL Theory thry (HOLThm, HOLThm)
newBasicTypeDefinition tyname absname repname dth =
  do failWhen (return or <*> mapM (can getConstType) [absname, repname]) $
       "newBasicTypeDefinition: Constant(s) " ++ absname ++ ", " ++ repname ++
         " already in use."
     (atyop, a, r, dth1, dth2) <- liftEither "newBasicTypeDefinition" $
                                    newDefinedTypeOp tyname absname repname dth
     failWhen (canNot (newType' tyname) atyop) $
       "newBasicTypeDefinition: Type " ++ tyname ++ " already defined."
     newConstant' absname a
     newConstant' repname r
     return (dth1, dth2)


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

deriveLiftMany [ ''TypeConstants, ''TermConstants
               , ''TheAxioms, ''TheCoreDefinitions ]