comparison Paper/src/AgdaInterface.agda @ 3:576637483425

fix section, source code,etc
author ryokka
date Thu, 19 Apr 2018 20:28:12 +0900
parents bf2887cd22c1
children 4312a27022d1
comparison
equal deleted inserted replaced
2:43e263faf88b 3:576637483425
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 1 data Maybe {n : Level } (a : Set n) : Set n where
5 Nothing : Maybe a 2 Nothing : Maybe a
6 Just : a -> Maybe a 3 Just : a -> Maybe a
7 4
8 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where 5 record StackMethods {n m : Level } (a : Set n ) {t : Set m }(stackImpl : Set n ) : Set (m Level.⊔ n) where
9 field 6 field
10 push : stackImpl -> a -> (stackImpl -> t) -> t 7 push : stackImpl -> a -> (stackImpl -> t) -> t
11 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t 8 pop : stackImpl -> (stackImpl -> Maybe a -> t) -> t
12 pop2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
13 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t 9 get : stackImpl -> (stackImpl -> Maybe a -> t) -> t
14 get2 : stackImpl -> (stackImpl -> Maybe a -> Maybe a -> t) -> t
15 clear : stackImpl -> (stackImpl -> t) -> t
16 open StackMethods 10 open StackMethods
17 11
18 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where 12 record Stack {n m : Level } (a : Set n ) {t : Set m } (si : Set n ) : Set (m Level.⊔ n) where
19 field 13 field
20 stack : si 14 stack : si
21 stackMethods : StackMethods {n} {m} a {t} si 15 stackMethods : StackMethods {n} {m} a {t} si
22 pushStack : a -> (Stack a si -> t) -> t 16 pushStack : a -> (Stack a si -> t) -> t
23 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } )) 17 pushStack d next = push (stackMethods ) (stack ) d (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
24 popStack : (Stack a si -> Maybe a -> t) -> t 18 popStack : (Stack a si -> Maybe a -> t) -> t
25 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) 19 popStack next = pop (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
26 pop2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
27 pop2Stack next = pop2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
28 getStack : (Stack a si -> Maybe a -> t) -> t 20 getStack : (Stack a si -> Maybe a -> t) -> t
29 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 ) 21 getStack next = get (stackMethods ) (stack ) (\s1 d1 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 )
30 get2Stack : (Stack a si -> Maybe a -> Maybe a -> t) -> t
31 get2Stack next = get2 (stackMethods ) (stack ) (\s1 d1 d2 -> next (record {stack = s1 ; stackMethods = stackMethods }) d1 d2)
32 clearStack : (Stack a si -> t) -> t
33 clearStack next = clear (stackMethods ) (stack ) (\s1 -> next (record {stack = s1 ; stackMethods = stackMethods } ))
34
35 open Stack 22 open Stack