From 5d0a80548fc1d82fcfebe61bae6136c804011315 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Wed, 13 Dec 2023 12:24:47 +0100 Subject: [PATCH] feat: super-basic support for manuals --- Main.lean | 5 +- UsersGuide.lean | 8 + UsersGuide/Basic.Lean | 11 + lakefile.lean | 14 + src/leanblog/LeanDoc/Genre/Blog/Basic.lean | 2 +- src/leanblog/LeanDoc/Genre/Blog/Generate.lean | 8 +- src/leanblog/LeanDoc/Genre/Blog/Site.lean | 8 +- src/leanblog/LeanDoc/Genre/Blog/Template.lean | 4 +- src/leanblog/LeanDoc/Genre/Blog/Theme.lean | 8 +- src/leandoc/LeanDoc/Doc.lean | 40 +-- src/leandoc/LeanDoc/Doc/Concrete.lean | 47 ++- src/leandoc/LeanDoc/Doc/Elab.lean | 25 +- src/leandoc/LeanDoc/Doc/Elab/Monad.lean | 104 ++++--- src/leandoc/LeanDoc/Doc/Html.lean | 29 +- src/leandoc/LeanDoc/Doc/TeX.lean | 96 +++++++ src/leandoc/LeanDoc/Examples.lean | 271 ++++++++---------- src/leandoc/LeanDoc/Output/TeX.lean | 102 +++++++ src/manual/LeanDoc/Genre/Manual.lean | 69 +++++ src/manual/LeanDoc/Genre/Manual/TeX.lean | 17 ++ 19 files changed, 565 insertions(+), 303 deletions(-) create mode 100644 UsersGuide.lean create mode 100644 UsersGuide/Basic.Lean create mode 100644 src/leandoc/LeanDoc/Doc/TeX.lean create mode 100644 src/leandoc/LeanDoc/Output/TeX.lean create mode 100644 src/manual/LeanDoc/Genre/Manual.lean create mode 100644 src/manual/LeanDoc/Genre/Manual/TeX.lean diff --git a/Main.lean b/Main.lean index eef68ef..3e971bb 100644 --- a/Main.lean +++ b/Main.lean @@ -10,6 +10,9 @@ import LeanDoc.Output.Html import LeanDoc.Doc.Concrete import LeanDoc.Doc.Lsp +import LeanDoc.Genre.Blog +import LeanDoc.Genre.Manual + open LeanDoc Doc Output Html Concrete ToHtml Elab Monad open Lean Elab Term @@ -23,7 +26,7 @@ def vanish : RoleExpander def rev : RoleExpander | _args, stxs => .reverse <$> stxs.mapM elabInline -def html [Monad m] (doc : Doc .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc +def html [Monad m] (doc : Part .none) : m Html := Genre.none.toHtml {logError := fun _ => pure ()} () () doc def main : IO Unit := do IO.println <| Html.asString <| Html.embody <| ← html <| #doc (.none) "My wonderful document" => diff --git a/UsersGuide.lean b/UsersGuide.lean new file mode 100644 index 0000000..08e8999 --- /dev/null +++ b/UsersGuide.lean @@ -0,0 +1,8 @@ +import LeanDoc.Genre.Manual + +import UsersGuide.Basic + + +open LeanDoc.Genre.Manual + +def main := manualMain (%doc UsersGuide.Basic) diff --git a/UsersGuide/Basic.Lean b/UsersGuide/Basic.Lean new file mode 100644 index 0000000..2539c7f --- /dev/null +++ b/UsersGuide/Basic.Lean @@ -0,0 +1,11 @@ +import LeanDoc.Genre.Manual + +open LeanDoc.Genre + +#doc (Manual) "Documentation in Lean" => + +Documentation can take many forms: + + * References + * Tutorials + * Etc diff --git a/lakefile.lean b/lakefile.lean index c4e18fa..b0418a9 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -15,6 +15,10 @@ lean_lib LeanBlog where srcDir := "src/leanblog" roots := #[`LeanDoc.Genre.Blog] +lean_lib LeanManual where + srcDir := "src/manual" + roots := #[`LeanDoc.Genre.Manual] + @[default_target] lean_exe «leandoc» where root := `Main @@ -22,3 +26,13 @@ lean_exe «leandoc» where -- `runFrontend`) at the expense of increased binary size on Linux. -- Remove this line if you do not need such functionality. supportInterpreter := true + +lean_lib UsersGuide where + +@[default_target] +lean_exe usersguide where + root := `UsersGuide + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true diff --git a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean index 2fc5c8f..2a1220c 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Basic.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Basic.lean @@ -97,7 +97,7 @@ namespace Blog structure Post where date : Date authors : List String - content : Doc Blog + content : Part Blog draft : Bool deriving TypeName, Inhabited diff --git a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean index 5cd8437..d8a758d 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Generate.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Generate.lean @@ -89,7 +89,7 @@ def inPage (here : Page) (act : GenerateM α) : GenerateM α := withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [here.name]}) act def inPost (here : Post) (act : GenerateM α) : GenerateM α := - withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.content.titleString ]}) act + withReader (fun c => {c with ctxt.path := c.ctxt.path ++ [c.ctxt.config.postName here.date here.content.titleString ]}) act @@ -125,7 +125,7 @@ mutual if post.draft && !(← showDrafts) then continue inPost post <| do let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.postTemplate, id⟩ - let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content.content + let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart post.content ensureDir (← currentDir) IO.println s!"Generating post {← currentDir}" IO.FS.withFile ((← currentDir).join "index.html") .write fun h => do @@ -142,7 +142,7 @@ mutual some <$> ps.mapM fun p => theme.archiveEntryTemplate.render (.ofList [("post", ⟨.mk p, #[]⟩)]) else pure none - let pageParams : Template.Params ← forPart txt.content + let pageParams : Template.Params ← forPart txt let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩ let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| match postList with @@ -164,7 +164,7 @@ def Site.generate (theme : Theme) (site : Site): GenerateM Unit := do let root ← currentDir ensureDir root let ⟨baseTemplate, modParams⟩ := theme.adHocTemplates (Array.mk (← currentPath)) |>.getD ⟨theme.pageTemplate, id⟩ - let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage.content + let output ← Template.renderMany [baseTemplate, theme.primaryTemplate] <| modParams <| ← forPart site.frontPage let filename := root.join "index.html" IO.FS.withFile filename .write fun h => do h.putStrLn "" diff --git a/src/leanblog/LeanDoc/Genre/Blog/Site.lean b/src/leanblog/LeanDoc/Genre/Blog/Site.lean index 0a8ae08..de79a78 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Site.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Site.lean @@ -10,7 +10,7 @@ inductive Dir α where deriving Inhabited defmethod Post.traverse1 (post : Post) : Blog.TraverseM Post := - withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.content.titleString]}) <| do + withReader (fun ctxt => {ctxt with path := ctxt.path ++ [ctxt.config.postName post.date post.content.titleString]}) <| do let content' ← Blog.traverse post.content pure {post with content := content'} @@ -20,7 +20,7 @@ def Dir.traverse1 (dir : Dir α) (sub : α → Blog.TraverseM α) : Blog.Travers | .blog posts => .blog <$> posts.mapM Post.traverse1 inductive Page where - | page (name : String) (id : Lean.Name) (text : Doc Blog) (contents : Dir Page) + | page (name : String) (id : Lean.Name) (text : Part Blog) (contents : Dir Page) | static (name : String) (files : System.FilePath) instance : Inhabited Page where @@ -41,7 +41,7 @@ partial def Page.traverse1 (nav : Page) : Blog.TraverseM Page := do | .static .. => pure nav structure Site where - frontPage : Doc Blog + frontPage : Part Blog contents : Dir Page def Site.traverse1 (site : Site) : Blog.TraverseM Site := do @@ -69,7 +69,7 @@ class MonadPath (m : Type → Type u) where export MonadPath (currentPath) def postName [Monad m] [MonadConfig m] (post : Post) : m String := do - pure <| (← currentConfig).postName post.date post.content.content.titleString + pure <| (← currentConfig).postName post.date post.content.titleString def relative [Monad m] [MonadConfig m] [MonadPath m] (target : List String) : m (List String) := do return relativize (← currentPath) target diff --git a/src/leanblog/LeanDoc/Genre/Blog/Template.lean b/src/leanblog/LeanDoc/Genre/Blog/Template.lean index 80ef7b5..6c40d4b 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Template.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Template.lean @@ -93,7 +93,7 @@ partial instance : GenreHtml Blog IO where pure {{s!"Can't find target {x}"}} | some tgt => let addr := s!"{String.join ((← relative tgt.path).intersperse "/")}#{tgt.htmlId}" - go <| .link contents (.url addr) + go <| .link contents addr | .pageref x, contents => do match (← state).pageIds.find? x with | none => @@ -101,7 +101,7 @@ partial instance : GenreHtml Blog IO where pure {{s!"Can't find target {x}"}} | some path => let addr := String.join ((← relative path).intersperse "/") - go <| .link contents (.url addr) + go <| .link contents addr | .htmlSpan classes, contents => do pure {{ {{← contents.mapM go}} }} | .blob html, _ => pure html diff --git a/src/leanblog/LeanDoc/Genre/Blog/Theme.lean b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean index 5abd674..1f250b3 100644 --- a/src/leanblog/LeanDoc/Genre/Blog/Theme.lean +++ b/src/leanblog/LeanDoc/Genre/Blog/Theme.lean @@ -31,12 +31,12 @@ def dirLinks : Dir Page → TemplateM (Array Html) | .pages subs => subs.filterMapM fun | .page name _id txt .. => - pure <| some {{
  • {{txt.content.titleString}}
    • }} + pure <| some {{
  • {{txt.titleString}}
    • }} | .static .. => pure none | .blog subs => subs.mapM fun s => do - let url ← mkLink [(← currentConfig).postName s.date s.content.content.titleString] - return {{
  • {{s.content.content.titleString}}
    • }} + let url ← mkLink [(← currentConfig).postName s.date s.content.titleString] + return {{
  • {{s.content.titleString}}
    • }} where mkLink dest := do let dest' ← relative dest @@ -91,7 +91,7 @@ def archiveEntry : Template := do | Date.mk y m d => {{ s!"{y}-{m}-{d}" }} }} " — " - {{post.content.content.titleString}} + {{post.content.titleString}} }}] diff --git a/src/leandoc/LeanDoc/Doc.lean b/src/leandoc/LeanDoc/Doc.lean index 59f5f46..b89acf1 100644 --- a/src/leandoc/LeanDoc/Doc.lean +++ b/src/leandoc/LeanDoc/Doc.lean @@ -42,20 +42,15 @@ instance : Repr Genre.none.PartMetadata where reprPrec e _ := nomatch e -inductive LinkDest where - | url (address : String) - | ref (name : String) -deriving Repr - inductive Inline (genre : Genre) : Type where | text (string : String) | emph (content : Array (Inline genre)) | bold (content : Array (Inline genre)) | code (string : String) | linebreak (string : String) - | link (content : Array (Inline genre)) (dest : LinkDest) - | footnote (name : String) - | image (alt : String) (dest : LinkDest) + | link (content : Array (Inline genre)) (url : String) + | footnote (name : String) (content : Array (Inline genre)) + | image (alt : String) (url : String) | concat (content : Array (Inline genre)) | other (container : genre.Inline) (content : Array (Inline genre)) @@ -71,10 +66,6 @@ private def reprPair (x : α → Nat → Format) (y : β → Nat → Format) (v private def reprCtor (c : Name) (args : List Format) : Format := .nest 2 <| .group (.joinSep (.text s!"{c}" :: args) .line) -private def reprHash [BEq α] [Hashable α] (k : α → Nat → Format) (v : β → Nat → Format) (h : Lean.HashMap α β) : Format := - reprCtor ``Lean.HashMap.ofList [reprList (fun x _ => reprPair k v x) h.toList] - - partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : Std.Format := open Repr Std.Format in let rec go i p := @@ -89,7 +80,7 @@ partial def Inline.reprPrec [Repr g.Inline] (inline : Inline g) (prec : Nat) : S reprArray go content, reprArg dest ] - | .footnote name => reprCtor ``Inline.footnote [reprArg name] + | .footnote name content => reprCtor ``Inline.footnote [reprArg name, reprArray go content] | .image content dest => reprCtor ``Inline.image [ reprArg content, reprArg dest @@ -187,20 +178,6 @@ partial def Part.reprPrec [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] ( instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] : Repr (Part g) := ⟨Part.reprPrec⟩ -structure Doc (genre : Genre) where - content : Part genre - linkRefs : Lean.HashMap String String - footnotes : Lean.HashMap String (Array (Inline genre)) -deriving Inhabited - -instance [Repr k] [Repr v] [BEq k] [Hashable k] : Repr (Lean.HashMap k v) where - reprPrec h _n := reprCtor ``Lean.HashMap.ofList [reprArg h.toList] - -def Doc.reprPrec [Repr (Inline g)] [Repr (Part g)] (doc : Doc g) (prec : Nat) : Std.Format := - reprCtor ``Doc.mk [reprArg doc.content, reprArg doc.linkRefs, reprArg doc.footnotes] - -instance [Repr g.Inline] [Repr g.Block] [Repr g.PartMetadata] [Repr (Part g)] : Repr (Doc g) := ⟨Doc.reprPrec⟩ - class Traverse (g : Genre) (m : outParam (Type → Type)) where part [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Part g → m Unit block [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] : Block g → m Unit @@ -213,8 +190,8 @@ class Traverse (g : Genre) (m : outParam (Type → Type)) where partial def Genre.traverse (g : Genre) [Traverse g m] [Monad m] [MonadReader g.TraverseContext m] [MonadState g.TraverseState m] - (top : Doc g) : m (Doc g) := - doc top + (top : Part g) : m (Part g) := + part top where inline (i : Doc.Inline g) : m (Doc.Inline g) := do @@ -223,7 +200,7 @@ where | .emph content => .emph <$> content.mapM inline | .bold content => .bold <$> content.mapM inline | .link content ref => (.link · ref) <$> content.mapM inline - | .footnote name => pure <| .footnote name + | .footnote name content => .footnote name <$> content.mapM inline | .image alt ref => pure <| .image alt ref | .concat content => .concat <$> content.mapM inline | .other container content => do @@ -257,6 +234,3 @@ where p := p' let .mk title titleString meta content subParts := p pure <| .mk (← title.mapM inline) titleString meta (← content.mapM block) (← subParts.mapM part) - - doc (d : Doc g) : m (Doc g) := do - pure <| .mk (← part d.content) d.linkRefs (← d.footnotes.foldM (fun fs k v => do pure <| fs.insert k (← v.mapM inline)) .empty) diff --git a/src/leandoc/LeanDoc/Doc/Concrete.lean b/src/leandoc/LeanDoc/Doc/Concrete.lean index 5a041b5..a5813fb 100644 --- a/src/leandoc/LeanDoc/Doc/Concrete.lean +++ b/src/leandoc/LeanDoc/Doc/Concrete.lean @@ -9,6 +9,7 @@ import Lean import LeanDoc.Doc import LeanDoc.Doc.Elab import LeanDoc.Doc.Elab.Monad +import LeanDoc.Doc.Lsp import LeanDoc.Parser import LeanDoc.SyntaxUtils @@ -64,7 +65,7 @@ info: #[Inline.text "Hello, ", Inline.emph #[Inline.bold #[Inline.text "emph"]]] #check inlines!"Hello, _*emph*_" def document : Parser where - fn := rawFn <| LeanDoc.Parser.document (blockContext := {maxDirective := some 6}) + fn := rawFn <| atomicFn <| LeanDoc.Parser.document (blockContext := {maxDirective := some 6}) @[combinator_parenthesizer document] def document.parenthesizer := PrettyPrinter.Parenthesizer.visitToken @[combinator_formatter document] def document.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous @@ -74,6 +75,14 @@ partial def findGenre [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv | `(($e)) => findGenre e | _ => pure () +def saveRefs [Monad m] [MonadInfoTree m] (st : DocElabM.State) (st' : PartElabM.State) : m Unit := do + for r in internalRefs st'.linkDefs st.linkRefs do + for stx in r.syntax do + pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} + for r in internalRefs st'.footnoteDefs st.footnoteRefs do + for stx in r.syntax do + pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} + elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:document ":::::::" : command => open Lean Elab Command PartElabM DocElabM in do findGenre genre let endTok := @@ -96,15 +105,9 @@ elab "#docs" "(" genre:term ")" n:ident title:inlineStr ":=" ":::::::" text:docu pure () let finished := st'.partContext.toPartFrame.close endPos pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC} - for r in internalRefs st'.linkDefs st.linkRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - for r in internalRefs st'.footnoteDefs st.footnoteRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - elabCommand (← `(def $n : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)})) + saveRefs st st' + + elabCommand (← `(def $n : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs))) elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term => open Lean Elab Term PartElabM DocElabM in do @@ -122,16 +125,8 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : term pure () let finished := st'.partContext.toPartFrame.close endPos pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC} - for r in internalRefs st'.linkDefs st.linkRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - for r in internalRefs st'.footnoteDefs st.footnoteRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - - let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - elabTerm (← `(({content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs) : Doc $genre}))) none + saveRefs st st' + elabTerm (← `( ($(← finished.toSyntax st'.linkDefs st'.footnoteDefs) : Part $genre))) none macro "%doc" moduleName:ident : term => @@ -161,14 +156,6 @@ elab "#doc" "(" genre:term ")" title:inlineStr "=>" text:document eof:eoi : comm pure () let finished := st'.partContext.toPartFrame.close endPos pushInfoLeaf <| .ofCustomInfo {stx := (← getRef) , value := Dynamic.mk finished.toTOC} + saveRefs st st' let docName ← mkIdentFrom title <$> currentDocName - let linkRefs : List (String × String) := st'.linkDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - let footnoteRefs : List (String × Array (TSyntax `term)) := st'.footnoteDefs.toList.map (fun (k, v) => (k, DocDef.val v)) - for r in internalRefs st'.linkDefs st.linkRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - for r in internalRefs st'.footnoteDefs st.footnoteRefs do - for stx in r.syntax do - pushInfoLeaf <| .ofCustomInfo {stx := stx , value := Dynamic.mk r} - - elabCommand (← `(def $docName : Doc $genre := {content := $(← finished.toSyntax), linkRefs := HashMap.ofList $(quote linkRefs), footnotes := HashMap.ofList $(quote footnoteRefs)})) + elabCommand (← `(def $docName : Part $genre := $(← finished.toSyntax st'.linkDefs st'.footnoteDefs))) diff --git a/src/leandoc/LeanDoc/Doc/Elab.lean b/src/leandoc/LeanDoc/Doc/Elab.lean index 78f722e..f6a0222 100644 --- a/src/leandoc/LeanDoc/Doc/Elab.lean +++ b/src/leandoc/LeanDoc/Doc/Elab.lean @@ -113,34 +113,37 @@ def _root_.LeanDoc.Syntax.role.expand : InlineExpander @[inline_expander LeanDoc.Syntax.link] def _root_.LeanDoc.Syntax.link.expand : InlineExpander | `(inline| link[ $txt* ] $dest:link_target) => do - let destStx ← + let url : TSyntax `term ← match dest with | `(link_target| ( $url )) => - ``(Inline.link #[$[$(← txt.mapM elabInline)],*] (LinkDest.url $url)) + pure (↑ url) | `(link_target| [ $ref ]) => do - addLinkRef ref -- Round-trip through quote to get rid of source locations, preventing unwanted IDE info - ``(Inline.link #[$[$(← txt.mapM elabInline)],*] (LinkDest.ref $(quote ref.getString))) - | _ => withRef dest throwUnsupportedSyntax + addLinkRef ref + | _ => throwErrorAt dest "Couldn't parse link destination" + ``(Inline.link #[$[$(← txt.mapM elabInline)],*] $url) | _ => throwUnsupportedSyntax @[inline_expander LeanDoc.Syntax.footnote] def _root_.LeanDoc.Syntax.link.footnote : InlineExpander | `(inline| [^ $name:str ]) => do - addFootnoteRef name - ``(Inline.footnote $(quote name.getString)) + ``(Inline.footnote $name $(← addFootnoteRef name)) | _ => throwUnsupportedSyntax @[inline_expander LeanDoc.Syntax.image] def _root_.LeanDoc.Syntax.image.expand : InlineExpander | `(inline| image[ $alt:str* ] $dest:link_target) => do - let destStx ← + let altText := String.join (alt.map (·.getString) |>.toList) + let url : TSyntax `term ← match dest with | `(link_target| ( $url )) => - let altText := String.join (alt.map (·.getString) |>.toList) - ``(Inline.image $(quote altText) (LinkDest.url $url)) - | _ => withRef dest throwUnsupportedSyntax + pure (↑ url) + | `(link_target| [ $ref ]) => do + -- Round-trip through quote to get rid of source locations, preventing unwanted IDE info + addLinkRef ref + | _ => throwErrorAt dest "Couldn't parse link destination" + ``(Inline.image $(quote altText) $url) | _ => throwUnsupportedSyntax diff --git a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean index 2accb8f..8708c54 100644 --- a/src/leandoc/LeanDoc/Doc/Elab/Monad.lean +++ b/src/leandoc/LeanDoc/Doc/Elab/Monad.lean @@ -55,6 +55,38 @@ def headerStxToString (env : Environment) : Syntax → String | headerStx => dbg_trace "didn't understand {headerStx} for string" "" + +/-- References that must be local to the current blob of concrete document syntax -/ +structure DocDef (α : Type) where + defSite : TSyntax `str + val : α + +structure DocUses where + useSites : Array Syntax := {} + +def DocUses.add (uses : DocUses) (loc : Syntax) : DocUses := {uses with useSites := uses.useSites.push loc} + +structure DocElabM.State where + linkRefs : HashMap String DocUses := {} + footnoteRefs : HashMap String DocUses := {} + +/-- Custom info tree data to save footnote and reflink cross-references -/ +structure DocRefInfo where + defSite : Option Syntax + useSites : Array Syntax +deriving TypeName, Repr + +def DocRefInfo.syntax (dri : DocRefInfo) : Array Syntax := + (dri.defSite.map (#[·])|>.getD #[]) ++ dri.useSites + +def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocUses) : Array DocRefInfo := Id.run do + let keys : HashSet String := defs.fold (fun soFar k _ => HashSet.insert soFar k) <| refs.fold (fun soFar k _ => soFar.insert k) {} + let mut refInfo := #[] + for k in keys do + refInfo := refInfo.push ⟨defs.find? k |>.map (·.defSite), refs.find? k |>.map (·.useSites) |>.getD #[]⟩ + refInfo + + inductive TOC where | mk (title : String) (titleSyntax : Syntax) (endPos : String.Pos) (children : Array TOC) deriving Repr, TypeName, Inhabited @@ -99,10 +131,34 @@ inductive FinishedPart where | mk (titleSyntax : Syntax) (expandedTitle : Array (TSyntax `term)) (titlePreview : String) (blocks : Array (TSyntax `term)) (subParts : Array FinishedPart) (endPos : String.Pos) deriving Repr, BEq -partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m] : FinishedPart → m (TSyntax `term) +private def linkRefName (ref : TSyntax `str) : TSyntax `ident := + let str := ref.getString + let name : Name := .num (.str (.str .anonymous "link reference") str) 1 + ⟨.ident .none str.toSubstring name []⟩ + +private def footnoteRefName (ref : TSyntax `str) : TSyntax `ident := + let str := ref.getString + let name : Name := .num (.str (.str .anonymous "footnote reference") str) 1 + ⟨.ident .none str.toSubstring name []⟩ + +open Lean.Parser.Term in +partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m] + (linkDefs : HashMap String (DocDef String)) (footnoteDefs : HashMap String (DocDef (Array (TSyntax `term)))) + : FinishedPart → m (TSyntax `term) | .mk _titleStx titleInlines titleString blocks subParts _endPos => do - let subStx ← subParts.mapM toSyntax - ``(Part.mk #[$[$titleInlines],*] $(quote titleString) none #[$[$blocks],*] #[$[$subStx],*]) + let subStx ← subParts.mapM (toSyntax {} {}) + let body ← ``(Part.mk #[$[$titleInlines],*] $(quote titleString) none #[$[$blocks],*] #[$[$subStx],*]) + bindFootnotes footnoteDefs (← bindLinks linkDefs body) +where + bindLinks (linkDefs : HashMap String (DocDef String)) (body : TSyntax `term) : m (TSyntax `term) := do + let defs ← linkDefs.toArray.mapM fun (_, defn) => + `(letIdDecl| $(linkRefName defn.defSite) := $(quote defn.val)) + defs.foldlM (fun stx letDecl => `(let $letDecl:letIdDecl; $stx)) body + bindFootnotes (linkDefs : HashMap String (DocDef (Array (TSyntax `term)))) (body : TSyntax `term) : m (TSyntax `term) := do + let defs ← linkDefs.toArray.mapM fun (_, defn) => + `(letIdDecl| $(footnoteRefName defn.defSite) := #[$[$defn.val],*]) + defs.foldlM (fun stx letDecl => `(let $letDecl:letIdDecl; $stx)) body + partial def FinishedPart.toTOC : FinishedPart → TOC | .mk titleStx _titleInlines titleString _blocks subParts endPos => @@ -136,40 +192,11 @@ def PartContext.close (ctxt : PartContext) (endPos : String.Pos) : Option PartCo def PartContext.push (ctxt : PartContext) (fr : PartFrame) : PartContext := ⟨fr, ctxt.parents.push ctxt.toPartFrame⟩ -/-- References that must be local to the current blob of concrete document syntax -/ -structure DocDef (α : Type) where - defSite : Syntax - val : α - -structure DocUses where - useSites : Array Syntax := {} - -def DocUses.add (uses : DocUses) (loc : Syntax) : DocUses := {uses with useSites := uses.useSites.push loc} - structure PartElabM.State where partContext : PartContext linkDefs : HashMap String (DocDef String) := {} footnoteDefs : HashMap String (DocDef (Array (TSyntax `term))) := {} -structure DocElabM.State where - linkRefs : HashMap String DocUses := {} - footnoteRefs : HashMap String DocUses := {} - -/-- Custom info tree data to save footnote and reflink cross-references -/ -structure DocRefInfo where - defSite : Option Syntax - useSites : Array Syntax -deriving TypeName, Repr - -def DocRefInfo.syntax (dri : DocRefInfo) : Array Syntax := - (dri.defSite.map (#[·])|>.getD #[]) ++ dri.useSites - -def internalRefs (defs : HashMap String (DocDef α)) (refs : HashMap String DocUses) : Array DocRefInfo := Id.run do - let keys : HashSet String := defs.fold (fun soFar k _ => HashSet.insert soFar k) <| refs.fold (fun soFar k _ => soFar.insert k) {} - let mut refInfo := #[] - for k in keys do - refInfo := refInfo.push ⟨defs.find? k |>.map (·.defSite), refs.find? k |>.map (·.useSites) |>.getD #[]⟩ - refInfo def PartElabM.State.init (title : Syntax) (expandedTitle : Option (String × Array (TSyntax `term)) := none) : PartElabM.State where partContext := {titleSyntax := title, expandedTitle, blocks := #[], priorParts := #[], parents := #[]} @@ -257,29 +284,34 @@ def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Uni | some ⟨_, url'⟩ => throwErrorAt refName "Already defined as '{url'}'" -def DocElabM.addLinkRef (refName : TSyntax `str) : DocElabM Unit := do +def DocElabM.addLinkRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := do let strName := refName.getString match (← getThe State).linkRefs.find? strName with | none => modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨#[refName]⟩} + pure <| linkRefName refName | some ⟨uses⟩ => modifyThe State fun st => {st with linkRefs := st.linkRefs.insert strName ⟨uses.push refName⟩} + pure <| linkRefName refName + def PartElabM.addFootnoteDef (refName : TSyntax `str) (content : Array (TSyntax `term)) : PartElabM Unit := do let strName := refName.getString match (← getThe State).footnoteDefs.find? strName with | none => modifyThe State fun st => {st with footnoteDefs := st.footnoteDefs.insert strName ⟨refName, content⟩} - | some ⟨_, url'⟩ => - throwErrorAt refName "Already defined as '{url'}'" + | some ⟨_, content⟩ => + throwErrorAt refName "Already defined as '{content}'" -def DocElabM.addFootnoteRef (refName : TSyntax `str) : DocElabM Unit := do +def DocElabM.addFootnoteRef (refName : TSyntax `str) : DocElabM (TSyntax `term) := do let strName := refName.getString match (← getThe State).footnoteRefs.find? strName with | none => modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨#[refName]⟩} + pure <| footnoteRefName refName | some ⟨uses⟩ => modifyThe State fun st => {st with footnoteRefs := st.footnoteRefs.insert strName ⟨uses.push refName⟩} + pure <| footnoteRefName refName def PartElabM.push (fr : PartFrame) : PartElabM Unit := modifyThe State fun st => {st with partContext := st.partContext.push fr} diff --git a/src/leandoc/LeanDoc/Doc/Html.lean b/src/leandoc/LeanDoc/Doc/Html.lean index 11478e2..a734f7c 100644 --- a/src/leandoc/LeanDoc/Doc/Html.lean +++ b/src/leandoc/LeanDoc/Doc/Html.lean @@ -19,8 +19,6 @@ structure Options (g : Genre) (m : Type → Type) where /-- The level of the top-level headers -/ headerLevel : Nat := 1 logError : String → m Unit - refLinks : Lean.HashMap String String := {} - footnotes : Lean.HashMap String (Array (Inline g)) := {} abbrev HtmlT (genre : Genre) (m : Type → Type) : Type → Type := ReaderT (Options genre m × genre.TraverseContext × genre.TraverseState) m @@ -70,30 +68,14 @@ class GenreHtml (genre : Genre) (m : Type → Type) where section open ToHtml -defmethod LinkDest.str [Monad m] : LinkDest → HtmlT g m String - | .url addr => pure addr - | .ref name => do - let ({refLinks := refs, ..}, _, _) ← read - if let some url := refs.find? name then - pure url - else - logError s!"Unknown reference '{name}'" - pure "" - partial def Inline.toHtml [Monad m] [GenreHtml g m] : Inline g → HtmlT g m Html | .text str => pure <| .text str | .link content dest => do - pure {{ {{← content.mapM toHtml}} }} + pure {{ {{← content.mapM toHtml}} }} | .image alt dest => do - pure {{ {{alt}}/ }} - | .footnote name => do - let ({footnotes := footnotes, ..}, _, _) ← read - if let some txt := footnotes.find? name then - pure {{
    "["{{name}}"]"{{← txt.mapM toHtml}}
    }} - else - let message := s!"Unknown footnote '{name}' - options were {footnotes.toList.map (·.fst)}" - logError message - pure {{{{message}}}} + pure {{ {{alt}}/ }} + | .footnote name content => do + pure {{
    "["{{name}}"]"{{← content.mapM toHtml}}
    }} | .linebreak _str => pure .empty | .emph content => do pure {{ {{← content.mapM toHtml }} }} @@ -153,9 +135,6 @@ partial def Part.toHtml [Monad m] [GenreHtml g m] (p : Part g) : HtmlT g m Html instance [Monad m] [GenreHtml g m] : ToHtml g m (Part g) where toHtml := Part.toHtml -instance [Monad m] [GenreHtml g m] : ToHtml g m (Doc g) where - toHtml (d : Doc g) := withReader (fun o => {o with fst.refLinks := d.linkRefs, fst.footnotes := d.footnotes}) (Part.toHtml d.content) - instance : GenreHtml .none m where part _ m := nomatch m block _ x := nomatch x diff --git a/src/leandoc/LeanDoc/Doc/TeX.lean b/src/leandoc/LeanDoc/Doc/TeX.lean new file mode 100644 index 0000000..f628ab7 --- /dev/null +++ b/src/leandoc/LeanDoc/Doc/TeX.lean @@ -0,0 +1,96 @@ +import LeanDoc.Doc +import LeanDoc.Method +import LeanDoc.Output.TeX + +open LeanDoc.Doc + +namespace LeanDoc.Doc.TeX + +open LeanDoc.Output TeX + +structure Options (g : Genre) (m : Type → Type) where + headerLevels : Array String := #["chapter", "section", "subsection", "subsubsection", "paragraph"] + /-- The level of the top-level headers -/ + headerLevel : Option (Fin headerLevels.size) + logError : String → m Unit + +abbrev TeXT (genre : Genre) (m : Type → Type) : Type → Type := + ReaderT (Options genre m × genre.TraverseContext × genre.TraverseState) m + +instance [Monad m] [Inhabited α] : Inhabited (TeXT g m α) := ⟨pure default⟩ + +def options [Monad m] : TeXT g m (Options g m) := do + pure (← read).fst + +def logError [Monad m] (message : String) : TeXT g m Unit := do + (← options).logError message + +def header [Monad m] (name : TeX) : TeXT g m TeX := do + let opts ← options + let some i := opts.headerLevel + | logError "No more header nesting available"; return \TeX{\textbf{\Lean{name}}} + let header := opts.headerLevels[i] + pure <| .raw (s!"\\{header}" ++ "{") ++ name ++ .raw "}" + +def inHeader [Monad m] (act : TeXT g m α) : TeXT g m α := + withReader (fun (opts, st, st') => (bumpHeader opts, st, st')) act +where + bumpHeader opts := + if let some i := opts.headerLevel then + if h : i.val + 1 < opts.headerLevels.size then + {opts with headerLevel := some ⟨i.val + 1, h⟩} + else {opts with headerLevel := none} + else opts + +class GenreTeX (genre : Genre) (m : Type → Type) where + part (partTeX : Part genre → TeXT genre m TeX) (metadata : genre.PartMetadata) (contents : Part genre) : TeXT genre m TeX + block (blockTeX : Block genre → TeXT genre m TeX) (container : genre.Block) (contents : Array (Block genre)) : TeXT genre m TeX + inline (inlineTeX : Inline genre → TeXT genre m TeX) (container : genre.Inline) (contents : Array (Inline genre)) : TeXT genre m TeX + +partial defmethod Inline.toTeX [Monad m] [GenreTeX g m] : Inline g → TeXT g m TeX + | .text str => pure <| .text str + | .link content dest => do + pure \TeX{\hyperlink{\Lean{.raw (toString (repr dest)) }}{\Lean{← content.mapM Inline.toTeX}}} -- TODO link destinations + | .image _alt dest => do + pure \TeX{\includegraphics{\Lean{.raw (toString (repr dest))}}} -- TODO link destinations + | .footnote _name txt => do + pure \TeX{\footnote{\Lean{← txt.mapM Inline.toTeX}}} + | .linebreak str => pure <| .text str + | .emph content => do + pure \TeX{\emph{\Lean{← content.mapM toTeX}}} + | .bold content => do + pure \TeX{\textbf{\Lean{← content.mapM toTeX}}} + | .code str => do + pure \TeX{s!"\\verb|{str}|"} --- TODO choose delimiter automatically + | .concat inlines => inlines.mapM toTeX + | .other container content => GenreTeX.inline Inline.toTeX container content + +partial defmethod Block.toTeX [Monad m] [GenreTeX g m] : Block g → TeXT g m TeX + | .para xs => do + pure <| (← xs.mapM Inline.toTeX) ++ TeX.raw "\n\n" + | .blockquote bs => do + pure \TeX{\begin{quotation} \Lean{← bs.mapM Block.toTeX} \end{quotation}} + | .ul items => do + pure \TeX{\begin{itemize} \Lean{← items.mapM fun li => do pure \TeX{\item " " \Lean{← li.contents.mapM Block.toTeX}}} \end{itemize} } + | .ol start items => do -- TODO start numbering here + pure \TeX{\begin{enumerate} \Lean{← items.mapM fun li => do pure \TeX{\item " " \Lean{← li.contents.mapM Block.toTeX}}} \end{enumerate} } + | .dl items => do + pure \TeX{\begin{description} \Lean{← items.mapM fun li => do pure \TeX{\item[\Lean{← li.term.mapM Inline.toTeX}] " " \Lean{← li.desc.mapM Block.toTeX}}} \end{description} } + | .code _ _ _ content => do + pure \TeX{\begin{verbatim} \Lean{.raw content} \end{verbatim}} + | .concat items => TeX.seq <$> items.mapM Block.toTeX + | .other container content => GenreTeX.block Block.toTeX container content + + +partial defmethod Part.toTeX [Monad m] [GenreTeX g m] (p : Part g) : TeXT g m TeX := + match p.metadata with + | .none => do + pure \TeX{ + \Lean{← header (← p.title.mapM Inline.toTeX)} + "\n\n" + \Lean{← p.content.mapM Block.toTeX} + "\n\n" + \Lean{← inHeader <| p.subParts.mapM Part.toTeX } + } + | some m => + GenreTeX.part Part.toTeX m p.withoutMetadata diff --git a/src/leandoc/LeanDoc/Examples.lean b/src/leandoc/LeanDoc/Examples.lean index 75f2cc1..0e781cd 100644 --- a/src/leandoc/LeanDoc/Examples.lean +++ b/src/leandoc/LeanDoc/Examples.lean @@ -16,12 +16,7 @@ set_option pp.rawOnError true ::::::: ::::::: -/-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk #[LeanDoc.Doc.Inline.text "Nothing"] "Nothing" none #[] #[] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] --/ +/-- info: LeanDoc.Doc.Part.mk #[LeanDoc.Doc.Inline.text "Nothing"] "Nothing" none #[] #[] -/ #guard_msgs in #eval noDoc @@ -35,15 +30,12 @@ Hello, I'm a paragraph. Yes I am! /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "My title here"] - "My title here" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Hello, I'm a paragraph. Yes I am!"]] - #[] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "My title here"] + "My title here" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Hello, I'm a paragraph. Yes I am!"]] + #[] -/ #guard_msgs in #eval a @@ -56,17 +48,13 @@ info: LeanDoc.Doc.Doc.mk ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "My title here"] - "My title here" - none - #[LeanDoc.Doc.Block.ul - #[{ indent := 0, - contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Just a list with one item"]] }]] - #[] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "My title here"] + "My title here" + none + #[LeanDoc.Doc.Block.ul + #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Just a list with one item"]] }]] + #[] -/ #guard_msgs in #eval a' @@ -83,20 +71,17 @@ a paragraph ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "My title here"] - "My title here" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]] - #[]] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "My title here"] + "My title here" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]] + #[]] -/ #guard_msgs in #eval b @@ -121,33 +106,30 @@ More text: ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "My title here"] - "My title here" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1.1"] - "Section 1.1" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "More text:"], - LeanDoc.Doc.Block.ul - #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "and a list"]] }, - { indent := 0, - contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "with two"], - LeanDoc.Doc.Block.ul - #[{ indent := 1, - contents := #[LeanDoc.Doc.Block.para - #[LeanDoc.Doc.Inline.text "and nested"]] }]] }]] - #[]]] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "My title here"] + "My title here" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "a paragraph"]] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1.1"] + "Section 1.1" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "More text:"], + LeanDoc.Doc.Block.ul + #[{ indent := 0, contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "and a list"]] }, + { indent := 0, + contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "with two"], + LeanDoc.Doc.Block.ul + #[{ indent := 1, + contents := #[LeanDoc.Doc.Block.para + #[LeanDoc.Doc.Inline.text "and nested"]] }]] }]] + #[]]] -/ #guard_msgs in #eval c @@ -167,26 +149,23 @@ Also, 2 > 3. ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "More writing"] - "More writing" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's a quote;"], - LeanDoc.Doc.Block.blockquote - #[(LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "I like quotes"]), - (LeanDoc.Doc.Block.ul - #[{ indent := 2, - contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also with lists in them"]] }])], - LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also, 2 > 3."]] - #[]] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "More writing"] + "More writing" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's a quote;"], + LeanDoc.Doc.Block.blockquote + #[(LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "I like quotes"]), + (LeanDoc.Doc.Block.ul + #[{ indent := 2, + contents := #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also with lists in them"]] }])], + LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Also, 2 > 3."]] + #[]] -/ #guard_msgs in #eval d @@ -206,21 +185,18 @@ Here's some code ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "More writing"] - "More writing" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's some code"], - LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"] - #[]] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "More writing"] + "More writing" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para #[LeanDoc.Doc.Inline.text "Here's some code"], + LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"] + #[]] -/ #guard_msgs in #eval e @@ -240,22 +216,19 @@ Here's some `code`! ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "More code writing"] - "More code writing" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para - #[LeanDoc.Doc.Inline.text "Here's some ", LeanDoc.Doc.Inline.code "code", LeanDoc.Doc.Inline.text "!"], - LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"] - #[]] - Lean.HashMap.ofList [] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "More code writing"] + "More code writing" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para + #[LeanDoc.Doc.Inline.text "Here's some ", LeanDoc.Doc.Inline.code "code", LeanDoc.Doc.Inline.text "!"], + LeanDoc.Doc.Block.code none #[] 0 "(define (zero f z) z)\n(define (succ n) (lambda (f x) (f (n f z))))\n"] + #[]] -/ #guard_msgs in #eval f @@ -272,23 +245,20 @@ Here's [a link][to here]! ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Ref link before"] - "Ref link before" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para - #[LeanDoc.Doc.Inline.text "Here's ", - LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] (LeanDoc.Doc.LinkDest.ref "to here"), - LeanDoc.Doc.Inline.text "!"]] - #[]] - Lean.HashMap.ofList [("to here", "http://example.com")] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Ref link before"] + "Ref link before" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para + #[LeanDoc.Doc.Inline.text "Here's ", + LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] "http://example.com", + LeanDoc.Doc.Inline.text "!"]] + #[]] -/ #guard_msgs in #eval g @@ -305,23 +275,20 @@ Here's [a link][to here]! ::::::: /-- -info: LeanDoc.Doc.Doc.mk - LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Ref link after"] - "Ref link after" - none - #[] - #[LeanDoc.Doc.Part.mk - #[LeanDoc.Doc.Inline.text "Section 1"] - "Section 1" - none - #[LeanDoc.Doc.Block.para - #[LeanDoc.Doc.Inline.text "Here's ", - LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] (LeanDoc.Doc.LinkDest.ref "to here"), - LeanDoc.Doc.Inline.text "!"]] - #[]] - Lean.HashMap.ofList [("to here", "http://example.com")] - Lean.HashMap.ofList [] +info: LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Ref link after"] + "Ref link after" + none + #[] + #[LeanDoc.Doc.Part.mk + #[LeanDoc.Doc.Inline.text "Section 1"] + "Section 1" + none + #[LeanDoc.Doc.Block.para + #[LeanDoc.Doc.Inline.text "Here's ", + LeanDoc.Doc.Inline.link #[(LeanDoc.Doc.Inline.text "a link")] "http://example.com", + LeanDoc.Doc.Inline.text "!"]] + #[]] -/ #guard_msgs in #eval g' diff --git a/src/leandoc/LeanDoc/Output/TeX.lean b/src/leandoc/LeanDoc/Output/TeX.lean new file mode 100644 index 0000000..f4a6fdf --- /dev/null +++ b/src/leandoc/LeanDoc/Output/TeX.lean @@ -0,0 +1,102 @@ +import Lean +import Std.Tactic.GuardMsgs + +open Lean + +namespace LeanDoc.Output + +inductive TeX where + | text (string : String) + | raw (string : String) + | command (name : String) (optArgs : Array TeX) (args : Array TeX) + | environment (name : String) (optArgs : Array TeX) (args : Array TeX) (content : Array TeX) + | seq (contents : Array TeX) +deriving Repr, Inhabited + +instance : Coe (Array TeX) TeX where + coe := .seq + +instance : Append TeX where + append + | .seq xs, .seq ys => .seq (xs ++ ys) + | .seq xs, y => .seq (xs.push y) + | x, .seq ys => .seq (#[x] ++ ys) + | x, y => .seq #[x, y] + +namespace TeX + +partial def asString (doc : TeX) : String := + match doc with + | .text str => escape str + | .raw str => str + | .command name opt req => + s!"\\{name}" ++ opt.foldl (· ++ "[" ++ ·.asString ++ "]") "" ++ req.foldl (· ++ "{" ++ ·.asString ++ "}") "" + | .environment name opt req content => + "\\begin{" ++ name ++ "}" ++ opt.foldl (· ++ "[" ++ ·.asString ++ "]") "" ++ req.foldl (· ++ "{" ++ ·.asString ++ "}") "" ++ "\n" ++ + String.join (content.map (·.asString) |>.toList) ++ "\n" ++ + "\\end{" ++ name ++ "}\n" + | .seq texs => String.join (texs.map (·.asString) |>.toList) +where + escape s := s.replace "\\" "\\\\" |>.replace "{" "\\{" |>.replace "}" "\\}" --TODO make correct! + +declare_syntax_cat macro_name +scoped syntax ident : macro_name +scoped syntax "section" : macro_name + +partial def _root_.Lean.TSyntax.macroName : TSyntax `macro_name → String + | ⟨.node _ _ #[.atom _ x]⟩ => x + | ⟨.node _ _ #[.ident _ _ x ..]⟩ => x.eraseMacroScopes.toString + | _ => "fake tag name!!!" + + +declare_syntax_cat tex + +scoped syntax "\\TeX{" tex* "}" : term + +scoped syntax "\\Lean{" term "}" : tex +scoped syntax "\\begin{" macro_name "}" ("[" tex* "]")* ("{" tex* "}")* tex* "\\end{" macro_name "}" : tex +scoped syntax "\\" macro_name ("[" tex* "]")* ("{" tex* "}")* : tex +scoped syntax "s!" interpolatedStr(term) : tex + +scoped syntax str : tex + +open Macro in +macro_rules + | `(term|\TeX{\Lean{$e}}) => pure e + | `(term|\TeX{ $s:str }) => + ``(TeX.text $s) + | `(term|\TeX{ s!$s }) => + ``(TeX.raw (s!$s)) + | `(term| \TeX{ \begin{ $env:macro_name } $[ [ $opt ] ]* $[ { $req } ]* $contents:tex* \end{ $env':macro_name}}) => do + if env.macroName != env'.macroName then Macro.throwErrorAt env' "Mismatched closing environment" + ``(TeX.environment $(quote env.macroName) #[$[\TeX{$opt}],*] #[$[\TeX{$req}],*] #[$[\TeX{$contents}],*]) + | `(term| \TeX{ \ $command:macro_name $[ [ $opt ] ]* $[ { $req } ]* }) => + ``(TeX.command $(quote command.macroName) #[$[\TeX{$opt}],*] #[$[\TeX{$req}],*]) + | `(term|\TeX{ $TeX:tex* }) => + ``(TeX.seq #[ $[\TeX{ $TeX }],* ]) + + +/-- info: LeanDoc.Output.TeX.seq #[] -/ +#guard_msgs in +#eval repr <| \TeX{} + +/-- info: LeanDoc.Output.TeX.text "Hello, world!" -/ +#guard_msgs in +#eval repr <| \TeX{"Hello, world!"} + +/-- +info: LeanDoc.Output.TeX.seq + #[LeanDoc.Output.TeX.text "Hello, ", LeanDoc.Output.TeX.command "textbf" #[] #[LeanDoc.Output.TeX.text "world"]] +-/ +#guard_msgs in +#eval repr <| \TeX{"Hello, " \textbf{"world"}} + +/-- +info: LeanDoc.Output.TeX.environment + "Verbatim" + #[] + #[LeanDoc.Output.TeX.raw "commandChars=\\\\"] + #[LeanDoc.Output.TeX.text "Hello, ", LeanDoc.Output.TeX.command "textbf" #[] #[LeanDoc.Output.TeX.text "world"]] +-/ +#guard_msgs in +#eval repr <| \TeX{\begin{Verbatim}{s!"commandChars=\\\\"}"Hello, " \textbf{"world"}\end{Verbatim}} diff --git a/src/manual/LeanDoc/Genre/Manual.lean b/src/manual/LeanDoc/Genre/Manual.lean new file mode 100644 index 0000000..7a2bfe8 --- /dev/null +++ b/src/manual/LeanDoc/Genre/Manual.lean @@ -0,0 +1,69 @@ +import LeanDoc.Doc +import LeanDoc.Doc.Concrete +import LeanDoc.Doc.TeX +import LeanDoc.Output.TeX + +import LeanDoc.Genre.Manual.TeX + + +open LeanDoc.Doc + +open LeanDoc.Genre.Manual.TeX + +namespace LeanDoc.Genre + +structure Manual.PartMetadata where + authors : List String := [] + +def Manual : Genre where + PartMetadata := Manual.PartMetadata + Block := Empty + Inline := Empty + TraverseContext := Unit + TraverseState := Unit + +instance : TeX.GenreTeX Manual IO where + part go _meta txt := go txt + block _go b _txt := nomatch b + inline _go i _txt := nomatch i + +namespace Manual + +structure Config where + destination : System.FilePath := "_out" + +def ensureDir (dir : System.FilePath) : IO Unit := do + if !(← dir.pathExists) then + IO.FS.createDirAll dir + if !(← dir.isDir) then + throw (↑ s!"Not a directory: {dir}") + +open IO.FS in +def emitTeX (logError : String → IO Unit) (config : Config) (text : Part Manual) : IO Unit := do + let opts : TeX.Options Manual IO := {headerLevels := #["chapter", "section", "subsection", "subsubsection", "paragraph"], headerLevel := some ⟨0, by simp_arith [Array.size, List.length]⟩, logError := logError} + let rendered ← text.toTeX (opts, (), ()) + let dir := config.destination.join "tex" + ensureDir dir + withFile (dir.join "main.tex") .write fun h => do + h.putStrLn (preamble text.titleString ["author 1", "author 2"]) + h.putStrLn rendered.asString + h.putStrLn postamble + +def manualMain (text : Part Manual) (options : List String) : IO UInt32 := do + let hasError ← IO.mkRef false + let logError msg := do hasError.set true; IO.eprintln msg + let cfg ← opts {} options + + -- TODO xrefs + emitTeX logError cfg text + + if (← hasError.get) then + IO.eprintln "Errors were encountered!" + return 1 + else + return 0 +where + opts (cfg : Config) + | ("--output"::dir::more) => opts {cfg with destination := dir} more + | (other :: _) => throw (↑ s!"Unknown option {other}") + | [] => pure cfg diff --git a/src/manual/LeanDoc/Genre/Manual/TeX.lean b/src/manual/LeanDoc/Genre/Manual/TeX.lean new file mode 100644 index 0000000..a7f7d0a --- /dev/null +++ b/src/manual/LeanDoc/Genre/Manual/TeX.lean @@ -0,0 +1,17 @@ +namespace LeanDoc.Genre.Manual.TeX + +def preamble (title : String) (authors : List String) : String := +" +\\documentclass{book} + +\\title{" ++ title ++ "} +\\author{" ++ String.join (authors.intersperse ",") ++ "} + +\\begin{document} + +\\maketitle + +\\tableofcontents +" + +def postamble : String := "\\end{document}"