feat: Simplify printing of function applications

This commit is contained in:
Leni Aniva 2023-10-29 12:50:36 -07:00
parent afed5bbc8d
commit 454a5bc6b9
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 10 additions and 30 deletions

View File

@ -55,26 +55,8 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String :=
let quote := "̈̈\""
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n
private def level_depth: Level → Nat
| .zero => 0
| .succ l => 1 + (level_depth l)
| .max u v | .imax u v => 1 + max (level_depth u) (level_depth v)
| .param _ | .mvar _ => 0
theorem level_depth_max_imax (u v: Level): (level_depth (Level.max u v) = level_depth (Level.imax u v)) := by
constructor
theorem level_max_depth_decrease (u v: Level): (level_depth u < level_depth (Level.max u v)) := by
have h1: level_depth (Level.max u v) = 1 + Nat.max (level_depth u) (level_depth v) := by constructor
rewrite [h1]
simp_arith
conv =>
rhs
apply Nat.max_def
sorry
theorem level_offset_decrease (u v: Level): (level_depth u ≤ level_depth (Level.max u v).getLevelOffset) := sorry
/-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/
def serialize_sort_level_ast (level: Level): String :=
partial def serialize_sort_level_ast (level: Level): String :=
let k := level.getOffset
let u := level.getLevelOffset
let u_str := match u with
@ -98,14 +80,11 @@ def serialize_sort_level_ast (level: Level): String :=
| 0, _ => u_str
| _, .zero => s!"{k}"
| _, _ => s!"(+ {u_str} {k})"
termination_by serialize_sort_level_ast level => level_depth level
decreasing_by
. sorry
/--
Completely serializes an expression tree. Json not used due to compactness
-/
def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
self expr
where
self (e: Expr): String :=
@ -128,10 +107,11 @@ def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
-- The universe level of the const expression is elided since it should be
-- inferrable from surrounding expression
s!"(:c {declName})"
| .app fn arg =>
let fn' := self fn
let arg' := self arg
s!"({fn'} {arg'})"
| .app _ _ =>
let fn' := self e.getAppFn
let args := e.getAppArgs.map self |>.toList
let args := " ".intercalate args
s!"({fn'} {args})"
| .lam binderName binderType body binderInfo =>
let binderName' := of_name binderName
let binderType' := self binderType

View File

@ -45,7 +45,7 @@ def subroutine_runner (steps: List (MainM LSpec.TestSeq)): IO LSpec.TestSeq := d
def test_option_modify : IO LSpec.TestSeq :=
let pp? := Option.some "∀ (n : Nat), n + 1 = Nat.succ n"
let sexp? := Option.some "(: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)))"
let sexp? := Option.some "(: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)))"
let module? := Option.some "Init.Data.Nat.Basic"
let options: Protocol.Options := {}
subroutine_runner [

View File

@ -45,8 +45,8 @@ def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
-- This one contains unhygienic variable names which must be suppressed
("Nat.add", "(:forall _ (:c Nat) (:forall _ (:c Nat) (:c Nat)))"),
-- 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.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.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)"),
-- Handling of higher order types
("Or", "(:forall a (:sort 0) (:forall b (:sort 0) (:sort 0)))"),
("List", "(:forall α (:sort (+ u 1)) (:sort (+ u 1)))")