max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-11 17:20:43 -08:00
parent b773bb9ceb
commit acccfdfbd5
7 changed files with 330 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Lean/Class.lean
View file

@ -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 ++ "'")

6
stage0/src/Init/Lean/Elab/BuiltinNotation.lean
View file

@ -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
-/

1
stage0/src/Init/Lean/Meta/Instances.lean
View file

@ -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"

8
stage0/src/library/class.cpp
View file

@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <string>
#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<environment>(lean_add_instance(env.to_obj_arg(), n.to_obj_arg()));
environment new_env = get_except_value<environment>(lean_add_instance_old(env.to_obj_arg(), n.to_obj_arg()));
new_env = get_io_result<environment>(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;

4
stage0/stdlib/Init/Lean/Class.c
View file

@ -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;

310
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

@ -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();

10
stage0/stdlib/Init/Lean/Meta/Instances.c
View file

@ -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