comparison src/parallel_execution/stack.agda @ 164:b0c6e0392b00

Add comment to stack.agda
author atton
date Thu, 17 Nov 2016 18:28:13 +0000 (2016-11-17)
parents db647f7ed2f6
children bf26f1105862
comparison
equal deleted inserted replaced
163:f0c144c3861d 164:b0c6e0392b00
3 open import Relation.Binary.PropositionalEquality 3 open import Relation.Binary.PropositionalEquality
4 4
5 data Bool : Set where 5 data Bool : Set where
6 True : Bool 6 True : Bool
7 False : Bool 7 False : Bool
8 8
9 data Maybe (a : Set) : Set where 9 data Maybe (a : Set) : Set where
10 Nothing : Maybe a 10 Nothing : Maybe a
11 Just : a -> Maybe a 11 Just : a -> Maybe a
12 12
13 record Stack {a t : Set} (stackImpl : Set) : Set where 13 record Stack {a t : Set} (stackImpl : Set) : Set where
24 24
25 next : {a : Set} -> Element a -> Maybe (Element a) 25 next : {a : Set} -> Element a -> Maybe (Element a)
26 next (cons _ n) = n 26 next (cons _ n) = n
27 27
28 28
29 {- 29 {-
30 -- cannot define recrusive record definition. so use linked list with maybe.
30 record Element {l : Level} (a : Set l) : Set (suc l) where 31 record Element {l : Level} (a : Set l) : Set (suc l) where
31 field 32 field
32 datum : a 33 datum : a -- `data` is reserved by Agda.
33 next : Maybe (Element a) 34 next : Maybe (Element a)
34 -} 35 -}
35 36
36 37
37 38
38 record SingleLinkedStack (a : Set) : Set where 39 record SingleLinkedStack (a : Set) : Set where
39 field 40 field
40 top : Maybe (Element a) 41 top : Maybe (Element a)
41 open SingleLinkedStack 42 open SingleLinkedStack
42 43
43 pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t 44 pushSingleLinkedStack : {Data t : Set} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
44 pushSingleLinkedStack stack datum next = next stack1 45 pushSingleLinkedStack stack datum next = next stack1
45 where 46 where
46 element = cons datum (top stack) 47 element = cons datum (top stack)
47 -- element = record {next = top stack; datum = datum} 48 stack1 = record {top = Just element}
48 stack1 = record {top = Just element}
49 49
50 50
51 popSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t 51 popSingleLinkedStack : {a t : Set} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
52 popSingleLinkedStack stack cs with (top stack) 52 popSingleLinkedStack stack cs with (top stack)
53 ... | Nothing = cs stack Nothing 53 ... | Nothing = cs stack Nothing
58 58
59 59
60 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a 60 emptySingleLinkedStack : {a : Set} -> SingleLinkedStack a
61 emptySingleLinkedStack = record {top = Nothing} 61 emptySingleLinkedStack = record {top = Nothing}
62 62
63 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a) 63 createSingleLinkedStack : {a b : Set} -> Stack {a} {b} (SingleLinkedStack a)
64 createSingleLinkedStack = record { stack = emptySingleLinkedStack 64 createSingleLinkedStack = record { stack = emptySingleLinkedStack
65 ; push = pushSingleLinkedStack 65 ; push = pushSingleLinkedStack
66 ; pop = popSingleLinkedStack 66 ; pop = popSingleLinkedStack
67 } 67 }
68 68
76 76
77 test02 : {a : Set} -> SingleLinkedStack a -> Bool 77 test02 : {a : Set} -> SingleLinkedStack a -> Bool
78 test02 stack = (popSingleLinkedStack stack) test01 78 test02 stack = (popSingleLinkedStack stack) test01
79 79
80 test03 : Bool 80 test03 : Bool
81 test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02 81 test03 = pushSingleLinkedStack emptySingleLinkedStack (cons True Nothing) test02 -- ok
82 --test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02 82 --test03 = pushSingleLinkedStack emptySingleLinkedStack (False) test02 -- ok
83 83
84 84
85 lemma : test03 ≡ False 85 lemma : test03 ≡ False
86 lemma = refl 86 lemma = refl