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

fix(frontends/lean/parser): unicode pattern aliases

Browse source
This commit is contained in:
Sebastian Ullrich 2017-11-27 12:38:17 +01:00
parent 18cf63e37f
commit 7c63b2f046
3 changed files with 30 additions and 23 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/parser.cpp
View file

@ -2175,7 +2175,9 @@ expr parser::parse_nud() {
// if `id` is immediately followed by `@`, parse an as pattern `id@pat`
if (in_pattern() && id.is_atomic() && curr_is_token(get_explicit_tk())) {
lean_assert(is_local(e));
auto id_len = id.to_string().length();
// note: This number is not accurate for an escaped identifier. We should be able to do a better job
// in the new backtracking parser.
auto id_len = utf8_strlen(id.to_string().c_str());
auto p = pos();
if (p.first == id_pos.first && p.second == id_pos.second + id_len) {
next();

15
tests/lean/as_pattern.lean
View file

@ -1,3 +1,4 @@
namespace as_pattern
inductive foo
| a | b | c
@ -8,21 +9,21 @@ inductive bar : foo → Type
def basic : list foo → list foo
| x@([_]) := x -- `@[` starts an attribute
| x@_ := x
#print prefix basic.equations
#print prefix as_pattern.basic.equations
def nested : list foo → list foo
| (x@foo.b :: _) := [x]
| x := x
#print prefix nested.equations
#print prefix as_pattern.nested.equations
def value : option ℕ → option ℕ
| (some x@2) := some x
| x := x
#print prefix value.equations
#print prefix as_pattern.value.equations
def weird_but_ok : ℕ → ℕ
| x@y@z := x+y+z
#print prefix weird_but_ok.equations
#print prefix as_pattern.weird_but_ok.equations
def too_many : ℕ → ℕ
| x@_ := x
@ -37,7 +38,7 @@ def too_many2 : ℕ → ℕ
def dependent : Π (f : foo), bar f → foo
| x@foo.a bar.a := x
| x@_ bar.b := x
#print prefix dependent.equations
#print prefix as_pattern.dependent.equations
section involved
universe variables u v
@ -47,3 +48,7 @@ inductive imf {A : Type u} {B : Type v} (f : A → B) : B → Type (max 1 u v)
definition inv_1 {A : Type u} {B : Type v} (f : A → B) : ∀ (b : B), imf f b → A
| x@.(f w) y@(imf.mk z@.(f) w@a) := w
end involved
def unicode : ℕ → ℕ
| n₁@_ := n₁
end as_pattern

34
tests/lean/as_pattern.lean.expected.out
View file

@ -1,18 +1,18 @@
basic.equations._eqn_1 : basic list.nil = list.nil
basic.equations._eqn_2 : ∀ (_x : foo), basic [_x] = [_x]
basic.equations._eqn_3 : ∀ (a a_1 : foo) (a_2 : list foo), basic (a :: a_1 :: a_2) = a :: a_1 :: a_2
nested.equations._eqn_1 : nested list.nil = list.nil
nested.equations._eqn_2 : ∀ (a : list foo), nested (foo.a :: a) = foo.a :: a
nested.equations._eqn_3 : ∀ (_x : list foo), nested (foo.b :: _x) = [foo.b]
nested.equations._eqn_4 : ∀ (a : list foo), nested (foo.c :: a) = foo.c :: a
value.equations._eqn_1 : value none = none
value.equations._eqn_2 : value (some 2) = some 2
value.equations._eqn_3 : ∀ (a : ℕ), ¬a = 2 → value (some a) = some a
weird_but_ok.equations._eqn_1 : ∀ (z : ℕ), weird_but_ok z = z + z + z
as_pattern.lean:29:6: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:30:6: error: equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:31:6: error: equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:34:4: error: invalid pattern, 'x' already appeared in this pattern
as_pattern.basic.equations._eqn_1 : basic list.nil = list.nil
as_pattern.basic.equations._eqn_2 : ∀ (_x : foo), basic [_x] = [_x]
as_pattern.basic.equations._eqn_3 : ∀ (a a_1 : foo) (a_2 : list foo), basic (a :: a_1 :: a_2) = a :: a_1 :: a_2
as_pattern.nested.equations._eqn_1 : nested list.nil = list.nil
as_pattern.nested.equations._eqn_2 : ∀ (a : list foo), nested (foo.a :: a) = foo.a :: a
as_pattern.nested.equations._eqn_3 : ∀ (_x : list foo), nested (foo.b :: _x) = [foo.b]
as_pattern.nested.equations._eqn_4 : ∀ (a : list foo), nested (foo.c :: a) = foo.c :: a
as_pattern.value.equations._eqn_1 : value none = none
as_pattern.value.equations._eqn_2 : value (some 2) = some 2
as_pattern.value.equations._eqn_3 : ∀ (a : ℕ), ¬a = 2 → value (some a) = some a
as_pattern.weird_but_ok.equations._eqn_1 : ∀ (z : ℕ), weird_but_ok z = z + z + z
as_pattern.lean:30:6: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:31:6: error: equation compiler error, equation #3 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:32:6: error: equation compiler error, equation #4 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
as_pattern.lean:35:4: error: invalid pattern, 'x' already appeared in this pattern
dependent.equations._eqn_1 : dependent foo.a bar.a = foo.a
dependent.equations._eqn_2 : dependent foo.b bar.b = foo.b
as_pattern.lean:36:4: error: invalid pattern, 'x' already appeared in this pattern
as_pattern.dependent.equations._eqn_1 : dependent foo.a bar.a = foo.a
as_pattern.dependent.equations._eqn_2 : dependent foo.b bar.b = foo.b