Mercurial > hg > Papers > 2023 > soto-master

comparison Paper/src/stack.agda @ 1:a72446879486

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Init paper
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Thu, 12 Jan 2023 20:28:50 +0900
parents
children
comparison
equal deleted inserted replaced
0:8df537cb6a18 1:a72446879486
1 open import Level renaming (suc to succ ; zero to Zero )
2 module stack where
3
4 open import Relation.Binary.PropositionalEquality
5 open import Relation.Binary.Core
6 open import Data.Nat
7
8 ex : 1 + 2 ≡ 3
9 ex = refl
10
11 data Bool {n : Level } : Set n where
12 True : Bool
13 False : Bool
14
15 record _∧_ {n : Level } (a : Set n) (b : Set n): Set n where
16 field
17 pi1 : a
18 pi2 : b
19
20 data Maybe {n : Level } (a : Set n) : Set n where
21 Nothing : Maybe a
22 Just : a -> Maybe a
23
24 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
25 field
26 push : stackImpl -> a -> (stackImpl -> t) -> t
27 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
28 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
29 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
30 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
31 clear : stackImpl -> (stackImpl -> t) -> t
32 open StackMethods
33
34 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
35 field
36 stack : si
37 stackMethods : StackMethods {n} {m} a {t} si
38 pushStack : a -> (Stack a si -> t) -> t
39 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
40 popStack : (Stack a si -> Maybe a -> t) -> t
41 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
42 pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
43 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
44 getStack : (Stack a si -> Maybe a -> t) -> t
45 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
46 get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
47 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
48 clearStack : (Stack a si -> t) -> t
49 clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
50
51 open Stack
52
53 {--
54 data Element {n : Level } (a : Set n) : Set n where
55 cons : a -> Maybe (Element a) -> Element a
56
57
58 datum : {n : Level } {a : Set n} -> Element a -> a
59 datum (cons a _) = a
60
61 next : {n : Level } {a : Set n} -> Element a -> Maybe (Element a)
62 next (cons _ n) = n
63 --}
64
65
66 -- cannot define recrusive record definition. so use linked list with maybe.
67 record Element {l : Level} (a : Set l) : Set l where
68 inductive
69 constructor cons
70 field
71 datum : a -- `data` is reserved by Agda.
72 next : Maybe (Element a)
73
74 open Element
75
76
77 record SingleLinkedStack {n : Level } (a : Set n) : Set n where
78 field
79 top : Maybe (Element a)
80 open SingleLinkedStack
81
82 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} -> SingleLinkedStack Data -> Data -> (Code : SingleLinkedStack Data -> t) -> t
83 pushSingleLinkedStack stack datum next = next stack1
84 where
85 element = cons datum (top stack)
86 stack1 = record {top = Just element}
87
88
89 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
90 popSingleLinkedStack stack cs with (top stack)
91 ... | Nothing = cs stack Nothing
92 ... | Just d = cs stack1 (Just data1)
93 where
94 data1 = datum d
95 stack1 = record { top = (next d) }
96
97 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
98 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
99 ... | Nothing = cs stack Nothing Nothing
100 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
101 where
102 pop2SingleLinkedStack' : {n m : Level } {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
103 pop2SingleLinkedStack' stack cs with (next d)
104 ... | Nothing = cs stack Nothing Nothing
105 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
106
107
108 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> t) -> t
109 getSingleLinkedStack stack cs with (top stack)
110 ... | Nothing = cs stack Nothing
111 ... | Just d = cs stack (Just data1)
112 where
113 data1 = datum d
114
115 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
116 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
117 ... | Nothing = cs stack Nothing Nothing
118 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
119 where
120 get2SingleLinkedStack' : {n m : Level} {t : Set m } -> SingleLinkedStack a -> (Code : SingleLinkedStack a -> (Maybe a) -> (Maybe a) -> t) -> t
121 get2SingleLinkedStack' stack cs with (next d)
122 ... | Nothing = cs stack Nothing Nothing
123 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
124
125 clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> SingleLinkedStack a -> (SingleLinkedStack a -> t) -> t
126 clearSingleLinkedStack stack next = next (record {top = Nothing})
127
128
129 emptySingleLinkedStack : {n : Level } {a : Set n} -> SingleLinkedStack a
130 emptySingleLinkedStack = record {top = Nothing}
131
132 -----
133 -- Basic stack implementations are specifications of a Stack
134 --
135 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} -> StackMethods {n} {m} a {t} (SingleLinkedStack a)
136 singleLinkedStackSpec = record {
137 push = pushSingleLinkedStack
138 ; pop = popSingleLinkedStack
139 ; pop2 = pop2SingleLinkedStack
140 ; get = getSingleLinkedStack
141 ; get2 = get2SingleLinkedStack
142 ; clear = clearSingleLinkedStack
143 }
144
145 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} -> Stack {n} {m} a {t} (SingleLinkedStack a)
146 createSingleLinkedStack = record {
147 stack = emptySingleLinkedStack ;
148 stackMethods = singleLinkedStackSpec
149 }