start working on the generation pipeline

Lean/Egg/Core/Config.lean

@@ -37,6 +37,7 @@ structure Gen where
   explosion       := false
   derivedGuides   := true
   genGroundEqs    := true
+  genStructProj   := true
   deriving BEq
 
 structure DefEq extends Erasure where
@@ -45,6 +46,7 @@ structure DefEq extends Erasure where
   etaExpand := false
   beta      := true
   levels    := true
+  structProj:= true
 
 structure Backend where
   blockInvalidMatches := true

Lean/Egg/Tactic/Premises/Gen/Derived.lean

@@ -17,9 +17,10 @@ private inductive DerivationCategory where
   | goalTcSpec
   | splits
   | explosion
+  | structureProj
 
 private def DerivationCategory.all : Array DerivationCategory :=
-  #[tcProj, tcSpec, goalTcSpec, splits, explosion]
+  #[tcProj, tcSpec, goalTcSpec, splits, explosion, structureProj]
 
 -- We maintain this theorem to ensure that we don't forget to add elements to
 -- `DerivationCategory.all`.
@@ -32,6 +33,7 @@ private def DerivationCategory.isEnabled (cfg : Config.Gen): DerivationCategory
   | goalTcSpec => cfg.genGoalTcSpec
   | splits     => cfg.genNestedSplits
   | explosion  => cfg.explosion
+  | structureProj => cfg.genStructProj
 
 -- Each index in this structure indicates to which point in `State.derived` a given derivation
 -- category has been applied. More precisely, these indices indicate the first element that has not
@@ -42,20 +44,23 @@ private structure State.Progress where
   goalTcSpec : Nat
   splits     : Nat
   explosion  : Nat
+  structProj : Nat
 
 private def State.Progress.get (p : Progress) : DerivationCategory → Nat
   | .tcProj     => p.tcProj
   | .tcSpec     => p.tcSpec
   | .goalTcSpec => p.goalTcSpec
   | .splits     => p.splits
   | .explosion  => p.explosion
+  | .structureProj => p.structProj
 
 private def State.Progress.set (p : Progress) : DerivationCategory → Nat → Progress
   | .tcProj,     n => { p with tcProj     := n }
   | .tcSpec,     n => { p with tcSpec     := n }
   | .goalTcSpec, n => { p with goalTcSpec := n }
   | .splits,     n => { p with splits     := n }
   | .explosion,  n => { p with explosion  := n }
+  | .structureProj, n => { p with structProj := n }
 
 private structure State where
   derived     : Rewrites
@@ -65,7 +70,7 @@ private structure State where
 private instance : EmptyCollection State where
   emptyCollection := {
     derived     := #[]
-    progress    := ⟨0, 0, 0, 0, 0⟩
+    progress    := ⟨0, 0, 0, 0, 0, 0⟩
     tcProjCover := ∅
   }
 
@@ -138,3 +143,5 @@ where
       let (rws, cover) ← genTcProjReductions targets (← tcProjCover) { cfg with amb }
       setTcProjCover cover
       return rws
+    generate cfg .structureProj do
+      genStructureProjections (← todo .structureProj) cfg.toDefEq