Skip to content

Commit

Permalink
Merge pull request #157 from rzk-lang/unit-testing
Browse files Browse the repository at this point in the history
Formatter unit tests
  • Loading branch information
aabounegm authored Dec 14, 2023
2 parents 744a53a + a7c055d commit 244cb67
Show file tree
Hide file tree
Showing 19 changed files with 294 additions and 3 deletions.
1 change: 0 additions & 1 deletion rzk/.gitignore
Original file line number Diff line number Diff line change
Expand Up @@ -2,4 +2,3 @@
*~
*.bak
.DS_Store
Test
2 changes: 2 additions & 0 deletions rzk/package.yaml
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,8 @@ tests:
- -with-rtsopts=-N
dependencies:
- rzk
- hspec
- hspec-discover

doctests:
source-dirs: test
Expand Down
3 changes: 3 additions & 0 deletions rzk/rzk.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
49 changes: 49 additions & 0 deletions rzk/test/Rzk/FormatSpec.hs
Original file line number Diff line number Diff line change
@@ -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
3 changes: 1 addition & 2 deletions rzk/test/Spec.hs
Original file line number Diff line number Diff line change
@@ -1,2 +1 @@
main :: IO ()
main = putStrLn "Test suite not yet implemented"
{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
19 changes: 19 additions & 0 deletions rzk/test/files/bin-ops-bad.rzk
Original file line number Diff line number Diff line change
@@ -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)))
19 changes: 19 additions & 0 deletions rzk/test/files/bin-ops-good.rzk
Original file line number Diff line number Diff line change
@@ -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)))
9 changes: 9 additions & 0 deletions rzk/test/files/comments-bad.rzk
Original file line number Diff line number Diff line change
@@ -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
9 changes: 9 additions & 0 deletions rzk/test/files/comments-good.rzk
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions rzk/test/files/definition-structure-bad.rzk
Original file line number Diff line number Diff line change
@@ -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
11 changes: 11 additions & 0 deletions rzk/test/files/definition-structure-good.rzk
Original file line number Diff line number Diff line change
@@ -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
Empty file added rzk/test/files/empty-bad.rzk
Empty file.
Empty file added rzk/test/files/empty-good.rzk
Empty file.
27 changes: 27 additions & 0 deletions rzk/test/files/literate-bad.rzk.md
Original file line number Diff line number Diff line change
@@ -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
```
28 changes: 28 additions & 0 deletions rzk/test/files/literate-good.rzk.md
Original file line number Diff line number Diff line change
@@ -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
```
38 changes: 38 additions & 0 deletions rzk/test/files/tree-structure-bad.rzk
Original file line number Diff line number Diff line change
@@ -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)
38 changes: 38 additions & 0 deletions rzk/test/files/tree-structure-good.rzk
Original file line number Diff line number Diff line change
@@ -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)
17 changes: 17 additions & 0 deletions rzk/test/files/unicode-bad.rzk
Original file line number Diff line number Diff line change
@@ -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)
17 changes: 17 additions & 0 deletions rzk/test/files/unicode-good.rzk
Original file line number Diff line number Diff line change
@@ -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₂)

0 comments on commit 244cb67

Please sign in to comment.