summaryrefslogtreecommitdiff
path: root/backends
diff options
context:
space:
mode:
authorSon Ho2024-03-07 18:17:41 +0100
committerSon Ho2024-03-07 18:17:41 +0100
commit23ce25c77052c02312f19f17c51fe0b61d6abc93 (patch)
tree06ed320b409e0b29ac38f0f7fc7cce441e9c72a7 /backends
parent124ee77181c4255e2c8f730305b0b1b7802b9a58 (diff)
Introduce a notation for constant scalars in match patterns
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Primitives/Scalar.lean29
1 files changed, 29 insertions, 0 deletions
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