Merge branch 'dev' into tactic/eval

2024-08-15 22:45:43 -07:00 · 2024-08-15 22:45:43 -07:00 · e07f9d9b3f
parent df8b6602ee 56100a30af
commit e07f9d9b3f
13 changed files with 192 additions and 184 deletions
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@ -1,21 +1,13 @@
 /- structures for FFI based interface -/
 import Lean
+import Pantograph.Goal
+import Pantograph.Expr
+import Pantograph.Protocol

 open Lean

-namespace Pantograph.Condensed
-
-/-
-These two functions are for user defiend names. For internal names such as
-`_uniq`, it is favourable to use `lean_name_hash_exported` and `lean_name_eq` to
-construct hash maps for Lean names.
-/
-@[export pantograph_str_to_name]
-def strToName (s: String) : Name := s.toName
-@[export pantograph_name_to_str]
-def nameToStr (s: String) : Name := s.toName
-@[export pantograph_name_is_inaccessible]
-def isInaccessible (n: Name) : Bool := n.isInaccessibleUserName
+namespace Pantograph
+namespace Condensed

 -- Mirrors Lean's LocalDecl
 structure LocalDecl where
@ -36,7 +28,69 @@ structure Goal where
@[export pantograph_goal_is_lhs]
 def isLHS (g: Goal) : Bool := isLHSGoal? g.target |>.isSome

+-- Functions for creating contexts and states
+@[export pantograph_elab_context]
+def elabContext: Elab.Term.Context := {
+    errToSorry := false
+  }

+end Condensed

+-- Get the list of visible (by default) free variables from a goal
+@[export pantograph_visible_fvars_of_mvar]
+protected def visibleFVarsOfMVar (mctx: MetavarContext) (mvarId: MVarId): Option (Array FVarId) := do
+  let mvarDecl ← mctx.findDecl? mvarId
+  let lctx := mvarDecl.lctx
+  return lctx.decls.foldl (init := #[]) fun r decl? => match decl? with
+    | some decl => if decl.isAuxDecl ∨ decl.isImplementationDetail then r else r.push decl.fvarId
+    | none      => r

-end Pantograph.Condensed
+@[export pantograph_to_condensed_goal_m]
+def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
+  let ppAuxDecls     := Meta.pp.auxDecls.get (← getOptions)
+  let ppImplDetailHyps := Meta.pp.implementationDetailHyps.get (← getOptions)
+  let mvarDecl ← mvarId.getDecl
+  let lctx     := mvarDecl.lctx
+  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
+  Meta.withLCtx lctx mvarDecl.localInstances do
+    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
+      match localDecl with
+      | .cdecl _ fvarId userName type _ _ =>
+        let type ← instantiate type
+        return { fvarId, userName, type }
+      | .ldecl _ fvarId userName type value _ _ => do
+        let userName := userName.simpMacroScopes
+        let type ← instantiate type
+        let value ← instantiate value
+        return { fvarId, userName, type, value? := .some value }
+    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
+      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
+        !ppImplDetailHyps && localDecl.isImplementationDetail
+      if skip then
+        return acc
+      else
+        let var ← ppVar localDecl
+        return var::acc
+    return {
+        mvarId,
+        userName := mvarDecl.userName,
+        context := vars.reverse.toArray,
+        target := ← instantiate mvarDecl.type
+    }
+  where
+  instantiate := instantiateAll
+
+@[export pantograph_goal_state_to_condensed_m]
+protected def GoalState.toCondensed (state: GoalState):
+    CoreM (Array Condensed.Goal):= do
+  let metaM := do
+    let goals := state.goals.toArray
+    goals.mapM fun goal => do
+      match state.mctx.findDecl? goal with
+      | .some _ =>
+        let serializedGoal ← toCondensedGoal goal
+        pure serializedGoal
+      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
+  metaM.run' (s := state.savedState.term.meta.meta)
+
+end Pantograph
--- a/Pantograph/Environment.lean
+++ b/Pantograph/Environment.lean
@ -7,15 +7,36 @@ open Pantograph

 namespace Pantograph.Environment

-def isNameInternal (n: Lean.Name): Bool :=
+@[export pantograph_is_name_internal]
+def isNameInternal (n: Name): Bool :=
  -- Returns true if the name is an implementation detail which should not be shown to the user.
  isLeanSymbol n ∨ (Lean.privateToUserName? n |>.map isLeanSymbol |>.getD false) ∨ n.isAuxLemma ∨ n.hasMacroScopes
  where
-  isLeanSymbol (name: Lean.Name): Bool := match name.getRoot with
+  isLeanSymbol (name: Name): Bool := match name.getRoot with
    | .str _ name => name == "Lean"
    | _ => true

-def toCompactSymbolName (n: Lean.Name) (info: Lean.ConstantInfo): String :=
+/-- Catalog all the non-internal and safe names -/
+@[export pantograph_environment_catalog]
+def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
+  match isNameInternal name || info.isUnsafe with
+  | false => acc.push name
+  | true => acc)
+
+@[export pantograph_environment_module_of_name]
+def module_of_name (env: Environment) (name: Name): Option Name := do
+  let moduleId ←  env.getModuleIdxFor? name
+  return env.allImportedModuleNames.get! moduleId.toNat
+
+@[export pantograph_constant_info_is_unsafe_or_partial]
+def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial
+
+@[export pantograph_constant_info_type]
+def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type
+@[export pantograph_constant_info_value]
+def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas
+
+def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
  let pref := match info with
  | .axiomInfo  _ => "a"
  | .defnInfo   _ => "d"
--- a/Pantograph/Expr.lean
+++ b/Pantograph/Expr.lean
@ -4,9 +4,29 @@ open Lean

 namespace Pantograph

+structure ProjectionApplication where
+  projector: Name
+  numParams: Nat
+  inner: Expr
+
+@[export pantograph_expr_proj_to_app]
+def exprProjToApp (env: Environment) (e: Expr): ProjectionApplication :=
+  let (typeName, idx, inner) := match e with
+    | .proj typeName idx inner => (typeName, idx, inner)
+    | _ => panic! "Argument must be proj"
+  let ctor := getStructureCtor env typeName
+  let fieldName := getStructureFields env typeName |>.get! idx
+  let projector := getProjFnForField? env typeName fieldName |>.get!
+  {
+    projector,
+    numParams := ctor.numParams,
+    inner,
+  }
+
 def _root_.Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxLemma") _

 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
+@[export pantograph_unfold_aux_lemmas]
 def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
  Lean.Meta.deltaExpand e Lean.Name.isAuxLemma

@ -98,7 +118,7 @@ Convert an expression to an equiavlent form with
 2. No aux lemmas
 3. No assigned mvars
 -/
-@[export pantograph_instantiate_all_meta_m]
+@[export pantograph_instantiate_all_m]
 def instantiateAll (e: Expr): MetaM Expr := do
  let e ← instantiateDelayedMVars e
  let e ← unfoldAuxLemmas e
@ -111,7 +131,7 @@ structure DelayedMVarInvocation where
  tail: Array Expr

 -- The pending mvar of any delayed assigned mvar must not be assigned in any way.
-@[export pantograph_to_delayed_mvar_invocation_meta_m]
+@[export pantograph_to_delayed_mvar_invocation_m]
 def toDelayedMVarInvocation (e: Expr): MetaM (Option DelayedMVarInvocation) := do
  let .mvar mvarId := e.getAppFn | return .none
  let .some decl ← getDelayedMVarAssignment? mvarId | return .none
--- a/Pantograph/Goal.lean
+++ b/Pantograph/Goal.lean
@ -34,6 +34,7 @@ structure GoalState where
  -- WARNING: If using `state with` outside of `calc`, this must be set to `.none`
  calcPrevRhs?: Option Expr := .none

+@[export pantograph_goal_state_create_m]
 protected def GoalState.create (expr: Expr): Elab.TermElabM GoalState := do
  -- May be necessary to immediately synthesise all metavariables if we need to leave the elaboration context.
  -- See https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Unknown.20universe.20metavariable/near/360130070
@ -54,6 +55,8 @@ protected def GoalState.isConv (state: GoalState): Bool :=
  state.convMVar?.isSome
 protected def GoalState.goals (state: GoalState): List MVarId :=
  state.savedState.tactic.goals
+@[export pantograph_goal_state_goals]
+protected def GoalState.goalsArray (state: GoalState): Array MVarId := state.goals.toArray
 protected def GoalState.mctx (state: GoalState): MetavarContext :=
  state.savedState.term.meta.meta.mctx
 protected def GoalState.env (state: GoalState): Environment :=
@ -109,6 +112,7 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
 /--
 Brings into scope a list of goals
 -/
+@[export pantograph_goal_state_resume]
 protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
  if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
    let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
@ -137,6 +141,7 @@ protected def GoalState.continue (target: GoalState) (branch: GoalState): Except
  else
    target.resume (goals := branch.goals)

+@[export pantograph_goal_state_root_expr]
 protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
  let expr ← goalState.mctx.eAssignment.find? goalState.root
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
@ -147,12 +152,14 @@ protected def GoalState.rootExpr? (goalState: GoalState): Option Expr := do
  else
    assert! goalState.goals.isEmpty
    return expr
+@[export pantograph_goal_state_parent_expr]
 protected def GoalState.parentExpr? (goalState: GoalState): Option Expr := do
  let parent ← goalState.parentMVar?
  let expr := goalState.mctx.eAssignment.find! parent
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
  return expr
-protected def GoalState.assignedExprOf? (goalState: GoalState) (mvar: MVarId): Option Expr := do
+@[export pantograph_goal_state_get_mvar_e_assignment]
+protected def GoalState.getMVarEAssignment (goalState: GoalState) (mvar: MVarId): Option Expr := do
  let expr ← goalState.mctx.eAssignment.find? mvar
  let (expr, _) := instantiateMVarsCore (mctx := goalState.mctx) (e := expr)
  return expr
@ -172,13 +179,14 @@ inductive TacticResult where
  -- The given action cannot be executed in the state
  | invalidAction (message: String)

-protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
+/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.tryTacticM (state: GoalState) (goalId: Nat) (tacticM: Elab.Tactic.TacticM Unit):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  let goal ← match state.savedState.tactic.goals.get? goalId with
    | .some goal => pure $ goal
    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.execute
+  goal.checkNotAssigned `GoalState.tryTacticM
  try
    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
    if (← getThe Core.State).messages.hasErrors then
@ -198,7 +206,7 @@ protected def GoalState.execute (state: GoalState) (goalId: Nat) (tacticM: Elab.
  catch exception =>
    return .failure #[← exception.toMessageData.toString]

-/-- Execute tactic on given state -/
+/-- Execute a string tactic on given state -/
 protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: String):
    Elab.TermElabM TacticResult := do
  let tactic ← match Parser.runParserCategory
@ -208,68 +216,19 @@ protected def GoalState.tryTactic (state: GoalState) (goalId: Nat) (tactic: Stri
    (fileName := filename) with
    | .ok stx => pure $ stx
    | .error error => return .parseError error
-  state.execute goalId $ Elab.Tactic.evalTactic tactic
-
-/-- Assumes elabM has already been restored. Assumes expr has already typechecked -/
-protected def GoalState.assign (state: GoalState) (goal: MVarId) (expr: Expr):
-      Elab.TermElabM TacticResult := do
-  let goalType ← goal.getType
-  try
-    -- For some reason this is needed. One of the unit tests will fail if this isn't here
-    let error?: Option String ← goal.withContext do
-      let exprType ← Meta.inferType expr
-      if ← Meta.isDefEq goalType exprType then
-        pure .none
-      else do
-        return .some s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} != {← Meta.ppExpr goalType}"
-    if let .some error := error? then
-      return .parseError error
-    goal.checkNotAssigned `GoalState.assign
-    goal.assign expr
-    if (← getThe Core.State).messages.hasErrors then
-      let messages := (← getThe Core.State).messages.toArray
-      let errors ← (messages.map (·.data)).mapM fun md => md.toString
-      return .failure errors
-    let prevMCtx := state.savedState.term.meta.meta.mctx
-    let nextMCtx ← getMCtx
-    -- Generate a list of mvarIds that exist in the parent state; Also test the
-    -- assertion that the types have not changed on any mvars.
-    let newMVars := newMVarSet prevMCtx nextMCtx
-    let nextGoals ← newMVars.toList.filterM (not <$> ·.isAssigned)
-    return .success {
-      root := state.root,
-      savedState := {
-        term := ← MonadBacktrack.saveState,
-        tactic := { goals := nextGoals }
-      },
-      newMVars,
-      parentMVar? := .some goal,
-      calcPrevRhs? := .none
-    }
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.tryTacticM goalId $ Elab.Tactic.evalTactic tactic

 protected def GoalState.tryAssign (state: GoalState) (goalId: Nat) (expr: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
-  let goal ← match state.savedState.tactic.goals.get? goalId with
-    | .some goal => pure goal
-    | .none => return .indexError goalId
-  goal.checkNotAssigned `GoalState.tryAssign
  let expr ← match Parser.runParserCategory
-    (env := state.env)
+    (env := ← MonadEnv.getEnv)
    (catName := `term)
    (input := expr)
    (fileName := filename) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  let goalType ← goal.getType
-  try
-    let expr ← goal.withContext $
-      Elab.Term.elabTermAndSynthesize (stx := expr) (expectedType? := .some goalType)
-    state.assign goal expr
-  catch exception =>
-    return .failure #[← exception.toMessageData.toString]
+  state.tryTacticM goalId $ Tactic.evalAssign expr

 -- Specialized Tactics

@ -475,13 +434,13 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
  let recursor ← match (← Compile.parseTermM recursor) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+  state.tryTacticM goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
  let eq ← match (← Compile.parseTermM eq) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.noConfuse eq)
+  state.tryTacticM goalId (tacticM := Tactic.noConfuse eq)

 end Pantograph
--- a/Pantograph/Library.lean
+++ b/Pantograph/Library.lean
@ -1,3 +1,4 @@
+import Pantograph.Condensed
 import Pantograph.Environment
 import Pantograph.Goal
 import Pantograph.Protocol
@ -38,13 +39,10 @@ open Lean

 namespace Pantograph

-def defaultTermElabMContext: Elab.Term.Context := {
-    errToSorry := false
-  }
 def runMetaM { α } (metaM: MetaM α): CoreM α :=
  metaM.run'
 def runTermElabM { α } (termElabM: Elab.TermElabM α): CoreM α :=
-  termElabM.run' (ctx := defaultTermElabMContext) |>.run'
+  termElabM.run' (ctx := Condensed.elabContext) |>.run'

 def errorI (type desc: String): Protocol.InteractionError := { error := type, desc := desc }

@ -78,26 +76,12 @@ def createCoreState (imports: Array String): IO Core.State := do
    (trustLevel := 1)
  return { env := env }

-@[export pantograph_create_meta_context]
-def createMetaContext: IO Lean.Meta.Context := do
-  return {}
-
-@[export pantograph_env_catalog_m]
-def envCatalog: CoreM Protocol.EnvCatalogResult :=
-  Environment.catalog ({}: Protocol.EnvCatalog)
-
-@[export pantograph_env_inspect_m]
-def envInspect (name: String) (value: Bool) (dependency: Bool) (options: @&Protocol.Options):
-    CoreM (Protocol.CR Protocol.EnvInspectResult) :=
-  Environment.inspect ({
-    name, value? := .some value, dependency?:= .some dependency
-  }: Protocol.EnvInspect) options
-
@[export pantograph_env_add_m]
 def envAdd (name: String) (type: String) (value: String) (isTheorem: Bool):
    CoreM (Protocol.CR Protocol.EnvAddResult) :=
  Environment.addDecl { name, type, value, isTheorem }

+@[export pantograph_parse_elab_type_m]
 def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
  let env ← MonadEnv.getEnv
  let syn ← match parseTerm env type with
@ -108,6 +92,7 @@ def parseElabType (type: String): Elab.TermElabM (Protocol.CR Expr) := do
  | .ok expr => return .ok (← instantiateMVars expr)

 /-- This must be a TermElabM since the parsed expr contains extra information -/
+@[export pantograph_parse_elab_expr_m]
 def parseElabExpr (expr: String) (expectedType?: Option String := .none): Elab.TermElabM (Protocol.CR Expr) := do
  let env ← MonadEnv.getEnv
  let expectedType? ← match ← expectedType?.mapM parseElabType with
@ -169,9 +154,6 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): CoreM Protocol.G
        state.withParentContext do
          serializeExpression options (← instantiateAll expr)),
    }
-@[export pantograph_goal_diag_m]
-def goalDiag (state: GoalState) (diagOptions: Protocol.GoalDiag) : CoreM String :=
-  runMetaM $ state.diag diagOptions

@[export pantograph_goal_tactic_m]
 def goalTactic (state: GoalState) (goalId: Nat) (tactic: String): CoreM TacticResult :=
@ -186,7 +168,7 @@ protected def GoalState.tryHave (state: GoalState) (goalId: Nat) (binderName: St
    | .error error => return .parseError error
  runTermElabM do
    state.restoreElabM
-    state.execute goalId (Tactic.«have» binderName.toName type)
+    state.tryTacticM goalId (Tactic.«have» binderName.toName type)
@[export pantograph_goal_evaluate_m]
 protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName: String) (expr: String): CoreM TacticResult := do
  let expr ← match (← Compile.parseTermM expr) with
@ -194,7 +176,7 @@ protected def GoalState.tryEvaluate (state: GoalState) (goalId: Nat) (binderName
    | .error error => return .parseError error
  runTermElabM do
    state.restoreElabM
-    state.execute goalId (Tactic.evaluate binderName.toName expr)
+    state.tryTacticM goalId (Tactic.evaluate binderName.toName expr)
@[export pantograph_goal_let_m]
 def goalLet (state: GoalState) (goalId: Nat) (binderName: String) (type: String): CoreM TacticResult :=
  runTermElabM <| state.tryLet goalId binderName type
@ -217,20 +199,4 @@ def goalMotivatedApply (state: GoalState) (goalId: Nat) (recursor: String): Core
 def goalNoConfuse (state: GoalState) (goalId: Nat) (eq: String): CoreM TacticResult :=
  runTermElabM <| state.tryNoConfuse goalId eq

-inductive SyntheticTactic where
-  | congruenceArg
-  | congruenceFun
-  | congruence
-/-- Executes a synthetic tactic which has no arguments -/
-@[export pantograph_goal_synthetic_tactic_m]
-def goalSyntheticTactic (state: GoalState) (goalId: Nat) (case: SyntheticTactic): CoreM TacticResult :=
-  runTermElabM do
-    state.restoreElabM
-    state.execute goalId $ match case with
-      | .congruenceArg => Tactic.congruenceArg
-      | .congruenceFun => Tactic.congruenceFun
-      | .congruence => Tactic.congruence
-
-
-
 end Pantograph
--- a/Pantograph/Serial.lean
+++ b/Pantograph/Serial.lean
@ -168,15 +168,12 @@ partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM
      -- NOTE: Equivalent to expr itself, but mdata influences the prettyprinter
      -- It may become necessary to incorporate the metadata.
      self inner
-    | .proj typeName idx inner => do
+    | .proj _ _ _ => do
      let env ← getEnv
-      let ctor := getStructureCtor env typeName
-      let fieldName := getStructureFields env typeName |>.get! idx
-      let projectorName := getProjFnForField? env typeName fieldName |>.get!
-
-      let autos := String.intercalate " " (List.replicate ctor.numParams "_")
-      let inner ← self inner
-      pure s!"((:c {projectorName}) {autos} {inner})"
+      let projApp := exprProjToApp env e
+      let autos := String.intercalate " " (List.replicate projApp.numParams "_")
+      let inner ← self projApp.inner
+      pure s!"((:c {projApp.projector}) {autos} {inner})"
  -- Elides all unhygenic names
  binderInfoSexp : Lean.BinderInfo → String
    | .default => ""
@ -201,54 +198,6 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
    dependentMVars?,
  }

-@[export pantograph_to_condensed_goal]
-def toCondensedGoal (mvarId: MVarId): MetaM Condensed.Goal := do
-  let options: Protocol.Options := {}
-  let ppAuxDecls       := options.printAuxDecls
-  let ppImplDetailHyps := options.printImplementationDetailHyps
-  let mvarDecl ← mvarId.getDecl
-  let lctx     := mvarDecl.lctx
-  let lctx     := lctx.sanitizeNames.run' { options := (← getOptions) }
-  Meta.withLCtx lctx mvarDecl.localInstances do
-    let ppVar (localDecl : LocalDecl) : MetaM Condensed.LocalDecl := do
-      match localDecl with
-      | .cdecl _ fvarId userName type _ _ =>
-        let type ← instantiate type
-        return { fvarId, userName, type }
-      | .ldecl _ fvarId userName type value _ _ => do
-        let userName := userName.simpMacroScopes
-        let type ← instantiate type
-        let value ← instantiate value
-        return { fvarId, userName, type, value? := .some value }
-    let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
-      let skip := !ppAuxDecls && localDecl.isAuxDecl ||
-        !ppImplDetailHyps && localDecl.isImplementationDetail
-      if skip then
-        return acc
-      else
-        let var ← ppVar localDecl
-        return var::acc
-    return {
-        mvarId,
-        userName := mvarDecl.userName,
-        context := vars.reverse.toArray,
-        target := ← instantiate mvarDecl.type
-    }
-  where
-  instantiate := instantiateAll
-
-@[export pantograph_goal_state_to_condensed]
-protected def GoalState.toCondensed (state: GoalState):
-    CoreM (Array Condensed.Goal):= do
-  let metaM := do
-    let goals := state.goals.toArray
-    goals.mapM fun goal => do
-      match state.mctx.findDecl? goal with
-      | .some _ =>
-        let serializedGoal ← toCondensedGoal goal
-        pure serializedGoal
-      | .none => throwError s!"Metavariable does not exist in context {goal.name}"
-  metaM.run' (s := state.savedState.term.meta.meta)

 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl := .none)
@ -337,7 +286,8 @@ protected def GoalState.serializeGoals
    | .none => throwError s!"Metavariable does not exist in context {goal.name}"

 /-- Print the metavariables in a readable format -/
-protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM String := do
+@[export pantograph_goal_state_diag_m]
+protected def GoalState.diag (goalState: GoalState) (parent?: Option GoalState := .none) (options: Protocol.GoalDiag := {}): MetaM String := do
  goalState.restoreMetaM
  let savedState := goalState.savedState
  let goals := savedState.tactic.goals
@ -356,7 +306,7 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
  let resultOthers ← mctx.decls.toList.filter (λ (mvarId, _) =>
      !(goals.contains mvarId || mvarId == root) && options.printAll)
      |>.mapM (fun (mvarId, decl) => do
-        let pref := if goalState.newMVars.contains mvarId then "~" else " "
+        let pref := if parentHasMVar mvarId then " " else "~"
        printMVar pref mvarId decl
      )
  pure $ result ++ "\n" ++ (resultGoals.map (· ++ "\n") |> String.join) ++ (resultOthers.map (· ++ "\n") |> String.join)
@ -396,5 +346,6 @@ protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag
    userNameToString : Name → String
      | .anonymous => ""
      | other => s!"[{other}]"
+    parentHasMVar (mvarId: MVarId): Bool := parent?.map (λ state => state.mctx.decls.contains mvarId) |>.getD true

 end Pantograph
--- a/Pantograph/Tactic.lean
+++ b/Pantograph/Tactic.lean
@ -1,3 +1,4 @@
+import Pantograph.Tactic.Assign
 import Pantograph.Tactic.Congruence
 import Pantograph.Tactic.MotivatedApply
 import Pantograph.Tactic.NoConfuse
--- a/Pantograph/Tactic/Assign.lean
+++ b/Pantograph/Tactic/Assign.lean
@ -0,0 +1,35 @@
+import Lean
+
+open Lean
+
+namespace Pantograph.Tactic
+
+private def newMVarSet (mctxOld: @&MetavarContext) (mctxNew: @&MetavarContext): SSet MVarId :=
+  mctxNew.decls.foldl (fun acc mvarId mvarDecl =>
+    if let .some prevMVarDecl := mctxOld.decls.find? mvarId then
+      assert! prevMVarDecl.type == mvarDecl.type
+      acc
+    else
+      acc.insert mvarId
+    ) SSet.empty
+def assign (goal: MVarId) (expr: Expr): MetaM (List MVarId) := do
+  goal.checkNotAssigned `Pantograph.Tactic.assign
+
+  -- This run of the unifier is critical in resolving mvars in passing
+  let exprType ← Meta.inferType expr
+  let goalType ← goal.getType
+  unless ← Meta.isDefEq goalType exprType do
+    throwError s!"{← Meta.ppExpr expr} : {← Meta.ppExpr exprType} ≠ {← Meta.ppExpr goalType}"
+
+  let nextGoals ← Meta.getMVars expr
+  goal.assign expr
+  nextGoals.toList.filterM (not <$> ·.isAssigned)
+
+def evalAssign : Elab.Tactic.Tactic := fun stx => Elab.Tactic.withMainContext do
+  let goalType ← Elab.Tactic.getMainTarget
+  let expr ← Elab.Term.elabTermAndSynthesize (stx := stx) (expectedType? := .some goalType)
+  let nextGoals ← assign (← Elab.Tactic.getMainGoal) expr
+  Elab.Tactic.setGoals nextGoals
+
+
+end Pantograph.Tactic
--- a/Test/Common.lean
+++ b/Test/Common.lean
@ -88,9 +88,9 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array
 def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq :=
  runCoreMSeq env metaM.run'
 def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α :=
-  termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+  termElabM.run' (ctx := Condensed.elabContext)
 def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq :=
-  runMetaMSeq env $ termElabM.run' (ctx := Pantograph.defaultTermElabMContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)

 def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e

--- a/Test/Metavar.lean
+++ b/Test/Metavar.lean
@ -67,7 +67,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options

  let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
@ -198,10 +198,10 @@ def test_proposition_generation: TestM Unit := do
      addTest $ assertUnreachable $ other.toString
      return ()
  addTest $ LSpec.check ":= λ (x: Nat), _" ((← state2.serializeGoals (options := ← read)).map (·.target.pp?) =
-    #[.some "Nat → Prop", .some "∀ (x : Nat), ?m.29 x"])
+    #[.some "∀ (x : Nat), ?m.29 x"])
  addTest $ LSpec.test "(2 root)" state2.rootExpr?.isNone

-  let state3 ← match ← state2.tryAssign (goalId := 1) (expr := "fun x => Eq.refl x") with
+  let state3 ← match ← state2.tryAssign (goalId := 0) (expr := "fun x => Eq.refl x") with
    | .success state => pure state
    | other => do
      addTest $ assertUnreachable $ other.toString
--- a/Test/Proofs.lean
+++ b/Test/Proofs.lean
@ -76,7 +76,7 @@ def proofRunner (env: Lean.Environment) (tests: TestM Unit): IO LSpec.TestSeq :=
  let termElabM := tests.run LSpec.TestSeq.done |>.run {} -- with default options

  let coreContext: Lean.Core.Context ← createCoreContext #[]
-  let metaM := termElabM.run' (ctx := defaultTermElabMContext)
+  let metaM := termElabM.run' (ctx := Condensed.elabContext)
  let coreM := metaM.run'
  match ← (coreM.run' coreContext { env := env }).toBaseIO with
  | .error exception =>
--- a/Test/Serial.lean
+++ b/Test/Serial.lean
@ -64,7 +64,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
        | .ok expr => pure expr
        | .error e => return elabFailure e
      return LSpec.check source ((← serializeExpressionSexp expr) = target)
-    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := defaultTermElabMContext)
+    let metaM := (Elab.Term.withLevelNames levels termElabM).run' (ctx := Condensed.elabContext)
    return LSpec.TestSeq.append suites (← runMetaMSeq env metaM))
    LSpec.TestSeq.done

@ -85,7 +85,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
    let testCaseName := target.take 10
    let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
    return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
-  runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
+  runMetaMSeq env $ termElabM.run' (ctx := Condensed.elabContext)

 -- Instance parsing
 def test_instance (env: Environment): IO LSpec.TestSeq :=
--- a/flake.nix
+++ b/flake.nix
@ -63,6 +63,7 @@
      packages = {
        inherit (leanPkgs) lean lean-all;
        inherit (project) sharedLib executable;
+        inherit project leanPkgs;
        default = project.executable;
      };
      checks = {