feat(library/init/lean,kernel): add KernelException, addDecl and compileDecl

This commit also refines the type of `addAndCompile`.
We also add `ElabException.kernel` constructor for kernel exceptions.

library/init/lean/elaborator/basic.lean

@@ -53,9 +53,10 @@ structure ElabState :=
 (scopes   : List ElabScope := [{ cmd := "root", header := Name.anonymous }])
 
 inductive ElabException
-| io    : IO.Error → ElabException
-| msg   : Message → ElabException
-| other : String → ElabException
+| io     : IO.Error → ElabException
+| msg    : Message → ElabException
+| kernel : KernelException → ElabException
+| other  : String → ElabException
 
 namespace ElabException
 
@@ -118,8 +119,9 @@ let type := Expr.app (mkConst `IO) (mkConst `Unit);
 let val  := mkCApp addFn [toExpr kind, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
-| none     => throw (IO.userError ("failed to emit registration code for builtin term elaborator '" ++ toString declName ++ "'"))
-| some env => IO.ofExcept (setInitAttr env name)
+-- TODO: pretty print error
+| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin term elaborator '" ++ toString declName ++ "'"))
+| Except.ok env  => IO.ofExcept (setInitAttr env name)
 
 def declareBuiltinTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
 declareBuiltinElab env `Lean.addBuiltinTermElab kind declName
@@ -237,9 +239,13 @@ do pos ← getPos stx;
    logErrorAt pos errorMsg
 
 def toMessage : ElabException → Elab Message
-| (ElabException.msg m)   := pure m
-| (ElabException.io e)    := mkMessage (toString e)
-| (ElabException.other e) := mkMessage e
+| (ElabException.msg m)    := pure m
+| (ElabException.io e)     := mkMessage (toString e)
+| (ElabException.other e)  := mkMessage e
+| (ElabException.kernel e) :=
+  match e with
+  | KernelException.other msg => mkMessage msg
+  | _                         => mkMessage "kernel exception" -- TODO(pretty print them)
 
 def logElabException (e : ElabException) : Elab Unit :=
 do msg ← toMessage e;

library/init/lean/environment.lean

@@ -10,6 +10,7 @@ import init.data.bytearray
 import init.lean.declaration
 import init.lean.smap
 import init.lean.path
+import init.lean.localcontext
 
 namespace Lean
 /- Opaque environment extension state. It is essentially the Lean version of a C `void *`
@@ -86,13 +87,35 @@ match env.find c with
 | ConstantInfo.ctorInfo _ => true
 | _ => false
 
-/--
-Type check, add and compile the given declaration.
+end Environment
 
-TODO: better error handling, we are forgetting the information produced by the C++ type checker and compiler.
--/
-@[extern "lean_add_and_compile"]
-constant addAndCompile (env : @& Environment) (o : @& Options) (d : @& Declaration) : Option Environment := default _
+inductive KernelException
+| unknownConstant  (env : Environment) (name : Name)
+| alreadyDeclared  (env : Environment) (name : Name)
+| declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
+| declHasMVars     (env : Environment) (name : Name) (expr : Expr)
+| declHasFVars     (env : Environment) (name : Name) (expr : Expr)
+| funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
+| typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
+| letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
+| exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
+| appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
+| invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+| other            (msg : String)
+
+namespace Environment
+
+/- Type check given declaration and add it to the environment -/
+@[extern "lean_add_decl"]
+constant addDecl (env : Environment) (decl : @& Declaration) : Except KernelException Environment := default _
+
+/- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
+@[extern "lean_compile_decl"]
+constant compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment := default _
+
+def addAndCompile (env : Environment) (opt : Options) (decl : Declaration) : Except KernelException Environment :=
+do env ← addDecl env decl;
+   compileDecl env opt decl
 
 end Environment
 

library/init/lean/parser/parser.lean

@@ -1438,8 +1438,9 @@ let type := Expr.app (mkConst `IO) (mkConst `Unit);
 let val  := mkCApp addFnName [mkConst refDeclName, toExpr declName, mkConst declName];
 let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
 match env.addAndCompile {} decl with
-| none     => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
-| some env => IO.ofExcept (setInitAttr env name)
+-- TODO: pretty print error
+| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
+| Except.ok env  => IO.ofExcept (setInitAttr env name)
 
 def declareLeadingBuiltinParser (env : Environment) (refDeclName : Name) (declName : Name) : IO Environment :=
 declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser refDeclName declName

src/kernel/environment.cpp

@@ -237,6 +237,12 @@ environment environment::add(declaration const & d, bool check) const {
     lean_unreachable();
 }
 
+extern "C" object * lean_add_decl(object * env, object * decl) {
+    return catch_kernel_exceptions<environment>([&]() {
+            return environment(env).add(declaration(decl, true));
+        });
+}
+
 static void env_ext_finalizer(void * ext) {
     delete static_cast<environment_extension*>(ext);
 }

src/kernel/kernel_exception.h

@@ -18,6 +18,7 @@ public:
     kernel_exception(environment const & env, char const * msg):exception(msg), m_env(env) {}
     kernel_exception(environment const & env, sstream const & strm):exception(strm), m_env(env) {}
     environment const & get_environment() const { return m_env; }
+    environment const & env() const { return m_env; }
 };
 
 class unknown_constant_exception : public kernel_exception {
@@ -136,4 +137,71 @@ public:
         kernel_exception_with_lctx(env, lctx), m_proj(proj) {}
     expr const & get_proj() const { return m_proj; }
 };
+
+/*
+Helper function for interfacing C++ code with code written in Lean.
+It executes closure `f` which produces an object_ref of type `A` and may throw
+an `kernel_exception` or `exception`. Then, convert result into `Except KernelException T`
+where `T` is the type of the lean objected represented by `A`.
+We use the constructor `KernelException.other <msg>` to handle C++ `exception` objects which
+are not `kernel_exception`.
+```
+inductive KernelException
+0  | unknownConstant  (env : Environment) (name : Name)
+1  | alreadyDeclared  (env : Environment) (name : Name)
+2  | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
+3  | declHasMVars     (env : Environment) (name : Name) (expr : Expr)
+4  | declHasFVars     (env : Environment) (name : Name) (expr : Expr)
+5  | funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
+6  | typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
+7  | letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
+8  | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
+9  | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
+10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+11 | other            (msg : String)
+```
+*/
+template<typename A>
+object * catch_kernel_exceptions(std::function<A()> const & f) {
+    try {
+        A a = f();
+        return mk_cnstr(1, a).steal();
+    } catch (unknown_constant_exception & ex) {
+        // 0  | unknownConstant  (env : Environment) (name : Name)
+        return mk_cnstr(0, mk_cnstr(0, ex.env(), ex.get_name())).steal();
+    } catch (already_declared_exception & ex) {
+        // 1  | alreadyDeclared  (env : Environment) (name : Name)
+        return mk_cnstr(0, mk_cnstr(1, ex.env(), ex.get_name())).steal();
+    } catch (definition_type_mismatch_exception & ex) {
+        // 2  | declTypeMismatch (env : Environment) (decl : Declaration) (givenType : Expr)
+        return mk_cnstr(0, mk_cnstr(2, ex.env(), ex.get_declaration(), ex.get_given_type())).steal();
+    } catch (declaration_has_metavars_exception & ex) {
+        // 3  | declHasMVars     (env : Environment) (name : Name) (expr : Expr)
+        return mk_cnstr(0, mk_cnstr(3, ex.env(), ex.get_decl_name(), ex.get_expr())).steal();
+    } catch (declaration_has_free_vars_exception & ex) {
+        // 4  | declHasFVars     (env : Environment) (name : Name) (expr : Expr)
+        return mk_cnstr(0, mk_cnstr(4, ex.env(), ex.get_decl_name(), ex.get_expr())).steal();
+    } catch (function_expected_exception & ex) {
+        // 5  | funExpected      (env : Environment) (lctx : LocalContext) (expr : Expr)
+        return mk_cnstr(0, mk_cnstr(5, ex.env(), ex.get_local_ctx(), ex.get_fn())).steal();
+    } catch (type_expected_exception & ex) {
+        // 6  | typeExpected     (env : Environment) (lctx : LocalContext) (expr : Expr)
+        return mk_cnstr(0, mk_cnstr(6, ex.env(), ex.get_local_ctx(), ex.get_type())).steal();
+    } catch (def_type_mismatch_exception & ex) {
+        // 7  | letTypeMismatch  (env : Environment) (lctx : LocalContext) (name : Name) (givenType : Expr) (expectedType : Expr)
+        return mk_cnstr(0, mk_cnstr(7, ex.env(), ex.get_local_ctx(), ex.get_name(), ex.get_given_type(), ex.get_expected_type())).steal();
+    } catch (expr_type_mismatch_exception & ex) {
+        // 8  | exprTypeMismatch (env : Environment) (lctx : LocalContext) (expr : Expr) (expectedType : Expr)
+        return mk_cnstr(0, mk_cnstr(8, ex.env(), ex.get_local_ctx(), ex.get_expr(), ex.get_expected_type())).steal();
+    } catch (app_type_mismatch_exception & ex) {
+        // 9  | appTypeMismatch  (env : Environment) (lctx : LocalContext) (app : Expr) (funType : Expr) (argType : Expr)
+        return mk_cnstr(0, mk_cnstr(9, ex.env(), ex.get_local_ctx(), ex.get_app(), ex.get_function_type(), ex.get_arg_type())).steal();
+    } catch (invalid_proj_exception & ex) {
+        // 10 | invalidProj      (env : Environment) (lctx : LocalContext) (proj : Expr)
+        return mk_cnstr(0, mk_cnstr(10, ex.env(), ex.get_local_ctx(), ex.get_proj())).steal();
+    } catch (exception & ex) {
+        // 11 | other            (msg : String)
+        return mk_cnstr(0, mk_cnstr(11, string_ref(ex.what()))).steal();
+    }
+}
 }

src/library/compiler/compiler.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "util/option_declarations.h"
 #include "kernel/type_checker.h"
+#include "kernel/kernel_exception.h"
 #include "library/max_sharing.h"
 #include "library/trace.h"
 #include "library/sorry.h"
@@ -244,6 +245,12 @@ names get_decl_names_for_code_gen(declaration const & decl) {
     return names(get_decl_names_for_code_gen_core(decl.to_obj_arg()));
 }
 
+extern "C" object * lean_compile_decl(object * env, object * opts, object * decl) {
+    return catch_kernel_exceptions<environment>([&]() {
+            return compile(environment(env), options(opts, true), get_decl_names_for_code_gen(declaration(decl, true)));
+        });
+}
+
 environment add_and_compile(environment const & env, options const & opts, declaration const & decl) {
     environment new_env = env.add(decl);
     return compile(new_env, opts, get_decl_names_for_code_gen(decl));