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