feat: Simplify printing of names and expressions #25

Merged
aniva merged 5 commits from io/serial into dev 2023-10-29 13:08:06 -07:00
3 changed files with 17 additions and 9 deletions
Showing only changes of commit e2526f11b1 - Show all commits

View File

@ -46,14 +46,14 @@ def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType))) return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
return { binders, target := toString (← Meta.ppExpr body) } return { binders, target := toString (← Meta.ppExpr body) }
private def name_to_ast (name: Name) (sanitize: Bool := true): String := def name_to_ast (name: Name) (sanitize: Bool := true): String :=
if sanitize && name.isInternal then "_" let internal := name.isInaccessibleUserName || name.hasMacroScopes
else name_to_ast_aux name |>.drop 1 if sanitize && internal then "_"
else toString name |> enclose_if_escaped
where where
name_to_ast_aux: Name → String enclose_if_escaped (n: String) :=
| .anonymous => "" let quote := "̈̈\""
| .num n i => s!"{name_to_ast_aux n} {i}" if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
| .str init last => s!"{name_to_ast_aux init} {last}"
private def level_depth: Level → Nat private def level_depth: Level → Nat
| .zero => 0 | .zero => 0

View File

@ -85,7 +85,7 @@ def test_malformed_command : IO LSpec.TestSeq :=
def test_tactic : IO LSpec.TestSeq := def test_tactic : IO LSpec.TestSeq :=
let goal: Protocol.Goal := { let goal: Protocol.Goal := {
target := { pp? := .some "∀ (q : Prop), x q → q x" }, target := { pp? := .some "∀ (q : Prop), x q → q x" },
vars := #[{ name := "_uniq 9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}], vars := #[{ name := "_uniq.9", userName := "x", isInaccessible? := .some false, type? := .some { pp? := .some "Prop" }}],
} }
subroutine_runner [ subroutine_runner [
subroutine_step "goal.start" subroutine_step "goal.start"

View File

@ -12,6 +12,13 @@ deriving instance Repr, DecidableEq for Protocol.BoundExpression
def test_str_to_name: LSpec.TestSeq := 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") 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 := "̈̈\""
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}")
-- Pathological test case
--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 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × Protocol.BoundExpression) := [ let entries: List (String × Protocol.BoundExpression) := [
("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }), ("Nat.add_comm", { binders := #[("n", "Nat"), ("m", "Nat")], target := "n + m = m + n" }),
@ -70,6 +77,7 @@ def suite: IO LSpec.TestSeq := do
return LSpec.group "Serialization" $ return LSpec.group "Serialization" $
(LSpec.group "str_to_name" test_str_to_name) ++ (LSpec.group "str_to_name" test_str_to_name) ++
(LSpec.group "name_to_ast" test_name_to_ast) ++
(LSpec.group "Expression binder" (← test_expr_to_binder env)) ++ (LSpec.group "Expression binder" (← test_expr_to_binder env)) ++
(LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env)) (LSpec.group "Sexp from symbol" (← test_sexp_of_symbol env))