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 2022-04-01 11:24:22 -07:00
parent 799c701f56
commit 16b2237d2d
18 changed files with 806 additions and 806 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Init/Conv.lean generated
View file

@ -55,7 +55,7 @@ macro "intro " xs:(colGt ident)* : conv => `(ext $(xs.getArgs)*)
syntax enterArg := ident <|> num
syntax "enter " "[" (colGt enterArg),+ "]": conv
macro_rules
| `(conv| enter [$i:numLit]) => `(conv| arg $i)
| `(conv| enter [$i:num]) => `(conv| arg $i)
| `(conv| enter [$id:ident]) => `(conv| ext $id)
| `(conv| enter [$arg:enterArg, $args,*]) => `(conv| (enter [$arg]; enter [$args,*]))

14
stage0/src/Init/Meta.lean generated
View file

@ -837,14 +837,14 @@ def evalPrec (stx : Syntax) : MacroM Nat :=
Macro.withIncRecDepth stx do
let stx ← expandMacros stx
match stx with
| `(prec| $num:numLit) => return num.isNatLit?.getD 0
| `(prec| $num:num) => return num.isNatLit?.getD 0
| _ => Macro.throwErrorAt stx "unexpected precedence"
macro_rules
| `(prec| $a + $b) => do `(prec| $(quote <| (← evalPrec a) + (← evalPrec b)):numLit)
| `(prec| $a + $b) => do `(prec| $(quote <| (← evalPrec a) + (← evalPrec b)):num)
macro_rules
| `(prec| $a - $b) => do `(prec| $(quote <| (← evalPrec a) - (← evalPrec b)):numLit)
| `(prec| $a - $b) => do `(prec| $(quote <| (← evalPrec a) - (← evalPrec b)):num)
macro "eval_prec " p:prec:max : term => return quote (← evalPrec p)
@ -853,20 +853,20 @@ def evalPrio (stx : Syntax) : MacroM Nat :=
Macro.withIncRecDepth stx do
let stx ← expandMacros stx
match stx with
| `(prio| $num:numLit) => return num.isNatLit?.getD 0
| `(prio| $num:num) => return num.isNatLit?.getD 0
| _ => Macro.throwErrorAt stx "unexpected priority"
macro_rules
| `(prio| $a + $b) => do `(prio| $(quote <| (← evalPrio a) + (← evalPrio b)):numLit)
| `(prio| $a + $b) => do `(prio| $(quote <| (← evalPrio a) + (← evalPrio b)):num)
macro_rules
| `(prio| $a - $b) => do `(prio| $(quote <| (← evalPrio a) - (← evalPrio b)):numLit)
| `(prio| $a - $b) => do `(prio| $(quote <| (← evalPrio a) - (← evalPrio b)):num)
macro "eval_prio " p:prio:max : term => return quote (← evalPrio p)
def evalOptPrio : Option Syntax → MacroM Nat
| some prio => evalPrio prio
| none => return eval_prio default
| none => return 1000 -- TODO: FIX back eval_prio default
end Lean

10
stage0/src/Init/Prelude.lean generated
View file

@ -1847,11 +1847,11 @@ def choiceKind : SyntaxNodeKind := `choice
def nullKind : SyntaxNodeKind := `null
def groupKind : SyntaxNodeKind := `group
def identKind : SyntaxNodeKind := `ident
def strLitKind : SyntaxNodeKind := `strLit
def charLitKind : SyntaxNodeKind := `charLit
def numLitKind : SyntaxNodeKind := `numLit
def scientificLitKind : SyntaxNodeKind := `scientificLit
def nameLitKind : SyntaxNodeKind := `nameLit
def strLitKind : SyntaxNodeKind := `str
def charLitKind : SyntaxNodeKind := `char
def numLitKind : SyntaxNodeKind := `num
def scientificLitKind : SyntaxNodeKind := `scientific
def nameLitKind : SyntaxNodeKind := `name
def fieldIdxKind : SyntaxNodeKind := `fieldIdx
def interpolatedStrLitKind : SyntaxNodeKind := `interpolatedStrLitKind
def interpolatedStrKind : SyntaxNodeKind := `interpolatedStrKind

2
stage0/src/Lean/Elab/DefView.lean generated
View file

@ -108,7 +108,7 @@ def mkDefViewOfInstance (modifiers : Modifiers) (stx : Syntax) : CommandElabM De
-- leading_parser Term.attrKind >> "instance " >> optNamedPrio >> optional declId >> declSig >> declVal
let attrKind ← liftMacroM <| toAttributeKind stx[0]
let prio ← liftMacroM <| expandOptNamedPrio stx[2]
let attrStx ← `(attr| instance $(quote prio):numLit)
let attrStx ← `(attr| instance $(quote prio):num)
let (binders, type) := expandDeclSig stx[4]
let modifiers := modifiers.addAttribute { kind := attrKind, name := `instance, stx := attrStx }
let declId ← match stx[3].getOptional? with

8
stage0/src/Lean/Elab/MacroArgUtil.lean generated
View file

@ -17,14 +17,14 @@ def expandMacroArg (stx : Syntax) : MacroM (Syntax × Syntax) := do
| `(macroArg| $stx:stx) => pure (none, (← `(x)), stx)
| _ => Macro.throwUnsupported
let pat ← match stx with
| `(stx| $s:strLit) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| &$s:strLit) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| $s:str) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| &$s:str) => pure <| mkNode `token_antiquot #[← strLitToPattern s, mkAtom "%", mkAtom "$", id]
| `(stx| optional($stx)) => pure <| mkSplicePat `optional id "?"
| `(stx| many($stx)) => pure <| mkSplicePat `many id "*"
| `(stx| many1($stx)) => pure <| mkSplicePat `many id "*"
| `(stx| sepBy($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
| `(stx| sepBy($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| `(stx| sepBy1($stx, $sep:strLit $[, $stxsep]? $[, allowTrailingSep]?)) =>
| `(stx| sepBy1($stx, $sep:str $[, $stxsep]? $[, allowTrailingSep]?)) =>
pure <| mkSplicePat `sepBy id ((isStrLit? sep).get! ++ "*")
| _ => match id? with
-- if there is a binding, we assume the user knows what they are doing

10
stage0/src/Lean/Elab/Mixfix.lean generated
View file

@ -12,17 +12,17 @@ namespace Lean.Elab.Command
match stx with
| `(infixl:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
let prec1 := quote <| (← evalPrec prec) + 1
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec $op:strLit rhs:$prec1 => $f lhs rhs)
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec $op:str rhs:$prec1 => $f lhs rhs)
| `(infix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
let prec1 := quote <| (← evalPrec prec) + 1
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs:$prec1 => $f lhs rhs)
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:str rhs:$prec1 => $f lhs rhs)
| `(infixr:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
let prec1 := quote <| (← evalPrec prec) + 1
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:strLit rhs:$prec => $f lhs rhs)
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? lhs:$prec1 $op:str rhs:$prec => $f lhs rhs)
| `(prefix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? $op:strLit arg:$prec => $f arg)
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? $op:str arg:$prec => $f arg)
| `(postfix:$prec $[(name := $name)]? $[(priority := $prio)]? $op => $f) =>
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? arg:$prec $op:strLit => $f arg)
`(notation:$prec $[(name := $name)]? $[(priority := $prio)]? arg:$prec $op:str => $f arg)
| _ => Macro.throwUnsupported
where
-- set "global" `attrKind`, apply `f`, and restore `attrKind` to result

2
stage0/src/Lean/Elab/Notation.lean generated
View file

@ -90,7 +90,7 @@ private def expandNotationAux (ref : Syntax)
So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
let fullName := currNamespace ++ name
let pat := mkNode fullName patArgs
let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):numLit) $[$syntaxParts]* : $cat)
let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat)
let mut macroDecl ← `(macro_rules | `($pat) => ``($qrhs))
if isLocalAttrKind attrKind then
-- Make sure the quotation pre-checker takes section variables into account for local notation.

2
stage0/src/Lean/Elab/Print.lean generated
View file

@ -83,7 +83,7 @@ private def printId (id : Syntax) : CommandElabM Unit := do
@[builtinCommandElab «print»] def elabPrint : CommandElab
| `(#print%$tk $id:ident) => withRef tk <| printId id
| `(#print%$tk $s:strLit) => logInfoAt tk s.isStrLit?.get!
| `(#print%$tk $s:str) => logInfoAt tk s.isStrLit?.get!
| _ => throwError "invalid #print command"
namespace CollectAxioms

4
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -323,10 +323,10 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
let declName := mkIdentFrom stx name
let d ←
if let some lhsPrec := lhsPrec? then
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.TrailingParserDescr :=
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.TrailingParserDescr :=
ParserDescr.trailingNode $(quote stxNodeKind) $(quote prec) $(quote lhsPrec) $val)
else
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):numLit] def $declName:ident : Lean.ParserDescr :=
`($[$doc?:docComment]? @[$attrKind:attrKind $catParserId:ident $(quote prio):num] def $declName:ident : Lean.ParserDescr :=
ParserDescr.node $(quote stxNodeKind) $(quote prec) $val)
trace `Elab fun _ => d
withMacroExpansion stx d <| elabCommand d

10
stage0/src/Lean/Parser/Basic.lean generated
View file

@ -1272,7 +1272,7 @@ def numLitFn : ParserFn :=
@[inline] def numLitNoAntiquot : Parser := {
fn := numLitFn,
info := mkAtomicInfo "numLit"
info := mkAtomicInfo "num"
}
def scientificLitFn : ParserFn :=
@ -1284,7 +1284,7 @@ def scientificLitFn : ParserFn :=
@[inline] def scientificLitNoAntiquot : Parser := {
fn := scientificLitFn,
info := mkAtomicInfo "scientificLit"
info := mkAtomicInfo "scientific"
}
def strLitFn : ParserFn := fun c s =>
@ -1295,7 +1295,7 @@ def strLitFn : ParserFn := fun c s =>
@[inline] def strLitNoAntiquot : Parser := {
fn := strLitFn,
info := mkAtomicInfo "strLit"
info := mkAtomicInfo "str"
}
def charLitFn : ParserFn := fun c s =>
@ -1306,7 +1306,7 @@ def charLitFn : ParserFn := fun c s =>
@[inline] def charLitNoAntiquot : Parser := {
fn := charLitFn,
info := mkAtomicInfo "charLit"
info := mkAtomicInfo "char"
}
def nameLitFn : ParserFn := fun c s =>
@ -1317,7 +1317,7 @@ def nameLitFn : ParserFn := fun c s =>
@[inline] def nameLitNoAntiquot : Parser := {
fn := nameLitFn,
info := mkAtomicInfo "nameLit"
info := mkAtomicInfo "name"
}
def identFn : ParserFn := fun c s =>

10
stage0/src/Lean/Parser/Extra.lean generated
View file

@ -34,19 +34,19 @@ attribute [runBuiltinParserAttributeHooks]
withAntiquot (mkAntiquot "ident" identKind) rawIdentNoAntiquot
@[runBuiltinParserAttributeHooks] def numLit : Parser :=
withAntiquot (mkAntiquot "numLit" numLitKind) numLitNoAntiquot
withAntiquot (mkAntiquot "num" numLitKind) numLitNoAntiquot
@[runBuiltinParserAttributeHooks] def scientificLit : Parser :=
withAntiquot (mkAntiquot "scientificLit" scientificLitKind) scientificLitNoAntiquot
withAntiquot (mkAntiquot "scientific" scientificLitKind) scientificLitNoAntiquot
@[runBuiltinParserAttributeHooks] def strLit : Parser :=
withAntiquot (mkAntiquot "strLit" strLitKind) strLitNoAntiquot
withAntiquot (mkAntiquot "str" strLitKind) strLitNoAntiquot
@[runBuiltinParserAttributeHooks] def charLit : Parser :=
withAntiquot (mkAntiquot "charLit" charLitKind) charLitNoAntiquot
withAntiquot (mkAntiquot "char" charLitKind) charLitNoAntiquot
@[runBuiltinParserAttributeHooks] def nameLit : Parser :=
withAntiquot (mkAntiquot "nameLit" nameLitKind) nameLitNoAntiquot
withAntiquot (mkAntiquot "name" nameLitKind) nameLitNoAntiquot
@[runBuiltinParserAttributeHooks, inline] def group (p : Parser) : Parser :=
node groupKind p

750
stage0/stdlib/Init/Meta.c generated
View file

File diff suppressed because it is too large Load diff

66
stage0/stdlib/Init/Prelude.c generated
View file

@ -7319,7 +7319,7 @@ static lean_object* _init_l_Lean_strLitKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("strLit");
x_1 = lean_mk_string("str");
return x_1;
}
}
@ -7345,7 +7345,7 @@ static lean_object* _init_l_Lean_charLitKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("charLit");
x_1 = lean_mk_string("char");
return x_1;
}
}
@ -7371,7 +7371,7 @@ static lean_object* _init_l_Lean_numLitKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("numLit");
x_1 = lean_mk_string("num");
return x_1;
}
}
@ -7397,7 +7397,7 @@ static lean_object* _init_l_Lean_scientificLitKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("scientificLit");
x_1 = lean_mk_string("scientific");
return x_1;
}
}
@ -7423,7 +7423,7 @@ static lean_object* _init_l_Lean_nameLitKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("nameLit");
x_1 = lean_mk_string("name");
return x_1;
}
}
@ -7620,7 +7620,7 @@ static lean_object* _init_l_Lean_Syntax_isOfKind___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("num");
x_1 = lean_mk_string("numLit");
return x_1;
}
}
@ -7638,7 +7638,7 @@ static lean_object* _init_l_Lean_Syntax_isOfKind___closed__3() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("str");
x_1 = lean_mk_string("strLit");
return x_1;
}
}
@ -7656,7 +7656,7 @@ static lean_object* _init_l_Lean_Syntax_isOfKind___closed__5() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("char");
x_1 = lean_mk_string("charLit");
return x_1;
}
}
@ -7674,7 +7674,7 @@ static lean_object* _init_l_Lean_Syntax_isOfKind___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("name");
x_1 = lean_mk_string("nameLit");
return x_1;
}
}
@ -7692,42 +7692,42 @@ LEAN_EXPORT uint8_t l_Lean_Syntax_isOfKind(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; uint8_t x_4;
x_3 = l_Lean_Syntax_isOfKind___closed__2;
x_3 = l_Lean_numLitKind___closed__2;
x_4 = lean_name_eq(x_2, x_3);
if (x_4 == 0)
{
lean_object* x_5; uint8_t x_6;
x_5 = l_Lean_numLitKind___closed__2;
x_5 = l_Lean_Syntax_isOfKind___closed__2;
x_6 = lean_name_eq(x_2, x_5);
if (x_6 == 0)
{
lean_object* x_7; uint8_t x_8;
x_7 = l_Lean_Syntax_isOfKind___closed__4;
x_7 = l_Lean_strLitKind___closed__2;
x_8 = lean_name_eq(x_2, x_7);
if (x_8 == 0)
{
lean_object* x_9; uint8_t x_10;
x_9 = l_Lean_strLitKind___closed__2;
x_9 = l_Lean_Syntax_isOfKind___closed__4;
x_10 = lean_name_eq(x_2, x_9);
if (x_10 == 0)
{
lean_object* x_11; uint8_t x_12;
x_11 = l_Lean_Syntax_isOfKind___closed__6;
x_11 = l_Lean_charLitKind___closed__2;
x_12 = lean_name_eq(x_2, x_11);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14;
x_13 = l_Lean_charLitKind___closed__2;
x_13 = l_Lean_Syntax_isOfKind___closed__6;
x_14 = lean_name_eq(x_2, x_13);
if (x_14 == 0)
{
lean_object* x_15; uint8_t x_16;
x_15 = l_Lean_Syntax_isOfKind___closed__8;
x_15 = l_Lean_nameLitKind___closed__2;
x_16 = lean_name_eq(x_2, x_15);
if (x_16 == 0)
{
lean_object* x_17; uint8_t x_18;
x_17 = l_Lean_nameLitKind___closed__2;
x_17 = l_Lean_Syntax_isOfKind___closed__8;
x_18 = lean_name_eq(x_2, x_17);
if (x_18 == 0)
{
@ -7766,7 +7766,7 @@ x_26 = lean_name_eq(x_25, x_15);
if (x_26 == 0)
{
lean_object* x_27; uint8_t x_28;
x_27 = l_Lean_nameLitKind___closed__2;
x_27 = l_Lean_Syntax_isOfKind___closed__8;
x_28 = lean_name_eq(x_25, x_27);
lean_dec(x_25);
return x_28;
@ -7809,7 +7809,7 @@ x_35 = lean_name_eq(x_34, x_11);
if (x_35 == 0)
{
lean_object* x_36; uint8_t x_37;
x_36 = l_Lean_charLitKind___closed__2;
x_36 = l_Lean_Syntax_isOfKind___closed__6;
x_37 = lean_name_eq(x_34, x_36);
lean_dec(x_34);
return x_37;
@ -7852,7 +7852,7 @@ x_44 = lean_name_eq(x_43, x_7);
if (x_44 == 0)
{
lean_object* x_45; uint8_t x_46;
x_45 = l_Lean_strLitKind___closed__2;
x_45 = l_Lean_Syntax_isOfKind___closed__4;
x_46 = lean_name_eq(x_43, x_45);
lean_dec(x_43);
return x_46;
@ -7895,7 +7895,7 @@ x_53 = lean_name_eq(x_52, x_3);
if (x_53 == 0)
{
lean_object* x_54; uint8_t x_55;
x_54 = l_Lean_numLitKind___closed__2;
x_54 = l_Lean_Syntax_isOfKind___closed__2;
x_55 = lean_name_eq(x_52, x_54);
lean_dec(x_52);
return x_55;
@ -8276,42 +8276,42 @@ LEAN_EXPORT uint8_t l_Lean_Syntax_matchesLit(lean_object* x_1, lean_object* x_2,
_start:
{
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Syntax_isOfKind___closed__2;
x_4 = l_Lean_numLitKind___closed__2;
x_5 = lean_name_eq(x_2, x_4);
if (x_5 == 0)
{
lean_object* x_6; uint8_t x_7;
x_6 = l_Lean_numLitKind___closed__2;
x_6 = l_Lean_Syntax_isOfKind___closed__2;
x_7 = lean_name_eq(x_2, x_6);
if (x_7 == 0)
{
lean_object* x_8; uint8_t x_9;
x_8 = l_Lean_Syntax_isOfKind___closed__4;
x_8 = l_Lean_strLitKind___closed__2;
x_9 = lean_name_eq(x_2, x_8);
if (x_9 == 0)
{
lean_object* x_10; uint8_t x_11;
x_10 = l_Lean_strLitKind___closed__2;
x_10 = l_Lean_Syntax_isOfKind___closed__4;
x_11 = lean_name_eq(x_2, x_10);
if (x_11 == 0)
{
lean_object* x_12; uint8_t x_13;
x_12 = l_Lean_Syntax_isOfKind___closed__6;
x_12 = l_Lean_charLitKind___closed__2;
x_13 = lean_name_eq(x_2, x_12);
if (x_13 == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = l_Lean_charLitKind___closed__2;
x_14 = l_Lean_Syntax_isOfKind___closed__6;
x_15 = lean_name_eq(x_2, x_14);
if (x_15 == 0)
{
lean_object* x_16; uint8_t x_17;
x_16 = l_Lean_Syntax_isOfKind___closed__8;
x_16 = l_Lean_nameLitKind___closed__2;
x_17 = lean_name_eq(x_2, x_16);
if (x_17 == 0)
{
lean_object* x_18; uint8_t x_19;
x_18 = l_Lean_nameLitKind___closed__2;
x_18 = l_Lean_Syntax_isOfKind___closed__8;
x_19 = lean_name_eq(x_2, x_18);
if (x_19 == 0)
{
@ -8344,7 +8344,7 @@ x_24 = l_Lean_Syntax_matchesLitCore(x_1, x_16, x_3);
if (x_24 == 0)
{
lean_object* x_25; uint8_t x_26;
x_25 = l_Lean_nameLitKind___closed__2;
x_25 = l_Lean_Syntax_isOfKind___closed__8;
x_26 = l_Lean_Syntax_matchesLitCore(x_1, x_25, x_3);
return x_26;
}
@ -8381,7 +8381,7 @@ x_31 = l_Lean_Syntax_matchesLitCore(x_1, x_12, x_3);
if (x_31 == 0)
{
lean_object* x_32; uint8_t x_33;
x_32 = l_Lean_charLitKind___closed__2;
x_32 = l_Lean_Syntax_isOfKind___closed__6;
x_33 = l_Lean_Syntax_matchesLitCore(x_1, x_32, x_3);
return x_33;
}
@ -8418,7 +8418,7 @@ x_38 = l_Lean_Syntax_matchesLitCore(x_1, x_8, x_3);
if (x_38 == 0)
{
lean_object* x_39; uint8_t x_40;
x_39 = l_Lean_strLitKind___closed__2;
x_39 = l_Lean_Syntax_isOfKind___closed__4;
x_40 = l_Lean_Syntax_matchesLitCore(x_1, x_39, x_3);
return x_40;
}
@ -8455,7 +8455,7 @@ x_45 = l_Lean_Syntax_matchesLitCore(x_1, x_4, x_3);
if (x_45 == 0)
{
lean_object* x_46; uint8_t x_47;
x_46 = l_Lean_numLitKind___closed__2;
x_46 = l_Lean_Syntax_isOfKind___closed__2;
x_47 = l_Lean_Syntax_matchesLitCore(x_1, x_46, x_3);
return x_47;
}

12
stage0/stdlib/Lean/Meta/Basic.c generated
View file

@ -252,7 +252,7 @@ LEAN_EXPORT lean_object* l_Lean_Meta_forallMetaBoundedTelescope(lean_object*, le
LEAN_EXPORT lean_object* l_Lean_Meta_instMonadEnvMetaM___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_forallTelescopeReducingAuxAux_process___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Basic_0__Lean_Meta_isClassExpensive_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_instAlternativeMetaM___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_setInlineAttribute___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_withConfig___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1440,7 +1440,7 @@ x_5 = lean_ctor_get(x_1, 1);
x_6 = lean_ctor_get_uint8(x_2, sizeof(void*)*2);
x_7 = lean_ctor_get(x_2, 0);
x_8 = lean_ctor_get(x_2, 1);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_3, x_6);
x_9 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_3, x_6);
if (x_9 == 0)
{
uint8_t x_10;
@ -6902,7 +6902,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 0;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -6918,7 +6918,7 @@ lean_dec(x_6);
x_15 = 0;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);
@ -6952,7 +6952,7 @@ x_8 = lean_ctor_get(x_6, 0);
x_9 = 2;
x_10 = lean_unbox(x_8);
lean_dec(x_8);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_10, x_9);
x_11 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_10, x_9);
x_12 = lean_box(x_11);
lean_ctor_set(x_6, 0, x_12);
return x_6;
@ -6968,7 +6968,7 @@ lean_dec(x_6);
x_15 = 2;
x_16 = lean_unbox(x_13);
lean_dec(x_13);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_16, x_15);
x_17 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_16, x_15);
x_18 = lean_box(x_17);
x_19 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_19, 0, x_18);

6
stage0/stdlib/Lean/Meta/GetConst.c generated
View file

@ -21,7 +21,7 @@ lean_object* lean_st_ref_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConstNoEx_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_isReducible___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_getConst_x3f(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(uint8_t, uint8_t);
lean_object* l_Lean_ConstantInfo_name(lean_object*);
LEAN_EXPORT lean_object* l_Lean_getReducibilityStatus___at___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_GetConst_0__Lean_Meta_canUnfoldDefault(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -315,7 +315,7 @@ x_39 = lean_ctor_get(x_38, 0);
lean_inc(x_39);
lean_dec(x_38);
x_40 = 3;
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_6, x_40);
x_41 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_6, x_40);
if (x_41 == 0)
{
uint8_t x_42; lean_object* x_43;
@ -360,7 +360,7 @@ x_51 = lean_ctor_get(x_49, 0);
lean_inc(x_51);
lean_dec(x_49);
x_52 = 3;
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_6, x_52);
x_53 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_6, x_52);
if (x_53 == 0)
{
uint8_t x_54; lean_object* x_55; lean_object* x_56;

8
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

@ -131,7 +131,7 @@ size_t lean_usize_shift_right(size_t, size_t);
static lean_object* l_Lean_Meta_reduceNative_x3f___closed__14;
LEAN_EXPORT lean_object* l_Lean_Meta_smartUnfoldingMatch_x3f(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21(lean_object*, lean_object*);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(uint8_t, uint8_t);
uint8_t l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(uint8_t, uint8_t);
static lean_object* l_Lean_Meta_toCtorIfLit___closed__16;
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Lean_getConstInfoCtor___at___private_Lean_Meta_WHNF_0__Lean_Meta_toCtorWhenStructure___spec__1___closed__3;
@ -8832,7 +8832,7 @@ lean_inc(x_9);
lean_dec(x_7);
x_10 = 2;
x_11 = lean_unbox(x_8);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_11, x_10);
x_12 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_11, x_10);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14; lean_object* x_15;
@ -19276,7 +19276,7 @@ x_10 = lean_ctor_get(x_7, 1);
x_11 = 3;
x_12 = lean_unbox(x_9);
lean_dec(x_9);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_12, x_11);
x_13 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_12, x_11);
if (x_13 == 0)
{
lean_object* x_14;
@ -19308,7 +19308,7 @@ lean_dec(x_7);
x_18 = 3;
x_19 = lean_unbox(x_16);
lean_dec(x_16);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8650_(x_19, x_18);
x_20 = l___private_Init_Meta_0__Lean_Meta_beqTransparencyMode____x40_Init_Meta___hyg_8647_(x_19, x_18);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;

662
stage0/stdlib/Lean/Parser/Basic.c generated
View file

File diff suppressed because it is too large Load diff

34
stage0/stdlib/Lean/Parser/Extra.c generated
View file

@ -3516,7 +3516,7 @@ static lean_object* _init_l_Lean_Parser_numLit_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__15;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__27;
x_2 = l_Lean_Parser_numLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -3549,7 +3549,7 @@ static lean_object* _init_l_Lean_Parser_numLit_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__15;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__27;
x_2 = l_Lean_Parser_numLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -3582,7 +3582,7 @@ static lean_object* _init_l_Lean_Parser_numLit___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__15;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__27;
x_2 = l_Lean_Parser_numLit_formatter___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -3628,7 +3628,7 @@ static lean_object* _init_l_Lean_Parser_numLit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__15;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__27;
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
return x_2;
}
@ -3687,7 +3687,7 @@ static lean_object* _init_l_Lean_Parser_scientificLit_formatter___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("scientificLit");
x_1 = lean_mk_string("scientific");
return x_1;
}
}
@ -3866,7 +3866,7 @@ static lean_object* _init_l_Lean_Parser_strLit_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__14;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__31;
x_2 = l_Lean_Parser_strLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -3899,7 +3899,7 @@ static lean_object* _init_l_Lean_Parser_strLit_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__14;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__31;
x_2 = l_Lean_Parser_strLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -3932,7 +3932,7 @@ static lean_object* _init_l_Lean_Parser_strLit___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__14;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__31;
x_2 = l_Lean_Parser_strLit_formatter___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -3978,7 +3978,7 @@ static lean_object* _init_l_Lean_Parser_strLit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__14;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__31;
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
return x_2;
}
@ -4037,7 +4037,7 @@ static lean_object* _init_l_Lean_Parser_charLit_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__17;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__19;
x_2 = l_Lean_Parser_charLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -4070,7 +4070,7 @@ static lean_object* _init_l_Lean_Parser_charLit_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__17;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__19;
x_2 = l_Lean_Parser_charLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -4103,7 +4103,7 @@ static lean_object* _init_l_Lean_Parser_charLit___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__17;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__19;
x_2 = l_Lean_Parser_charLit_formatter___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -4149,7 +4149,7 @@ static lean_object* _init_l_Lean_Parser_charLit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__17;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__19;
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
return x_2;
}
@ -4208,7 +4208,7 @@ static lean_object* _init_l_Lean_Parser_nameLit_formatter___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__16;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__23;
x_2 = l_Lean_Parser_nameLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -4241,7 +4241,7 @@ static lean_object* _init_l_Lean_Parser_nameLit_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__16;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__23;
x_2 = l_Lean_Parser_nameLit_formatter___closed__1;
x_3 = 1;
x_4 = lean_box(x_3);
@ -4274,7 +4274,7 @@ static lean_object* _init_l_Lean_Parser_nameLit___elambda__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; uint8_t x_3; lean_object* x_4;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__16;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__23;
x_2 = l_Lean_Parser_nameLit_formatter___closed__1;
x_3 = 1;
x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
@ -4320,7 +4320,7 @@ static lean_object* _init_l_Lean_Parser_nameLit___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__16;
x_1 = l_Lean_Parser_mkAntiquot_formatter___closed__23;
x_2 = l_Lean_Parser_mkAtomicInfo(x_1);
return x_2;
}