Project

General

Profile

Revision d50b0dc0

View differences:

src/causality.ml
28 28
   by duplication of some mem vars into local node vars.
29 29
   Thus, cylic dependency errors may only arise between no-mem vars.
30 30
   non-mem variables are:
31
   - inputs: not needed for causality/scheduling, needed only for detecting useless vars
31
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
32 32
   - read mems (fake vars): same remark as above.
33 33
   - outputs: decoupled from mems, if necessary
34 34
   - locals
......
133 133
let node_local_variables nd =
134 134
 List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
135 135

  
136
let node_constant_variables nd =
137
  List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals
138

  
136 139
let node_output_variables nd =
137 140
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
138 141

  
......
533 536

  
534 537
let global_dependency node =
535 538
  let mems = ExprDep.node_memory_variables node in
536
  let inputs = ExprDep.node_input_variables node in
539
  let inputs =
540
    ISet.union
541
      (ExprDep.node_input_variables node)
542
      (ExprDep.node_constant_variables node) in
537 543
  let outputs = ExprDep.node_output_variables node in
538 544
  let node_vars = ExprDep.node_variables node in
539 545
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
src/clock_calculus.ml
779 779
      if Types.get_clock_base_type vdecl.var_type <> None
780 780
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
781 781
      else ck in
782
  vdecl.var_clock <- ck;
782
  (if vdecl.var_dec_const
783
   then match vdecl.var_dec_value with
784
   | None   -> ()
785
   | Some v ->
786
     begin
787
       let ck_static = clock_expr env v in
788
       try_unify ck ck_static v.expr_loc
789
     end);
790
  try_unify ck vdecl.var_clock vdecl.var_loc;
783 791
  Env.add_value env vdecl.var_id ck
784 792

  
785 793
(* Clocks a variable declaration list *)
src/clock_predef.ml
42 42
  let cuniv = new_carrier Carry_var false in
43 43
  new_ck (Carrow (new_ck (Ccarrying (cuniv, univ)) false, univ))
44 44

  
45
let ck_carrier id ck =
46
 new_ck (Ccarrying (new_carrier (Carry_const id) true, ck)) true
45 47
(* Local Variables: *)
46 48
(* compile-command:"make -C .." *)
47 49
(* End: *)
src/clocks.ml
72 72
exception Scope_clock of clock_expr
73 73
exception Error of Location.t * error
74 74

  
75
let print_ckset fmt s =
76
  match s with
77
  | CSet_all -> ()
78
  | CSet_pck (k,q) ->
79
      let (a,b) = simplify_rat q in
80
      if k = 1 && a = 0 then
81
        fprintf fmt "<:P"
82
      else
83
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
84

  
85
let rec print_carrier fmt cr =
86
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
87
  match cr.carrier_desc with
88
  | Carry_const id -> fprintf fmt "%s" id
89
  | Carry_name ->
90
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
91
  | Carry_var ->
92
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
93
  | Carry_link cr' ->
94
    print_carrier fmt cr'
95

  
96
(* Simple pretty-printing, performs no simplifications. Linear
97
   complexity. For debug mainly. *)
98
let rec print_ck_long fmt ck =
99
  match ck.cdesc with
100
  | Carrow (ck1,ck2) ->
101
      fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
102
  | Ctuple cklist ->
103
    fprintf fmt "(%a)"
104
      (fprintf_list ~sep:" * " print_ck_long) cklist
105
  | Con (ck,c,l) ->
106
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
107
  | Pck_up (ck,k) ->
108
    fprintf fmt "%a*^%i" print_ck_long ck k
109
  | Pck_down (ck,k) ->
110
    fprintf fmt "%a/^%i" print_ck_long ck k
111
  | Pck_phase (ck,q) ->
112
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
113
  | Pck_const (n,p) ->
114
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
115
  | Cvar cset ->
116
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
117
  | Cunivar cset ->
118
    fprintf fmt "'%i%a" ck.cid print_ckset cset
119
  | Clink ck' ->
120
    fprintf fmt "link %a" print_ck_long ck'
121
  | Ccarrying (cr,ck') ->
122
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
123

  
75 124
let new_id = ref (-1)
76 125

  
77 126
let new_ck desc scoped =
......
117 166
 | Ccarrying (cr, _) -> Some cr
118 167
 | _                 -> None
119 168

  
169
let rename_carrier_static rename cr =
170
  match (carrier_repr cr).carrier_desc with
171
  | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
172
  | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
173

  
174
let rec rename_static rename ck =
175
 match (repr ck).cdesc with
176
 | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
177
 | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
178
 | _                   -> ck
179

  
120 180
let uncarrier ck =
121 181
 match ck.cdesc with
122 182
 | Ccarrying (_, ck') -> ck'
......
257 317
  in
258 318
  aux [] ck
259 319

  
260
let print_ckset fmt s =
261
  match s with
262
  | CSet_all -> ()
263
  | CSet_pck (k,q) ->
264
      let (a,b) = simplify_rat q in
265
      if k = 1 && a = 0 then
266
        fprintf fmt "<:P"
267
      else
268
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
269

  
270
let rec print_carrier fmt cr =
271
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
272
  match cr.carrier_desc with
273
  | Carry_const id -> fprintf fmt "%s" id
274
  | Carry_name ->
275
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
276
  | Carry_var ->
277
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
278
  | Carry_link cr' ->
279
    print_carrier fmt cr'
280

  
281
(* Simple pretty-printing, performs no simplifications. Linear
282
   complexity. For debug mainly. *)
283
let rec print_ck_long fmt ck =
284
  match ck.cdesc with
285
  | Carrow (ck1,ck2) ->
286
      fprintf fmt "%a->%a" print_ck_long ck1 print_ck_long ck2
287
  | Ctuple cklist ->
288
    fprintf fmt "(%a)"
289
      (fprintf_list ~sep:" * " print_ck_long) cklist
290
  | Con (ck,c,l) ->
291
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
292
  | Pck_up (ck,k) ->
293
    fprintf fmt "%a*^%i" print_ck_long ck k
294
  | Pck_down (ck,k) ->
295
    fprintf fmt "%a/^%i" print_ck_long ck k
296
  | Pck_phase (ck,q) ->
297
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
298
  | Pck_const (n,p) ->
299
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
300
  | Cvar cset ->
301
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
302
  | Cunivar cset ->
303
    fprintf fmt "'%i%a" ck.cid print_ckset cset
304
  | Clink ck' ->
305
    fprintf fmt "link %a" print_ck_long ck'
306
  | Ccarrying (cr,ck') ->
307
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
308

  
309 320
(** [period ck] returns the period of [ck]. Expects a constant pclock
310 321
    expression belonging to the correct clock set. *)
311 322
let rec period ck =
......
518 529
    let ck = simplify ck in
519 530
    match ck.cdesc with
520 531
    | Carrow (ck1,ck2) ->
521
      fprintf fmt "%a->%a" aux ck1 aux ck2
532
      fprintf fmt "%a -> %a" aux ck1 aux ck2
522 533
    | Ctuple cklist ->
523 534
      fprintf fmt "(%a)" 
524 535
	(fprintf_list ~sep:" * " aux) cklist
src/compiler_common.ml
73 73
    Parse.report_error err;
74 74
    raise exc
75 75
  | Corelang.Error (loc, err) as exc ->
76
    eprintf "Parsing error %a%a@."
76
    eprintf "Parsing error: %a%a@."
77 77
      Corelang.pp_error err
78 78
      Location.pp_loc loc;
79 79
    raise exc
......
83 83
  try
84 84
    Stateless.check_prog decls
85 85
  with (Stateless.Error (loc, err)) as exc ->
86
    eprintf "Stateless status error %a%a@."
86
    eprintf "Stateless status error: %a%a@."
87 87
      Stateless.pp_error err
88 88
      Location.pp_loc loc;
89 89
    raise exc
......
95 95
      try
96 96
	Typing.type_prog env decls
97 97
      with (Types.Error (loc,err)) as exc ->
98
	eprintf "Typing error %a%a@."
98
	eprintf "Typing error: %a%a@."
99 99
	  Types.pp_error err
100 100
	  Location.pp_loc loc;
101 101
	raise exc
......
112 112
      try
113 113
	Clock_calculus.clock_prog env decls
114 114
      with (Clocks.Error (loc,err)) as exc ->
115
	eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc;
115
	eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
116 116
	raise exc
117 117
    end
118 118
  in
......
176 176
    Stateless.check_compat header
177 177
  with
178 178
  | (Types.Error (loc,err)) as exc ->
179
    eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@."
180
      Types.pp_error err;
179
    eprintf "Type mismatch between computed type and declared type in lustre interface file: %a%a@."
180
      Types.pp_error err
181
      Location.pp_loc loc;
181 182
    raise exc
182 183
  | Clocks.Error (loc, err) as exc ->
183
    eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@."
184
      Clocks.pp_error err;
184
    eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a%a@."
185
      Clocks.pp_error err
186
      Location.pp_loc loc;
185 187
    raise exc
186 188
  | Stateless.Error (loc, err) as exc ->
187
    eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
188
      Stateless.pp_error err;
189
    eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a%a@."
190
      Stateless.pp_error err
191
      Location.pp_loc loc;
189 192
    raise exc
190 193

  
191 194
let is_stateful topdecl =
src/liveness.ml
121 121
    | None           -> []
122 122
    | Some (_, args) -> List.fold_right (fun e r -> match e.expr_desc with Expr_ident id -> id::r | _ -> r) args [] in
123 123
  fun v -> is_aliasable v && List.mem v.var_id inputs_var
124

  
124
(*
125
    let res =
126
is_aliasable v && List.mem v.var_id inputs_var
127
    in (Format.eprintf "aliasable %s by %s = %B@." var v.var_id res; res)
128
*)
125 129
(* replace variable [v] by [v'] in graph [g].
126 130
   [v'] is a dead variable
127 131
*)
......
171 175
  end
172 176

  
173 177
(* tests whether a variable [v] may be (re)used instead of [var]. The conditions are:
178
   - [v] has been really used ([v] is its own representative)
174 179
   - same type
175 180
   - [v] is not an aliasable input of the equation defining [var]
176 181
   - [v] is not one of the current heads (which contain [var])
177
   - the representative of [v] is not currently in use
182
   - [v] is not currently in use
178 183
 *)
179 184
let eligible node ctx heads var v =
180
     Typing.eq_ground var.var_type v.var_type
185
     Hashtbl.find ctx.policy v.var_id == v
186
  && Typing.eq_ground (Types.unclock_type var.var_type) (Types.unclock_type v.var_type)
181 187
  && not (is_aliasable_input node var.var_id v)
182 188
  && not (List.exists (fun h -> h.var_id = v.var_id) heads)
183
  && let repr_v = Hashtbl.find ctx.policy v.var_id
184
     in not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id repr_v.var_id) ctx.evaluated)
189
  && (*let repr_v = Hashtbl.find ctx.policy v.var_id*)
190
     not (Disjunction.CISet.exists (fun p -> IdentDepGraph.mem_edge ctx.dep_graph p.var_id v.var_id) ctx.evaluated)
185 191

  
186 192
let compute_reuse node ctx heads var =
187 193
  let disjoint = Hashtbl.find ctx.disjoint var.var_id in
188 194
  let locally_reusable v =
189 195
    IdentDepGraph.fold_pred (fun p r -> r && Disjunction.CISet.exists (fun d -> p = d.var_id) disjoint) ctx.dep_graph v.var_id true in
190 196
  let eligibles = Disjunction.CISet.filter (eligible node ctx heads var) ctx.evaluated in
197
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "eligibles:%a@." Disjunction.pp_ciset eligibles);
191 198
  let quasi_dead, live = Disjunction.CISet.partition locally_reusable eligibles in
199
  Log.report ~level:7 (fun fmt -> Format.fprintf fmt "live:%a@." Disjunction.pp_ciset live);
192 200
  try
193 201
    let disjoint_live = Disjunction.CISet.inter disjoint live in
202
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "disjoint live:%a@." Disjunction.pp_ciset disjoint_live);
194 203
    let reuse = Disjunction.CISet.max_elt disjoint_live in
204
    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
195 205
    begin
196 206
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
197
      Hashtbl.add ctx.policy var.var_id (Hashtbl.find ctx.policy reuse.var_id);
207
      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
208
      Hashtbl.add ctx.policy var.var_id reuse;
198 209
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
199 210
      (*Format.eprintf "%s reused by live@." var.var_id;*)
200 211
    end
201 212
  with Not_found ->
202 213
  try
203 214
    let dead = Disjunction.CISet.filter (fun v -> is_graph_root v.var_id ctx.dep_graph) quasi_dead in
215
    Log.report ~level:7 (fun fmt -> Format.fprintf fmt "dead:%a@." Disjunction.pp_ciset dead);
204 216
    let reuse = Disjunction.CISet.choose dead in
217
    (*let reuse' = Hashtbl.find ctx.policy reuse.var_id in*)
205 218
    begin
206 219
      IdentDepGraph.add_edge ctx.dep_graph var.var_id reuse.var_id;
207
      Hashtbl.add ctx.policy var.var_id (Hashtbl.find ctx.policy reuse.var_id);
220
      (*if reuse != reuse' then IdentDepGraph.add_edge ctx.dep_graph reuse.var_id reuse'.var_id;*)
221
      Hashtbl.add ctx.policy var.var_id reuse;
208 222
      ctx.evaluated <- Disjunction.CISet.add var ctx.evaluated;
209 223
      (*Format.eprintf "%s reused by dead %a@." var.var_id Disjunction.pp_ciset dead;*)
210 224
    end
......
225 239
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new context:%a@." pp_context ctx);
226 240
    let heads = List.map (fun v -> get_node_var v node) (List.hd !sort) in
227 241
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "NEW HEADS:");
228
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s " head.var_id)) heads;
242
    List.iter (fun head -> Log.report ~level:6 (fun fmt -> Format.fprintf fmt "%s (%a)" head.var_id Printers.pp_node_eq (get_node_eq head.var_id node))) heads;
229 243
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "@.");
230 244
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "COMPUTE_DEPENDENCIES@.");
231 245
    compute_dependencies heads ctx;
src/location.ml
67 67

  
68 68

  
69 69
let pp_loc fmt loc =
70
  if loc == dummy_loc then () else
70 71
  let filename = loc.loc_start.Lexing.pos_fname in
71 72
  let line = loc.loc_start.Lexing.pos_lnum in
72 73
  let start_char =
src/log.ml
11 11

  
12 12
let report ~level:level p =
13 13
if !Options.verbose_level >= level then
14
  Format.eprintf "%t" p
14
  begin
15
    Format.eprintf "%t" p;
16
    Format.pp_print_flush Format.err_formatter ()
17
  end
15 18

  
16 19
(* Local Variables: *)
17 20
(* compile-command:"make -C .." *)
src/main_lustre_compiler.ml
70 70
	begin
71 71
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating compiled header file %s@," header_name);
72 72
       	  Lusic.write_lusic false (Lusic.extract_header dirname basename prog) destname lusic_ext;
73
(*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
73
	  (*List.iter (fun top_decl -> Format.eprintf "lusic: %a@." Printers.pp_decl top_decl) lusic.Lusic.contents;*)
74 74
	  Lusic.print_lusic_to_h destname lusic_ext
75 75
	end
76 76
      else
......
85 85
	end
86 86
  end
87 87

  
88

  
89

  
88 90
(* compile a .lus source file *)
89 91
let rec compile_source dirname basename extension =
90 92

  
......
155 157

  
156 158
  (* Compatibility with Lusi *)
157 159
  (* Checking the existence of a lusi (Lustre Interface file) *)
158
  match !Options.output with
160
  (match !Options.output with
159 161
    "C" ->
160 162
      begin
161 163
        let extension = ".lusi" in
162 164
        compile_source_to_header prog computed_types_env computed_clocks_env dirname basename extension;
163 165
      end
164
   |_ -> ();
166
   |_ -> ());
165 167

  
166 168
  Typing.uneval_prog_generics prog;
167 169
  Clock_calculus.uneval_prog_generics prog;
......
299 301
	let source_file = destname ^ ".smt2" in (* Could be changed *)
300 302
	let source_out = open_out source_file in
301 303
	let fmt = formatter_of_out_channel source_out in
302
        Log.report ~level:1 (fun fmt -> fprintf fmt "@.. hornification@,");
303
	Horn_backend.translate fmt basename prog machine_code;
304
	Log.report ~level:1 (fun fmt -> fprintf fmt ".. hornification@,");
305
        Horn_backend.translate fmt basename prog machine_code;
304 306
	(* Tracability file if option is activated *)
305 307
	if !Options.traces then (
306
	  let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
307
	  let traces_out = open_out traces_file in
308
	  let fmt = formatter_of_out_channel traces_out in
309
          Log.report ~level:1 (fun fmt -> fprintf fmt "@.. tracing info@,");
310
	  Horn_backend.traces_file fmt basename prog machine_code;
308
	let traces_file = destname ^ ".traces.xml" in (* Could be changed *)
309
	let traces_out = open_out traces_file in
310
	let fmt = formatter_of_out_channel traces_out in
311
        Log.report ~level:1 (fun fmt -> fprintf fmt ".. tracing info@,");
312
	Horn_backend.traces_file fmt basename prog machine_code;
311 313
	)
312 314
      end
313 315
    | "lustre" ->
......
323 325
    | _ -> assert false
324 326
  in
325 327
  begin
326
    Log.report ~level:1 (fun fmt -> fprintf fmt "@.. done @ @]@.");
328
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
327 329
  (* We stop the process here *)
328 330
    exit 0
329 331
  end
src/options.ml
13 13
let include_path = Version.include_path
14 14

  
15 15
let print_version () =
16
  Format.printf "Lustrec compiler, version %s@." version;
16
  Format.printf "Lustrec compiler, version %s (dev)@." version;
17 17
  Format.printf "Include directory: %s@." include_path
18 18

  
19 19
let main_node = ref ""
......
37 37

  
38 38
let horntraces = ref false
39 39
let horn_cex = ref false
40
let horn_query = ref false
40
let horn_query = ref true
41 41

  
42 42

  
43 43
let options =
......
67 67
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
68 68
    "-version", Arg.Unit print_version, " displays the version";]
69 69

  
70

  
70 71
let get_witness_dir filename =
71 72
  (* Make sure the directory exists *)
72 73
  let dir = !dest_dir ^ "/" ^ (Filename.basename filename) ^ "_witnesses" in
src/parserLustreSpec.mly
73 73
%nonassoc UMINUS
74 74

  
75 75
%start lustre_annot
76
%type <LustreSpec.expr_annot> lustre_annot
76
%type <LustreSpec.ident -> LustreSpec.expr_annot> lustre_annot
77 77

  
78 78
%start lustre_spec
79 79
%type <LustreSpec.node_annot> lustre_spec
......
287 287
| STRING {Const_string $1}
288 288

  
289 289
lustre_annot:
290
lustre_annot_list EOF { $1 }
290
lustre_annot_list EOF { fun node_id -> $1 }
291 291

  
292 292
lustre_annot_list:
293 293
  { [] } 
src/parser_lustre.mly
43 43
let pop_node () = try node_stack := List.tl !node_stack with _ -> assert false
44 44
let get_current_node () = try List.hd !node_stack with _ -> assert false
45 45

  
46
let rec fby expr n init =
47
  if n<=1 then
48
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre expr)))
49
  else
50
    mkexpr (Expr_arrow (init, mkexpr (Expr_pre (fby expr (n-1) init))))
51
  
46 52
%}
47 53

  
48 54
%token <int> INT
......
403 409
| node_ident LPAR expr RPAR EVERY expr
404 410
    {mkexpr (Expr_appl ($1, $3, Some $6))}
405 411
| node_ident LPAR tuple_expr RPAR
406
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), None))}
412
    {
413
      let id=$1 in
414
      let args=List.rev $3 in
415
      match id, args with
416
      | "fbyn", [expr;n;init] ->
417
	let n = match n.expr_desc with
418
	  | Expr_const (Const_int n) -> n
419
	  | _ -> assert false
420
	in
421
	fby expr n init
422
      | _ -> mkexpr (Expr_appl ($1, mkexpr (Expr_tuple args), None))
423
    }
407 424
| node_ident LPAR tuple_expr RPAR EVERY expr
408
    {mkexpr (Expr_appl ($1, mkexpr (Expr_tuple (List.rev $3)), Some $6)) }
425
    {
426
      let id=$1 in
427
      let args=List.rev $3 in
428
      let clock=$6 in
429
      if id="fby" then
430
	assert false (* TODO Ca veut dire quoi fby (e,n,init) every c *)
431
      else
432
	mkexpr (Expr_appl (id, mkexpr (Expr_tuple args), Some clock)) 
433
    }
409 434

  
410 435
/* Boolean expr */
411 436
| expr AND expr 
src/printers.ml
24 24
    pp_set_all_formatter_output_functions fmt out flush newline spaces;
25 25
  end
26 26

  
27
let rec print_dec_struct_ty_field fmt (label, cty) =
28
  fprintf fmt "%a : %a" pp_print_string label print_dec_ty cty
29
and print_dec_ty fmt cty =
30
  match (*get_repr_type*) cty with
31
  | Tydec_any -> fprintf fmt "Any"
32
  | Tydec_int -> fprintf fmt "int"
33
  | Tydec_real 
34
  | Tydec_float -> fprintf fmt "real"
35
  | Tydec_bool -> fprintf fmt "bool"
36
  | Tydec_clock cty' -> fprintf fmt "%a clock" print_dec_ty cty'
37
  | Tydec_const c -> fprintf fmt "%s" c
38
  | Tydec_enum taglist -> fprintf fmt "enum {%a }"
39
      (Utils.fprintf_list ~sep:", " pp_print_string) taglist
40
  | Tydec_struct fieldlist -> fprintf fmt "struct {%a }"
41
      (Utils.fprintf_list ~sep:"; " print_dec_struct_ty_field) fieldlist
42
  | Tydec_array (d, cty') -> fprintf fmt "%a^%a" print_dec_ty cty' Dimension.pp_dimension d
27 43

  
28 44
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
29 45

  
......
31 47

  
32 48
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
33 49

  
34
let pp_node_var fmt id = fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock
35

  
36
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
37

  
38 50
let pp_quantifiers fmt (q, vars) =
39 51
  match q with
40 52
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
......
125 137
  in
126 138
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
127 139
    
128
	
140
(*
141
let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock
142
*)
143
let pp_node_var fmt id =
144
  begin
145
    fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock;
146
    match id.var_dec_value with
147
    | None -> () 
148
    | Some v -> fprintf fmt " = %a" pp_expr v
149
  end 
150

  
151
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
152

  
129 153
let pp_node_eq fmt eq = 
130 154
  fprintf fmt "%a = %a;" 
131 155
    pp_eq_lhs eq.eq_lhs
src/scheduling.ml
31 31
   For variables still unrelated, standard compare is used to choose the minimal element.
32 32
   This priority is used since it helps a lot in factorizing generated code.
33 33
   Moreover, the dependency graph is browsed in a depth-first manner whenever possible,
34
   to improve the behavior of optimization algorithms applied in forthcoming compilation steps.
34
   to improve the behavior of optimization algorithms applied in forthcoming compilation steps. 
35 35
   In the following functions:
36 36
   - [eq_equiv] is the equivalence relation between vars of the same equation lhs
37 37
   - [g] the (imperative) graph to be topologically sorted
......
46 46
 List.exists ExprDep.is_instance_var (IdentDepGraph.succ g choice)
47 47

  
48 48
(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt [eq_equiv],
49
   then removes [v] from [g]
49
   then removes [v] from [g] 
50 50
*)
51 51
let add_successors eq_equiv g v pending frontier =
52 52
  let succs_v = IdentDepGraph.succ g v in
53 53
  begin
54 54
    IdentDepGraph.remove_vertex g v;
55
    List.iter
56
      (fun v' ->
57
	if is_graph_root v' g then
58
	  (if eq_equiv v v' then
59
	      pending := ISet.add v' !pending
55
    List.iter 
56
      (fun v' -> 
57
	if is_graph_root v' g then 
58
	  (if eq_equiv v v' then 
59
	      pending := ISet.add v' !pending 
60 60
	   else
61 61
	      frontier := ISet.add v' !frontier)
62 62
      ) succs_v;
......
134 134
      with Not_found -> false in
135 135

  
136 136
    let n', g = global_dependency n in
137
    Log.report ~level:5
138
      (fun fmt ->
137
    Log.report ~level:5 
138
      (fun fmt -> 
139 139
	Format.fprintf fmt
140
	  "dependency graph for node %s: %a"
140
	  "dependency graph for node %s: %a" 
141 141
	  n'.node_id
142 142
	  pp_dep_graph g
143 143
      );
144

  
144
    
145 145
    (* TODO X: extend the graph with inputs (adapt the causality analysis to deal with inputs
146 146
     compute: coi predecessors of outputs
147 147
     warning (no modification) when memories are non used (do not impact output) or when inputs are not used (do not impact output)
......
166 166
    if !Options.print_reuse
167 167
    then
168 168
      begin
169
	Log.report ~level:0
170
	  (fun fmt ->
169
	Log.report ~level:0 
170
	  (fun fmt -> 
171 171
	    Format.fprintf fmt
172 172
	      "OPT:%B@." (try (Hashtbl.iter (fun s1 v2 -> if s1 = v2.var_id then raise Not_found) reuse; false) with Not_found -> true)
173 173
	  );
174
	Log.report ~level:0
175
	  (fun fmt ->
174
	Log.report ~level:0 
175
	  (fun fmt -> 
176 176
	    Format.fprintf fmt
177
	      "OPT:clock disjoint map for node %s: %a"
177
	      "OPT:clock disjoint map for node %s: %a" 
178 178
	      n'.node_id
179 179
	      Disjunction.pp_disjoint_map disjoint
180 180
	  );
181
	Log.report ~level:0
182
	  (fun fmt ->
181
	Log.report ~level:0 
182
	  (fun fmt -> 
183 183
	    Format.fprintf fmt
184
	      "OPT:reuse policy for node %s: %a"
184
	      "OPT:reuse policy for node %s: %a" 
185 185
	      n'.node_id
186 186
	      Liveness.pp_reuse_policy reuse
187 187
	  );
......
196 196
  List.fold_right (
197 197
    fun top_decl (accu_prog, sch_map)  ->
198 198
      match top_decl.top_decl_desc with
199
	| Node nd ->
199
	| Node nd -> 
200 200
	  let nd', report = schedule_node nd in
201
	  {top_decl with top_decl_desc = Node nd'}::accu_prog,
201
	  {top_decl with top_decl_desc = Node nd'}::accu_prog, 
202 202
	  IMap.add nd.node_id report sch_map
203 203
	| _ -> top_decl::accu_prog, sch_map
204
    )
204
    ) 
205 205
    prog
206 206
    ([],IMap.empty)
207 207

  
......
210 210
  | []  -> assert false
211 211
  | [v] -> Format.fprintf fmt "%s" v
212 212
  | _   -> Format.fprintf fmt "(%a)" (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) vl
213

  
213
 
214 214
let pp_schedule fmt node_schs =
215 215
 IMap.iter
216 216
   (fun nd report ->
src/types.ml
41 41
    Unbound_value of ident  
42 42
  | Already_bound of ident
43 43
  | Already_defined of ident
44
  | Undefined_var of (unit IMap.t)
44
  | Undefined_var of ISet.t
45 45
  | Declared_but_undefined of ident
46 46
  | Unbound_type of ident
47 47
  | Not_a_dimension
......
83 83
    fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2
84 84
  | Ttuple tylist ->
85 85
    fprintf fmt "(%a)"
86
      (Utils.fprintf_list ~sep:"*" print_ty) tylist
86
      (Utils.fprintf_list ~sep:" * " print_ty) tylist
87 87
  | Tenum taglist ->
88 88
    fprintf fmt "enum {%a }"
89 89
      (Utils.fprintf_list ~sep:", " pp_print_string) taglist
......
158 158
    fprintf fmt "Expecting %d argument(s) for homomorphic extension, found %d@." ar1 ar2
159 159
  | Type_mismatch id ->
160 160
    fprintf fmt "Definition and declaration of type %s don't agree@." id
161
  | Undefined_var vmap ->
161
  | Undefined_var vset ->
162 162
    fprintf fmt "No definition provided for variable(s): %a@."
163 163
      (Utils.fprintf_list ~sep:"," pp_print_string)
164
      (fst (Utils.list_of_imap vmap))
164
      (ISet.elements vset)
165 165
  | Declared_but_undefined id ->
166 166
     fprintf fmt "%s is declared but not defined@." id
167 167
  | Type_clash (ty1,ty2) ->
......
214 214
 | Tclock ty -> Some ty
215 215
 | _         -> None
216 216

  
217
let unclock_type ty =
218
  let ty = repr ty in
219
  match ty.tdesc with
220
  | Tclock ty' -> ty'
221
  | _          -> ty
222

  
217 223
let rec is_dimension_type ty =
218 224
 match (repr ty).tdesc with
219 225
 | Tint
......
254 260
let array_type_dimension ty =
255 261
  match (dynamic_type ty).tdesc with
256 262
  | Tarray (d, _) -> d
257
  | _             -> assert false
263
  | _             -> (Format.eprintf "internal error: Types.array_type_dimension %a@." print_ty ty; assert false)
258 264

  
259 265
let rec array_type_multi_dimension ty =
260 266
  match (dynamic_type ty).tdesc with
......
264 270
let array_element_type ty =
265 271
  match (dynamic_type ty).tdesc with
266 272
  | Tarray (_, ty') -> ty'
267
  | _               -> assert false
273
  | _               -> (Format.eprintf "internal error: Types.array_element_type %a@." print_ty ty; assert false)
268 274

  
269 275
let rec array_base_type ty =
270 276
  let ty = repr ty in
src/typing.ml
111 111
  | Tydec_struct fl -> Type_predef.type_struct (List.map (fun (f, ty) -> (f, type_coretype type_dim ty)) fl)
112 112
  | Tydec_array (d, ty) ->
113 113
    begin
114
      let d = Dimension.copy (ref []) d in
114 115
      type_dim d;
115 116
      Type_predef.type_array d (type_coretype type_dim ty)
116 117
    end
......
311 312
  then raise (Error (loc, Not_a_constant))
312 313

  
313 314
let rec type_add_const env const arg targ =
315
(*Format.eprintf "Typing.type_add_const %a %a@." Printers.pp_expr arg Types.print_ty targ;*)
314 316
  if const
315 317
  then let d =
316 318
	 if is_dimension_type targ
......
357 359

  
358 360
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
359 361
and type_dependent_call env in_main loc const f targs =
362
(*Format.eprintf "Typing.type_dependent_call %s@." f;*)
360 363
  let tins, touts = new_var (), new_var () in
361 364
  let tfun = Type_predef.type_arrow tins touts in
362 365
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
......
367 370
    begin
368 371
      List.iter2 (fun (a,t) ti ->
369 372
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
370
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
371
      touts
373
	in try_unify ~sub:true ti t' a.expr_loc;
374
      ) targs tins;
375
(*Format.eprintf "Typing.type_dependent_call END@.";*)
376
      touts;
372 377
    end
373 378

  
374 379
(* type a simple call without dependent types 
......
506 511

  
507 512
(** [type_eq env eq] types equation [eq] in environment [env] *)
508 513
let type_eq env in_main undefined_vars eq =
514
(*Format.eprintf "Typing.type_eq %a@." Printers.pp_node_eq eq;*)
509 515
  (* Check undefined variables, type lhs *)
510 516
  let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
511 517
  let ty_lhs = type_expr env in_main false expr_lhs in
512 518
  (* Check multiple variable definitions *)
513 519
  let define_var id uvars =
514
    try
515
      ignore(IMap.find id uvars);
516
      IMap.remove id uvars
517
    with Not_found ->
518
      raise (Error (eq.eq_loc, Already_defined id))
520
    if ISet.mem id uvars
521
    then ISet.remove id uvars
522
    else raise (Error (eq.eq_loc, Already_defined id))
519 523
  in
520 524
  (* check assignment of declared constant, assignment of clock *)
521 525
  let ty_lhs =
......
566 570
 | _                   -> ()
567 571

  
568 572
let type_var_decl vd_env env vdecl =
573
(*Format.eprintf "Typing.type_var_decl START %a:%a@." Printers.pp_var vdecl Printers.print_dec_ty vdecl.var_dec_type.ty_dec_desc;*)
569 574
  check_type_declaration vdecl.var_loc vdecl.var_dec_type.ty_dec_desc;
570 575
  let eval_const id = Types.get_static_value (Env.lookup_value env id) in
571 576
  let type_dim d =
572 577
    begin
573 578
      type_subtyping_arg (env, vd_env) false true (expr_of_dimension d) Type_predef.type_int;
579

  
574 580
      Dimension.eval Basic_library.eval_env eval_const d;
575 581
    end in
576 582
  let ty = type_coretype type_dim vdecl.var_dec_type.ty_dec_desc in
577
  let ty_status =
583

  
584
  let ty_static =
578 585
    if vdecl.var_dec_const
579
    then Type_predef.type_static (Dimension.mkdim_var ()) ty
586
    then  Type_predef.type_static (Dimension.mkdim_var ()) ty
580 587
    else ty in
581
  let new_env = Env.add_value env vdecl.var_id ty_status in
588
  (match vdecl.var_dec_value with
589
  | None   -> ()
590
  | Some v -> type_subtyping_arg (env, vd_env) false ~sub:false true v ty_static);
591
  try_unify ty_static vdecl.var_type vdecl.var_loc;
592
  let new_env = Env.add_value env vdecl.var_id ty_static in
582 593
  type_coreclock (new_env,vd_env) vdecl.var_dec_clock vdecl.var_id vdecl.var_loc;
583
  vdecl.var_type <- ty_status;
594
(*Format.eprintf "END %a@." Types.print_ty ty_static;*)
584 595
  new_env
585 596

  
586 597
let type_var_decl_list vd_env env l =
......
612 623
  let new_env = Env.overwrite env delta_env in
613 624
  let undefined_vars_init =
614 625
    List.fold_left
615
      (fun uvs v -> IMap.add v.var_id () uvs)
616
      IMap.empty vd_env_ol in
626
      (fun uvs v -> ISet.add v.var_id uvs)
627
      ISet.empty vd_env_ol in
617 628
  let undefined_vars =
618 629
    List.fold_left (type_eq (new_env, vd_env) is_main) undefined_vars_init (get_node_eqs nd)
619 630
  in
......
624 635
  )  nd.node_asserts;
625 636
  
626 637
  (* check that table is empty *)
627
  if (not (IMap.is_empty undefined_vars)) then
638
  let local_consts = List.fold_left (fun res vdecl -> if vdecl.var_dec_const then ISet.add vdecl.var_id res else res) ISet.empty nd.node_locals in
639
  let undefined_vars = ISet.diff undefined_vars local_consts in
640
  if (not (ISet.is_empty undefined_vars)) then
628 641
    raise (Error (loc, Undefined_var undefined_vars));
629 642
  let ty_ins = type_of_vlist nd.node_inputs in
630 643
  let ty_outs = type_of_vlist nd.node_outputs in
......
671 684
      try
672 685
	type_node env nd decl.top_decl_loc
673 686
      with Error (loc, err) as exc -> (
674
	if !Options.global_inline then
687
	(*if !Options.global_inline then
675 688
	  Format.eprintf "Type error: failing node@.%a@.@?"
676 689
	    Printers.pp_node nd
677
	;
690
	;*)
678 691
	raise exc)
679 692
  )
680 693
  | ImportedNode nd ->
......
745 758

  
746 759
let check_typedef_top decl =
747 760
(*Format.eprintf "check_typedef %a@." Printers.pp_short_decl decl;*)
748
(*Printers.pp_var_type_dec_desc (typedef_of_top decl).tydef_id*)
761
(*Format.eprintf "%a" Printers.pp_typedef (typedef_of_top decl);*)
749 762
(*Format.eprintf "%a" Corelang.print_type_table ();*)
750 763
  match decl.top_decl_desc with
751 764
  | TypeDef ty ->
......
755 768
       try Hashtbl.find type_table (Tydec_const (typedef_of_top decl).tydef_id)
756 769
       with Not_found -> raise (Error (decl.top_decl_loc, Declared_but_undefined ("type "^ ty.tydef_id))) in
757 770
     let owner' = decl'.top_decl_owner in
771
(*Format.eprintf "def owner = %s@.decl owner = %s@." owner' owner;*)
758 772
     let itf' = decl'.top_decl_itf in
759 773
     (match decl'.top_decl_desc with
760 774
     | Const _ | Node _ | ImportedNode _ -> assert false
src/version.ml
1 1

  
2
let number = "1.0-Unversioned directory"
2
let number = "1.0-449"
3 3

  
4 4
let prefix = "/usr/local"
5 5

  

Also available in: Unified diff