Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
src/tools/stateflow/semantics/cPS_interpreter.ml | ||
---|---|---|
1 | 1 |
open Basetypes |
2 | 2 |
open Datatype |
3 |
|
|
3 | 4 |
(* open ActiveEnv *) |
4 | 5 |
open CPS_transformer |
6 |
|
|
5 | 7 |
(* open Simulink *) |
6 | 8 |
open Theta |
7 | 9 |
|
8 |
module Interpreter (Transformer : TransformerType) = |
|
9 |
struct |
|
10 |
module Interpreter (Transformer : TransformerType) = struct |
|
10 | 11 |
module KT = KenvTheta (Transformer) |
11 | 12 |
open KT |
12 | 13 |
|
13 |
let ( >? ) cond tr = |
|
14 |
if cond then tr else Transformer.null |
|
14 |
let ( >? ) cond tr = if cond then tr else Transformer.null |
|
15 | 15 |
|
16 |
module type DenotationType = |
|
17 |
sig |
|
16 |
module type DenotationType = sig |
|
18 | 17 |
module Theta : MemoThetaType |
19 | 18 |
|
20 |
val eval_dest : destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
21 |
val eval_tau : trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
22 |
val eval_T : transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
23 |
val eval_C : (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t |
|
19 |
val eval_dest : |
|
20 |
destination_t -> |
|
21 |
Transformer.t wrapper_t -> |
|
22 |
Transformer.t success_t -> |
|
23 |
Transformer.t fail_t -> |
|
24 |
Transformer.t |
|
25 |
|
|
26 |
val eval_tau : |
|
27 |
trans_t -> |
|
28 |
Transformer.t wrapper_t -> |
|
29 |
Transformer.t success_t -> |
|
30 |
Transformer.t fail_t -> |
|
31 |
Transformer.t |
|
32 |
|
|
33 |
val eval_T : |
|
34 |
transitions_t -> |
|
35 |
Transformer.t wrapper_t -> |
|
36 |
Transformer.t success_t -> |
|
37 |
Transformer.t fail_t -> |
|
38 |
Transformer.t |
|
39 |
|
|
40 |
val eval_C : |
|
41 |
(path_t, 'b, Transformer.t) tag_t -> |
|
42 |
path_t -> |
|
43 |
composition_t -> |
|
44 |
Transformer.t |
|
45 |
|
|
24 | 46 |
val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
25 |
val eval_S : (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
47 |
|
|
48 |
val eval_S : |
|
49 |
(path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
26 | 50 |
end |
27 | 51 |
|
28 |
module type AbsDenotationType = |
|
29 |
sig |
|
30 |
val eval_dest : kenv_t -> destination_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
31 |
val eval_tau : kenv_t -> trans_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
32 |
val eval_T : kenv_t -> transitions_t -> Transformer.t wrapper_t -> Transformer.t success_t -> Transformer.t fail_t -> Transformer.t |
|
33 |
val eval_C : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t |
|
34 |
val eval_open_path : kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
|
35 |
val eval_S : kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
52 |
module type AbsDenotationType = sig |
|
53 |
val eval_dest : |
|
54 |
kenv_t -> |
|
55 |
destination_t -> |
|
56 |
Transformer.t wrapper_t -> |
|
57 |
Transformer.t success_t -> |
|
58 |
Transformer.t fail_t -> |
|
59 |
Transformer.t |
|
60 |
|
|
61 |
val eval_tau : |
|
62 |
kenv_t -> |
|
63 |
trans_t -> |
|
64 |
Transformer.t wrapper_t -> |
|
65 |
Transformer.t success_t -> |
|
66 |
Transformer.t fail_t -> |
|
67 |
Transformer.t |
|
68 |
|
|
69 |
val eval_T : |
|
70 |
kenv_t -> |
|
71 |
transitions_t -> |
|
72 |
Transformer.t wrapper_t -> |
|
73 |
Transformer.t success_t -> |
|
74 |
Transformer.t fail_t -> |
|
75 |
Transformer.t |
|
76 |
|
|
77 |
val eval_C : |
|
78 |
kenv_t -> |
|
79 |
(path_t, 'b, Transformer.t) tag_t -> |
|
80 |
path_t -> |
|
81 |
composition_t -> |
|
82 |
Transformer.t |
|
83 |
|
|
84 |
val eval_open_path : |
|
85 |
kenv_t -> mode_t -> path_t -> path_t -> Transformer.t wrapper_t |
|
86 |
|
|
87 |
val eval_S : |
|
88 |
kenv_t -> (path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b |
|
36 | 89 |
end |
37 | 90 |
|
38 |
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
|
|
39 |
struct |
|
91 |
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : |
|
92 |
AbsDenotationType = struct
|
|
40 | 93 |
let eval_dest kenv = |
41 |
let module Kenv = |
|
42 |
struct |
|
43 |
let kenv = kenv |
|
44 |
end in |
|
94 |
let module Kenv = struct |
|
95 |
let kenv = kenv |
|
96 |
end in |
|
45 | 97 |
let module D = Denot (Kenv) in |
46 | 98 |
D.eval_dest |
47 | 99 |
|
48 | 100 |
let eval_tau kenv = |
49 |
let module Kenv = |
|
50 |
struct |
|
51 |
let kenv = kenv |
|
52 |
end in |
|
101 |
let module Kenv = struct |
|
102 |
let kenv = kenv |
|
103 |
end in |
|
53 | 104 |
let module D = Denot (Kenv) in |
54 | 105 |
D.eval_tau |
55 | 106 |
|
56 | 107 |
let eval_T kenv = |
57 |
let module Kenv = |
|
58 |
struct |
|
59 |
let kenv = kenv |
|
60 |
end in |
|
108 |
let module Kenv = struct |
|
109 |
let kenv = kenv |
|
110 |
end in |
|
61 | 111 |
let module D = Denot (Kenv) in |
62 | 112 |
D.eval_T |
63 | 113 |
|
64 | 114 |
let eval_C kenv = |
65 |
let module Kenv = |
|
66 |
struct |
|
67 |
let kenv = kenv |
|
68 |
end in |
|
115 |
let module Kenv = struct |
|
116 |
let kenv = kenv |
|
117 |
end in |
|
69 | 118 |
let module D = Denot (Kenv) in |
70 | 119 |
D.eval_C |
71 | 120 |
|
72 | 121 |
let eval_open_path kenv = |
73 |
let module Kenv = |
|
74 |
struct |
|
75 |
let kenv = kenv |
|
76 |
end in |
|
122 |
let module Kenv = struct |
|
123 |
let kenv = kenv |
|
124 |
end in |
|
77 | 125 |
let module D = Denot (Kenv) in |
78 | 126 |
D.eval_open_path |
79 | 127 |
|
80 | 128 |
let eval_S kenv = |
81 |
let module Kenv = |
|
82 |
struct |
|
83 |
let kenv = kenv |
|
84 |
end in |
|
129 |
let module Kenv = struct |
|
130 |
let kenv = kenv |
|
131 |
end in |
|
85 | 132 |
let module D = Denot (Kenv) in |
86 | 133 |
D.eval_S |
87 | 134 |
end |
88 | 135 |
|
89 |
module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> DenotationType = |
|
90 |
functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> |
|
91 |
struct |
|
92 |
module Theta = Thetaify (Kenv) |
|
93 |
|
|
94 |
let eval_dest dest wrapper success fail = |
|
95 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest); |
|
96 |
match dest with |
|
97 |
| DPath p -> wrapper p (success p) |
|
98 |
| DJunction j -> Theta.theta J j wrapper success fail |
|
99 |
|
|
100 |
let eval_tau trans wrapper success fail = |
|
101 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans); |
|
102 |
let success' p = |
|
103 |
Transformer.(success p >> eval_act (module Theta) trans.transition_act) |
|
104 |
in |
|
105 |
let cond = Transformer.(event trans.event && trans.condition) in |
|
106 |
Transformer.(eval_cond cond |
|
107 |
(eval_act (module Theta) trans.condition_act >> eval_dest trans.dest wrapper success' fail) |
|
108 |
fail.local) |
|
109 |
|
|
110 |
let rec eval_T tl wrapper success fail = |
|
111 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl); |
|
112 |
match tl with |
|
113 |
| [] -> fail.global |
|
114 |
| t::[] -> eval_tau t wrapper success fail |
|
115 |
| t::tl -> |
|
116 |
let fail' = { fail with local = eval_T tl wrapper success fail } in |
|
117 |
eval_tau t wrapper success fail' |
|
118 |
|
|
119 |
let frontier path = |
|
120 |
match path with |
|
121 |
| [] -> [], [] |
|
122 |
| t::q -> [t], q |
|
123 |
|
|
124 |
let rec eval_open_path mode p p1 p2 success_p2 = |
|
125 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " pp_mode mode pp_path p pp_path p1 pp_path p2); |
|
126 |
match frontier p1, frontier p2 with |
|
127 |
| ([x], ps), ([y], pd) when x = y -> eval_open_path mode (p@[x]) ps pd success_p2 |
|
128 |
| (x , _ ), (y , pd) -> |
|
129 |
match mode with |
|
130 |
| Outer -> (Transformer.(Theta.theta X (p@x) Loose >> success_p2 >> Theta.theta E (p@y) pd Loose)) |
|
131 |
| Inner -> (assert (x = []); |
|
132 |
Transformer.(Theta.theta X (p@x) Strict >> success_p2 >> Theta.theta E (p@y) pd Strict)) |
|
133 |
| Enter -> (assert (x = [] && y <> []); |
|
134 |
Transformer.( success_p2 >> Theta.theta E (p@y) pd Loose)) |
|
135 |
|
|
136 |
let rec eval_C : type a b. (a, b, Transformer.t) tag_t -> path_t -> composition_t -> Transformer.t = |
|
137 |
fun tag prefix comp -> |
|
138 |
match tag with |
|
139 |
| E -> Transformer.( |
|
140 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path prefix SF.pp_comp comp); |
|
141 |
match comp with |
|
142 |
| Or (_T, []) -> null |
|
143 |
| Or ([], [s0]) -> eval_open_path Enter prefix [] [s0] null |
|
144 |
| Or (_T, _S) -> let wrapper = eval_open_path Enter [] prefix in |
|
145 |
let success _p_d = null in |
|
146 |
eval_T _T wrapper success { local = bot; global = bot } |
|
147 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta E (prefix@[p]) [] Loose)) _S null |
|
148 |
) |
|
149 |
| D -> Transformer.( |
|
150 |
match comp with |
|
151 |
| Or (_T, []) -> null |
|
152 |
| Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta D (prefix@[p])) (eval_C D prefix (Or (_T, _S))) |
|
153 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta D (prefix@[p]))) _S null |
|
154 |
) |
|
155 |
| X -> Transformer.( |
|
156 |
match comp with |
|
157 |
| Or (_T, []) -> null |
|
158 |
| Or (_T, p::_S) -> eval_cond (active (prefix@[p])) (Theta.theta X (prefix@[p]) Loose) (eval_C X prefix (Or (_T, _S))) |
|
159 |
| And (_S) -> List.fold_right (fun p -> (>>) (Theta.theta X (prefix@[p]) Loose)) _S null |
|
160 |
) |
|
161 |
| J -> assert false |
|
162 |
|
|
163 |
let eval_S : type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b = |
|
164 |
fun tag p p_def -> |
|
165 |
match tag with |
|
166 |
| E -> fun path frontier -> Transformer.( |
|
167 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag pp_path p pp_path path pp_frontier frontier); |
|
168 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.entry_act >> eval_act (module Theta) (open_path p))) >> |
|
169 |
match path with |
|
170 |
| [] -> eval_C E p p_def.internal_composition |
|
171 |
| s::path_tl -> Theta.theta E (p@[s]) path_tl Loose |
|
172 |
) |
|
173 |
| D -> Transformer.( |
|
174 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path p); |
|
175 |
let wrapper_i = eval_open_path Inner [] p in |
|
176 |
let wrapper_o = eval_open_path Outer [] p in |
|
177 |
let success _p_d = null in |
|
178 |
let fail_o = |
|
179 |
let fail_i = |
|
180 |
let same_fail_C = eval_C D p p_def.internal_composition in |
|
181 |
{ local = same_fail_C; global = same_fail_C } |
|
182 |
in |
|
183 |
let same_fail_i = eval_act (module Theta) p_def.state_actions.during_act >> eval_T p_def.inner_trans wrapper_i success fail_i in |
|
184 |
{ local = same_fail_i; global = same_fail_i } |
|
185 |
in |
|
186 |
eval_T p_def.outer_trans wrapper_o success fail_o |
|
187 |
) |
|
188 |
| X -> fun frontier -> Transformer.( |
|
189 |
Log.report ~level:sf_level (fun fmt -> Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " pp_tag tag pp_path p pp_frontier frontier); |
|
190 |
eval_C X p p_def.internal_composition >> |
|
191 |
((frontier = Loose) >? (eval_act (module Theta) p_def.state_actions.exit_act >> eval_act (module Theta) (close_path p))) |
|
192 |
) |
|
193 |
end |
|
136 |
module Denotation : functor (Thetaify : ThetaifyType) (Kenv : KenvType) -> |
|
137 |
DenotationType = |
|
138 |
functor |
|
139 |
(Thetaify : ThetaifyType) |
|
140 |
(Kenv : KenvType) |
|
141 |
-> |
|
142 |
struct |
|
143 |
module Theta = Thetaify (Kenv) |
|
144 |
|
|
145 |
let eval_dest dest wrapper success fail = |
|
146 |
Log.report ~level:sf_level (fun fmt -> |
|
147 |
Format.fprintf fmt "@[<v 2>D[[%a]]@ " SF.pp_dest dest); |
|
148 |
match dest with |
|
149 |
| DPath p -> |
|
150 |
wrapper p (success p) |
|
151 |
| DJunction j -> |
|
152 |
Theta.theta J j wrapper success fail |
|
153 |
|
|
154 |
let eval_tau trans wrapper success fail = |
|
155 |
Log.report ~level:sf_level (fun fmt -> |
|
156 |
Format.fprintf fmt "@[<v 2>tau[[%a]]@ " SF.pp_trans trans); |
|
157 |
let success' p = |
|
158 |
Transformer.( |
|
159 |
success p >> eval_act (module Theta) trans.transition_act) |
|
160 |
in |
|
161 |
let cond = Transformer.(event trans.event && trans.condition) in |
|
162 |
Transformer.( |
|
163 |
eval_cond cond |
|
164 |
(eval_act (module Theta) trans.condition_act |
|
165 |
>> eval_dest trans.dest wrapper success' fail) |
|
166 |
fail.local) |
|
167 |
|
|
168 |
let rec eval_T tl wrapper success fail = |
|
169 |
Log.report ~level:sf_level (fun fmt -> |
|
170 |
Format.fprintf fmt "@[<v 2>T[[%a]]@ " SF.pp_transitions tl); |
|
171 |
match tl with |
|
172 |
| [] -> |
|
173 |
fail.global |
|
174 |
| [ t ] -> |
|
175 |
eval_tau t wrapper success fail |
|
176 |
| t :: tl -> |
|
177 |
let fail' = { fail with local = eval_T tl wrapper success fail } in |
|
178 |
eval_tau t wrapper success fail' |
|
179 |
|
|
180 |
let frontier path = match path with [] -> [], [] | t :: q -> [ t ], q |
|
181 |
|
|
182 |
let rec eval_open_path mode p p1 p2 success_p2 = |
|
183 |
Log.report ~level:sf_level (fun fmt -> |
|
184 |
Format.fprintf fmt |
|
185 |
"@[<v 2>open_path_rec[[mode %a, prefix %a, src %a, dst %a]]@ " |
|
186 |
pp_mode mode pp_path p pp_path p1 pp_path p2); |
|
187 |
match frontier p1, frontier p2 with |
|
188 |
| ([ x ], ps), ([ y ], pd) when x = y -> |
|
189 |
eval_open_path mode (p @ [ x ]) ps pd success_p2 |
|
190 |
| (x, _), (y, pd) -> ( |
|
191 |
match mode with |
|
192 |
| Outer -> |
|
193 |
Transformer.( |
|
194 |
Theta.theta X (p @ x) Loose |
|
195 |
>> success_p2 |
|
196 |
>> Theta.theta E (p @ y) pd Loose) |
|
197 |
| Inner -> |
|
198 |
assert (x = []); |
|
199 |
Transformer.( |
|
200 |
Theta.theta X (p @ x) Strict |
|
201 |
>> success_p2 |
|
202 |
>> Theta.theta E (p @ y) pd Strict) |
|
203 |
| Enter -> |
|
204 |
assert (x = [] && y <> []); |
|
205 |
Transformer.(success_p2 >> Theta.theta E (p @ y) pd Loose)) |
|
206 |
|
|
207 |
let rec eval_C : |
|
208 |
type a b. |
|
209 |
(a, b, Transformer.t) tag_t -> |
|
210 |
path_t -> |
|
211 |
composition_t -> |
|
212 |
Transformer.t = |
|
213 |
fun tag prefix comp -> |
|
214 |
match tag with |
|
215 |
| E -> ( |
|
216 |
Transformer.( |
|
217 |
Log.report ~level:sf_level (fun fmt -> |
|
218 |
Format.fprintf fmt "@[<v 2>C_%a[[%a, %a]]@ " pp_tag tag pp_path |
|
219 |
prefix SF.pp_comp comp); |
|
220 |
match comp with |
|
221 |
| Or (_T, []) -> |
|
222 |
null |
|
223 |
| Or ([], [ s0 ]) -> |
|
224 |
eval_open_path Enter prefix [] [ s0 ] null |
|
225 |
| Or (_T, _S) -> |
|
226 |
let wrapper = eval_open_path Enter [] prefix in |
|
227 |
let success _p_d = null in |
|
228 |
eval_T _T wrapper success { local = bot; global = bot } |
|
229 |
| And _S -> |
|
230 |
List.fold_right |
|
231 |
(fun p -> ( >> ) (Theta.theta E (prefix @ [ p ]) [] Loose)) |
|
232 |
_S null)) |
|
233 |
| D -> ( |
|
234 |
Transformer.( |
|
235 |
match comp with |
|
236 |
| Or (_T, []) -> |
|
237 |
null |
|
238 |
| Or (_T, p :: _S) -> |
|
239 |
eval_cond |
|
240 |
(active (prefix @ [ p ])) |
|
241 |
(Theta.theta D (prefix @ [ p ])) |
|
242 |
(eval_C D prefix (Or (_T, _S))) |
|
243 |
| And _S -> |
|
244 |
List.fold_right |
|
245 |
(fun p -> ( >> ) (Theta.theta D (prefix @ [ p ]))) |
|
246 |
_S null)) |
|
247 |
| X -> ( |
|
248 |
Transformer.( |
|
249 |
match comp with |
|
250 |
| Or (_T, []) -> |
|
251 |
null |
|
252 |
| Or (_T, p :: _S) -> |
|
253 |
eval_cond |
|
254 |
(active (prefix @ [ p ])) |
|
255 |
(Theta.theta X (prefix @ [ p ]) Loose) |
|
256 |
(eval_C X prefix (Or (_T, _S))) |
|
257 |
| And _S -> |
|
258 |
List.fold_right |
|
259 |
(fun p -> ( >> ) (Theta.theta X (prefix @ [ p ]) Loose)) |
|
260 |
_S null)) |
|
261 |
| J -> |
|
262 |
assert false |
|
263 |
|
|
264 |
let eval_S : |
|
265 |
type b. (path_t, b, Transformer.t) tag_t -> path_t -> state_def_t -> b |
|
266 |
= |
|
267 |
fun tag p p_def -> |
|
268 |
match tag with |
|
269 |
| E -> ( |
|
270 |
fun path frontier -> |
|
271 |
Transformer.( |
|
272 |
Log.report ~level:sf_level (fun fmt -> |
|
273 |
Format.fprintf fmt |
|
274 |
"@[<v 2>S_%a[[node %a, dest %a, frontier %a]]@ " pp_tag tag |
|
275 |
pp_path p pp_path path pp_frontier frontier); |
|
276 |
frontier = Loose |
|
277 |
>? (eval_act (module Theta) p_def.state_actions.entry_act |
|
278 |
>> eval_act (module Theta) (open_path p)) |
|
279 |
>> |
|
280 |
match path with |
|
281 |
| [] -> |
|
282 |
eval_C E p p_def.internal_composition |
|
283 |
| s :: path_tl -> |
|
284 |
Theta.theta E (p @ [ s ]) path_tl Loose)) |
|
285 |
| D -> |
|
286 |
Transformer.( |
|
287 |
Log.report ~level:sf_level (fun fmt -> |
|
288 |
Format.fprintf fmt "@[<v 2>S_%a[[node %a]]@ " pp_tag tag pp_path |
|
289 |
p); |
|
290 |
let wrapper_i = eval_open_path Inner [] p in |
|
291 |
let wrapper_o = eval_open_path Outer [] p in |
|
292 |
let success _p_d = null in |
|
293 |
let fail_o = |
|
294 |
let fail_i = |
|
295 |
let same_fail_C = eval_C D p p_def.internal_composition in |
|
296 |
{ local = same_fail_C; global = same_fail_C } |
|
297 |
in |
|
298 |
let same_fail_i = |
|
299 |
eval_act (module Theta) p_def.state_actions.during_act |
|
300 |
>> eval_T p_def.inner_trans wrapper_i success fail_i |
|
301 |
in |
|
302 |
{ local = same_fail_i; global = same_fail_i } |
|
303 |
in |
|
304 |
eval_T p_def.outer_trans wrapper_o success fail_o) |
|
305 |
| X -> |
|
306 |
fun frontier -> |
|
307 |
Transformer.( |
|
308 |
Log.report ~level:sf_level (fun fmt -> |
|
309 |
Format.fprintf fmt "@[<v 2>S_%a[[node %a, frontier %a]]@ " |
|
310 |
pp_tag tag pp_path p pp_frontier frontier); |
|
311 |
eval_C X p p_def.internal_composition |
|
312 |
>> (frontier = Loose |
|
313 |
>? (eval_act (module Theta) p_def.state_actions.exit_act |
|
314 |
>> eval_act (module Theta) (close_path p)))) |
|
315 |
end |
|
194 | 316 |
|
195 |
module type ProgType = |
|
196 |
sig |
|
317 |
module type ProgType = sig |
|
197 | 318 |
val init : state_name_t |
319 |
|
|
198 | 320 |
val defs : prog_t src_components_t list |
199 | 321 |
end |
200 | 322 |
|
201 |
module type EvaluationType = |
|
202 |
sig |
|
323 |
module type EvaluationType = sig |
|
203 | 324 |
module Theta : ThetaType with type t = Transformer.t |
325 |
|
|
204 | 326 |
val eval_prog : Transformer.t |
327 |
|
|
205 | 328 |
val eval_components : 'c call_t -> ('c * Transformer.t) list |
206 | 329 |
end |
207 | 330 |
|
208 |
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
|
|
209 |
struct |
|
331 |
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : |
|
332 |
EvaluationType = struct
|
|
210 | 333 |
module Denotation = Denotation (Thetaify) |
211 | 334 |
module AbsDenotation = AbstractKenv (Denotation) |
212 | 335 |
include AbsDenotation |
213 | 336 |
|
214 |
module Kenv : KenvType = |
|
215 |
struct |
|
337 |
module Kenv : KenvType = struct |
|
216 | 338 |
let kenv = |
217 |
List.fold_left ( |
|
218 |
fun accu d -> match d with |
|
219 |
| State (p, defp) -> { accu with cont_node = (p, ((fun kenv -> eval_S kenv E p defp), |
|
220 |
(fun kenv -> eval_S kenv D p defp), |
|
221 |
(fun kenv -> eval_S kenv X p defp)))::accu.cont_node } |
|
222 |
| Junction (j, defj) -> { accu with cont_junc = (j, (fun kenv -> eval_T kenv defj))::accu.cont_junc } |
|
223 |
| SFFunction _ -> accu |
|
224 |
) {cont_node = []; cont_junc = []} Prog.defs |
|
339 |
List.fold_left |
|
340 |
(fun accu d -> |
|
341 |
match d with |
|
342 |
| State (p, defp) -> |
|
343 |
{ |
|
344 |
accu with |
|
345 |
cont_node = |
|
346 |
( p, |
|
347 |
( (fun kenv -> eval_S kenv E p defp), |
|
348 |
(fun kenv -> eval_S kenv D p defp), |
|
349 |
fun kenv -> eval_S kenv X p defp ) ) |
|
350 |
:: accu.cont_node; |
|
351 |
} |
|
352 |
| Junction (j, defj) -> |
|
353 |
{ |
|
354 |
accu with |
|
355 |
cont_junc = (j, fun kenv -> eval_T kenv defj) :: accu.cont_junc; |
|
356 |
} |
|
357 |
| SFFunction _ -> |
|
358 |
accu) |
|
359 |
{ cont_node = []; cont_junc = [] } |
|
360 |
Prog.defs |
|
225 | 361 |
end |
226 | 362 |
|
227 | 363 |
module AppDenotation = Denotation (Kenv) |
... | ... | |
230 | 366 |
let eval_components = Theta.components |
231 | 367 |
|
232 | 368 |
let eval_prog = |
233 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [] Loose)) |
|
234 |
end |
|
235 |
(* |
|
236 |
module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType = |
|
237 |
struct |
|
238 |
include Denotation (Theta) |
|
239 |
|
|
240 |
let theta = |
|
241 |
let kenv = |
|
242 |
List.fold_left ( |
|
243 |
fun accu d -> match d with |
|
244 |
| State (p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node } |
|
245 |
| Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc } |
|
246 |
) {cont_node = []; cont_junc = []} Prog.defs |
|
247 |
in Obj.magic (fun tag -> theta_ify kenv tag) |
|
369 |
Transformer.( |
|
370 |
eval_cond |
|
371 |
(active [ Prog.init ]) |
|
372 |
(Theta.theta D [ Prog.init ]) |
|
373 |
(Theta.theta E [ Prog.init ] [] Loose)) |
|
248 | 374 |
end |
249 |
module Rec (Prog : ProgType) = |
|
250 |
struct |
|
251 |
module rec Theta : ThetaType = ThetaFix (Prog) (Theta) |
|
252 |
end |
|
253 |
|
|
254 |
module Eval (Prog : ProgType) : EvaluationType = |
|
255 |
struct |
|
256 |
module RecTheta = Rec (Prog) |
|
257 |
module Theta = RecTheta.Theta |
|
258 |
|
|
259 |
let eval_prog = |
|
260 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) |
|
261 |
end |
|
262 |
|
|
263 |
module Eval (Prog : ProgType) = |
|
264 |
struct |
|
265 |
module ThetaFunctor (Evaluation : EvaluationType) : ThetaType = |
|
266 |
struct |
|
267 |
let theta tag = (theta_ify Evaluation.kenv) tag |
|
268 |
end |
|
269 |
module EvaluationFunctor (Theta : ThetaType) : EvaluationType = |
|
270 |
struct |
|
271 |
include Denotation (Theta) |
|
272 |
|
|
273 |
let kenv = |
|
274 |
List.fold_left ( |
|
275 |
fun accu d -> match d with |
|
276 |
| State (p, defp) -> { accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp, eval_S X p defp))::accu.cont_node } |
|
277 |
| Junction (j, defj) -> { accu with cont_junc = (j, (eval_T defj))::accu.cont_junc } |
|
278 |
) {cont_node = []; cont_junc = []} Prog.defs |
|
279 |
|
|
280 |
let eval_prog = |
|
281 |
Transformer.(eval_cond (active [Prog.init]) (Theta.theta D [Prog.init]) (Theta.theta E [Prog.init] [])) |
|
282 |
end |
|
283 |
module rec Theta : ThetaType = ThetaFunctor (Evaluation) |
|
284 |
and Evaluation : EvaluationType = EvaluationFunctor (Theta) |
|
285 |
end |
|
286 |
*) |
|
375 |
(* module ThetaFix (Prog : ProgType) (Theta : ThetaType) : ThetaType = struct |
|
376 |
include Denotation (Theta) |
|
377 |
|
|
378 |
let theta = let kenv = List.fold_left ( fun accu d -> match d with | State |
|
379 |
(p, defp) -> { accu with cont_node = (p, (eval_S E p defp, eval_S D p defp, |
|
380 |
eval_S X p defp))::accu.cont_node } | Junction (j, defj) -> { accu with |
|
381 |
cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = []; |
|
382 |
cont_junc = []} Prog.defs in Obj.magic (fun tag -> theta_ify kenv tag) end |
|
383 |
module Rec (Prog : ProgType) = struct module rec Theta : ThetaType = |
|
384 |
ThetaFix (Prog) (Theta) end |
|
385 |
|
|
386 |
module Eval (Prog : ProgType) : EvaluationType = struct module RecTheta = |
|
387 |
Rec (Prog) module Theta = RecTheta.Theta |
|
388 |
|
|
389 |
let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D |
|
390 |
[Prog.init]) (Theta.theta E [Prog.init] [])) end |
|
391 |
|
|
392 |
module Eval (Prog : ProgType) = struct module ThetaFunctor (Evaluation : |
|
393 |
EvaluationType) : ThetaType = struct let theta tag = (theta_ify |
|
394 |
Evaluation.kenv) tag end module EvaluationFunctor (Theta : ThetaType) : |
|
395 |
EvaluationType = struct include Denotation (Theta) |
|
396 |
|
|
397 |
let kenv = List.fold_left ( fun accu d -> match d with | State (p, defp) -> |
|
398 |
{ accu with cont_node = (p, (fun kenv -> eval_S E p defp, eval_S D p defp, |
|
399 |
eval_S X p defp))::accu.cont_node } | Junction (j, defj) -> { accu with |
|
400 |
cont_junc = (j, (eval_T defj))::accu.cont_junc } ) {cont_node = []; |
|
401 |
cont_junc = []} Prog.defs |
|
402 |
|
|
403 |
let eval_prog = Transformer.(eval_cond (active [Prog.init]) (Theta.theta D |
|
404 |
[Prog.init]) (Theta.theta E [Prog.init] [])) end module rec Theta : |
|
405 |
ThetaType = ThetaFunctor (Evaluation) and Evaluation : EvaluationType = |
|
406 |
EvaluationFunctor (Theta) end *) |
|
287 | 407 |
end |
Also available in: Unified diff
reformatting