Project

General

Profile

Revision 3769b712 src/tools/stateflow/semantics/cPS_lustre_generator.ml

View differences:

src/tools/stateflow/semantics/cPS_lustre_generator.ml
14 14
  include TransformerStub
15 15

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

  
20 20
	
......
31 31
  let pp_path prefix fmt path =
32 32
    Format.fprintf fmt "%s%t"
33 33
      prefix
34
      (fun fmt -> Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
34
      (fun fmt -> Lustrec.Utils.fprintf_list ~sep:"_" Format.pp_print_string fmt path)
35 35

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

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

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

  
59 59
  let var_to_vdecl ?(prefix="") var typ = mkvar (var_to_ident prefix var) typ 
60 60
  let state_vars_to_vdecl_list ?(prefix="") vars =
61
    let bool_type = Corelang.mktyp Location.dummy_loc Lustre_types.Tydec_bool in
61
    let bool_type = Lustrec.Corelang.mktyp Lustrec.Location.dummy_loc Lustrec.Lustre_types.Tydec_bool in
62 62
    List.map 
63 63
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
64 64
      (ActiveStates.Vars.elements vars)
......
69 69
    ) locs []
70 70
     (* TODO: declare global vars *)
71 71

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

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

  
98 98
  let vars_to_exprl ?(prefix="") vars =
99 99
    List.map
......
103 103

  
104 104
  (* Events *)
105 105
  let event_type_decl =
106
    Corelang.mktop
106
    Lustrec.Corelang.mktop
107 107
      (
108
	Lustre_types.TypeDef {
109
	  Lustre_types.tydef_id = "event_type";
110
	  tydef_desc = Lustre_types.Tydec_int
108
	Lustrec.Lustre_types.TypeDef {
109
	  Lustrec.Lustre_types.tydef_id = "event_type";
110
	  tydef_desc = Lustrec.Lustre_types.Tydec_int
111 111
	}
112 112
      )
113 113
    
114 114
  let event_type = {
115
    Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
116
    Lustre_types.ty_dec_loc = Location.dummy_loc;
115
    Lustrec.Lustre_types.ty_dec_desc = Lustrec.Lustre_types.Tydec_const "event_type";
116
    Lustrec.Lustre_types.ty_dec_loc = Lustrec.Location.dummy_loc;
117 117
  }
118 118
    
119 119
  let event_var = mkvar "event" event_type 
......
135 135
    ActiveStates.Vars.empty,
136 136
    (
137 137
      (* Nothing happen here: out_vars = in_vars *)
138
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
138
      let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in 
139 139
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
140 140
    )
141 141
      
......
183 183
    fun sin sout call arg ->
184 184
      pp_name call arg;
185 185
      let funname = Format.flush_str_formatter () in
186
      let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
186
      let args = (Lustrec.Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
187 187
      let rhs = mkpredef_call funname args in
188 188
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
189 189
	
......
207 207
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool true) in
208 208
       (* eq2: sout_xx = sin_xx *)
209 209
       let expr_list = vars_to_exprl ~prefix:sin vars' in
210
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
210
       let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in 
211 211
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
212 212
	 {
213 213
	   statements = [
214
	     Lustre_types.Eq (eq1);
215
	     Lustre_types.Eq (eq2);
214
	     Lustrec.Lustre_types.Eq (eq1);
215
	     Lustrec.Lustre_types.Eq (eq2);
216 216
	   ];
217 217
	   assert_false = false
218 218
	 }
......
223 223
       let eq1 = mkeq ([var_to_ident sout p] , expr_of_bool false) in
224 224
       (* eq2: sout_xx = sin_xx *)
225 225
       let expr_list = vars_to_exprl ~prefix:sin vars' in
226
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
226
       let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in 
227 227
       let eq2 = mkeq (vars_to_ident_list ~prefix:sout vars', rhs) in
228 228
	 {
229 229
	   statements = [
230
	     Lustre_types.Eq (eq1);
231
	     Lustre_types.Eq (eq2);
230
	     Lustrec.Lustre_types.Eq (eq1);
231
	     Lustrec.Lustre_types.Eq (eq2);
232 232
	   ];
233 233
	   assert_false = false
234 234
	 }
235 235

  
236 236
    | Action.Nil         ->
237 237
       let expr_list = vars_to_exprl ~prefix:sin Vars.state_vars in
238
       let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
238
       let rhs = mkexpr (Lustrec.Lustre_types.Expr_tuple expr_list) in 
239 239
       mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
240 240
	 
241 241
  let eval_act kenv (action : act_t) =
......
250 250
    | Condition.Active p           -> var_to_expr ~prefix:sin p
251 251
    | Condition.Event e            ->
252 252
       mkpredef_call "=" [
253
	 Corelang.expr_of_vdecl event_var;
254
	 mkexpr (Lustre_types.Expr_const (Lustre_types.Const_int (get_event_const e)))
253
	 Lustrec.Corelang.expr_of_vdecl event_var;
254
	 mkexpr (Lustrec.Lustre_types.Expr_const (Lustrec.Lustre_types.Const_int (get_event_const e)))
255 255
       ]
256 256
    | Condition.Neg cond           -> mkpredef_call "not" [mkcond' sin cond]
257 257
    | Condition.And (cond1, cond2) -> mkpredef_call "&&" [mkcond' sin cond1;
......
259 259
    | Condition.Quote c            -> c.expr (* TODO: shall we prefix with sin ? *)
260 260

  
261 261
  let rec eval_cond condition (ok:t) ko sin sout =
262
    let open Lustre_types in
263
    let loc = Location.dummy_loc in
262
    let open Lustrec.Lustre_types in
263
    let loc = Lustrec.Location.dummy_loc in
264 264
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
265 265
    let (vars1, tr1) = ok sin sout in
266 266
    let (vars2, tr2) = ko sin sout in
......
275 275
	     (loc, mkcond' sin (Condition.Neg condition), true (* restart *), "NotCond_" ^ aut);
276 276
	   ]
277 277
	   in
278
	   Automata.mkhandler
278
	   Lustrec.Automata.mkhandler
279 279
	     loc                                      (* location *)
280 280
	     ("CenterPoint_" ^ aut)                   (* state name *)
281 281
	     handler_default_mode_unless              (* unless *)
......
288 288
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
289 289
       	   ]
290 290
	   in
291
	   Automata.mkhandler
291
	   Lustrec.Automata.mkhandler
292 292
	     loc                                      (* location *)
293 293
	     ("Cond_" ^ aut)                          (* state name *)
294 294
	     []                                       (* unless *)
......
301 301
	     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
302 302
       	   ]
303 303
	   in
304
	   Automata.mkhandler
304
	   Lustrec.Automata.mkhandler
305 305
	     loc                                      (* location *)
306 306
	     ("NotCond_" ^ aut)                       (* state name *)
307 307
	     []                                       (* unless *)
......
310 310
	     (tr2.statements, base_to_assert tr2, []) (* stmts, asserts, annots *)
311 311
	 in
312 312
	 let handlers = [ handler_default_mode; handler_cond_mode; handler_notcond_mode ] in
313
	 Aut (Automata.mkautomata loc aut handlers)
313
	 Aut (Lustrec.Automata.mkautomata loc aut handlers)
314 314
       ];
315 315
       assert_false = false
316 316
     }
......
321 321
    in tr 
322 322
    
323 323
  let mkcomponent :
324
  type c. c call_t -> c -> t -> Lustre_types.program_t =
324
  type c. c call_t -> c -> t -> Lustrec.Lustre_types.program_t =
325 325
    fun call args ->
326 326
      fun tr ->
327 327
	reset_loc ();
......
331 331
	let inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars in
332 332
	let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
333 333
	let node =
334
	  Corelang.mktop (	
335
	    Lustre_types.Node {Lustre_types.node_id = funname;
336
			   node_type = Types.new_var ();
337
			   node_clock = Clocks.new_var true;
334
	  Lustrec.Corelang.mktop (	
335
	    Lustrec.Lustre_types.Node {Lustrec.Lustre_types.node_id = funname;
336
			   node_type = Lustrec.Types.new_var ();
337
			   node_clock = Lustrec.Clocks.new_var true;
338 338
			   node_inputs = inputs;
339 339
			   node_outputs = outputs;
340 340
			   node_locals = mk_locals vars'; (* TODO: add global vars *)
......
364 364

  
365 365
	  
366 366
  let mk_main_loop () =
367
    (* let loc = Location.dummy_loc in *)
367
    (* let loc = Lustrec.Location.dummy_loc in *)
368 368
    
369 369
    let call_stmt =
370 370
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
......
373 373
	  List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
374 374
	let init_globals =
375 375
	  List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
376
	mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))
376
	mkexpr (Lustrec.Lustre_types.Expr_tuple (init_state_false @ init_globals))
377 377
      in
378
      let args = (Corelang.expr_of_vdecl event_var)::
378
      let args = (Lustrec.Corelang.expr_of_vdecl event_var)::
379 379
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
380 380
      in
381 381
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
382
      let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in
383
      let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in
382
      let pre_call_expr = mkexpr (Lustrec.Lustre_types.Expr_pre (call_expr)) in
383
      let rhs = mkexpr (Lustrec.Lustre_types.Expr_arrow (init, pre_call_expr)) in
384 384
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
385 385
    in
386
    let inputs = List.map Corelang.copy_var_decl [event_var] in
386
    let inputs = List.map Lustrec.Corelang.copy_var_decl [event_var] in
387 387
    let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
388 388
    (* TODO add the globals as sout_data_x entry values *)
389 389
    let node_principal =
390
      Corelang.mktop (	
391
	Lustre_types.Node {Lustre_types.node_id = "principal_loop";
392
			 node_type = Types.new_var ();
393
			 node_clock = Clocks.new_var true;
390
      Lustrec.Corelang.mktop (	
391
	Lustrec.Lustre_types.Node {Lustrec.Lustre_types.node_id = "principal_loop";
392
			 node_type = Lustrec.Types.new_var ();
393
			 node_clock = Lustrec.Clocks.new_var true;
394 394
			 node_inputs = inputs;
395 395
			 node_outputs = outputs;
396 396
			 node_locals = []; (* TODO: add global vars *)

Also available in: Unified diff