Prims.hs

{-# LANGUAGE DeriveDataTypeable, FlexibleInstances, MultiParamTypeClasses, 
             TemplateHaskell #-}

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

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

  This module defines the primitive data types for HaskHOL: 
  'HOLType', 'HOLTerm', and 'HOLThm'.

   Note:  This module is intended to be hidden by cabal to prevent manual, and 
   possibly unsound, construction of the primitive data types.  

   To include the contents of this module with the appropriate restrictions in 
   place, along with the entirey of the core system, import the "HaskHOL.Core"
   module.  Alternatively, the following modules also export individual
   primitive types with their associated restrictions:
   * "HaskHOL.Core.Types"  - Exports types
   * "HaskHOL.Core.Terms"  - Exports terms
   * "HaskHOL.Core.Kernel" - Exports theorems
-}

module HaskHOL.Core.Kernel.Prims
    ( -- * HOL types
      HOLType(..)
    , HOLTypeView(..)
    , TypeOp(..)
    , HOLTypeEnv
    , SubstTrip
      -- * HOL terms
    , HOLTerm(..)
    , HOLTermView(..)
    , ConstTag(..)
    , HOLTermEnv
      -- * HOL theorems
    , HOLThm(..)
    , HOLThmView(..)
      -- * The View pattern class
    , Viewable(..)
    ) where

import HaskHOL.Core.Lib

{-
  A quick note on how the primitive data types of HaskHOL are implemented -- 
  view patterns are used to simulate private data types for HOL types and 
  terms:
  * Internal constructors are hidden to prevent manual construction of terms.
 
  * View constructors (those of 'HOLTypeView', 'HOLTermView', and 'HOLThmView')
    are exposed to enable pattern matching. 
 
  * View patterns, as defined by instances of the 'view' function from the 
    @Viewable@ class, provide a conversion between the two sets of constructors.
-}

{-
  The following data types combined provide the definition of HOL types in 
  HaskHOL.

  The primary data type, 'HOLType', follows closely from the 
  simply typed lambda calculus approach used in John Harrison's HOL Light 
  system. 

  There are two principle changes to Harrison's implementation:
  1.  Type operators have been introduced, via the 'TypeOp' data type, to 
      facilitate a stateless logical kernel following from Freek Wiedijk's 
      Stateless HOL system.

  2.  Universal types and type operator variables have been introduced to move
      the logic from simply typed to polymorphic following from Norbert 
      Voelker's HOL2P system.
-}

{-|
  The 'HOLType' data type defines the internal constructors for HOL types in
  HaskHOL.  For more details, see the documentation for its view pattern data
  type, 'HOLTypeView'.
-}
data HOLType
    = TyVarIn !Bool !String
    | TyAppIn !TypeOp ![HOLType]
    | UTypeIn !HOLType !HOLType
    deriving (Eq, Ord, Typeable) 

-- | The view pattern data type for HOL types.
data HOLTypeView
    -- | A type variable consisting of a constraint flag and name.
    = TyVar Bool String
    {-| 
      A type application consisting of a type operator and a list of type
      arguments.  See 'TypeOp' for more details.
    -}
    | TyApp TypeOp [HOLType]
    {-| 
      A universal type consisting of a bound type and a body type.  Note that 
      the bound type must be a small, type variable.
    -}
    | UType HOLType HOLType

{-|
  The data type for type operators, 'TypeOp', is a mashing together of the
  representation of type operators from both both HOL2P and Stateless HOL.
  For more information regarding construction of the different operators, see
  the documentation of the following functions: 'mkTypeOpVar', 'newPrimTypeOp',
  'newDefinedTypeOp'
-}
data TypeOp 
    = TyOpVar !String
    | TyPrim !String !Int
    | TyDefined !String !Int !HOLThm
    deriving (Eq, Ord, Typeable)

{-
  In order to keep HaskHOL's type system decidable, we follow the same 
  \"smallness\" constraint used by HOL2P: type variables that are constrained 
  to be small cannot be replaced with types that contain either universal types
  or unconstrained type variables.  This constraint, in addition to the
  restriction that universal types can only bind small type variables, prevents
  the system from performing a substitution that would result in a higher rank
  type than the system is capable of dealing with.  This effectively limits the
  type system to 2nd order polymorphism.

  Voelker elected to rely on syntactic distinction to differentiate between the
  many kinds of type variables (small, unconstrained, and operator); depending 
  on how it was to be used, the name of a variable was prepended with a special 
  symbol.  Internal to HaskHOL, we elected to replace these syntactic 
  distinctions with structural ones such that the following hold true:

  * @TyVarIn True \"x\"@ represents the small type variable @\'x@
 
  * @TyVarIn False \"x\"@ represents the unconstrainted type variable @x@
 
  * @TyOpVar "x"@ represents the type operator variable @_x@

  Note that external to HaskHOL, during I/O of terms, both the parser and
  pretty-printer still rely on the syntactic distinctions introduced by
  Voelker.
-} 

-- | Type synonym for the commonly used, list-based, type environment.
type HOLTypeEnv = [(HOLType, HOLType)]

{-| 
  Type synonym for the commonly used triplet of substitution environments.
  See 'TypeSubst' for more information.
-}
type SubstTrip = (HOLTypeEnv, [(TypeOp, HOLType)], [(TypeOp, TypeOp)])

-- Viewable and Show instances for HOLType
instance Viewable HOLType HOLTypeView where
    view (TyVarIn b s) = TyVar b s
    view (TyAppIn tyop tys) = TyApp tyop tys
    view (UTypeIn v b) = UType v b

instance Show TypeOp where
    show (TyOpVar s) = '_' : s
    show (TyPrim s _) = s
    show (TyDefined s _ _) = s

{-
  The following data types combined provide the definition of HOL terms in 
  HaskHOL.

  Corresponding with the 'HOLType' data type, 'HOLTerm' follows closely from
  the definition of terms in HOL Light.  Again, the appropriate modifications
  have been made to facilitate a stateless and polymorphic term language.

  Most notably this includes:
  (1) The introduction of tags for constants to carry information formerly
      contained in the state.

  2.  Additional constructors have been added to 'HOLTerm' to facilitate
      term-level, type abstractions and applications.
-}

{-|
  The 'HOLTerm' data type defines the internal constructors for HOL terms in
  HaskHOL.  For more details, see the documentation for its view pattern data
  type, 'HOLTermView'.
-}
data HOLTerm
    = VarIn !String !HOLType
    | ConstIn !String !HOLType !ConstTag
    | CombIn !HOLTerm !HOLTerm
    | AbsIn !HOLTerm !HOLTerm
    | TyCombIn !HOLTerm !HOLType
    | TyAbsIn !HOLType !HOLTerm
    deriving (Eq, Ord, Typeable)

-- | The view pattern data type for HOL terms.
data HOLTermView
    -- | A term variable consisting of a name and type.
    = Var String HOLType
    {-| 
      A term constant consisting of a name, type, and tag.  See 'ConstTag' for 
      more information.
    -}
    | Const String HOLType ConstTag
    -- | A term application consisting of a function term and argument term.
    | Comb HOLTerm HOLTerm
    {-| 
      A term abstraction consisting of a bound term and a body term.  Note that
      the bound term must be a type variable.
    -}
    | Abs HOLTerm HOLTerm
    {-| 
      A term-level, type application consisting of a body term and an argument 
      type. Note that the body term must have a universal type.
    -}
    | TyComb HOLTerm HOLType
    {-| 
      A term-level, type abstraction consisting of a bound type and a body term.
      Note that the bound type must be a small, type variable.
    -}
    | TyAbs HOLType HOLTerm
   
{-| 
  The data type for constant tags, 'ConstTag', follows identically from the
  implementation in Stateless HOL.  For more information regarding construction
  of the different tags, see the documentation of the following functions:
  'newPrimConst', 'newDefinedConst', and 'newDefinedTypeOp'.
-}
data ConstTag
    = Prim
    | Defined !HOLTerm
    | MkAbstract !String !Int !HOLThm
    | DestAbstract !String !Int !HOLThm
    deriving (Eq, Ord, Typeable)

-- | Type synonym for the commonly used, list-based, term environment.
type HOLTermEnv = [(HOLTerm, HOLTerm)]

{- 
  The Viewable instance for terms.  
  Note that the Show instance for terms is more complicated than for types and, 
  as such, is included separately in the HaskHOL.Core.Printer module.
-}
instance Viewable HOLTerm HOLTermView where
    view (VarIn s ty) = Var s ty
    view (ConstIn s ty tag) = Const s ty tag
    view (CombIn l r) = Comb l r
    view (AbsIn v bod) = Abs v bod
    view (TyAbsIn tv tb) = TyAbs tv tb
    view (TyCombIn tm ty) = TyComb tm ty

{-| 
  The 'HOLThm' data type defines HOL Theorems in HaskHOL.  A theorem is defined
  simply as a list of assumption terms and a conclusion term.

  Note that this representation, in combination with a stateless 
  approach, means that the introduction of axioms is not tracked in the kernel.
  Axioms can be tracked once the stateful layer of the prover is introduced,
  though.  For more details see the documentation for `newAxiom`.
-}
data HOLThm = ThmIn ![HOLTerm] !HOLTerm
  deriving (Eq, Ord, Typeable)

-- | The view pattern data type for HOL theorems.
data HOLThmView = Thm [HOLTerm] HOLTerm

instance Viewable HOLThm HOLThmView where
  view (ThmIn asl c) = Thm asl c

{-| 
  The @Viewable@ class is used to provide a polymorphic view pattern for
  HaskHOL's primitive data types.
-}
class Viewable a b where
    {-| 
      The view pattern function for HaskHOL's primitive data types:
      
      * For types - Converts from 'HOLType' to 'HOLTypeView'.
      
      * For terms - Converts from 'HOLTerm' to 'HOLTermView'.

      * For theorems - Converts from 'HOLThm' to 'HOLThmView'.
    -}
    view :: a -> b

{- 
  Deepseq instances for the primitive data types.  These are included as they 
  are commonly used by a number of benchmarking libraries.
-}
instance NFData HOLType where
    rnf (TyVarIn b s) = rnf b `seq` rnf s
    rnf (TyAppIn s tys) = rnf s `seq` rnf tys
    rnf (UTypeIn tv tb) = rnf tv `seq` rnf tb

instance NFData TypeOp where
    rnf (TyOpVar s) = rnf s
    rnf (TyPrim s n) = rnf s `seq` rnf n
    rnf (TyDefined s n thm) = rnf s `seq` rnf n `seq` rnf thm

instance NFData HOLTerm where
    rnf (VarIn s ty) = rnf s `seq` rnf ty
    rnf (ConstIn s ty d) = rnf s `seq` rnf ty `seq` rnf d
    rnf (CombIn l r) = rnf l `seq` rnf r
    rnf (AbsIn bv bod) = rnf bv `seq` rnf bod
    rnf (TyAbsIn bty bod) = rnf bty `seq` rnf bod
    rnf (TyCombIn tm ty) = rnf tm `seq` rnf ty

instance NFData ConstTag where
    rnf Prim = ()
    rnf (Defined tm) = rnf tm
    rnf (MkAbstract s i thm) = rnf s `seq` rnf i `seq` rnf thm
    rnf (DestAbstract s i thm) = rnf s `seq` rnf i `seq` rnf thm

instance NFData HOLThm where
    rnf (ThmIn asl c) = rnf asl `seq` rnf c

{- 
  These are the automatically derived Lift instances for the primitive data
  types.  These instances are used by the compile-time operations found in
  the HaskHOL.Core.Protected module.
-}
$(deriveLiftMany [ ''TypeOp, ''HOLType
                 , ''ConstTag, ''HOLTerm
                 , ''HOLThm])