Project

General

Profile

Revision 8446bf03 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 : LustreSpec.statement list; assert_false: bool }
17
  type t_base = { statements : Lustre_types.statement list; assert_false: bool }
18 18
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
19 19

  
20 20
	
......
54 54
    let loc = Location.dummy_loc in
55 55
    Corelang.mkvar_decl
56 56
      loc
57
      (name, typ, Corelang.mkclock loc LustreSpec.Ckdec_any, false, None, None (*"__no_parent__" *))
57
      (name, typ, Corelang.mkclock loc 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 LustreSpec.Tydec_bool in
61
    let bool_type = Corelang.mktyp Location.dummy_loc 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)
......
72 72
  let mkeq = Corelang.mkeq Location.dummy_loc
73 73
  let mkexpr = Corelang.mkexpr Location.dummy_loc
74 74
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
75
  let expr_of_bool b = mkexpr (LustreSpec.Expr_const (Corelang.const_of_bool b))
75
  let expr_of_bool b = mkexpr (Lustre_types.Expr_const (Corelang.const_of_bool b))
76 76
  let mkstmt_eq lhs_vars ?(prefix_lhs="") rhs =
77 77
    { statements = [
78
      LustreSpec.Eq (
78
      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
      [{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
89
      [{Lustre_types.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
90 90
    else
91 91
      []
92 92

  
......
105 105
  let event_type_decl =
106 106
    Corelang.mktop
107 107
      (
108
	LustreSpec.TypeDef {
109
	  LustreSpec.tydef_id = "event_type";
110
	  tydef_desc = LustreSpec.Tydec_int
108
	Lustre_types.TypeDef {
109
	  Lustre_types.tydef_id = "event_type";
110
	  tydef_desc = Lustre_types.Tydec_int
111 111
	}
112 112
      )
113 113
    
114 114
  let event_type = {
115
    LustreSpec.ty_dec_desc = LustreSpec.Tydec_const "event_type";
116
    LustreSpec.ty_dec_loc = Location.dummy_loc;
115
    Lustre_types.ty_dec_desc = Lustre_types.Tydec_const "event_type";
116
    Lustre_types.ty_dec_loc = 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 (LustreSpec.Expr_tuple expr_list) in 
138
      let rhs = mkexpr (Lustre_types.Expr_tuple expr_list) in 
139 139
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
140 140
    )
141 141
      
......
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 (LustreSpec.Expr_tuple expr_list) in 
210
       let rhs = mkexpr (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
	     LustreSpec.Eq (eq1);
215
	     LustreSpec.Eq (eq2);
214
	     Lustre_types.Eq (eq1);
215
	     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 (LustreSpec.Expr_tuple expr_list) in 
226
       let rhs = mkexpr (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
	     LustreSpec.Eq (eq1);
231
	     LustreSpec.Eq (eq2);
230
	     Lustre_types.Eq (eq1);
231
	     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 (LustreSpec.Expr_tuple expr_list) in 
238
       let rhs = mkexpr (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) =
......
251 251
    | Condition.Event e            ->
252 252
       mkpredef_call "=" [
253 253
	 Corelang.expr_of_vdecl event_var;
254
	 mkexpr (LustreSpec.Expr_const (LustreSpec.Const_int (get_event_const e)))
254
	 mkexpr (Lustre_types.Expr_const (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 LustreSpec in
262
    let open Lustre_types in
263 263
    let loc = Location.dummy_loc in
264 264
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
265 265
    let (vars1, tr1) = ok sin sout in
......
321 321
    in tr 
322 322
    
323 323
  let mkcomponent :
324
  type c. c call_t -> c -> t -> LustreSpec.program =
324
  type c. c call_t -> c -> t -> Lustre_types.program =
325 325
    fun call args ->
326 326
      fun tr ->
327 327
	reset_loc ();
......
332 332
	let outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars in
333 333
	let node =
334 334
	  Corelang.mktop (	
335
	    LustreSpec.Node {LustreSpec.node_id = funname;
335
	    Lustre_types.Node {Lustre_types.node_id = funname;
336 336
			   node_type = Types.new_var ();
337 337
			   node_clock = Clocks.new_var true;
338 338
			   node_inputs = inputs;
......
372 372
	  List.map (fun _ -> expr_of_bool false) (ActiveStates.Vars.elements Vars.state_vars) in
373 373
	let init_globals =
374 374
	  List.map (fun v -> v.GlobalVarDef.init_val) Vars.global_vars in
375
	mkexpr (LustreSpec.Expr_tuple (init_state_false @ init_globals))
375
	mkexpr (Lustre_types.Expr_tuple (init_state_false @ init_globals))
376 376
      in
377 377
      let args = (Corelang.expr_of_vdecl event_var)::
378 378
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
379 379
      in
380 380
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
381
      let pre_call_expr = mkexpr (LustreSpec.Expr_pre (call_expr)) in
382
      let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in
381
      let pre_call_expr = mkexpr (Lustre_types.Expr_pre (call_expr)) in
382
      let rhs = mkexpr (Lustre_types.Expr_arrow (init, pre_call_expr)) in
383 383
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
384 384
    in
385 385
    let inputs = List.map Corelang.copy_var_decl [event_var] in
......
387 387
    (* TODO add the globals as sout_data_x entry values *)
388 388
    let node_principal =
389 389
      Corelang.mktop (	
390
	LustreSpec.Node {LustreSpec.node_id = "principal_loop";
390
	Lustre_types.Node {Lustre_types.node_id = "principal_loop";
391 391
			 node_type = Types.new_var ();
392 392
			 node_clock = Clocks.new_var true;
393 393
			 node_inputs = inputs;

Also available in: Unified diff