From 9a46d6935fd3f2a285aa6b832e82e3ac89182a87 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <Andrés Goens>
Date: Wed, 15 Nov 2023 20:00:05 +0100
Subject: [PATCH] Add syntactic sugar for HVector

---
 SSA/Core/HVector.lean                         | 14 ++++++++++++++
 SSA/Projects/PaperExamples/PaperExamples.lean |  6 +++---
 2 files changed, 17 insertions(+), 3 deletions(-)

diff --git a/SSA/Core/HVector.lean b/SSA/Core/HVector.lean
index 4d2c00da9..ab5d4a993 100644
--- a/SSA/Core/HVector.lean
+++ b/SSA/Core/HVector.lean
@@ -92,5 +92,19 @@ theorem map_map {A B C : α → Type*} {l : List α} (t : HVector A l)
 theorem eq_of_type_eq_nil {A : α → Type*} {l : List α}
     {t₁ t₂ : HVector A l} (h : l = []) : t₁ = t₂ := by
   cases h; cases t₁; cases t₂; rfl
+syntax "[" withoutPosition(term,*) "]ₕ"  : term
+
+-- Copied from core for List
+macro_rules
+  | `([ $elems,* ]ₕ) => do
+    let rec expandListLit (i : Nat) (skip : Bool) (result : Lean.TSyntax `term) : Lean.MacroM Lean.Syntax := do
+      match i, skip with
+      | 0,   _     => pure result
+      | i+1, true  => expandListLit i false result
+      | i+1, false => expandListLit i true  (← ``(HVector.cons $(⟨elems.elemsAndSeps.get! i⟩) $result))
+    if elems.elemsAndSeps.size < 64 then
+      expandListLit elems.elemsAndSeps.size false (← ``(HVector.nil))
+    else
+      `(%[ $elems,* | List.nil ])
 
 end HVector
diff --git a/SSA/Projects/PaperExamples/PaperExamples.lean b/SSA/Projects/PaperExamples/PaperExamples.lean
index ca9694912..9a644f3f0 100644
--- a/SSA/Projects/PaperExamples/PaperExamples.lean
+++ b/SSA/Projects/PaperExamples/PaperExamples.lean
@@ -33,7 +33,7 @@ instance : OpSignature Op Ty where
 instance : OpDenote Op Ty where
   denote
     | .const n, _, _ => BitVec.ofInt 32 n
-    | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b
+    | .add, [(a : BitVec 32), (b : BitVec 32)]ₕ, _ => a + b
 
 def cst {Γ : Ctxt _} (n : ℤ) : Expr Op Γ .int  :=
   Expr.mk
@@ -125,8 +125,8 @@ instance : OpSignature Op Ty where
 instance : OpDenote Op Ty where
   denote
     | .const n, _, _ => BitVec.ofInt 32 n
-    | .add, .cons (a : BitVec 32) (.cons (b : BitVec 32) .nil), _ => a + b
-    | .iterate k, (.cons (x : BitVec 32) .nil), (.cons (f : _ → BitVec 32) .nil) =>
+    | .add, [(a : BitVec 32), (b : BitVec 32)]ₕ , _ => a + b
+    | .iterate k, [(x : BitVec 32)]ₕ, [(f : _ → BitVec 32)]ₕ =>
       let f' (v :  BitVec 32) : BitVec 32 := f  (Ctxt.Valuation.nil.snoc v)
       k.iterate f' x
       -- let f_k := Nat.iterate f' k