Mercurial > hg > GearsTemplate
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 |