Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype.agda @ 61:7af6c894f411

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 02:10:28 +0000
parents bd428bd6b394
children 44d448a978d3
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
1 open import Level hiding (lift)
52
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
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
4 open import Data.Nat hiding (suc)
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
5 open import Function
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 module stack-subtype (A : Set) where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 -- data definitions
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 data Element (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 cons : a -> Maybe (Element a) -> Element a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 datum : {a : Set} -> Element a -> a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 datum (cons a _) = a
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 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
18 next (cons _ n) = n
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 record SingleLinkedStack (a : Set) : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
21 field
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 top : Maybe (Element a)
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 open SingleLinkedStack
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 record Context : Set where
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 field
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
27 -- fields for concrete data segments
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
28 n : ℕ
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
29 -- fields for stack
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
30 element : Maybe A
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
31
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
32
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
33
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
34
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
35
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
36 open import subtype Context as N
52
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 instance
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
39 ContextIsDataSegment : N.DataSegment Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
40 ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
41
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
42
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
43 record Meta : Set₁ where
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
44 field
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
45 -- context as set of data segments
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
46 context : Context
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
47 stack : SingleLinkedStack A
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
48 nextCS : N.CodeSegment Context Context
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
49
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
50
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
51
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
52
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
53 open import subtype Meta as M
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
55 instance
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
56 MetaIncludeContext : M.DataSegment Context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
57 MetaIncludeContext = record { get = Meta.context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
58 ; set = (\m c -> record m {context = c}) }
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
59
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
60 MetaIsMetaDataSegment : M.DataSegment Meta
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
61 MetaIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) }
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
62
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
63
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
64 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
65 liftMeta (N.cs f) = M.cs f
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
66
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
67 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
68 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> N.DataSegment.set y c (f (N.DataSegment.get x c)))
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
69
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
70 -- 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
71
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
72 emptySingleLinkedStack : SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 emptySingleLinkedStack = record {top = nothing}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
75
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
76 pushSingleLinkedStack : Meta -> Meta
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
77 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
78 where
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
79 n = Meta.nextCS m
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
80 s = Meta.stack m
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
81 e = Context.element (Meta.context m)
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
82 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
83 push s nothing = s
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
84 push s (just x) = record {top = just (cons x (top s))}
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
85
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
86
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
87
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
88 popSingleLinkedStack : Meta -> Meta
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
89 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
90 where
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
91 n = Meta.nextCS m
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
92 con = Meta.context m
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
93 elem : Meta -> Maybe A
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
94 elem record {stack = record { top = (just (cons x _)) }} = just x
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
95 elem record {stack = record { top = nothing }} = nothing
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
96 st : Meta -> SingleLinkedStack A
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
97 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
98 st record {stack = record { top = nothing }} = record {top = nothing}
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
99
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
100
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
101
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
102
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
103 pushSingleLinkedStackCS : M.CodeSegment Meta Meta
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
104 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
105
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
106 popSingleLinkedStackCS : M.CodeSegment Meta Meta
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
107 popSingleLinkedStackCS = M.cs popSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
108
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
109
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
110 -- for sample
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
111
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
112 firstContext : Context
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
113 firstContext = record {element = nothing ; n = 0}
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
114
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
115
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
116 firstMeta : Meta
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
117 firstMeta = record { context = firstContext
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
118 ; stack = emptySingleLinkedStack
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
119 ; nextCS = (N.cs (\m -> m))
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
120 }
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
121
61
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
122
7af6c894f411 Trying define n-push
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 60
diff changeset
123