refactor: emit part structure as a string

src/tests/TestMain.lean

@@ -36,7 +36,7 @@ Tests manual-genre TeX generation. `dir` is a subdirectory specific to a particu
 which is where actual output should go, and which contains the expected output directory.
 `doc` is the document to be rendered.
 -/
-def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.Manual) :
+def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.DocThunk Verso.Genre.Manual) :
     Config →  IO Unit := fun config =>
   let versoConfig : Verso.Genre.Manual.Config := {
     destination := "src/tests/integration" / dir / "output",
@@ -47,7 +47,7 @@ def testTexOutput (dir : System.FilePath) (doc : Verso.Doc.VersoDoc Verso.Genre.
   let runTest : IO Unit  :=
     open Verso Genre Manual in do
     let logError (msg : String) := IO.eprintln msg
-    ReaderT.run (emitTeX logError versoConfig doc.toPart) extension_impls%
+    ReaderT.run (emitTeX logError versoConfig doc.force) extension_impls%
 
   Verso.Integration.runTests {
     testDir := "src/tests/integration" / dir,

src/tests/Tests/Basic.lean

@@ -16,7 +16,7 @@ set_option pp.rawOnError true
 :::::::
 /-- info: Verso.Doc.Part.mk #[Verso.Doc.Inline.text "Nothing"] "Nothing" none #[] #[] -/
 #guard_msgs in
-  #eval noDoc.toPart
+  #eval noDoc.force
 
 
 /- ----- -/
@@ -36,7 +36,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval littleParagraph.toPart
+  #eval littleParagraph.force
 
 
 /- ----- -/
@@ -56,7 +56,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval listOneItem.toPart
+  #eval listOneItem.force
 
 
 /- ----- -/
@@ -83,7 +83,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval sectionAndPara.toPart
+  #eval sectionAndPara.force
 
 
 /- ----- -/
@@ -128,7 +128,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc1.toPart
+  #eval nestedDoc1.force
 
 
 /- ----- -/
@@ -173,7 +173,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc2.toPart
+  #eval nestedDoc2.force
 
 
 /- ----- -/
@@ -223,7 +223,7 @@ info: Verso.Doc.Part.mk
           #[]]]
 -/
 #guard_msgs in
-  #eval nestedDoc3.toPart
+  #eval nestedDoc3.force
 
 
 /- ----- -/
@@ -260,7 +260,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval nestedDoc4.toPart
+  #eval nestedDoc4.force
 
 
 /- ----- -/

src/tests/Tests/GenericCode.lean

@@ -39,7 +39,7 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval code1.toPart
+  #eval code1.force
 /--
 info: Verso.Output.Html.tag
   "section"
@@ -58,7 +58,7 @@ info: Verso.Output.Html.tag
               (Verso.Output.Html.text true "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n")])])
 -/
 #guard_msgs in
-  #eval Doc.Genre.none.toHtml (m:=Id) {logError := fun _ => ()} () () {} {} {} code1.toPart |>.run .empty |>.fst
+  #eval Doc.Genre.none.toHtml (m:=Id) {logError := fun _ => ()} () () {} {} {} code1.force |>.run .empty |>.fst
 
 
 /- ----- -/
@@ -92,4 +92,4 @@ info: Verso.Doc.Part.mk
       #[]]
 -/
 #guard_msgs in
-  #eval code2.toPart
+  #eval code2.force

src/tests/Tests/LeanCode.lean

@@ -70,7 +70,7 @@ info: (some (Verso.Genre.Manual.InlineLean.Inline.lean, [{"seq":
      {"tok": {"kind": {"withType": {"type": "Nat"}}, "content": "3"}}}]}},
  []]))-/
 #guard_msgs in
-#eval match inspect.toPart.content[0]! with
+#eval match inspect.force.content[0]! with
   | .para x => match x[0]! with
     | .other code _ => Option.some (code.name, code.data)
     | _ => .none

src/tests/Tests/Refs.lean

@@ -24,7 +24,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval regularLink.toPart
+  #eval regularLink.force
 
 
 /- ----- -/
@@ -46,7 +46,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refLink.toPart
+  #eval refLink.force
 
 
 /- ----- -/
@@ -68,7 +68,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval noteLink.toPart
+  #eval noteLink.force
 
 
 /- ----- -/
@@ -95,7 +95,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refAndLink.toPart
+  #eval refAndLink.force
 
 #docs (.none) refAndLink2 "Ref/link ordering" :=
 :::::::
@@ -123,13 +123,13 @@ Here's [a link][to here][^note]!
 :::::::
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink2.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink2.force
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink3.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink3.force
 
 /-- info: true -/
-#guard_msgs in #eval refAndLink.toPart == refAndLink4.toPart
+#guard_msgs in #eval refAndLink.force == refAndLink4.force
 
 #docs (.none) refAndLinkRecursion "Ref/link recursion" :=
 :::::::
@@ -162,7 +162,7 @@ info: Verso.Doc.Part.mk
   #[]
 -/
 #guard_msgs in
-  #eval refAndLinkRecursion.toPart
+  #eval refAndLinkRecursion.force
 
 /--
 error: Already defined link [foo] as 'https://example.com'

src/verso-blog/VersoBlog/LiterateLeanPage.lean

@@ -528,7 +528,7 @@ def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPage
       | _ => p
     else finished
 
-  let ty ← ``(VersoDoc $genre)
+  let ty ← ``(DocThunk $genre)
   let doc ← Command.runTermElabM fun _ => finished.toVersoDoc genre ctx docState partState
   elabCommand <| ← `(def $x : $ty := $doc)
 

src/verso-blog/VersoBlog/LiterateModuleDocs.lean

@@ -78,7 +78,7 @@ def elabFromModuleDocs (x : Ident) (path : StrLit) (mod : Ident) (title : StrLit
     let title ← Meta.mkArrayLit (.app (mkConst ``Verso.Doc.Inline) g) title.toList
     withOptions (Compiler.LCNF.compiler.extract_closed.set · false) do
       addAndCompile <| .defnDecl {
-        name, levelParams := [], type := .app (mkConst ``Verso.Doc.VersoDoc) g,
+        name, levelParams := [], type := .app (mkConst ``Verso.Doc.DocThunk) g,
         value := ← Meta.mkAppM ``modToPage! #[
           ← Meta.mkAppM ``VersoLiterate.loadJsonString! #[mkConst jsonName, mkStrLit s!"JSON for {x.getId}"],
           title,

src/verso-literate/VersoLiterate/Exported.lean

@@ -247,7 +247,7 @@ private partial def mdBlock : MD4Lean.Block → Except String (Block g)
   | .html .. => throw "Literal HTML in Markdown not supported"
   | .hr => throw "Thematic break (horizontal rule) in Markdown not supported"
 
-partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : Except String (VersoDoc g) := do
+partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : Except String (DocThunk g) := do
   let mut stack : Array (Part g) := #[]
   let mut p : Part g := {title, titleString, metadata := none, content := #[], subParts := #[]}
 
@@ -305,7 +305,7 @@ partial def modToPage [LoadLiterate g] (mod : LitMod) (title : Array (Inline g))
     let p' := stack.back
     stack := stack.pop
     p := pushPart p' p
-  return VersoDoc.mk (fun _ => p) "{}"
+  return DocThunk.value p
 where
   docstringBlock (doc : LitVersoDocString) : Array (Block g) :=
     let parts := doc.subsections.map loadPart

src/verso-literate/VersoLiterate/Module.lean

@@ -30,7 +30,7 @@ def load (jsonFile : System.FilePath) : IO LitMod := do
   | .error e => throw <| .userError e
   | .ok v => pure v
 
-def modToPage! [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : VersoDoc g :=
+def modToPage! [LoadLiterate g] (mod : LitMod) (title : Array (Inline g)) (titleString : String) : DocThunk g :=
   match modToPage mod title titleString with
   | .error e => panic! s!"Couldn't load {titleString}: {e}"
   | .ok v => v

src/verso-manual/VersoManual/Literate.lean

@@ -101,7 +101,7 @@ def getModuleWithDocs (path : StrLit) (mod : Ident) (title : StrLit) : PartElabM
     let title ← Meta.mkArrayLit (.app (mkConst ``Verso.Doc.Inline) g) title.toList
     withOptions (Compiler.LCNF.compiler.extract_closed.set · false) do
       addAndCompile <| .defnDecl {
-        name, levelParams := [], type := .app (mkConst ``Verso.Doc.VersoDoc) g,
+        name, levelParams := [], type := .app (mkConst ``Verso.Doc.DocThunk) g,
         value := ← Meta.mkAppM ``modToPage! #[
           ← Meta.mkAppM ``VersoLiterate.loadJsonString! #[mkConst jsonName, mkStrLit s!"JSON for {mod.getId}"],
           title,

src/verso/Verso.lean

@@ -7,6 +7,7 @@ module
 -- This module serves as the root of the `Verso` library.
 -- Import modules here that should be built as part of the library.
 public import Verso.Code
+public import Verso.Deserialize
 public import Verso.Doc
 public import Verso.Doc.ArgParse
 public import Verso.Doc.Concrete

src/verso/Verso/Deserialize.lean

@@ -0,0 +1,126 @@
+/-
+Copyright (c) 2023-2024 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Rob Simmons
+-/
+module
+public import Verso.Doc
+public import SubVerso.Highlighting
+import Verso.Serialize
+
+set_option doc.verso true
+set_option pp.rawOnError true
+
+namespace Verso.Doc
+open Lean
+
+/--
+Deserializing a partially-serialized document syntax is done with access to a structure that fills
+in the parts of the document structure that weren't serialized.
+-/
+public structure DeserializeAux (genre : Genre) : Type where
+  inlines : Array (Inline genre)
+  blocks : Array (Block genre)
+  partMetadata : Array genre.PartMetadata
+  /-- Sorted by {name}`Name.quickLt` -/
+  docs : Array (Name × Part genre)
+deriving Inhabited
+
+
+/--
+Transform a previously-serialized {name (full := Elab.FinishedPart)}`FinishedPart` into a
+{name}`Part`.
+-/
+public partial def Part.deserialize : Json → ReaderM (DeserializeAux genre) (Part genre)
+  | name@(.str _) => do
+    let .ok id := FromJson.fromJson? name
+      | panic! "Failed to deserialize as id `{name}`"
+    let .some (_, part) := (← read).docs.binSearch (id, default) (fun (a, _) (b, _) => Name.quickLt a b)
+      | panic! "Failed to find id `{id}`"
+    return part
+  | .obj o => do
+    let aux ← read
+    let titleArr := match o.get! "title" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"ill-formed JSON part serialization (title) {e}"
+    let title := titleArr.map (match ·.getNat? with
+      | .ok n => match aux.inlines[n]? with
+        | .some t => t
+        | .none => panic! s!"out of bound inline: {n} vs {aux.inlines.size}"
+      | .error e => panic! s!"Ill-formed JSON part serialization (title) {e}")
+    let titleString := match o.get! "titleString" |>.getStr? with
+      | .ok str => str
+      | .error e => panic! panic! s!"Ill-formed JSON part serialization (titleString) {e}"
+    let metadata := match o.get! "metadata" with
+      | .null => .none
+      | .arr #[.num (n : Nat)] =>
+        match (aux.partMetadata[n]?) with
+          | .some s => .some s
+          | .none => panic! s!"Ill-formed JSON part serialization (metadata) {n}"
+      | json => panic! s!"Ill-formed JSON part serialization (metadata) {json}"
+    let contentArr := match o.get! "content" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"Ill-formed JSON part serialization (content) {e}"
+    let content := contentArr.map (match ·.getNat? with
+      | .ok n => match aux.blocks[n]? with
+        | .some t => t
+        | .none => panic! s!"out of bound block: {n} vs {aux.blocks.size}"
+      | .error e => panic! s!"Ill-formed JSON part serialization (content) {e}")
+    let subPartsArr := match o.get! "subParts" |>.getArr? with
+      | .ok arr => arr
+      | .error e => panic! s!"Ill-formed JSON part serialization (subParts) {e}"
+    let subParts ← subPartsArr.mapM deserialize
+    return Part.mk title titleString metadata content subParts
+  | json => panic s!"Ill-formed JSON part serialization {json}"
+
+public structure DocReconstruction where
+  highlightDeduplication : SubVerso.Highlighting.Export
+
+/--
+The result type of values created by Verso's {lit}`#doc` and {lit}`#docs` commands. A value of type
+{lean}`DocThunk` represents a partially-serialized value of type {lean}`Part` that can be turned
+into a value by invoking the `DocThunk.force` method. The actual structure of a {lean}`DocThunk`
+should not be relied on.
+-/
+public inductive DocThunk (genre : Genre) where
+  | serialized
+      (aux : DocReconstruction → DeserializeAux genre)
+      (doc : String)
+      (docReconstructionData : String := "{}")
+      (replacementMetadata? : Option (Option genre.PartMetadata) := .none)
+  | value (part : Part genre)
+
+instance : Inhabited (DocThunk genre) where
+  default := DocThunk.value default
+
+/--
+Replace the top-level metadata in a {name}`DocThunk` without forcing the thunk.
+-/
+public def DocThunk.withMetadata (metadata? : Option genre.PartMetadata) : DocThunk genre → DocThunk genre
+  | .serialized aux doc docReconstStr _replacementMetadata? =>
+    .serialized aux doc docReconstStr (.some metadata?)
+  | .value part =>
+    .value { part with metadata := metadata? }
+
+/--
+A {lean}`DocThunk` represents a potentially-not-fully-evaluated {lean}`Part`. Calling
+{lean}`DocThunk.force` forces evaluation of the {lean}`DocThunk` to a {lean}`Part`.
+-/
+public def DocThunk.force: DocThunk genre → Part genre
+  | .serialized auxFn docStr highlight replacementMetadata? =>
+    match (Json.parse highlight, Json.parse docStr) with
+    | (.error e, _) => panic! s!"Failed to parse DocThunk's Export data as JSON: {e}"
+    | (_, .error e) => panic! s!"Failed to parse doc data as JSON: {e}"
+    | (.ok reconJson, .ok docJson) =>
+      if let .ok highlightJson := reconJson.getObjVal? "highlight" then
+        match SubVerso.Highlighting.Export.fromJson? highlightJson with
+        | .error e => panic! s!"Failed to deserialize Export data from parsed JSON: {e}"
+        | .ok table =>
+          let aux := auxFn ⟨table⟩
+          let part := Id.run <| ReaderT.run (Part.deserialize docJson) aux
+          match replacementMetadata? with
+          | .none => part
+          | .some replacementMetadata => { part with metadata := replacementMetadata }
+      else
+        Id.run <| ReaderT.run (Part.deserialize docJson) (auxFn ⟨{}⟩)
+  | .value part => part