diff --git a/README.md b/README.md index f337b0570..9d15dee80 100644 --- a/README.md +++ b/README.md @@ -6,7 +6,7 @@ An experimental proof assistant for synthetic ∞-categories. -[![Early prototype demo.](images/split-demo.png)](https://fizruk.github.io/rzk/) +[![Early prototype demo.](images/split-demo-render.png)](https://fizruk.github.io/rzk/) ## About this project diff --git a/docs/docs/related/sHoTT.md b/docs/docs/related/sHoTT.md index aecbb113d..029732444 100644 --- a/docs/docs/related/sHoTT.md +++ b/docs/docs/related/sHoTT.md @@ -1,11 +1,11 @@ # sHoTT -[sHoTT](https://github.com/fizruk/sHoTT) is a formalisation project for simplicial HoTT and ∞-categories. +sHoTT is a formalisation project for simplicial HoTT and ∞-categories. -The project is a fork of https://github.com/emilyriehl/yoneda, +The project is a fork of https://github.com/emilyriehl/yoneda, with a goal to grow and eventually include various formalisations for HoTT (e.g. HoTT book), -synthetic fibered ∞-categories from the work of Ulrich Buchholtz and Jonathan Weinberger, variations of cubical type theories, etc. +synthetic fibered ∞-categories from the work of Ulrik Buchholtz and Jonathan Weinberger, variations of cubical type theories, etc. See more details in the documentation of the project at -[https://github.com/fizruk/sHoTT](https://github.com/fizruk/sHoTT). +https://github.com/fizruk/sHoTT. diff --git a/docs/docs/related/simple-topes.md b/docs/docs/related/simple-topes.md index 9517161b7..651bb04e9 100644 --- a/docs/docs/related/simple-topes.md +++ b/docs/docs/related/simple-topes.md @@ -1,6 +1,6 @@ # simple-topes -[simple-topes](https://github.com/fizruk/simple-topes) is a playground theorem prover project for type theory with shapes that allows user-defined cubes and topes. Once stable, the project will be merged into `rzk`, extending it to a proof assistant for type theory with (user-defined) cubes, topes, and shapes. +simple-topes is a playground theorem prover project for type theory with shapes that allows user-defined cubes and topes. Once stable, the project will be merged into `rzk`, extending it to a proof assistant for type theory with (user-defined) cubes, topes, and shapes. See more details in the documentation of the project at -[https://github.com/fizruk/simple-topes](https://github.com/fizruk/simple-topes). +https://github.com/fizruk/simple-topes. diff --git a/docs/docs/rzk-1/introduction.md b/docs/docs/rzk-1/introduction.md index 8135bfcb8..8cd6fa6ca 100644 --- a/docs/docs/rzk-1/introduction.md +++ b/docs/docs/rzk-1/introduction.md @@ -3,7 +3,7 @@ !!! warning "Work-in-progress" The documentation is not yet up-to-date with all the changes introduced in `rzk-0.2.0`.
- See [`rzk` changelog](https://github.com/fizruk/rzk/blob/release-v0.2.0/rzk/ChangeLog.md#v020---2022-04-20) for more details. + See [`rzk` changelog](https://github.com/fizruk/rzk/blob/release-v0.3.0/rzk/ChangeLog.md#v020---2022-04-20) for more details. `rzk` is an experimental proof assistant for synthetic ∞-categories. `rzk-1` is an early version of the language supported by `rzk`. diff --git a/docs/docs/rzk-1/render.md b/docs/docs/rzk-1/render.md new file mode 100644 index 000000000..a1d9fd153 --- /dev/null +++ b/docs/docs/rzk-1/render.md @@ -0,0 +1,415 @@ +# 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 + + + + + + + + + + + + +``` + +## Examples + +### Visualising Simplicial Topes + +Topes are visualised with **orange** color: + + + + + + + + + + + • + • + • + + +```rzk +-- 2-simplex +#def Δ² : (2 * 2) -> TOPE + := \(t, s) -> s <= t +``` +

+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: +

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + • + • + • + • + • + • + • + • + + +```rzk +-- 3-dim cube +#def 2³ : (2 * 2 * 2) -> TOPE + := \_ -> TOP +``` +


+ + + + + + + + + + + + + + + + + + + + + + • + • + • + • + + +```rzk +-- 3-simplex +#def Δ³ : (2 * 2 * 2) -> TOPE + := \((t1, t2), t3) -> t3 <= t2 /\ t2 <= t1 +``` + +

+### Visualising Simplicial Types + +Types are visualised with **blue** color. Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a type is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. + + + + + x + y + + +```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 + ] +``` + + + + + f + f + h + h + g + g + x + y + z + + +```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 **red** color (you can see a detailed label on hover). Recognised parameter part (e.g. fixed endpoints, edges, faces with clear labels) are visualised with **purple** color. When a term is constructed by taking a part of another shape, the rest of the larger shape is colored using **gray** color. + +We can visualise terms that fill a shape: + + + second a (second x₂, first x₂) + + second a (first x₂, second x₂) + + f + f + f + f + first a (second (first x₂, second x₂)) + + g + g + g + g + x + y + y + z + + +```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): + + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + first a (second x₂) + + first a (second x₂) + + f + f + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + second a x₂ + + first a (second x₂) + + y + y + first a (second x₂) + + z + z + first a (second x₂) + + x + y + y + z + y + z + + +```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) +``` + + + + + + + + + + + + + + diff --git a/docs/mkdocs.yml b/docs/mkdocs.yml index 84b15ea60..aa042002e 100644 --- a/docs/mkdocs.yml +++ b/docs/mkdocs.yml @@ -4,6 +4,7 @@ nav: - About: index.md - rzk-1 Language: - Introduction: rzk-1/introduction.md + - Rendering Diagrams: rzk-1/render.md - Weak tope disjunction elimination: rzk-1/recId.md - Tools: - IDE support: tools/ide.md diff --git a/images/split-demo-render.png b/images/split-demo-render.png new file mode 100644 index 000000000..a98b752d6 Binary files /dev/null and b/images/split-demo-render.png differ diff --git a/rzk/ChangeLog.md b/rzk/ChangeLog.md index 05543b32c..1f5efdf65 100644 --- a/rzk/ChangeLog.md +++ b/rzk/ChangeLog.md @@ -6,6 +6,25 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to the [Haskell Package Versioning Policy](https://pvp.haskell.org/). +## v0.3.0 — 2022-04-28 + +This version introduces an experimental feature for generating visualisations for simplicial terms in SVG. +To enable rendering, enable option `"render" = "svg"` (to disable, `"render" = "none"`): + +```rzk +#set-option "render" = "svg" -- enable rendering in SVG +``` + +Minor changes: + +- Exit with non-zero code upon a type error (see b135c4fb) +- Fix external links and some typos in the documentation + +Fixes: + +- Fixed an issue with tope solver when context was empty (see 6196af9e); +- Fixed #33 (missing coherence check for restricted types). + ## v0.2.0 - 2022-04-20 This version was a complete rewrite of the proof assistant, using a new parser, a new internal representation, and a rewrite of the typechecking logic. This is still a prototype, but, arguably, significantly more stable and manageable than version 0.1.0. diff --git a/rzk/debug.txt b/rzk/debug.txt deleted file mode 100644 index 0755b1c4d..000000000 --- a/rzk/debug.txt +++ /dev/null @@ -1,200 +0,0 @@ -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/0-common.rzk -[ 1 out of 7 ] Checking #def prod -[ 2 out of 7 ] Checking #def diagonal -[ 3 out of 7 ] Checking #def composition -[ 4 out of 7 ] Checking #def triple-composition -[ 5 out of 7 ] Checking #def identity -[ 6 out of 7 ] Checking #def constant -[ 7 out of 7 ] Checking #def reindex -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/1-contractible.rzk -[ 1 out of 3 ] Checking #def isContr -[ 2 out of 3 ] Checking #def contraction-center -[ 3 out of 3 ] Checking #def contracting-htpy -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/2-paths.rzk -[ 1 out of 21 ] Checking #def rev -[ 2 out of 21 ] Checking #def concat -[ 3 out of 21 ] Checking #def altconcat -[ 4 out of 21 ] Checking #def refl-concat -[ 5 out of 21 ] Checking #def concat-altconcat -[ 6 out of 21 ] Checking #def altconcat-concat -[ 7 out of 21 ] Checking #def zig-zag-concat -[ 8 out of 21 ] Checking #def zag-zig-concat -[ 9 out of 21 ] Checking #def concat-right-cancel -[ 10 out of 21 ] Checking #def homotopy-concat -[ 11 out of 21 ] Checking #def concat-homotopy -[ 12 out of 21 ] Checking #def alt-triangle-rotation -[ 13 out of 21 ] Checking #def triangle-rotation -[ 14 out of 21 ] Checking #def ap -[ 15 out of 21 ] Checking #def ap-id -[ 16 out of 21 ] Checking #def ap-htpy -[ 17 out of 21 ] Checking #def ap-comp -[ 18 out of 21 ] Checking #def rev-ap-comp -[ 19 out of 21 ] Checking #def transport -[ 20 out of 21 ] Checking #def transport2 -[ 21 out of 21 ] Checking #def apd -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/3-homotopies.rzk -[ 1 out of 10 ] Checking #def homotopy -[ 2 out of 10 ] Checking #def homotopy-rev -[ 3 out of 10 ] Checking #def homotopy-composition -[ 4 out of 10 ] Checking #def homotopy-postwhisker -[ 5 out of 10 ] Checking #def homotopy-prewhisker -[ 6 out of 10 ] Checking #def nat-htpy -[ 7 out of 10 ] Checking #def a-cylinder-homotopy-coherence -[ 8 out of 10 ] Checking #def another-cylinder-homotopy-coherence -[ 9 out of 10 ] Checking #def cylinder-homotopy-coherence -[ 10 out of 10 ] Checking #def rev-cylinder-homotopy-coherence -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/4-equivalences.rzk -[ 1 out of 39 ] Checking #def hasSection -[ 2 out of 39 ] Checking #def hasRetraction -[ 3 out of 39 ] Checking #def isEquiv -[ 4 out of 39 ] Checking #def isEquiv-section -[ 5 out of 39 ] Checking #def isEquiv-retraction -[ 6 out of 39 ] Checking #def isEquiv-htpic-inverses -[ 7 out of 39 ] Checking #def hasInverse -[ 8 out of 39 ] Checking #def hasInverse-inverse -[ 9 out of 39 ] Checking #def hasInverse-isEquiv -[ 10 out of 39 ] Checking #def isEquiv-hasInverse -[ 11 out of 39 ] Checking #def hasInverse-retraction-composite -[ 12 out of 39 ] Checking #def hasInverse-section-composite -[ 13 out of 39 ] Checking #def hasInverse-triple-composite -[ 14 out of 39 ] Checking #def hasInverse-quintuple-composite -[ 15 out of 39 ] Checking #def isHalfAdjointEquiv -[ 16 out of 39 ] Checking #def ALTisHalfAdjointEquiv -[ 17 out of 39 ] Checking #def hasInverse-kept-htpy -[ 18 out of 39 ] Checking #def hasInverse-discarded-htpy -[ 19 out of 39 ] Checking #def hasInverse-discarded-naturality-square -[ 20 out of 39 ] Checking #def hasInverse-rev-cylinder-homotopy-coherence -[ 21 out of 39 ] Checking #def hasInverse-ap-rev-cylinder-homotopy-coherence -[ 22 out of 39 ] Checking #def hasInverse-cylinder-coherence -[ 23 out of 39 ] Checking #def hasInverse-replaced-naturality-square -[ 24 out of 39 ] Checking #def hasInverse-corrected-htpy -[ 25 out of 39 ] Checking #def hasInverse-coherence -[ 26 out of 39 ] Checking #def hasInverse-correctedhasInverse -[ 27 out of 39 ] Checking #def hasInverse-isHalfAdjointEquiv -[ 28 out of 39 ] Checking #def isEquiv-isHalfAdjointEquiv -[ 29 out of 39 ] Checking #def iff -[ 30 out of 39 ] Checking #def Eq -[ 31 out of 39 ] Checking #def sym_Eq -[ 32 out of 39 ] Checking #def compose_Eq -[ 33 out of 39 ] Checking #def compose_isEquiv -[ 34 out of 39 ] Checking #def triple_compose_Eq -[ 35 out of 39 ] Checking #def triple_compose_isEquiv -[ 36 out of 39 ] Checking #def FunExt -[ 37 out of 39 ] Checking #def funext_test -[ 38 out of 39 ] Checking #def fibered-equiv-function-iff -[ 39 out of 39 ] Checking #def fibered-equiv-function-equiv -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/hott/5-total-space.rzk -[ 1 out of 25 ] Checking #def total-space-projection -[ 2 out of 25 ] Checking #def contractible-fibers -[ 3 out of 25 ] Checking #def contractible-fibers-section -[ 4 out of 25 ] Checking #def contractible-fibers-actual-section -[ 5 out of 25 ] Checking #def contractible-fibers-section-htpy -[ 6 out of 25 ] Checking #def contractible-fibers-section-is-section -[ 7 out of 25 ] Checking #def check -[ 8 out of 25 ] Checking #def fibered-path-to-sigma-path -[ 9 out of 25 ] Checking #def contractible-fibers-retraction-htpy -[ 10 out of 25 ] Checking #def contractible-fibers-retraction -[ 11 out of 25 ] Checking #def contractible-fibers-projection-equiv -[ 12 out of 25 ] Checking #def total-path-to-base-path -[ 13 out of 25 ] Checking #def total-path-to-fibered-path -[ 14 out of 25 ] Checking #def projection-equiv-implies-inhabited-fibers -[ 15 out of 25 ] Checking #def projection-coherent-equiv-inverse -[ 16 out of 25 ] Checking #def projection-coherent-equiv-base-htpy -[ 17 out of 25 ] Checking #def projection-coherent-equiv-section -[ 18 out of 25 ] Checking #def projection-coherent-equiv-total-htpy -[ 19 out of 25 ] Checking #def projection-coherent-equiv-fibered-htpy -[ 20 out of 25 ] Checking #def projection-coherent-equiv-base-coherence -[ 21 out of 25 ] Checking #def projection-coherent-equiv-transport-coherence -[ 22 out of 25 ] Checking #def projection-coherent-equiv-fibered-contracting-htpy -[ 23 out of 25 ] Checking #def projection-coherent-equiv-contractible-fibers -[ 24 out of 25 ] Checking #def projection-equiv-contractible-fibers -[ 25 out of 25 ] Checking #def projection-theorem -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/3-simplicial-type-theory.md -[ 1 out of 11 ] Checking #def Δ¹ -[ 2 out of 11 ] Checking #def Δ² -[ 3 out of 11 ] Checking #def Δ³ -[ 4 out of 11 ] Checking #def ∂Δ¹ -[ 5 out of 11 ] Checking #def ∂Δ¹-in-Δ¹ -[ 6 out of 11 ] Checking #def ∂Δ² -[ 7 out of 11 ] Checking #def Λ -[ 8 out of 11 ] Checking #def shapeProd -[ 9 out of 11 ] Checking #def Δ¹×Δ¹ -[ 10 out of 11 ] Checking #def ∂Δ¹×Δ¹ -[ 11 out of 11 ] Checking #def Δ²×Δ¹ -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/4-extension-types.md -[ 1 out of 11 ] Checking #def extension-projection -[ 2 out of 11 ] Checking #def flip-ext-fun -[ 3 out of 11 ] Checking #def flip-ext-fun-inv -[ 4 out of 11 ] Checking #def curry-uncurry -[ 5 out of 11 ] Checking #def uncurry-opcurry -[ 6 out of 11 ] Checking #def fubini -[ 7 out of 11 ] Checking #def axiom-choice -[ 8 out of 11 ] Checking #def cofibration_composition' -[ 9 out of 11 ] Checking #def cofibration_union -[ 10 out of 11 ] Checking #def ExtExt -[ 11 out of 11 ] Checking #def fibered-equiv-extension-equiv -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/5-segal-types.md -[ 1 out of 61 ] Checking #def hom -[ 2 out of 61 ] Checking #def hom2 -[ 3 out of 61 ] Checking #def hom2-triangle -[ 4 out of 61 ] Checking #def isSegal -[ 5 out of 61 ] Checking #def Segal-comp -[ 6 out of 61 ] Checking #def Segal-comp-witness -[ 7 out of 61 ] Checking #def Segal-comp-uniqueness -[ 8 out of 61 ] Checking #def horn-restriction -[ 9 out of 61 ] Checking #def identity-identity-composition -[ 10 out of 61 ] Checking #def horn -[ 11 out of 61 ] Checking #def compositions-are-horn-fillings -[ 12 out of 61 ] Checking #def restriction-equiv -[ 13 out of 61 ] Checking #def Segal-restriction-equiv -[ 14 out of 61 ] Checking #def Segal-restriction-equiv-test -[ 15 out of 61 ] Checking #def isSegal' -[ 16 out of 61 ] Checking #def isSegal-isSegal' -[ 17 out of 61 ] Checking #def isSegal'-isSegal -[ 18 out of 61 ] Checking #def isSegal-iff-isSegal' -[ 19 out of 61 ] Checking #def Segal-function-types-function -[ 20 out of 61 ] Checking #def Segal-function-types-function' -[ 21 out of 61 ] Checking #def Segal-function-types-function-pointwise-check -[ 22 out of 61 ] Checking #def Segal-function-types-function-check -[ 23 out of 61 ] Checking #def Segal-function-types -[ 24 out of 61 ] Checking #def Segal-extension-types-function -[ 25 out of 61 ] Checking #def Segal-extension-types-function' -[ 26 out of 61 ] Checking #def Segal-extension-types-function-pointwise-check -[ 27 out of 61 ] Checking #def Segal-extension-types-function-check -[ 28 out of 61 ] Checking #def Segal-extension-types-start -[ 29 out of 61 ] Checking #def Segal-extension-types-middle -[ 30 out of 61 ] Checking #def Segal-extension-types-last -[ 31 out of 61 ] Checking #def Segal-extension-types -[ 32 out of 61 ] Checking #def arr -[ 33 out of 61 ] Checking #def Segal'-arrow-types -[ 34 out of 61 ] Checking #def Segal-arrow-types -[ 35 out of 61 ] Checking #def id-arr -[ 36 out of 61 ] Checking #def Segal-comp-id -[ 37 out of 61 ] Checking #def Segal-id-comp -[ 38 out of 61 ] Checking #def unbounded-arrow -[ 39 out of 61 ] Checking #def unfolding-square -[ 40 out of 61 ] Checking #def unfolding-square-test -[ 41 out of 61 ] Checking #def unfolding-square-another-test -[ 42 out of 61 ] Checking #def unfolding-square-yet-another-test -[ 43 out of 61 ] Checking #def unfolding-square-horn-left-test -[ 44 out of 61 ] Checking #def unfolding-square-horn-right-test -[ 45 out of 61 ] Checking #def unfolding-square-horn-combined-test -[ 46 out of 61 ] Checking #def square-to-arr-in-arr -[ 47 out of 61 ] Checking #def Segal-comp-witness-triangle -[ 48 out of 61 ] Checking #def Segal-comp-witness-square -[ 49 out of 61 ] Checking #def Segal-arr-in-arr -[ 50 out of 61 ] Checking #def Segal-horn-in-arrow -[ 51 out of 61 ] Checking #def Segal-associativity-witness -[ 52 out of 61 ] Checking #def Segal-associativity-prism -[ 53 out of 61 ] Checking #def Segal-associativity-tetrahedron -[ 54 out of 61 ] Checking #def Segal-triple-composite-also-fails -[ 55 out of 61 ] Checking #def Segal-triple-composite-fails -[ 56 out of 61 ] Checking #def Segal-triple-composite -[ 57 out of 61 ] Checking #def Segal-left-associativity-witness -[ 58 out of 61 ] Checking #def Segal-right-associativity-witness -[ 59 out of 61 ] Checking #def Segal-left-associativity -[ 60 out of 61 ] Checking #def Segal-right-associativity -[ 61 out of 61 ] Checking #def Segal-associativity -Checking module from /Users/nikolaikudasov/git/emilyriehl/yoneda/6-2cat-of-segal-types.md -[ 1 out of 2 ] Checking #def ap -[ 2 out of 2 ] Checking #def functors-pres-id diff --git a/rzk/package.yaml b/rzk/package.yaml index a60851c13..8ff8fef17 100644 --- a/rzk/package.yaml +++ b/rzk/package.yaml @@ -1,5 +1,5 @@ name: rzk -version: 0.2.0 +version: 0.3.0 github: "fizruk/rzk" license: BSD3 author: "Nikolai Kudasov" diff --git a/rzk/rzk.cabal b/rzk/rzk.cabal index d1f374483..1f2905484 100644 --- a/rzk/rzk.cabal +++ b/rzk/rzk.cabal @@ -4,10 +4,10 @@ cabal-version: 1.12 -- -- see: https://github.com/sol/hpack -- --- hash: e731bc697ba22a070995646c30c641e0805466b3cabb2fdf377ce74e07985a32 +-- hash: 7855530fcdfd2a28c4ea3654677ed2d18f83d419f5d1c173f4bb44a915464c06 name: rzk -version: 0.2.0 +version: 0.3.0 synopsis: An experimental proof assistant for synthetic ∞-categories description: Please see the README on GitHub at category: Dependent Types diff --git a/rzk/src/Rzk/Main.hs b/rzk/src/Rzk/Main.hs index a120f55a8..58ec566d5 100644 --- a/rzk/src/Rzk/Main.hs +++ b/rzk/src/Rzk/Main.hs @@ -1,5 +1,6 @@ module Rzk.Main where +import System.Exit (exitFailure) import System.Environment (getArgs) import Control.Monad (forM) @@ -22,11 +23,11 @@ main = do case defaultTypeCheck (typecheckModulesWithLocation modules) of Left err -> do putStrLn "An error occurred when typechecking!" - putStrLn "Rendering type error... (this may take a few seconds)" putStrLn $ unlines [ "Type Error:" , ppTypeErrorInScopedContext' err ] + exitFailure Right () -> putStrLn "Everything is ok!" _ -> ppUsage diff --git a/rzk/src/Rzk/TypeCheck.hs b/rzk/src/Rzk/TypeCheck.hs index 76e7e49bf..485c45787 100644 --- a/rzk/src/Rzk/TypeCheck.hs +++ b/rzk/src/Rzk/TypeCheck.hs @@ -1,4 +1,7 @@ +{-# OPTIONS_GHC -fno-warn-type-defaults #-} {-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE RecordWildCards #-} @@ -84,8 +87,15 @@ typecheckModule (Rzk.Module _loc _lang commands) = go 1 commands term' <- typecheck (toTerm' (addParams params term)) ty' >>= whnfT >>= pure . termIsWHNF let decl = Decl name ty' (Just term') fmap (decl :) $ - localDeclPrepared decl $ - go (i + 1) moreCommands + localDeclPrepared decl $ do + Context{..} <- ask + termSVG <- + case renderBackend of + Just RenderSVG -> renderTermSVG (Pure name) + Just RenderLaTeX -> issueTypeError $ TypeErrorOther "\"latex\" rendering is not yet supported" + Nothing -> pure Nothing + maybe id trace termSVG $ do + go (i + 1) moreCommands go i (command@(Rzk.CommandPostulate _loc name params ty) : moreCommands) = traceTypeCheck Normal ("[ " <> show i <> " out of " <> show totalCommands <> " ]" @@ -132,6 +142,12 @@ setOption "verbosity" = \case "silent" -> localVerbosity Silent _ -> const $ issueTypeError $ TypeErrorOther "unknown verbosity level (use \"debug\", \"normal\", or \"silent\")" +setOption "render" = \case + "svg" -> localRenderBackend (Just RenderSVG) + "latex" -> localRenderBackend (Just RenderLaTeX) + "none" -> localRenderBackend Nothing + _ -> const $ + issueTypeError $ TypeErrorOther "unknown render backend (use \"svg\", \"latex\", or \"none\")" setOption optionName = const $ const $ issueTypeError $ TypeErrorOther ("unknown option " <> show optionName) @@ -328,9 +344,9 @@ data Action var | ActionUnify (TermT var) (TermT var) (TermT var) | ActionUnifyTerms (TermT var) (TermT var) | ActionInfer (Term var) - | ActionContextEntailedBy (TermT var) - | ActionContextEntails (TermT var) - | ActionContextEquiv [TermT var] + | ActionContextEntailedBy [TermT var] (TermT var) + | ActionContextEntails [TermT var] (TermT var) + | ActionContextEquiv [TermT var] [TermT var] | ActionWHNF (TermT var) | ActionNF (TermT var) | ActionCheckCoherence (TermT var, TermT var) (TermT var, TermT var) @@ -338,6 +354,16 @@ data Action var type Action' = Action Rzk.VarIdent +ppTermInContext :: Eq var => TermT var -> TypeCheck var String +ppTermInContext term = do + Context{..} <- ask + return (show (untyped (toRzkVarIdent varOrigs <$> term))) + where + vars = nub (foldMap pure term) + mapping = zip vars defaultVarIdents + toRzkVarIdent origs var = fromMaybe (Rzk.VarIdent "_") $ + join (lookup var origs) <|> lookup var mapping + ppSomeAction :: Eq var => [(var, Maybe Rzk.VarIdent)] -> Int -> Action var -> String ppSomeAction origs n action = ppAction n (toRzkVarIdent <$> action) where @@ -372,16 +398,22 @@ ppAction n = unlines . map (replicate (2 * n) ' ' <>) . \case [ "inferring type for term" , " " <> show term ] - ActionContextEntailedBy term -> - [ "checking if local context includes (is entailed by) restriction tope" + ActionContextEntailedBy ctxTopes term -> + [ "checking if local context" + , intercalate "\n" (map ((" " <>) . show . untyped) ctxTopes) + , "includes (is entailed by) restriction tope" , " " <> show (untyped term) ] - ActionContextEntails term -> - [ "checking if local context is included in (entails) the tope" + ActionContextEntails ctxTopes term -> + [ "checking if local context" + , intercalate "\n" (map ((" " <>) . show . untyped) ctxTopes) + , "is included in (entails) the tope" , " " <> show (untyped term) ] - ActionContextEquiv terms -> - [ "checking if local context is equivalent to the union of the topes" + ActionContextEquiv ctxTopes terms -> + [ "checking if local context" + , intercalate "\n" (map ((" " <>) . show . untyped) ctxTopes) + , "is equivalent to the union of the topes" , intercalate "\n" (map ((" " <>) . show . untyped) terms) ] ActionWHNF term -> @@ -431,10 +463,17 @@ traceTypeCheck msgLevel msg tc = do localVerbosity :: Verbosity -> TypeCheck var a -> TypeCheck var a localVerbosity v = local $ \Context{..} -> Context { verbosity = v, .. } +localRenderBackend :: Maybe RenderBackend -> TypeCheck var a -> TypeCheck var a +localRenderBackend v = local $ \Context{..} -> Context { renderBackend = v, .. } + data Covariance = Covariant -- ^ Positive position. | Contravariant -- ^ Negative position +data RenderBackend + = RenderSVG + | RenderLaTeX + data Context var = Context { varTypes :: [(var, TermT var)] , varValues :: [(var, Maybe (TermT var))] @@ -448,6 +487,7 @@ data Context var = Context , location :: Maybe LocationInfo , verbosity :: Verbosity , covariance :: Covariance + , renderBackend :: Maybe RenderBackend } deriving (Functor, Foldable) emptyContext :: Context var @@ -455,15 +495,16 @@ emptyContext = Context { varTypes = [] , varValues = [] , varOrigs = [] - , localTopes = [] - , localTopesNF = [] - , localTopesNFUnion = [[]] + , localTopes = [topeTopT] + , localTopesNF = [topeTopT] + , localTopesNFUnion = [[topeTopT]] , localTopesEntailBottom = False , actionStack = [] , currentCommand = Nothing , location = Nothing , verbosity = Normal , covariance = Covariant + , renderBackend = Nothing } ppContext' :: Context Rzk.VarIdent -> String @@ -730,25 +771,46 @@ solveRHS topes tope = _ -> tope `elem` topes checkTope :: Eq var => TermT var -> TypeCheck var Bool -checkTope tope = performing (ActionContextEntails tope) $ do - topes' <- asks localTopesNF - tope' <- nfTope tope - return (topes' `entail` tope') +checkTope tope = do + ctxTopes <- asks localTopes + performing (ActionContextEntails ctxTopes tope) $ do + topes' <- asks localTopesNF + tope' <- nfTope tope + return (topes' `entail` tope') + +checkTopeEntails :: Eq var => TermT var -> TypeCheck var Bool +checkTopeEntails tope = do + ctxTopes <- asks localTopes + performing (ActionContextEntailedBy ctxTopes tope) $ do + contextTopes <- asks localTopesNF + restrictionTope <- nfTope tope + let contextTopesRHS = foldr topeAndT topeTopT contextTopes + return ([restrictionTope] `entail` contextTopesRHS) + +checkEntails :: Eq var => TermT var -> TermT var -> TypeCheck var Bool +checkEntails l r = do -- FIXME: add action + l' <- nfTope l + r' <- nfTope r + return ([l'] `entail` r') contextEntailedBy :: Eq var => TermT var -> TypeCheck var () -contextEntailedBy tope = performing (ActionContextEntailedBy tope) $ do - contextTopes <- asks localTopesNF - restrictionTope <- nfTope tope - let contextTopesRHS = foldr topeOrT topeBottomT contextTopes - unless ([restrictionTope] `entail` contextTopesRHS) $ - issueTypeError $ TypeErrorTopeNotSatisfied [restrictionTope] contextTopesRHS +contextEntailedBy tope = do + ctxTopes <- asks localTopes + performing (ActionContextEntailedBy ctxTopes tope) $ do + contextTopes <- asks localTopesNF + restrictionTope <- nfTope tope + let contextTopesRHS = foldr topeOrT topeBottomT contextTopes + unless ([restrictionTope] `entail` contextTopesRHS) $ + issueTypeError $ TypeErrorTopeNotSatisfied [restrictionTope] contextTopesRHS contextEntails :: Eq var => TermT var -> TypeCheck var () -contextEntails tope = performing (ActionContextEntails tope) $ do - topeIsEntailed <- checkTope tope - topes' <- asks localTopesNF - unless topeIsEntailed $ - issueTypeError $ TypeErrorTopeNotSatisfied topes' tope +contextEntails tope = do + ctxTopes <- asks localTopes + performing (ActionContextEntails ctxTopes tope) $ do + topeIsEntailed <- checkTope tope + topes' <- asks localTopesNF + unless topeIsEntailed $ + issueTypeError $ TypeErrorTopeNotSatisfied topes' tope topesEquiv :: Eq var => TermT var -> TermT var -> TypeCheck var Bool topesEquiv expected actual = performing (ActionUnifyTerms expected actual) $ do @@ -757,15 +819,17 @@ topesEquiv expected actual = performing (ActionUnifyTerms expected actual) $ do return ([expected'] `entail` actual' && [actual'] `entail` expected') contextEquiv :: Eq var => [TermT var] -> TypeCheck var () -contextEquiv topes = performing (ActionContextEquiv topes) $ do - contextTopes <- asks localTopesNF - recTopes <- mapM nfTope topes - let contextTopesRHS = foldr topeOrT topeBottomT contextTopes - recTopesRHS = foldr topeOrT topeBottomT recTopes - unless (contextTopes `entail` recTopesRHS) $ - issueTypeError $ TypeErrorTopeNotSatisfied contextTopes recTopesRHS - unless (recTopes `entail` contextTopesRHS) $ - issueTypeError $ TypeErrorTopeNotSatisfied recTopes contextTopesRHS +contextEquiv topes = do + ctxTopes <- asks localTopes + performing (ActionContextEquiv ctxTopes topes) $ do + contextTopes <- asks localTopesNF + recTopes <- mapM nfTope topes + let contextTopesRHS = foldr topeOrT topeBottomT contextTopes + recTopesRHS = foldr topeOrT topeBottomT recTopes + unless (contextTopes `entail` recTopesRHS) $ + issueTypeError $ TypeErrorTopeNotSatisfied contextTopes recTopesRHS + unless (recTopes `entail` contextTopesRHS) $ + issueTypeError $ TypeErrorTopeNotSatisfied recTopes contextTopesRHS switchVariance :: TypeCheck var a -> TypeCheck var a switchVariance = local $ \Context{..} -> Context @@ -1492,7 +1556,7 @@ localTope tope tc = do -- A small optimisation to help unify terms faster let refine = case tope' of TopeEQT _ x y | x == y -> const tc -- no new information added! - _ | tope' `elem` localTopes -> const tc + _ | tope' `elem` localTopes -> const tc -- no new information added! | otherwise -> id refine $ do local (f tope' localTopesNF) tc @@ -2074,7 +2138,7 @@ infer tt = performing (ActionInfer tt) $ case tt of ret <- typeOf body' return (lambdaT (typeFunT orig ty' mtope ret) orig (Just (ty', mtope)) body') Lambda orig (Just (cube, Just tope)) body -> do - cube' <- typecheck cube universeT + cube' <- typecheck cube cubeT mapM_ checkNameShadowing orig enterScope orig cube' $ do tope' <- infer tope @@ -2126,6 +2190,7 @@ infer tt = performing (ActionInfer tt) $ case tt of tope' <- typecheck tope topeT term' <- localTope tope' $ typecheck term ty' return (tope', term') + sequence_ [ checkCoherence l r | l:rs'' <- tails rs', r <- rs'' ] return (typeRestrictedT ty' rs') checkCoherence @@ -2153,3 +2218,576 @@ unsafeInferStandalone' t = , ppTypeErrorInScopedContext' err ] Right tt -> tt + +type PointId = String +type ShapeId = [PointId] + +cube2powerT :: Int -> TermT var +cube2powerT 1 = cube2T +cube2powerT dim = cubeProductT (cube2powerT (dim - 1)) cube2T + +splits :: [a] -> [([a], [a])] +splits [] = [([], [])] +splits (x:xs) = ([], x:xs) : [ (x : before, after) | (before, after) <- splits xs ] + +verticesFrom :: [TermT var] -> [(ShapeId, TermT var)] +verticesFrom ts = combine <$> mapM mk ts + where + mk t = [("0", topeEQT t cube2_0T), ("1", topeEQT t cube2_1T)] + combine xs = ([concat (map fst xs)], foldr1 topeAndT (map snd xs)) + +subTopes2 :: Int -> TermT var -> [(ShapeId, TermT var)] +-- 1-dim +subTopes2 1 t = + [ (words "0", topeEQT t cube2_0T) + , (words "1", topeEQT t cube2_1T) + , (words "0 1", topeTopT) ] +-- 2-dim +subTopes2 2 ts = + -- vertices + [ (words "00", topeEQT t cube2_0T `topeAndT` topeEQT s cube2_0T) + , (words "01", topeEQT t cube2_0T `topeAndT` topeEQT s cube2_1T) + , (words "10", topeEQT t cube2_1T `topeAndT` topeEQT s cube2_0T) + , (words "11", topeEQT t cube2_1T `topeAndT` topeEQT s cube2_1T) + -- edges and the diagonal + , (words "00 01", topeEQT t cube2_0T) + , (words "10 11", topeEQT t cube2_1T) + , (words "00 10", topeEQT s cube2_0T) + , (words "01 11", topeEQT s cube2_1T) + , (words "00 11", topeEQT s t) + -- triangles + , (words "00 01 11", topeLEQT t s) + , (words "00 10 11", topeLEQT s t) + ] + where + t = firstT cube2T ts + s = secondT cube2T ts +-- 3-dim +subTopes2 3 t = + -- vertices + [ (words "000", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_0T) + , (words "001", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_1T) + , (words "010", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_0T) + , (words "011", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_1T) + , (words "100", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_0T) + , (words "101", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_1T) + , (words "110", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_0T) + , (words "111", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_1T) + -- edges + , (words "000 001", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_0T) + , (words "010 011", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 cube2_1T) + , (words "000 010", topeEQT t1 cube2_0T `topeAndT` topeEQT t3 cube2_0T) + , (words "001 011", topeEQT t1 cube2_0T `topeAndT` topeEQT t3 cube2_1T) + , (words "100 101", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_0T) + , (words "110 111", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 cube2_1T) + , (words "100 110", topeEQT t1 cube2_1T `topeAndT` topeEQT t3 cube2_0T) + , (words "101 111", topeEQT t1 cube2_1T `topeAndT` topeEQT t3 cube2_1T) + , (words "000 100", topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_0T) + , (words "001 101", topeEQT t2 cube2_0T `topeAndT` topeEQT t3 cube2_1T) + , (words "010 110", topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_0T) + , (words "011 111", topeEQT t2 cube2_1T `topeAndT` topeEQT t3 cube2_1T) + -- face diagonals + , (words "000 011", topeEQT t1 cube2_0T `topeAndT` topeEQT t2 t3) + , (words "100 111", topeEQT t1 cube2_1T `topeAndT` topeEQT t2 t3) + , (words "000 101", topeEQT t2 cube2_0T `topeAndT` topeEQT t1 t3) + , (words "010 111", topeEQT t2 cube2_1T `topeAndT` topeEQT t1 t3) + , (words "000 110", topeEQT t3 cube2_0T `topeAndT` topeEQT t1 t2) + , (words "001 111", topeEQT t3 cube2_1T `topeAndT` topeEQT t1 t2) + -- the long diagonal + , (words "000 111", topeEQT t3 t2 `topeAndT` topeEQT t2 t1) + -- face triangles + , (words "000 001 011", topeEQT t1 cube2_0T `topeAndT` topeLEQT t2 t3) + , (words "000 010 011", topeEQT t1 cube2_0T `topeAndT` topeLEQT t3 t2) + , (words "100 101 111", topeEQT t1 cube2_1T `topeAndT` topeLEQT t2 t3) + , (words "100 110 111", topeEQT t1 cube2_1T `topeAndT` topeLEQT t3 t2) + , (words "000 001 101", topeEQT t2 cube2_0T `topeAndT` topeLEQT t1 t3) + , (words "000 100 101", topeEQT t2 cube2_0T `topeAndT` topeLEQT t3 t1) + , (words "010 011 111", topeEQT t2 cube2_1T `topeAndT` topeLEQT t1 t3) + , (words "010 110 111", topeEQT t2 cube2_1T `topeAndT` topeLEQT t3 t1) + , (words "000 010 110", topeEQT t3 cube2_0T `topeAndT` topeLEQT t1 t2) + , (words "000 100 110", topeEQT t3 cube2_0T `topeAndT` topeLEQT t2 t1) + , (words "001 011 111", topeEQT t3 cube2_1T `topeAndT` topeLEQT t1 t2) + , (words "001 101 111", topeEQT t3 cube2_1T `topeAndT` topeLEQT t2 t1) + -- diagonal triangles + , (words "000 001 111", topeEQT t1 t2 `topeAndT` topeLEQT t2 t3) + , (words "000 010 111", topeEQT t1 t3 `topeAndT` topeLEQT t1 t2) + , (words "000 100 111", topeEQT t2 t3 `topeAndT` topeLEQT t2 t1) + , (words "000 011 111", topeLEQT t1 t2 `topeAndT` topeEQT t2 t3) + , (words "000 101 111", topeLEQT t2 t1 `topeAndT` topeEQT t1 t3) + , (words "000 110 111", topeLEQT t3 t1 `topeAndT` topeEQT t1 t2) + -- tetrahedra + , (words "000 001 011 111", topeLEQT t1 t2 `topeAndT` topeLEQT t2 t3) + , (words "000 010 011 111", topeLEQT t1 t3 `topeAndT` topeLEQT t3 t2) + , (words "000 001 101 111", topeLEQT t2 t1 `topeAndT` topeLEQT t1 t3) + , (words "000 100 101 111", topeLEQT t2 t3 `topeAndT` topeLEQT t3 t1) + , (words "000 010 110 111", topeLEQT t3 t1 `topeAndT` topeLEQT t1 t2) + , (words "000 100 110 111", topeLEQT t3 t2 `topeAndT` topeLEQT t2 t1) + ] + where + t1 = firstT cube2T (firstT (cube2powerT 2) t) + t2 = secondT cube2T (firstT (cube2powerT 2) t) + t3 = secondT cube2T t +subTopes2 dim _ = error (show dim <> " dimensions are not supported") + +cubeSubTopes :: [(ShapeId, TermT (Inc var))] +cubeSubTopes = subTopes2 3 (Pure Z) + +limitLength :: Int -> String -> String +limitLength n s + | length s > n = take (n - 1) s <> "…" + | otherwise = s + +renderObjectsFor + :: Eq var + => String + -> Int + -> TermT var + -> TermT var + -> TypeCheck var [(ShapeId, RenderObjectData)] +renderObjectsFor mainColor dim t term = fmap catMaybes $ do + forM (subTopes2 dim t) $ \(shapeId, tope) -> do + checkTopeEntails tope >>= \case + False -> return Nothing + True -> typeOf term >>= \case + UniverseTopeT{} -> localTope term $ checkTopeEntails tope >>= \case + False -> return Nothing + True -> return $ Just (shapeId, RenderObjectData + { renderObjectDataLabel = "" + , renderObjectDataFullLabel = "" + , renderObjectDataColor = "orange" -- FIXME: orange for topes? + }) + _ -> do + Context{..} <- ask + term' <- localTope tope $ whnfT term + label <- + case term' of + AppT _ (Pure z) arg + | Just (Just "_") <- lookup z varOrigs -> return "" + | null (nub (foldMap pure arg) \\ nub (foldMap pure t)) -> ppTermInContext (Pure z) + _ -> ppTermInContext term' + return $ Just (shapeId, RenderObjectData + { renderObjectDataLabel = label + , renderObjectDataFullLabel = label + , renderObjectDataColor = + case term' of + Pure{} -> "purple" + AppT _ (Pure x) arg + | Just (Just "_") <- lookup x varOrigs -> mainColor + | null (nub (foldMap pure arg) \\ nub (foldMap pure t)) -> "purple" + _ -> mainColor + }) + +componentWiseEQT :: Int -> TermT var -> TermT var -> TermT var +componentWiseEQT 1 t s = topeEQT t s +componentWiseEQT 2 t s = topeAndT + (componentWiseEQT 1 (firstT cube2T t) (firstT cube2T s)) + (componentWiseEQT 1 (secondT cube2T t) (secondT cube2T s)) +componentWiseEQT 3 t s = topeAndT + (componentWiseEQT 2 (firstT (cube2powerT 2) t) (firstT (cube2powerT 2) s)) + (componentWiseEQT 1 (secondT cube2T t) (secondT cube2T s)) +componentWiseEQT dim _ _ = error ("cannot work with " <> show dim <> " dimensions") + +renderObjectsInSubShapeFor + :: Eq var + => String + -> Int + -> [var] + -> var + -> TermT var + -> TermT var + -> TermT var + -> TypeCheck var [(ShapeId, RenderObjectData)] +renderObjectsInSubShapeFor mainColor dim sub super retType f x = fmap catMaybes $ do + let reduceContext + = foldr topeOrT topeBottomT + . map (foldr topeAndT topeTopT) + . map (filter (\tope -> all (`notElem` tope) sub)) + . map (saturateTopes []) + . simplifyLHS + contextTopes <- asks (reduceContext . localTopesNF) + contextTopes' <- localTope (componentWiseEQT dim (Pure super) x) $ asks (reduceContext . localTopesNF) + forM (subTopes2 dim (Pure super)) $ \(shapeId, tope) -> do + checkEntails tope contextTopes >>= \case + False -> return Nothing + True -> do + Context{..} <- ask + term <- localTope tope (whnfT (appT retType f (Pure super))) + label <- typeOf term >>= \case + UniverseTopeT{} -> return "" + _ -> do + case term of + AppT _ (Pure z) arg + | Just (Just "_") <- lookup z varOrigs -> return "" + | null (nub (foldMap pure arg) \\ [super]) -> ppTermInContext (Pure z) + _ -> ppTermInContext term + color <- checkEntails tope contextTopes' >>= \case + True -> do + case term of + Pure{} -> return "purple" + AppT _ (Pure z) arg + | Just (Just "_") <- lookup z varOrigs -> return mainColor + | null (nub (foldMap pure arg) \\ [super]) -> return "purple" + _ -> return mainColor + False -> return "gray" + return $ Just (shapeId, RenderObjectData + { renderObjectDataLabel = label + , renderObjectDataFullLabel = label + , renderObjectDataColor = color + }) + +renderForSubShapeSVG + :: Eq var + => String + -> Int + -> [var] + -> var + -> TermT var + -> TermT var + -> TermT var + -> TypeCheck var String +renderForSubShapeSVG mainColor dim sub super retType f x = do + objects <- renderObjectsInSubShapeFor mainColor dim sub super retType f x + let objects' = map mk objects + return $ renderCube defaultCamera (if dim > 2 then (pi/7) else 0) $ \obj -> + lookup obj objects' + where + mk (shapeId, renderData) = (intercalate "-" (map fill shapeId), renderData) + fill xs = xs <> replicate (3 - length xs) '1' + +renderForSVG :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var String +renderForSVG mainColor dim t term = do + objects <- renderObjectsFor mainColor dim t term + let objects' = map mk objects + return $ renderCube defaultCamera (if dim > 2 then (pi/7) else 0) $ \obj -> + lookup obj objects' + where + mk (shapeId, renderData) = (intercalate "-" (map fill shapeId), renderData) + fill xs = xs <> replicate (3 - length xs) '1' + +renderTermSVGFor + :: Eq var + => String -- ^ Main color. + -> Int -- ^ Accumulated dimensions so far (from 0 to 3). + -> (Maybe (TermT var, TermT var), [var]) -- ^ Accumulated point term (and its time). + -> TermT var -- ^ Term to render. + -> TypeCheck var (Maybe String) +renderTermSVGFor mainColor accDim (mp, xs) t = do + t' <- whnfT t + ty <- typeOf t' + case t of -- check unevaluated term + AppT _info f x -> typeOf f >>= \case + TypeFunT _ fOrig fArg mtopeArg ret | Just dim <- dimOf fArg, dim <= maxDim -> do + enterScope fOrig fArg $ do + maybe id localTope mtopeArg $ do + Just <$> renderForSubShapeSVG mainColor dim (map S xs) Z ret (S <$> f) (S <$> x) -- FIXME: breaks for 2 * (2 * 2), but works for 2 * 2 * 2 = (2 * 2) * 2 + _ -> traverse (\(p', _) -> renderForSVG mainColor accDim p' t') mp + TypeFunT{} | null xs -> enterScope (Just "_") t' $ do + renderTermSVGFor "blue" 0 (Nothing, []) (Pure Z) -- use blue for types + + _ -> case t' of -- check evaluated term + AppT _info f x -> typeOf f >>= \case + TypeFunT _ fOrig fArg mtopeArg ret | Just dim <- dimOf fArg, dim <= maxDim -> do + enterScope fOrig fArg $ do + maybe id localTope mtopeArg $ do + Just <$> renderForSubShapeSVG mainColor dim (map S xs) Z ret (S <$> f) (S <$> x) -- FIXME: breaks for 2 * (2 * 2), but works for 2 * 2 * 2 = (2 * 2) * 2 + _ -> traverse (\(p', _) -> renderForSVG mainColor accDim p' t') mp + TypeFunT{} | null xs -> enterScope (Just "_") t' $ do + renderTermSVGFor "blue" 0 (Nothing, []) (Pure Z) -- use blue for types + + _ -> case ty of -- check type of the term + TypeFunT _ orig arg mtope ret + | Just dim <- dimOf arg, accDim + dim <= maxDim -> enterScope orig arg $ do + maybe id localTope mtope $ + renderTermSVGFor mainColor (accDim + dim) + (join' (both (fmap S) <$> mp) (S <$> arg) (Pure Z), Z : map S xs) $ + case t' of + LambdaT _ _orig _marg body -> body + _ -> appT ret (S <$> t') (Pure Z) + | null xs -> enterScope orig arg $ do + maybe id localTope mtope $ + renderTermSVGFor mainColor accDim + (both (fmap S) <$> mp, map S xs) $ + case t' of + LambdaT _ _orig _marg body -> body + _ -> appT ret (S <$> t') (Pure Z) + _ -> traverse (\(p', _) -> renderForSVG mainColor accDim p' t') mp + where + maxDim = 3 + + both f (x, y) = (f x, f y) + + join' Nothing Cube2T{} x = Just (x, cube2T) + join' (Just (p, pt)) Cube2T{} x = Just (p', pt') + where + pt' = cubeProductT pt cube2T + p' = pairT pt' p x + join' p (CubeProductT _ l r) x = + join' (join' p l (firstT l x)) r (secondT r x) + join' _ _ _ = Nothing -- FIXME: error? + + dimOf = \case + Cube2T{} -> Just 1 + CubeProductT _ l r -> (+) <$> dimOf l <*> dimOf r + _ -> Nothing + +renderTermSVG :: Eq var => TermT var -> TypeCheck var (Maybe String) +renderTermSVG = renderTermSVGFor "red" 0 (Nothing, []) -- use red for terms by default + +renderTermSVG' :: Eq var => TermT var -> TypeCheck var (Maybe String) +renderTermSVG' t = whnfT t >>= \t' -> typeOf t >>= \case + TypeFunT _ orig arg mtope ret -> enterScope orig arg $ do + maybe id localTope mtope $ case t' of + LambdaT _ _orig _marg (AppT _info f x) -> + typeOf f >>= \case + TypeFunT _ fOrig fArg mtope2 _ret | Just dim <- dimOf fArg -> do + enterScope fOrig fArg $ do + maybe id localTope mtope2 $ do + Just <$> renderForSubShapeSVG "red" dim [S Z] Z (S <$> ret) (S <$> f) (S <$> x) + _ -> defaultRenderTermSVG t' arg ret + _ -> defaultRenderTermSVG t' arg ret + _t' -> return Nothing + where + dimOf = \case + Cube2T{} -> Just 1 + CubeProductT _ l r -> (+) <$> dimOf l <*> dimOf r -- WARNING: breaks for 2 * (2 * 2) + _ -> Nothing + + defaultRenderTermSVG t' arg ret = + case dimOf arg of + Just dim | dim <= 3 -> + Just <$> renderForSVG "red" dim (Pure Z) (appT ret (S <$> t') (Pure Z)) + _ -> renderTermSVG' (appT ret (S <$> t') (Pure Z)) + + +type Point2D a = (a, a) +type Point3D a = (a, a, a) +type Edge3D a = (Point3D a, Point3D a) +type Face3D a = (Point3D a, Point3D a, Point3D a) +type Volume3D a = (Point3D a, Point3D a, Point3D a, Point3D a) + +data CubeCoords2D a b = CubeCoords2D + { vertices :: [(Point3D a, Point2D b)] + , edges :: [(Edge3D a, (Point2D b, Point2D b))] + , faces :: [(Face3D a, (Point2D b, Point2D b, Point2D b))] + , volumes :: [(Volume3D a, (Point2D b, Point2D b, Point2D b, Point2D b))] + } + +data Matrix3D a = Matrix3D + a a a + a a a + a a a + +data Matrix4D a = Matrix4D + a a a a + a a a a + a a a a + a a a a + +data Vector3D a = Vector3D a a a + +data Vector4D a = Vector4D a a a a + +rotateX :: Floating a => a -> Matrix3D a +rotateX theta = Matrix3D + 1 0 0 + 0 (cos theta) (- sin theta) + 0 (sin theta) (cos theta) + +rotateY :: Floating a => a -> Matrix3D a +rotateY theta = Matrix3D + (cos theta) 0 (sin theta) + 0 1 0 + (- sin theta) 0 (cos theta) + +rotateZ :: Floating a => a -> Matrix3D a +rotateZ theta = Matrix3D + (cos theta) (- sin theta) 0 + (sin theta) (cos theta) 0 + 0 0 1 + +data Camera a = Camera + { cameraPos :: Point3D a + , cameraFoV :: a + , cameraAspectRatio :: a + , cameraAngleY :: a + , cameraAngleX :: a + } + +viewRotateX :: Floating a => Camera a -> Matrix4D a +viewRotateX Camera{..} = matrix3Dto4D (rotateX cameraAngleX) + +viewRotateY :: Floating a => Camera a -> Matrix4D a +viewRotateY Camera{..} = matrix3Dto4D (rotateY cameraAngleY) + +viewTranslate :: Num a => Camera a -> Matrix4D a +viewTranslate Camera{..} = Matrix4D + 1 0 0 0 + 0 1 0 0 + 0 0 1 0 + (-x) (-y) (-z) 1 + where + (x, y, z) = cameraPos + +project2D :: Floating a => Camera a -> Matrix4D a +project2D Camera{..} = Matrix4D + (2 * n / (r - l)) 0 ((r + l) / (r - l)) 0 + 0 (2 * n / (t - b)) ((t + b) / (t - b)) 0 + 0 0 (- (f + n) / (f - n)) (- 2 * f * n / (f - n)) + 0 0 (-1) 0 + where + n = 1 + f = 2 + r = n * tan (cameraFoV / 2) + l = -r + t = r * cameraAspectRatio + b = -t + + +matrixVectorMult4D :: Num a => Matrix4D a -> Vector4D a -> Vector4D a +matrixVectorMult4D + (Matrix4D + a1 a2 a3 a4 + b1 b2 b3 b4 + c1 c2 c3 c4 + d1 d2 d3 d4) + (Vector4D a b c d) + = Vector4D a' b' c' d' + where + a' = sum (zipWith (*) [a1, b1, c1, d1] [a, b, c, d]) + b' = sum (zipWith (*) [a2, b2, c2, d2] [a, b, c, d]) + c' = sum (zipWith (*) [a3, b3, c3, d3] [a, b, c, d]) + d' = sum (zipWith (*) [a4, b4, c4, d4] [a, b, c, d]) + +matrix3Dto4D :: Num a => Matrix3D a -> Matrix4D a +matrix3Dto4D + (Matrix3D + a1 b1 c1 + a2 b2 c2 + a3 b3 c3) = Matrix4D + a1 b1 c1 0 + a2 b2 c2 0 + a3 b3 c3 0 + 0 0 0 1 + +fromAffine :: Fractional a => Vector4D a -> (Point2D a, a) +fromAffine (Vector4D a b c d) = ((x, y), zIndex) + where + x = a / d + y = b / d + zIndex = c / d + +point3Dto2D :: Floating a => Camera a -> a -> Point3D a -> (Point2D a, a) +point3Dto2D camera rotY (x, y, z) = fromAffine $ + foldr matrixVectorMult4D (Vector4D x y z 1) $ reverse + [ matrix3Dto4D (rotateY rotY) + , viewTranslate camera + , viewRotateY camera + , viewRotateX camera + , project2D camera + ] + +data RenderObjectData = RenderObjectData + { renderObjectDataLabel :: String + , renderObjectDataFullLabel :: String + , renderObjectDataColor :: String + } + +renderCube + :: (Floating a, Show a) + => Camera a + -> a + -> (String -> Maybe RenderObjectData) + -> String +renderCube camera rotY renderDataOf' = unlines $ filter (not . null) + [ "" + , intercalate "\n" + [ " show x1 <> " " <> show y1 + <> " L " <> show x2 <> " " <> show y2 + <> " L " <> show x3 <> " " <> show y3 + <> " Z\" style=\"fill: " <> renderObjectDataColor <> "; opacity: 0.2\">" <> renderObjectDataFullLabel <> "" <> "\n" <> + " show x <> "\" y=\"" <> show y <> "\" fill=\"" <> renderObjectDataColor <> "\">" <> renderObjectDataLabel <> "" + | (faceId, (((x1, y1), (x2, y2), (x3, y3)), _)) <- faces + , Just RenderObjectData{..} <- [renderDataOf faceId] + , let x = (x1 + x2 + x3) / 3 + , let y = (y1 + y2 + y3) / 3 ] + , intercalate "\n" + [ " show x1 <> "," <> show y1 <> " " <> show x2 <> "," <> show y2 + <> "\" stroke=\"" <> renderObjectDataColor <> "\" stroke-width=\"3\" marker-end=\"url(#arrow)\">" <> renderObjectDataFullLabel <> "" <> "\n" <> + " show x <> "\" y=\"" <> show y <> "\" fill=\"" <> renderObjectDataColor <> "\" stroke=\"white\" stroke-width=\"10\" stroke-opacity=\".8\" paint-order=\"stroke\">" <> renderObjectDataLabel <> "" + | (edge, (((x1, y1), (x2, y2)), _)) <- edges + , Just RenderObjectData{..} <- [renderDataOf edge] + , let x = (x1 + x2) / 2 + , let y = (y1 + y2) / 2 ] + , intercalate "\n" + [ " show x <> "\" y=\"" <> show y <> "\" fill=\"" <> renderObjectDataColor <> "\">" <> renderObjectDataLabel <> "" + | (v, ((x, y), _)) <- vertices + , Just RenderObjectData{..} <- [renderDataOf v]] + , "" ] + where + renderDataOf shapeId = + case renderDataOf' shapeId of + Nothing -> Nothing + Just RenderObjectData{..} -> Just RenderObjectData + -- FIXME: move constants to configurable parameters + { renderObjectDataLabel = hideWhenLargerThan shapeId 5 renderObjectDataLabel + , renderObjectDataFullLabel = limitLength 30 renderObjectDataFullLabel + , .. } + + hideWhenLargerThan shapeId n s + | null s || length s > n = if '-' `elem` shapeId then "" else "•" + | otherwise = s + + vertices = + [ (show x <> show y <> show z, ((500 * x'', 500 * y''), zIndex)) + | x <- [0,1] + , y <- [0,1] + , z <- [0,1] + , let f c = 2 * fromInteger c - 1 + , let x' = f x + , let y' = f (1-y) + , let z' = f z + , let ((x'', y''), zIndex) = point3Dto2D camera rotY (x', y', z') ] + + radius = 20 + + mkEdge r (x1, y1) (x2, y2) = ((x1 + dx, y1 + dy), ((x2 - dx), (y2 - dy))) + where + d = sqrt ((x2 - x1)^2 + (y2 - y1)^2) + dx = r * (x2 - x1) / d + dy = r * (y2 - y1) / d + + scaleAround (cx, cy) s (x, y) = (cx + s * (x - cx), cy + s * (y - cy)) + + mkFace (x1, y1) (x2, y2) (x3, y3) = (p1, p2, p3) + where + cx = (x1 + x2 + x3) / 3 + cy = (y1 + y2 + y3) / 3 + p1 = scaleAround (cx, cy) 0.85 (x1, y1) + p2 = scaleAround (cx, cy) 0.85 (x2, y2) + p3 = scaleAround (cx, cy) 0.85 (x3, y3) + + edges = + [ (intercalate "-" [fromName, toName], (mkEdge radius from to, 0)) + | (fromName, (from, _)) : vs <- tails vertices + , (toName, (to, _)) <- vs + , and (zipWith (<=) fromName toName) + ] + + faces = + [ (intercalate "-" [name1, name2, name3], (mkFace v1 v2 v3, 0)) + | (name1, (v1, _)) : vs <- tails vertices + , (name2, (v2, _)) : vs' <- tails vs + , and (zipWith (<=) name1 name2) + , (name3, (v3, _)) <- vs' + , and (zipWith (<=) name2 name3) + ] + + +defaultCamera :: Floating a => Camera a +defaultCamera = Camera + { cameraPos = (0, 7, 10) + , cameraAngleY = pi + , cameraAngleX = pi/5 + , cameraFoV = pi/15 + , cameraAspectRatio = 1 + }