trying to address levels: (probably) infinite loop in whnf, isDefEq?

marcusrossel · Jan 24, 2025 · 54ec708 · 54ec708
1 parent b9eb0d9
commit 54ec708
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 6 deletions.
diff --git 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
@@ -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)