Merge pull request 'feat: Simplify printing of names and expressions' (#25) from io/serial into dev
Reviewed-on: #25
This commit is contained in:
commit
796f0d8336
|
@ -46,64 +46,45 @@ def type_expr_to_bound (expr: Expr): MetaM Protocol.BoundExpression := do
|
|||
return (toString (← fvar.fvarId!.getUserName), toString (← Meta.ppExpr (← fvar.fvarId!.getType)))
|
||||
return { binders, target := toString (← Meta.ppExpr body) }
|
||||
|
||||
private def name_to_ast (name: Lean.Name) (sanitize: Bool := true): String := match name with
|
||||
| .anonymous => ":anon"
|
||||
| .num n i => match sanitize with
|
||||
| false => s!"{toString n} {i}"
|
||||
| true => ":anon"
|
||||
| n@(.str _ _) => toString 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
|
||||
def name_to_ast (name: Name) (sanitize: Bool := true): String :=
|
||||
let internal := name.isInaccessibleUserName || name.hasMacroScopes
|
||||
if sanitize && internal then "_"
|
||||
else toString name |> enclose_if_escaped
|
||||
where
|
||||
enclose_if_escaped (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)` -/
|
||||
def serialize_sort_level_ast (level: Level): String :=
|
||||
partial def serialize_sort_level_ast (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
|
||||
let w := serialize_sort_level_ast w
|
||||
let v := serialize_sort_level_ast v sanitize
|
||||
let w := serialize_sort_level_ast w sanitize
|
||||
s!"(:max {v} {w})"
|
||||
| .imax v w =>
|
||||
let v := serialize_sort_level_ast v
|
||||
let w := serialize_sort_level_ast w
|
||||
let v := serialize_sort_level_ast v sanitize
|
||||
let w := serialize_sort_level_ast w sanitize
|
||||
s!"(:imax {v} {w})"
|
||||
| .param name =>
|
||||
let name := name_to_ast name
|
||||
let name := name_to_ast name sanitize
|
||||
s!"{name}"
|
||||
| .mvar id =>
|
||||
let name := name_to_ast id.name
|
||||
let name := name_to_ast id.name sanitize
|
||||
s!"(:mv {name})"
|
||||
match k, u with
|
||||
| 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 :=
|
||||
|
@ -120,16 +101,17 @@ def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): String :=
|
|||
let name := of_name mvarId.name
|
||||
s!"(:mv {name})"
|
||||
| .sort level =>
|
||||
let level := serialize_sort_level_ast level
|
||||
let level := serialize_sort_level_ast level sanitize
|
||||
s!"(:sort {level})"
|
||||
| .const declName _ =>
|
||||
-- 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
|
||||
|
|
|
@ -1,5 +1,5 @@
|
|||
namespace Pantograph
|
||||
|
||||
def version := "0.2.6"
|
||||
def version := "0.2.7"
|
||||
|
||||
end Pantograph
|
||||
|
|
|
@ -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 [
|
||||
|
@ -85,7 +85,7 @@ def test_malformed_command : IO LSpec.TestSeq :=
|
|||
def test_tactic : IO LSpec.TestSeq :=
|
||||
let goal: Protocol.Goal := {
|
||||
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_step "goal.start"
|
||||
|
|
|
@ -10,7 +10,14 @@ open Lean
|
|||
deriving instance Repr, DecidableEq for Protocol.BoundExpression
|
||||
|
||||
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
|
||||
let entries: List (String × Protocol.BoundExpression) := [
|
||||
|
@ -36,10 +43,10 @@ def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
|
|||
def test_sexp_of_symbol (env: Environment): IO LSpec.TestSeq := do
|
||||
let entries: List (String × String) := [
|
||||
-- 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
|
||||
("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)))")
|
||||
|
@ -70,6 +77,7 @@ def suite: IO LSpec.TestSeq := do
|
|||
|
||||
return LSpec.group "Serialization" $
|
||||
(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 "Sexp from symbol" (← test_sexp_of_symbol env))
|
||||
|
||||
|
|
Loading…
Reference in New Issue