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-06-10 16:22:32 -07:00
parent 7269a721ff
commit b5dff38ecf
6 changed files with 833 additions and 476 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
stage0/src/Lean/Parser/Level.lean
View file

@ -23,7 +23,7 @@ namespace Level
@[builtinLevelParser] def hole := parser! "_"
@[builtinLevelParser] def num := parser! numLit
@[builtinLevelParser] def ident := parser! ident
@[builtinLevelParser] def addLit := tparser! [65] "+" >> numLit
@[builtinLevelParser] def addLit := tparser!:65 "+" >> numLit
end Level

2
stage0/src/Lean/Parser/Syntax.lean
View file

@ -39,7 +39,7 @@ namespace Syntax
@[builtinSyntaxParser] def optional := tparser! "?"
@[builtinSyntaxParser] def many := tparser! "*"
@[builtinSyntaxParser] def many1 := tparser! "+"
@[builtinSyntaxParser] def orelse := tparser! [2] " <|> " >> syntaxParser 1
@[builtinSyntaxParser] def orelse := tparser!:2 " <|> " >> syntaxParser 1
end Syntax

2
stage0/src/Lean/Parser/Tactic.lean
View file

@ -51,7 +51,7 @@ def withIds : Parser := optional (" with " >> many1 ident')
@[builtinTacticParser] def paren := parser! "(" >> nonEmptySeq >> ")"
@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
@[builtinTacticParser] def orelse := tparser! [2] " <|> " >> tacticParser 1
@[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
end Tactic
end Parser

45
stage0/src/Lean/Parser/Term.lean
View file

@ -66,12 +66,12 @@ def parenSpecial : Parser := optional (tupleTail <|> typeAscription)
@[builtinTermParser] def paren := parser! "(" >> optional (termParser >> parenSpecial) >> ")"
@[builtinTermParser] def anonymousCtor := parser! "⟨" >> sepBy termParser ", " >> "⟩"
def optIdent : Parser := optional (try (ident >> " : "))
@[builtinTermParser] def «if» := parser! [leadPrec] "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
@[builtinTermParser] def «if» := parser!:leadPrec "if " >> optIdent >> termParser >> " then " >> termParser >> " else " >> termParser
def fromTerm := parser! " from " >> termParser
def haveAssign := parser! " := " >> termParser
@[builtinTermParser] def «have» := parser! [leadPrec] "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
@[builtinTermParser] def «suffices» := parser! [leadPrec] "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
@[builtinTermParser] def «show» := parser! [leadPrec] "show " >> termParser >> fromTerm
@[builtinTermParser] def «have» := parser!:leadPrec "have " >> optIdent >> termParser >> (haveAssign <|> fromTerm) >> "; " >> termParser
@[builtinTermParser] def «suffices» := parser!:leadPrec "suffices " >> optIdent >> termParser >> fromTerm >> "; " >> termParser
@[builtinTermParser] def «show» := parser!:leadPrec "show " >> termParser >> fromTerm
def structInstArrayRef := parser! "[" >> termParser >>"]"
def structInstLVal := (ident <|> fieldIdx <|> structInstArrayRef) >> many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
def structInstField := parser! structInstLVal >> " := " >> termParser
@ -93,10 +93,10 @@ def instBinder := parser! "[" >> optIdent >> termParser >> "]"
def bracketedBinder (requireType := false) := explicitBinder requireType <|> implicitBinder requireType <|> instBinder
@[builtinTermParser] def depArrow := parser! bracketedBinder true >> checkPrec 25 >> unicodeSymbol " → " " -> " >> termParser
def simpleBinder := parser! many1 binderIdent
@[builtinTermParser] def «forall» := parser! [leadPrec] unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
@[builtinTermParser] def «forall» := parser!:leadPrec unicodeSymbol "∀" "forall" >> many1 (simpleBinder <|> bracketedBinder) >> ", " >> termParser
def funBinder : Parser := implicitBinder <|> instBinder <|> termParser appPrec
@[builtinTermParser] def «fun» := parser! [leadPrec] unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser
@[builtinTermParser] def «fun» := parser!:leadPrec unicodeSymbol "λ" "fun" >> many1 funBinder >> darrow >> termParser
def matchAlt : Parser :=
nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
@ -107,14 +107,15 @@ withPosition $ fun pos =>
(if optionalFirstBar then optional "|" else "|") >>
sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
@[builtinTermParser] def «match» := parser! [leadPrec] "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser! [leadPrec] "nomatch " >> termParser
@[builtinTermParser] def «parser!» := parser! [leadPrec] "parser! " >> termParser -- TODO optional prec
@[builtinTermParser] def «tparser!» := parser! [leadPrec] "tparser! " >> termParser
@[builtinTermParser] def «match» := parser!:leadPrec "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
@[builtinTermParser] def «nomatch» := parser!:leadPrec "nomatch " >> termParser
def optExprPrecedence := optional (try ":" >> termParser appPrec)
@[builtinTermParser] def «parser!» := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def «tparser!» := parser!:leadPrec "tparser! " >> optExprPrecedence >> termParser
@[builtinTermParser] def borrowed := parser! "@&" >> termParser (appPrec - 1)
@[builtinTermParser] def quotedName := parser! nameLit
-- NOTE: syntax quotations are defined in Init.Lean.Parser.Command
@[builtinTermParser] def «match_syntax» := parser! [leadPrec] "match_syntax" >> termParser >> " with " >> matchAlts
@[builtinTermParser] def «match_syntax» := parser!:leadPrec "match_syntax" >> termParser >> " with " >> matchAlts
/- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/
def letIdLhs : Parser := ident >> checkWsBefore "expected space before binders" >> many bracketedBinder >> optType
@ -122,8 +123,8 @@ def letIdDecl : Parser := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl
def letPatDecl : Parser := node `Lean.Parser.Term.letDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser
def letEqnsDecl : Parser := node `Lean.Parser.Term.letDecl $ letIdLhs >> matchAlts false
def letDecl := letIdDecl <|> letPatDecl <|> letEqnsDecl
@[builtinTermParser] def «let» := parser! [leadPrec] "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let!» := parser! [leadPrec] "let! " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let» := parser!:leadPrec "let " >> letDecl >> "; " >> termParser
@[builtinTermParser] def «let!» := parser!:leadPrec "let! " >> letDecl >> "; " >> termParser
def leftArrow : Parser := unicodeSymbol " ← " " <- "
def doLet := parser! "let ">> letDecl
@ -133,8 +134,8 @@ def doExpr := parser! termParser
def doElem := doLet <|> doId <|> doPat <|> doExpr
def doSeq := sepBy1 doElem "; "
def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def liftMethod := parser! [0] leftArrow >> termParser
@[builtinTermParser] def «do» := parser! [leadPrec] "do " >> (bracketedDoSeq <|> doSeq)
@[builtinTermParser] def liftMethod := parser!:0 leftArrow >> termParser
@[builtinTermParser] def «do» := parser!:leadPrec "do " >> (bracketedDoSeq <|> doSeq)
@[builtinTermParser] def nativeRefl := parser! "nativeRefl! " >> termParser appPrec
@[builtinTermParser] def nativeDecide := parser! "nativeDecide! " >> termParser appPrec
@ -143,19 +144,19 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def not := parser! "¬" >> termParser 40
@[builtinTermParser] def bnot := parser! "!" >> termParser 40
-- symbol precedence should be higher, but must match the one of `sub` below
@[builtinTermParser] def uminus := parser! [65] "-" >> termParser 100
@[builtinTermParser] def uminus := parser!:65 "-" >> termParser 100
def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! [appPrec-1] many1 (namedArgument <|> termParser appPrec)
@[builtinTermParser] def app := tparser!:(appPrec-1) many1 (namedArgument <|> termParser appPrec)
@[builtinTermParser] def proj := tparser! symbolNoWs "." >> (fieldIdx <|> ident)
@[builtinTermParser] def arrow := tparser! unicodeInfixR " → " " -> " 25
@[builtinTermParser] def arrayRef := tparser! symbolNoWs "[" >> termParser >>"]"
@[builtinTermParser] def dollar := tparser! [0] try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
@[builtinTermParser] def dollarProj := tparser! [0] "$." >> (fieldIdx <|> ident)
@[builtinTermParser] def dollar := tparser!:0 try (dollarSymbol >> checkWsBefore "space expected") >> termParser 0
@[builtinTermParser] def dollarProj := tparser!:0 "$." >> (fieldIdx <|> ident)
@[builtinTermParser] def «where» := tparser! [0] " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
@[builtinTermParser] def «where» := tparser!:0 " where " >> sepBy1 letDecl (group ("; " >> symbol " where "))
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
@ -180,7 +181,7 @@ def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50
@[builtinTermParser] def equiv := tparser! infixL " ≈ " 50
@[builtinTermParser] def subst := tparser! [75] " ▸ " >> sepBy1 (termParser 75) " ▸ "
@[builtinTermParser] def subst := tparser!:75 " ▸ " >> sepBy1 (termParser 75) " ▸ "
@[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35
@[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30
@ -206,7 +207,7 @@ def namedArgument := parser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def mapConstRev := tparser! infixR " $> " 100
@[builtinTermParser] def tacticBlock := parser! "begin " >> Tactic.seq >> "end"
@[builtinTermParser] def byTactic := parser! [leadPrec] "by " >> Tactic.nonEmptySeq
@[builtinTermParser] def byTactic := parser!:leadPrec "by " >> Tactic.nonEmptySeq
-- Use `unboxSingleton` trick similar to the one used at Command.lean for `Term.stxQuot`
@[builtinTermParser] def tacticStxQuot : Parser :=
checkPrec appPrec >> (node `Lean.Parser.Term.stxQuot $ "`(tactic|" >> sepBy1 tacticParser "; " true true >> ")")

66
stage0/stdlib/Lean/Parser/Syntax.c
View file

@ -37,7 +37,6 @@ lean_object* l_Lean_Parser_Syntax_sepBy___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_notation___closed__7;
lean_object* l_Lean_Parser_Command_macroArgSimple___closed__3;
lean_object* l_Lean_Parser_Command_macroTailTactic___closed__1;
lean_object* l_Lean_Parser_precedence___elambda__1___closed__6;
lean_object* l_Lean_Parser_Command_macro__rules___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_mixfixKind___closed__2;
lean_object* l_Lean_Parser_Command_infixr___elambda__1___closed__3;
@ -106,6 +105,7 @@ lean_object* l_Lean_Parser_Command_infixr___closed__1;
extern lean_object* l_Lean_Parser_ident;
lean_object* l_Lean_Parser_Syntax_lookahead___closed__5;
lean_object* l_Lean_Parser_precedence___elambda__1___closed__2;
extern lean_object* l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
lean_object* l_Lean_Parser_Syntax_str___closed__3;
lean_object* l_Lean_Parser_Syntax_sepBy;
lean_object* l_Lean_Parser_Syntax_sepBy___closed__5;
@ -312,7 +312,6 @@ lean_object* l_Lean_Parser_Command_prefix___elambda__1___closed__3;
lean_object* l_Lean_Parser_Syntax_optional___elambda__1___closed__1;
lean_object* l_Lean_Parser_Syntax_paren___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__9;
lean_object* l_Lean_Parser_precedence___elambda__1___closed__5;
lean_object* l_Lean_Parser_Command_reserve___elambda__1___closed__4;
lean_object* l_Lean_Parser_Command_identPrec___closed__3;
lean_object* l_Lean_Parser_Command_macroArgType;
@ -400,7 +399,6 @@ lean_object* l_Lean_Parser_Syntax_ident___closed__2;
lean_object* l_Lean_Parser_ParserState_restore(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Command_macroTailDefault___closed__6;
lean_object* l___regBuiltinParser_Lean_Parser_Command_syntaxCat(lean_object*);
lean_object* l_Lean_Parser_precedence___elambda__1___closed__7;
lean_object* l_Lean_Parser_Command_macro___elambda__1___closed__5;
lean_object* l_Lean_Parser_Syntax_many___closed__3;
lean_object* l_Lean_Parser_Syntax_optional___elambda__1(lean_object*, lean_object*);
@ -1147,38 +1145,6 @@ x_4 = l_Lean_Parser_mkAntiquot(x_1, x_2, x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Parser_precedence___elambda__1___closed__5() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Char_HasRepr___closed__1;
x_2 = l_Lean_Parser_mkAntiquot___closed__4;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_precedence___elambda__1___closed__6() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Parser_precedence___elambda__1___closed__5;
x_2 = l_Char_HasRepr___closed__1;
x_3 = lean_string_append(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Parser_precedence___elambda__1___closed__7() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Parser_precedence___elambda__1___closed__6;
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_Parser_precedence___elambda__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1229,7 +1195,7 @@ lean_dec(x_24);
if (x_26 == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_27 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_28 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_27, x_19);
x_11 = x_28;
goto block_18;
@ -1245,7 +1211,7 @@ else
{
lean_object* x_29; lean_object* x_30;
lean_dec(x_23);
x_29 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_29 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_30 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_29, x_19);
x_11 = x_30;
goto block_18;
@ -1255,7 +1221,7 @@ else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_21);
x_31 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_31 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_20, x_31, x_19);
x_11 = x_32;
goto block_18;
@ -1371,7 +1337,7 @@ lean_dec(x_62);
if (x_64 == 0)
{
lean_object* x_65; lean_object* x_66;
x_65 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_65 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_66 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_65, x_57);
x_47 = x_66;
goto block_56;
@ -1387,7 +1353,7 @@ else
{
lean_object* x_67; lean_object* x_68;
lean_dec(x_61);
x_67 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_67 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_68 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_67, x_57);
x_47 = x_68;
goto block_56;
@ -1397,7 +1363,7 @@ else
{
lean_object* x_69; lean_object* x_70;
lean_dec(x_59);
x_69 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_69 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_70 = l_Lean_Parser_ParserState_mkErrorsAt(x_58, x_69, x_57);
x_47 = x_70;
goto block_56;
@ -13137,7 +13103,7 @@ if (x_23 == 0)
{
lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27;
lean_dec(x_1);
x_24 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_24 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_25 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_24, x_16);
x_26 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_27 = l_Lean_Parser_ParserState_mkNode(x_25, x_26, x_10);
@ -13158,7 +13124,7 @@ else
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
lean_dec(x_20);
lean_dec(x_1);
x_31 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_31 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_32 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_31, x_16);
x_33 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_34 = l_Lean_Parser_ParserState_mkNode(x_32, x_33, x_10);
@ -13170,7 +13136,7 @@ else
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_18);
lean_dec(x_1);
x_35 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_35 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_36 = l_Lean_Parser_ParserState_mkErrorsAt(x_17, x_35, x_16);
x_37 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_38 = l_Lean_Parser_ParserState_mkNode(x_36, x_37, x_10);
@ -13299,7 +13265,7 @@ if (x_69 == 0)
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74;
lean_dec(x_1);
x_70 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_70 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_71 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_70, x_62);
x_72 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_73 = l_Lean_Parser_ParserState_mkNode(x_71, x_72, x_56);
@ -13324,7 +13290,7 @@ else
lean_object* x_79; lean_object* x_80; lean_object* x_81; lean_object* x_82; lean_object* x_83;
lean_dec(x_66);
lean_dec(x_1);
x_79 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_79 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_80 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_79, x_62);
x_81 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_82 = l_Lean_Parser_ParserState_mkNode(x_80, x_81, x_56);
@ -13338,7 +13304,7 @@ else
lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88;
lean_dec(x_64);
lean_dec(x_1);
x_84 = l_Lean_Parser_precedence___elambda__1___closed__7;
x_84 = l_Lean_Parser_Term_optExprPrecedence___elambda__1___closed__3;
x_85 = l_Lean_Parser_ParserState_mkErrorsAt(x_63, x_84, x_62);
x_86 = l_Lean_Parser_Command_macroArgSimple___elambda__1___closed__2;
x_87 = l_Lean_Parser_ParserState_mkNode(x_85, x_86, x_56);
@ -16165,12 +16131,6 @@ l_Lean_Parser_precedence___elambda__1___closed__3 = _init_l_Lean_Parser_preceden
lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__3);
l_Lean_Parser_precedence___elambda__1___closed__4 = _init_l_Lean_Parser_precedence___elambda__1___closed__4();
lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__4);
l_Lean_Parser_precedence___elambda__1___closed__5 = _init_l_Lean_Parser_precedence___elambda__1___closed__5();
lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__5);
l_Lean_Parser_precedence___elambda__1___closed__6 = _init_l_Lean_Parser_precedence___elambda__1___closed__6();
lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__6);
l_Lean_Parser_precedence___elambda__1___closed__7 = _init_l_Lean_Parser_precedence___elambda__1___closed__7();
lean_mark_persistent(l_Lean_Parser_precedence___elambda__1___closed__7);
l_Lean_Parser_precedence___closed__1 = _init_l_Lean_Parser_precedence___closed__1();
lean_mark_persistent(l_Lean_Parser_precedence___closed__1);
l_Lean_Parser_precedence___closed__2 = _init_l_Lean_Parser_precedence___closed__2();

1192
stage0/stdlib/Lean/Parser/Term.c
View file

File diff suppressed because it is too large Load diff