Initial move from public to private repo.

HaskHOL-Deductive.cabal

@@ -0,0 +1,78 @@
+name:          haskhol-deductive
+version:       0.1.0
+synopsis:      HaskHOL libraries for higher level deductive reasoning.
+description:   More details can be found at the following page:  
+               http://haskhol.org. 
+license:       BSD3
+license-file:  LICENSE
+author:        Evan Austin <[email protected]>
+maintainer:    Evan Austin <[email protected]>
+category:      Theorem Provers
+cabal-version: >=1.18
+build-type:    Simple
+stability:     experimental
+homepage:      http://haskhol.org
+
+library
+    default-language:  Haskell2010
+    default-extensions: ConstraintKinds, DeriveDataTypeable, OverloadedStrings,
+                        QuasiQuotes, TemplateHaskell, TypeFamilies
+    build-depends:   base >= 4.7
+                   , template-haskell >= 2.9
+                   , pretty >= 1.1
+                   , haskhol-core >= 1.1
+
+    exposed-modules:
+      HaskHOL.Deductive
+      HaskHOL.Lib.Equal
+      HaskHOL.Lib.Bool
+      HaskHOL.Lib.DRule
+      HaskHOL.Lib.Tactics
+      HaskHOL.Lib.Itab
+      HaskHOL.Lib.Simp
+      HaskHOL.Lib.Theorems
+      HaskHOL.Lib.IndDefs
+      HaskHOL.Lib.Classic
+      HaskHOL.Lib.Trivia
+      HaskHOL.Lib.Canon
+      HaskHOL.Lib.Meson
+      HaskHOL.Lib.Quot
+      HaskHOL.Lib.Misc
+      HaskHOL.Lib.TypeQuant
+
+    exposed: True
+    buildable: True
+    hs-source-dirs: src
+
+    other-modules:
+      HaskHOL.Lib.Bool.Base
+      HaskHOL.Lib.Bool.Context
+      HaskHOL.Lib.Theorems.Base
+      HaskHOL.Lib.Theorems.Context
+      HaskHOL.Lib.IndDefs.Base
+      HaskHOL.Lib.IndDefs.Context 
+      HaskHOL.Lib.Classic.A
+      HaskHOL.Lib.Classic.A.Base
+      HaskHOL.Lib.Classic.A.Context
+      HaskHOL.Lib.Classic.B
+      HaskHOL.Lib.Classic.B.Base
+      HaskHOL.Lib.Classic.B.Context
+      HaskHOL.Lib.Classic.C
+      HaskHOL.Lib.Classic.C.Base
+      HaskHOL.Lib.Classic.C.Context
+      HaskHOL.Lib.Classic.Base
+      HaskHOL.Lib.Classic.Context
+      HaskHOL.Lib.Trivia.A
+      HaskHOL.Lib.Trivia.A.Base
+      HaskHOL.Lib.Trivia.A.Context
+      HaskHOL.Lib.Trivia.Base
+      HaskHOL.Lib.Trivia.Context
+      HaskHOL.Lib.TypeQuant.Context
+
+    ghc-prof-options: -prof -fprof-auto
+    ghc-options: -Wall -O2
+
+source-repository head
+  type: git 
+  location: git://github.com/ecaustin/haskhol-deductive.git
+

LICENSE

@@ -0,0 +1,24 @@
+Copyright (c) 2013, University of Kansas
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+  * Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+  * Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+

Setup.hs

@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain

src/HaskHOL/Deductive.hs

@@ -0,0 +1,82 @@
+{-|
+  Module:    HaskHOL.Deductive
+  Copyright: (c) The University of Kansas 2013
+  LICENSE:   BSD3
+
+  Maintainer:  [email protected]
+  Stability:   unstable
+  Portability: unknown
+
+  This module is the one to import for users looking to include the entirety of
+  the deductive reasoning engine of the HaskHOL proof system.  It re-exports all
+  of the deductive sub-modules; additionally, it exports aliases to a theory 
+  context, quasi-quoter, and compile-time proof methods for users who are
+  working only with these libraries.
+-}
+module HaskHOL.Deductive
+    ( -- * Theory Context
+       -- $ThryCtxt
+      DeductiveType
+    , DeductiveCtxt
+    , ctxtDeductive
+    , deductive
+      -- * Re-exported Modules
+    , module HaskHOL.Lib.Equal
+    , module HaskHOL.Lib.Bool
+    , module HaskHOL.Lib.DRule
+    , module HaskHOL.Lib.Tactics
+    , module HaskHOL.Lib.Itab
+    , module HaskHOL.Lib.Simp
+    , module HaskHOL.Lib.Theorems
+    , module HaskHOL.Lib.IndDefs
+    , module HaskHOL.Lib.Classic
+    , module HaskHOL.Lib.Trivia
+    , module HaskHOL.Lib.Canon
+    , module HaskHOL.Lib.Meson
+    , module HaskHOL.Lib.Quot
+    , module HaskHOL.Lib.Misc
+    , module HaskHOL.Lib.TypeQuant
+    ) where
+
+import HaskHOL.Core
+
+import HaskHOL.Lib.Equal
+import HaskHOL.Lib.Bool
+import HaskHOL.Lib.DRule
+import HaskHOL.Lib.Tactics
+import HaskHOL.Lib.Itab
+import HaskHOL.Lib.Simp
+import HaskHOL.Lib.Theorems
+import HaskHOL.Lib.IndDefs
+import HaskHOL.Lib.Classic
+import HaskHOL.Lib.Trivia
+import HaskHOL.Lib.Canon
+import HaskHOL.Lib.Meson
+import HaskHOL.Lib.Quot
+import HaskHOL.Lib.Misc
+import HaskHOL.Lib.TypeQuant
+
+import HaskHOL.Lib.TypeQuant.Context
+
+{- $ThryCtxt
+  See 'extendCtxt' in the "HaskHOL.Core.Ext" module for more information.
+-}
+
+{-| 
+  The theory context type for the deductive libraries.  
+  An alias to 'TypeQuantType'.
+-}
+type DeductiveType = TypeQuantType
+type DeductiveCtxt a = TypeQuantCtxt a
+
+{-| 
+  The theory context for the deductive libraries.  
+  An alias to 'ctxtTypeQuant'.
+-}
+{-# NOINLINE ctxtDeductive #-}
+ctxtDeductive :: TheoryPath DeductiveType
+ctxtDeductive = ctxtTypeQuant
+
+-- | The quasi-quoter for the deductive libraries.  An alias to 'typeQuant'.
+deductive :: QuasiQuoter
+deductive = typeQuant