Pantograph/Frontend/Elab.lean

@@ -168,10 +168,9 @@ private def collectSorrysInTree (t : Elab.InfoTree) : List InfoWithContext :=
   let infos := findAllInfo t none fun i => match i with
     | .ofTermInfo { expectedType?, expr, stx, .. } =>
       expr.isSorry ∧ expectedType?.isSome ∧ stx.isOfKind `Lean.Parser.Term.sorry
-    | .ofTacticInfo { stx, goalsBefore, .. } =>
+    | .ofTacticInfo { stx, .. } =>
       -- The `sorry` term is distinct from the `sorry` tactic
-      let isSorry := stx.isOfKind `Lean.Parser.Tactic.tacticSorry
-      isSorry ∧ !goalsBefore.isEmpty
+      stx.isOfKind `Lean.Parser.Tactic.tacticSorry
     | _ => false
   infos.map fun (info, context?, _) => { info, context? }
 
@@ -198,9 +197,9 @@ def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM GoalState := do
     | .ofTacticInfo tacticInfo => do
       MetaTranslate.translateMVarFromTacticInfoBefore tacticInfo i.context?
     | _ => panic! "Invalid info"
-  let goals := List.join (← goalsM.run {} |>.run' {})
+  let goals := (← goalsM.run {} |>.run' {}).bind id
   let root := match goals with
-    | [] => panic! "No MVars generated"
+    | [] => panic! "This function cannot be called on an empty list"
     | [g] => g
     | _ => { name := .anonymous }
   GoalState.createFromMVars goals root

Pantograph/Frontend/MetaTranslate.lean

@@ -39,28 +39,8 @@ def resetFVarMap : MetaTranslateM Unit := do
   modifyGet λ state => ((), { state with fvarMap := {} })
 
 mutual
-private partial def translateLevel (srcLevel: Level) : MetaTranslateM Level := do
-  let sourceMCtx ← getSourceMCtx
-  let (_, level) := instantiateLevelMVarsImp sourceMCtx srcLevel
-  match level with
-  | .zero => return .zero
-  | .succ inner => do
-    let inner' ← translateLevel inner
-    return .succ inner'
-  | .max l1 l2 => do
-    let l1' ← translateLevel l1
-    let l2' ← translateLevel l2
-    return .max l1' l2'
-  | .imax l1 l2 => do
-    let l1' ← translateLevel l1
-    let l2' ← translateLevel l2
-    return .imax l1' l2'
-  | .param p => return .param p
-  | .mvar _ =>
-    Meta.mkFreshLevelMVar
 private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
   let sourceMCtx ← getSourceMCtx
-  -- We want to create as few mvars as possible
   let (srcExpr, _) := instantiateMVarsCore (mctx := sourceMCtx) srcExpr
   --IO.println s!"Transform src: {srcExpr}"
   let result ← Core.transform srcExpr λ e => do
@@ -71,7 +51,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
       assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
-      -- Must not be assigned
+      assert! !(sourceMCtx.dAssignment.contains mvarId)
       assert! !(sourceMCtx.eAssignment.contains mvarId)
       match state.mvarMap[mvarId]? with
       | .some mvarId' => do
@@ -82,9 +62,6 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
         let mvarId' ← translateMVarId mvarId
         restoreFVarMap fvarMap
         return .done $ .mvar mvarId'
-    | .sort level => do
-      let level' ← translateLevel level
-      return .done $ .sort level'
     | _ => return .continue
   Meta.check result
   return result
@@ -118,23 +95,16 @@ partial def translateLCtx : MetaTranslateM LocalContext := do
 partial def translateMVarId (srcMVarId: MVarId) : MetaTranslateM MVarId := do
   if let .some mvarId' := (← get).mvarMap[srcMVarId]? then
     return mvarId'
-  let mvarId' ← Meta.withLCtx .empty #[] do
+  let mvar ← Meta.withLCtx .empty #[] do
     let srcDecl := (← getSourceMCtx).findDecl? srcMVarId |>.get!
     withTheReader Context (λ ctx => { ctx with sourceLCtx := srcDecl.lctx }) do
       let lctx' ← translateLCtx
       let localInstances' ← srcDecl.localInstances.mapM translateLocalInstance
       Meta.withLCtx lctx' localInstances' do
         let target' ← translateExpr srcDecl.type
-        let mvar' ← Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
-        let mvarId' := mvar'.mvarId!
-        if let .some { fvars, mvarIdPending }:= (← getSourceMCtx).getDelayedMVarAssignmentExp srcMVarId then
-          -- Map the fvars in the pending context.
-          let mvarIdPending' ← translateMVarId mvarIdPending
-          let fvars' ← mvarIdPending'.withContext $ fvars.mapM translateExpr
-          assignDelayedMVar mvarId' fvars' mvarIdPending'
-        pure mvarId'
-  addTranslatedMVar srcMVarId mvarId'
-  return mvarId'
+        Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
+  addTranslatedMVar srcMVarId mvar.mvarId!
+  return mvar.mvarId!
 end
 
 def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)