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

feat(library/init/lean/parser/term): builtin operators

Browse source
This commit is contained in:
Leonardo de Moura 2019-07-11 10:11:20 -07:00
parent 195fb27ce5
commit 57e2f1be2a
4 changed files with 35 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
library/init/core.lean
View file

@ -84,7 +84,6 @@ reserve infixr ` :: `:67
/- Control -/
reserve infixr ` <|> `:2
reserve infixr `; ` :3
reserve infixr ` >>= `:55
reserve infixr ` >=> `:55
reserve infixl ` <*> `:60

30
library/init/lean/parser/term.lean
View file

@ -89,6 +89,10 @@ def letLhsPat := parser! termParser >> " := "
def letLhs := (try letLhsId <|> try letLhsBinders <|> letLhsPat)
@[builtinTermParser] def «let» := parser! "let " >> letLhs >> termParser >> "; " >> termParser
@[builtinTermParser] def not := parser! symbol "¬" 40 >> termParser 40
@[builtinTermParser] def bnot := parser! symbol "!" 40 >> termParser 40
@[builtinTermParser] def uminus := parser! "-" >> termParser 100
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Term.type || leading.isOfKind `Lean.Parser.Term.sort)
@ -99,24 +103,50 @@ def checkIsSort := checkLeading (fun leading => leading.isOfKind `Lean.Parser.Te
@[builtinTermParser] def fcomp := tparser! infixR " ∘ " 90
@[builtinTermParser] def prod := tparser! infixR " × " 35
@[builtinTermParser] def add := tparser! infixL " + " 65
@[builtinTermParser] def sub := tparser! infixL " - " 65
@[builtinTermParser] def mul := tparser! infixL " * " 70
@[builtinTermParser] def div := tparser! infixL " / " 70
@[builtinTermParser] def mod := tparser! infixL " % " 70
@[builtinTermParser] def modN := tparser! infixL " %ₙ " 70
@[builtinTermParser] def pow := tparser! infixR " ^ " 80
@[builtinTermParser] def le := tparser! unicodeInfixL " ≤ " " <= " 50
@[builtinTermParser] def ge := tparser! unicodeInfixL " ≥ " " >= " 50
@[builtinTermParser] def lt := tparser! infixL " < " 50
@[builtinTermParser] def gt := tparser! infixL " > " 50
@[builtinTermParser] def eq := tparser! infixL " = " 50
@[builtinTermParser] def ne := tparser! infixL " ≠ " 50
@[builtinTermParser] def beq := tparser! infixL " == " 50
@[builtinTermParser] def bne := tparser! infixL " != " 50
@[builtinTermParser] def heq := tparser! unicodeInfixL " ≅ " " ~= " 50
@[builtinTermParser] def equiv := tparser! infixL " ≈ " 50
@[builtinTermParser] def subst := tparser! infixR " ▸ " 75
@[builtinTermParser] def and := tparser! unicodeInfixR " ∧ " " /\\ " 35
@[builtinTermParser] def or := tparser! unicodeInfixR " ∨ " " \\/ " 30
@[builtinTermParser] def iff := tparser! unicodeInfixL " ↔ " " <-> " 20
@[builtinTermParser] def band := tparser! infixL " && " 35
@[builtinTermParser] def bor := tparser! infixL " || " 30
@[builtinTermParser] def append := tparser! infixL " ++ " 65
@[builtinTermParser] def cons := tparser! infixR " :: " 67
@[builtinTermParser] def orelse := tparser! infixR " <|> " 2
@[builtinTermParser] def andthen := tparser! infixR " >> " 60
@[builtinTermParser] def bind := tparser! infixR " >>= " 55
@[builtinTermParser] def andM := tparser! infixR " <&> " 100
@[builtinTermParser] def seq := tparser! infixL " <*> " 60
@[builtinTermParser] def seqLeft := tparser! infixL " <* " 60
@[builtinTermParser] def seqRight := tparser! infixR " *> " 60
@[builtinTermParser] def map := tparser! infixR " <$> " 100
@[builtinTermParser] def mapConst := tparser! infixR " <$ " 100
@[builtinTermParser] def mapConstRev := tparser! infixR " $> " 100
end Term
end Parser

2
src/frontends/lean/token_table.cpp
View file

@ -90,7 +90,7 @@ void init_token_table(token_table & t) {
{"Type", g_max_prec}, {"Type*", g_max_prec}, {"Sort", g_max_prec}, {"Sort*", g_max_prec},
{"(:", g_max_prec}, {":)", 0}, {".(", g_max_prec}, {"._", g_max_prec},
{"⟨", g_max_prec}, {"⟩", 0}, {"^", 0},
{"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"..", 0}, {"...", 0}, {",", 0}, {"=>", 0},
{"//", 0}, {"|", 0}, {"with", 0}, {"without", 0}, {"..", 0}, {"...", 0}, {",", 0}, {";", 0}, {"=>", 0},
{".", 0}, {":", 0}, {"!", 0}, {":=", 0}, {"--", 0}, {"#", g_max_prec},
{"/-", 0}, {"/--", 0}, {"/-!", 0}, {"begin", g_max_prec}, {"using", 0},
{"@@", g_max_prec}, {"@", g_max_prec}, {"@&", g_max_prec},

5
tests/playground/termparsertest1.lean
View file

@ -100,7 +100,10 @@ match x with
"let x.y := f 10; x",
"let x.1 := f 10; x",
"let x[i].y := f 10; x",
"let x[i] := f 20; x"
"let x[i] := f 20; x",
"-x + y",
"!x",
"¬ a ∧ b"
];
testFailures [
"f {x : a} -> b",