idris2-containers/test/src/Seq1/Unsized.idr at 8ca9f408df875d121f0feb36aa503236501bc4a3 · Matthew-Mosior/idris2-containers · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
module Seq1.Unsized

import Data.List
import Data.Linear.Ref1
import Data.Linear.Token
import Data.Seq1.Unsized
import Hedgehog

%hide Prelude.Ops.infixl.(|>)
%hide Prelude.Ops.infixr.(<|)
%hide Prelude.Stream.(::)

prop_eq_refl : Property
prop_eq_refl = property $ do
  vs <- forAll (list (linear 0 20) anyBits8)
  ( run1 $ \t =>
      let vs' # t := Data.Seq1.Unsized.fromList vs t
        in Data.Seq1.Unsized.toList vs' t ) === vs

prop_size : Property
prop_size = property $ do
  vs <- forAll (list (linear 0 20) anyBits8)
  ( run1 $ \t =>
      let vs' # t := Data.Seq1.Unsized.fromList vs t
        in Data.Seq1.Unsized.length vs' t ) === length vs

prop_replicate : Property
prop_replicate = property $ do
  vs <- forAll (list (linear 0 20) anyBits8)
  ( run1 $ \t =>
      let vs' # t := Data.Seq1.Unsized.replicate 5 1 t
        in Data.Seq1.Unsized.toList vs' t ) === replicate 5 1

prop_cons : Property
prop_cons = property $ do
  vs <- forAll (list (linear 0 20) anyBits8)
  ( run1 $ \t =>
      let vs' # t := Data.Seq1.Unsized.fromList vs t
          _   # t := Data.Seq1.Unsized.cons 1 vs' t
        in Data.Seq1.Unsized.toList vs' t ) === 1 :: vs

prop_snoc : Property
prop_snoc = property $ do
  vs <- forAll (list (linear 0 20) anyBits8)
  ( run1 $ \t =>
      let vs' # t := Data.Seq1.Unsized.fromList vs t
          _   # t := Data.Seq1.Unsized.snoc vs' 1 t
        in Data.Seq1.Unsized.toList vs' t ) === vs ++ [1]

export
props : Group
props = MkGroup "Seq1 (Unsized)"
  [ ("prop_eq_refl", prop_eq_refl)
  , ("prop_size", prop_size)
  , ("prop_replicate", prop_replicate)
  , ("prop_cons", prop_cons)
  , ("prop_snoc", prop_snoc)
  ]