Pointer pattern (#280)

* Pointer pattern

* elab new Pattern.pointer constructor

* pointer match test

---------

Co-authored-by: Arthur Paulino <arthurleonardo.ap@gmail.com>

Author: gabriel-barrett

Ix/Aiur/Check.lean

@@ -392,6 +392,7 @@ where
       let bind ← aux pat typ
       let bind' ← aux pat' typ
       if bind != bind' then throw $ .differentBindings bind bind' else pure bind
+    | (.pointer pat, .pointer typ) => aux pat typ
     | _ => throw $ .incompatiblePattern pat typ
 
 partial def inferTuple (term : Term) : CheckM (Array Typ × TypedTermInner) := do

Ix/Aiur/Match.lean

@@ -11,6 +11,7 @@ inductive SPattern
   | ref : Global → Array Local → SPattern
   | tuple : Array Local → SPattern
   | array : Array Local → SPattern
+  | pointer : Local → SPattern
   deriving BEq, Hashable, Inhabited
 
 structure Clause where
@@ -76,6 +77,12 @@ def dnfProd (branches: List $ Pattern × UniqTerm) (body : ExtTerm) : CompilerM
       let (vars, guards) ← flattenArgs args.toArray
       let clause := ⟨.ref global vars, guards, term⟩
       aux renames (clauses.push clause) rest body
+    | (.pointer arg, term) :: rest => do
+      let id ← newId
+      let var := .idx id
+      let guards := #[(arg, (id, .var var))]
+      let clause := ⟨.pointer var, guards, term⟩
+      aux renames (clauses.push clause) rest body
   aux Array.empty Array.empty branches body
 where
   flattenArgs args := do
@@ -98,6 +105,7 @@ def patTypeLength (decls : Decls) : SPattern → Nat
   | .tuple _ => 1
   | .array _ => 1
   | .ref global _ => typeLookup global |>.constructors.length
+  | .pointer _ => 1
 where
   typeLookup (global : Global) :=
     match global.popNamespace with
@@ -200,6 +208,8 @@ def spatternToPattern : SPattern → Pattern
   | .ref global vars => .ref global (vars.map .var).toList
   | .tuple vars => .tuple (vars.map .var)
   | .array vars => .array (vars.map .var)
+  -- pointer patterns are unique and will be converted into a load operation before this function is called
+  | .pointer _ => unreachable!
 
 mutual
 
@@ -214,6 +224,9 @@ partial def branchesToTerm (branches : List (SPattern × Decision)) (dec : Decis
 partial def decisionToTerm : Decision → Option Term
   | .success ⟨renames, value⟩ =>
     some $ renames.foldr (init := value) fun (x, y) acc => .let (.var x) y acc
+  | .switch ptr [(.pointer val, body)] _ => do
+    let body' ← decisionToTerm body
+    some $ .let (.var val) (.load (.var ptr)) body'
   | .switch var branches dec => some $ .match (.var var) (branchesToTerm branches dec)
   | .let var term body => do
     let body' ← decisionToTerm body

Ix/Aiur/Meta.lean

@@ -15,6 +15,7 @@ syntax num                                   : pattern
 syntax "(" pattern (", " pattern)* ")"       : pattern
 syntax "[" pattern (", " pattern)* "]"       : pattern
 syntax pattern "|" pattern                   : pattern
+syntax "&" pattern                           : pattern
 
 def elabListCore (head : α) (tail : Array α) (elabFn : α → TermElabM Expr)
     (listEltType : Expr) (isArray := false) : TermElabM Expr := do
@@ -58,6 +59,8 @@ partial def elabPattern : ElabStxCat `pattern
     mkAppM ``Pattern.array #[← elabList p ps elabPattern ``Pattern true]
   | `(pattern| $p₁:pattern | $p₂:pattern) => do
     mkAppM ``Pattern.or #[← elabPattern p₁, ← elabPattern p₂]
+  | `(pattern| &$p:pattern) => do
+    mkAppM ``Pattern.pointer #[← elabPattern p]
   | stx => throw $ .error stx "Invalid syntax for pattern"
 
 declare_syntax_cat                               typ

Ix/Aiur/Term.lean

@@ -7,7 +7,7 @@ namespace Aiur
 inductive Local
   | str : String → Local
   | idx : Nat → Local
-  deriving Repr, BEq, Hashable
+  deriving Repr, BEq, Inhabited, Hashable
 
 structure Global where
   toName : Lean.Name
@@ -46,6 +46,7 @@ inductive Pattern
   | tuple : Array Pattern → Pattern
   | array : Array Pattern → Pattern
   | or : Pattern → Pattern → Pattern
+  | pointer : Pattern → Pattern
   deriving Repr, BEq, Hashable, Inhabited
 
 inductive Typ where

Tests/Aiur.lean

@@ -50,6 +50,14 @@ def toplevel := ⟦
   --   cast(Nat.Zero, (G, G))
   -- }
 
+  fn pointer_match() -> G {
+    let two = Nat.Succ(store(Nat.Succ(store(Nat.Zero))));
+    match two {
+      Nat.Succ(&Nat.Succ(&Nat.Zero)) => 1,
+      _ => 0,
+    }
+  }
+
   fn even(m: Nat) -> G {
     match m {
       Nat.Zero => 1,
@@ -210,6 +218,7 @@ def aiurTestCases : List AiurTestCase := [
     .noIO `eq_zero_dummy #[0, 37] #[1, 0, 1, 0],
     .noIO `store_and_load #[42] #[42],
     -- .noIO `cast_zero #[] #[0, 0],
+    .noIO `pointer_match #[] #[1],
     .noIO `is_0_even #[] #[1],
     .noIO `is_1_even #[] #[0],
     .noIO `is_2_even #[] #[1],