Mercurial > hg > Members > atton > agda-proofs
comparison cbc/stack-subtype.agda @ 61:7af6c894f411
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 |
comparison
equal
deleted
inserted
replaced
60:bd428bd6b394 | 61:7af6c894f411 |
---|---|
1 open import Level hiding (lift) | 1 open import Level hiding (lift) |
2 open import Data.Maybe | 2 open import Data.Maybe |
3 open import Data.Product | 3 open import Data.Product |
4 open import Data.Nat hiding (suc) | 4 open import Data.Nat hiding (suc) |
5 open import Function | |
5 | 6 |
6 module stack-subtype (A : Set) where | 7 module stack-subtype (A : Set) where |
7 | 8 |
8 -- data definitions | 9 -- data definitions |
9 | 10 |
21 top : Maybe (Element a) | 22 top : Maybe (Element a) |
22 open SingleLinkedStack | 23 open SingleLinkedStack |
23 | 24 |
24 record Context : Set where | 25 record Context : Set where |
25 field | 26 field |
27 -- fields for concrete data segments | |
28 n : ℕ | |
26 -- fields for stack | 29 -- fields for stack |
27 element : Maybe A | 30 element : Maybe A |
28 stack : SingleLinkedStack A | 31 |
29 -- fields for data segments | 32 |
30 n : ℕ | |
31 | 33 |
32 | 34 |
33 | 35 |
34 open import subtype Context as N | 36 open import subtype Context as N |
35 | 37 |
38 ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} | 40 ContextIsDataSegment = record {get = (\c -> c) ; set = (\_ c -> c)} |
39 | 41 |
40 | 42 |
41 record Meta : Set₁ where | 43 record Meta : Set₁ where |
42 field | 44 field |
45 -- context as set of data segments | |
43 context : Context | 46 context : Context |
47 stack : SingleLinkedStack A | |
44 nextCS : N.CodeSegment Context Context | 48 nextCS : N.CodeSegment Context Context |
49 | |
45 | 50 |
46 | 51 |
47 | 52 |
48 open import subtype Meta as M | 53 open import subtype Meta as M |
49 | 54 |
67 emptySingleLinkedStack : SingleLinkedStack A | 72 emptySingleLinkedStack : SingleLinkedStack A |
68 emptySingleLinkedStack = record {top = nothing} | 73 emptySingleLinkedStack = record {top = nothing} |
69 | 74 |
70 | 75 |
71 pushSingleLinkedStack : Meta -> Meta | 76 pushSingleLinkedStack : Meta -> Meta |
72 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {context = record c {stack = (push s e)}}) | 77 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) }) |
73 where | 78 where |
74 c = (Meta.context m) | 79 n = Meta.nextCS m |
75 n = Meta.nextCS m | 80 s = Meta.stack m |
76 e = Context.element c | 81 e = Context.element (Meta.context m) |
77 s = Context.stack c | |
78 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A | 82 push : SingleLinkedStack A -> Maybe A -> SingleLinkedStack A |
79 push s nothing = s | 83 push s nothing = s |
80 push s (just x) = record {top = just (cons x (top s))} | 84 push s (just x) = record {top = just (cons x (top s))} |
81 | 85 |
82 | 86 |
87 | |
83 popSingleLinkedStack : Meta -> Meta | 88 popSingleLinkedStack : Meta -> Meta |
84 popSingleLinkedStack m = M.exec (liftMeta n) (record m { context = record c { stack = (st c) ; element = (elem c)}}) | 89 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}}) |
85 where | 90 where |
86 n = Meta.nextCS m | 91 n = Meta.nextCS m |
87 c = Meta.context m | 92 con = Meta.context m |
88 elem : Context -> Maybe A | 93 elem : Meta -> Maybe A |
89 elem record {stack = record { top = (just (cons x _)) }} = just x | 94 elem record {stack = record { top = (just (cons x _)) }} = just x |
90 elem record {stack = record { top = nothing } } = nothing | 95 elem record {stack = record { top = nothing }} = nothing |
91 st : Context -> SingleLinkedStack A | 96 st : Meta -> SingleLinkedStack A |
92 st record {stack = record { top = (just (cons _ s)) }} = record {top = s} | 97 st record {stack = record { top = (just (cons _ s)) }} = record {top = s} |
93 st record {stack = record { top = nothing } } = record {top = nothing} | 98 st record {stack = record { top = nothing }} = record {top = nothing} |
99 | |
100 | |
94 | 101 |
95 | 102 |
96 pushSingleLinkedStackCS : M.CodeSegment Meta Meta | 103 pushSingleLinkedStackCS : M.CodeSegment Meta Meta |
97 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack | 104 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack |
98 | 105 |
101 | 108 |
102 | 109 |
103 -- for sample | 110 -- for sample |
104 | 111 |
105 firstContext : Context | 112 firstContext : Context |
106 firstContext = record {stack = emptySingleLinkedStack ; element = nothing ; n = 0} | 113 firstContext = record {element = nothing ; n = 0} |
107 | 114 |
108 | 115 |
109 firstMeta : Meta | 116 firstMeta : Meta |
110 firstMeta = record {nextCS = (N.cs (\m -> m)) ; context = firstContext} | 117 firstMeta = record { context = firstContext |
118 ; stack = emptySingleLinkedStack | |
119 ; nextCS = (N.cs (\m -> m)) | |
120 } | |
111 | 121 |
122 | |
123 |