Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/AgdaSingleLinkedStack.agda.replaced @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
1 singleLinkedStackSpec : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ StackMethods {n} {m} a {t} (SingleLinkedStack a)
2 singleLinkedStackSpec = record {
3 push = pushSingleLinkedStack
4 ; pop = popSingleLinkedStack
5 ; pop2 = pop2SingleLinkedStack
6 ; get = getSingleLinkedStack
7 ; get2 = get2SingleLinkedStack
8 ; clear = clearSingleLinkedStack
9 }
10
11 createSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ Stack {n} {m} a {t} (SingleLinkedStack a)
12 createSingleLinkedStack = record {
13 stack = emptySingleLinkedStack ;
14 stackMethods = singleLinkedStackSpec
15 }
16
17 -- Implementation
18
19 pushSingleLinkedStack : {n m : Level } {t : Set m } {Data : Set n} @$\rightarrow$@ SingleLinkedStack Data @$\rightarrow$@ Data @$\rightarrow$@ (Code : SingleLinkedStack Data @$\rightarrow$@ t) @$\rightarrow$@ t
20 pushSingleLinkedStack stack datum next = next stack1
21 where
22 element = cons datum (top stack)
23 stack1 = record {top = Just element}
24
25
26 popSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
27 popSingleLinkedStack stack cs with (top stack)
28 ... | Nothing = cs stack Nothing
29 ... | Just d = cs stack1 (Just data1)
30 where
31 data1 = datum d
32 stack1 = record { top = (next d) }
33
34 pop2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
35 pop2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
36 ... | Nothing = cs stack Nothing Nothing
37 ... | Just d = pop2SingleLinkedStack' {n} {m} stack cs
38 where
39 pop2SingleLinkedStack' : {n m : Level } {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
40 pop2SingleLinkedStack' stack cs with (next d)
41 ... | Nothing = cs stack Nothing Nothing
42 ... | Just d1 = cs (record {top = (next d1)}) (Just (datum d)) (Just (datum d1))
43
44
45 getSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
46 getSingleLinkedStack stack cs with (top stack)
47 ... | Nothing = cs stack Nothing
48 ... | Just d = cs stack (Just data1)
49 where
50 data1 = datum d
51
52 get2SingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
53 get2SingleLinkedStack {n} {m} {t} {a} stack cs with (top stack)
54 ... | Nothing = cs stack Nothing Nothing
55 ... | Just d = get2SingleLinkedStack' {n} {m} stack cs
56 where
57 get2SingleLinkedStack' : {n m : Level} {t : Set m } @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (Code : SingleLinkedStack a @$\rightarrow$@ (Maybe a) @$\rightarrow$@ (Maybe a) @$\rightarrow$@ t) @$\rightarrow$@ t
58 get2SingleLinkedStack' stack cs with (next d)
59 ... | Nothing = cs stack Nothing Nothing
60 ... | Just d1 = cs stack (Just (datum d)) (Just (datum d1))
61
62 clearSingleLinkedStack : {n m : Level } {t : Set m } {a : Set n} @$\rightarrow$@ SingleLinkedStack a @$\rightarrow$@ (SingleLinkedStack a @$\rightarrow$@ t) @$\rightarrow$@ t
63 clearSingleLinkedStack stack next = next (record {top = Nothing})