Initial commit

Author: gilith

.gitignore

@@ -0,0 +1 @@
+/dist

LICENSE

@@ -0,0 +1,17 @@
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in
+all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
+THE SOFTWARE.

Setup.hs

@@ -0,0 +1,6 @@
+module Main ( main ) where
+
+import Distribution.Simple
+
+main :: IO ()
+main = defaultMain

hol.cabal

@@ -0,0 +1,20 @@
+name: hol
+version: 1.0
+category: Logic
+synopsis: Higher order logic
+license: MIT
+license-file: LICENSE
+cabal-version: >= 1.8.0.2
+build-type: Simple
+author: Joe Leslie-Hurd <[email protected]>
+maintainer: Joe Leslie-Hurd <[email protected]>
+description:
+  This package implements a higher order logic kernel.
+
+Library
+  build-depends:
+    base >= 4.0 && < 5.0
+  hs-source-dirs: src
+  ghc-options: -Wall
+  exposed-modules:
+    HOL.Data

src/HOL/Data.hs

@@ -0,0 +1,50 @@
+{- |
+module: $Header$
+description: Mutually recursive datatypes of higher order logic types and terms
+license: MIT
+
+maintainer: Joe Leslie-Hurd <[email protected]>
+stability: provisional
+portability: portable
+-}
+
+module HOL.Data
+where
+
+type Name = String
+
+data Type = Type TypeData Integer
+
+data TypeData =
+    VarType TypeVar
+  | OpType TypeOp [Type]
+
+data TypeVar = TypeVar Name
+
+data TypeOp = TypeOp Name TypeOpProv
+
+data TypeOpProv =
+    UndefTypeOpProv
+  | DefTypeOpProv TypeOpDef
+
+data TypeOpDef = TypeOpDef Term [TypeVar]
+
+data Var = Var Name Type
+
+data Term = Term TermData Type Integer
+
+data TermData =
+    ConstTerm Const Type
+  | VarTerm Var
+  | AppTerm Term Term
+  | AbsTerm Var Term
+
+data Const = Const Name ConstProv
+
+data ConstProv =
+    UndefConstProv
+  | DefConstProv ConstDef
+  | AbsConstProv TypeOp
+  | RepConstProv TypeOp
+
+data ConstDef = ConstDef Term