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 2020-01-23 11:47:07 -08:00
parent 4ef8aa347a
commit aef998af72
4 changed files with 895 additions and 583 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
stage0/src/Init/Lean/Elab/Quotation.lean
View file

@ -106,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
let val := quote val;
-- `scp` is bound in stxQuot.expand
`(Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved))
`(Syntax.ident none $(quote rawVal) (addMacroScopeExt mainModule $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k args) =>
if isAntiquot stx then
@ -137,7 +137,7 @@ let quoted := stx.getArg 1;
including it literally in a syntax quotation. -/
-- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted))
stx ← quoteSyntax (elimAntiquotChoices quoted);
`(bind getCurrMacroScope (fun scp => pure $stx))
`(bind getCurrMacroScope (fun scp => bind getMainModule (fun mainModule => pure $stx)))
/- NOTE: It may seem like the newly introduced binding `scp` may accidentally
capture identifiers in an antiquotation introduced by `quoteSyntax`. However,
note that the syntax quotation above enjoys the same hygiene guarantees as

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

@ -318,6 +318,7 @@ lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabAppend___closed__3;
lean_object* l_Lean_Elab_Term_elabLE(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabDollar___closed__1;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__31;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
lean_object* l_Lean_Elab_Term_elabOr___closed__1;
extern lean_object* l_Lean_mkAppStx___closed__6;
lean_object* l_Lean_Elab_Term_elabTParserMacro___lambda__1___closed__3;
@ -500,7 +501,6 @@ lean_object* l_Lean_Elab_Term_elabGT___boxed(lean_object*, lean_object*, lean_ob
lean_object* l___regBuiltinTermElab_Lean_Elab_Term_elabHEq___closed__3;
extern lean_object* l_Lean_Parser_Term_mapConst___elambda__1___closed__2;
lean_object* l_Lean_Elab_Term_elabParserMacro___lambda__1___closed__15;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
lean_object* l_Lean_Elab_Term_elabHEq___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_elabOrM(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_addBuiltinTermElab(lean_object*, lean_object*, lean_object*, lean_object*);
@ -1449,7 +1449,7 @@ lean_ctor_set(x_118, 0, x_69);
lean_ctor_set(x_118, 1, x_117);
x_119 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_120 = lean_array_push(x_119, x_118);
x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_121 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_122 = lean_array_push(x_120, x_121);
x_123 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_124 = lean_alloc_ctor(1, 2, 0);
@ -1537,7 +1537,7 @@ lean_ctor_set(x_170, 0, x_69);
lean_ctor_set(x_170, 1, x_169);
x_171 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_172 = lean_array_push(x_171, x_170);
x_173 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_173 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_174 = lean_array_push(x_172, x_173);
x_175 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_176 = lean_alloc_ctor(1, 2, 0);
@ -1895,7 +1895,7 @@ lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_42 = lean_array_push(x_41, x_40);
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_44 = lean_array_push(x_42, x_43);
x_45 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_46 = lean_alloc_ctor(1, 2, 0);
@ -1978,7 +1978,7 @@ lean_ctor_set(x_90, 0, x_89);
lean_ctor_set(x_90, 1, x_88);
x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_92 = lean_array_push(x_91, x_90);
x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_93 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_94 = lean_array_push(x_92, x_93);
x_95 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_96 = lean_alloc_ctor(1, 2, 0);
@ -2147,7 +2147,7 @@ lean_ctor_set(x_164, 0, x_119);
lean_ctor_set(x_164, 1, x_163);
x_165 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_166 = lean_array_push(x_165, x_164);
x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_167 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_168 = lean_array_push(x_166, x_167);
x_169 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_170 = lean_alloc_ctor(1, 2, 0);
@ -2238,7 +2238,7 @@ lean_ctor_set(x_218, 0, x_119);
lean_ctor_set(x_218, 1, x_217);
x_219 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_220 = lean_array_push(x_219, x_218);
x_221 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_221 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_222 = lean_array_push(x_220, x_221);
x_223 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_224 = lean_alloc_ctor(1, 2, 0);
@ -2953,7 +2953,7 @@ lean_ctor_set(x_30, 0, x_27);
lean_ctor_set(x_30, 1, x_29);
x_31 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_32 = lean_array_push(x_31, x_30);
x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_33 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_34 = lean_array_push(x_32, x_33);
x_35 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_36 = lean_alloc_ctor(1, 2, 0);
@ -3022,7 +3022,7 @@ lean_ctor_set(x_70, 0, x_67);
lean_ctor_set(x_70, 1, x_69);
x_71 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_72 = lean_array_push(x_71, x_70);
x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_73 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_74 = lean_array_push(x_72, x_73);
x_75 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_76 = lean_alloc_ctor(1, 2, 0);
@ -3298,7 +3298,7 @@ lean_ctor_set(x_42, 0, x_39);
lean_ctor_set(x_42, 1, x_41);
x_43 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_44 = lean_array_push(x_43, x_42);
x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_45 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_46 = lean_array_push(x_44, x_45);
x_47 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_48 = lean_alloc_ctor(1, 2, 0);
@ -3372,7 +3372,7 @@ lean_ctor_set(x_86, 0, x_83);
lean_ctor_set(x_86, 1, x_85);
x_87 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_88 = lean_array_push(x_87, x_86);
x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_90 = lean_array_push(x_88, x_89);
x_91 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_92 = lean_alloc_ctor(1, 2, 0);
@ -3488,7 +3488,7 @@ lean_ctor_set(x_145, 0, x_142);
lean_ctor_set(x_145, 1, x_144);
x_146 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_147 = lean_array_push(x_146, x_145);
x_148 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_148 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_149 = lean_array_push(x_147, x_148);
x_150 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_151 = lean_alloc_ctor(1, 2, 0);
@ -3562,7 +3562,7 @@ lean_ctor_set(x_189, 0, x_186);
lean_ctor_set(x_189, 1, x_188);
x_190 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_191 = lean_array_push(x_190, x_189);
x_192 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_192 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_193 = lean_array_push(x_191, x_192);
x_194 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_195 = lean_alloc_ctor(1, 2, 0);
@ -3713,7 +3713,7 @@ lean_ctor_set(x_259, 0, x_226);
lean_ctor_set(x_259, 1, x_258);
x_260 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_261 = lean_array_push(x_260, x_259);
x_262 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_262 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_263 = lean_array_push(x_261, x_262);
x_264 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_265 = lean_alloc_ctor(1, 2, 0);
@ -3780,7 +3780,7 @@ lean_ctor_set(x_298, 0, x_226);
lean_ctor_set(x_298, 1, x_297);
x_299 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_300 = lean_array_push(x_299, x_298);
x_301 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_301 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_302 = lean_array_push(x_300, x_301);
x_303 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_304 = lean_alloc_ctor(1, 2, 0);
@ -3891,7 +3891,7 @@ lean_ctor_set(x_354, 0, x_226);
lean_ctor_set(x_354, 1, x_353);
x_355 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_356 = lean_array_push(x_355, x_354);
x_357 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_357 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_358 = lean_array_push(x_356, x_357);
x_359 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_360 = lean_alloc_ctor(1, 2, 0);
@ -3958,7 +3958,7 @@ lean_ctor_set(x_393, 0, x_226);
lean_ctor_set(x_393, 1, x_392);
x_394 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_395 = lean_array_push(x_394, x_393);
x_396 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_396 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_397 = lean_array_push(x_395, x_396);
x_398 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_399 = lean_alloc_ctor(1, 2, 0);
@ -4814,7 +4814,7 @@ lean_ctor_set(x_88, 0, x_46);
lean_ctor_set(x_88, 1, x_87);
x_89 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_90 = lean_array_push(x_89, x_88);
x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_91 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_92 = lean_array_push(x_90, x_91);
x_93 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_94 = lean_alloc_ctor(1, 2, 0);
@ -4902,7 +4902,7 @@ lean_ctor_set(x_135, 0, x_46);
lean_ctor_set(x_135, 1, x_134);
x_136 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_137 = lean_array_push(x_136, x_135);
x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_138 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_139 = lean_array_push(x_137, x_138);
x_140 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_141 = lean_alloc_ctor(1, 2, 0);
@ -4995,7 +4995,7 @@ lean_ctor_set(x_184, 0, x_46);
lean_ctor_set(x_184, 1, x_183);
x_185 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_186 = lean_array_push(x_185, x_184);
x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_187 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_188 = lean_array_push(x_186, x_187);
x_189 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_190 = lean_alloc_ctor(1, 2, 0);
@ -5101,7 +5101,7 @@ lean_ctor_set(x_241, 0, x_46);
lean_ctor_set(x_241, 1, x_240);
x_242 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__43;
x_243 = lean_array_push(x_242, x_241);
x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_244 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_245 = lean_array_push(x_243, x_244);
x_246 = l___private_Init_Lean_Parser_Parser_12__antiquotNestedExpr___elambda__1___rarg___closed__2;
x_247 = lean_alloc_ctor(1, 2, 0);

1418
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

@ -266,6 +266,7 @@ lean_object* l_Array_iterateMAux___main___at___private_Init_Lean_Elab_Syntax_2__
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__93;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__121;
lean_object* l___private_Init_Lean_Elab_Command_6__mkTermContext(lean_object*, lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
lean_object* l_Lean_Elab_Command_elabSyntax___closed__28;
extern lean_object* l_Lean_Elab_Term_elabArrow___lambda__1___closed__6;
extern lean_object* l_Lean_Parser_Term_match__syntax___elambda__1___closed__1;
@ -427,7 +428,6 @@ lean_object* l_Lean_Elab_Command_elabSyntax___closed__13;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__57;
lean_object* l___private_Init_Lean_Elab_Syntax_5__withNoPushLeading___rarg(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__122;
extern lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__94;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__8;
lean_object* l_Lean_Elab_Term_toParserDescrAux___main___closed__65;
@ -11767,7 +11767,7 @@ lean_ctor_set(x_50, 1, x_48);
x_51 = lean_array_push(x_42, x_50);
x_52 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_53 = lean_array_push(x_52, x_29);
x_54 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_54 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_55 = lean_array_push(x_53, x_54);
x_56 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_57 = lean_alloc_ctor(1, 2, 0);
@ -11843,7 +11843,7 @@ lean_ctor_set(x_96, 1, x_94);
x_97 = lean_array_push(x_88, x_96);
x_98 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_99 = lean_array_push(x_98, x_29);
x_100 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_100 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_101 = lean_array_push(x_99, x_100);
x_102 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_103 = lean_alloc_ctor(1, 2, 0);
@ -12751,7 +12751,7 @@ lean_ctor_set(x_60, 1, x_58);
x_61 = lean_array_push(x_52, x_60);
x_62 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_63 = lean_array_push(x_62, x_34);
x_64 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_64 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_65 = lean_array_push(x_63, x_64);
x_66 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_67 = lean_alloc_ctor(1, 2, 0);
@ -12826,7 +12826,7 @@ lean_ctor_set(x_106, 1, x_104);
x_107 = lean_array_push(x_98, x_106);
x_108 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_109 = lean_array_push(x_108, x_34);
x_110 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_110 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_111 = lean_array_push(x_109, x_110);
x_112 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_113 = lean_alloc_ctor(1, 2, 0);
@ -12911,7 +12911,7 @@ lean_ctor_set(x_157, 1, x_155);
x_158 = lean_array_push(x_149, x_157);
x_159 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_160 = lean_array_push(x_159, x_34);
x_161 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_161 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_162 = lean_array_push(x_160, x_161);
x_163 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_164 = lean_alloc_ctor(1, 2, 0);
@ -12981,7 +12981,7 @@ lean_ctor_set(x_200, 1, x_198);
x_201 = lean_array_push(x_192, x_200);
x_202 = l_Lean_Elab_Command_elabNotation___lambda__1___closed__6;
x_203 = lean_array_push(x_202, x_34);
x_204 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__55;
x_204 = l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__59;
x_205 = lean_array_push(x_203, x_204);
x_206 = l_Lean_Parser_Term_stxQuot___elambda__1___closed__2;
x_207 = lean_alloc_ctor(1, 2, 0);