Formatter unit tests

rzk/.gitignore

@@ -2,4 +2,3 @@
 *~
 *.bak
 .DS_Store
-Test

rzk/package.yaml

@@ -117,6 +117,8 @@ tests:
       - -with-rtsopts=-N
     dependencies:
       - rzk
+      - hspec
+      - hspec-discover
 
   doctests:
     source-dirs: test

rzk/rzk.cabal

@@ -159,6 +159,7 @@ test-suite rzk-test
   type: exitcode-stdio-1.0
   main-is: Spec.hs
   other-modules:
+      Rzk.FormatSpec
       Paths_rzk
   hs-source-dirs:
       test
@@ -175,6 +176,8 @@ test-suite rzk-test
     , bifunctors >=5.5.3
     , bytestring >=0.10.8.2
     , directory >=1.2.7.0
+    , hspec
+    , hspec-discover
     , mtl >=2.2.2
     , rzk
     , template-haskell >=2.14.0.0

rzk/test/Rzk/FormatSpec.hs

@@ -0,0 +1,49 @@
+{-|
+Module      : FormatterSpec
+Description : Tests related to the formatter module
+-}
+module Rzk.FormatSpec where
+
+import           Test.Hspec
+
+import           Rzk.Format (format, isWellFormatted)
+
+formatsTo :: FilePath -> FilePath -> Expectation
+formatsTo beforePath afterPath = do
+  beforeSrc <- readFile ("test/files/" ++ beforePath)
+  afterSrc <- readFile ("test/files/" ++ afterPath)
+  format beforeSrc `shouldBe` afterSrc
+  isWellFormatted afterSrc `shouldBe` True -- idempotency
+
+formats :: FilePath -> Expectation
+formats path = (path ++ "-bad.rzk") `formatsTo` (path ++ "-good.rzk")
+
+
+spec :: Spec
+spec = do
+  describe "Formatter" $ do
+    it "Puts definition assumptions, conclusion, and construction on separate lines" $ do
+      -- formats "definition-structure"
+      pendingWith "Doesn't currently place assumptions on a new line"
+
+    it "Replaces common ASCII sequences with their unicode equivalent" $ do
+      formats "unicode"
+
+    it "Formats Rzk blocks in Literate Rzk Markdown" $ do
+      "literate-bad.rzk.md" `formatsTo` "literate-good.rzk.md"
+
+    it "Preserves comments" $ do
+      formats "comments"
+
+    it "Moves trailing binary operators to next line (except lambda arrow)" $ do
+      formats "bin-ops"
+
+    it "Adds relevant spaces to structure constructions like a tree" $ do
+      formats "tree-structure"
+
+    it "Doesn't fail on empty inputs" $ do
+      formats "empty"
+
+    it "Fixes indentation" pending
+
+    it "Wraps long lines" pending

rzk/test/Spec.hs

@@ -1,2 +1 @@
-main :: IO ()
-main = putStrLn "Test suite not yet implemented"
+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}

rzk/test/files/bin-ops-bad.rzk

@@ -0,0 +1,19 @@
+#def function
+  ( parameter-1 : type-1)
+  ( parameter-2 : type-2)
+  : type-with-a-name-3 →
+  type-with-a-longer-name-4 ->
+  short-type-5
+  := undefined
+
+#def is-contr-map-has-retraction uses (is-contr-f)
+  : has-retraction A B f
+  :=
+    ( is-contr-map-inverse ,
+      \ a
+      → ( ap (fib A B f (f a)) A
+          ( is-contr-map-data-in-fiber a)
+          ( (a , refl))
+          ( ( a , refl))
+          ( \ u → first u)
+          ( is-contr-map-path-in-fiber a)))

rzk/test/files/bin-ops-good.rzk

@@ -0,0 +1,19 @@
+#def function
+  ( parameter-1 : type-1)
+  ( parameter-2 : type-2)
+  : type-with-a-name-3
+  → type-with-a-longer-name-4
+  → short-type-5
+  := undefined
+
+#def is-contr-map-has-retraction uses (is-contr-f)
+  : has-retraction A B f
+  :=
+    ( is-contr-map-inverse
+    , \ a →
+      ( ap (fib A B f (f a)) A
+          ( is-contr-map-data-in-fiber a)
+          ( ( a , refl))
+          ( ( a , refl))
+          ( \ u → first u)
+          ( is-contr-map-path-in-fiber a)))

rzk/test/files/comments-bad.rzk

@@ -0,0 +1,9 @@
+#lang rzk-1
+
+-- Flipping the arguments of a function.
+#define flip
+    (A B : U)                         -- For any types A and B
+    (C : (x : A) -> (y : B) -> U)     -- and a type family C
+    (f : (x : A) -> (y : B) -> C x y) -- given a function f : A -> B -> C
+  : (y : B) -> (x : A) -> C x y       -- we construct a function of type B -> A -> C
+  := \y x -> f x y    -- by swapping the arguments

rzk/test/files/comments-good.rzk

@@ -0,0 +1,9 @@
+#lang rzk-1
+
+-- Flipping the arguments of a function.
+#define flip
+    ( A B : U)                         -- For any types A and B
+    ( C : (x : A) → (y : B) → U)     -- and a type family C
+    ( f : (x : A) → (y : B) → C x y) -- given a function f : A -> B -> C
+  : ( y : B) → (x : A) → C x y       -- we construct a function of type B -> A -> C
+  := \ y x → f x y    -- by swapping the arguments

rzk/test/files/definition-structure-bad.rzk

@@ -0,0 +1,7 @@
+#lang  rzk-1
+
+#define id   ( A : U)  :  A → A := \ x → x
+
+#define swap
+  ( A B C : U)
+ : ( A → B → C) → (B → A → C)   := \ f y x → f x y

rzk/test/files/definition-structure-good.rzk

@@ -0,0 +1,11 @@
+#lang rzk-1
+
+#define id
+  ( A : U)
+  : A → A
+  := \ x → x
+
+#define swap
+  ( A B C : U)
+  : ( A → B → C) → (B → A → C)
+  := \ f y x → f x y

rzk/test/files/literate-bad.rzk.md

@@ -0,0 +1,27 @@
+# 1.4 Dependent function types ($\Pi$-types)
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
+
+A polymorphic function is one which takes a type as one of its arguments,
+and then acts on elements of that type (or of other types constructed from it).
+An example is the polymorphic identity function:
+
+```rzk
+#define id
+  (A : U)  : A -> A
+  := \ x →  x
+```
+
+Another, less trivial, example of a polymorphic function is the "swap" operation
+that switches the order of the arguments of a (curried) two-argument function:
+
+```rzk
+#define swap
+  (A B C : U)
+  : (A → B → C) -> (B → A → C)
+  :=\f y x → f x y
+```

rzk/test/files/literate-good.rzk.md

@@ -0,0 +1,28 @@
+# 1.4 Dependent function types ($\Pi$-types)
+
+This is a literate Rzk file:
+
+```rzk
+#lang rzk-1
+```
+
+A polymorphic function is one which takes a type as one of its arguments,
+and then acts on elements of that type (or of other types constructed from it).
+An example is the polymorphic identity function:
+
+```rzk
+#define id
+  ( A : U)
+  : A → A
+  := \ x → x
+```
+
+Another, less trivial, example of a polymorphic function is the "swap" operation
+that switches the order of the arguments of a (curried) two-argument function:
+
+```rzk
+#define swap
+  ( A B C : U)
+  : ( A → B → C) → (B → A → C)
+  := \ f y x → f x y
+```

rzk/test/files/tree-structure-bad.rzk

@@ -0,0 +1,38 @@
+#def is-segal-is-local-horn-inclusion
+  (A : U)
+  (is-local-horn-inclusion-A : is-local-horn-inclusion A)
+  : is-segal A
+  :=
+  \ x y z f g →
+  contractible-fibers-is-equiv-projection
+  (   Λ → A)
+  (\ k →
+    Σ (h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+    , (  hom2 A
+        ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+        (  \ t → k (t , 0₂))
+        ( \t → k (1₂ , t))
+        (h)))
+  (second
+    (   equiv-comp
+      ( Σ ( k : Λ → A)
+        , Σ (h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+          , (hom2 A
+              ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+              (\ t → k (t , 0₂))
+              (\ t → k (1₂ , t))
+              (h)))
+      (Δ² → A)
+      ( Λ → A)
+      ( inv-equiv
+        (  Δ² → A)
+        (  Σ ( k : Λ → A)
+          , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+            , (hom2 A
+                (k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+                (\ t → k (t , 0₂))
+                (\ t → k (1₂ , t))
+                (h)))
+        ( equiv-horn-restriction A))
+      (horn-restriction A , is-local-horn-inclusion-A)))
+  (horn A x y z f g)

rzk/test/files/tree-structure-good.rzk

@@ -0,0 +1,38 @@
+#def is-segal-is-local-horn-inclusion
+  ( A : U)
+  ( is-local-horn-inclusion-A : is-local-horn-inclusion A)
+  : is-segal A
+  :=
+  \ x y z f g →
+  contractible-fibers-is-equiv-projection
+  ( Λ → A)
+  ( \ k →
+    Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+    , ( hom2 A
+        ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+        ( \ t → k (t , 0₂))
+        ( \ t → k (1₂ , t))
+        ( h)))
+  ( second
+    ( equiv-comp
+      ( Σ ( k : Λ → A)
+        , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+          , ( hom2 A
+              ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+              ( \ t → k (t , 0₂))
+              ( \ t → k (1₂ , t))
+              ( h)))
+      ( Δ² → A)
+      ( Λ → A)
+      ( inv-equiv
+        ( Δ² → A)
+        ( Σ ( k : Λ → A)
+          , Σ ( h : hom A (k (0₂ , 0₂)) (k (1₂ , 1₂)))
+            , ( hom2 A
+                ( k (0₂ , 0₂)) (k (1₂ , 0₂)) (k (1₂ , 1₂))
+                ( \ t → k (t , 0₂))
+                ( \ t → k (1₂ , t))
+                ( h)))
+        ( equiv-horn-restriction A))
+      ( horn-restriction A , is-local-horn-inclusion-A)))
+  ( horn A x y z f g)

rzk/test/files/unicode-bad.rzk

@@ -0,0 +1,17 @@
+#lang rzk-1
+
+#define weird
+  ( A : U)
+  ( I : A -> CUBE)
+  ( x y : A)
+  : CUBE
+  := I x * I y
+
+#define iscontr
+  ( A : U)
+  : U
+  := Sigma (a : A) , (x : A) -> a =_{A} x
+
+#def ∂Δ¹
+  : Δ¹ -> TOPE
+  := \ t -> (t === 0_2 \/ t === 1_2)

rzk/test/files/unicode-good.rzk

@@ -0,0 +1,17 @@
+#lang rzk-1
+
+#define weird
+  ( A : U)
+  ( I : A → CUBE)
+  ( x y : A)
+  : CUBE
+  := I x × I y
+
+#define iscontr
+  ( A : U)
+  : U
+  := Σ (a : A) , (x : A) → a =_{A} x
+
+#def ∂Δ¹
+  : Δ¹ → TOPE
+  := \ t → (t ≡ 0₂ ∨ t ≡ 1₂)