Project

General

Profile

Revision 6a1a01d2

View differences:

src/automata.ml
22 22
let mkfby loc e1 e2 =
23 23
 mkexpr loc (Expr_arrow (e1, mkexpr loc (Expr_pre e2)))
24 24

  
25
let init loc restart state =
25
let mkidentpair loc restart state =
26 26
 mkexpr loc (Expr_tuple [mkident loc restart; mkident loc state])
27 27

  
28 28
let add_branch (loc, expr, restart, st) cont =
......
61 61
      | Aut aut -> List.fold_left handler_write write aut.aut_handlers) writes handler.hand_stmts
62 62
  in ISet.diff allvars locals
63 63

  
64
let node_of_handler nused node aut_id handler =
65
  let inputs = handler_read ISet.empty handler in
64
let rename_output used name = mk_new_name used (Format.sprintf "%s_out" name)
65

  
66
let rec rename_stmts_outputs frename stmts =
67
  match stmts with
68
  | []           -> []
69
  | (Eq eq) :: q   -> let eq' = Eq { eq with eq_lhs = List.map frename eq.eq_lhs } in
70
		      eq' :: rename_stmts_outputs frename q
71
  | (Aut aut) :: q -> let handlers' = List.map (fun h -> { h with hand_stmts = rename_stmts_outputs frename h.hand_stmts}) aut.aut_handlers in
72
                      let aut' = Aut { aut with aut_handlers = handlers' } in
73
		      aut' :: rename_stmts_outputs frename q
74

  
75
let mk_frename used outputs =
76
  let table = ISet.fold (fun name table -> IMap.add name (rename_output used name) table) outputs IMap.empty in
77
  (fun name -> try IMap.find name table with Not_found -> name)
78
  
79
let node_of_handler nused used node aut_id handler =
66 80
  let outputs = handler_write ISet.empty handler in
81
  let (new_locals, inputs) = ISet.partition (fun v -> ISet.mem v outputs) (handler_read ISet.empty handler) in
82
  let frename = mk_frename used outputs in
83
  let var_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs) in
84
  let new_var_locals = List.map (fun v -> get_node_var v node) (ISet.elements new_locals) in
85
  let var_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs) in
86
  let new_var_outputs = List.map (fun vdecl -> { vdecl with var_id = frename vdecl.var_id }) var_outputs in
87
  let new_output_eqs = List.map2 (fun o o' -> Eq (mkeq handler.hand_loc ([o'.var_id], mkident handler.hand_loc o.var_id))) var_outputs new_var_outputs in
88
  var_outputs,
67 89
  {
68 90
    node_id = mk_new_name nused (Format.sprintf "%s_%s_handler" aut_id handler.hand_state);
69 91
    node_type = Types.new_var ();
70 92
    node_clock = Clocks.new_var true;
71
    node_inputs = List.map (fun v -> get_node_var v node) (ISet.elements inputs);
72
    node_outputs = List.map (fun v -> get_node_var v node) (ISet.elements outputs);
73
    node_locals = handler.hand_locals;
93
    node_inputs = var_inputs;
94
    node_outputs = new_var_outputs;
95
    node_locals = new_var_locals @ handler.hand_locals;
74 96
    node_gencalls = [];
75 97
    node_checks = [];
76 98
    node_asserts = handler.hand_asserts; 
77
    node_stmts = handler.hand_stmts;
99
    node_stmts = new_output_eqs @ handler.hand_stmts;
78 100
    node_dec_stateless = false;
79 101
    node_stateless = None;
80 102
    node_spec = None;
......
82 104
  }
83 105

  
84 106
let expr_of_exit loc restart state conds tag =
85
  mkexpr loc (Expr_when (List.fold_right add_branch conds (init loc restart state), state, tag))
107
  mkexpr loc (Expr_when (List.fold_right add_branch conds (mkidentpair loc restart state), state, tag))
86 108

  
87 109
let expr_of_handler loc restart state node tag =
88
  let arg = mkexpr loc (Expr_tuple (List.map (fun v -> mkident loc v.var_id) node.node_inputs)) in
89
  mkexpr loc (Expr_when (mkexpr loc (Expr_appl (node.node_id, arg, Some (restart, tag_true))), state, tag))
110
  let args = List.map (fun v -> mkexpr loc (Expr_when (mkident loc v.var_id, state, tag))) node.node_inputs in
111
  let arg = mkexpr loc (Expr_tuple args) in
112
  let reset = Some (mkident loc restart) in
113
  mkexpr loc (Expr_appl (node.node_id, arg, reset))
90 114

  
91 115
let assign_aut_handlers loc actual_r actual_s hnodes =
92
  let outputs = (snd (List.hd hnodes)).node_outputs in
93
  let assign_handlers = List.map (fun (hs, n) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
116
  let outputs = fst (snd (List.hd hnodes)) in
117
  let assign_handlers = List.map (fun (hs, (_, n)) -> (hs, expr_of_handler loc actual_r actual_s n hs)) hnodes in
94 118
  let assign_expr = mkexpr loc (Expr_merge (actual_s, assign_handlers)) in
95 119
  let assign_eq = mkeq loc (List.map (fun v -> v.var_id) outputs, assign_expr) in
96 120
  assign_eq
......
100 124
  { tydef_id = tname;
101 125
    tydef_desc = Tydec_enum (List.map (fun h -> h.hand_state) aut.aut_handlers)
102 126
  }
127
(*
128
let expand_automata nused used owner typedef node aut =
129
  let initial = (List.hd aut.aut_handlers).hand_state in
130
  let incoming_r = mk_new_name used (aut.aut_id ^ "__restart_in") in
131
  let incoming_s = mk_new_name used (aut.aut_id ^ "__state_in") in
132
  let actual_r = mk_new_name used (aut.aut_id ^ "__restart_act") in
133
  let actual_s = mk_new_name used (aut.aut_id ^ "__state_act") in
134
  let next_incoming_r = mk_new_name used (aut.aut_id ^ "__next_restart_in") in
135
  let next_incoming_s = mk_new_name used (aut.aut_id ^ "__next_state_in") in
136
  (* merge on incoming_s gives actual_s by the unless equations *)
137
  let actual_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc incoming_r incoming_s h.hand_unless h.hand_state)) aut.aut_handlers in
138
  let actual_expr = mkexpr aut.aut_loc (Expr_merge (incoming_s, unless_handlers)) in
139
  let actual_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
140
  (* next_incoming_s and initial conditions gives incoming_s *)
141
  let incoming_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) (mkidentpair aut.aut_loc next_incoming_r next_incoming_s) in
142
  let incoming_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], incoming_expr) in
143
  (* merge on actual_s gives handler assigned variables and next_incoming_s by the until equations *)
144
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
145
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
146
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
147
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
148
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
149
  let outputs = fst (snd (List.hd hnodes)) in
150
  let next_incoming_and_assigned_vars = next_incoming_r :: next_incoming_s :: List.map (fun v -> v.var_id) outputs in
151
  let next_incoming_and_assigned_handlers =
152
    List.map (fun h -> ) aut.aut_handlers in
153
  let next_incoming_and_assigned_expr = mkexpr loc (Expr_merge (actual_s, next_incoming_and_assigned_handlers) in
154
  let next_incoming_and_assigned_eq = mkeq aut.aut_loc (next_incoming_and_assigned_vars, next_incoming_and_assigned_expr) in
155
  (* declaration of new local variables, equations and handler nodes *)
156
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
157
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
158
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
159
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
160
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
161
                 mkvar_decl aut.aut_loc (next_incoming_r  , tydec_bool, ckdec_any, false);
162
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
163
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false);
164
                 mkvar_decl aut.aut_loc (next_incoming_s, tydec_state typedef.tydef_id, ckdec_any, false)] in
165
  let eqs' = [Eq actual_eq; Eq next_incoming_and_assigned_eq; Eq incoming_eq] in
166
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
167
  locals',
168
  eqs')
169
*)
103 170

  
104 171
let expand_automata nused used owner typedef node aut =
105 172
  let initial = (List.hd aut.aut_handlers).hand_state in
......
112 179
  let unless_eq = mkeq aut.aut_loc ([actual_r; actual_s], unless_expr) in
113 180
  let until_handlers = List.map (fun h -> (h.hand_state, expr_of_exit h.hand_loc actual_r actual_s h.hand_until h.hand_state)) aut.aut_handlers in
114 181
  let until_expr = mkexpr aut.aut_loc (Expr_merge (actual_s, until_handlers)) in
115
  let fby_until_expr = mkfby aut.aut_loc (init aut.aut_loc tag_false initial) until_expr in
182
  let fby_until_expr = mkfby aut.aut_loc (mkidentpair aut.aut_loc tag_false initial) until_expr in
116 183
  let until_eq = mkeq aut.aut_loc ([incoming_r; incoming_s], fby_until_expr) in
117
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused node aut.aut_id h)) aut.aut_handlers in
184
  let hnodes = List.map (fun h -> (h.hand_state, node_of_handler nused used node aut.aut_id h)) aut.aut_handlers in
118 185
  let assign_eq = assign_aut_handlers aut.aut_loc actual_r actual_s hnodes in
119 186
  let tydec_bool = { ty_dec_desc = Tydec_bool; ty_dec_loc = aut.aut_loc } in
120
  let tydec_const id = { ty_dec_desc = Tydec_const id; ty_dec_loc = aut.aut_loc } in
187
  let tydec_state id = { ty_dec_desc = Tydec_clock (Tydec_const id); ty_dec_loc = aut.aut_loc } in
121 188
  let ckdec_any = { ck_dec_desc = Ckdec_any; ck_dec_loc = aut.aut_loc } in
122 189
  let locals' = [mkvar_decl aut.aut_loc (incoming_r, tydec_bool, ckdec_any, false);
123 190
                 mkvar_decl aut.aut_loc (actual_r  , tydec_bool, ckdec_any, false);
124
                 mkvar_decl aut.aut_loc (incoming_s, tydec_const typedef.tydef_id, ckdec_any, false);
125
                 mkvar_decl aut.aut_loc (actual_s  , tydec_const typedef.tydef_id, ckdec_any, false)] in
191
                 mkvar_decl aut.aut_loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
192
                 mkvar_decl aut.aut_loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)] in
126 193
  let eqs' = [Eq unless_eq; Eq assign_eq; Eq until_eq] in
127
  (List.map2 (fun h (hs, n) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
194
  (List.map2 (fun h (hs, (_, n)) -> mktop_decl h.hand_loc owner false (Node n)) aut.aut_handlers hnodes,
128 195
  locals',
129 196
  eqs')
130 197

  
src/backends/C/c_backend_common.ml
47 47

  
48 48
let mk_call_var_decl loc id =
49 49
  { var_id = id;
50
    var_orig = false;
50 51
    var_dec_type = mktyp Location.dummy_loc Tydec_any;
51 52
    var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
52 53
    var_dec_const = false;
src/causality.ml
109 109
 assert (is_read_var id);
110 110
 String.sub id 1 (String.length id - 1)
111 111

  
112
let undo_instance_var id =
113
 assert (is_instance_var id);
114
 String.sub id 1 (String.length id - 1)
115

  
112 116
let eq_memory_variables mems eq =
113 117
  let rec match_mem lhs rhs mems =
114 118
    match rhs.expr_desc with
......
241 245
      (* mashed up dependency for user-defined operators *)
242 246
      else
243 247
	mashup_appl_dependencies f e g
244
    | Expr_appl (f, e, Some (r, _)) ->
245
      mashup_appl_dependencies f e (add_var lhs_is_mem lhs r g)
248
    | Expr_appl (f, e, Some c) ->
249
      mashup_appl_dependencies f e (add_dep lhs_is_mem lhs c g)
246 250
  in
247 251
  let g =
248 252
    List.fold_left
......
362 366
	expr_delay = Delay.new_var ();
363 367
	expr_annot = None;
364 368
	expr_loc = var_decl.var_loc } in
365
    { var_decl with var_id = cp_var },
369
    { var_decl with var_id = cp_var; var_orig = false },
366 370
    mkeq var_decl.var_loc ([cp_var], expr)
367 371

  
368 372
  let wrong_partition g partition =
......
526 530

  
527 531
let pp_error fmt trace =
528 532
  fprintf fmt "@.Causality error, cyclic data dependencies: %a@."
529
    (fprintf_list ~sep:"->" pp_print_string) trace
533
    (fprintf_list ~sep:", " pp_print_string) trace
530 534

  
531 535
(* Merges elements of graph [g2] into graph [g1] *)
532 536
let merge_with g1 g2 =
src/clock_calculus.ml
441 441
      (Const_int i) -> i
442 442
  | _ -> failwith "Internal error: int_factor_of_expr"
443 443

  
444
(** [clock_uncarry ck] drops the possible carrier name from clock [ck] *)
445
let clock_uncarry ck =
444
(** [clock_uncarry ck] drops the possible carrier(s) name(s) from clock [ck] *)
445
let rec clock_uncarry ck =
446 446
  let ck = repr ck in
447 447
  match ck.cdesc with
448 448
  | Ccarrying (_, ck') -> ck'
449
  | Con(ck', cr, l)    -> clock_on (clock_uncarry ck') cr l
450
  | Ctuple ckl         -> clock_of_clock_list (List.map clock_uncarry ckl)
449 451
  | _                  -> ck
450 452

  
451 453
let try_unify ck1 ck2 loc =
......
557 559
  in
558 560
  aux ck
559 561

  
562
(* Computes the root clock of a tuple or a node clock,
563
   which is not the same as the base clock.
564
   Root clock will be used as the call clock 
565
   of a given node instance *)
566
let compute_root_clock ck =
567
  let root = Clocks.root ck in
568
  let branch = ref None in
569
  let rec aux ck =
570
    match (repr ck).cdesc with
571
    | Ctuple cl ->
572
        List.iter aux cl
573
    | Carrow (ck1,ck2) ->
574
        aux ck1; aux ck2
575
    | _ ->
576
        begin
577
          match !branch with
578
          | None ->
579
              branch := Some (Clocks.branch ck)
580
          | Some br ->
581
              (* cannot fail *)
582
              branch := Some (Clocks.common_prefix br (Clocks.branch ck))
583
        end
584
  in
585
  begin
586
    aux ck;
587
    Clocks.clock_of_root_branch root (Utils.desome !branch)
588
  end
589

  
560 590
(* Clocks a list of arguments of Lustre builtin operators:
561 591
   - type each expression, remove carriers of clocks as
562 592
     carriers may only denote variables, not arbitrary expr.
......
658 688
    let cr =
659 689
      match r with
660 690
      | None        -> new_var true
661
      | Some (x, _) -> let loc_r = loc_of_cond expr.expr_loc x in
662
		       let expr_r = expr_of_ident x loc_r in
663
		       clock_expr env expr_r in
691
      | Some c      -> clock_standard_args env [c] in
664 692
    let couts = clock_appl env id args cr expr.expr_loc in
665 693
    expr.expr_clock <- couts;
666 694
    couts
......
690 718
  | Expr_merge (c,hl) ->
691 719
      let cvar = new_var true in
692 720
      let crvar = new_carrier Carry_name true in
693
      List.iter (fun (t, h) -> let ckh = clock_expr env h in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
721
      List.iter (fun (t, h) -> let ckh = clock_uncarry (clock_expr env h) in unify_tuple_clock (Some (new_ck (Con (cvar,crvar,t)) true)) ckh h.expr_loc) hl;
694 722
      let cr = clock_carrier env c expr.expr_loc cvar in
695 723
      try_unify_carrier cr crvar expr.expr_loc;
696
      expr.expr_clock <- cvar;
697
      cvar
724
      let cres = clock_current ((snd (List.hd hl)).expr_clock) in
725
      expr.expr_clock <- cres;
726
      cres
698 727
  in
699 728
  Log.report ~level:4 (fun fmt -> Format.fprintf fmt "Clock of expr %a: %a@." Printers.pp_expr expr Clocks.print_ck resulting_ck);
700 729
  resulting_ck
src/clocks.ml
164 164
let clock_on ck cr l =
165 165
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
166 166

  
167
let clock_current ck =
168
 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
169

  
167 170
let clock_of_impnode_clock ck =
168 171
  let ck = repr ck in
169 172
  match ck.cdesc with
......
378 381
    | _                 -> acc
379 382
  in branch ck [];;
380 383

  
384
let clock_of_root_branch r br =
385
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
386

  
387
(* Computes the (longest) common prefix of two branches *)
388
let rec common_prefix br1 br2 =
389
 match br1, br2 with
390
 | []          , _
391
 | _           , []           -> []
392
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
393
   if eq_carrier cr1 cr2 && (l1 = l2)
394
   then (cr1, l1) :: common_prefix q1 q2
395
   else []
396

  
381 397
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
382 398
let rec disjoint_branches br1 br2 =
383 399
 match br1, br2 with
src/compiler_common.ml
39 39
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. parsing header file %s@ " filename);
40 40
    try
41 41
      let header = Parse.header Parser_lustre.header Lexer_lustre.token lexbuf in
42
      ignore (Modules.load_header ISet.empty header);
42
      (*ignore (Modules.load_header ISet.empty header);*)
43 43
      close_in h_in;
44 44
      header
45 45
    with
......
65 65
    (fun fmt -> fprintf fmt ".. parsing source file %s@," source_name);
66 66
  try
67 67
    let prog = Parse.prog Parser_lustre.prog Lexer_lustre.token lexbuf in
68
    ignore (Modules.load_program ISet.empty prog);
68
    (*ignore (Modules.load_program ISet.empty prog);*)
69 69
    close_in s_in;
70 70
    prog
71 71
  with
src/corelang.ml
41 41
let mkclock loc d =
42 42
  { ck_dec_desc = d; ck_dec_loc = loc }
43 43

  
44
let mkvar_decl loc (id, ty_dec, ck_dec, is_const) =
44
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) =
45 45
  { var_id = id;
46
    var_orig = orig;
46 47
    var_dec_type = ty_dec;
47 48
    var_dec_clock = ck_dec;
48 49
    var_dec_const = is_const;
......
61 62

  
62 63
let var_decl_of_const c =
63 64
  { var_id = c.const_id;
65
    var_orig = true;
64 66
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
65 67
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
66 68
    var_dec_const = true;
......
572 574
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
573 575
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
574 576
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
575
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (fun (x, l) -> fvar x, l) i')
577
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
576 578

  
577 579
(* Applies the renaming function [fvar] to every rhs
578 580
   only when the corresponding lhs satisfies predicate [pvar] *)
......
631 633
   | Expr_merge (i, hl) -> 
632 634
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
633 635
   | Expr_appl (i, e', i') -> 
634
     Expr_appl (f_node i, re e', Utils.option_map (fun (x, l) -> f_var x, l) i')
636
     Expr_appl (f_node i, re e', Utils.option_map re i')
635 637
  
636 638
 let rename_node_annot f_node f_var f_const expr  =
637 639
   expr
......
929 931
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
930 932
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
931 933
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
932
  | Expr_appl (_, arg, Some (r,_)) -> get_expr_vars (Utils.ISet.add r vars) arg
934
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
933 935

  
934 936

  
935 937
let rec expr_has_arrows e =
src/corelang.mli
19 19

  
20 20
val mktyp: Location.t -> type_dec_desc -> type_dec
21 21
val mkclock: Location.t -> clock_dec_desc -> clock_dec
22
val mkvar_decl: Location.t -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl
22
val mkvar_decl: Location.t -> ?orig:bool -> ident * type_dec * clock_dec * bool (* is const *) -> var_decl
23 23
val var_decl_of_const: const_desc -> var_decl
24 24
val mkexpr: Location.t ->  expr_desc -> expr
25 25
val mkeq: Location.t -> ident list * expr -> eq
......
83 83
val expr_of_ident : ident -> Location.t -> expr
84 84
val expr_list_of_expr : expr -> expr list
85 85
val expr_of_expr_list : Location.t -> expr list -> expr
86
val call_of_expr: expr -> (ident * expr list * (ident * label) option)
86
val call_of_expr: expr -> (ident * expr list * expr option)
87 87
val expr_of_dimension: Dimension.dim_expr -> expr
88 88
val dimension_of_expr: expr -> Dimension.dim_expr
89 89
val dimension_of_const: Location.t -> constant -> Dimension.dim_expr
src/expand.ml
73 73
  let ty_dec = {ty_dec_desc = Tydec_any; ty_dec_loc = vloc} in (* dummy *)
74 74
  let ck_dec = {ck_dec_desc = Ckdec_any; ck_dec_loc = vloc} in (* dummy *)
75 75
  {var_id = vid;
76
   var_orig = false;
76 77
   var_dec_type = ty_dec;
77 78
   var_dec_clock = ck_dec;
78 79
   var_dec_deadline = vdd;
src/lustreSpec.ml
50 50

  
51 51
type var_decl = 
52 52
    {var_id: ident;
53
     var_orig:bool;
53 54
     var_dec_type: type_dec;
54 55
     var_dec_clock: clock_dec;
55 56
     var_dec_const: bool;
......
102 103
  | Expr_merge of ident * (label * expr) list
103 104
  | Expr_appl of call_t
104 105

  
105
and call_t = ident * expr * (ident * label) option 
106
     (* The third part denotes the reseting clock label and value *)
106
and call_t = ident * expr * expr option 
107
     (* The third part denotes the boolean condition for resetting *)
107 108

  
108 109
and eq =
109 110
    {eq_lhs: ident list;
src/machine_code.ml
133 133
let dummy_var_decl name typ =
134 134
  {
135 135
    var_id = name;
136
    var_orig = false;
136 137
    var_dec_type = dummy_type_dec;
137 138
    var_dec_clock = dummy_clock_dec;
138 139
    var_dec_const = false;
......
327 328
let reset_instance node args i r c =
328 329
  match r with
329 330
  | None        -> []
330
  | Some (x, l) -> [control_on_clock node args c (MBranch (translate_ident node args x, [l, [MReset i]]))]
331
  | Some r      -> let g = translate_guard node args r in
332
                   [control_on_clock node args c (conditional g [MReset i] [])]
331 333

  
332 334
let translate_eq node ((m, si, j, d, s) as args) eq =
333 335
  (*Format.eprintf "translate_eq %a with clock %a@." Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;*)
......
366 368
      node_f,
367 369
      NodeDep.filter_static_inputs (node_inputs node_f) el in 
368 370
    let o = new_instance node node_f eq.eq_rhs.expr_tag in
369
    let call_ck = Clocks.new_var true in
371
    let env_cks = List.fold_right (fun arg cks -> arg.expr_clock :: cks) el [eq.eq_rhs.expr_clock] in
372
    let call_ck = Clock_calculus.compute_root_clock (Clock_predef.ck_tuple env_cks) in
373
    (*Clocks.new_var true in
370 374
    Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
375
    Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
371 376
    (m,
372 377
     (if Stateless.check_node node_f then si else MReset o :: si),
373 378
     Utils.IMap.add o call_f j,
src/main_lustre_compiler.ml
12 12
open Format
13 13
open Log
14 14

  
15
open Utils
15 16
open LustreSpec
16 17
open Compiler_common
17 18

  
......
38 39
  begin
39 40
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
40 41
    let header = parse_header true header_name in
42
    ignore (Modules.load_header ISet.empty header);
41 43
    ignore (check_top_decls header);
42 44
    create_dest_dir ();
43 45
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %sc@," header_name);
......
85 87

  
86 88
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
87 89

  
90
  (* Parsing source *)
88 91
  let prog = parse_source source_name in
89 92

  
93
  (* Removing automata *) 
94
  let prog = Automata.expand_decls prog in
95

  
96
  (* Importing source *)
97
  let _ = Modules.load_program ISet.empty prog in
98

  
90 99
  (* Extracting dependencies *)
91 100
  let dependencies, type_env, clock_env = import_dependencies prog in
92 101

  
93
  (* Removing automata *) 
94
  (*let prog = Automata.expand_decls prog in*)
95

  
96
  (*Printers.pp_prog Format.std_formatter prog;*)
97 102
  (* Sorting nodes *)
98 103
  let prog = SortProg.sort prog in
99 104

  
src/modules.ml
82 82
  in import ((typedef_of_top tydef).tydef_desc)
83 83

  
84 84
let add_type itf name value =
85
(*Format.eprintf "add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)
85
(*Format.eprintf "Modules.add_type %B %s %a (owner=%s)@." itf name Printers.pp_typedef (typedef_of_top value) value.top_decl_owner;*)
86 86
  try
87 87
    let value' = Hashtbl.find type_table (Tydec_const name) in
88 88
    let owner' = value'.top_decl_owner in
src/normalization.ml
65 65
  if List.exists (fun v -> v.var_id = s) vars then aux () else
66 66
  {
67 67
    var_id = s;
68
    var_orig = false;
68 69
    var_dec_type = dummy_type_dec;
69 70
    var_dec_clock = dummy_clock_dec;
70 71
    var_dec_const = false;
......
371 372
     - compute the associated expression without aliases     
372 373
  *)
373 374
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
375
  let split_defs = Splitting.tuple_split_eq_list defs in
374 376
  let norm_traceability = {
375
    annots =
376
      List.map 
377
	(fun v -> 
378
	  let expr = substitute_expr diff_vars defs (
379
	    let eq = try
380
		       List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
381
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
	    eq.eq_rhs) in 
383
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
384
	  ["horn_backend";"trace"], pair 
385
	)
386
    diff_vars ;
377
    annots = List.map (fun v ->
378
      let eq =
379
	try
380
	  List.find (fun eq -> eq.eq_lhs = [v.var_id]) split_defs 
381
	with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
382
      let expr = substitute_expr diff_vars split_defs eq.eq_rhs in
383
      let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in
384
      (["horn_backend";"trace"], pair)
385
    ) diff_vars;
387 386
    annot_loc = Location.dummy_loc
388 387
  }
389 388

  
src/optimize_machine.ml
40 40
  | Cst _ | StateVar _ -> expr
41 41

  
42 42
(* see if elim has to take in account the provided instr:
43
   if so, upodate elim and return the remove flag,
43
   if so, update elim and return the remove flag,
44 44
   otherwise, the expression should be kept and elim is left untouched *)
45 45
let update_elim outputs elim instr =
46 46
(*  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;*)
src/parser_lustre.mly
20 20

  
21 21
let mktyp x = mktyp (get_loc ()) x
22 22
let mkclock x = mkclock (get_loc ()) x
23
let mkvar_decl x = mkvar_decl (get_loc ()) x
23
let mkvar_decl x = mkvar_decl (get_loc ()) ~orig:true x
24 24
let mkexpr x = mkexpr (get_loc ()) x
25 25
let mkeexpr x = mkeexpr (get_loc ()) x 
26 26
let mkeq x = mkeq (get_loc ()) x
......
266 266
| handler handler_list { $1::$2 }
267 267

  
268 268
handler:
269
 STATE UIDENT ARROW unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
269
 STATE UIDENT COL unless_list locals LET stmt_list TEL until_list { Automata.mkhandler (get_loc ()) $2 $4 $9 $5 $7 }
270 270

  
271 271
unless_list:
272 272
    { [] }
......
381 381
/* Applications */
382 382
| node_ident LPAR expr RPAR
383 383
    {mkexpr (Expr_appl ($1, $3, None))}
384
| node_ident LPAR expr RPAR EVERY vdecl_ident
385
    {mkexpr (Expr_appl ($1, $3, Some ($6, tag_true)))}
386
| node_ident LPAR expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR
387
    {mkexpr (Expr_appl ($1, $3, Some ($8, $6))) }
384
| node_ident LPAR expr RPAR EVERY expr
385
    {mkexpr (Expr_appl ($1, $3, Some $6))}
388 386
| node_ident LPAR tuple_expr RPAR
389 387
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
390
| node_ident LPAR tuple_expr RPAR EVERY vdecl_ident
391
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($6, tag_true))) }
392
| node_ident LPAR tuple_expr RPAR EVERY tag_ident LPAR vdecl_ident RPAR
393
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some ($8, $6))) }
388
| node_ident LPAR tuple_expr RPAR EVERY expr
389
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }
394 390

  
395 391
/* Boolean expr */
396 392
| expr AND expr 
......
527 523

  
528 524
vdecl:
529 525
/* Useless no ?*/    ident_list
530
    {List.map mkvar_decl 
531
        (List.map (fun id -> (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1)}
526
    { List.map (fun id -> mkvar_decl (id, mktyp Tydec_any, mkclock Ckdec_any, false)) $1 }
532 527

  
533 528
| ident_list COL typeconst clock 
534
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $3, $4, false)) $1)}
529
    { List.map (fun id -> mkvar_decl (id, mktyp $3, $4, false)) $1 }
535 530
| CONST ident_list COL typeconst /* static parameters don't have clocks */
536
    {List.map mkvar_decl (List.map (fun id -> (id, mktyp $4, mkclock Ckdec_any, true)) $2)}
531
    { List.map (fun id -> mkvar_decl (id, mktyp $4, mkclock Ckdec_any, true)) $2 }
537 532

  
538 533
cdecl_list:
539 534
  cdecl SCOL { (fun itf -> [$1 itf]) }
src/printers.ml
86 86
and pp_app fmt id e r =
87 87
  match r with
88 88
  | None -> pp_call fmt id e
89
  | Some (x, l) -> fprintf fmt "%t every %s(%s)" (fun fmt -> pp_call fmt id e) l x 
89
  | Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
90 90

  
91 91
and pp_call fmt id e =
92 92
  match id, e.expr_desc with
......
135 135
  Format.fprintf fmt "%s" (if restart then "restart" else "resume")
136 136

  
137 137
let pp_unless fmt (_, expr, restart, st) =
138
  Format.fprintf fmt "unless %a %a %s"
138
  Format.fprintf fmt "unless %a %a %s@ "
139 139
    pp_expr expr
140 140
    pp_restart restart
141 141
    st
142 142

  
143 143
let pp_until fmt (_, expr, restart, st) =
144
  Format.fprintf fmt "until %a %a %s"
144
  Format.fprintf fmt "until %a %a %s@ "
145 145
    pp_expr expr
146 146
    pp_restart restart
147 147
    st
148 148

  
149 149
let rec pp_handler fmt handler =
150
  Format.fprintf fmt "state %s -> %a %a let %a tel %a"
150
  Format.fprintf fmt "state %s ->@ @[<v 2>  %a%alet@,@[<v 2>  %a@]@,tel%a@]"
151 151
    handler.hand_state
152
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
152
    (Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless
153 153
    (fun fmt locals ->
154 154
      match locals with [] -> () | _ ->
155 155
	Format.fprintf fmt "@[<v 4>var %a@]@ " 
......
158 158
	  locals)
159 159
    handler.hand_locals
160 160
    pp_node_stmts handler.hand_stmts
161
    (Utils.fprintf_list ~sep:"@ " pp_until) handler.hand_until
161
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
162 162

  
163 163
and pp_node_stmt fmt stmt =
164 164
  match stmt with
......
168 168
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
169 169

  
170 170
and pp_node_aut fmt aut =
171
  Format.fprintf fmt "automaton %s %a"
171
  Format.fprintf fmt "@[<v 0>automaton %s@,%a@]"
172 172
    aut.aut_id
173 173
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
174 174

  
src/scheduling.ml
116 116
    !sorted
117 117
  end
118 118

  
119
(* Filters out normalization variables and renames instance variables to keep things readable,
120
   in a case of a dependency error *)
121
let filter_original n vl =
122
 List.fold_right (fun v res ->
123
   if ExprDep.is_instance_var v then Format.sprintf "node %s" (ExprDep.undo_instance_var v) :: res else
124
   let vdecl = get_node_var v n in
125
   if vdecl.var_orig then v :: res else res) vl []
126

  
119 127
let schedule_node n =
128
  let node_vars = get_node_vars n in
120 129
  try
121 130
    let eq_equiv = ExprDep.node_eq_equiv n in
122 131
    let eq_equiv v1 v2 =
......
143 152
    let sort = topological_sort eq_equiv g in
144 153
    let unused = Liveness.compute_unused_variables n gg in
145 154
    let fanin = Liveness.compute_fanin n gg in
146

  
147
    let disjoint = Disjunction.clock_disjoint_map (get_node_vars n) in
155
 
156
    let disjoint = Disjunction.clock_disjoint_map node_vars in
148 157
    
149 158
    Log.report ~level:2 
150 159
      (fun fmt -> 
......
164 173
      );
165 174
 
166 175
    n', { schedule = sort; unused_vars = unused; fanin_table = fanin; reuse_table = reuse }
167
  with (Causality.Cycle v) as exc ->
168
    pp_error Format.err_formatter v;
176
  with (Causality.Cycle vl) as exc ->
177
    let vl = filter_original n vl in
178
    pp_error Format.err_formatter vl;
169 179
    raise exc
170 180

  
171 181
let schedule_prog prog =
src/typing.ml
444 444
       expression *)
445 445
    (match r with
446 446
    | None        -> ()
447
    | Some (x, l) -> 
448
      check_constant expr.expr_loc const false;
449
      let expr_x = expr_of_ident x expr.expr_loc in	
450
      let typ_l = 
451
	Type_predef.type_clock 
452
	  (type_const expr.expr_loc (Const_tag l)) in
453
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
447
    | Some c -> 
448
      check_constant expr.expr_loc const false;	
449
      type_subtyping_arg env in_main const c Type_predef.type_bool);
454 450
    let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
455 451
    expr.expr_type <- touts;
456 452
    touts
test/tests_ok.list
908 908
./tests/lusic/test1.lusi
909 909
./tests/lusic/test1.lus,as_soon_as
910 910
./tests/lusic/test2.lus
911
./tests/automata/aut1.lus
911 912
./tests/linear_ctl/ex8sat.lus,top
912 913
./tests/linear_ctl/ex2reset.lus,top
913 914
./tests/linear_ctl/lp_iir_9600_2.lus,top

Also available in: Unified diff