From d87217c6bb1112cf0fb35b1ec77e0e227dfaffdf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Oct 2023 14:44:06 -0700 Subject: [PATCH 1/2] feat: Print metavariable name in goal --- Pantograph/Protocol.lean | 5 +++-- Pantograph/Serial.lean | 7 ++++--- Test/Common.lean | 1 + Test/Integration.lean | 1 + Test/Proofs.lean | 16 +++++++++------- 5 files changed, 18 insertions(+), 12 deletions(-) diff --git a/Pantograph/Protocol.lean b/Pantograph/Protocol.lean index e379782..fd790bb 100644 --- a/Pantograph/Protocol.lean +++ b/Pantograph/Protocol.lean @@ -54,8 +54,9 @@ structure Variable where value?: Option Expression := .none deriving Lean.ToJson structure Goal where - /-- String case id -/ - caseName?: Option String := .none + name: String := "" + /-- Name of the metavariable -/ + userName?: Option String := .none /-- Is the goal in conversion mode -/ isConversion: Bool := false /-- target expression type -/ diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 615d9b9..a46c2c7 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -168,7 +168,7 @@ def serialize_expression (options: Protocol.Options) (e: Expr): MetaM Protocol.E } /-- Adapted from ppGoal -/ -def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDecl?: Option MetavarDecl) +def serialize_goal (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 @@ -229,7 +229,8 @@ def serialize_goal (options: Protocol.Options) (mvarDecl: MetavarDecl) (parentDe | false => ppVar localDecl return var::acc return { - caseName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), + name := of_name goal.name, + userName? := if mvarDecl.userName == .anonymous then .none else .some (of_name mvarDecl.userName), isConversion := isLHSGoal? mvarDecl.type |>.isSome, target := (← serialize_expression options (← instantiateMVars mvarDecl.type)), vars := vars.reverse.toArray @@ -246,7 +247,7 @@ protected def GoalState.serializeGoals (state: GoalState) (parent: Option GoalSt goals.mapM fun goal => do match state.mctx.findDecl? goal with | .some mvarDecl => - let serializedGoal ← serialize_goal options mvarDecl (parentDecl? := parentDecl?) + let serializedGoal ← serialize_goal options goal mvarDecl (parentDecl? := parentDecl?) pure serializedGoal | .none => throwError s!"Metavariable does not exist in context {goal.name}" diff --git a/Test/Common.lean b/Test/Common.lean index 3e52932..f74e6a2 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -7,6 +7,7 @@ namespace Protocol def Goal.devolatilize (goal: Goal): Goal := { goal with + name := "", vars := goal.vars.map removeInternalAux, } where removeInternalAux (v: Variable): Variable := diff --git a/Test/Integration.lean b/Test/Integration.lean index 6400cca..0420a29 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -84,6 +84,7 @@ def test_malformed_command : IO LSpec.TestSeq := ] def test_tactic : IO LSpec.TestSeq := let goal: Protocol.Goal := { + name := "_uniq.10", target := { pp? := .some "∀ (q : Prop), x ∨ q → q ∨ x" }, vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], } diff --git a/Test/Proofs.lean b/Test/Proofs.lean index a726627..c08ecb2 100644 --- a/Test/Proofs.lean +++ b/Test/Proofs.lean @@ -66,9 +66,9 @@ def startProof (start: Start): TestM (Option GoalState) := do def assertUnreachable (message: String): LSpec.TestSeq := LSpec.check message false -def buildGoal (nameType: List (String × String)) (target: String) (caseName?: Option String := .none): Protocol.Goal := +def buildGoal (nameType: List (String × String)) (target: String) (userName?: Option String := .none): Protocol.Goal := { - caseName?, + userName?, target := { pp? := .some target}, vars := (nameType.map fun x => ({ userName := x.fst, @@ -293,13 +293,13 @@ def proof_or_comm: TestM Unit := do return () where typeProp: Protocol.Expression := { pp? := .some "Prop" } - branchGoal (caseName name: String): Protocol.Goal := { - caseName? := .some caseName, + branchGoal (caseName varName: String): Protocol.Goal := { + userName? := .some caseName, target := { pp? := .some "q ∨ p" }, vars := #[ { userName := "p", type? := .some typeProp, isInaccessible? := .some false }, { userName := "q", type? := .some typeProp, isInaccessible? := .some false }, - { userName := "h✝", type? := .some { pp? := .some name }, isInaccessible? := .some true } + { userName := "h✝", type? := .some { pp? := .some varName }, isInaccessible? := .some true } ] } @@ -352,9 +352,11 @@ def proof_proposition_generation: TestM Unit := do return () addTest $ LSpec.check "apply PSigma.mk" ((← state1.serializeGoals (options := ← read)).map (·.devolatilize) = #[ - buildGoal [] "?fst" (caseName? := .some "snd"), - buildGoal [] "Prop" (caseName? := .some "fst") + buildGoal [] "?fst" (userName? := .some "snd"), + buildGoal [] "Prop" (userName? := .some "fst") ]) + if let #[goal1, goal2] := ← state1.serializeGoals (options := { (← read) with printExprAST := true }) then + addTest $ LSpec.test "(1 reference)" (goal1.target.sexp? = .some s!"(:mv {goal2.name})") addTest $ LSpec.test "(1 root)" state1.rootExpr?.isNone let state2 ← match ← state1.tryAssign (goalId := 0) (expr := "λ (x: Nat) => _") with From 8dd994d1ca91238ff845bb6abe4a93292e54ad89 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Mon, 30 Oct 2023 14:45:43 -0700 Subject: [PATCH 2/2] bug: Fix quote escape problem --- Pantograph/Serial.lean | 2 +- Test/Serial.lean | 7 ++++--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index a46c2c7..c89fc7f 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -52,7 +52,7 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String := else toString name |> enclose_if_escaped where enclose_if_escaped (n: String) := - let quote := "̈̈\"" + 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)` -/ diff --git a/Test/Serial.lean b/Test/Serial.lean index f1b0a9d..dfa3890 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -13,11 +13,12 @@ def test_str_to_name: LSpec.TestSeq := LSpec.test "Symbol parsing" (Name.str (.str (.str .anonymous "Lean") "Meta") "run" = Pantograph.str_to_name "Lean.Meta.run") def test_name_to_ast: LSpec.TestSeq := - let quote := "̈̈\"" + 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 "seg.«a.b»" (name_to_ast (Name.str (.str .anonymous "seg") "a.b") = s!"{quote}seg.«a.b»{quote}") + LSpec.test "seg.«a.b»" (name_to_ast (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}»" (name_to_ast (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 (String × Protocol.BoundExpression) := [