Mercurial > hg > Papers > 2018 > ryokka-sigos
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 |