Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype.agda @ 60:bd428bd6b394

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Trying define n-push/n-pop
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Sat, 14 Jan 2017 00:00:40 +0000
parents ddcd652969e0
children 7af6c894f411
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)
52
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
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
26 -- fields for stack
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 element : Maybe A
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
28 stack : SingleLinkedStack A
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
29 -- fields for data segments
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
30 n : ℕ
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
31
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
32
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
33
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
34 open import subtype Context as N
52
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 instance
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
37 ContextIsDataSegment : N.DataSegment Context
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
38 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
39
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
40
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
41 record Meta : Set₁ where
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
42 field
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
43 context : Context
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
44 nextCS : N.CodeSegment Context Context
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
45
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
46
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
47
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
48 open import subtype Meta as M
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
49
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
50 instance
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
51 MetaIncludeContext : M.DataSegment Context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
52 MetaIncludeContext = record { get = Meta.context
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
53 ; 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
54
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
55 MetaIsMetaDataSegment : M.DataSegment Meta
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
56 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
57
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
58
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
59 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
60 liftMeta (N.cs f) = M.cs f
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
61
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
62 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
63 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
64
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 -- 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
66
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
67 emptySingleLinkedStack : SingleLinkedStack A
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
68 emptySingleLinkedStack = record {top = nothing}
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
69
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
70
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
71 pushSingleLinkedStack : Meta -> Meta
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
72 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {context = record c {stack = (push s e)}})
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
73 where
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
74 c = (Meta.context m)
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
75 n = Meta.nextCS m
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
76 e = Context.element c
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
77 s = Context.stack c
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
78 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
79 push s nothing = s
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
80 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
81
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
82
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
83 popSingleLinkedStack : Meta -> Meta
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
84 popSingleLinkedStack m = M.exec (liftMeta n) (record m { context = record c { stack = (st c) ; element = (elem c)}})
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
85 where
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
86 n = Meta.nextCS m
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
87 c = Meta.context m
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
88 elem : Context -> Maybe A
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
89 elem record {stack = record { top = (just (cons x _)) }} = just x
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
90 elem record {stack = record { top = nothing } } = nothing
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
91 st : Context -> SingleLinkedStack A
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
92 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
93 st record {stack = record { top = nothing } } = record {top = nothing}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
94
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
95
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
96 pushSingleLinkedStackCS : M.CodeSegment Meta Meta
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
97 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
98
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
99 popSingleLinkedStackCS : M.CodeSegment Meta Meta
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
100 popSingleLinkedStackCS = M.cs popSingleLinkedStack
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
101
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
102
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
103 -- for sample
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
104
56
ddcd652969e0 Add executable subtype-stack
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 55
diff changeset
105 firstContext : Context
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
106 firstContext = record {stack = emptySingleLinkedStack ; element = nothing ; n = 0}
54
fa95e3070138 Define SingleLinkedStack using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 53
diff changeset
107
52
4880184e4ab5 Define push/pop using subtype
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents:
diff changeset
108
60
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
109 firstMeta : Meta
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
110 firstMeta = record {nextCS = (N.cs (\m -> m)) ; context = firstContext}
bd428bd6b394 Trying define n-push/n-pop
atton <atton@cr.ie.u-ryukyu.ac.jp>
parents: 56
diff changeset
111