Merge pull request 'feat: Condensed interface' (#85) from serial/expr into dev

Reviewed-on: #85
2024-08-15 22:41:58 -07:00 · 2024-08-15 22:41:58 -07:00 · 56100a30af
parent 9b1dd0ffda e943a4b065
commit 56100a30af
13 changed files with 241 additions and 124 deletions
--- a/Pantograph/Condensed.lean
+++ b/Pantograph/Condensed.lean
@ -0,0 +1,96 @@
+/- structures for FFI based interface -/
+import Lean
+import Pantograph.Goal
+import Pantograph.Expr
+import Pantograph.Protocol
+
+open Lean
+
+namespace Pantograph
+namespace Condensed
+
+-- Mirrors Lean's LocalDecl
+structure LocalDecl where
+  -- Default value is for testing
+  fvarId: FVarId := { name := .anonymous }
+  userName: Name
+
+  -- Normalized expression
+  type : Expr
+  value? : Option Expr := .none
+
+structure Goal where
+  mvarId: MVarId := { name := .anonymous }
+  userName: Name := .anonymous
+  context: Array LocalDecl
+  target: Expr
+
+@[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
+
+@[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
@ -33,6 +33,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
@ -53,14 +54,23 @@ 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 :=
  state.savedState.term.meta.core.env

+@[export pantograph_goal_state_meta_context_of_goal]
+protected def GoalState.metaContextOfGoal (state: GoalState) (mvarId: MVarId): Option Meta.Context := do
+  let mvarDecl ← state.mctx.findDecl? mvarId
+  return { lctx := mvarDecl.lctx, localInstances := mvarDecl.localInstances }
+@[export pantograph_goal_state_meta_state]
+protected def GoalState.metaState (state: GoalState): Meta.State :=
+  state.savedState.term.meta.meta
+
 protected def GoalState.withContext (state: GoalState) (mvarId: MVarId) (m: MetaM α): MetaM α := do
-  let metaM := mvarId.withContext m
-  metaM.run' (← read) state.savedState.term.meta.meta
+  mvarId.withContext m |>.run' (← read) state.metaState

 protected def GoalState.withParentContext (state: GoalState) (m: MetaM α): MetaM α := do
  state.withContext state.parentMVar?.get! m
@ -77,6 +87,7 @@ private def GoalState.restoreTacticM (state: GoalState) (goal: MVarId): Elab.Tac
  state.savedState.restore
  Elab.Tactic.setGoals [goal]

+
 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
@ -100,6 +111,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)
@ -128,6 +140,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)
@ -138,12 +151,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
@ -163,13 +178,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):
-          Elab.TermElabM TacticResult := do
+/-- Executes a `TacticM` monads on this `GoalState`, collecting the errors as necessary -/
+protected def GoalState.executeTactic (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.executeTactic
  try
    let (_, newGoals) ← tacticM { elaborator := .anonymous } |>.run { goals := [goal] }
    if (← getThe Core.State).messages.hasErrors then
@ -189,7 +205,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
@ -199,68 +215,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.executeTactic 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.executeTactic goalId $ Tactic.evalAssign expr

 -- Specialized Tactics

@ -520,7 +487,7 @@ protected def GoalState.tryMotivatedApply (state: GoalState) (goalId: Nat) (recu
    (fileName := filename) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.motivatedApply recursor)
+  state.executeTactic goalId (tacticM := Tactic.motivatedApply recursor)
 protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: String):
      Elab.TermElabM TacticResult := do
  state.restoreElabM
@ -531,6 +498,6 @@ protected def GoalState.tryNoConfuse (state: GoalState) (goalId: Nat) (eq: Strin
    (fileName := filename) with
    | .ok syn => pure syn
    | .error error => return .parseError error
-  state.execute goalId (tacticM := Tactic.noConfuse recursor)
+  state.executeTactic goalId (tacticM := Tactic.noConfuse recursor)

 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 :=
@ -204,20 +186,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
@ -4,10 +4,10 @@ This replicates the behaviour of `Scope`s in `Lean/Elab/Command.lean` without
 using `Scope`s.
 -/
 import Lean
+import Pantograph.Condensed
 import Pantograph.Expr
-
-import Pantograph.Protocol
 import Pantograph.Goal
+import Pantograph.Protocol

 open 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,6 +198,7 @@ def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.
    dependentMVars?,
  }

+
 /-- Adapted from ppGoal -/
 def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
      : MetaM Protocol.Goal := do
@ -214,7 +212,6 @@ def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metava
    let ppVarNameOnly (localDecl: LocalDecl): MetaM Protocol.Variable := do
      match localDecl with
      | .cdecl _ fvarId userName _ _ _ =>
-        let userName := userName.simpMacroScopes
        return {
          name := ofName fvarId.name,
          userName:= ofName userName.simpMacroScopes,
@ -289,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
@ -308,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)
@ -348,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,4 +1,5 @@

+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
@ -8,6 +8,17 @@ open Lean

 namespace Pantograph

+deriving instance Repr for Expr
+-- Use strict equality check for expressions
+--instance : BEq Expr := ⟨Expr.equal⟩
+instance (priority := 80) (x y : Expr) : LSpec.Testable (x.equal y) :=
+  if h : Expr.equal x y then
+    .isTrue h
+  else
+    .isFalse h $ s!"Expected to be equalaaa: '{x.dbgToString}' and '{y.dbgToString}'"
+
+def uniq (n: Nat): Name := .num (.str .anonymous "_uniq") n
+
 -- Auxiliary functions
 namespace Protocol
 def Goal.devolatilizeVars (goal: Goal): Goal :=
@ -62,7 +73,7 @@ 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 := Pantograph.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 = {