Merge pull request #161 from rzk-lang/fix/formatter-crash

Fix formatter crashing the server

.github/workflows/mkdocs.yml

@@ -43,6 +43,12 @@ jobs:
             pushd ${lang_dir} && rzk typecheck; popd ;
           done
 
+      - name: Check Rzk formatting for each language
+        run:
+          for lang_dir in $(ls -d docs/docs/*/); do
+            pushd ${lang_dir} && rzk format --check; popd ;
+          done
+
       - name: 🔨 Install MkDocs Material and mike
         run: pip install -r docs/requirements.txt
 

docs/docs/en/examples/recId.rzk.md

@@ -19,33 +19,33 @@ We begin by introducing common HoTT definitions:
 -- A is contractible there exists x : A such that for any y : A we have x = y.
 #define iscontr (A : U)
   : U
-  := Σ ( a : A) , (x : A) → a =_{A} x
+  := Σ (a : A) , (x : A) → a =_{A} x
 
 -- A is a proposition if for any x, y : A we have x = y
 #define isaprop (A : U)
   : U
-  := ( x : A) → (y : A) → x =_{A} y
+  := (x : A) → (y : A) → x =_{A} y
 
 -- A is a set if for any x, y : A the type x =_{A} y is a proposition
 #define isaset (A : U)
   : U
-  := ( x : A) → (y : A) → isaprop (x =_{A} y)
+  := (x : A) → (y : A) → isaprop (x =_{A} y)
 
 -- A function f : A → B is an equivalence
 -- if there exists g : B → A
 -- such that for all x : A we have g (f x) = x
 -- and for all y : B we have f (g y) = y
 #define isweq (A : U) (B : U) (f : A → B)
   : U
-  := Σ ( g : B → A)
+  := Σ (g : B → A)
   , prod
     ( ( x : A) → g (f x) =_{A} x)
     ( ( y : B) → f (g y) =_{B} y)
 
 -- Equivalence of types A and B
 #define weq (A : U) (B : U)
   : U
-  := Σ ( f : A → B)
+  := Σ (f : A → B)
   , isweq A B f
 
 -- Transport along a path
@@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio
 -- [RS17, Axiom 4.6] Relative function extensionality.
 #define relfunext
   : U
-  := ( I : CUBE)
+  := (I : CUBE)
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
   → ( ( t : ψ) → iscontr (A t))
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( t : ψ) → A t [ φ t ↦ a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
@@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( f : (t : ψ) → A t [ φ t ↦ a t ])
-  → ( g : ( t : ψ) → A t [ φ t ↦ a t ])
+  → ( g : (t : ψ) → A t [ φ t ↦ a t ])
   → weq
     ( f = g)
     ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])
@@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape:
 
 -- Restrict extension type to a subshape.
 #define restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 
 -- Restrict extension type to a subshape.
 #define restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 ```
@@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : ψ)
   → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
   := a  -- type is coerced automatically here
 
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : φ)
   → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
   := a  -- type is coerced automatically here

docs/docs/en/getting-started/dependent-types.rzk.md

@@ -79,7 +79,7 @@ which we will discuss soon. For now, we give definition of product types:
 #define prod
   ( A B : U)
   : U
-  := Σ ( _ : A) , B
+  := Σ (_ : A) , B
 ```
 
 The type `#!rzk prod A B` corresponds to the product type $A \times B$.
@@ -188,7 +188,7 @@ For example, for the product type `#!rzk prod A B`, recursion principle looks li
   ( C : U)
   ( f : A → B → C)
   : prod A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 For the `#!rzk Unit` type, recursion principle is trivial:
@@ -223,7 +223,7 @@ For example, for the product type `#!rzk prod A B`, induction principle looks li
   ( C : prod A B → U)
   ( f : (a : A) → (b : B) → C (a , b))
   : ( z : prod A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 We can use `#!rzk ind-prod` to prove the uniqueness principle for products.
@@ -313,7 +313,7 @@ The first projection can be easily defined in terms of pattern matching:
   ( A : U)
   ( B : A → U)
   : ( Σ ( a : A) , B a) → A
-  := \ ( a , _) → a
+  := \ (a , _) → a
 ```
 
 However, second projection requires some care. For instance, we might try this:
@@ -339,7 +339,7 @@ To access it, we need a dependent function:
   ( A : U)
   ( B : A → U)
   : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
-  := \ ( _ , b) → b
+  := \ (_ , b) → b
 ```
 
 In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types (as in "total spaces"):
@@ -349,7 +349,7 @@ In Rzk, it is sometimes more convenient to talk about Σ-types as "total" types
   ( A : U)
   ( B : A → U)
   : U
-  := Σ ( a : A) , B a
+  := Σ (a : A) , B a
 ```
 
 We can use pattern matching in the function type and this new definition to write
@@ -376,7 +376,7 @@ the recursion principle for product types:
   ( C : U)
   ( f : (a : A) → B a → C)
   : total-type A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 The induction principle is, again, a generalization of the recursion
@@ -389,7 +389,7 @@ principle to dependent types:
   ( C : total-type A B → U)
   ( f : (a : A) → (b : B a) → C (a , b))
   : ( z : total-type A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 As before, using `#!rzk ind-Σ` we may prove the uniqueness principle, now for Σ-types:
@@ -424,7 +424,7 @@ Using `#!rzk ind-Σ` we can also prove a type-theoretic axiom of choice:
 ```rzk
 #define AxiomOfChoice
   : U
-  := ( A : U)
+  := (A : U)
     → ( B : U)
     → ( R : A → B → U)
     → ( ( x : A) → Σ (y : B) , R x y)

docs/docs/ru/examples/recId.rzk.md

@@ -19,33 +19,33 @@ We begin by introducing common HoTT definitions:
 -- A is contractible there exists x : A such that for any y : A we have x = y.
 #define iscontr (A : U)
   : U
-  := Σ ( a : A) , (x : A) → a =_{A} x
+  := Σ (a : A) , (x : A) → a =_{A} x
 
 -- A is a proposition if for any x, y : A we have x = y
 #define isaprop (A : U)
   : U
-  := ( x : A) → (y : A) → x =_{A} y
+  := (x : A) → (y : A) → x =_{A} y
 
 -- A is a set if for any x, y : A the type x =_{A} y is a proposition
 #define isaset (A : U)
   : U
-  := ( x : A) → (y : A) → isaprop (x =_{A} y)
+  := (x : A) → (y : A) → isaprop (x =_{A} y)
 
 -- A function f : A → B is an equivalence
 -- if there exists g : B → A
 -- such that for all x : A we have g (f x) = x
 -- and for all y : B we have f (g y) = y
 #define isweq (A : U) (B : U) (f : A → B)
   : U
-  := Σ ( g : B → A)
+  := Σ (g : B → A)
   , prod
     ( ( x : A) → g (f x) =_{A} x)
     ( ( y : B) → f (g y) =_{B} y)
 
 -- Equivalence of types A and B
 #define weq (A : U) (B : U)
   : U
-  := Σ ( f : A → B)
+  := Σ (f : A → B)
   , isweq A B f
 
 -- Transport along a path
@@ -66,12 +66,12 @@ We can now define relative function extensionality. There are several formulatio
 -- [RS17, Axiom 4.6] Relative function extensionality.
 #define relfunext
   : U
-  := ( I : CUBE)
+  := (I : CUBE)
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
   → ( ( t : ψ) → iscontr (A t))
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( t : ψ) → A t [ φ t ↦ a t]
 
 -- [RS17, Proposition 4.8] A (weaker) formulation of function extensionality.
@@ -82,9 +82,9 @@ We can now define relative function extensionality. There are several formulatio
   → ( ψ : I → TOPE)
   → ( φ : ψ → TOPE)
   → ( A : ψ → U)
-  → ( a : ( t : φ) → A t)
+  → ( a : (t : φ) → A t)
   → ( f : (t : ψ) → A t [ φ t ↦ a t ])
-  → ( g : ( t : ψ) → A t [ φ t ↦ a t ])
+  → ( g : (t : ψ) → A t [ φ t ↦ a t ])
   → weq
     ( f = g)
     ( ( t : ψ) → (f t =_{A t} g t) [ φ t ↦ refl ])
@@ -106,13 +106,13 @@ First, we define how to restrict an extension type to a subshape:
 
 -- Restrict extension type to a subshape.
 #define restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 
 -- Restrict extension type to a subshape.
 #define restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : I | ψ t ∧ φ t) → A t
   := \ t → a t
 ```
@@ -122,14 +122,14 @@ Then, how to reformulate an `a` (or `b`) as an extension of its restriction:
 ```rzk
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_psi
-  ( a : ( t : ψ) → A t)
+  ( a : (t : ψ) → A t)
   : ( t : ψ)
   → A t [ ψ t ∧ φ t ↦ restrict_psi a t ]
   := a  -- type is coerced automatically here
 
 -- Reformulate extension type as an extension of a restriction.
 #define ext-of-restrict_phi
-  ( a : ( t : φ) → A t)
+  ( a : (t : φ) → A t)
   : ( t : φ)
   → A t [ ψ t ∧ φ t ↦ restrict_phi a t ]
   := a  -- type is coerced automatically here

docs/docs/ru/getting-started/dependent-types.rzk.md

@@ -83,7 +83,7 @@ Rzk не предоставляет встроенных типов-произв
 #define prod
   ( A B : U)
   : U
-  := Σ ( _ : A) , B
+  := Σ (_ : A) , B
 ```
 
 Запись `#!rzk prod A B` соответствует типу-произведению $A \times B$.
@@ -193,7 +193,7 @@ Rzk не предоставляет встроенных типов-произв
   ( C : U)
   ( f : A → B → C)
   : prod A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Для типа `#!rzk Unit`, принцип рекурсии тривиален:
@@ -228,7 +228,7 @@ Rzk не предоставляет встроенных типов-произв
   ( C : prod A B → U)
   ( f : (a : A) → (b : B) → C (a , b))
   : ( z : prod A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Мы можем использовать `#!rzk ind-prod` для доказательства принципа уникальности.
@@ -318,7 +318,7 @@ Rzk не предоставляет встроенных типов-произв
   ( A : U)
   ( B : A → U)
   : ( Σ ( a : A) , B a) → A
-  := \ ( a , _) → a
+  := \ (a , _) → a
 ```
 
 Однако, для определения второй проекции нужна осторожность. В частности, следующее определение не сработает:
@@ -344,7 +344,7 @@ undefined variable: a
   ( A : U)
   ( B : A → U)
   : ( z : Σ (a : A) , B a) → B (pr₁ A B z)
-  := \ ( _ , b) → b
+  := \ (_ , b) → b
 ```
 
 Иногда о Σ-типах удобнее говорить как о тотальных (общих?) типах (аналогично "total spaces"):
@@ -354,7 +354,7 @@ undefined variable: a
   ( A : U)
   ( B : A → U)
   : U
-  := Σ ( a : A) , B a
+  := Σ (a : A) , B a
 ```
 
 Мы можем переписать более компактно определение второй проекции,
@@ -381,7 +381,7 @@ undefined variable: a
   ( C : U)
   ( f : (a : A) → B a → C)
   : total-type A B → C
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Аналогично с принципом индукции:
@@ -393,7 +393,7 @@ undefined variable: a
   ( C : total-type A B → U)
   ( f : (a : A) → (b : B a) → C (a , b))
   : ( z : total-type A B) → C z
-  := \ ( a , b) → f a b
+  := \ (a , b) → f a b
 ```
 
 Как и раньше, мы можем использовать `#!rzk ind-Σ` для доказательства принципа уникальности,
@@ -431,7 +431,7 @@ undefined variable: a
 ```rzk
 #define AxiomOfChoice
   : U
-  := ( A : U)
+  := (A : U)
     → ( B : U)
     → ( R : A → B → U)
     → ( ( x : A) → Σ (y : B) , R x y)