summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthewFarkasDyck <>2019-05-15 17:42:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-05-15 17:42:00 (GMT)
commit65ffbc2ce6f7f66a49162afcbe9825b3391b3366 (patch)
treeb522f72fdc3254f07023cdc071e03d9d14082111
version 0.0.0.1HEAD0.0.0.1master
-rw-r--r--LICENSE30
-rw-r--r--Lean/Exception.hs25
-rw-r--r--Lean/Expr.hs23
-rw-r--r--Lean/IO/Util.hs66
-rw-r--r--Lean/Name.hs39
-rw-r--r--Lean/Raw/C/Decl.hsc34
-rw-r--r--Lean/Raw/C/Decl/Cert.hsc14
-rw-r--r--Lean/Raw/C/Env.hsc21
-rw-r--r--Lean/Raw/C/Exception.hsc30
-rw-r--r--Lean/Raw/C/Expr.hsc40
-rw-r--r--Lean/Raw/C/Name.hsc41
-rw-r--r--Lean/Raw/C/Univ.hsc43
-rw-r--r--Lean/Univ.hs49
-rw-r--r--Lean/Wrapper.hs12
-rw-r--r--Lean/Wrapper/Univ.hs6
-rw-r--r--Prelude.hs7
-rwxr-xr-xREADME.md1
-rw-r--r--lean.cabal67
18 files changed, 548 insertions, 0 deletions
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..8f879a5
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright M Farkas-Dyck © 2019
+
+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.
+
+ * Neither the name of M Farkas-Dyck nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+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
+OWNER 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. \ No newline at end of file
diff --git a/Lean/Exception.hs b/Lean/Exception.hs
new file mode 100644
index 0000000..9a0bec3
--- /dev/null
+++ b/Lean/Exception.hs
@@ -0,0 +1,25 @@
+module Lean.Exception
+ (Exception, message, detailedMessage, kind,
+ Kind (Null, System, OutOfMemory, Interrupted, Kernel, Parser)) where
+
+import qualified Control.Exception.Base as Base
+import Control.Monad
+import Data.Text (Text)
+import qualified Data.Text as Text
+import System.IO.Unsafe
+
+import Lean.IO.Util
+import Lean.Raw.C.Exception (Kind)
+import qualified Lean.Raw.C.Exception as Raw
+import Lean.Wrapper
+
+type Exception = Wrapper Raw.Struct
+
+instance Base.Exception Exception where displayException = Text.unpack . message
+
+message, detailedMessage :: Exception -> Text
+message = unsafePerformIO <<< fromRaw <=< Raw.message . unwrap'
+detailedMessage = unsafePerformIO <<< fromRaw <=< Raw.detailedMessage . unwrap'
+
+kind :: Exception -> Raw.Kind
+kind = Raw.kind . unwrap'
diff --git a/Lean/Expr.hs b/Lean/Expr.hs
new file mode 100644
index 0000000..8650704
--- /dev/null
+++ b/Lean/Expr.hs
@@ -0,0 +1,23 @@
+module Lean.Expr (Expr (Lean.Expr.Var, Lean.Expr.Sort)) where
+
+import System.IO.Unsafe
+
+import Lean.Exception ()
+import Lean.IO.Util
+import qualified Lean.Raw.C.Expr as Raw
+import Lean.Wrapper
+import Lean.Wrapper.Univ (Univ (Univ))
+import qualified Lean.Wrapper.Univ as Univ
+
+newtype Expr = Expr { raw :: Wrapper Raw.Struct }
+
+kindChecked :: Raw.Kind -> (Wrapper Raw.Struct -> IO b) -> Expr -> Maybe b
+kindChecked k f = checked ((==) k . Raw.kind) f . raw
+
+pattern Var :: Word -> Expr
+pattern Var k <- (kindChecked Raw.Var (liftLean1 Raw.getVarIdx) -> Just k) where
+ Var = Expr . unsafePerformIO . liftLean0 . Raw.mkVar . fromIntegral
+
+pattern Sort :: Univ -> Expr
+pattern Sort u <- (fmap Univ . kindChecked Raw.Sort (liftLean1 Raw.getSortUniv) -> Just u) where
+ Sort = Expr . unsafePerformIO . liftLean1 Raw.mkSort . Univ.raw
diff --git a/Lean/IO/Util.hs b/Lean/IO/Util.hs
new file mode 100644
index 0000000..eed39bd
--- /dev/null
+++ b/Lean/IO/Util.hs
@@ -0,0 +1,66 @@
+{-# LANGUAGE TypeFamilies #-}
+
+module Lean.IO.Util where
+
+import Control.Applicative
+import Control.Exception.Base
+import Control.Monad
+import Data.Text (Text)
+import qualified Data.Text.Foreign as Text
+import Foreign
+import Foreign.C.Types
+import Foreign.ForeignPtr.Unsafe
+import System.IO.Unsafe
+
+import Lean.Wrapper
+
+unwrap' :: Wrapper a -> Ptr a
+unwrap' = unsafeForeignPtrToPtr . unwrap
+
+class Storable (Raw a) => FromRaw a where
+ type Raw a
+ fromRaw :: Raw a -> IO a
+
+instance Drop a => FromRaw (Wrapper a) where
+ type Raw (Wrapper a) = Ptr a
+ fromRaw = wrap
+
+instance FromRaw Bool where
+ type Raw Bool = CInt
+ fromRaw = pure . (/= 0)
+
+instance FromRaw Word where
+ type Raw Word = CUInt
+ fromRaw = pure . fromIntegral
+
+instance FromRaw Int where
+ type Raw Int = CInt
+ fromRaw = pure . fromIntegral
+
+instance FromRaw Text where
+ type Raw Text = Ptr CChar
+ fromRaw = getCompose $ Compose (liftA2 (=<<) Text.fromPtr (fmap fromIntegral . cNulArrayLen) . castPtr) <* Compose dropString
+
+foreign import ccall unsafe "lean_string_del" dropString :: Ptr CChar -> IO ()
+
+liftLean0 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> IO z
+liftLean0 f = alloca $ \ p -> alloca $ \ q ->
+ f p q >>= \ case 0 -> peek q >>= wrap >>= throw; _ -> peek p >>= fromRaw
+
+liftLean1 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> IO z
+liftLean1 f a = liftLean0 $ f (unwrap' a)
+
+liftLean2 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr b -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> Wrapper b -> IO z
+liftLean2 f a b = liftLean0 $ f (unwrap' a) (unwrap' b)
+
+liftLean3 :: (FromRaw z, Drop ex, Exception (Wrapper ex)) => (Ptr a -> Ptr b -> Ptr c -> Ptr (Raw z) -> Ptr (Ptr ex) -> IO CInt) -> Wrapper a -> Wrapper b -> Wrapper c -> IO z
+liftLean3 f a b c = liftLean0 $ f (unwrap' a) (unwrap' b) (unwrap' c)
+
+checked :: (Ptr s -> Bool) -> (Wrapper s -> IO z) -> Wrapper s -> Maybe z
+checked pred f s = unsafePerformIO . sequenceA $ f s <$ guard (pred (unwrap' s))
+
+cNulArrayLen :: _ => Ptr a -> IO Word
+cNulArrayLen = go 0 where
+ go n ptr = peek ptr >>= \ case
+ 0 -> pure n
+ _ -> go (n+1) $ plusPtr ptr 1
diff --git a/Lean/Name.hs b/Lean/Name.hs
new file mode 100644
index 0000000..14d9125
--- /dev/null
+++ b/Lean/Name.hs
@@ -0,0 +1,39 @@
+module Lean.Name where
+
+import Data.Function (on)
+import Data.Text (Text)
+import qualified Data.Text as Text
+import qualified Data.Text.Foreign as Text
+import Foreign.Ptr
+import System.IO.Unsafe
+import Util
+
+import Lean.Exception ()
+import Lean.IO.Util
+import qualified Lean.Raw.C.Name as Raw
+import Lean.Wrapper
+
+newtype Name = Name { raw :: Wrapper Raw.Struct }
+
+instance Show Name where
+ show (Name name) = Text.unpack . unsafePerformIO $ liftLean1 Raw.toString name
+
+instance Eq Name where
+ Name a == Name b = (/= 0) . unsafePerformIO $ (Raw.eq `on` unwrap') a b
+
+instance Ord Name where
+ Name a <= Name b = ((/= 0) . unsafePerformIO $ (Raw.lt `on` unwrap') a b) || Name a == Name b
+
+{-# COMPLETE Anonymous, Str, Idx #-}
+
+pattern Anonymous :: Name
+pattern Anonymous <- ((/= 0) . unsafePerformIO . Raw.isAnonymous . unwrap' . raw -> True) where
+ Anonymous = Name . unsafePerformIO $ liftLean0 Raw.mkAnonymous
+
+pattern Str :: Name -> Text -> Name
+pattern Str name xs <- (checked ((/= 0) . unsafePerformIO . Raw.isStr) (fmap Name . liftLean1 Raw.getPrefix &=& liftLean1 Raw.getStr) . raw -> Just (name, xs)) where
+ Str (Name name) = Name . unsafePerformIO . flip Text.useAsPtr (pure . flip (liftLean1 . flip Raw.mkStr) name . castPtr) . flip Text.snoc '\0'
+
+pattern Idx :: Name -> Word -> Name
+pattern Idx name k <- (checked ((/= 0) . unsafePerformIO . Raw.isIdx) (fmap Name . liftLean1 Raw.getPrefix &=& liftLean1 Raw.getIdx) . raw -> Just (name, k)) where
+ Idx (Name name) = Name . unsafePerformIO . flip (liftLean1 . flip Raw.mkIdx) name . fromIntegral
diff --git a/Lean/Raw/C/Decl.hsc b/Lean/Raw/C/Decl.hsc
new file mode 100644
index 0000000..453ed99
--- /dev/null
+++ b/Lean/Raw/C/Decl.hsc
@@ -0,0 +1,34 @@
+module Lean.Raw.C.Decl where
+
+import Foreign
+import Foreign.C.Types
+
+import qualified Lean.Raw.C.Decl.Cert as Cert
+import Lean.Raw.C.Env (Env)
+import Lean.Raw.C.Exception (Exception)
+import Lean.Raw.C.Expr (Expr)
+import Lean.Raw.C.Name (ListName, Name)
+import Lean.Wrapper
+
+#include <lean.h>
+
+newtype Kind = Kind CInt
+ deriving (Eq)
+
+#{enum Kind, Kind,
+ Const = LEAN_DECL_CONST,
+ Axiom = LEAN_DECL_AXIOM,
+ Def = LEAN_DECL_DEF,
+ Thm = LEAN_DECL_THM}
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_decl_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Decl = Ptr Struct
+
+foreign import ccall unsafe "lean_decl_mk_axiom" mkAxiom :: Name -> ListName -> Expr -> Ptr Decl -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_decl_mk_const" mkConst :: Name -> ListName -> Expr -> Ptr Decl -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_decl_mk_def_with" mkDef :: Env -> Name -> ListName -> Expr -> Expr -> CUInt -> CInt -> Ptr Decl -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_decl_check" check :: Env -> Decl -> Ptr Cert.Decl -> Ptr Exception -> IO CInt
diff --git a/Lean/Raw/C/Decl/Cert.hsc b/Lean/Raw/C/Decl/Cert.hsc
new file mode 100644
index 0000000..9995558
--- /dev/null
+++ b/Lean/Raw/C/Decl/Cert.hsc
@@ -0,0 +1,14 @@
+module Lean.Raw.C.Decl.Cert where
+
+import Foreign
+
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_cert_decl_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Decl = Ptr Struct
diff --git a/Lean/Raw/C/Env.hsc b/Lean/Raw/C/Env.hsc
new file mode 100644
index 0000000..794b6b2
--- /dev/null
+++ b/Lean/Raw/C/Env.hsc
@@ -0,0 +1,21 @@
+module Lean.Raw.C.Env where
+
+import Foreign
+import Foreign.C.Types
+
+import qualified Lean.Raw.C.Decl.Cert as Cert (Decl)
+import Lean.Raw.C.Exception (Exception)
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_env_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Env = Ptr Struct
+
+foreign import ccall unsafe "lean_env_mk_std" mkStd :: CUInt -> Ptr Env -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_env_add" add :: Env -> Cert.Decl -> Ptr Env -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_env_replace" replace :: Env -> Cert.Decl -> Ptr Env -> Ptr Exception -> IO CInt
diff --git a/Lean/Raw/C/Exception.hsc b/Lean/Raw/C/Exception.hsc
new file mode 100644
index 0000000..92f1863
--- /dev/null
+++ b/Lean/Raw/C/Exception.hsc
@@ -0,0 +1,30 @@
+module Lean.Raw.C.Exception where
+
+import Foreign
+import Foreign.C.Types
+
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_exception_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Exception = Ptr Struct
+
+newtype Kind = Kind CInt
+ deriving (Eq)
+
+#{enum Kind, Kind,
+ Null = LEAN_NULL_EXCEPTION,
+ System = LEAN_SYSTEM_EXCEPTION,
+ OutOfMemory = LEAN_OUT_OF_MEMORY,
+ Interrupted = LEAN_INTERRUPTED,
+ Kernel = LEAN_KERNEL_EXCEPTION,
+ Parser = LEAN_PARSER_EXCEPTION}
+
+foreign import ccall unsafe "lean_exception_get_message" message :: Exception -> IO (Ptr CChar)
+foreign import ccall unsafe "lean_exception_get_detailed_message" detailedMessage :: Exception -> IO (Ptr CChar)
+foreign import ccall unsafe "lean_exception_get_kind" kind :: Exception -> Kind
diff --git a/Lean/Raw/C/Expr.hsc b/Lean/Raw/C/Expr.hsc
new file mode 100644
index 0000000..8886f39
--- /dev/null
+++ b/Lean/Raw/C/Expr.hsc
@@ -0,0 +1,40 @@
+module Lean.Raw.C.Expr where
+
+import Foreign
+import Foreign.C.Types
+
+import Lean.Raw.C.Exception (Exception)
+import Lean.Raw.C.Univ (Univ)
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_expr_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Expr = Ptr Struct
+
+newtype Kind = Kind CInt
+ deriving (Eq)
+
+#{enum Kind, Kind,
+ Var = LEAN_EXPR_VAR,
+ Sort = LEAN_EXPR_SORT,
+ Const = LEAN_EXPR_CONST,
+ Local = LEAN_EXPR_LOCAL,
+ Meta = LEAN_EXPR_META,
+ App = LEAN_EXPR_APP,
+ Lambda = LEAN_EXPR_LAMBDA,
+ Pi = LEAN_EXPR_PI,
+ Let = LEAN_EXPR_LET,
+ Macro = LEAN_EXPR_MACRO}
+
+foreign import ccall unsafe "lean_expr_mk_var" mkVar :: CUInt -> Ptr Expr -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_expr_mk_sort" mkSort :: Univ -> Ptr Expr -> Ptr Exception -> IO CInt
+
+foreign import ccall unsafe "lean_expr_get_var_idx" getVarIdx :: Expr -> Ptr CUInt -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_expr_get_sort_univ" getSortUniv :: Expr -> Ptr Univ -> Ptr Exception -> IO CInt
+
+foreign import ccall unsafe "lean_expr_kind" kind :: Expr -> Kind
diff --git a/Lean/Raw/C/Name.hsc b/Lean/Raw/C/Name.hsc
new file mode 100644
index 0000000..b9468b0
--- /dev/null
+++ b/Lean/Raw/C/Name.hsc
@@ -0,0 +1,41 @@
+module Lean.Raw.C.Name where
+
+import Foreign
+import Foreign.C.Types
+
+import Lean.Raw.C.Exception (Exception)
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_name_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Name = Ptr Struct
+
+foreign import ccall unsafe "lean_name_del" drop :: Name -> IO ()
+foreign import ccall unsafe "lean_name_mk_anonymous" mkAnonymous :: Ptr Name -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_mk_str" mkStr :: Name -> Ptr CChar -> Ptr Name -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_mk_idx" mkIdx :: Name -> CUInt -> Ptr Name -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_eq" eq :: Name -> Name -> IO CInt
+foreign import ccall unsafe "lean_name_lt" lt :: Name -> Name -> IO CInt
+foreign import ccall unsafe "lean_name_to_string" toString :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_is_anonymous" isAnonymous :: Name -> IO CInt
+foreign import ccall unsafe "lean_name_is_str" isStr :: Name -> IO CInt
+foreign import ccall unsafe "lean_name_is_idx" isIdx :: Name -> IO CInt
+foreign import ccall unsafe "lean_name_get_prefix" getPrefix :: Name -> Ptr Name -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_get_str" getStr :: Name -> Ptr (Ptr CChar) -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_name_get_idx" getIdx :: Name -> Ptr CUInt -> Ptr Exception -> IO CInt
+
+data ListStruct
+
+type ListName = Ptr ListStruct
+
+foreign import ccall unsafe "lean_list_name_del" dropList :: ListName -> IO ()
+foreign import ccall unsafe "lean_list_name_mk_nil" mkNil :: Ptr ListName -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_list_name_mk_cons" mkCons :: Name -> ListName -> Ptr ListName -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_list_name_eq" eqList :: ListName -> ListName -> IO CInt
+foreign import ccall unsafe "lean_list_name_head" head :: ListName -> Ptr Name -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_list_name_del" tail :: ListName -> Ptr ListName -> Ptr Exception -> IO CInt
diff --git a/Lean/Raw/C/Univ.hsc b/Lean/Raw/C/Univ.hsc
new file mode 100644
index 0000000..b7c8b1c
--- /dev/null
+++ b/Lean/Raw/C/Univ.hsc
@@ -0,0 +1,43 @@
+module Lean.Raw.C.Univ where
+
+import Foreign
+import Foreign.C.Types
+
+import Lean.Raw.C.Exception (Exception)
+import Lean.Raw.C.Name (Name)
+import Lean.Wrapper
+
+#include <lean.h>
+
+data Struct
+
+instance Drop Struct where drop = drop'
+foreign import ccall unsafe "&lean_univ_del" drop' :: FunPtr (Ptr Struct -> IO ())
+
+type Univ = Ptr Struct
+
+foreign import ccall unsafe "lean_univ_mk_zero" mkZero :: Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_mk_succ" mkSucc :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_mk_max" mkMax :: Univ -> Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_mk_imax" mkImax :: Univ -> Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_mk_param" mkParam :: Name -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_mk_meta" mkMeta :: Name -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_eq" eq :: Univ -> Univ -> Ptr CInt -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_lt" lt :: Univ -> Univ -> Ptr CInt -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_get_pred" getPred :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_get_max_lhs" getMaxLhs :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_get_max_rhs" getMaxRhs :: Univ -> Ptr Univ -> Ptr Exception -> IO CInt
+foreign import ccall unsafe "lean_univ_get_name" getName :: Univ -> Ptr Name -> Ptr Exception -> IO CInt
+
+newtype Kind = Kind CInt
+ deriving (Eq)
+
+#{enum Kind, Kind,
+ Zero = LEAN_UNIV_ZERO,
+ Succ = LEAN_UNIV_SUCC,
+ Max = LEAN_UNIV_MAX,
+ Imax = LEAN_UNIV_IMAX,
+ Param = LEAN_UNIV_PARAM,
+ Meta = LEAN_UNIV_META}
+
+foreign import ccall unsafe "lean_univ_kind" kind :: Univ -> Kind
diff --git a/Lean/Univ.hs b/Lean/Univ.hs
new file mode 100644
index 0000000..b63ce87
--- /dev/null
+++ b/Lean/Univ.hs
@@ -0,0 +1,49 @@
+module Lean.Univ (Univ (Lean.Univ.Zero, Lean.Univ.Succ, Lean.Univ.Max, Lean.Univ.Imax, Lean.Univ.Param, Lean.Univ.Meta)) where
+
+import Control.Arrow ((***))
+import Foreign.Ptr
+import System.IO.Unsafe
+import Util
+
+import Lean.IO.Util
+import Lean.Exception ()
+import Lean.Name (Name (Name))
+import qualified Lean.Name as Name
+import qualified Lean.Raw.C.Univ as Raw
+import Lean.Wrapper.Univ
+
+instance FromRaw Univ where
+ type Raw Univ = Ptr Raw.Struct
+ fromRaw = fmap Univ . fromRaw
+
+instance Eq Univ where
+ Univ a == Univ b = unsafePerformIO $ liftLean2 Raw.eq a b
+
+instance Ord Univ where
+ Univ a <= Univ b = (unsafePerformIO $ liftLean2 Raw.lt a b) || Univ a == Univ b
+
+{-# COMPLETE Zero, Succ, Max, Imax, Param, Meta #-}
+
+pattern Zero :: Univ
+pattern Zero <- (Raw.kind . unwrap' . raw -> Raw.Zero) where
+ Zero = Univ . unsafePerformIO $ liftLean0 Raw.mkZero
+
+pattern Succ :: Univ -> Univ
+pattern Succ u <- (fmap Univ . checked ((==) Raw.Succ . Raw.kind) (liftLean1 Raw.getPred) . raw -> Just u) where
+ Succ = Univ . unsafePerformIO . liftLean1 Raw.mkSucc . raw
+
+pattern Max :: Univ -> Univ -> Univ
+pattern Max u v <- (fmap (Univ *** Univ) . checked ((==) Raw.Max . Raw.kind) (liftLean1 Raw.getMaxLhs &=& liftLean1 Raw.getMaxRhs) . raw -> Just (u, v)) where
+ Max = curry $ Univ . unsafePerformIO . \ (Univ u, Univ v) -> liftLean2 Raw.mkMax u v
+
+pattern Imax :: Univ -> Univ -> Univ
+pattern Imax u v <- (fmap (Univ *** Univ) . checked ((==) Raw.Imax . Raw.kind) (liftLean1 Raw.getMaxLhs &=& liftLean1 Raw.getMaxRhs) . raw -> Just (u, v)) where
+ Imax = curry $ Univ . unsafePerformIO . \ (Univ u, Univ v) -> liftLean2 Raw.mkImax u v
+
+pattern Param :: Name -> Univ
+pattern Param name <- (fmap Name . checked ((==) Raw.Param . Raw.kind) (liftLean1 Raw.getName) . raw -> Just name) where
+ Param = Univ . unsafePerformIO . liftLean1 Raw.mkParam . Name.raw
+
+pattern Meta :: Name -> Univ
+pattern Meta name <- (fmap Name . checked ((==) Raw.Meta . Raw.kind) (liftLean1 Raw.getName) . raw -> Just name) where
+ Meta = Univ . unsafePerformIO . liftLean1 Raw.mkMeta . Name.raw
diff --git a/Lean/Wrapper.hs b/Lean/Wrapper.hs
new file mode 100644
index 0000000..1bb81ac
--- /dev/null
+++ b/Lean/Wrapper.hs
@@ -0,0 +1,12 @@
+module Lean.Wrapper where
+
+import Foreign
+
+class Drop a where
+ drop :: FunPtr (Ptr a -> IO ())
+
+newtype Wrapper a = Wrapper { unwrap :: ForeignPtr a }
+ deriving (Show)
+
+wrap :: Drop a => Ptr a -> IO (Wrapper a)
+wrap = fmap Wrapper . newForeignPtr drop
diff --git a/Lean/Wrapper/Univ.hs b/Lean/Wrapper/Univ.hs
new file mode 100644
index 0000000..ee28c8d
--- /dev/null
+++ b/Lean/Wrapper/Univ.hs
@@ -0,0 +1,6 @@
+module Lean.Wrapper.Univ where
+
+import qualified Lean.Raw.C.Univ as Raw
+import Lean.Wrapper
+
+newtype Univ = Univ { raw :: Wrapper Raw.Struct }
diff --git a/Prelude.hs b/Prelude.hs
new file mode 100644
index 0000000..9eb9df0
--- /dev/null
+++ b/Prelude.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE PackageImports #-}
+
+module Prelude (module A) where
+
+import "base" Prelude as A hiding (drop, id, (.))
+import Control.Category as A
+import Data.Functor.Compose as A
diff --git a/README.md b/README.md
new file mode 100755
index 0000000..92a11c8
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+# lean
diff --git a/lean.cabal b/lean.cabal
new file mode 100644
index 0000000..454c16e
--- /dev/null
+++ b/lean.cabal
@@ -0,0 +1,67 @@
+name: lean
+version: 0.0.0.1
+synopsis: Bonds to Lean theorem prover
+-- description:
+license: BSD3
+license-file: LICENSE
+author: M Farkas-Dyck
+maintainer: strake888@gmail.com
+copyright: 2019 M Farkas-Dyck
+category: Math
+build-type: Simple
+extra-source-files: README.md
+cabal-version: >=1.10
+
+library
+ hs-source-dirs: .
+ exposed-modules: Lean.Exception
+ , Lean.Expr
+ , Lean.Name
+ , Lean.Univ
+ , Lean.Raw.C.Decl
+ , Lean.Raw.C.Decl.Cert
+ , Lean.Raw.C.Env
+ , Lean.Raw.C.Exception
+ , Lean.Raw.C.Expr
+ , Lean.Raw.C.Name
+ , Lean.Raw.C.Univ
+ other-modules: Prelude
+ , Lean.IO.Util
+ , Lean.Wrapper
+ , Lean.Wrapper.Univ
+ build-depends: base >= 4.7 && < 5
+ , base-unicode-symbols
+ , text-utf8
+ , transformers
+ , util
+ default-language: Haskell2010
+ default-extensions: UnicodeSyntax
+ , LambdaCase
+ , EmptyCase
+ , InstanceSigs
+ , PartialTypeSignatures
+ , PatternSynonyms
+ , ViewPatterns
+ , PolyKinds
+ , ConstraintKinds
+ , FlexibleContexts
+ , FlexibleInstances
+ , TypeFamilies
+ , MonadComprehensions
+ , StandaloneDeriving
+ , GeneralizedNewtypeDeriving
+ , DeriveFunctor, DeriveFoldable, DeriveTraversable
+ ghc-options: -Wall -Wcompat -Wredundant-constraints -Wno-name-shadowing
+ -Wincomplete-record-updates -Wincomplete-uni-patterns
+ -Werror=incomplete-patterns
+ -Werror=incomplete-uni-patterns
+ -Werror=incomplete-record-updates
+ -Werror=missing-fields
+ -Werror=missing-methods
+ -Wno-partial-type-signatures
+ -Wno-orphans
+ build-tools: hsc2hs
+
+source-repository head
+ type: git
+ location: https://github.com/strake/lean.hs