From 7c63b2f046ea67ba61b9050bc683520209dc18e3 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 27 Nov 2017 12:38:17 +0100 Subject: [PATCH] fix(frontends/lean/parser): unicode pattern aliases --- src/frontends/lean/parser.cpp | 4 ++- tests/lean/as_pattern.lean | 15 +++++++---- tests/lean/as_pattern.lean.expected.out | 34 ++++++++++++------------- 3 files changed, 30 insertions(+), 23 deletions(-) diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 3c19e3b276..7089935f7f 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -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(); diff --git a/tests/lean/as_pattern.lean b/tests/lean/as_pattern.lean index f0d5a12943..bc6aede0a2 100644 --- a/tests/lean/as_pattern.lean +++ b/tests/lean/as_pattern.lean @@ -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 diff --git a/tests/lean/as_pattern.lean.expected.out b/tests/lean/as_pattern.lean.expected.out index a6bd9904cf..c7135fe242 100644 --- a/tests/lean/as_pattern.lean.expected.out +++ b/tests/lean/as_pattern.lean.expected.out @@ -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