unison/doc2.u

{-
- [x] Debug the lexer/parser combination
- [x] Implement display logic for doc type (Unison side)
- [ ] Add to IOSource
- [ ] Implement display logic for new doc type in DisplayValues
- [ ] Write illustrative transcript (and possibly separate tests)
- [ ] Review with Simon, Rúnar, to see if we're missing any elements
- [ ] PR writeup
- [ ] (Later) Pretty-printer should reverse the syntax
- [ ] (Later) docs command should look for foo.doc if nothing is linked, or just have it do: display foo.doc
- [ ] (Later) Top level types should allow anon doc blocks
- [ ] (Later) Remove backticks syntax
- [ ] (Later) Instant docs preview
- [ ] (Later) Remove old doc, rename Doc2 to Doc
-}

id x = x 

unique[fb488e55e66e2492c2946388e4e846450701db04] type Doc2.Term = Term Any

Doc2.term : 'a -> Doc2.Term
Doc2.term a = Doc2.Term.Term (Any a)

unique[da70bff6431da17fa515f3d18ded11852b6a745f] type Doc2.SpecialForm
  = Source [Either Link.Type Doc2.Term]
  | Example Nat Doc2.Term
  | Link (Either Link.Type Doc2.Term)
  | Signature [Doc2.Term]
  | InlineSignature Doc2.Term
  | Eval Doc2.Term
  | InlineEval Doc2.Term
  | Embed Any
  | InlineEmbed Any

unique[b7a4fb87e34569319591130bf3ec6e24c9955b6a] type Doc2
  = Word Text
  | Code Doc2
  | CodeBlock Text Doc2
  | Bold Doc2
  | Italic Doc2
  | Strikethrough Doc2
  -- style {{ myclass }} mydoc
  | Style Doc2 Doc2
  | Blockquote Doc2
  | Blankline
  | SectionBreak
  | Aside (Optional Doc2) Doc2
  -- callout icon content
  | Callout (Optional Doc2) Doc2
  | Folded Boolean Doc2 Doc2
  | Paragraph [Doc2]
  | BulletedList [Doc2]
  | NumberedList Nat [Doc2]
  | Section Doc2 [Doc2]
  | NamedLink Doc2 Doc2
  | Special Doc2.SpecialForm
  | Docs [Doc2]

unique[d7b2ced8c08b2c6e54050d1f5acedef3395f293d] type Pretty.Annotated w txt
  = Empty
  | Group w (Pretty.Annotated w txt)
  | Lit w txt
  | Wrap w (Pretty.Annotated w txt)
  | OrElse w (Pretty.Annotated w txt) (Pretty.Annotated w txt)
  -- Indent _ initialIndent indentAfterNewline p prefixes the first
  -- line of `p` with `initialIndent`, and subsequent lines by `indentAfterNewline`.
  | Indent w (Pretty.Annotated w txt) (Pretty.Annotated w txt) (Pretty.Annotated w txt)
  | Append w [Pretty.Annotated w txt]

type Pretty txt = Pretty (Pretty.Annotated () txt)

Pretty.get = cases Pretty p -> p

Pretty.map : (txt ->{g} txt2) ->{} Pretty txt ->{g} Pretty txt2
Pretty.map f p =
  go = cases
    Empty -> Empty
    Group _ p -> Group () (go p)
    Lit _ t -> Lit () (f t)
    Wrap _ p -> Wrap () (go p)
    OrElse _ p1 p2 -> OrElse () (go p1) (go p2)
    Indent _ i0 iN p -> Indent () (go i0) (go iN) (go p)
    -- Append _ ps -> Append () (List.map go ps)
  Pretty (go (Pretty.get p))

Pretty.empty : Pretty txt
Pretty.empty = Pretty Empty

{- A group adds a level of breaking. Layout tries not to break a group
   unless needed to fit in available width. Breaking is done "outside in".

   (a | b) <> (c | d) will try (a <> c)
                          then (b <> d)

   (a | b) <> group (c | d) will try (a <> c)
                                then (b <> c)
                                then (b <> d)
-}
Pretty.group : Pretty txt -> Pretty txt
Pretty.group p = Pretty (Group () (Pretty.get p))

-- Create a leaf-level `Pretty` that cannot be broken.
Pretty.lit : txt -> Pretty txt
Pretty.lit txt = Pretty (Lit () txt)

-- Turn on wrapping for `p`, which means that it inserts
-- softbreaks (either a space or a newline) between each
-- subgroup or leaf.
-- wrap (lit a <> lit b <> group c) ==
-- wrap (lit a <> group (orElse (lit " ") (lit "\n")
Pretty.wrap : Pretty txt -> Pretty txt
Pretty.wrap p = Pretty (Wrap () (Pretty.get p))

-- If `p1` fits on the current line at its preferred width,
-- it will be chosen, otherwise `p2` is chosen.
Pretty.orElse : Pretty txt -> Pretty txt -> Pretty txt
Pretty.orElse p1 p2 = Pretty (OrElse () (Pretty.get p1) (Pretty.get p2))

-- Prefixes all lines of `p` by `by`.
Pretty.indent : Pretty txt -> Pretty txt -> Pretty txt
Pretty.indent by p = Pretty (Indent () (Pretty.get by) (Pretty.get by) (Pretty.get p))

-- Prefixes the first line of `p` with `initialIndent`, and
-- subsequent lines by `indentAfterNewline`.
Pretty.indent' : Pretty txt -> Pretty txt -> Pretty txt -> Pretty txt
Pretty.indent' initialIndent indentAfterNewline p =
  Pretty (Indent () (Pretty.get initialIndent)
                    (Pretty.get indentAfterNewline)
                    (Pretty.get p))

Pretty.append : Pretty txt -> Pretty txt -> Pretty txt
Pretty.append p1 p2 =
  use Pretty.Annotated Empty Append
  match (Pretty.get p1, Pretty.get p2) with
    (_, Empty) -> p1
    (Empty, _) -> p2
    (Append _ ps1, Append _ ps2) -> Pretty (Append () (ps1 List.++ ps2))
    (Append _ ps1, p2) -> Pretty (Append () (ps1 :+ p2))
    (p1, Append _ ps2) -> Pretty (Append () (p1 +: ps2))
    (p1,p2) -> Pretty (Append () [p1,p2])

Pretty.join : [Pretty txt] -> Pretty txt
Pretty.join =
  go acc = cases [] -> acc
                 h +: t -> go (append acc h) t
  go Pretty.empty

Pretty.sepBy : Pretty txt -> [Pretty txt] -> Pretty txt
Pretty.sepBy sep ps =
  go acc insertSep = cases
    [] -> acc
    ps | insertSep -> go (append acc sep) false ps
    h +: t -> go (append acc h) true t
  go Pretty.empty false ps

syntax.doc.docs = cases [d] -> d
                        ds -> Docs ds
syntax.doc.word = Word
syntax.doc.bold = Doc2.Bold
syntax.doc.italic = Italic
syntax.doc.strikethrough = Strikethrough
syntax.doc.paragraph = Paragraph
syntax.doc.embedTermLink tm =
  guid = "b7a4fb87e34569319591130bf3ec6e24"
  Right (Doc2.term tm)
syntax.doc.embedTypeLink typ =
  guid = "b7a4fb87e34569319591130bf3ec6e24"
  Left typ
syntax.doc.source t = Special (Source t)
syntax.doc.signature ts = Special (Signature ts)
syntax.doc.inlineSignature t = Special (InlineSignature t)
syntax.doc.inlineEval e = Special (InlineEval (Doc2.term e))
syntax.doc.embedSignatureLink tm =
  guid = "d9a4fb87e34569319591130bf3ec6e24"
  Doc2.term tm
syntax.doc.code c = Code c
syntax.doc.codeBlock typ c = CodeBlock typ (word c)
syntax.doc.verbatim c = CodeBlock "raw" c
syntax.doc.evalBlock d = Special (Eval (Doc2.term d))
syntax.doc.eval a = Special (InlineEval (Doc2.term a))
syntax.doc.example n a = Special (Example n (Doc2.term a))
syntax.doc.link t = Special (Link t)
syntax.doc.transclude d =
  guid = "b7a4fb87e34569319591130bf3ec6e24"
  d
syntax.doc.namedLink = NamedLink
syntax.doc.bulletedList = BulletedList
syntax.doc.numberedList = NumberedList
syntax.doc.section = Section

unique[e25bc44d251ae0301517ad0bd02cbd294161dc89] type ConsoleText
  = Plain Text
  | Foreground ANSI.Color ConsoleText
  | Background ANSI.Color ConsoleText
  | Bold ConsoleText
  | Underline ConsoleText
  | Invert ConsoleText

unique[de2e0ee924578939213c950dfd8e0ba1047703ae] type ANSI.Color
  = Black | Red | Green | Yellow | Blue | Magenta | Cyan | White
  | BrightBlack | BrightRed | BrightGreen | BrightYellow | BrightBlue
  | BrightMagenta | BrightCyan | BrightWhite

List.map : (a ->{g} b) ->{} [a] ->{g} [b]
List.map f as =
  go acc = cases
    [] -> acc
    h +: t -> go (acc :+ f h) t
  go [] as

Either.mapRight : (a -> b) -> Either e a -> Either e b
Either.mapRight f = cases
  Right a -> Right (f a)
  Left e -> Left e

syntax.doc.formatConsole : Doc2 -> Pretty (Either SpecialForm ConsoleText)
syntax.doc.formatConsole d =
  lit t = Pretty.lit (Right (Plain t))
  p1 <> p2 = Pretty.append p1 p2
  nl = lit "\n"
  map f p = Pretty.map (mapRight f) p
  go = cases
    Word t -> lit t
    Code d -> lit "`" <> go d <> lit "`"
    CodeBlock typ d ->
      lit "``` " <> lit typ <> nl <>
      go d <> nl <>
      lit "```"
    Italic d -> lit "*" <> go d <> lit "*"
    Strikethrough d -> lit "~~" <> go d <> lit "~~"
    Doc2.Bold d -> map ConsoleText.Bold (go d)
    Style _ d -> go d
    Blockquote d -> Pretty.indent (lit "> ") (go d)
    Blankline -> lit "\n\n"
    SectionBreak -> lit "܍"
    Aside None d -> Pretty.indent (lit "  | ") (go d)
    Aside (Some title) d ->
      Pretty.indent (lit "  | ") (go (Doc2.Bold title) <> nl <> nl <> go d)
    Callout icon d -> go (Aside icon d) --
    Folded _ _closed open -> go open
    Paragraph ds -> Pretty.wrap (Pretty.join (List.map go ds))
    BulletedList ds ->
      item d = Pretty.indent' (lit "* ") (lit "  ") (go d)
      items = List.map item ds
      Pretty.sepBy nl items
    NumberedList n ds ->
      dot = ". "
      w = Text.size (Nat.toText (n + List.size ds)) + size dot
      num n = lit (Text.alignRightWith w ?\s (Nat.toText n Text.++ dot))
      indent = lit (Text.repeat w " ")
      item : Nat -> Doc2 -> Pretty (Either SpecialForm ConsoleText)
      item n d = Pretty.indent' (num n) indent (go d)
      items n acc = cases [] -> acc
                          d +: ds -> items (n+1) (acc :+ item n d) ds
      Pretty.sepBy nl (items n [] ds)
    Section title ds ->
      t = Pretty.indent' (lit "# ") (lit "  ") (go (Doc2.Bold title))
      subs = List.map (d -> Pretty.indent (lit "  ") (go d)) ds
      Pretty.sepBy (nl <> nl) (t +: subs)
    Docs ds -> Pretty.join (List.map go ds)
    NamedLink name _target -> map ConsoleText.Underline (go name)
    Special sf -> Pretty.lit (Left sf)
  go d

doc1 = {{

# Unison documentation format

The syntax tries to be close to markdown.

## Basic formatting

Paragraphs are separated by one or more blanklines. There's syntax for bold, italics, and strikethrough text:

'''
_italics_ or *italics*

**bold text** or __moar bold text__

~~striken text~~

''some code''

[The Unison website](https://unisonweb.org)

A link to a term: {Some}. A link to a type {type List}.
'''

Renders as:

_italics_ or *italics*

**bold text** or __moar bold text__

~~stricken text~~

''some code''

[The Unison website](https://unisonweb.org)

A link to a term: {Some}. A link to a type {type List}.

### Escaping formatting

If you want the text. 

'''
{{ syntax.doc.word "__not bold__"}}
'''

Renders as:

{{ syntax.doc.word "__not bold__" }}

If you have some inline text you want to leave unparsed and have it render in a monospace font, do:

'''
An example of bold text syntax: ''__some bold text__''
'''

Renders as:

An example of bold text syntax: ''__some bold text__''

## Sections and subsections

'''
# Section title! 

Sections consist of section titles followed by zero or more paragraphs or other section elements (such as subsections). 

## Subsection title 

* Item 1
* Item 2

## An empty subsection!

### Subsection 2.1

Some deeply nested content in subsection 2.1
'''

Sections start with a title, then zero or more documents, separated by blanklines. Sections whose title starts with ''##'' are subsections of sections whose title starts with one ''#''. Sections may be nested arbitrarily.

## Lists

### Bulleted lists

Bulleted lists can use ''+'', ''-'', or ''*'' for the bullets. They can be nested, to any depth:

'''
+ A
+ B
+ C
  - C1
  * C2
'''

Renders as:

+ A
+ B
+ C
  - C1
  * C2

### Numbered lists

'''
1. A
2. B
3. C
'''

Renders as:

1. A
2. B
3. C

The first number of the list determines the starting number in the rendered output. The other numbers are ignored:

'''
10. A
99. B
102. C
'''

Renders as:

10. A
99. B
102. C

Numbered lists can be nested as well, and combined with bulleted lists:

'''
1. Wake up.
  + What am I doing here?
  + In this nested list. 
2. Take shower.  
3. Get dressed.
'''

1. Wake up.
  + What am I doing here?
  + In this nested list. 
2. Take shower.  
3. Get dressed.

## Evaluation 

'''
Expressions can be evaluated inline, for instance @eval{1 + 1}.
'''

Renders as:

Expressions can be evaluated inline, for instance @eval{1 + 1}.

Blocks of code can be evaluated as well, for instance:

'''
```
id x = x

id 99
``` 
'''

Renders as:

```
id x = x

id 99
``` 

## Including Unison source code

'''
@source{ type Optional, id }
'''

Renders as:

@source{ type Optional, id }

You can also render just the signatures of a collection of terms: 

'''
@signatures{ id, Some, None }
'''

Renders as:

@signatures{ id, Some, None }

You can reference a signature inline, like so 

'''
An inline signature @signature{id}.
'''

Renders as:

An inline signature @signature{id}.

## Including other documents

'''
"And what is the use of a book," thought {{name}}, "without pictures or conversations?"

* [The documentation]({{baseUrl}}/docs)
'''

"And what is the use of a book," thought {{name}}, "without pictures or conversations?"

## Non-unison code blocks 

A code block with no syntax highlighting starts with at least two {{ code (word "'") }} characters, and is terminated by the same number of {{ code (word "'") }} characters. 

''''
'''
Not formatted. Rendered as a code block with no syntax highlighting.
'''
''''

Renders as:

'''
Not formatted. Rendered as a code block with no syntax highlighting.
'''

You can use triple (or greater) backticks plus a language name for blocks with syntax highlighting.

'''
``` Haskell
-- A fenced code block which isn't parsed by Unison
reverse = foldl (flip (:)) []
```

``` Scala
// A fenced code block which isn't parsed by Unison
def reverse[A](xs: List[A]) = 
  xs.foldLeft(Nil : List[A])((acc,a) => a +: acc)
```
'''

Renders as:

``` Haskell
-- A fenced code block which isn't parsed by Unison
reverse = foldl (flip (:)) []
```

``` Scala
// A fenced code block which isn't parsed by Unison
def reverse[A](xs: List[A]) = 
  xs.foldLeft(Nil : List[A])((acc,a) => a +: acc)
```
}}

name = {{ Alice }}
baseUrl = {{ https://www.unisonweb.org }}