diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index fbc474124b..aa48dbbb0d 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/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; diff --git a/library/init/lean/environment.lean b/library/init/lean/environment.lean index a7811faefd..f0e5887762 100644 --- a/library/init/lean/environment.lean +++ b/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 diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean index 664f1127a6..c1eb473d45 100644 --- a/library/init/lean/parser/parser.lean +++ b/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 diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp index 97269a3616..c01c73ec2c 100644 --- a/src/kernel/environment.cpp +++ b/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([&]() { + return environment(env).add(declaration(decl, true)); + }); +} + static void env_ext_finalizer(void * ext) { delete static_cast(ext); } diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h index bd03792308..a8dd633f47 100644 --- a/src/kernel/kernel_exception.h +++ b/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 ` 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 +object * catch_kernel_exceptions(std::function 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(); + } +} } diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index 5d5aab6d7a..1bcda2f354 100644 --- a/src/library/compiler/compiler.cpp +++ b/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([&]() { + 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));