From 2078181d6ff8adc160455b0571dfb0ca5a42ec9a Mon Sep 17 00:00:00 2001
From: PratherConid <syxx2013050321@163.com>
Date: Tue, 26 Nov 2024 01:41:38 -0800
Subject: [PATCH] clean up corecheck code

---
 Auto/Lib/MetaExtra.lean       | 52 ++++++++++++-----------------------
 Auto/Tactic.lean              |  2 +-
 Auto/Translation/LamReif.lean |  4 ---
 3 files changed, 19 insertions(+), 39 deletions(-)

diff --git a/Auto/Lib/MetaExtra.lean b/Auto/Lib/MetaExtra.lean
index 06f4c9b..25e0f56 100644
--- a/Auto/Lib/MetaExtra.lean
+++ b/Auto/Lib/MetaExtra.lean
@@ -65,22 +65,9 @@ unsafe def evalFromMetaTactic : Tactic.Tactic
   Tactic.liftMetaTactic mt
 | _ => Elab.throwUnsupportedSyntax
 
-/-- We assume that `value` contains no free variables or metavariables -/
-def Meta.exprAddAndCompile (value : Expr) (declName : Name) : MetaM Unit := do
-  let type ← inferType value
-  let us := collectLevelParams {} value |>.params
-  let decl := Declaration.defnDecl {
-    name        := declName
-    levelParams := us.toList
-    type        := type
-    value       := value
-    hints       := ReducibilityHints.opaque
-    safety      := DefinitionSafety.unsafe
-  }
-  addDecl decl
-
-def Meta.coreCheck (e : Expr) : MetaM Unit := do
-  let startTime ← IO.monoMsNow
+-- **-TODO: Deal with mutual dependencies between mvar and fvar**
+-- **-      Maybe inspect the LocalContext in the metavariable declaration**
+def Meta.abstractAllMVarFVar (e : Expr) : MetaM Expr := do
   let mut curr := e
   -- **TODO: Fix**
   while true do
@@ -90,8 +77,8 @@ def Meta.coreCheck (e : Expr) : MetaM Unit := do
     curr := next
   let e := curr
   -- Now `(e == (← instantiateMVars) e) && (e == (← zetaReduce e))`
-  let res ← Meta.abstractMVars e
-  -- Now metavariables in `e` are abstracted
+  let res ← Meta.abstractMVars (levels := false) e
+  -- Now expr mvars in `e` are abstracted
   let mut e := res.expr
   -- **TODO: Fix**
   while true do
@@ -100,23 +87,20 @@ def Meta.coreCheck (e : Expr) : MetaM Unit := do
     e ← mkLambdaFVars (collectFVarsState.fvarIds.map Expr.fvar) e
     if !e.hasFVar then
       break
-  -- Use `Core.addAndCompile` to typecheck `e`
-  let coreChkStart ← IO.monoMsNow
-  trace[auto.metaExtra] "Meta.coreCheck :: Preprocessing done in {coreChkStart - startTime}"
-  let env ← getEnv
-  try
-    Meta.exprAddAndCompile e `_coreCheck
-  finally
-    trace[auto.metaExtra] "Meta.coreCheck :: Core check done in {(← IO.monoMsNow) - coreChkStart}"
-    setEnv env
+  let res ← Meta.abstractMVars (levels := true) e
+  -- Now level mvars in `e` are abstracted
+  -- Level mvars must be abstracted after fvars are abstracted,
+  --   because they may occur in fvars
+  return res.expr
+
+def Meta.coreCheck (e : Expr) : MetaM (Option Expr) := do
+  let e ← Meta.abstractAllMVarFVar e
+  match Kernel.check (← getEnv) {} e with
+  | Except.ok type => return .some type
+  | Except.error _ => return .none
 
 def Meta.isTypeCorrectCore (e : Expr) : MetaM Bool := do
-  try
-    Meta.coreCheck e
-    pure true
-  catch e =>
-    let msg := MessageData.compose "Meta.isTypeCorrectCore failed with message : \n" e.toMessageData
-    trace[auto.metaExtra] msg
-    pure false
+  let type? ← Meta.coreCheck e
+  return type?.isSome
 
 end Auto
diff --git a/Auto/Tactic.lean b/Auto/Tactic.lean
index d50352f..20060ff 100644
--- a/Auto/Tactic.lean
+++ b/Auto/Tactic.lean
@@ -131,7 +131,7 @@ def parseUOrDs (stxs : Array (TSyntax ``uord)) : TacticM (Array Prep.ConstUnfold
       defeqs := defeqs.append d
   return (unfolds, defeqs)
 
-def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : TacticM (Array Lemma) :=
+def collectLctxLemmas (lctxhyps : Bool) (ngoalAndBinders : Array FVarId) : MetaM (Array Lemma) :=
   Meta.withNewMCtxDepth do
     let fVarIds ← if lctxhyps then pure (← getLCtx).getFVarIds else pure ngoalAndBinders
     let mut lemmas := #[]
diff --git a/Auto/Translation/LamReif.lean b/Auto/Translation/LamReif.lean
index aabe7a5..49ddc87 100644
--- a/Auto/Translation/LamReif.lean
+++ b/Auto/Translation/LamReif.lean
@@ -1628,7 +1628,6 @@ section BuildChecker
       (.app (.const ``ilβ [u]) tyValExpr))
 
   def buildCPValExpr : ReifM Expr := do
-    -- let startTime ← IO.monoMsNow
     let u ← getU
     let tyValExpr ← buildTyVal
     let tyValTy := Expr.forallE `_ (.const ``Nat []) (.sort (.succ u)) .default
@@ -1637,9 +1636,6 @@ section BuildChecker
       let ilExpr ← buildILExpr tyValFVarExpr
       let checkerValuationExpr := Lean.mkApp3 (.const ``CPVal.mk [u]) tyValExpr varExpr ilExpr
       Meta.mkLetFVars #[tyValFVarExpr] checkerValuationExpr
-    -- if !(← Meta.isTypeCorrectCore lamValuationExpr) then
-    --   throwError "buildLamValuation :: Malformed LamValuation"
-    -- trace[auto.buildChecker] "LamValuation typechecked in time {(← IO.monoMsNow) - startTime}"
     return lamValuationExpr
 
   /-- `lvalExpr` is the `LamValuation` -/