Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / tools / stateflow / src / semantics / CPS / cPS_transformer.ml @ 2de7fa82

History | View | Annotate | Download (16.8 KB)

1
open Basetypes
2
open ActiveStates
3

    
4
type mode_t =
5
  | Outer
6
  | Inner
7
  | Enter
8

    
9

    
10
type 't success_t = path_t -> 't
11
type 't fail_t = { local: 't; global: 't }
12
type 't wrapper_t = path_t -> 't -> 't
13

    
14
type ('a, 'b, 't) tag_t =
15
  | E : (path_t, path_t -> frontier_t -> 't, 't) tag_t
16
  | D : (path_t, 't, 't) tag_t
17
  | X : (path_t, frontier_t -> 't, 't) tag_t
18
  | J : (junction_name_t, 't wrapper_t -> 't success_t -> 't fail_t -> 't, 't) tag_t
19

    
20

    
21
type ('a, 'b, 't) theta_t = ('a, 'b, 't) tag_t -> 'a -> 'b
22

    
23
module type ThetaType =
24
sig
25
  type t
26
  val theta : ('a, 'b, t) theta_t
27
end
28

    
29
let pp_mode fmt mode =
30
  match mode with
31
  | Outer -> Format.fprintf fmt "Outer"
32
  | Inner -> Format.fprintf fmt "Inner"
33
  | Enter -> Format.fprintf fmt "Enter"
34

    
35

    
36
let pp_tag : type a b t. Format.formatter -> (a, b, t) tag_t -> unit =
37
  fun fmt tag ->
38
    match tag with
39
    | E -> Format.fprintf fmt "e"
40
    | D -> Format.fprintf fmt "d"
41
    | X -> Format.fprintf fmt "x"
42
    | J -> Format.fprintf fmt "j"
43

    
44
(*
45
module Proj1Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t1 =
46
struct
47
  type t = T.t1
48

    
49
  let f f1 = (f1, T.bot2)
50
  let s s1 p = (s1 p, T.bot2)
51
  let w w1 p (tr1, _) = (w1 p tr1, T.bot2)
52

    
53
  let theta : type a b. (a, b, t) theta_t =
54
    fun tag ->
55
    match tag with
56
    | E -> (fun p p' f     -> fst (Theta.theta E p p' f))
57
    | D -> (fun p          -> fst (Theta.theta D p))
58
    | X -> (fun p f        -> fst (Theta.theta X p f))
59
    | J -> (fun j w1 s1 f1 -> fst (Theta.theta J j (w w1) (s s1) (f f1)))
60
end
61

    
62
module Proj2Theta (T : sig type t1 val bot1 : t1 type t2 val bot2 : t2 end) (Theta : ThetaType with type t = T.t1 * T.t2) : ThetaType with type t = T.t2 =
63
struct
64
  type t = T.t2
65

    
66
  let f f2 = (T.bot1, f2)
67
  let s s2 p = (T.bot1, s2 p)
68
  let w w2 p (_, tr2) = (T.bot1, w2 p tr2)
69

    
70
  let theta : type a b. (a, b, t) theta_t =
71
    fun tag ->
72
    match tag with
73
    | E -> (fun p p' f     -> snd (Theta.theta E p p' f))
74
    | D -> (fun p          -> snd (Theta.theta D p))
75
    | X -> (fun p f        -> snd (Theta.theta X p f))
76
    | J -> (fun j w2 s2 f2 -> snd (Theta.theta J j (w w2) (s s2) (f f2)))
77
end
78
*)
79

    
80
module TransformerStub =
81
struct
82
  type act_t = Action.t
83
  type cond_t = Condition.t
84

    
85
  let nil = Action.nil
86
  let aquote = Action.aquote
87
  let open_path = Action.open_path
88
  let close_path = Action.close_path
89
  let call = Action.call
90
  let pp_act = Action.pp_act
91

    
92
  let cquote = Condition.cquote
93
  let tru = Condition.tru
94
  let event = Condition.event
95
  let active = Condition.active
96
  let ( && ) = Condition.( && )
97
  let neg = Condition.neg
98
  let pp_cond = Condition.pp_cond
99
end
100

    
101
module type TransformerType =
102
sig
103
  type act_t = Action.t
104
  type cond_t = Condition.t
105
  type t
106

    
107
  include ActionType with type t := act_t
108
  include ConditionType with type t := cond_t
109

    
110
  val null : t
111
  val bot : t
112
  val ( >> ) : t -> t -> t
113
  val eval_act : (module ThetaType with type t = t) -> act_t -> t
114
  val eval_cond : cond_t -> t -> t -> t
115
  val pp_transformer : Format.formatter -> t -> unit
116
  val pp_principal : Format.formatter -> t -> unit
117
  val pp_component : Format.formatter -> 'c call_t -> 'c -> t -> unit
118
end
119

    
120
module type ComparableTransformerType =
121
sig
122
  include TransformerType
123

    
124
  val ( == ) : t -> t -> bool
125
end
126
(*
127
module Pair (T1 : ComparableTransformerType) (T2 : TransformerType) : ComparableTransformerType with type t = T1.t * T2.t =
128
struct
129
  include TransformerStub
130

    
131
  type t = T1.t * T2.t
132

    
133
  module T =
134
  struct
135
    type t1 = T1.t
136
    type t2 = T2.t
137
    let bot1 = T1.bot
138
    let bot2 = T2.bot
139
  end
140

    
141
  let null = T1.null, T2.null
142

    
143
  let bot = T1.bot, T2.bot
144

    
145
  let ( >> ) (tr11, tr12) (tr21, tr22) =
146
    T1.(tr11 >> tr21), T2.(tr12 >> tr22)
147

    
148
  let eval_act theta action =
149
    let module Theta = (val theta : ThetaType with type t = T1.t * T2.t) in
150
    let theta1 = (module Proj1Theta (T) (Theta) : ThetaType with type t = T1.t) in
151
    let theta2 = (module Proj2Theta (T) (Theta) : ThetaType with type t = T2.t) in
152
    T1.eval_act theta1 action, T2.eval_act theta2 action
153

    
154
  let eval_cond cond (trt1, trt2) (tre1, tre2) =
155
    T1.eval_cond cond trt1 tre1, T2.eval_cond cond trt2 tre2
156

    
157
  let ( == ) (tr1, _) (tr2, _) = T1.(tr1 == tr2)
158

    
159
  let pp_transformer fmt (tr1, tr2) =
160
    Format.fprintf fmt "< %a , %a >" T1.pp_transformer tr1 T2.pp_transformer tr2
161

    
162
  let pp_principal fmt (tr1, tr2) =
163
    Format.fprintf fmt "< %a , %a >" T1.pp_principal tr1 T2.pp_principal tr2
164

    
165
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
166
    fun fmt call ->
167
    match call with
168
    | Ecall -> (fun c (tr1, tr2) ->
169
      Format.fprintf fmt "< %t , %t >"
170
	(fun fmt -> T1.pp_component fmt Ecall c tr1)
171
	(fun fmt -> T2.pp_component fmt Ecall c tr2))
172
    | Dcall -> (fun c (tr1, tr2) ->
173
      Format.fprintf fmt "< %t , %t >"
174
	(fun fmt -> T1.pp_component fmt Dcall c tr1)
175
	(fun fmt -> T2.pp_component fmt Dcall c tr2))
176
    | Xcall -> (fun c (tr1, tr2) ->
177
      Format.fprintf fmt "< %t , %t >"
178
	(fun fmt -> T1.pp_component fmt Xcall c tr1)
179
	(fun fmt -> T2.pp_component fmt Xcall c tr2))
180
end
181
*)
182
  
183
module Evaluator : TransformerType with type t = (event_t * bool ActiveStates.Env.t * base_action_t list -> event_t * bool ActiveStates.Env.t * base_action_t list ) =
184
struct
185
  include TransformerStub
186

    
187
  type env_t = event_t * bool ActiveStates.Env.t * base_action_t list (* Don't care for values yet *)
188
  type t = env_t -> env_t
189
 
190
  let null rho = rho
191
  let add_action a (evt, rho, al) = (evt, rho, al@[a]) (* not very efficient but
192
							  avoid to keep track of
193
							  action order *)
194
  let bot _ = assert false
195
 
196
  let ( >> ) tr1 tr2 = fun rho -> rho |> tr1 |> tr2
197

    
198
  let ( ?? ) b tr = if b then tr else null
199

    
200
  let eval_open p (evt, rho, al)  = (evt, ActiveStates.Env.add p true rho, al)
201
  let eval_close p (evt, rho, al) = (evt, ActiveStates.Env.add p false rho, al)
202
  let eval_call : type c. (module ThetaType with type t = t) -> c call_t -> c -> t =
203
    fun kenv ->
204
    let module Theta = (val kenv : ThetaType with type t = t) in	      
205
    fun call -> match call with
206
    | Ecall -> (fun (p, p', f) -> Theta.theta E p p' f)
207
    | Dcall -> (fun p          -> Theta.theta D p)
208
    | Xcall -> (fun (p, f)     -> Theta.theta X p f)
209

    
210
  let eval_act kenv action =
211
    (* Format.printf "----- action = %a@." Action.pp_act action; *)
212
    match action with
213
    | Action.Call (c, a)      -> eval_call kenv c a
214
    | Action.Quote a          -> add_action a
215
    | Action.Open p           -> eval_open p
216
    | Action.Close p          -> eval_close p
217
    | Action.Nil              -> null
218

    
219
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
220
  let rec eval_cond condition ok ko =
221
    (* Format.printf "----- cond = %a@." Condition.pp_cond condition; *)
222
    match condition with
223
    | Condition.True               -> ok
224
    | Condition.Active p           -> (fun ((evt, env, al) as rho) -> if ActiveStates.Env.find p env then ok rho else ko rho)
225
    | Condition.Event e            -> (fun ((evt, env, al) as rho) -> match evt with None -> ko rho | Some e' -> if e=e' then ok rho else ko rho)
226
    | Condition.Neg cond           -> eval_cond cond ko ok
227
    | Condition.And (cond1, cond2) -> eval_cond cond1 (eval_cond cond2 ok ko) ko
228
    | Condition.Quote c            -> add_action c >> ok (* invalid behavior but similar to the other: should evaluate condition *)
229

    
230
  let pp_transformer fmt tr =
231
    Format.fprintf fmt "<transformer>"
232

    
233
  let pp_principal fmt tr =
234
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
235

    
236
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
237
    fun fmt call -> match call with
238
    | Ecall -> (fun (p, p', f) tr ->
239
      Format.fprintf fmt "component %a(%a, %a, %a) =@.%a" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
240
    | Dcall -> (fun p tr ->
241
      Format.fprintf fmt "component %a(%a) =@.%a" pp_call call pp_path p pp_transformer tr)
242
    | Xcall -> (fun (p, f) tr ->
243
      Format.fprintf fmt "component %a(%a, %a) =@.%a" pp_call call pp_path p pp_frontier f pp_transformer tr)
244
end
245

    
246
module CodeGenerator : ComparableTransformerType =
247
struct
248
  include TransformerStub
249

    
250
  type t =
251
  | Bot
252
  | Act of act_t
253
  | Seq of t list
254
  | Ite of cond_t * t * t
255

    
256
  let null = Seq []
257

    
258
  let bot = Bot
259
 
260
  let ( >> ) tr1 tr2 =
261
    match tr1, tr2 with
262
    | Seq trl1, Seq trl2 -> Seq (trl1@trl2)
263
    | Seq trl1, _        -> Seq (trl1@[tr2])
264
    | _       , Seq trl2 -> Seq (tr1::trl2)
265
    | _                  -> Seq ([tr1;tr2])
266

    
267
  let rec ( == ) tr1 tr2 = tr1 = tr2
268

    
269
  let eval_act kenv (action : act_t) =
270
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
271
    Act action
272

    
273
  (*if (match trans.event with None -> true | _ -> e = trans.event) && trans.condition rho*)
274
  let rec eval_cond condition ok ko =
275
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
276
    Ite (condition, ok, ko)
277
    
278
  let rec pp_transformer fmt tr =
279
    match tr with
280
    | Bot           -> Format.fprintf fmt "bot"
281
    | Act a         ->
282
       Format.fprintf fmt "<%a>" pp_act a
283
    | Seq trl       ->
284
       Format.fprintf fmt "@[<v 0>%a@]"
285
	 (Utils.fprintf_list ~sep:";@ " pp_transformer)
286
	 trl
287
    | Ite (c, t, e) ->
288
       Format.fprintf fmt "@[<v 0>if %a@ @[<v 2>then@ %a@]@ @[<v 2>else@ %a@]@ endif@]" pp_cond c pp_transformer t pp_transformer e
289

    
290
  let pp_principal fmt tr =
291
    Format.fprintf fmt "principal =@.%a" pp_transformer tr
292
      
293
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
294
    fun fmt call -> match call with
295
    | Ecall -> (fun (p, p', f) tr ->
296
      Format.fprintf fmt "component %a(%a, %a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_path p' pp_frontier f pp_transformer tr)
297
    | Dcall -> (fun p tr ->
298
      Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
299
    | Xcall -> (fun (p, f) tr ->
300
      Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)
301
end
302

    
303
module LustrePrinter (Vars : sig val vars : ActiveStates.Vars.t end) : TransformerType =
304
struct
305
  include TransformerStub
306

    
307
  type name_t = string
308
  type t = name_t -> name_t -> (ActiveStates.Vars.t * (Format.formatter -> unit))
309

    
310
  let new_loc, reset_loc =
311
    let cpt = ref 0 in
312
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
313
     (fun () -> cpt := 0))
314

    
315
  let new_aut, reset_aut =
316
    let cpt = ref 0 in
317
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
318
     (fun () -> cpt := 0))
319
      
320
  let pp_path sin fmt path =
321
    Format.fprintf fmt "%s%t" sin (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
322

    
323
  let pp_typed_path sin fmt path =
324
    Format.fprintf fmt "%a : bool" (pp_path sin) path
325

    
326
  let pp_vars sin fmt vars =
327
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
328

    
329
  let pp_vars_decl sin fmt vars =
330
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
331

    
332
  let pp_locals fmt locs =
333
    ActiveStates.Vars.iter (fun v -> Format.fprintf fmt "%a;@ " (pp_vars_decl (List.hd v)) Vars.vars) locs
334

    
335
  let null sin sout =
336
    (ActiveStates.Vars.empty,
337
     fun fmt -> Format.fprintf fmt "(%a) = (%a);" (pp_vars sout) Vars.vars (pp_vars sin) Vars.vars)
338

    
339
  let bot sin sout =
340
    let (vars, tr) = null sin sout in
341
    (ActiveStates.Vars.empty,
342
     (fun fmt -> Format.fprintf fmt "assert false;@ %t" tr))
343
 
344
  let ( >> ) tr1 tr2 sin sout =
345
    let l = new_loc () in
346
    let (vars1, tr1) = tr1 sin l in
347
    let (vars2, tr2) = tr2 l sout in
348
    (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
349
     fun fmt -> Format.fprintf fmt "%t@ %t" tr1 tr2)
350

    
351
  let pp_call' : type c. name_t -> name_t -> Format.formatter -> c call_t -> c -> unit =
352
    fun sin sout fmt call ->
353
    match call with
354
    | Ecall -> (fun (p, p', f) ->
355
      Format.fprintf fmt "(%a) = theta%a%a%a_%a(event, %a);"
356
	(pp_vars sout) Vars.vars
357
	pp_call call
358
	(pp_path "_from_") p
359
	(pp_path "_to_") p'
360
	pp_frontier f
361
	(pp_vars sin) Vars.vars)
362
    | Dcall -> (fun p          ->
363
      Format.fprintf fmt "(%a) = theta%a%a(event, %a);"
364
	(pp_vars sout) Vars.vars
365
	pp_call call
366
	(pp_path "_from_") p
367
	(pp_vars sin) Vars.vars)
368
    | Xcall -> (fun (p, f)     ->
369
      Format.fprintf fmt "(%a) = theta%a%a_%a(event, %a);"
370
	(pp_vars sout) Vars.vars
371
	pp_call call
372
	(pp_path "_from_") p
373
	pp_frontier f
374
	(pp_vars sin) Vars.vars)
375

    
376
  let pp_act' action sin sout fmt =
377
    match action with
378
    | Action.Call (c, a) -> pp_call' sin sout fmt c a
379
    | Action.Quote a     -> Format.fprintf fmt "(%a) = (* %s *)(%a);" (pp_vars sout) Vars.vars a (pp_vars sin) Vars.vars
380
    | Action.Open p      -> let vars' = ActiveStates.Vars.remove p Vars.vars in
381
			    Format.fprintf fmt "%a = true;@ (%a) = (%a);" (pp_path sout) p (pp_vars sout) vars' (pp_vars sin) vars'
382
    | Action.Close p     -> let vars' = ActiveStates.Vars.remove p Vars.vars in
383
			    Format.fprintf fmt "%a = false;@ (%a) = (%a);" (pp_path sout) p (pp_vars sout) vars' (pp_vars sin) vars'
384
    | Action.Nil         -> Format.fprintf fmt "(%a) = (%a);" (pp_vars sout) Vars.vars (pp_vars sin) Vars.vars
385

    
386
  let eval_act kenv (action : act_t) =
387
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
388
    (fun sin sout -> (ActiveStates.Vars.empty, pp_act' action sin sout))
389
       
390
  let rec pp_cond' sin fmt condition =
391
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
392
    match condition with
393
    | Condition.True               -> Format.fprintf fmt "true"
394
    | Condition.Active p           -> Format.fprintf fmt "%a" (pp_path sin) p
395
    | Condition.Event e            -> Format.fprintf fmt "(event = %s)" e
396
    | Condition.Neg cond           -> Format.fprintf fmt "not (%a)" (pp_cond' sin) cond
397
    | Condition.And (cond1, cond2) -> Format.fprintf fmt "%a && %a" (pp_cond' sin) cond1 (pp_cond' sin) cond2
398
    | Condition.Quote c            -> Format.fprintf fmt "(* %s *) true" c
399

    
400
  let rec eval_cond condition ok ko sin sout =
401
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
402
    let (vars1, tr1) = ok sin sout in
403
    let (vars2, tr2) = ko sin sout in
404
    let (vars0, tr0) = bot sin sout in
405
    let aut = new_aut () in
406
    (ActiveStates.Vars.empty,
407
     (fun fmt -> 
408
    Format.fprintf fmt "@[<v 1>automaton %s@ @[<v 2>state CenterPoint_%s:@ unless %a restart Cond_%s@ unless %a restart NotCond_%s@ let@ %t@ tel@]@ @[<v 2>state Cond_%s:@ %t%a@ let@ %t@ tel@ until true restart CenterPoint_%s@]@ @[<v 2>state NotCond_%s:@ %t%a@ let@ %t@ tel@ until true restart CenterPoint_%s@]@]"
409
      aut
410
      aut
411
      (pp_cond' sin) condition
412
      aut
413
      (pp_cond' sin) (Condition.Neg condition)
414
      aut
415
      tr0
416
      aut
417
      (fun fmt -> if ActiveStates.Vars.is_empty vars1 then () else Format.fprintf fmt "var@ ")
418
      pp_locals vars1
419
      tr1
420
      aut
421
      aut
422
      (fun fmt -> if ActiveStates.Vars.is_empty vars2 then () else Format.fprintf fmt "var@ ")
423
      pp_locals vars2
424
      tr2
425
      aut))
426

    
427
  let pp_transformer fmt tr =
428
    let (vars, tr) = tr "sin_" "sout_"
429
    in tr fmt
430

    
431
  let pp_component : type c. Format.formatter -> c call_t -> c -> t -> unit =
432
    fun fmt call -> match call with
433
    | Ecall -> (fun (p, p', f) tr ->
434
      reset_loc ();
435
      let (vars', tr') = tr "sin_" "sout_" in
436
      Format.fprintf fmt "node theta%a%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
437
	pp_call call
438
	(pp_path "_from_") p
439
	(pp_path "_to_") p'
440
	pp_frontier f
441
	(pp_vars_decl "sin_") Vars.vars
442
	(pp_vars_decl "sout_") Vars.vars
443
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
444
	pp_locals vars'
445
	tr')
446
    | Dcall -> (fun p tr ->
447
      reset_loc ();
448
      let (vars', tr') = tr "sin_" "sout_" in
449
      Format.fprintf fmt "node theta%a%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
450
	pp_call call
451
	(pp_path "_from_") p
452
	(pp_vars_decl "sin_") Vars.vars
453
	(pp_vars_decl "sout_") Vars.vars
454
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
455
	pp_locals vars'
456
	tr')
457
    | Xcall -> (fun (p, f) tr ->
458
      reset_loc ();
459
      let (vars', tr') = tr "sin_" "sout_" in
460
      Format.fprintf fmt "node theta%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
461
	pp_call call
462
	(pp_path "_from_") p
463
	pp_frontier f
464
	(pp_vars_decl "sin_") Vars.vars
465
	(pp_vars_decl "sout_") Vars.vars
466
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
467
	pp_locals vars'
468
	tr')
469

    
470
  let pp_main_loop fmt () =
471
    Format.fprintf fmt "type event_type = int;@.node principal_loop(event : event_type) returns (%a);@.let@.(%a) = (%t) -> pre (thetaCallD_from_principal (event, %a));@.tel@."
472
      (pp_vars_decl "sout_") Vars.vars
473
      (pp_vars "sout_") Vars.vars
474
      (fun fmt -> Utils.fprintf_list ~sep:", " (fun fmt _ -> Format.fprintf fmt "false") fmt (ActiveStates.Vars.elements Vars.vars))
475
      (pp_vars "sout_") Vars.vars
476

    
477
  let pp_principal fmt tr =
478
    Format.fprintf fmt "%a@.%a@."
479
      pp_main_loop ()
480
      (fun fmt -> pp_component fmt Dcall ["principal"]) tr
481

    
482
end