1
|
open Basetypes
|
2
|
open Datatype
|
3
|
|
4
|
(* open ActiveEnv *)
|
5
|
open CPS_transformer
|
6
|
|
7
|
(* open Simulink *)
|
8
|
open Theta
|
9
|
|
10
|
module Interpreter (Transformer : TransformerType) = struct
|
11
|
module KT = KenvTheta (Transformer)
|
12
|
open KT
|
13
|
|
14
|
let ( >? ) cond tr = if cond then tr else Transformer.null
|
15
|
|
16
|
module type DenotationType = sig
|
17
|
module Theta : MemoThetaType
|
18
|
|
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
|
|
46
|
val eval_open_path : mode_t -> path_t -> path_t -> Transformer.t wrapper_t
|
47
|
|
48
|
val eval_S :
|
49
|
(path_t, 'b, Transformer.t) tag_t -> path_t -> state_def_t -> 'b
|
50
|
end
|
51
|
|
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
|
89
|
end
|
90
|
|
91
|
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) :
|
92
|
AbsDenotationType = struct
|
93
|
let eval_dest kenv =
|
94
|
let module Kenv = struct
|
95
|
let kenv = kenv
|
96
|
end in
|
97
|
let module D = Denot (Kenv) in
|
98
|
D.eval_dest
|
99
|
|
100
|
let eval_tau kenv =
|
101
|
let module Kenv = struct
|
102
|
let kenv = kenv
|
103
|
end in
|
104
|
let module D = Denot (Kenv) in
|
105
|
D.eval_tau
|
106
|
|
107
|
let eval_T kenv =
|
108
|
let module Kenv = struct
|
109
|
let kenv = kenv
|
110
|
end in
|
111
|
let module D = Denot (Kenv) in
|
112
|
D.eval_T
|
113
|
|
114
|
let eval_C kenv =
|
115
|
let module Kenv = struct
|
116
|
let kenv = kenv
|
117
|
end in
|
118
|
let module D = Denot (Kenv) in
|
119
|
D.eval_C
|
120
|
|
121
|
let eval_open_path kenv =
|
122
|
let module Kenv = struct
|
123
|
let kenv = kenv
|
124
|
end in
|
125
|
let module D = Denot (Kenv) in
|
126
|
D.eval_open_path
|
127
|
|
128
|
let eval_S kenv =
|
129
|
let module Kenv = struct
|
130
|
let kenv = kenv
|
131
|
end in
|
132
|
let module D = Denot (Kenv) in
|
133
|
D.eval_S
|
134
|
end
|
135
|
|
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
|
316
|
|
317
|
module type ProgType = sig
|
318
|
val init : state_name_t
|
319
|
|
320
|
val defs : prog_t src_components_t list
|
321
|
end
|
322
|
|
323
|
module type EvaluationType = sig
|
324
|
module Theta : ThetaType with type t = Transformer.t
|
325
|
|
326
|
val eval_prog : Transformer.t
|
327
|
|
328
|
val eval_components : 'c call_t -> ('c * Transformer.t) list
|
329
|
end
|
330
|
|
331
|
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) :
|
332
|
EvaluationType = struct
|
333
|
module Denotation = Denotation (Thetaify)
|
334
|
module AbsDenotation = AbstractKenv (Denotation)
|
335
|
include AbsDenotation
|
336
|
|
337
|
module Kenv : KenvType = struct
|
338
|
let kenv =
|
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
|
361
|
end
|
362
|
|
363
|
module AppDenotation = Denotation (Kenv)
|
364
|
module Theta = AppDenotation.Theta
|
365
|
|
366
|
let eval_components = Theta.components
|
367
|
|
368
|
let eval_prog =
|
369
|
Transformer.(
|
370
|
eval_cond
|
371
|
(active [ Prog.init ])
|
372
|
(Theta.theta D [ Prog.init ])
|
373
|
(Theta.theta E [ Prog.init ] [] Loose))
|
374
|
end
|
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 *)
|
407
|
end
|