|
7
|
1 open import Level renaming (suc to succ ; zero to Zero )
|
|
|
2 module AgdaInterface where
|
|
|
3
|
|
|
4 data Maybe {n : Level } (a : Set n) : Set n where
|
|
|
5 Nothing : Maybe a
|
|
|
6 Just : a @$\rightarrow$@ Maybe a
|
|
|
7
|
|
|
8 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
9 field
|
|
|
10 push : stackImpl @$\rightarrow$@ a @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
11 pop : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
12 pop2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
13 get : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
14 get2 : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
15 clear : stackImpl @$\rightarrow$@ (stackImpl @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
16 open StackMethods
|
|
|
17
|
|
|
18 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.@$\sqcup$@ n) where
|
|
|
19 field
|
|
|
20 stack : si
|
|
|
21 stackMethods : StackMethods {n} {m} a {t} si
|
|
|
22 pushStack : a @$\rightarrow$@ (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
23 pushStack d next = push (stackMethods ) (stack ) d (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
|
|
|
24 popStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
25 popStack next = pop (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
|
|
|
26 pop2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
27 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
|
|
|
28 getStack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
29 getStack next = get (stackMethods ) (stack ) (\s1 d1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
|
|
|
30 get2Stack : (Stack a si @$\rightarrow$@ Maybe a @$\rightarrow$@ Maybe a @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
31 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
|
|
|
32 clearStack : (Stack a si @$\rightarrow$@ t) @$\rightarrow$@ t
|
|
|
33 clearStack next = clear (stackMethods ) (stack ) (\s1 @$\rightarrow$@ next (record {stack = s1 ; stackMethods = stackMethods } ))
|
|
|
34
|
|
|
35 open Stack
|
