Project

General

Profile

Download (13.7 KB) Statistics
| Branch: | Tag: | Revision:
1
open Lustrec
2
open Basetypes
3
open ActiveStates
4
open CPS_transformer
5

    
6
let ff = Format.fprintf 
7
       
8
module LustrePrinter (
9
  Vars : sig
10
    val state_vars : ActiveStates.Vars.t
11
    val global_vars : GlobalVarDef.t list
12

    
13
  end) : TransformerType =
14
struct
15
  include TransformerStub
16

    
17
  type name_t = string
18
  type t_base = { statements : Lustre_types.statement list; assert_false: bool }
19
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
20

    
21
	
22
  let new_loc, reset_loc =
23
    let cpt = ref 0 in
24
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
25
     (fun () -> cpt := 0))
26

    
27
  let new_aut, reset_aut =
28
    let cpt = ref 0 in
29
    ((fun () -> incr cpt; Format.sprintf "aut_%i" !cpt),
30
     (fun () -> cpt := 0))
31
      
32
  let pp_path prefix fmt path =
33
    Format.fprintf fmt "%s%t"
34
      prefix
35
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
36

    
37
  let pp_typed_path sin fmt path =
38
    Format.fprintf fmt "%a : bool" (pp_path sin) path
39

    
40
  let pp_vars sin fmt vars =
41
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:", " (pp_path sin) fmt (ActiveStates.Vars.elements vars))
42
  let pp_vars_decl sin fmt vars =
43
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
44
       
45
  let var_to_ident prefix p =
46
    pp_path prefix Format.str_formatter p;
47
    Format.flush_str_formatter ()
48

    
49
  let vars_to_ident_list ?(prefix="") vars =
50
    List.map (
51
      fun p -> var_to_ident prefix p
52
    ) (ActiveStates.Vars.elements vars)
53

    
54
  let mkvar name typ = 
55
    let loc = Location.dummy_loc in
56
    Corelang.mkvar_decl
57
      loc
58
      (name, typ, Corelang.mkclock loc Lustre_types.Ckdec_any, false, None, None (*"__no_parent__" *))
59

    
60
  let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
61
  let state_vars_to_vdecl_list ?(prefix="") vars =
62
    let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in
63
    List.map 
64
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
65
      (ActiveStates.Vars.elements vars)
66

    
67
  let mk_locals locs =
68
    ActiveStates.Vars.fold (fun v accu ->
69
      (state_vars_to_vdecl_list ~prefix:(List.hd v) Vars.state_vars)@accu
70
    ) locs []
71
     (* TODO: declare global vars *)
72

    
73
  let mkeq = Corelang.mkeq Location.dummy_loc
74
  let mkexpr = Corelang.mkexpr Location.dummy_loc
75
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
76
  let expr_of_bool b = mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))
77
  let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =
78
    { statements = [
79
      Lustre_types.Eq (
80
	mkeq (
81
	  vars_to_ident_list ~prefix:prefix_lhs lhs_vars, (* lhs *)
82
	  rhs (* rhs *)
83
	)
84
      )
85
      ];
86
      assert_false = false
87
    }
88
  let base_to_assert b =
89
    if b.assert_false then
90
      [{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
91
    else
92
      []
93

    
94
    
95
  let var_to_expr ?(prefix="") p =
96
    let id = var_to_ident prefix p in
97
    Corelang.expr_of_ident id Location.dummy_loc
98

    
99
  let vars_to_exprl ?(prefix="") vars =
100
    List.map
101
      (fun p -> var_to_expr ~prefix:prefix p)
102
      (ActiveStates.Vars.elements vars)
103

    
104

    
105
  (* Events *)
106
  let event_type_decl =
107
    Corelang.mktop
108
      (
109
	Lustre_types.TypeDef {
110
	  Lustre_types.tydef_id = "event_type";
111
	  tydef_desc = Lustre_types.Tydec_int
112
	}
113
      )
114
    
115
  let event_type = {
116
    Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
117
    Lustre_types.ty_dec_loc = Location.dummy_loc;
118
  }
119
    
120
  let event_var = mkvar "event" event_type 
121

    
122

    
123
  let const_map : (event_base_t, int) Hashtbl.t = Hashtbl.create 13
124
  let get_event_const e =
125
    try Hashtbl.find const_map e
126
    with Not_found -> (
127
      let nb = Hashtbl.length const_map in
128
      Hashtbl.add const_map e nb;
129
      nb	
130
    )
131

    
132

    
133
      
134
  let null sin sout =
135
    let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
136
    ActiveStates.Vars.empty,
137
    (
138
      (* Nothing happen here: out_vars = in_vars *)
139
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
140
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
141
    )
142
      
143
  let bot sin sout =
144
    let (vars, tr) = null sin sout in
145
    (
146
      ActiveStates.Vars.empty,
147
      { tr with assert_false = true }
148
    )
149
      
150
  let ( >> ) tr1 tr2 sin sout =
151
    let l = new_loc () in
152
    let (vars1, tr1) = tr1 sin l in
153
    let (vars2, tr2) = tr2 l sout in
154
    (ActiveStates.Vars.add [l] (ActiveStates.Vars.union vars1 vars2),
155
     {
156
       statements = tr1.statements @ tr2.statements;
157
       assert_false = tr1.assert_false || tr2.assert_false
158
     }
159
    )
160
      
161
  let pp_name :
162
  type c. c call_t  -> c -> unit =
163
    fun call -> 
164
      match call with
165
      | Ecall -> (fun (p, p', f) ->
166
	Format.fprintf Format.str_formatter "theta%a%a%a_%a"
167
	  pp_call call
168
	  (pp_path "_from_") p
169
	  (pp_path "_to_") p'
170
	  pp_frontier f)
171
      | Dcall -> (fun p          ->
172
	Format.fprintf Format.str_formatter "theta%a%a"
173
	  pp_call call
174
	  (pp_path "_from_") p)
175
      | Xcall -> (fun (p, f)     ->
176
	Format.fprintf Format.str_formatter "theta%a%a_%a"
177
	  pp_call call
178
	  (pp_path "_from_") p
179
	  pp_frontier f)
180
	     
181

    
182
  let mkcall' :
183
  type c. name_t -> name_t -> c call_t -> c -> t_base =
184
    fun sin sout call arg ->
185
      pp_name call arg;
186
      let funname = Format.flush_str_formatter () in
187
      let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
188
      let rhs = mkpredef_call funname args in
189
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
190
	
191
  let mkact' action sin sout =
192
    match action with
193
    | Action.Call (c, a) -> mkcall' sin sout c a
194
    | Action.Quote a     ->
195
        (* TODO: check. This seems to be innappropriate *)
196
        (* let funname = "action_" ^ a.ident in
197
	let args = vars_to_exprl ~prefix:sin Vars.state_vars in
198
	let rhs = mkpredef_call funname args in
199
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
200
	*)
201
       {
202
	 statements = a.defs;
203
	 assert_false = false
204
       }
205
    | Action.Open p      ->
206
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
207
       (* eq1: sout_p = true *)
208
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in
209
       (* eq2: sout_xx = sin_xx *)
210
       let expr_list = vars_to_exprl ~prefix:sin vars' in
211
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
212
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
213
	 {
214
	   statements = [
215
	     Lustre_types.Eq (eq1);
216
	     Lustre_types.Eq (eq2);
217
	   ];
218
	   assert_false = false
219
	 }
220
	 
221
    | Action.Close p     ->
222
       let vars' = ActiveStates.Vars.remove p Vars.state_vars in
223
       (* eq1: sout_p = false *)
224
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in
225
       (* eq2: sout_xx = sin_xx *)
226
       let expr_list = vars_to_exprl ~prefix:sin vars' in
227
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
228
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
229
	 {
230
	   statements = [
231
	     Lustre_types.Eq (eq1);
232
	     Lustre_types.Eq (eq2);
233
	   ];
234
	   assert_false = false
235
	 }
236

    
237
    | Action.Nil         ->
238
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
239
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
240
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
241
	 
242
  let eval_act kenv (action : act_t) =
243
    (*Format.printf "----- action = %a@." Action.pp_act action;*)
244
    (fun sin sout -> (ActiveStates.Vars.empty,
245
		      mkact' action sin sout   ))
246
       
247
  let rec mkcond' sin condition =
248
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
249
    match condition with
250
    | Condition.True               -> expr_of_bool true
251
    | Condition.Active p           -> var_to_expr ~prefix:sin p
252
    | Condition.Event e            ->
253
       mkpredef_call "=" [
254
	 Corelang.expr_of_vdecl event_var;
255
	 mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e)))
256
       ]
257
    | Condition.Neg cond           -> mkpredef_call "not" [mkcond' sin cond]
258
    | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1;
259
							  mkcond' sin cond2]
260
    | Condition.Quote c            -> c.expr (* TODO: shall we prefix with sin ? *)
261

    
262
  let rec eval_cond condition (ok:t) ko sin sout =
263
    let open Lustre_types in
264
    let loc = Location.dummy_loc in
265
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
266
    let (vars1, tr1) = ok sin sout in
267
    let (vars2, tr2) = ko sin sout in
268
    let (vars0, tr0) = bot sin sout in
269
    let aut = new_aut () in
270
    (ActiveStates.Vars.empty,
271
     {
272
       statements = [
273
	 let handler_default_mode =          	      (* Default mode : CenterPoint *)
274
	   let handler_default_mode_unless = [
275
	     (loc, mkcond' sin condition, true (* restart *), "Cond_" ^ aut);
276
	     (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);
277
	   ]
278
	   in
279
	   Automata.mkhandler
280
	     loc                                      (* location *)
281
	     ("CenterPoint_" ^ aut)                   (* state name *)
282
	     handler_default_mode_unless              (* unless *)
283
	     []                                       (* until *)
284
	     []                                       (* locals *)
285
	     (tr0.statements, base_to_assert tr0, []) (* stmts, asserts, annots *)
286
	 in
287
	 let handler_cond_mode =                       	 (* Cond mode *)
288
       	   let handler_cond_mode_until = [
289
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
290
       	   ]
291
	   in
292
	   Automata.mkhandler
293
	     loc                                      (* location *)
294
	     ("Cond_" ^ aut)                          (* state name *)
295
	     []                                       (* unless *)
296
	     handler_cond_mode_until                  (* until *)
297
	     (mk_locals vars1)                        (* locals *)
298
	     (tr1.statements, base_to_assert tr1, []) (* stmts, asserts, annots *)
299
	 in
300
	 let handler_notcond_mode =                       	 (* NotCond mode *)
301
       	   let handler_notcond_mode_until = [
302
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
303
       	   ]
304
	   in
305
	   Automata.mkhandler
306
	     loc                                      (* location *)
307
	     ("NotCond_" ^ aut)                       (* state name *)
308
	     []                                       (* unless *)
309
	     handler_notcond_mode_until               (* until *)
310
	     (mk_locals vars2)                        (* locals *)
311
	     (tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *)
312
	 in
313
	 let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in
314
	 Aut (Automata.mkautomata loc aut handlers)
315
       ];
316
       assert_false = false
317
     }
318
    )
319
      
320
  let mktransformer tr =
321
    let (vars, tr) = tr "sin_" "sout_"
322
    in tr 
323
    
324
  let mkcomponent :
325
  type c. c call_t -> c -> t -> Lustre_types.program_t =
326
    fun call args ->
327
      fun tr ->
328
	reset_loc ();
329
	let (vars', tr') = tr "sin_" "sout_" in
330
	pp_name call args;
331
	let funname = Format.flush_str_formatter () in
332
	let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in
333
	let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
334
	let node =
335
	  Corelang.mktop (	
336
	    Lustre_types.Node {Lustre_types.node_id = funname;
337
			   node_type = Types.new_var ();
338
			   node_clock = Clocks.new_var true;
339
			   node_inputs = inputs;
340
			   node_outputs = outputs;
341
			   node_locals = mk_locals vars'; (* TODO: add global vars *)
342
			   node_gencalls = [];
343
			   node_checks = [];
344
			   node_stmts = tr'.statements;
345
			   node_asserts = base_to_assert tr';
346
			   node_dec_stateless = false;
347
			   node_stateless = None;
348
			   node_spec = None;
349
			   node_annot = [];
350
                           node_iscontract = false}
351
      )  
352
	in
353
	[node]
354

    
355

    
356

    
357
	  (* TODO
358
	     C'est pas evident. 
359
Il faut faire les choses suivantes:
360
- rajouter dans un ensemble les variables manipulées localement
361
- on doit comprendre comment les variables globales sont injectées dans le modele final:
362
   - le node principal doit uniquement les afficher. Il peut les initialiser avec les valeurs init définies. Puis appeller la fcn thetacallD_from_principal.
363
   - elles peuvent/doivent etre dans input et output de ce node thetacallD
364
	  *)
365

    
366
	  
367
  let mk_main_loop () =
368
    (* let loc = Location.dummy_loc in *)
369
    
370
    let call_stmt =
371
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
372
      let init =
373
	let init_state_false =
374
	  List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
375
	let init_globals =
376
	  List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
377
	mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))
378
      in
379
      let args = (Corelang.expr_of_vdecl event_var)::
380
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
381
      in
382
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
383
      let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in
384
      let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in
385
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
386
    in
387
    let inputs = List.map Corelang.copy_var_decl [event_var] in
388
    let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
389
    (* TODO add the globals as sout_data_x entry values *)
390
    let node_principal =
391
      Corelang.mktop (	
392
	Lustre_types.Node {Lustre_types.node_id = "principal_loop";
393
			 node_type = Types.new_var ();
394
			 node_clock = Clocks.new_var true;
395
			 node_inputs = inputs;
396
			 node_outputs = outputs;
397
			 node_locals = []; (* TODO: add global vars *)
398
			 node_gencalls = [];
399
			 node_checks = [];
400
			 node_asserts = base_to_assert call_stmt; 
401
			 node_stmts = call_stmt.statements;
402
			 node_dec_stateless = false;
403
			 node_stateless = None;
404
			 node_spec = None;
405
			 node_annot = [];
406
                         node_iscontract = false;}
407
      )  
408
    in
409
    node_principal
410
    
411

    
412
  let mkprincipal tr =
413
    event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
414

    
415
end
416

    
417
(* Local Variables: *)
418
(* compile-command:"make -C ../../../.." *)
419
(* End: *)
(6-6/10)