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
2 changed files with 9 additions and 7 deletions
Showing only changes of commit c2d606b9d9 - Show all commits

View File

@ -46,12 +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: Lean.Name) (sanitize: Bool := true): String := match name with private def name_to_ast (name: Name) (sanitize: Bool := true): String :=
| .anonymous => ":anon" if sanitize && name.isInternal then "_"
| .num n i => match sanitize with else name_to_ast_aux name |>.drop 1
| false => s!"{toString n} {i}" where
| true => ":anon" name_to_ast_aux: Name → String
| n@(.str _ _) => toString n | .anonymous => ""
| .num n i => s!"{name_to_ast_aux n} {i}"
| .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

@ -36,7 +36,7 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × String) := [ let entries: List (String × String) := [
-- This one contains unhygienic variable names which must be suppressed -- This one contains unhygienic variable names which must be suppressed
("Nat.add", "(:forall :anon (:c Nat) (:forall :anon (:c Nat) (:c Nat)))"), ("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
-- These ones are normal and easy -- These ones are normal and easy
("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"), ("Nat.add_one", "(:forall n (:c Nat) ((((:c Eq) (:c Nat)) (((((((:c HAdd.hAdd) (:c Nat)) (:c Nat)) (:c Nat)) (((:c instHAdd) (:c Nat)) (:c instAddNat))) 0) ((((:c OfNat.ofNat) (:c Nat)) (:lit 1)) ((:c instOfNatNat) (:lit 1))))) ((:c Nat.succ) 0)))"),
("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"), ("Nat.le_of_succ_le", "(:forall n (:c Nat) (:forall m (:c Nat) (:forall h (((((:c LE.le) (:c Nat)) (:c instLENat)) ((:c Nat.succ) 1)) 0) (((((:c LE.le) (:c Nat)) (:c instLENat)) 2) 1)) :implicit) :implicit)"),