From eda89935dd634aabfe23ee00f3b0580c912a2d2a Mon Sep 17 00:00:00 2001
From: utkn <utkns09@gmail.com>
Date: Mon, 9 Dec 2024 19:35:30 +0300
Subject: [PATCH] struct field projector and project struct builtin

---
 Lampe/Lampe/Builtin/Struct.lean | 25 ++++++++++++++++++++++++-
 1 file changed, 24 insertions(+), 1 deletion(-)

diff --git a/Lampe/Lampe/Builtin/Struct.lean b/Lampe/Lampe/Builtin/Struct.lean
index e8892ca..12b27c3 100644
--- a/Lampe/Lampe/Builtin/Struct.lean
+++ b/Lampe/Lampe/Builtin/Struct.lean
@@ -35,7 +35,7 @@ def tupleNth {fieldTps : List Tp} (tpl : Tp.denote p (.tuple nameOpt fieldTps))
     | _, 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} :
+| mk {p st} {n : Fin fieldTps.length} {tpl Q} :
   Q (some (st, tupleNth tpl n)) →
   projectTupleOmni p st [.tuple _ fieldTps] (fieldTps.get n) h![tpl] Q
 
@@ -55,4 +55,27 @@ def projectTuple : Builtin := {
     repeat apply Exists.intro <;> tauto
 }
 
+def structFieldProjector (fieldTps : List Tp) := (fieldName : String) → Fin fieldTps.length
+
+inductive projectStructOmni : Omni where
+| mk {p st} {proj : structFieldProjector fieldTps} {fieldName : String} {tpl Q} :
+  Q (some (st, tupleNth tpl (proj fieldName))) →
+  projectStructOmni p st [.tuple _ fieldTps] (fieldTps.get (proj fieldName)) h![tpl] Q
+
+def projectStruct : Builtin := {
+  omni := projectStructOmni
+  conseq := by
+    unfold omni_conseq
+    intros
+    cases_type projectStructOmni
+    tauto
+  frame := by
+    unfold omni_frame
+    intros
+    cases_type projectStructOmni
+    constructor
+    simp only
+    repeat apply Exists.intro <;> tauto
+}
+
 end Lampe.Builtin