Merge pull request 'feat: Option to collect dependent metavariables' (#69) from serial/goal into dev

Reviewed-on: #69

Pantograph/Environment.lean

@@ -54,18 +54,18 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
     | .none, _ => .none
   -- Information common to all symbols
   let core := {
-    type := ← (serialize_expression options info.type).run',
+    type := ← (serializeExpression options info.type).run',
     isUnsafe := info.isUnsafe,
-    value? := ← value?.mapM (λ v => serialize_expression options v |>.run'),
+    value? := ← value?.mapM (λ v => serializeExpression options v |>.run'),
     publicName? := Lean.privateToUserName? name |>.map (·.toString),
     -- BUG: Warning: getUsedConstants here will not include projections. This is a known bug.
     typeDependency? := if args.dependency?.getD false
-      then .some <| info.type.getUsedConstants.map (λ n => name_to_ast n)
+      then .some <| info.type.getUsedConstants.map (λ n => serializeName n)
       else .none,
     valueDependency? := ← if args.dependency?.getD false
       then info.value?.mapM (λ e => do
         let e ← unfoldAuxLemmas e
-        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => name_to_ast n) )
+        pure $ e.getUsedConstants.filter (!isNameInternal ·) |>.map (λ n => serializeName n) )
       else pure (.none),
     module? := module?
   }
@@ -95,7 +95,7 @@ def inspect (args: Protocol.EnvInspect) (options: @&Protocol.Options): CoreM (Pr
               pure {
                 ctor := rule.ctor.toString,
                 nFields := rule.nfields,
-                rhs := ← (serialize_expression options rule.rhs).run',
+                rhs := ← (serializeExpression options rule.rhs).run',
               })
           k := r.k,
       } }

Pantograph/Library.lean

@@ -144,8 +144,8 @@ def exprEcho (expr: String) (expectedType?: Option String := .none) (options: @&
     try
       let type ← unfoldAuxLemmas (← Lean.Meta.inferType expr)
       return .ok {
-          type := (← serialize_expression options type),
+          type := (← serializeExpression options type),
-          expr := (← serialize_expression options expr)
+          expr := (← serializeExpression options expr)
       }
     catch exception =>
       return .error $ errorI "typing" (← exception.toMessageData.toString)
@@ -204,9 +204,9 @@ def goalPrint (state: GoalState) (options: @&Protocol.Options): Lean.CoreM Proto
     state.restoreMetaM
     return {
       root? := ← state.rootExpr?.mapM (λ expr => do
-        serialize_expression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← unfoldAuxLemmas expr)),
       parent? := ← state.parentExpr?.mapM (λ expr => do
-        serialize_expression options (← unfoldAuxLemmas expr)),
+        serializeExpression options (← unfoldAuxLemmas expr)),
     }
 
 

Pantograph/Protocol.lean

@@ -18,6 +18,7 @@ structure Options where
   printExprPretty: Bool    := true
   -- When enabled, print the raw AST of expressions
   printExprAST: Bool       := false
+  printDependentMVars: Bool := false
   -- When enabled, the types and values of persistent variables in a goal
   -- are not shown unless they are new to the proof step. Reduces overhead.
   -- NOTE: that this assumes the type and assignment of variables can never change.
@@ -41,6 +42,7 @@ structure Expression where
   pp?: Option String             := .none
   -- AST structure
   sexp?: Option String           := .none
+  dependentMVars?: Option (Array String) := .none
   deriving Lean.ToJson
 
 structure Variable where
@@ -182,6 +184,7 @@ structure OptionsSet where
   printJsonPretty?: Option Bool
   printExprPretty?: Option Bool
   printExprAST?: Option Bool
+  printDependentMVars?: Option Bool
   noRepeat?: Option Bool
   printAuxDecls?: Option Bool
   printImplementationDetailHyps?: Option Bool

Pantograph/Serial.lean

@@ -15,7 +15,7 @@ def Lean.Name.isAuxLemma (n : Lean.Name) : Bool := n matches .num (.str _ "_auxL
 namespace Pantograph
 
 /-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. These end in `_auxLemma.nn` where `nn` is a number. -/
-def unfoldAuxLemmas (e : Lean.Expr) : Lean.CoreM Lean.Expr := do
+def unfoldAuxLemmas (e : Expr) : CoreM Expr := do
   Lean.Meta.deltaExpand e Lean.Name.isAuxLemma
 
 --- Input Functions ---
@@ -43,41 +43,41 @@ def elabTerm (syn: Syntax) (expectedType? : Option Expr := .none): Elab.TermElab
 
 --- Output Functions ---
 
-def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
+def typeExprToBound (expr: Expr): MetaM Protocol.BoundExpression := do
   Meta.forallTelescope expr fun arr body => do
     let binders ← arr.mapM fun fvar => do
       return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
     return { binders, target := toString (← Meta.ppExpr body) }
 
-def name_to_ast (name: Name) (sanitize: Bool := true): String :=
+def serializeName (name: Name) (sanitize: Bool := true): String :=
   let internal := name.isInaccessibleUserName || name.hasMacroScopes
   if sanitize && internal then "_"
-  else toString name |> enclose_if_escaped
+  else toString name |> addQuotes
   where
-  enclose_if_escaped (n: String) :=
+  addQuotes (n: String) :=
     let quote := "\""
     if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
 
 /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
-partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
+partial def serializeSortLevel (level: Level) (sanitize: Bool): String :=
   let k := level.getOffset
   let u := level.getLevelOffset
   let u_str := match u with
     | .zero => "0"
     | .succ _ => panic! "getLevelOffset should not return .succ"
     | .max v w =>
-      let v := serialize_sort_level_ast v sanitize
+      let v := serializeSortLevel v sanitize
-      let w := serialize_sort_level_ast w sanitize
+      let w := serializeSortLevel w sanitize
       s!"(:max {v} {w})"
     | .imax v w =>
-      let v := serialize_sort_level_ast v sanitize
+      let v := serializeSortLevel v sanitize
-      let w := serialize_sort_level_ast w sanitize
+      let w := serializeSortLevel w sanitize
       s!"(:imax {v} {w})"
     | .param name =>
-      let name := name_to_ast name sanitize
+      let name := serializeName name sanitize
       s!"{name}"
     | .mvar id =>
-      let name := name_to_ast id.name sanitize
+      let name := serializeName id.name sanitize
       s!"(:mv {name})"
   match k, u with
   | 0, _ => u_str
@@ -89,7 +89,7 @@ partial def serialize_sort_level_ast (level: Level) (sanitize: Bool): String :=
 
 A `_` symbol in the AST indicates automatic deductions not present in the original expression.
 -/
-partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): MetaM String := do
+partial def serializeExpressionSexp (expr: Expr) (sanitize: Bool := true): MetaM String := do
   self expr
   where
   self (e: Expr): MetaM String :=
@@ -100,13 +100,13 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
       -- Lean these are handled using a `#` prefix.
       pure s!"{deBruijnIndex}"
     | .fvar fvarId =>
-      let name := of_name fvarId.name
+      let name := ofName fvarId.name
       pure s!"(:fv {name})"
     | .mvar mvarId =>
-      let name := of_name mvarId.name
+      let name := ofName mvarId.name
       pure s!"(:mv {name})"
     | .sort level =>
-      let level := serialize_sort_level_ast level sanitize
+      let level := serializeSortLevel level sanitize
       pure s!"(:sort {level})"
     | .const declName _ =>
       -- The universe level of the const expression is elided since it should be
@@ -118,20 +118,20 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
       let args := " ".intercalate args
       pure s!"({fn'} {args})"
     | .lam binderName binderType body binderInfo => do
-      let binderName' := of_name binderName
+      let binderName' := ofName binderName
       let binderType' ← self binderType
       let body' ← self body
-      let binderInfo' := binder_info_to_ast binderInfo
+      let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:lambda {binderName'} {binderType'} {body'}{binderInfo'})"
     | .forallE binderName binderType body binderInfo => do
-      let binderName' := of_name binderName
+      let binderName' := ofName binderName
       let binderType' ← self binderType
       let body' ← self body
-      let binderInfo' := binder_info_to_ast binderInfo
+      let binderInfo' := binderInfoSexp binderInfo
       pure s!"(:forall {binderName'} {binderType'} {body'}{binderInfo'})"
     | .letE name type value body _ => do
       -- Dependent boolean flag diacarded
-      let name' := name_to_ast name
+      let name' := serializeName name
       let type' ← self type
       let value' ← self value
       let body' ← self body
@@ -157,27 +157,31 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
       let inner ← self inner
       pure s!"((:c {projectorName}) {autos} {inner})"
   -- Elides all unhygenic names
-  binder_info_to_ast : Lean.BinderInfo → String
+  binderInfoSexp : Lean.BinderInfo → String
     | .default => ""
     | .implicit => " :implicit"
     | .strictImplicit => " :strictImplicit"
     | .instImplicit => " :instImplicit"
-  of_name (name: Name) := name_to_ast name sanitize
+  ofName (name: Name) := serializeName name sanitize
 
-def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
+def serializeExpression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
   let pp?: Option String ← match options.printExprPretty with
     | true => pure $ .some $ toString $ ← Meta.ppExpr e
     | false => pure $ .none
   let sexp?: Option String ← match options.printExprAST with
-    | true => pure $ .some $ ← serialize_expression_ast e
+    | true => pure $ .some $ ← serializeExpressionSexp e
+    | false => pure $ .none
+  let dependentMVars? ← match options.printDependentMVars with
+    | true => pure $ .some $ (← Meta.getMVars e).map (λ mvarId => mvarId.name.toString)
     | false => pure $ .none
   return {
     pp?,
     sexp?
+    dependentMVars?,
   }
 
 /-- Adapted from ppGoal -/
-def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
+def serializeGoal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl)
       : MetaM Protocol.Goal := do
   -- Options for printing; See Meta.ppGoal for details
   let showLetValues  := true
@@ -191,12 +195,12 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
       | .cdecl _ fvarId userName _ _ _ =>
         let userName := userName.simpMacroScopes
         return {
-          name := of_name fvarId.name,
+          name := ofName fvarId.name,
-          userName:= of_name userName.simpMacroScopes,
+          userName:= ofName userName.simpMacroScopes,
         }
       | .ldecl _ fvarId userName _ _ _ _ => do
         return {
-          name := of_name fvarId.name,
+          name := ofName fvarId.name,
           userName := toString userName.simpMacroScopes,
         }
     let ppVar (localDecl : LocalDecl) : MetaM Protocol.Variable := do
@@ -205,24 +209,24 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
         let userName := userName.simpMacroScopes
         let type ← instantiateMVars type
         return {
-          name := of_name fvarId.name,
+          name := ofName fvarId.name,
-          userName:= of_name userName,
+          userName:= ofName userName,
           isInaccessible? := .some userName.isInaccessibleUserName
-          type? := .some (← serialize_expression options type)
+          type? := .some (← serializeExpression options type)
         }
       | .ldecl _ fvarId userName type val _ _ => do
         let userName := userName.simpMacroScopes
         let type ← instantiateMVars type
         let value? ← if showLetValues then
           let val ← instantiateMVars val
-          pure $ .some (← serialize_expression options val)
+          pure $ .some (← serializeExpression options val)
         else
           pure $ .none
         return {
-          name := of_name fvarId.name,
+          name := ofName fvarId.name,
-          userName:= of_name userName,
+          userName:= ofName userName,
           isInaccessible? := .some userName.isInaccessibleUserName
-          type? := .some (← serialize_expression options type)
+          type? := .some (← serializeExpression options type)
           value? := value?
         }
     let vars ← lctx.foldlM (init := []) fun acc (localDecl : LocalDecl) => do
@@ -238,14 +242,14 @@ def serialize_goal (options: @&Protocol.Options) (goal: MVarId) (mvarDecl: Metav
           | false => ppVar localDecl
         return var::acc
     return {
-      name := of_name goal.name,
+      name := ofName goal.name,
-      userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName),
+      userName? := if mvarDecl.userName == .anonymous then .none else .some (ofName mvarDecl.userName),
       isConversion := isLHSGoal? mvarDecl.type |>.isSome,
-      target := (← serialize_expression options (← instantiateMVars mvarDecl.type)),
+      target := (← serializeExpression options (← instantiateMVars mvarDecl.type)),
       vars := vars.reverse.toArray
     }
   where
-  of_name (n: Name) := name_to_ast n (sanitize := false)
+  ofName (n: Name) := serializeName n (sanitize := false)
 
 protected def GoalState.serializeGoals
       (state: GoalState)
@@ -258,12 +262,12 @@ protected def GoalState.serializeGoals
   goals.mapM fun goal => do
     match state.mctx.findDecl? goal with
     | .some mvarDecl =>
-      let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?)
+      let serializedGoal ← serializeGoal options goal mvarDecl (parentDecl? := parentDecl?)
       pure serializedGoal
     | .none => throwError s!"Metavariable does not exist in context {goal.name}"
 
 /-- Print the metavariables in a readable format -/
-protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
+protected def GoalState.diag (goalState: GoalState) (options: Protocol.GoalDiag := {}): MetaM Unit := do
   goalState.restoreMetaM
   let savedState := goalState.savedState
   let goals := savedState.tactic.goals
@@ -298,7 +302,7 @@ protected def GoalState.print (goalState: GoalState) (options: Protocol.GoalDiag
       let type ← if options.instantiate
         then instantiateMVars decl.type
         else pure $ decl.type
-      let type_sexp ← serialize_expression_ast type (sanitize := false)
+      let type_sexp ← serializeExpressionSexp type (sanitize := false)
       IO.println s!"{pref}{mvarId.name}{userNameToString decl.userName}: {← Meta.ppExpr decl.type} {type_sexp}"
       if options.printValue then
         if let Option.some value := (← getMCtx).eAssignment.find? mvarId then

Test/Metavar.lean

@@ -28,7 +28,7 @@ def test_instantiate_mvar: TestM Unit := do
       addTest $ assertUnreachable e
       return ()
   let t ← Lean.Meta.inferType expr
-  addTest $ LSpec.check "typing" ((toString (← serialize_expression_ast t)) =
+  addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) =
     "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))")
   return ()
 
@@ -121,8 +121,12 @@ def test_m_couple_simp: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  addTest $ LSpec.check "apply Nat.le_trans" ((← state1.serializeGoals (options := ← read)).map (·.target.pp?) =
+  let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true })
+  addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) =
     #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"])
+  addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) =
+    #[#["_uniq.38"], #["_uniq.38"], #[]])
+
   let state2 ← match ← state1.tryTactic (goalId := 2) (tactic := "exact 2") with
     | .success state => pure state
     | other => do
@@ -245,8 +249,8 @@ def test_partial_continuation: TestM Unit := do
 
   -- Roundtrip
   --let coupled_goals := coupled_goals.map (λ g =>
-  --  { name := str_to_name $ name_to_ast g.name (sanitize := false)})
+  --  { name := str_to_name $ serializeName g.name (sanitize := false)})
-  let coupled_goals := coupled_goals.map (λ g => name_to_ast g.name (sanitize := false))
+  let coupled_goals := coupled_goals.map (λ g => serializeName g.name (sanitize := false))
   let coupled_goals := coupled_goals.map (λ g => { name := g.toName })
   let state1b ← match state2.resume (goals := coupled_goals) with
     | .error msg => do

Test/Proofs.lean

@@ -229,7 +229,7 @@ def test_or_comm: TestM Unit := do
   addTest $ LSpec.check "(2 parent)" state2.parentExpr?.isSome
   addTest $ LSpec.check "(2 root)" state2.rootExpr?.isNone
 
-  let state2parent ← serialize_expression_ast state2.parentExpr?.get! (sanitize := false)
+  let state2parent ← serializeExpressionSexp state2.parentExpr?.get! (sanitize := false)
   -- This is due to delayed assignment
   addTest $ LSpec.test "(2 parent)" (state2parent ==
     "((:mv _uniq.43) (:fv _uniq.16) ((:c Eq.refl) ((:c Or) (:fv _uniq.10) (:fv _uniq.13)) (:fv _uniq.16)))")
@@ -239,7 +239,7 @@ def test_or_comm: TestM Unit := do
     | other => do
       addTest $ assertUnreachable $ other.toString
       return ()
-  let state3_1parent ← serialize_expression_ast state3_1.parentExpr?.get! (sanitize := false)
+  let state3_1parent ← serializeExpressionSexp state3_1.parentExpr?.get! (sanitize := false)
   addTest $ LSpec.test "(3_1 parent)" (state3_1parent == "((:c Or.inr) (:fv _uniq.13) (:fv _uniq.10) (:mv _uniq.78))")
   addTest $ LSpec.check "· apply Or.inr" (state3_1.goals.length = 1)
   let state4_1 ← match ← state3_1.tryTactic (goalId := 0) (tactic := "assumption") with
@@ -248,7 +248,7 @@ def test_or_comm: TestM Unit := do
       addTest $ assertUnreachable $ other.toString
       return ()
   addTest $ LSpec.check "  assumption" state4_1.goals.isEmpty
-  let state4_1parent ← serialize_expression_ast state4_1.parentExpr?.get! (sanitize := false)
+  let state4_1parent ← serializeExpressionSexp state4_1.parentExpr?.get! (sanitize := false)
   addTest $ LSpec.test "(4_1 parent)" (state4_1parent == "(:fv _uniq.47)")
   addTest $ LSpec.check "(4_1 root)" state4_1.rootExpr?.isNone
   let state3_2 ← match ← state2.tryTactic (goalId := 1) (tactic := "apply Or.inl") with

Test/Serial.lean

@@ -10,13 +10,13 @@ open Pantograph
 
 deriving instance Repr, DecidableEq for Protocol.BoundExpression
 
-def test_name_to_ast: LSpec.TestSeq :=
+def test_serializeName: LSpec.TestSeq :=
   let quote := "\""
   let escape := "\\"
-  LSpec.test "a.b.1" (name_to_ast (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
+  LSpec.test "a.b.1" (serializeName (Name.num (.str (.str .anonymous "a") "b") 1) = "a.b.1") ++
-  LSpec.test "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
+  LSpec.test "seg.«a.b»" (serializeName (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") ++
   -- Pathological test case
-  LSpec.test s!"«̈{escape}{quote}»" (name_to_ast (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
+  LSpec.test s!"«̈{escape}{quote}»" (serializeName (Name.str .anonymous s!"{escape}{quote}") = s!"{quote}«{escape}{quote}»{quote}")
 
 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   let entries: List (Name × Protocol.BoundExpression) := [
@@ -26,7 +26,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
   runCoreMSeq env $ entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol |>.get! |>.type
-    let test := LSpec.check symbol.toString ((← type_expr_to_bound expr) = target)
+    let test := LSpec.check symbol.toString ((← typeExprToBound expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done |>.run'
 
 def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
@@ -43,7 +43,7 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
   runMetaMSeq env $ entries.foldlM (λ suites (symbol, target) => do
     let env ← MonadEnv.getEnv
     let expr := env.find? symbol.toName |>.get! |>.type
-    let test := LSpec.check symbol ((← serialize_expression_ast expr) = target)
+    let test := LSpec.check symbol ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
 
 def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
@@ -61,7 +61,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do
     let expr ← match (← elabTerm s) with
       | .ok expr => pure expr
       | .error e => return elabFailure e
-    let test := LSpec.check source ((← serialize_expression_ast expr) = target)
+    let test := LSpec.check source ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
 
@@ -80,7 +80,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
   let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
     let env ← MonadEnv.getEnv
     let testCaseName := target.take 10
-    let test := LSpec.check   testCaseName ((← serialize_expression_ast expr) = target)
+    let test := LSpec.check   testCaseName ((← serializeExpressionSexp expr) = target)
     return LSpec.TestSeq.append suites test) LSpec.TestSeq.done
   runMetaMSeq env $ termElabM.run' (ctx := defaultTermElabMContext)
 
@@ -95,7 +95,7 @@ def test_instance (env: Environment): IO LSpec.TestSeq :=
 
 def suite (env: Environment): List (String × IO LSpec.TestSeq) :=
   [
-    ("name_to_ast", do pure test_name_to_ast),
+    ("serializeName", do pure test_serializeName),
     ("Expression binder", test_expr_to_binder env),
     ("Sexp from symbol", test_sexp_of_symbol env),
     ("Sexp from elaborated expr", test_sexp_of_elab env),