Pantograph/Frontend/Elab.lean

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

Pantograph/Frontend/MetaTranslate.lean

@@ -39,8 +39,28 @@ 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
@@ -51,7 +71,7 @@ private partial def translateExpr (srcExpr: Expr) : MetaTranslateM Expr := do
       assert! (← getLCtx).contains fvarId'
       return .done $ .fvar fvarId'
     | .mvar mvarId => do
-      assert! !(sourceMCtx.dAssignment.contains mvarId)
+      -- Must not be assigned
       assert! !(sourceMCtx.eAssignment.contains mvarId)
       match state.mvarMap[mvarId]? with
       | .some mvarId' => do
@@ -62,6 +82,9 @@ 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
@@ -95,16 +118,23 @@ 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 mvar ← Meta.withLCtx .empty #[] do
+  let mvarId' ← 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
-        Meta.mkFreshExprMVar target' srcDecl.kind srcDecl.userName
-  addTranslatedMVar srcMVarId mvar.mvarId!
-  return mvar.mvarId!
+        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'
 end
 
 def translateMVarFromTermInfo (termInfo : Elab.TermInfo) (context? : Option Elab.ContextInfo)