From 79e19aa701086de9f080357d817284559f900bcc Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:40:17 +0200
Subject: Update the scalar notations in Lean

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 87 ++++++++++++++++++++++
 1 file changed, 87 insertions(+)
 create mode 100644 backends/lean/Base/Primitives/ScalarNotations.lean

(limited to 'backends/lean/Base/Primitives/ScalarNotations.lean')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
new file mode 100644
index 00000000..50d8c1b6
--- /dev/null
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -0,0 +1,87 @@
+import Lean
+import Lean.Meta.Tactic.Simp
+import Mathlib.Tactic.Linarith
+import Base.Primitives.Scalar
+import Base.Arith
+
+namespace Primitives
+
+open Lean Meta Elab Term
+
+macro x:term:max "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
+macro x:term:max "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
+macro x:term:max "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
+macro x:term:max "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
+macro x:term:max "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
+macro x:term:max "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
+macro x:term:max "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
+macro x:term:max "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
+macro x:term:max "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
+macro x:term:max "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro x:term:max "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
+macro x:term:max "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
+
+macro x:term:max noWs "u32"   : term => `(U32.ofInt $x (by scalar_tac))
+
+-- Notation for pattern matching
+-- We make the precedence looser than the negation.
+notation:70 a:70 "#scalar" => Scalar.mk (a) _ _
+
+/- Testing the notations -/
+example := 0#u32
+example := 1#u32
+example := 1#i32
+example := 0#isize
+example := (-1)#isize
+
+/-
+-- This doesn't work anymore
+example (x : U32) : Bool :=
+  match x with
+  | 0#u32 => true
+  | _ => false
+
+example (x : U32) : Bool :=
+  match x with
+  | 1#u32 => true
+  | _ => false
+
+example (x : I32) : Bool :=
+  match x with
+  | (-1)#i32 => true
+  | _ => false
+-/
+
+example (x : U32) : Bool :=
+  match x with
+  | 0#scalar => true
+  | _ => false
+
+example (x : U32) : Bool :=
+  match x with
+  | 1#scalar => true
+  | _ => false
+
+example (x : I32) : Bool :=
+  match x with
+  | (-1)#scalar => true
+  | _ => false
+
+example {ty} (x : Scalar ty) : ℤ :=
+  match x with
+  | v#scalar => v
+
+example {ty} (x : Scalar ty) : Bool :=
+  match x with
+  | 1#scalar => true
+  | _ => false
+
+example {ty} (x : Scalar ty) : Bool :=
+  match x with
+  | -(1 : Int)#scalar => true
+  | _ => false
+
+-- Testing the notations
+example : Result Usize := 0#usize + 1#usize
+
+end Primitives
-- 
cgit v1.2.3


From a46d785eb548043535a05d1b67dde48c18f5cf5f Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 12 Jun 2024 18:46:08 +0200
Subject: Add an example

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'backends/lean/Base/Primitives/ScalarNotations.lean')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index 50d8c1b6..cc6e6f02 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -84,4 +84,7 @@ example {ty} (x : Scalar ty) : Bool :=
 -- Testing the notations
 example : Result Usize := 0#usize + 1#usize
 
+-- More complex expressions
+example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
+
 end Primitives
-- 
cgit v1.2.3


From 1979d72b37d3a4abdff555da3f75ecfc9f629c26 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 11:33:13 +0200
Subject: Fix more issues

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 33 +++++++++++++---------
 1 file changed, 19 insertions(+), 14 deletions(-)

(limited to 'backends/lean/Base/Primitives/ScalarNotations.lean')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index cc6e6f02..94c0c779 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -8,20 +8,18 @@ namespace Primitives
 
 open Lean Meta Elab Term
 
-macro x:term:max "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
-macro x:term:max "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
-macro x:term:max "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
-macro x:term:max "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
-macro x:term:max "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
-macro x:term:max "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
-macro x:term:max "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
-macro x:term:max "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
-macro x:term:max "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
-macro x:term:max "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
-macro x:term:max "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
-macro x:term:max "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
-
-macro x:term:max noWs "u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
+macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
 
 -- Notation for pattern matching
 -- We make the precedence looser than the negation.
@@ -87,4 +85,11 @@ example : Result Usize := 0#usize + 1#usize
 -- More complex expressions
 example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
 
+section Scalar.Examples
+abbrev NList (a : Type) (x : U32) := { l : List a // l.length = x.val }
+
+example : NList Int 0#u32 := ⟨ [], by simp ⟩
+
+end Scalar.Examples
+
 end Primitives
-- 
cgit v1.2.3


From 87d088fa9e4493f32ae3f8d447ff1ff6d44e6396 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 13 Jun 2024 15:07:21 +0200
Subject: Fix more issues with the scalar notations

---
 backends/lean/Base/Primitives/ScalarNotations.lean | 44 ++++++++++++++--------
 1 file changed, 29 insertions(+), 15 deletions(-)

(limited to 'backends/lean/Base/Primitives/ScalarNotations.lean')

diff --git a/backends/lean/Base/Primitives/ScalarNotations.lean b/backends/lean/Base/Primitives/ScalarNotations.lean
index 94c0c779..3bc86a9c 100644
--- a/backends/lean/Base/Primitives/ScalarNotations.lean
+++ b/backends/lean/Base/Primitives/ScalarNotations.lean
@@ -8,18 +8,24 @@ namespace Primitives
 
 open Lean Meta Elab Term
 
-macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by scalar_tac))
-macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by scalar_tac))
+/- Something strange happens here: when we solve the goal with scalar_tac, it
+   sometimes leaves meta-variables in place, which then causes issues when
+   type-checking functions. For instance, it happens when we have const-generics
+   in the translation: the constants contain meta-variables, which are then
+   used in the types, which cause issues later. An example is given below:
+ -/
+macro:max x:term:max noWs "#isize" : term => `(Isize.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i8"    : term => `(I8.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i16"   : term => `(I16.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i32"   : term => `(I32.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i64"   : term => `(I64.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#i128"  : term => `(I128.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#usize" : term => `(Usize.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u8"    : term => `(U8.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u16"   : term => `(U16.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u32"   : term => `(U32.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u64"   : term => `(U64.ofInt $x (by first | decide | scalar_tac))
+macro:max x:term:max noWs "#u128"  : term => `(U128.ofInt $x (by first | decide | scalar_tac))
 
 -- Notation for pattern matching
 -- We make the precedence looser than the negation.
@@ -32,6 +38,8 @@ example := 1#i32
 example := 0#isize
 example := (-1)#isize
 
+example := 1#u32
+
 /-
 -- This doesn't work anymore
 example (x : U32) : Bool :=
@@ -85,10 +93,16 @@ example : Result Usize := 0#usize + 1#usize
 -- More complex expressions
 example (x y : Int) (h : 0 ≤ x + y ∧ x + y ≤ 1000) : U32 := (x + y)#u32
 
-section Scalar.Examples
-abbrev NList (a : Type) (x : U32) := { l : List a // l.length = x.val }
+namespace Scalar.Examples
+
+  abbrev Array (a : Type) (len : U32) := { l : List a // l.length = len.val }
+
+  -- Checking the syntax
+  example : Array Int 0#u32 := ⟨ [], by simp ⟩
 
-example : NList Int 0#u32 := ⟨ [], by simp ⟩
+  /- The example below fails if we don't use `decide` in the elaboration
+     of the scalar notation -/
+  example (a : Array (Array Int 32#u32) 32#u32) := a
 
 end Scalar.Examples
 
-- 
cgit v1.2.3

