From acccfdfbd5dff8dc3009319f88db6d2af9b3e430 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 11 Dec 2019 17:20:43 -0800 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Class.lean | 2 +- .../src/Init/Lean/Elab/BuiltinNotation.lean | 6 +- stage0/src/Init/Lean/Meta/Instances.lean | 1 + stage0/src/library/class.cpp | 8 +- stage0/stdlib/Init/Lean/Class.c | 4 +- .../stdlib/Init/Lean/Elab/BuiltinNotation.c | 310 ++++++++++++++++++ stage0/stdlib/Init/Lean/Meta/Instances.c | 10 +- 7 files changed, 330 insertions(+), 11 deletions(-) diff --git a/stage0/src/Init/Lean/Class.lean b/stage0/src/Init/Lean/Class.lean index c7b5fbf98d..53d466b86a 100644 --- a/stage0/src/Init/Lean/Class.lean +++ b/stage0/src/Init/Lean/Class.lean @@ -147,7 +147,7 @@ registerAttribute { } -- TODO: delete -@[export lean_add_instance] +@[export lean_add_instance_old] def addGlobalInstanceOld (env : Environment) (instName : Name) : Except String Environment := match env.find instName with | none => Except.error ("unknown declaration '" ++ toString instName ++ "'") diff --git a/stage0/src/Init/Lean/Elab/BuiltinNotation.lean b/stage0/src/Init/Lean/Elab/BuiltinNotation.lean index e1535bef79..a3f2e5c82f 100644 --- a/stage0/src/Init/Lean/Elab/BuiltinNotation.lean +++ b/stage0/src/Init/Lean/Elab/BuiltinNotation.lean @@ -27,6 +27,9 @@ fun stx expectedType? => do def elabInfixOp (op : Name) : TermElab := fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType? +@[builtinTermElab prod] def elabProd : TermElab := elabInfixOp `Prod +@[builtinTermElab fcomp] def ElabFComp : TermElab := elabInfixOp `Function.comp + @[builtinTermElab add] def elabAdd : TermElab := elabInfixOp `HasAdd.add @[builtinTermElab sub] def elabSub : TermElab := elabInfixOp `HasSub.sub @[builtinTermElab mul] def elabMul : TermElab := elabInfixOp `HasMul.mul @@ -57,7 +60,7 @@ fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType @[builtinTermElab cons] def elabCons : TermElab := elabInfixOp `List.cons @[builtinTermElab andthen] def elabAndThen : TermElab := elabInfixOp `HasAndthen.andthen --- @[builtinTermElab bind] def elabBind : TermElab := elabInfixOp `HasBind.bind +@[builtinTermElab bindOp] def elabBind : TermElab := elabInfixOp `HasBind.bind @[builtinTermElab seq] def elabseq : TermElab := elabInfixOp `HasSeq.seq @[builtinTermElab seqLeft] def elabseqLeft : TermElab := elabInfixOp `HasSeqLeft.seqLeft @@ -73,6 +76,7 @@ fun stx expectedType? => elabInfix (mkTermId (stx.getArg 1) op) stx expectedType @[builtinTermElab andM] def elabAndM : TermElab := elabInfixOp `andM /- +TODO @[builtinTermElab] def elabsubst : TermElab := elabInfixOp infixR " ▸ " 75 -/ diff --git a/stage0/src/Init/Lean/Meta/Instances.lean b/stage0/src/Init/Lean/Meta/Instances.lean index 0c5d9f3093..0a0fca8076 100644 --- a/stage0/src/Init/Lean/Meta/Instances.lean +++ b/stage0/src/Init/Lean/Meta/Instances.lean @@ -34,6 +34,7 @@ withNewMCtxDepth $ do (_, _, type) ← forallMetaTelescopeReducing type; DiscrTree.mkPath type +@[export lean_add_instance] def addGlobalInstance (env : Environment) (constName : Name) : IO Environment := match env.find constName with | none => throw $ IO.userError "unknown constant" diff --git a/stage0/src/library/class.cpp b/stage0/src/library/class.cpp index 3607d64be1..be47c91932 100644 --- a/stage0/src/library/class.cpp +++ b/stage0/src/library/class.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include "util/io.h" #include "library/class.h" namespace lean { @@ -13,7 +14,8 @@ extern "C" uint8 lean_is_instance(object* env, object* n); extern "C" object* lean_get_class_instances(object* env, object* n); extern "C" uint8 lean_is_out_param(object* e); extern "C" uint8 lean_has_out_params(object* env, object* n); -extern "C" object* lean_add_instance(object* env, object* n); +extern "C" object* lean_add_instance(object* env, object* n, object* w); +extern "C" object* lean_add_instance_old(object* env, object* n); bool is_class_out_param(expr const & e) { return lean_is_out_param(e.to_obj_arg()); } bool has_class_out_params(environment const & env, name const & c) { return lean_has_out_params(env.to_obj_arg(), c.to_obj_arg()); } @@ -23,7 +25,9 @@ names get_class_instances(environment const & env, name const & c) { return name environment add_instance(environment const & env, name const & n, bool persistent) { if (!persistent) throw exception("local instances have been disabled"); - return get_except_value(lean_add_instance(env.to_obj_arg(), n.to_obj_arg())); + environment new_env = get_except_value(lean_add_instance_old(env.to_obj_arg(), n.to_obj_arg())); + new_env = get_io_result(lean_add_instance(new_env.to_obj_arg(), n.to_obj_arg(), io_mk_world())); + return new_env; } static name * g_anonymous_inst_name_prefix = nullptr; diff --git a/stage0/stdlib/Init/Lean/Class.c b/stage0/stdlib/Init/Lean/Class.c index dac15951d6..af239662e4 100644 --- a/stage0/stdlib/Init/Lean/Class.c +++ b/stage0/stdlib/Init/Lean/Class.c @@ -181,7 +181,7 @@ lean_object* l_Lean_getClassName(lean_object*, lean_object*); uint8_t l_Lean_SMap_contains___at_Lean_isInstance___spec__1(lean_object*, lean_object*); lean_object* l_Lean_addGlobalInstanceOld___closed__1; lean_object* l_Lean_ConstantInfo_value_x3f(lean_object*); -lean_object* lean_add_instance(lean_object*, lean_object*); +lean_object* lean_add_instance_old(lean_object*, lean_object*); lean_object* l_PersistentHashMap_insertAux___main___at_Lean_ClassState_addEntry___spec__20(lean_object*, size_t, size_t, lean_object*, lean_object*); uint8_t lean_is_instance(lean_object*, lean_object*); lean_object* l_Lean_classExtension___elambda__4(lean_object*); @@ -6602,7 +6602,7 @@ x_1 = lean_mk_string("', failed to retrieve class"); return x_1; } } -lean_object* lean_add_instance(lean_object* x_1, lean_object* x_2) { +lean_object* lean_add_instance_old(lean_object* x_1, lean_object* x_2) { _start: { lean_object* x_3; diff --git a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c index c8f42c2328..2414f12fa4 100644 --- a/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c +++ b/stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c @@ -14,6 +14,7 @@ extern "C" { #endif lean_object* l_Lean_Elab_Term_elabModN___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3; lean_object* l_Lean_Elab_Term_elabBAnd___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseq___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrElse___closed__2; @@ -22,6 +23,7 @@ lean_object* l_Lean_Elab_Term_elabseqLeft___boxed(lean_object*, lean_object*, le lean_object* l_Lean_Elab_Term_elabDiv(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabAdd___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabseqLeft___closed__1; +lean_object* l_Lean_Elab_Term_elabBind___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabAdd___closed__1; extern lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapRev___closed__1; @@ -29,18 +31,21 @@ lean_object* l_Lean_Elab_Term_elabModN___closed__1; lean_object* l_Lean_Elab_Term_elabIff(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_andthen___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_elabBAnd___closed__1; +lean_object* l_Lean_Elab_Term_elabBind___closed__2; extern lean_object* l_Lean_Expr_eq_x3f___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabIff___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBEq(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNe___closed__3; extern lean_object* l_Lean_Parser_Term_sub___elambda__1___closed__2; +lean_object* l_Lean_Elab_Term_elabBind___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr___closed__3; lean_object* l_Lean_Elab_Term_elabseqLeft___closed__2; lean_object* l_Lean_Elab_Term_elabMod___closed__2; lean_object* l_Lean_Elab_Term_elabPow(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabModN___closed__3; +lean_object* l_Lean_Elab_Term_elabBind___closed__4; lean_object* l_Lean_Elab_Term_elabBOr___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabInfix(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_eq___elambda__1___closed__2; @@ -58,6 +63,7 @@ extern lean_object* l_Lean_stxInh; lean_object* l_Lean_Elab_Term_elabMul___closed__2; lean_object* l_Lean_Elab_Term_elabPow___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd___closed__3; +extern lean_object* l_List_map___main___at___private_Init_Lean_Elab_Quotation_7__quote___main___spec__11___closed__2; lean_object* l_Lean_Elab_Term_elabMod___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabIff___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMul___closed__3; @@ -71,6 +77,7 @@ extern lean_object* l_Lean_Parser_Term_pow___elambda__1___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMod(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabIff___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSub___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1; lean_object* l_Lean_Elab_Term_elabMul___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabModN___closed__4; lean_object* l_Lean_Elab_Term_elabseq(lean_object*, lean_object*, lean_object*, lean_object*); @@ -115,6 +122,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapConstRev(lean_object*) lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen___closed__3; lean_object* l_Lean_Elab_Term_elabMapRev(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAdd___closed__3; +extern lean_object* l_Lean_Parser_Term_prod___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMapConst___closed__1; lean_object* l_Lean_Elab_Term_elabOrElse___closed__3; extern lean_object* l_Lean_Parser_Term_or___elambda__1___closed__2; @@ -140,6 +148,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabSub(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__2; lean_object* l_Lean_Elab_Term_elabAppend(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2; extern lean_object* l_Lean_Parser_Term_or___elambda__1___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqLeft___closed__1; extern lean_object* l_Lean_Parser_Term_ne___elambda__1___closed__2; @@ -161,6 +170,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEq(lean_object*); lean_object* l_Lean_Elab_Term_elabLE___closed__1; lean_object* lean_array_get(lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__1; +lean_object* l_Lean_Elab_Term_ElabFComp___closed__4; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd___closed__2; lean_object* l_Lean_Elab_Term_elabDiv___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabLE___boxed(lean_object*, lean_object*, lean_object*, lean_object*); @@ -168,17 +178,23 @@ lean_object* l_Lean_Elab_Term_elabOrElse(lean_object*, lean_object*, lean_object lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabCons(lean_object*); extern lean_object* l_Lean_Parser_Term_equiv___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_elabDiv___closed__1; +lean_object* l_Lean_Elab_Term_elabBind(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabEquiv___closed__3; +lean_object* l_Lean_Elab_Term_ElabFComp(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__3; +lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_mod___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_elabMapRev___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1; lean_object* l_Lean_Elab_Term_elabSub(lean_object*, lean_object*, lean_object*, lean_object*); +extern lean_object* l_Lean_Parser_Term_fcomp___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_elabMapRev___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabMod___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAnd___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__1; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp(lean_object*); lean_object* l_Lean_Elab_Term_elabLE___closed__2; lean_object* l_Lean_Elab_Term_elabseqRight___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBOr___closed__3; @@ -267,10 +283,12 @@ extern lean_object* l_Lean_Parser_Term_le___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMod___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDiv___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend(lean_object*); +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3; lean_object* l_Lean_Elab_Term_elabAnd___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEq___closed__2; extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteList___main___closed__6; lean_object* l_Array_iterateMAux___main___at_Lean_mkAppStx___spec__1(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBind(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabGT___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndM___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAdd___closed__1; @@ -282,6 +300,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqLeft___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBOr(lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabDollar___closed__1; +lean_object* l_Lean_Elab_Term_elabBind___closed__3; lean_object* l_Lean_Elab_Term_elabLE___closed__4; lean_object* l_Lean_Elab_Term_elabOrM___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabIff___closed__1; @@ -297,12 +316,15 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBNe___closed__2; extern lean_object* l_Lean_Elab_Term_declareBuiltinTermElab___closed__4; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBAnd___closed__1; lean_object* l_Lean_Elab_Term_elabInfix___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l_Lean_Elab_Term_ElabFComp___boxed(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__1; +lean_object* l_Lean_Elab_Term_ElabFComp___closed__1; lean_object* l_Lean_Elab_Term_elabBEq(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_pow___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabModN___closed__1; extern lean_object* l_Lean_Parser_Term_cons___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM___closed__3; +lean_object* l_Lean_Elab_Term_ElabFComp___closed__3; lean_object* l_Lean_Elab_Term_elabAndThen___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabseqRight___closed__2; extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__2; @@ -336,15 +358,18 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabMul___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNe___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLT___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabModN___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProd(lean_object*); extern lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_elabCons(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabMod(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr___closed__1; extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__2; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2; extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__2; lean_object* l_Lean_Elab_Term_elabBEq___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLT___closed__2; lean_object* l_Lean_Elab_Term_elabBNe___closed__1; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1; lean_object* l_Lean_Elab_Term_elabBNe___boxed(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabSub___closed__1; lean_object* l_Lean_Elab_Term_elabMap(lean_object*, lean_object*, lean_object*, lean_object*); @@ -355,7 +380,10 @@ extern lean_object* l_Lean_Parser_Term_bne___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_elabDollar(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_map___elambda__1___closed__1; lean_object* l_Lean_Elab_Term_elabAndThen(lean_object*, lean_object*, lean_object*, lean_object*); +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3; +extern lean_object* l_Lean_Parser_Term_bindOp___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabLE___closed__1; +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2; extern lean_object* l_Lean_Parser_Term_modN___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabEquiv___closed__3; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAndM___closed__1; @@ -364,7 +392,9 @@ extern lean_object* l_Lean_Parser_Term_and___elambda__1___closed__1; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOrM(lean_object*); lean_object* l_Lean_Elab_Term_elabNe(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_orelse___elambda__1___closed__1; +lean_object* l_Lean_Elab_Term_ElabFComp___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabOr(lean_object*); +lean_object* l_Lean_Elab_Term_elabProd(lean_object*, lean_object*, lean_object*, lean_object*); lean_object* l_Lean_Elab_Term_elabSub___boxed(lean_object*, lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_Parser_Term_dollar___elambda__1___closed__2; lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabNe___closed__1; @@ -497,6 +527,152 @@ lean_dec(x_2); return x_6; } } +lean_object* l_Lean_Elab_Term_elabProd(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; lean_object* x_6; +x_5 = l_List_map___main___at___private_Init_Lean_Elab_Quotation_7__quote___main___spec__11___closed__2; +x_6 = l_Lean_Elab_Term_elabInfixOp(x_5, x_1, x_2, x_3, x_4); +return x_6; +} +} +lean_object* l_Lean_Elab_Term_elabProd___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l_Lean_Elab_Term_elabProd(x_1, x_2, x_3, x_4); +lean_dec(x_1); +return x_5; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("elabProd"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__4; +x_2 = l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabProd___boxed), 4, 0); +return x_1; +} +} +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabProd(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_Term_prod___elambda__1___closed__2; +x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2; +x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3; +x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1); +return x_5; +} +} +lean_object* _init_l_Lean_Elab_Term_ElabFComp___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("Function"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_ElabFComp___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_ElabFComp___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Term_ElabFComp___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("comp"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_ElabFComp___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_ElabFComp___closed__2; +x_2 = l_Lean_Elab_Term_ElabFComp___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Elab_Term_ElabFComp(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; lean_object* x_6; +x_5 = l_Lean_Elab_Term_ElabFComp___closed__4; +x_6 = l_Lean_Elab_Term_elabInfixOp(x_5, x_1, x_2, x_3, x_4); +return x_6; +} +} +lean_object* l_Lean_Elab_Term_ElabFComp___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l_Lean_Elab_Term_ElabFComp(x_1, x_2, x_3, x_4); +lean_dec(x_1); +return x_5; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("ElabFComp"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__4; +x_2 = l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_ElabFComp___boxed), 4, 0); +return x_1; +} +} +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_Term_fcomp___elambda__1___closed__2; +x_3 = l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2; +x_4 = l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3; +x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* _init_l_Lean_Elab_Term_elabAdd___closed__1() { _start: { @@ -2388,6 +2564,97 @@ x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1); return x_5; } } +lean_object* _init_l_Lean_Elab_Term_elabBind___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("HasBind"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_elabBind___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = lean_box(0); +x_2 = l_Lean_Elab_Term_elabBind___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l_Lean_Elab_Term_elabBind___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("bind"); +return x_1; +} +} +lean_object* _init_l_Lean_Elab_Term_elabBind___closed__4() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_elabBind___closed__2; +x_2 = l_Lean_Elab_Term_elabBind___closed__3; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* l_Lean_Elab_Term_elabBind(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; lean_object* x_6; +x_5 = l_Lean_Elab_Term_elabBind___closed__4; +x_6 = l_Lean_Elab_Term_elabInfixOp(x_5, x_1, x_2, x_3, x_4); +return x_6; +} +} +lean_object* l_Lean_Elab_Term_elabBind___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) { +_start: +{ +lean_object* x_5; +x_5 = l_Lean_Elab_Term_elabBind(x_1, x_2, x_3, x_4); +lean_dec(x_1); +return x_5; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1() { +_start: +{ +lean_object* x_1; +x_1 = lean_mk_string("elabBind"); +return x_1; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2() { +_start: +{ +lean_object* x_1; lean_object* x_2; lean_object* x_3; +x_1 = l_Lean_Elab_Term_declareBuiltinTermElab___closed__4; +x_2 = l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1; +x_3 = lean_name_mk_string(x_1, x_2); +return x_3; +} +} +lean_object* _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3() { +_start: +{ +lean_object* x_1; +x_1 = lean_alloc_closure((void*)(l_Lean_Elab_Term_elabBind___boxed), 4, 0); +return x_1; +} +} +lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabBind(lean_object* x_1) { +_start: +{ +lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; +x_2 = l_Lean_Parser_Term_bindOp___elambda__1___closed__2; +x_3 = l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2; +x_4 = l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3; +x_5 = l_Lean_Elab_Term_addBuiltinTermElab(x_2, x_3, x_4, x_1); +return x_5; +} +} lean_object* _init_l_Lean_Elab_Term_elabseq___closed__1() { _start: { @@ -3146,6 +3413,32 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabDollar___closed__ res = l___regBuiltinTermElab_Lean_Elab_Term_elabDollar(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__1); +l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__2); +l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabProd___closed__3); +res = l___regBuiltinTermElab_Lean_Elab_Term_elabProd(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); +l_Lean_Elab_Term_ElabFComp___closed__1 = _init_l_Lean_Elab_Term_ElabFComp___closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_ElabFComp___closed__1); +l_Lean_Elab_Term_ElabFComp___closed__2 = _init_l_Lean_Elab_Term_ElabFComp___closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_ElabFComp___closed__2); +l_Lean_Elab_Term_ElabFComp___closed__3 = _init_l_Lean_Elab_Term_ElabFComp___closed__3(); +lean_mark_persistent(l_Lean_Elab_Term_ElabFComp___closed__3); +l_Lean_Elab_Term_ElabFComp___closed__4 = _init_l_Lean_Elab_Term_ElabFComp___closed__4(); +lean_mark_persistent(l_Lean_Elab_Term_ElabFComp___closed__4); +l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__1); +l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__2); +l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp___closed__3); +res = l___regBuiltinTermElab_Lean_Elab_Term_ElabFComp(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Elab_Term_elabAdd___closed__1 = _init_l_Lean_Elab_Term_elabAdd___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_elabAdd___closed__1); l___regBuiltinTermElab_Lean_Elab_Term_elabAdd___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabAdd___closed__1(); @@ -3483,6 +3776,23 @@ lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen___closed_ res = l___regBuiltinTermElab_Lean_Elab_Term_elabAndThen(lean_io_mk_world()); if (lean_io_result_is_error(res)) return res; lean_dec_ref(res); +l_Lean_Elab_Term_elabBind___closed__1 = _init_l_Lean_Elab_Term_elabBind___closed__1(); +lean_mark_persistent(l_Lean_Elab_Term_elabBind___closed__1); +l_Lean_Elab_Term_elabBind___closed__2 = _init_l_Lean_Elab_Term_elabBind___closed__2(); +lean_mark_persistent(l_Lean_Elab_Term_elabBind___closed__2); +l_Lean_Elab_Term_elabBind___closed__3 = _init_l_Lean_Elab_Term_elabBind___closed__3(); +lean_mark_persistent(l_Lean_Elab_Term_elabBind___closed__3); +l_Lean_Elab_Term_elabBind___closed__4 = _init_l_Lean_Elab_Term_elabBind___closed__4(); +lean_mark_persistent(l_Lean_Elab_Term_elabBind___closed__4); +l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__1); +l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__2); +l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3 = _init_l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3(); +lean_mark_persistent(l___regBuiltinTermElab_Lean_Elab_Term_elabBind___closed__3); +res = l___regBuiltinTermElab_Lean_Elab_Term_elabBind(lean_io_mk_world()); +if (lean_io_result_is_error(res)) return res; +lean_dec_ref(res); l_Lean_Elab_Term_elabseq___closed__1 = _init_l_Lean_Elab_Term_elabseq___closed__1(); lean_mark_persistent(l_Lean_Elab_Term_elabseq___closed__1); l_Lean_Elab_Term_elabseq___closed__2 = _init_l_Lean_Elab_Term_elabseq___closed__2(); diff --git a/stage0/stdlib/Init/Lean/Meta/Instances.c b/stage0/stdlib/Init/Lean/Meta/Instances.c index 3dcff52a74..f8712b0b95 100644 --- a/stage0/stdlib/Init/Lean/Meta/Instances.c +++ b/stage0/stdlib/Init/Lean/Meta/Instances.c @@ -63,7 +63,7 @@ lean_object* l_Lean_Meta_instanceExtension___elambda__4___rarg(lean_object*); extern lean_object* l_Lean_AttributeImpl_inhabited___closed__4; lean_object* l_Lean_Environment_getGlobalInstances___boxed(lean_object*); lean_object* l_Lean_Meta_mkInstanceExtension___closed__5; -lean_object* l_Lean_Meta_addGlobalInstance(lean_object*, lean_object*, lean_object*); +lean_object* lean_add_instance(lean_object*, lean_object*, lean_object*); extern lean_object* l_Lean_LocalContext_Inhabited___closed__2; lean_object* l_PersistentHashMap_find___at_Lean_Meta_addInstanceEntry___spec__2(lean_object*, lean_object*); lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean_object*, lean_object*, lean_object*); @@ -107,7 +107,7 @@ lean_object* l_Lean_Meta_instanceExtension___closed__1; lean_object* l_Lean_Meta_registerInstanceAttr___closed__6; lean_object* l_Lean_Meta_instanceExtension___closed__2; lean_object* l_Lean_Meta_registerInstanceAttr___lambda__1___closed__2; -lean_object* lean_add_instance(lean_object*, lean_object*); +lean_object* lean_add_instance_old(lean_object*, lean_object*); lean_object* l_Lean_PersistentEnvExtension_addEntry___rarg(lean_object*, lean_object*, lean_object*); size_t l_USize_land(size_t, size_t); lean_object* l_Lean_Meta_addGlobalInstance___closed__2; @@ -3207,7 +3207,7 @@ lean_ctor_set(x_4, 2, x_3); return x_4; } } -lean_object* l_Lean_Meta_addGlobalInstance(lean_object* x_1, lean_object* x_2, lean_object* x_3) { +lean_object* lean_add_instance(lean_object* x_1, lean_object* x_2, lean_object* x_3) { _start: { lean_object* x_4; @@ -3374,7 +3374,7 @@ else { lean_object* x_11; lean_object* x_12; lean_inc(x_2); -x_11 = lean_add_instance(x_1, x_2); +x_11 = lean_add_instance_old(x_1, x_2); x_12 = l_IO_ofExcept___at_Lean_registerClassAttr___spec__1(x_11, x_5); lean_dec(x_11); if (lean_obj_tag(x_12) == 0) @@ -3385,7 +3385,7 @@ lean_inc(x_13); x_14 = lean_ctor_get(x_12, 1); lean_inc(x_14); lean_dec(x_12); -x_15 = l_Lean_Meta_addGlobalInstance(x_13, x_2, x_14); +x_15 = lean_add_instance(x_13, x_2, x_14); return x_15; } else