Mercurial > hg > Members > atton > agda-proofs

annotate cbc/stack-subtype.agda @ 56:ddcd652969e0

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