|
1
|
1 open import Level hiding (lift)
|
|
|
2 open import Data.Maybe
|
|
|
3 open import Data.Product
|
|
|
4 open import Data.Nat hiding (suc)
|
|
|
5 open import Function
|
|
|
6
|
|
|
7 module stack-subtype (A : Set) where
|
|
|
8
|
|
|
9 -- data definitions
|
|
|
10
|
|
|
11 data Element (a : Set) : Set where
|
|
|
12 cons : a @$\rightarrow$@ Maybe (Element a) @$\rightarrow$@ Element a
|
|
|
13
|
|
|
14 datum : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ a
|
|
|
15 datum (cons a _) = a
|
|
|
16
|
|
|
17 next : {a : Set} @$\rightarrow$@ Element a @$\rightarrow$@ Maybe (Element a)
|
|
|
18 next (cons _ n) = n
|
|
|
19
|
|
|
20 record SingleLinkedStack (a : Set) : Set where
|
|
|
21 field
|
|
|
22 top : Maybe (Element a)
|
|
|
23 open SingleLinkedStack
|
|
|
24
|
|
|
25 record Context : Set where
|
|
|
26 field
|
|
|
27 -- fields for concrete data segments
|
|
|
28 n : @$\mathbb{N}$@
|
|
|
29 -- fields for stack
|
|
|
30 element : Maybe A
|
|
|
31
|
|
|
32
|
|
|
33
|
|
|
34
|
|
|
35
|
|
|
36 open import subtype Context as N
|
|
|
37
|
|
|
38 instance
|
|
|
39 ContextIsDataSegment : N.DataSegment Context
|
|
|
40 ContextIsDataSegment = record {get = (\c @$\rightarrow$@ c) ; set = (\_ c @$\rightarrow$@ c)}
|
|
|
41
|
|
|
42
|
|
|
43 record Meta : Set@$\_{1}$@ where
|
|
|
44 field
|
|
|
45 -- context as set of data segments
|
|
|
46 context : Context
|
|
|
47 stack : SingleLinkedStack A
|
|
|
48 nextCS : N.CodeSegment Context Context
|
|
|
49
|
|
|
50
|
|
|
51
|
|
|
52
|
|
|
53 open import subtype Meta as M
|
|
|
54
|
|
|
55 instance
|
|
|
56 MetaIncludeContext : M.DataSegment Context
|
|
|
57 MetaIncludeContext = record { get = Meta.context
|
|
|
58 ; set = (\m c @$\rightarrow$@ record m {context = c}) }
|
|
|
59
|
|
|
60 MetaIsMetaDataSegment : M.DataSegment Meta
|
|
|
61 MetaIsMetaDataSegment = record { get = (\m @$\rightarrow$@ m) ; set = (\_ m @$\rightarrow$@ m) }
|
|
|
62
|
|
|
63
|
|
|
64 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ M.CodeSegment X Y
|
|
|
65 liftMeta (N.cs f) = M.cs f
|
|
|
66
|
|
|
67 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} @$\rightarrow$@ N.CodeSegment X Y @$\rightarrow$@ N.CodeSegment Context Context
|
|
|
68 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c @$\rightarrow$@ N.DataSegment.set y c (f (N.DataSegment.get x c)))
|
|
|
69
|
|
|
70 -- definition based from Gears(209:5708390a9d88) src/parallel_execution
|
|
|
71
|
|
|
72 emptySingleLinkedStack : SingleLinkedStack A
|
|
|
73 emptySingleLinkedStack = record {top = nothing}
|
|
|
74
|
|
|
75
|
|
|
76 pushSingleLinkedStack : Meta @$\rightarrow$@ Meta
|
|
|
77 pushSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (push s e) })
|
|
|
78 where
|
|
|
79 n = Meta.nextCS m
|
|
|
80 s = Meta.stack m
|
|
|
81 e = Context.element (Meta.context m)
|
|
|
82 push : SingleLinkedStack A @$\rightarrow$@ Maybe A @$\rightarrow$@ SingleLinkedStack A
|
|
|
83 push s nothing = s
|
|
|
84 push s (just x) = record {top = just (cons x (top s))}
|
|
|
85
|
|
|
86
|
|
|
87
|
|
|
88 popSingleLinkedStack : Meta @$\rightarrow$@ Meta
|
|
|
89 popSingleLinkedStack m = M.exec (liftMeta n) (record m {stack = (st m) ; context = record con {element = (elem m)}})
|
|
|
90 where
|
|
|
91 n = Meta.nextCS m
|
|
|
92 con = Meta.context m
|
|
|
93 elem : Meta @$\rightarrow$@ Maybe A
|
|
|
94 elem record {stack = record { top = (just (cons x _)) }} = just x
|
|
|
95 elem record {stack = record { top = nothing }} = nothing
|
|
|
96 st : Meta @$\rightarrow$@ SingleLinkedStack A
|
|
|
97 st record {stack = record { top = (just (cons _ s)) }} = record {top = s}
|
|
|
98 st record {stack = record { top = nothing }} = record {top = nothing}
|
|
|
99
|
|
|
100
|
|
|
101
|
|
|
102
|
|
|
103 pushSingleLinkedStackCS : M.CodeSegment Meta Meta
|
|
|
104 pushSingleLinkedStackCS = M.cs pushSingleLinkedStack
|
|
|
105
|
|
|
106 popSingleLinkedStackCS : M.CodeSegment Meta Meta
|
|
|
107 popSingleLinkedStackCS = M.cs popSingleLinkedStack
|
|
|
108
|
|
|
109
|
|
|
110 -- for sample
|
|
|
111
|
|
|
112 firstContext : Context
|
|
|
113 firstContext = record {element = nothing ; n = 0}
|
|
|
114
|
|
|
115
|
|
|
116 firstMeta : Meta
|
|
|
117 firstMeta = record { context = firstContext
|
|
|
118 ; stack = emptySingleLinkedStack
|
|
|
119 ; nextCS = (N.cs (\m @$\rightarrow$@ m))
|
|
|
120 }
|
|
|
121
|
|
|
122
|
|
|
123
|
