Mercurial > hg > Members > atton > agda-proofs
annotate cbc/stack-subtype.agda @ 52:4880184e4ab5
Define push/pop using subtype
author | atton <atton@cr.ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 10 Jan 2017 09:04:55 +0000 |
parents | |
children | 6af88ee5c4ca |
rev | line source |
---|---|
52
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
1 open import Level |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
2 open import Data.Maybe |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
3 open import Data.Product |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 open import Data.Nat |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
6 module stack-subtype (A : Set) where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
7 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 -- data definitions |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 data Element (a : Set) : Set where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 cons : a -> Maybe (Element a) -> Element a |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
12 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 datum : {a : Set} -> Element a -> a |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
14 datum (cons a _) = a |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
15 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 next : {a : Set} -> Element a -> Maybe (Element a) |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
17 next (cons _ n) = n |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
19 record SingleLinkedStack (a : Set) : Set where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
20 field |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
21 top : Maybe (Element a) |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
22 open SingleLinkedStack |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
24 record Context : Set where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
25 field |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
26 stack : SingleLinkedStack A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
27 element : Maybe A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
28 n : ℕ |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
29 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
30 open import subtype Context |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
31 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
32 instance |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
33 yo : DataSegment Context |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
34 yo = record {get = (\x -> x) ; set = (\_ c -> c)} |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
35 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
36 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
37 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
38 -- definition based from Gears(209:5708390a9d88) src/parallel_execution |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
39 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
40 emptySingleLinkedStack : SingleLinkedStack A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
41 emptySingleLinkedStack = record {top = nothing} |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
42 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
43 pushSingleLinkedStack : Context -> Context |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
44 pushSingleLinkedStack c = record c { stack = (push c) ; element = nothing} |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
45 where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
46 push : Context -> SingleLinkedStack A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
47 push record { stack = stack ; element = nothing } = stack |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
48 push record { stack = stack ; element = (just x) } = stack1 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
49 where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
50 el = cons x (top stack) |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
51 stack1 = record {top = just el} |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
52 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
53 popSingleLinkedStack : Context -> Context |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
54 popSingleLinkedStack c = record c {element = (elem c) ; stack = (popdStack c)} |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
55 where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
56 elem : Context -> Maybe A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
57 elem record { stack = record { top = (just (cons x _)) } } = just x |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
58 elem record { stack = record { top = nothing } } = nothing |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
59 popdStack : Context -> SingleLinkedStack A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
60 popdStack record { stack = record { top = (just (cons _ s)) } } = record { top = s } |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
61 popdStack record { stack = record { top = nothing } } = record { top = nothing } |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
62 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
63 -- sample |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
64 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
65 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
66 pushCS = cs pushSingleLinkedStack |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
67 popCS = cs popSingleLinkedStack |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
68 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
69 |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
70 -- stack |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
71 record Stack {X Y : Set} (stackImpl : Set -> Set) : Set where |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
72 field |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
73 stack : stackImpl A |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
74 push : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
75 pop : {{_ : DataSegment X}} {{_ : DataSegment Y}} -> CodeSegment X Y |
4880184e4ab5
Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
76 |