Project

General

Profile

Revision 69c96b6c

View differences:

src/modules.ml
162 162
       if ISet.mem basename imported then imported else
163 163
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
164 164
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
165
		 ) imported header
165
  ) imported header
166 166

  
167 167
let load_header imported header =
168 168
  try
......
187 187
       if ISet.mem basename imported then imported else
188 188
	 let lusic = import_dependency_aux decl.top_decl_loc (local, dep)
189 189
	 in load_header_rec (ISet.add basename imported) lusic.Lusic.contents
190
		 ) imported program
191

  
190
  ) imported program
191
    
192 192
let load_program imported program =
193 193
  try
194 194
    load_program_rec imported program
src/tools/stateflow/models/model_simple.ml
4 4
let name = "simple"
5 5

  
6 6
  let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
7

  
7
  let action _ = no_action
8 8
 
9 9
let model : prog_t =
10 10
    let state_main = "main" in
src/tools/stateflow/models/model_stopwatch.ml
3 3
open SF
4 4

  
5 5
let verbose = false
6
let actionv x = if verbose then action x else no_action
6
let actionv x = no_action (*TODO if verbose then action x else no_action*)
7
let action x = no_action (* TODO *)
7 8
let condition x = condition (Corelang.mkexpr Location.dummy_loc (LustreSpec.Expr_const (Corelang.const_of_bool true)))
8 9
    
9 10
let name = "stopwatch"
src/tools/stateflow/semantics/cPS.ml
40 40
  let module Eval = (val (eval modular)) in
41 41
  Eval.eval_prog 
42 42
    
43
let code_gen fmt modular  =
43
let code_gen modular  =
44 44
  let module Eval = (val (eval modular)) in
45 45
  let principal, components =  Eval.eval_prog, Eval.eval_components in
46
  [
47
    List.map (fun (c, tr) -> T.mkcomponent Ecall c tr) (components Ecall);
48
    List.map (fun (c, tr) -> T.mkcomponent Dcall c tr) (components Dcall);
49
    List.map (fun (c, tr) -> T.mkcomponent Xcall c tr) (components Xcall);
50
    T.mkprincipal principal;
51
  ]
46
  List.flatten (List.map (fun (c, tr) -> T.mkcomponent Ecall c tr) (components Ecall))@
47
    List.flatten (List.map (fun (c, tr) -> T.mkcomponent Dcall c tr) (components Dcall))@
48
    List.flatten (List.map (fun (c, tr) -> T.mkcomponent Xcall c tr) (components Xcall))@
49
    (T.mkprincipal principal)
52 50
end
src/tools/stateflow/semantics/cPS_ccode_generator.ml
57 57
      Format.fprintf fmt "component %a(%a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_transformer tr)
58 58
    | Xcall -> (fun (p, f) tr ->
59 59
      Format.fprintf fmt "component %a(%a, %a) =@.@[<v 2>begin@ %a@]@.end" pp_call call pp_path p pp_frontier f pp_transformer tr)
60

  
61
		     let mkcomponent _  = assert false
62
		     let mkprincipal _  = assert false
63
		     let mktransformer _  = assert false
64
		       
60 65
end
61 66

  
src/tools/stateflow/semantics/cPS_lustre_generator.ml
16 16
  type t_base = { statements : LustreSpec.statement list; assert_false: bool }
17 17
  type t = name_t -> name_t -> (ActiveStates.Vars.t * t_base)
18 18

  
19
	
19 20
  let new_loc, reset_loc =
20 21
    let cpt = ref 0 in
21 22
    ((fun () -> incr cpt; Format.sprintf "loc_%i" !cpt),
......
39 40
  let pp_vars_decl sin fmt vars =
40 41
    Format.fprintf fmt "%t" (fun fmt -> Utils.fprintf_list ~sep:"; " (pp_typed_path sin) fmt (ActiveStates.Vars.elements vars))
41 42

  
42
  let pp_locals fmt locs =
43
    ActiveStates.Vars.iter (fun v -> Format.fprintf fmt "%a;@ " (pp_vars_decl (List.hd v)) Vars.state_vars) locs;
44
    () (* TODO: declare global vars *)
45

  
46 43
  let var_to_ident prefix p =
47 44
    pp_path prefix Format.str_formatter p;
48 45
    Format.flush_str_formatter ()
......
65 62
      (fun v -> var_to_vdecl ~prefix:prefix v bool_type)
66 63
      (ActiveStates.Vars.elements vars)
67 64

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

  
68 71
  let mkeq = Corelang.mkeq Location.dummy_loc
69 72
  let mkexpr = Corelang.mkexpr Location.dummy_loc
70 73
  let mkpredef_call = Corelang.mkpredef_call Location.dummy_loc
......
80 83
      ];
81 84
      assert_false = false
82 85
    }
86
  let base_to_assert b =
87
    if b.assert_false then
88
      [{LustreSpec.assert_expr = expr_of_bool false; assert_loc = Location.dummy_loc}]
89
    else
90
      []
91

  
83 92
    
84 93
  let var_to_expr ?(prefix="") p =
85 94
    let id = var_to_ident prefix p in
......
146 155
       assert_false = tr1.assert_false || tr2.assert_false
147 156
     }
148 157
    )
149
       
158
      
159
  let pp_name :
160
  type c. c call_t  -> c -> unit =
161
    fun call -> 
162
      match call with
163
      | Ecall -> (fun (p, p', f) ->
164
	Format.fprintf Format.str_formatter "theta%a%a%a_%a"
165
	  pp_call call
166
	  (pp_path "_from_") p
167
	  (pp_path "_to_") p'
168
	  pp_frontier f)
169
      | Dcall -> (fun p          ->
170
	Format.fprintf Format.str_formatter "theta%a%a"
171
	  pp_call call
172
	  (pp_path "_from_") p)
173
      | Xcall -> (fun (p, f)     ->
174
	Format.fprintf Format.str_formatter "theta%a%a_%a"
175
	  pp_call call
176
	  (pp_path "_from_") p
177
	  pp_frontier f)
178
	     
179

  
150 180
  let mkcall' :
151 181
  type c. name_t -> name_t -> c call_t -> c -> t_base =
152
    fun sin sout call ->
153
      let pp_name : type c. c call_t  -> c -> unit =
154
	fun call -> 
155
	  match call with
156
	  | Ecall -> (fun (p, p', f) ->
157
	    Format.fprintf Format.str_formatter "theta%a%a%a_%a"
158
	      pp_call call
159
	      (pp_path "_from_") p
160
	      (pp_path "_to_") p'
161
	      pp_frontier f)
162
	  | Dcall -> (fun p          ->
163
	    Format.fprintf Format.str_formatter "theta%a%a"
164
	      pp_call call
165
	      (pp_path "_from_") p)
166
	  | Xcall -> (fun (p, f)     ->
167
	    Format.fprintf Format.str_formatter "theta%a%a_%a"
168
	      pp_call call
169
	      (pp_path "_from_") p
170
	      pp_frontier f)
171
      in
172
      fun arg ->
173
	pp_name call arg;
174
	let funname = Format.flush_str_formatter () in
175
	let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
176
	let rhs = mkpredef_call funname args in
177
	mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
178

  
182
    fun sin sout call arg ->
183
      pp_name call arg;
184
      let funname = Format.flush_str_formatter () in
185
      let args = (Corelang.expr_of_vdecl event_var)::(vars_to_exprl ~prefix:sin Vars.state_vars) in
186
      let rhs = mkpredef_call funname args in
187
      mkstmt_eq ~prefix_lhs:sout Vars.state_vars rhs
188
	
179 189
  let mkact' action sin sout =
180 190
    match action with
181 191
    | Action.Call (c, a) -> mkcall' sin sout c a
......
241 251
							  mkcond' sin cond2]
242 252
    | Condition.Quote c            -> c (* TODO: shall we prefix with sin ? *)
243 253

  
244
  let rec eval_cond condition ok ko sin sout =
254
  let rec eval_cond condition (ok:t) ko sin sout =
245 255
    let open LustreSpec in
246 256
    let loc = Location.dummy_loc in
247 257
    (*Format.printf "----- cond = %a@." Condition.pp_cond condition;*)
......
266 276
		   hand_until = [];
267 277
		   hand_locals = [];
268 278
		   hand_stmts = tr0.statements;
269
		   hand_asserts = if tr0.assert_false then
270
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
271
		     else
272
		       [];
279
		   hand_asserts = base_to_assert tr0;
273 280
		   hand_annots = [];
274 281
		   hand_loc = loc;
275 282
		 };
......
279 286
		   hand_until = [
280 287
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
281 288
		   ];
282
		   hand_locals = [vars1] (* TODO convert to valid type *);
289
		   hand_locals = mk_locals vars1;
283 290
		   hand_stmts = tr1.statements;
284
		   hand_asserts = if tr1.assert_false then
285
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
286
		     else
287
		       [];
291
		   hand_asserts = base_to_assert tr1;
288 292
		   hand_annots = [];
289 293
		   hand_loc = loc;
290 294
		 };
......
294 298
		   hand_until = [
295 299
		     (loc, expr_of_bool true, true (* restart *), "CenterPoint_" ^ aut);
296 300
		   ];
297
		   hand_locals = [vars2] (* TODO convert to valid type *);
301
		   hand_locals = mk_locals vars2;
298 302
		   hand_stmts = tr2.statements;
299
		   hand_asserts = if tr2.assert_false then
300
		       [{assert_expr = expr_of_bool false; assert_loc = loc}]
301
		     else
302
		       [];
303
		   hand_asserts = base_to_assert tr2;
303 304
		   hand_annots = [];
304 305
		   hand_loc = loc;
305 306
		 };
......
311 312
     }
312 313
    )
313 314
      
314
  let pp_transformer fmt tr =
315
  let mktransformer tr =
315 316
    let (vars, tr) = tr "sin_" "sout_"
316
    in tr fmt
317
    in tr 
317 318
    
318 319
  let mkcomponent :
319
  type c. c call_t -> c -> t -> prog =
320
    fun fmt call -> match call with
321
    | Ecall -> (fun (p, p', f) tr ->
322
      reset_loc ();
323
      let (vars', tr') = tr "sin_" "sout_" in
324
      Format.fprintf fmt "node theta%a%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
325
	pp_call call
326
	(pp_path "_from_") p
327
	(pp_path "_to_") p'
328
	pp_frontier f
329
	(pp_vars_decl "sin_") Vars.state_vars
330
	(pp_vars_decl "sout_") Vars.state_vars
331
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
332
	pp_locals vars'
333
	tr')
334
    | Dcall -> (fun p tr ->
335
      reset_loc ();
336
      let (vars', tr') = tr "sin_" "sout_" in
337
      Format.fprintf fmt "node theta%a%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
338
	pp_call call
339
	(pp_path "_from_") p
340
	(pp_vars_decl "sin_") Vars.state_vars
341
	(pp_vars_decl "sout_") Vars.state_vars
342
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
343
	pp_locals vars'
344
	tr')
345
    | Xcall -> (fun (p, f) tr ->
346
      reset_loc ();
347
      let (vars', tr') = tr "sin_" "sout_" in
348
      Format.fprintf fmt "node theta%a%a_%a(event : event_type; %a) returns (%a);@.%t%a@.let@.%t@.tel@."
349
	pp_call call
350
	(pp_path "_from_") p
351
	pp_frontier f
352
	(pp_vars_decl "sin_") Vars.state_vars
353
	(pp_vars_decl "sout_") Vars.state_vars
354
	(fun fmt -> if ActiveStates.Vars.is_empty vars' then () else Format.fprintf fmt "var@.")
355
	pp_locals vars'
356
	tr')
357

  
320
  type c. c call_t -> c -> t -> LustreSpec.program =
321
    fun call args ->
322
      fun tr ->
323
	reset_loc ();
324
	let (vars', tr') = tr "sin_" "sout_" in
325
	pp_name call args;
326
	let funname = Format.flush_str_formatter () in
327
	let node =
328
	  Corelang.mktop (	
329
	    LustreSpec.Node {LustreSpec.node_id = funname;
330
			   node_type = Types.new_var ();
331
			   node_clock = Clocks.new_var true;
332
			   node_inputs = event_var :: state_vars_to_vdecl_list ~prefix:"sin_" Vars.state_vars;
333
			   node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
334
			   node_locals = mk_locals vars'; (* TODO: add global vars *)
335
			   node_gencalls = [];
336
			   node_checks = [];
337
			   node_stmts = tr'.statements;
338
			   node_asserts = base_to_assert tr';
339
			   node_dec_stateless = false;
340
			   node_stateless = None;
341
			   node_spec = None;
342
			   node_annot = []}
343
      )  
344
	in
345
	[node]
346
	  
358 347
  let mk_main_loop () =
359
    let loc = Location.dummy_loc in
348
    (* let loc = Location.dummy_loc in *)
349
    
350
    let call_stmt =
351
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
352
      let init = mkexpr
353
	(LustreSpec.Expr_tuple (vars_to_exprl ~prefix:"sout_" Vars.state_vars))
354
      in
355
      let args = (Corelang.expr_of_vdecl event_var)::
356
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
357
      in
358
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
359
      let pre_call_expr = mkexpr (LustreSpec.Expr_pre (call_expr)) in
360
      let rhs = mkexpr (LustreSpec.Expr_arrow (init, pre_call_expr)) in
361
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
362
    in
360 363
    let node_principal =
361 364
      Corelang.mktop (	
362 365
	LustreSpec.Node {LustreSpec.node_id = "principal_loop";
363 366
			 node_type = Types.new_var ();
364 367
			 node_clock = Clocks.new_var true;
365 368
			 node_inputs = [event_var];
366
			 node_outputs = state_vars_to_vdecl_list ~prefx:"sout_" Vars.state_vars;
369
			 node_outputs = state_vars_to_vdecl_list ~prefix:"sout_" Vars.state_vars;
367 370
			 node_locals = []; (* TODO: add global vars *)
368 371
			 node_gencalls = [];
369 372
			 node_checks = [];
370
			 node_asserts = []; 
371
			 node_stmts = call_stmt;
373
			 node_asserts = base_to_assert call_stmt; 
374
			 node_stmts = call_stmt.statements;
372 375
			 node_dec_stateless = false;
373 376
			 node_stateless = None;
374 377
			 node_spec = None;
375 378
			 node_annot = []}
376 379
      )  
377 380
    in
378
    
379
    let call_stmt =
380
      (* (%t) -> pre (thetaCallD_from_principal (event, %a)) *)
381
      let init = mkexpr loc
382
	(Expr_tuple (vars_to_exprl ~prefix:"sout_" Vars.state_vars))
383
      in
384
      let args = (Corelang.expr_of_vdecl event_var)::
385
	(vars_to_exprl ~prefix:"sout_" Vars.state_vars)
386
      in
387
      let call_expr = mkpredef_call "thetaCallD_from_principal" args in
388
      let pre_call_expr = mkexpr loc (Expr_pre (call_expr)) in
389
      let rhs = mkexpr loc (Expr_arrow (init, pre_call_expr)) in
390
      mkstmt_eq Vars.state_vars ~prefix_lhs:"sout_" rhs
391
    in
392
    [
393
      event_type_decl;
394 381
      node_principal
395
    ]
382
    
396 383

  
397 384
  let mkprincipal tr =
398
    mk_main_loop () @ mkcomponent Dcall ["principal"] tr
385
    event_type_decl :: mkcomponent Dcall ["principal"] tr @ [mk_main_loop ()]
399 386

  
400 387
end
src/tools/stateflow/semantics/cPS_transformer.ml
77 77
  val ( >> ) : t -> t -> t
78 78
  val eval_act : (module ThetaType with type t = t) -> act_t -> t
79 79
  val eval_cond : cond_t -> t -> t -> t
80
  val mktransformer : Format.formatter -> t -> unit
80
  (* val mktransformer : t -> unit *)
81 81
  val mkprincipal : t -> LustreSpec.program
82 82
  val mkcomponent : 'c call_t -> 'c -> t -> LustreSpec.program
83 83
end
src/tools/stateflow/sf_sem.ml
3 3
type backend = GenLus | GenImp
4 4

  
5 5
(* Model choice *)
6
let model_name = ref "stopwatch" (*"simple"*)
6
let model_name = ref "simple"
7 7

  
8 8
let models = [(module Model_simple : Datatype.MODEL_T);
9 9
	      (module Model_stopwatch : Datatype.MODEL_T);
10
	      (module Model_medium : Datatype.MODEL_T)
10
	     (*  (module Model_medium : Datatype.MODEL_T)*)
11 11
	     ]
12 12
let get_model_name m = let module M = (val m : Datatype.MODEL_T) in M.name
13 13
let set_model name = 
......
56 56
    let module Model = (val model) in
57 57
    let module T = CPS_ccode_generator.CodeGenerator in
58 58
    let module Sem = CPS.Semantics (T) (Model) in
59
    Sem.code_gen Format.std_formatter modularmode
59
    let _ = Sem.code_gen modularmode in
60
    ()
60 61
  )				     
61 62
  | GenLus ->
62 63
     let module Model = (val model) in
......
68 69
       let global_vars = global_vars 
69 70
     end) in
70 71
     let module Sem = CPS.Semantics (T) (Model) in
71
     Sem.code_gen Format.std_formatter modularmode
72
     let prog = Sem.code_gen modularmode in
73

  
74
     Format.printf "%a@." Printers.pp_prog prog;
75

  
76
     let prog, deps = Main_lustre_compiler.stage1 prog "" "" in
77

  
78
     
79
     (* (\* Importing source *\) *)
80
     (* let _ = Modules.load_program Utils.ISet.empty prog in *)
81

  
82
     (* (\* Extracting dependencies *\) *)
83
     (* let dependencies, type_env, clock_env = Compiler_common.import_dependencies prog in *)
84

  
85

  
86
     (* (\* Typing *\) *)
87
     (* let computed_types_env = Compiler_common.type_decls type_env prog in *)
88
     
89
     (* (\* Clock calculus *\) *)
90
     (* let computed_clocks_env = Compiler_common.clock_decls clock_env prog in *)
91

  
92
     Format.printf "%a@." Printers.pp_prog prog
72 93

  
73 94

  
74 95
  

Also available in: Unified diff