1
|
open Basetypes
|
2
|
open Datatype
|
3
|
(* open ActiveEnv *)
|
4
|
open CPS_transformer
|
5
|
(* open Simulink *)
|
6
|
open Theta
|
7
|
|
8
|
module Interpreter (Transformer : TransformerType) =
|
9
|
struct
|
10
|
module KT = KenvTheta (Transformer)
|
11
|
open KT
|
12
|
|
13
|
let ( >? ) cond tr =
|
14
|
if cond then tr else Transformer.null
|
15
|
|
16
|
module type DenotationType =
|
17
|
sig
|
18
|
module Theta : MemoThetaType
|
19
|
|
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
|
24
|
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
|
26
|
end
|
27
|
|
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
|
36
|
end
|
37
|
|
38
|
module AbstractKenv (Denot : functor (Kenv : KenvType) -> DenotationType) : AbsDenotationType =
|
39
|
struct
|
40
|
let eval_dest kenv =
|
41
|
let module Kenv =
|
42
|
struct
|
43
|
let kenv = kenv
|
44
|
end in
|
45
|
let module D = Denot (Kenv) in
|
46
|
D.eval_dest
|
47
|
|
48
|
let eval_tau kenv =
|
49
|
let module Kenv =
|
50
|
struct
|
51
|
let kenv = kenv
|
52
|
end in
|
53
|
let module D = Denot (Kenv) in
|
54
|
D.eval_tau
|
55
|
|
56
|
let eval_T kenv =
|
57
|
let module Kenv =
|
58
|
struct
|
59
|
let kenv = kenv
|
60
|
end in
|
61
|
let module D = Denot (Kenv) in
|
62
|
D.eval_T
|
63
|
|
64
|
let eval_C kenv =
|
65
|
let module Kenv =
|
66
|
struct
|
67
|
let kenv = kenv
|
68
|
end in
|
69
|
let module D = Denot (Kenv) in
|
70
|
D.eval_C
|
71
|
|
72
|
let eval_open_path kenv =
|
73
|
let module Kenv =
|
74
|
struct
|
75
|
let kenv = kenv
|
76
|
end in
|
77
|
let module D = Denot (Kenv) in
|
78
|
D.eval_open_path
|
79
|
|
80
|
let eval_S kenv =
|
81
|
let module Kenv =
|
82
|
struct
|
83
|
let kenv = kenv
|
84
|
end in
|
85
|
let module D = Denot (Kenv) in
|
86
|
D.eval_S
|
87
|
end
|
88
|
|
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
|
194
|
|
195
|
module type ProgType =
|
196
|
sig
|
197
|
val init : state_name_t
|
198
|
val defs : prog_t src_components_t list
|
199
|
end
|
200
|
|
201
|
module type EvaluationType =
|
202
|
sig
|
203
|
module Theta : ThetaType with type t = Transformer.t
|
204
|
val eval_prog : Transformer.t
|
205
|
val eval_components : 'c call_t -> ('c * Transformer.t) list
|
206
|
end
|
207
|
|
208
|
module Evaluation (Thetaify : ThetaifyType) (Prog : ProgType) : EvaluationType =
|
209
|
struct
|
210
|
module Denotation = Denotation (Thetaify)
|
211
|
module AbsDenotation = AbstractKenv (Denotation)
|
212
|
include AbsDenotation
|
213
|
|
214
|
module Kenv : KenvType =
|
215
|
struct
|
216
|
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
|
225
|
end
|
226
|
|
227
|
module AppDenotation = Denotation (Kenv)
|
228
|
module Theta = AppDenotation.Theta
|
229
|
|
230
|
let eval_components = Theta.components
|
231
|
|
232
|
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)
|
248
|
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
|
*)
|
287
|
end
|