|
7
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2 module AgdaStackTest where
|
|
|
3
|
|
|
4 open import stack
|
|
|
5
|
|
|
6 open import Relation.Binary.PropositionalEquality
|
|
|
7 open import Relation.Binary.Core
|
|
|
8 open import Data.Nat
|
|
|
9 open import Function
|
|
|
10
|
|
|
11
|
|
|
12 open SingleLinkedStack
|
|
|
13 open Stack
|
|
|
14
|
|
|
15
|
|
|
16 -- after push 1 and 2, pop2 get 1 and 2
|
|
|
17
|
|
|
18 testStack02 : {m : Level } -> ( Stack ℕ (SingleLinkedStack ℕ) -> Bool {m} ) -> Bool {m}
|
|
|
19 testStack02 cs = pushStack createSingleLinkedStack 1 (\s -> pushStack s 2 cs)
|
|
|
20
|
|
|
21
|
|
|
22 testStack031 : (d1 d2 : ℕ ) -> Bool {Zero}
|
|
|
23 testStack031 2 1 = True
|
|
|
24 testStack031 _ _ = False
|
|
|
25
|
|
|
26 testStack032 : (d1 d2 : Maybe ℕ) -> Bool {Zero}
|
|
|
27 testStack032 (Just d1) (Just d2) = testStack031 d1 d2
|
|
|
28 testStack032 _ _ = False
|
|
|
29
|
|
|
30 testStack03 : {m : Level } -> Stack ℕ (SingleLinkedStack ℕ) -> ((Maybe ℕ) -> (Maybe ℕ) -> Bool {m} ) -> Bool {m}
|
|
|
31 testStack03 s cs = pop2Stack s (\s d1 d2 -> cs d1 d2 )
|
|
|
32
|
|
|
33 testStack04 : Bool
|
|
|
34 testStack04 = testStack02 (\s -> testStack03 s testStack032)
|
|
|
35
|
|
|
36 testStack05 : testStack04 ≡ True
|
|
|
37 testStack05 = refl
|
