From 3442c3fafa97f022ea7a40c51eaad8d6bf2e1f94 Mon Sep 17 00:00:00 2001
From: utkn <utkns09@gmail.com>
Date: Mon, 9 Dec 2024 19:17:16 +0300
Subject: [PATCH] tuple projection by index builtin

---
 Lampe/Lampe/Builtin/Struct.lean | 54 +++++++++++++++++++++++++++++++++
 Lampe/Lampe/Data/HList.lean     |  4 +++
 Lampe/Lampe/Tp.lean             |  8 ++---
 3 files changed, 60 insertions(+), 6 deletions(-)

diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
index d05c2ee..e8892ca 100644
--- a/Lampe/Lampe/Builtin/Struct.lean
+++ b/Lampe/Lampe/Builtin/Struct.lean
@@ -1,4 +1,58 @@
 import Lampe.Builtin.Basic
 namespace Lampe.Builtin
 
+@[reducible]
+def listRep (rep : Tp → Type _) : List Tp → Type := fun l => match l with
+| tp :: tps => (rep tp) × (listRep rep tps)
+| [] => Unit
+
+@[reducible]
+def HList.toProd (hList : HList rep tps) : (listRep rep) tps := match hList with
+| .nil => ()
+| .cons arg args => ⟨arg, HList.toProd args⟩
+
+lemma listRep_tp_denote_is_tp_denote_tuple {nameOpt} :
+  listRep (Tp.denote p) tps = Tp.denote p (.tuple nameOpt tps) := by
+  induction tps <;> {
+    unfold listRep Tp.denoteArgs
+    tauto
+  }
+
+def mkTuple := newGenericPureBuiltin
+  (fun fieldTps => ⟨fieldTps, (.tuple none fieldTps)⟩)
+  (fun _ fieldExprs => ⟨True,
+    fun _ => listRep_tp_denote_is_tp_denote_tuple ▸ HList.toProd fieldExprs⟩)
+
+def mkStruct := newGenericPureBuiltin
+  (fun (name, fieldTps) => ⟨fieldTps, (.tuple (some name) fieldTps)⟩)
+  (fun (_, _) fieldExprs => ⟨True,
+    fun _ => listRep_tp_denote_is_tp_denote_tuple ▸ HList.toProd fieldExprs⟩)
+
+def tupleNth {fieldTps : List Tp} (tpl : Tp.denote p (.tuple nameOpt fieldTps)) (n : Fin fieldTps.length) :
+ Tp.denote p $ fieldTps.get n := match fieldTps with
+  | _ :: _ => match tpl, n with
+    | Prod.mk a _, Fin.mk 0 _ => a
+    | _, Fin.mk (.succ n') _ => tupleNth tpl.snd (Fin.mk n' _) (nameOpt := nameOpt)
+
+inductive projectTupleOmni : Omni where
+| mk {p st} {fieldTps : List Tp} {n : Fin fieldTps.length} {tpl Q} :
+  Q (some (st, tupleNth tpl n)) →
+  projectTupleOmni p st [.tuple _ fieldTps] (fieldTps.get n) h![tpl] Q
+
+def projectTuple : Builtin := {
+  omni := projectTupleOmni
+  conseq := by
+    unfold omni_conseq
+    intros
+    cases_type projectTupleOmni
+    tauto
+  frame := by
+    unfold omni_frame
+    intros
+    cases_type projectTupleOmni
+    constructor
+    simp only
+    repeat apply Exists.intro <;> tauto
+}
+
 end Lampe.Builtin
diff --git a/Lampe/Lampe/Data/HList.lean b/Lampe/Lampe/Data/HList.lean
index 9aff02c..ac8229e 100644
--- a/Lampe/Lampe/Data/HList.lean
+++ b/Lampe/Lampe/Data/HList.lean
@@ -7,3 +7,7 @@ macro_rules
 | `(h![]) => `(HList.nil)
 | `(h![$x]) => `(HList.cons $x HList.nil)
 | `(h![$x, $xs,*]) => `(HList.cons $x h![$xs,*])
+
+-- def HList.get (hList : HList rep tps)
+-- | HList.nil => ()
+-- | HList.cons (a := tp) (as := tps) v rem => v
diff --git a/Lampe/Lampe/Tp.lean b/Lampe/Lampe/Tp.lean
index 021fb54..ed215b1 100644
--- a/Lampe/Lampe/Tp.lean
+++ b/Lampe/Lampe/Tp.lean
@@ -8,10 +8,7 @@ namespace Lampe
 
 structure Ref where
   val : Nat
-deriving DecidableEq
-
-structure NamedTuple (name : String) (T : Type) where
-  tuple : T
+  deriving DecidableEq
 
 variable (p : Prime)
 
@@ -51,8 +48,7 @@ def Tp.denote : Tp → Type
 | .slice tp => List (denote tp)
 | .array tp n => Mathlib.Vector (denote tp) n.toNat
 | .ref _ => Ref
-| .tuple (some name) fields => NamedTuple name $ Tp.denoteArgs fields
-| .tuple none fields => Tp.denoteArgs fields
+| .tuple _ fields => Tp.denoteArgs fields
 
 end