Add syntactic sugar for HVector

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

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