aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Minor updates to serialization #26

Merged
aniva merged 2 commits from io/serial into dev 2023-10-30 14:47:42 -07:00
Conversation 0 Commits 2 Files Changed 6 +5 -4
2 changed files with 5 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit 8dd994d1ca - Show all commits

2
Pantograph/Serial.lean
View File

@ -52,7 +52,7 @@ def name_to_ast (name: Name) (sanitize: Bool := true): String :=
else toString name |> enclose_if_escaped else toString name |> enclose_if_escaped
where where
enclose_if_escaped (n: String) := enclose_if_escaped (n: String) :=
let quote := "̈̈\"" let quote := "\""
if n.contains Lean.idBeginEscape then s!"{quote}{n}{quote}" else n 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)` -/ /-- serialize a sort level. Expression is optimized to be compact e.g. `(+ u 2)` -/

7
Test/Serial.lean
View File

@ -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") 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 := 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 "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 -- 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 def test_expr_to_binder (env: Environment): IO LSpec.TestSeq := do
let entries: List (String × Protocol.BoundExpression) := [ let entries: List (String × Protocol.BoundExpression) := [