From 54ec70818b0be148a9e3a9cc59ecc0f536466d12 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Andr=C3=A9s=20Goens?= <andres@goens.org>
Date: Fri, 24 Jan 2025 08:43:45 +0100
Subject: [PATCH] trying to address levels: (probably) infinite loop in whnf,
 isDefEq?

---
 Lean/Egg/Core/Gen/StructureProjs.lean | 12 +++++++-----
 Lean/Egg/Tests/WIP Projections.lean   |  7 ++++++-
 2 files changed, 13 insertions(+), 6 deletions(-)

diff --git a/Lean/Egg/Core/Gen/StructureProjs.lean b/Lean/Egg/Core/Gen/StructureProjs.lean
index 3530474..7c50e6b 100644
--- a/Lean/Egg/Core/Gen/StructureProjs.lean
+++ b/Lean/Egg/Core/Gen/StructureProjs.lean
@@ -6,10 +6,11 @@ open Lean Syntax
 structure RawStructProjInfo where
   ctor : Name
   params : Nat
-  levels : List Name
+  levels : List Level
   projs : Array Name
 
-private def getStructureCtorAndProjs (structName : Name) : MetaM RawStructProjInfo := do --Elab.Command.CommandElabM Unit := do
+private def getStructureCtorAndProjs (structName : Name) :
+ MetaM RawStructProjInfo := do
     let env ← getEnv
     match env.find? structName with
     | none => throwError s!"Structure {structName} not found"
@@ -23,8 +24,9 @@ private def getStructureCtorAndProjs (structName : Name) : MetaM RawStructProjIn
                --logInfo s!"Constructor: {ctorVal.name}"
                let projs := structInfo.fieldNames.map
                  fun nm => structInfo.structName.append nm
+               let levels := ctorVal.levelParams.map mkLevelParam
                return {ctor := ctorVal.name, params := ctorVal.numParams,
-                       levels := ctorVal.levelParams,  projs := projs}
+                       levels := levels,  projs := projs}
         | _ => throwError s!"{structName} is not a structure"
 
 open Egg
@@ -48,10 +50,10 @@ private def buildStructureProjEqns (structName : Name) (cfg : Rewrite.Config) :
       return acc.push mvar
   let mvars ← rawInfo.projs.mapM
     fun pr => Meta.mkFreshExprMVar none (userName := pr)
-  let ctorApp := mkAppN (mkConst rawInfo.ctor) (paramMvars ++ mvars)
+  let ctorApp := mkAppN (mkConst rawInfo.ctor rawInfo.levels) (paramMvars ++ mvars)
   let rawRws := rawInfo.projs.zipWithIndex.map
     fun (proj, idx) =>
-      (mkAppN (mkConst proj) (paramMvars ++ #[ctorApp]), mvars[idx]!)
+      (mkAppN (mkConst proj rawInfo.levels) (paramMvars ++ #[ctorApp]), mvars[idx]!)
   let mut rws := []
   for (lhs, rhs) in rawRws do
     let rw ← Rewrite.mkDefEq lhs rhs cfg
diff --git a/Lean/Egg/Tests/WIP Projections.lean b/Lean/Egg/Tests/WIP Projections.lean
index aad24b1..eae33f6 100644
--- a/Lean/Egg/Tests/WIP Projections.lean	
+++ b/Lean/Egg/Tests/WIP Projections.lean	
@@ -7,10 +7,12 @@ example (x1 x2 : α) : x1 = (x1,x2).1 := by rfl
 
 example (x1 x2 : α) : x1 = (x1,x2).1 := by egg
 
-
 set_option trace.egg true in
 example (x1 x2 : α) : x1 = Prod.fst (Prod.mk x1 x2) := by egg
 
+set_option pp.raw true in
+#eval (1,2)
+
 #reduce  Prod.fst (Prod.mk ?Prod.fst ?Prod.snd)
 
 open Lean in
@@ -42,3 +44,6 @@ structure Foo where
   y : Nat
 
 example (m n : Nat) : { x := m, y := n : Foo}.x = m := by egg
+
+set_option pp.raw true
+#eval (1,2)