rzk-lang · fizruk · Jun 15, 2023 · May 30, 2023 · May 30, 2023 · May 30, 2023
diff --git a/.github/workflows/ghcjs.yml b/.github/workflows/ghcjs.yml
@@ -73,6 +73,7 @@ jobs:
           folder: dist
           target-folder: ${{ github.ref_name }}
           clean: false
+          single-commit: true
 
       - name: "📘 Publish JS \"binaries\""
         if: ${{ github.ref_name == 'main' && github.event_name == 'push' }}
@@ -81,3 +82,4 @@ jobs:
           token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           clean: false
+          single-commit: true
diff --git a/.github/workflows/haddock.yml b/.github/workflows/haddock.yml
@@ -59,3 +59,4 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist/haddock
           target-folder: haddock
+          single-commit: true
diff --git a/.github/workflows/mkdocs.yml b/.github/workflows/mkdocs.yml
@@ -17,6 +17,12 @@ jobs:
       - name: 📥 Checkout repository
         uses: actions/checkout@v3
 
+      - name: 🔨 Install rzk proof assistant
+        uses: jaxxstorm/action-install-gh-release@v1.10.0
+        with:
+          repo: fizruk/rzk
+          rename-to: rzk
+
       - name: 🔨 Build MkDocs
         uses: Tiryoh/actions-mkdocs@v0
         with:
@@ -37,6 +43,7 @@ jobs:
           folder: dist
           target-folder: ${{ github.ref_name }}
           clean: false
+          single-commit: true
 
       - name: 📘 Publish Generated MkDocs
         if: ${{ github.ref_name == 'main' }}
@@ -45,3 +52,4 @@ jobs:
           github_token: ${{ secrets.GITHUB_TOKEN }}
           folder: dist
           clean: false
+          single-commit: true
diff --git a/.gitignore b/.gitignore
@@ -27,3 +27,5 @@ cabal.project.local~
 docs/site
 result
 .direnv
+venv
+__pycache__
diff --git a/docs/custom_theme/main.html b/docs/custom_theme/main.html
@@ -17,5 +17,11 @@
       hljs.addPlugin(new CopyButtonPlugin());
       hljs.highlightAll();
     </script>
+    <style>
+      .rzk-render {
+        float: right;
+        clear: both;
+      }
+    </style>
     {{ super() }}
 {% endblock %}
diff --git a/docs/docs/examples/hom.md → docs/docs/examples/hom.rzk.md b/docs/docs/examples/hom.md → docs/docs/examples/hom.rzk.md
diff --git a/docs/docs/examples/section4.md → docs/docs/examples/section4.rzk.md b/docs/docs/examples/section4.md → docs/docs/examples/section4.rzk.md
diff --git a/docs/docs/examples/short.md → docs/docs/examples/short.rzk.md b/docs/docs/examples/short.md → docs/docs/examples/short.rzk.md
diff --git a/docs/docs/examples/test.md → docs/docs/examples/test.rzk.md b/docs/docs/examples/test.md → docs/docs/examples/test.rzk.md
diff --git a/docs/docs/rzk-1/introduction.md → docs/docs/rzk-1/introduction.rzk.md b/docs/docs/rzk-1/introduction.md → docs/docs/rzk-1/introduction.rzk.md
diff --git a/docs/docs/rzk-1/recId.md → docs/docs/rzk-1/recId.rzk.md b/docs/docs/rzk-1/recId.md → docs/docs/rzk-1/recId.rzk.md
diff --git a/docs/docs/rzk-1/render.md b/docs/docs/rzk-1/render.md
diff --git a/docs/docs/rzk-1/render.rzk.md b/docs/docs/rzk-1/render.rzk.md
@@ -0,0 +1,183 @@
+# Rendering Diagrams
+
+Starting from version `0.3.0`, `rzk` supports rendering of topes, types, and terms as diagrams.
+
+This is a literate `rzk` file:
+
+```rzk
+#lang rzk-1
+```
+
+To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`):
+
+```rzk
+#set-option "render" = "svg"  -- enable rendering in SVG
+```
+
+Rendering is completely automatic, and works in the following situations:
+
+1. Mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes;
+2. Type of mapping from a shape (including curried mappings), up to 3 dimensions, only in products of `2` cubes.
+3. Mappings from a shape that is a section of an existing shape.
+
+The rendering assigns the following colors:
+
+- purple is assigned for parameters (context) variables;
+- blue is used for fillings for types (e.g. for `hom` and `hom2`);
+- red is used for terms (e.g. `Segal-comp-witness`);
+- orange is used for shapes in the tope layer;
+- grey is used for discarded parts of a (larger) mapping (e.g. when extracting a diagonal/face from a larger shape).
+
+The SVG pictures can be inserted directly into `.md` files before a corresponding `rzk` code block. At the bottom of a markdown file, you might want to add stylization, e.g.:
+
+```html
+<style>
+.rzk-render { transition: transform .2s; /* Animation */ }
+.rzk-render:hover { transform: scale(1.5); /* (150% zoom - Note: if the zoom is too large, it will go outside of the viewport) */ }
+</style>
+
+<!-- Definitions for the SVG images above -->
+<svg width="0" height="0">
+  <defs>
+    <style data-bx-fonts="Noto Serif">@import url(https://fonts.googleapis.com/css2?family=Noto+Serif&display=swap);</style>
+    <marker id="arrow" viewBox="0 0 10 10" refX="5" refY="5"
+      markerWidth="5" markerHeight="5" orient="auto-start-reverse">
+      <path d="M 0 2 L 5 5 L 0 8 z" stroke="purple" fill="purple" />
+    </marker>
+  </defs>
+  <style>
+    text, textPath {
+      font-family: Noto Serif;
+      font-size: 28px;
+      dominant-baseline: middle;
+      text-anchor: middle;
+    }
+  </style>
+</svg>
+```
+
+## Examples
+
+### Visualising Simplicial Topes
+
+Topes are visualised with <span style="color: orange">**orange**</span> color:
+
+```rzk
+-- 2-simplex
+#def Δ² : (2 * 2) -> TOPE
+  := \(t, s) -> s <= t
+```
+<br><br>
+Boundary of a tope:
+
+```rzk
+-- boundary of a 2-simplex
+#def ∂Δ² : Δ² -> TOPE
+  := \(t, s) -> s === 0_2 \/ t === 1_2 \/ s === t
+```
+
+The busiest tope diagram involves the entire 3D cube:
+<br><br>
+
+```rzk
+-- 3-dim cube
+#def 2³ : (2 * 2 * 2) -> TOPE
+  := \_ -> TOP
+```
+<br><br><br>
+
+```rzk
+-- 3-simplex
+#def Δ³ : (2 * 2 * 2) -> TOPE
+  := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1
+```
+
+<br><br>
+### Visualising Simplicial Types
+
+Types are visualised with <span style="color: blue">**blue**</span> color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with <span style="color: purple">**purple**</span> color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using <span style="color: gray">**gray**</span> color.
+
+```rzk
+-- [RS17, Definition 5.1]
+-- The type of arrows in A from x to y.
+#def hom
+  (A : U)   -- A type.
+  (x y : A) -- Two points in A.
+  : U                   -- (hom A x y) is a 1-simplex (an arrow)
+  := (t : 2) -> A [    -- in A where
+    t === 0_2 |-> x,    -- * the left endpoint is exactly x
+    t === 1_2 |-> y     -- * the right endpoint is exactly y
+  ]
+```
+
+```rzk
+-- [RS17, Definition 5.2]
+-- the type of commutative triangles in A
+#def hom2
+  (A : U)           -- A type.
+  (x y z : A)       -- Three points in A.
+  (f : hom A x y)   -- An arrow in A from x to y.
+  (g : hom A y z)   -- An arrow in A from y to z.
+  (h : hom A x z)   -- An arrow in A from x to z.
+  : U                           -- (hom2 A x y z f g h) is a 2-simplex (triangle)
+  := { (t1, t2) : Δ² } -> A [   -- in A where
+    t2 === 0_2 |-> f t1,        -- * the top edge is exactly f,
+    t1 === 1_2 |-> g t2,        -- * the right edge is exactly g, and
+    t2 === t1  |-> h t2         -- * the diagonal is exactly h
+  ]
+```
+
+### Visualising Terms of Simplicial Types
+
+Terms (with non-trivial labels) are visualised with <span style="color: red">**red**</span> color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with <span style="color: purple">**purple**</span> color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using <span style="color: gray">**gray**</span> color.
+
+We can visualise terms that fill a shape:
+
+```rzk
+#def square
+  (A : U)
+  (x y z : A)
+  (f : hom A x y)
+  (g : hom A y z)
+  (h : hom A x z)
+  (a : Sigma (h' : hom A x z), hom2 A x y z f g h')
+  : (2 * 2) -> A
+  := \(t, s) -> recOR( s <= t |-> second a (t, s) , t <= s |-> second a (s, t))
+```
+
+If a term is extracted as a part of a larger shape, generally, the whole shape will be shown (in gray):
+
+```rzk
+#def face
+  (A : U)
+  (x y z : A)
+  (f : hom A x y)
+  (a : Sigma (g : hom A y z), {((t1, t2), t3) : 2 * 2 * 2 | t3 <= t1 \/ t2 <= t1} -> A [ t1 === 0_2 |-> f t2, t1 === 1_2 |-> g t3 ])
+  : Δ² -> A
+  := \(t, s) -> second a ((t, t), s)
+```
+
+<!-- Style for the SVG images above -->
+<style>
+.rzk-render { transition: transform .2s; /* Animation */ }
+.rzk-render:hover { transform: scale(1.5); /* (150% zoom - Note: if the zoom is too large, it will go outside of the viewport) */ }
+</style>
+
+<!-- Definitions for the SVG images above -->
+<svg width="0" height="0">
+  <defs>
+    <style data-bx-fonts="Noto Serif">@import url(https://fonts.googleapis.com/css2?family=Noto+Serif&display=swap);</style>
+    <marker id="arrow" viewBox="0 0 10 10" refX="5" refY="5"
+      markerWidth="5" markerHeight="5" orient="auto-start-reverse">
+      <path d="M 0 2 L 5 5 L 0 8 z" stroke="black" fill="black" />
+    </marker>
+  </defs>
+  <style>
+    text, textPath {
+      font-family: Noto Serif;
+      font-size: 28px;
+      dominant-baseline: middle;
+      text-anchor: middle;
+    }
+  </style>
+</svg>
diff --git a/docs/docs/rzk-1/sections.md → docs/docs/rzk-1/sections.rzk.md b/docs/docs/rzk-1/sections.md → docs/docs/rzk-1/sections.rzk.md
diff --git a/docs/generate_svgs.py b/docs/generate_svgs.py
@@ -0,0 +1,46 @@
+import re
+import logging
+import subprocess
+
+from mkdocs.structure.pages import Page
+from mkdocs.structure.files import Files
+from mkdocs.config.defaults import MkDocsConfig
+
+
+logger = logging.getLogger('mkdocs')
+rzk_code_block = re.compile(r'(^```\s*rzk[^\n]*\s+(.*?)\s+^```)', flags=re.MULTILINE | re.DOTALL)
+svg_element = re.compile(r'^(<svg.*?</svg>)', flags=re.MULTILINE | re.DOTALL)
+rzk_installed = True
+
+try:
+    # Capture output to prevent logging usage
+    subprocess.run('rzk', capture_output=True)
+except FileNotFoundError:
+    logger.warn('Rzk executable not found')
+    rzk_installed = False
+
+
+def on_page_markdown(md: str, page: Page, config: MkDocsConfig, files: Files) -> str:
+    if not page.file.src_uri.endswith('.rzk.md'): return md
+    if not rzk_installed: return md
+    # Some snippets can depend on terms defined in previous snippets, so we need to store them all
+    previous_snippets = ['#lang rzk-1\n#set-option "render" = "svg"\n\n']
+    # Since each snippet will contain previous ones, the previously printed SVGs should not be repeated
+    previous_svgs: set[str] = set()
+    code_blocks = rzk_code_block.findall(md)
+    for (fenced_block, code) in code_blocks:
+        previous_snippets.append(code.replace('#lang rzk-1', ''))
+        full_code = '\n'.join(previous_snippets).encode()
+        process = subprocess.run('rzk typecheck', capture_output=True, input=full_code)
+        if process.returncode != 0: continue
+
+        output = process.stderr.decode()
+        svgs: list[str] = svg_element.findall(output)
+        # One snippet might have more than one diagram, so we shouldn't just use svgs[-1]
+        # However, there is probably a more efficient way than iterating over all matches everytime
+        for svg in svgs:
+            if svg in previous_svgs: continue
+            previous_svgs.add(svg)
+            md = md.replace(fenced_block, svg + '\n\n' + fenced_block)
+
+    return md
diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml
@@ -25,3 +25,6 @@ theme:
   custom_dir: custom_theme/
 extra_css:
   - https://cdnjs.cloudflare.com/ajax/libs/highlight.js/11.7.0/styles/default.min.css
+
+hooks:
+  - generate_svgs.py
diff --git a/docs/requirements.txt b/docs/requirements.txt
@@ -1 +1,2 @@
+mkdocs
 python-markdown-math
diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs
@@ -2936,7 +2936,7 @@ renderCube
   -> (String -> Maybe RenderObjectData)
   -> String
 renderCube camera rotY renderDataOf' = unlines $ filter (not . null)
-  [ "<svg class=\"zoom\" style=\"float: right\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"
+  [ "<svg class=\"rzk-render\" viewBox=\"-175 -200 350 375\" width=\"150\" height=\"150\">"
   , intercalate "\n"
       [ "  <path d=\"M " <> show x1 <> " " <> show y1
                 <> " L " <> show x2 <> " " <> show y2