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