chore: add aux fixpoint

library/Init/Lean/Meta/Default.lean

@@ -7,39 +7,51 @@ prelude
 import Init.Lean.Meta.Basic
 import Init.Lean.Meta.WHNF
 import Init.Lean.Meta.InferType
+import Init.Lean.Meta.FunInfo
+import Init.Lean.Meta.DefEq
+
+namespace Lean
+namespace Meta
 
-#exit
 /- =========================================== -/
 /- BIG HACK until we add `mutual` keyword back -/
 /- =========================================== -/
-inductive TypeUtilOp
-| whnfOp | inferTypeOp | isDefEqOp
-open TypeUtilOp
+inductive MetaOp
+| whnfOp | inferTypeOp | isDefEqOp | synthPendingOp
+
+open MetaOp
+
 private def exprToBool : Expr → Bool
 | Expr.sort Level.zero => false
 | _                    => true
+
 private def boolToExpr : Bool → Expr
 | false => Expr.sort Level.zero
 | true  => Expr.bvar 0
 
-private partial def auxFixpoint [AbstractMetavarContext σ] [AbstractTypeUtilCache ϕ] : TypeUtilOp → Expr → Expr → TypeUtilM σ ϕ Expr
+private partial def auxFixpoint : MetaOp → Expr → Expr → MetaM Expr
 | op, e₁, e₂ =>
-  let whnf      := fun e => auxFixpoint whnfOp e e;
-  let inferType := fun e => auxFixpoint inferTypeOp e e;
-  let isDefEq   := fun e₁ e₂ => exprToBool <$> auxFixpoint isDefEqOp e₁ e₂;
+  let whnf         := fun e => auxFixpoint whnfOp e e;
+  let inferType    := fun e => auxFixpoint inferTypeOp e e;
+  let isDefEq      := fun e₁ e₂ => pure false; -- TODO
+  let synthPending := fun e => pure false;     -- TODO
   match op with
-  | whnfOp      => whnfAux whnf inferType isDefEq e₁
-  | inferTypeOp => inferTypeAux whnf inferType isDefEq e₁
-  | isDefEqOp   => boolToExpr <$> isDefEqAux whnf inferType isDefEq e₁ e₂
+  | whnfOp         => whnfAux inferType isDefEq synthPending e₁
+  | inferTypeOp    => inferType e₁
+  | synthPendingOp => boolToExpr <$> synthPending e₁
+  | isDefEqOp      => boolToExpr <$> isDefEq e₁ e₂
 
-def whnf [AbstractMetavarContext σ] [AbstractTypeUtilCache ϕ] (e : Expr) : TypeUtilM σ ϕ Expr :=
+def whnf (e : Expr) : MetaM Expr :=
 auxFixpoint whnfOp e e
 
-def inferType [AbstractMetavarContext σ] [AbstractTypeUtilCache ϕ] (e : Expr) : TypeUtilM σ ϕ Expr :=
+def inferType (e : Expr) : MetaM Expr :=
 auxFixpoint inferTypeOp e e
 
-def isDefEq [AbstractMetavarContext σ] [AbstractTypeUtilCache ϕ] (e₁ e₂ : Expr) : TypeUtilM σ ϕ Bool :=
+def isDefEq (e₁ e₂ : Expr) : MetaM Bool :=
 exprToBool <$> auxFixpoint isDefEqOp e₁ e₂
 /- =========================================== -/
 /-          END OF BIG HACK                    -/
 /- =========================================== -/
+
+end Meta
+end Lean

library/Init/Lean/Meta/WHNF.lean

@@ -23,7 +23,7 @@ do t ← getTransparency;
 do t ← getTransparency;
    modify $ fun s => { cache := { whnf := s.cache.whnf.insert (t, e) r, .. s.cache }, .. s }
 
-@[specialize] private partial def whnfAux
+@[specialize] partial def whnfAux
     (inferType         : Expr → MetaM Expr)
     (isDefEq           : Expr → Expr → MetaM Bool)
     (synthesizePending : Expr → MetaM Bool)