From c8272aeea205ca9cb36e22757473ca2a931a4933 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 14:52:34 +0200
Subject: Update the scalar notation for the Lean backend

---
 compiler/ExtractTypes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'compiler')

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 15e75da2..5446f912 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
               let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt ("#" ^ iname)
+              F.pp_print_string fmt iname
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
-- 
cgit v1.3.1


From f05a0faf14fdd558039da52624d57028eb64f9fd Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 16:54:24 +0200
Subject: Fix some mistakes

---
 compiler/ExtractBase.ml         |  2 ++
 tests/lean/Arrays.lean          |  4 ++--
 tests/lean/Demo/Properties.lean |  4 ++--
 tests/lean/Tutorial.lean        | 22 +++++++++++-----------
 4 files changed, 17 insertions(+), 15 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 4aac270f..8fe36d5b 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1016,6 +1016,8 @@ let keywords () =
           "where";
           "with";
         ]
+        @ (* This comes from the scalar notations: `1u32`, etc. *)
+        List.map StringUtils.lowercase_first_letter all_int_names
     | HOL4 ->
         [
           "Axiom";
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 70b4a26b..5f50e580 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -266,9 +266,9 @@ def index_all : Result U32 :=
   let (s1, to_slice_mut_back) ←
     Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
-  let i8 ← i6 + i7
+  let i9 ← i6 + i7
   let _ ← to_slice_mut_back s2
-  Result.ok i8
+  Result.ok i9
 
 /- [arrays::update_array]:
    Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index abdc2985..67023727 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp_all; scalar_tac
   | CCons hd tl =>
     simp_all
-    if hi: i = 0#u32 then
+    if hi: i = 0u32 then
       simp_all
     else
       simp_all
@@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0#i32 then
+  if hx : x = 0i32 then
     simp_all
   else
     simp_all
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 94b70991..7d347277 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -17,7 +17,7 @@ namespace Tutorial
 
 def mul2_add1 (x : U32) : Result U32 := do
   let x1 ← x + x
-  let x2 ← x1 + 1#u32
+  let x2 ← x1 + 1u32
   ok x2
 
 /- There are several things to note.
@@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do
    Because Rust programs manipulate machine integers which occupy a fixed
    size in memory, we model integers by using types like [U32], which is
    the type of integers which take their values between 0 and 2^32 - 1 (inclusive).
-   [1#u32] is simply the constant 1 (seen as a [U32]).
+   [1u32] is simply the constant 1 (seen as a [U32]).
 
    You can see a definition or its type by using the [#print] and [#check] commands.
    It is also possible to jump to definitions (right-click + "Go to Definition"
@@ -229,10 +229,10 @@ open CList
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CCons x tl =>
-    if i = 0#u32
+    if i = 0u32
     then ok x
     else do
-      let i1 ← i - 1#u32
+      let i1 ← i - 1u32
       list_nth T tl i1
   | CNil => fail Error.panic
 
@@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp only []
     -- Perform a case disjunction on [i].
     -- The notation [hi : ...] allows us to introduce an assumption in the
-    -- context, to remember the fact that in the branches we have [i = 0#u32]
-    -- and [¬ i = 0#u32].
-    if hi: i = 0#u32 then
+    -- context, to remember the fact that in the branches we have [i = 0u32]
+    -- and [¬ i = 0u32].
+    if hi: i = 0u32 then
       -- We can finish the proof simply by using the simplifier.
       -- We decompose the proof into several calls on purpose, so that it is
       -- easier to understand what is going on.
@@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
    annotates it with the [divergent] keyword.
  -/
 divergent def i32_id (x : I32) : Result I32 :=
-  if x = 0#i32 then ok 0#i32
+  if x = 0i32 then ok 0i32
   else do
-    let x1 ← x - 1#i32
+    let x1 ← x - 1i32
     let x2 ← i32_id x1
-    x2 + 1#i32
+    x2 + 1i32
 
 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0#i32 then
+  if hx : x = 0i32 then
     simp_all
   else
     simp [hx]
-- 
cgit v1.3.1


From 8ca43c32b30c03cc3fde51736ea5884dfd1c2c50 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:14 +0200
Subject: Revert "Fix some mistakes"

This reverts commit f05a0faf14fdd558039da52624d57028eb64f9fd.
---
 compiler/ExtractBase.ml         |  2 --
 tests/lean/Arrays.lean          |  4 ++--
 tests/lean/Demo/Properties.lean |  4 ++--
 tests/lean/Tutorial.lean        | 22 +++++++++++-----------
 4 files changed, 15 insertions(+), 17 deletions(-)

(limited to 'compiler')

diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index 8fe36d5b..4aac270f 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -1016,8 +1016,6 @@ let keywords () =
           "where";
           "with";
         ]
-        @ (* This comes from the scalar notations: `1u32`, etc. *)
-        List.map StringUtils.lowercase_first_letter all_int_names
     | HOL4 ->
         [
           "Axiom";
diff --git a/tests/lean/Arrays.lean b/tests/lean/Arrays.lean
index 5f50e580..70b4a26b 100644
--- a/tests/lean/Arrays.lean
+++ b/tests/lean/Arrays.lean
@@ -266,9 +266,9 @@ def index_all : Result U32 :=
   let (s1, to_slice_mut_back) ←
     Array.to_slice_mut U32 2usize (Array.make U32 2usize [ 0u32, 0u32 ])
   let (i7, s2) ← index_mut_slice_u32_0 s1
-  let i9 ← i6 + i7
+  let i8 ← i6 + i7
   let _ ← to_slice_mut_back s2
-  Result.ok i9
+  Result.ok i8
 
 /- [arrays::update_array]:
    Source: 'tests/src/arrays.rs', lines 187:0-187:36 -/
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index 67023727..abdc2985 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -43,7 +43,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp_all; scalar_tac
   | CCons hd tl =>
     simp_all
-    if hi: i = 0u32 then
+    if hi: i = 0#u32 then
       simp_all
     else
       simp_all
@@ -54,7 +54,7 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0i32 then
+  if hx : x = 0#i32 then
     simp_all
   else
     simp_all
diff --git a/tests/lean/Tutorial.lean b/tests/lean/Tutorial.lean
index 7d347277..94b70991 100644
--- a/tests/lean/Tutorial.lean
+++ b/tests/lean/Tutorial.lean
@@ -17,7 +17,7 @@ namespace Tutorial
 
 def mul2_add1 (x : U32) : Result U32 := do
   let x1 ← x + x
-  let x2 ← x1 + 1u32
+  let x2 ← x1 + 1#u32
   ok x2
 
 /- There are several things to note.
@@ -27,7 +27,7 @@ def mul2_add1 (x : U32) : Result U32 := do
    Because Rust programs manipulate machine integers which occupy a fixed
    size in memory, we model integers by using types like [U32], which is
    the type of integers which take their values between 0 and 2^32 - 1 (inclusive).
-   [1u32] is simply the constant 1 (seen as a [U32]).
+   [1#u32] is simply the constant 1 (seen as a [U32]).
 
    You can see a definition or its type by using the [#print] and [#check] commands.
    It is also possible to jump to definitions (right-click + "Go to Definition"
@@ -229,10 +229,10 @@ open CList
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CCons x tl =>
-    if i = 0u32
+    if i = 0#u32
     then ok x
     else do
-      let i1 ← i - 1u32
+      let i1 ← i - 1#u32
       list_nth T tl i1
   | CNil => fail Error.panic
 
@@ -285,9 +285,9 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
     simp only []
     -- Perform a case disjunction on [i].
     -- The notation [hi : ...] allows us to introduce an assumption in the
-    -- context, to remember the fact that in the branches we have [i = 0u32]
-    -- and [¬ i = 0u32].
-    if hi: i = 0u32 then
+    -- context, to remember the fact that in the branches we have [i = 0#u32]
+    -- and [¬ i = 0#u32].
+    if hi: i = 0#u32 then
       -- We can finish the proof simply by using the simplifier.
       -- We decompose the proof into several calls on purpose, so that it is
       -- easier to understand what is going on.
@@ -348,17 +348,17 @@ theorem list_nth_spec {T : Type} [Inhabited T] (l : CList T) (i : U32)
    annotates it with the [divergent] keyword.
  -/
 divergent def i32_id (x : I32) : Result I32 :=
-  if x = 0i32 then ok 0i32
+  if x = 0#i32 then ok 0#i32
   else do
-    let x1 ← x - 1i32
+    let x1 ← x - 1#i32
     let x2 ← i32_id x1
-    x2 + 1i32
+    x2 + 1#i32
 
 /- We can easily prove that [i32_id] behaves like the identity on positive inputs -/
 theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
   ∃ y, i32_id x = ok y ∧ x.val = y.val := by
   rw [i32_id]
-  if hx : x = 0i32 then
+  if hx : x = 0#i32 then
     simp_all
   else
     simp [hx]
-- 
cgit v1.3.1


From d36736fa4e7eb9f42f35303b8080d17ddbee92d2 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:20:52 +0200
Subject: Revert "Update the scalar notation for the Lean backend"

This reverts commit c8272aeea205ca9cb36e22757473ca2a931a4933.
---
 backends/lean/Base/Primitives/Scalar.lean | 50 +++++++++++++++----------------
 compiler/ExtractTypes.ml                  |  2 +-
 2 files changed, 26 insertions(+), 26 deletions(-)

(limited to 'compiler')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 5f14a14f..157ade2c 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -313,13 +313,13 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   apply And.intro <;> have hmin := Scalar.cMin_bound ty <;> have hmax := Scalar.cMax_bound ty <;> linarith
 
 /- [match_pattern] attribute: allows to us `Scalar.ofIntCore` inside of patterns.
-   This is particularly useful once we introduce notations like `u32` (which
+   This is particularly useful once we introduce notations like `#u32` (which
    desugards to `Scalar.ofIntCore`) as it allows to write expressions like this:
    Example:
    ```
    match x with
-   | 0u32 => ...
-   | 1u32 => ...
+   | 0#u32 => ...
+   | 1#u32 => ...
    | ...
    ```
  -/
@@ -328,7 +328,7 @@ theorem Scalar.bound_suffices (ty : ScalarTy) (x : Int) :
   { val := x, hmin := h.left, hmax := h.right }
 
 -- The definitions below are used later to introduce nice syntax for constants,
--- like `1u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
+-- like `1#u32`. We are reusing the technique described here: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Different.20elaboration.20inside.2Foutside.20of.20match.20patterns/near/425455284
 
 class InBounds (ty : ScalarTy) (x : Int) :=
   hInBounds : Scalar.cMin ty ≤ x ∧ x ≤ Scalar.cMax ty
@@ -1281,38 +1281,38 @@ def U128.ofIntCore  := @Scalar.ofIntCore .U128
 @[match_pattern] abbrev U64.ofInt   := @Scalar.ofInt .U64
 @[match_pattern] abbrev U128.ofInt  := @Scalar.ofInt .U128
 
-postfix:max "isize" => Isize.ofInt
-postfix:max "i8"    => I8.ofInt
-postfix:max "i16"   => I16.ofInt
-postfix:max "i32"   => I32.ofInt
-postfix:max "i64"   => I64.ofInt
-postfix:max "i128"  => I128.ofInt
-postfix:max "usize" => Usize.ofInt
-postfix:max "u8"    => U8.ofInt
-postfix:max "u16"   => U16.ofInt
-postfix:max "u32"   => U32.ofInt
-postfix:max "u64"   => U64.ofInt
-postfix:max "u128"  => U128.ofInt
+postfix:max "#isize" => Isize.ofInt
+postfix:max "#i8"    => I8.ofInt
+postfix:max "#i16"   => I16.ofInt
+postfix:max "#i32"   => I32.ofInt
+postfix:max "#i64"   => I64.ofInt
+postfix:max "#i128"  => I128.ofInt
+postfix:max "#usize" => Usize.ofInt
+postfix:max "#u8"    => U8.ofInt
+postfix:max "#u16"   => U16.ofInt
+postfix:max "#u32"   => U32.ofInt
+postfix:max "#u64"   => U64.ofInt
+postfix:max "#u128"  => U128.ofInt
 
 /- Testing the notations -/
-example := 0u32
-example := 1u32
-example := 1i32
-example := 0isize
-example := (-1)isize
+example := 0#u32
+example := 1#u32
+example := 1#i32
+example := 0#isize
+example := (-1)#isize
 example (x : U32) : Bool :=
   match x with
-  | 0u32 => true
+  | 0#u32 => true
   | _ => false
 
 example (x : U32) : Bool :=
   match x with
-  | 1u32 => true
+  | 1#u32 => true
   | _ => false
 
 example (x : I32) : Bool :=
   match x with
-  | (-1)i32 => true
+  | (-1)#i32 => true
   | _ => false
 
 -- Notation for pattern matching
@@ -1334,7 +1334,7 @@ example {ty} (x : Scalar ty) : Bool :=
   | _ => false
 
 -- Testing the notations
-example : Result Usize := 0usize + 1usize
+example : Result Usize := 0#usize + 1#usize
 
 -- TODO: factor those lemmas out
 @[simp] theorem Scalar.ofInt_val_eq {ty} (h : Scalar.min ty ≤ x ∧ x ≤ Scalar.max ty) : (Scalar.ofIntCore x h).val = x := by
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 5446f912..15e75da2 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -40,7 +40,7 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
               let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt iname
+              F.pp_print_string fmt ("#" ^ iname)
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
-- 
cgit v1.3.1


From 19abb19134efe0b16409f955b13af36262f231a8 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:40:27 +0200
Subject: Update the code extraction and regenerate the tests

---
 compiler/Extract.ml      |  6 ++++--
 compiler/ExtractTypes.ml | 14 +++++++++-----
 tests/lean/Matches.lean  |  4 ++--
 3 files changed, 15 insertions(+), 9 deletions(-)

(limited to 'compiler')

diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index eab85054..4acf3f99 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -241,11 +241,12 @@ let rec extract_typed_pattern (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (is_let : bool) (inside : bool) ?(with_type = false)
     (v : typed_pattern) : extraction_ctx =
   if with_type then F.pp_print_string fmt "(";
+  let is_pattern = true in
   let inside = inside && not with_type in
   let ctx =
     match v.value with
     | PatConstant cv ->
-        extract_literal span fmt inside cv;
+        extract_literal span fmt is_pattern inside cv;
         ctx
     | PatVar (v, _) ->
         let vname = ctx_compute_var_basename span ctx v.basename v.ty in
@@ -307,6 +308,7 @@ let extract_texpression_errors (fmt : F.formatter) =
 
 let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
     (fmt : F.formatter) (inside : bool) (e : texpression) : unit =
+  let is_pattern = false in
   match e.e with
   | Var var_id ->
       let var_name = ctx_get_var span var_id ctx in
@@ -314,7 +316,7 @@ let rec extract_texpression (span : Meta.span) (ctx : extraction_ctx)
   | CVar var_id ->
       let var_name = ctx_get_const_generic_var span var_id ctx in
       F.pp_print_string fmt var_name
-  | Const cv -> extract_literal span fmt inside cv
+  | Const cv -> extract_literal span fmt is_pattern inside cv
   | App _ ->
       let app, args = destruct_apps e in
       extract_App span ctx fmt inside app args
diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 15e75da2..631db13e 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -11,12 +11,13 @@ include ExtractBase
 
     Inputs:
     - formatter
+    - [is_pattern]: if [true], it means we are generating a (match) pattern
     - [inside]: if [true], the value should be wrapped in parentheses
       if it is made of an application (ex.: [U32 3])
     - the constant value
  *)
-let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
-    (cv : literal) : unit =
+let extract_literal (span : Meta.span) (fmt : F.formatter) (is_pattern : bool)
+    (inside : bool) (cv : literal) : unit =
   match cv with
   | VScalar sv -> (
       match backend () with
@@ -39,8 +40,11 @@ let extract_literal (span : Meta.span) (fmt : F.formatter) (inside : bool)
               let iname = int_name sv.int_ty in
               F.pp_print_string fmt ("%" ^ iname)
           | Lean ->
-              let iname = String.lowercase_ascii (int_name sv.int_ty) in
-              F.pp_print_string fmt ("#" ^ iname)
+              (* We don't use the same notation for patterns and regular literals *)
+              if is_pattern then F.pp_print_string fmt "#scalar"
+              else
+                let iname = String.lowercase_ascii (int_name sv.int_ty) in
+                F.pp_print_string fmt ("#" ^ iname)
           | HOL4 -> ()
           | _ -> craise __FILE__ __LINE__ span "Unreachable");
           if print_brackets then F.pp_print_string fmt ")")
@@ -409,7 +413,7 @@ let extract_const_generic (span : Meta.span) (ctx : extraction_ctx)
   | CgGlobal id ->
       let s = ctx_get_global span id ctx in
       F.pp_print_string fmt s
-  | CgValue v -> extract_literal span fmt inside v
+  | CgValue v -> extract_literal span fmt false inside v
   | CgVar id ->
       let s = ctx_get_const_generic_var span id ctx in
       F.pp_print_string fmt s
diff --git a/tests/lean/Matches.lean b/tests/lean/Matches.lean
index 3e3a558b..9233841b 100644
--- a/tests/lean/Matches.lean
+++ b/tests/lean/Matches.lean
@@ -9,8 +9,8 @@ namespace matches
    Source: 'tests/src/matches.rs', lines 4:0-4:27 -/
 def match_u32 (x : U32) : Result U32 :=
   match x with
-  | 0#u32 => Result.ok 0#u32
-  | 1#u32 => Result.ok 1#u32
+  | 0#scalar => Result.ok 0#u32
+  | 1#scalar => Result.ok 1#u32
   | _ => Result.ok 2#u32
 
 end matches
-- 
cgit v1.3.1