Mercurial > hg > Papers > 2018 > ryokka-thesis

comparison final_pre/src/AgdaInterface.agda.replaced @ 7:28f900230c26

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add final_pre
author ryokka
date Mon, 19 Feb 2018 23:32:24 +0900
parents
children
comparison
equal deleted inserted replaced
6:d927f6b3d2b3 7:28f900230c26
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