From 23ce25c77052c02312f19f17c51fe0b61d6abc93 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Mar 2024 18:17:41 +0100
Subject: Introduce a notation for constant scalars in match patterns

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

(limited to 'backends/lean')

diff --git a/backends/lean/Base/Primitives/Scalar.lean b/backends/lean/Base/Primitives/Scalar.lean
index 285bc7fb..422cbc6a 100644
--- a/backends/lean/Base/Primitives/Scalar.lean
+++ b/backends/lean/Base/Primitives/Scalar.lean
@@ -488,6 +488,17 @@ class HNeg (α : Type u) (β : outParam (Type v)) where
 
 prefix:75  "-"   => HNeg.hNeg
 
+/- We need this, otherwise we break pattern matching like in:
+
+   ```
+   def is_minus_one (x : Int) : Bool :=
+     match x with
+     | -1 => true
+     | _ => false
+   ```
+-/
+attribute [match_pattern] HNeg.hNeg
+
 instance : HNeg Isize (Result Isize) where hNeg x := Scalar.neg x
 instance : HNeg I8 (Result I8) where hNeg x := Scalar.neg x
 instance : HNeg I16 (Result I16) where hNeg x := Scalar.neg x
@@ -1113,4 +1124,22 @@ instance (ty : ScalarTy) : DecidableEq (Scalar ty) :=
 --   else
 --     .fail integerOverflow
 
+-- Notation for pattern matching
+-- We make the precedence looser than the negation.
+notation:70 a:70 "#scalar" => Scalar.mk (a) _ _
+
+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
+
 end Primitives
-- 
cgit v1.2.3