Mercurial > hg > Papers > 2020 > soto-midterm

comparison src/stack-subtype.agda @ 1:73127e0ab57c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
(none)
author soto@cr.ie.u-ryukyu.ac.jp
date Tue, 08 Sep 2020 18:38:08 +0900
parents
children
comparison
equal deleted inserted replaced
0:b919985837a3 1:73127e0ab57c
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 -> Maybe (Element a) -> Element a
13
14 datum : {a : Set} -> Element a -> a
15 datum (cons a _) = a
16
17 next : {a : Set} -> Element a -> 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 : ℕ
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 -> c) ; set = (\_ c -> c)}
41
42
43 record Meta : Set₁ 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 -> record m {context = c}) }
59
60 MetaIsMetaDataSegment : M.DataSegment Meta
61 MetaIsMetaDataSegment = record { get = (\m -> m) ; set = (\_ m -> m) }
62
63
64 liftMeta : {X Y : Set} {{_ : M.DataSegment X}} {{_ : M.DataSegment Y}} -> N.CodeSegment X Y -> M.CodeSegment X Y
65 liftMeta (N.cs f) = M.cs f
66
67 liftContext : {X Y : Set} {{_ : N.DataSegment X}} {{_ : N.DataSegment Y}} -> N.CodeSegment X Y -> N.CodeSegment Context Context
68 liftContext {{x}} {{y}} (N.cs f) = N.cs (\c -> 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 -> 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 -> Maybe A -> 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 -> 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 -> Maybe A
94 elem record {stack = record { top = (just (cons x _)) }} = just x
95 elem record {stack = record { top = nothing }} = nothing
96 st : Meta -> 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 -> m))
120 }
121
122
123