From 4c11743f4b440bb25fd8137d29f3600ccb2a7d03 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 4 Nov 2022 11:04:23 +0100 Subject: [PATCH] refactor: split paren parser, part 2 --- src/Lean/Parser/Term.lean | 29 ++++++++++--------- tests/lean/StxQuot.lean.expected.out | 4 +-- .../lean/interactive/hover.lean.expected.out | 2 +- 3 files changed, 18 insertions(+), 17 deletions(-) diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 2af57d6e3c..1385f91e89 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -128,27 +128,28 @@ For example, `(· + ·)` is equivalent to `fun x y => x + y`. -/ @[builtin_term_parser] def cdot := leading_parser symbol "·" <|> "." -def typeAscription := leading_parser - "(" >> withoutPosition (withoutForbidden (termParser >> " : " >> optional termParser)) >> ")" -def tuple := leading_parser +/-- +Type ascription notation: `(0 : Int)` instructs Lean to process `0` as a value of type `Int`. +An empty type ascription `(e :)` elaborates `e` without the expected type. +This is occasionally useful when Lean's heuristics for filling arguments from the expected type +do not yield the right result. +-/ +@[builtin_term_parser] def typeAscription := leading_parser + "(" >> (withoutPosition (withoutForbidden (termParser >> " : " >> optional termParser))) >> ")" +/-- Tuple notation; `()` is short for `Unit.unit`, `(a, b, c)` for `Prod.mk a (Prod.mk b c)`, etc. -/ +@[builtin_term_parser] def tuple := leading_parser "(" >> optional (withoutPosition (withoutForbidden (termParser >> ", " >> sepBy1 termParser ", "))) >> ")" /-- -Parentheses, used for -- Grouping expressions, e.g., `a * (b + c)`. -- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`. -- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`. - - An empty type ascription `(e :)` elaborates `e` without the expected type. - This is occasionally useful when Lean's heuristics for filling arguments from the expected type - do not yield the right result. -- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`. -- Creating simple functions when combined with `·`. Here are some examples: +Parentheses, used for grouping expressions (e.g., `a * (b + c)`). +Can also be used for creating simple functions when combined with `·`. Here are some examples: - `(· + 1)` is shorthand for `fun x => x + 1` - `(· + ·)` is shorthand for `fun x y => x + y` - `(f · a b)` is shorthand for `fun x => f x a b` - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x` + - also applies to other parentheses-like notations such as `(·, 1)` -/ -@[builtin_term_parser] def paren := (leading_parser - atomic ("(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")")) <|> atomic typeAscription <|> tuple +@[builtin_term_parser] def paren := leading_parser + "(" >> withoutPosition (withoutForbidden (ppDedentIfGrouped termParser)) >> ")" /-- The *anonymous constructor* `⟨e, ...⟩` is equivalent to `c e ...` if the expected type is an inductive type with a single constructor `c`. diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index d2224f2bb1..b1203c8845 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -24,8 +24,8 @@ StxQuot.lean:19:15: error: expected term 0 1 "1" -"(Term.fun\n \"fun\"\n (Term.basicFun\n [`a._@.UnhygienicMain._hyg.1\n (Term.paren \"(\" [`b._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" [`Nat._@.UnhygienicMain._hyg.1])]] \")\")]\n []\n \"=>\"\n (num \"1\")))" -"#[(Term.paren \"(\" [`a._@.UnhygienicMain._hyg.1 [(Term.typeAscription \":\" [`Nat._@.UnhygienicMain._hyg.1])]] \")\"), `b._@.UnhygienicMain._hyg.1]" +"(Term.fun\n \"fun\"\n (Term.basicFun\n [`a._@.UnhygienicMain._hyg.1\n (Term.typeAscription \"(\" `b._@.UnhygienicMain._hyg.1 \":\" [`Nat._@.UnhygienicMain._hyg.1] \")\")]\n []\n \"=>\"\n (num \"1\")))" +"#[(Term.typeAscription \"(\" `a._@.UnhygienicMain._hyg.1 \":\" [`Nat._@.UnhygienicMain._hyg.1] \")\"), `b._@.UnhygienicMain._hyg.1]" "`a._@.UnhygienicMain._hyg.1" "(Term.forall \"∀\" [(Term.hole \"_\")] [] \",\" `c._@.UnhygienicMain._hyg.1)" "(Term.hole \"_\")" diff --git a/tests/lean/interactive/hover.lean.expected.out b/tests/lean/interactive/hover.lean.expected.out index e55115b02d..09c73726c6 100644 --- a/tests/lean/interactive/hover.lean.expected.out +++ b/tests/lean/interactive/hover.lean.expected.out @@ -387,7 +387,7 @@ null "end": {"line": 201, "character": 32}}, "contents": {"value": - "```lean\nId ℕ\n```\n***\nParentheses, used for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n - An empty type ascription `(e :)` elaborates `e` without the expected type.\n This is occasionally useful when Lean's heuristics for filling arguments from the expected type\n do not yield the right result.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n", + "```lean\nId ℕ\n```\n***\nParentheses, used for grouping expressions (e.g., `a * (b + c)`).\nCan also be used for creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n - also applies to other parentheses-like notations such as `(·, 1)`\n", "kind": "markdown"}} {"textDocument": {"uri": "file://hover.lean"}, "position": {"line": 204, "character": 8}}