Project

General

Profile

Revision a38c681e

View differences:

src/causality.ml
457 457
     maybe removing shorter branches *)
458 458
  type disjoint_map = (ident, CISet.t) Hashtbl.t
459 459

  
460
  let pp_ciset fmt t =
461
    begin
462
      Format.fprintf fmt "{@ ";
463
      CISet.iter (fun s -> Format.fprintf fmt "%a@ " Printers.pp_var_name s) t;
464
      Format.fprintf fmt "}@."
465
    end
466

  
460 467
  let clock_disjoint_map vdecls =
461 468
    let map = Hashtbl.create 23 in
462 469
    begin
src/clock_calculus.ml
664 664
  | Expr_fby (e1,e2)
665 665
  | Expr_arrow (e1,e2) ->
666 666
    let ck = clock_standard_args env [e1; e2] in
667
    unify_tuple_clock None ck;
667 668
    expr.expr_clock <- ck;
668 669
    ck
669 670
  | Expr_pre e -> (* todo : deal with phases as in tail ? *)
src/liveness.ml
98 98
  ISet.fold
99 99
    (fun var unused -> ISet.diff unused (cone_of_influence g var))
100 100
    (ISet.union outputs mems)
101
    (ISet.union inputs mems) 
101
    (ISet.union inputs mems)
102 102

  
103
(* Computes the set of output and mem variables of [node].
104
   We don't reuse input variables, due to possible aliasing *)
105
let node_non_locals node =
106
  let mems = ExprDep.node_memory_variables node in
107
 List.fold_left (fun non_loc v -> if ISet.mem v.var_id mems then non_loc else ISet.add v.var_id non_loc) (ExprDep.node_output_variables node) node.node_locals
108

  
109
(* checks whether a variable is aliasable,
110
   depending on its (address) type *)
111
let is_aliasable var =
112
 Types.is_address_type var.var_type
113
 
114 103
(* computes the set of potentially reusable variables.
115 104
   We don't reuse input variables, due to possible aliasing *)
116 105
let node_reusable_variables node =
......
123 112

  
124 113
(* Recursively removes useless variables,
125 114
   i.e. variables that are current roots of the dep graph [g]
126
   and returns [reusable] such roots *)
127
let remove_local_roots reusable g =
115
   and returns [locals] and [evaluated] such roots *)
116
let remove_local_roots locals evaluated g =
128 117
  let rem = ref true in
129 118
  let roots = ref Disjunction.CISet.empty in
130 119
  while !rem
131 120
  do
132 121
    rem := false;
133 122
    let new_roots = graph_roots g in
134
    let reusable_roots = Disjunction.CISet.filter (fun v -> List.mem v.var_id new_roots) reusable in
123
    let reusable_roots = Disjunction.CISet.filter (fun v -> (List.mem v.var_id new_roots) && (Disjunction.CISet.mem v locals)) evaluated in
135 124
    if not (Disjunction.CISet.is_empty reusable_roots) then
136 125
      begin
137 126
	rem := true;
......
141 130
  done;
142 131
  !roots
143 132

  
133
(* checks whether a variable is aliasable,
134
   depending on its (address) type *)
135
let is_aliasable var =
136
 Types.is_address_type var.var_type
137
 
144 138
(* checks whether a variable [v] is an input of the [var] equation, with an address type.
145 139
   if so, [var] could not safely reuse/alias [v], should [v] be dead in the caller node,
146 140
   because [v] may not be dead in the callee node when [var] is assigned *)
......
163 157
    IdentDepGraph.remove_vertex g v
164 158
  end
165 159

  
166
(* computes the dead dependencies of variable [var] in graph [g],
167
   once [var] has been evaluated *)
168
let compute_dead_dependencies reusable var g dead =
160
(* computes the reusable dependencies of variable [var] in graph [g],
161
   once [var] has been evaluated
162
   [dead] is the set of evaluated and dead variables
163
   [eval] is the set of evaluated variables
164
*)
165
let compute_reusable_dependencies locals evaluated reusable var g =
169 166
  begin
170
    IdentDepGraph.iter_succ (IdentDepGraph.remove_edge g var) g var;
171
    dead := Disjunction.CISet.union (remove_local_roots reusable g) !dead;
167
    Log.report ~level:2 (fun fmt -> Format.fprintf fmt "compute_reusable_dependencies %a %a %a %a %a@." Disjunction.pp_ciset locals Disjunction.pp_ciset !evaluated Disjunction.pp_ciset !reusable Printers.pp_var_name var pp_dep_graph g);
168
    evaluated := Disjunction.CISet.add var !evaluated;
169
    IdentDepGraph.iter_succ (IdentDepGraph.remove_edge g var.var_id) g var.var_id;
170
    reusable := Disjunction.CISet.union (remove_local_roots locals !evaluated g) !reusable;
172 171
  end
173 172

  
174 173
let compute_reuse_policy node schedule disjoint g =
175
  let reusable = node_reusable_variables node in
174
  let locals = node_reusable_variables node in
176 175
  let sort = ref schedule in
177
  let dead = ref Disjunction.CISet.empty in
176
  let evaluated = ref Disjunction.CISet.empty in
177
  let reusable = ref Disjunction.CISet.empty in
178 178
  let policy = Hashtbl.create 23 in
179
  while false (*!sort <> []*)
179
  while !sort <> []
180 180
  do
181 181
    let head = get_node_var (List.hd !sort) node in
182
    compute_dead_dependencies reusable head.var_id g dead;
182
    compute_reusable_dependencies locals evaluated reusable head g;
183 183
    let aliasable = is_aliasable_input node head.var_id in
184 184
    let eligible v = Typing.eq_ground head.var_type v.var_type && not (aliasable v) in
185 185
    let reuse =
186 186
      try
187 187
	let disj = Hashtbl.find disjoint head.var_id in
188
	Disjunction.CISet.max_elt (Disjunction.CISet.filter (fun v -> (eligible v) && not (Disjunction.CISet.mem v !dead)) disj)
188
	Disjunction.CISet.max_elt (Disjunction.CISet.filter (fun v -> (eligible v) && (Disjunction.CISet.mem v !evaluated) && not (Disjunction.CISet.mem v !reusable)) disj)
189 189
      with Not_found ->
190 190
      try
191
	Disjunction.CISet.choose (Disjunction.CISet.filter (fun v -> eligible v) !dead)
191
	Disjunction.CISet.choose (Disjunction.CISet.filter (fun v -> eligible v) !reusable)
192 192
      with Not_found -> head in
193
    dead := Disjunction.CISet.remove reuse !dead;
193
    reusable := Disjunction.CISet.remove reuse !reusable;
194 194
    Disjunction.replace_in_disjoint_map disjoint head reuse;
195 195
    merge_in_dep_graph head.var_id reuse.var_id g;
196 196
    Hashtbl.add policy head.var_id reuse;
197
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "reuse %s instead of %s@." reuse.var_id head.var_id);
198
    Log.report ~level:6 (fun fmt -> Format.fprintf fmt "new disjoint:%a@." Disjunction.pp_disjoint_map disjoint);
199
    Log.report ~level:6 
197
    Log.report ~level:2 (fun fmt -> Format.fprintf fmt "reuse %s instead of %s@." reuse.var_id head.var_id);
198
    Log.report ~level:1 (fun fmt -> Format.fprintf fmt "new disjoint:%a@." Disjunction.pp_disjoint_map disjoint);
199
    Log.report ~level:2 
200 200
      (fun fmt -> Format.fprintf fmt "new dependency graph:%a@." pp_dep_graph g);
201 201
    sort := List.tl !sort;
202 202
  done;
src/machine_code.ml
271 271
let join_guards_list insts =
272 272
 List.fold_right join_guards insts []
273 273

  
274
let find_eq x eqs =
275
  let rec aux accu eqs =
276
      match eqs with
277
	| [] ->
278
	  begin
279
	    Format.eprintf "Looking for variable %a in the following equations@.%a@."
280
	      Format.pp_print_string x
281
	      Printers.pp_node_eqs eqs;
282
	    assert false
283
	  end
284
	| hd::tl -> 
285
	  if List.mem x hd.eq_lhs then hd, accu@tl else aux (hd::accu) tl
286
    in
287
    aux [] eqs
288

  
289 274
(* specialize predefined (polymorphic) operators
290 275
   wrt their instances, so that the C semantics 
291 276
   is preserved *)
......
430 415
      assert false
431 416
    end
432 417

  
418
let find_eq xl eqs =
419
  let rec aux accu eqs =
420
      match eqs with
421
	| [] ->
422
	  begin
423
	    Format.eprintf "Looking for variables %a in the following equations@.%a@."
424
	      (Utils.fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) xl
425
	      Printers.pp_node_eqs eqs;
426
	    assert false
427
	  end
428
	| hd::tl -> 
429
	  if List.exists (fun x -> List.mem x hd.eq_lhs) xl then hd, accu@tl else aux (hd::accu) tl
430
    in
431
    aux [] eqs
432

  
433
(* Sort the set of equations of node [nd] according 
434
   to the computed schedule [sch]
435
*)
436
let sort_equations_from_schedule nd sch =
437
  let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in
438
  let eqs_rev, remainder =
439
    List.fold_left 
440
      (fun (accu, node_eqs_remainder) vl -> 
441
       if List.exists (fun eq -> List.exists (fun v -> List.mem v eq.eq_lhs) vl) accu
442
       then
443
	 (accu, node_eqs_remainder)
444
       else
445
	 let eq_v, remainder = find_eq vl node_eqs_remainder in
446
	 eq_v::accu, remainder
447
      ) 
448
      ([], split_eqs) 
449
      sch 
450
  in
451
  if List.length remainder > 0 then (
452
    Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
453
		   Printers.pp_node_eqs remainder
454
      		   Printers.pp_node_eqs nd.node_eqs;
455
    assert false);
456
  List.rev eqs_rev
457

  
433 458
let translate_eqs node args eqs =
434 459
  List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
435 460

  
436 461
let translate_decl nd sch =
437 462
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
438
  let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in
463

  
464
(*
439 465
  let eqs_rev, remainder = 
440 466
    List.fold_left 
441 467
      (fun (accu, node_eqs_remainder) v -> 
......
455 481
      ([], split_eqs) 
456 482
      sch 
457 483
  in
458
  if List.length remainder > 0 then (
459
    Format.eprintf "Equations not used are@.%a@.Full equation set is:@.%a@.@?"
460
	    Printers.pp_node_eqs remainder
461
      	    Printers.pp_node_eqs nd.node_eqs;
462
    assert false )
463
  ;
484
 *)
485
  let sorted_eqs = sort_equations_from_schedule nd sch in
464 486

  
465 487
  let init_args = ISet.empty, [], Utils.IMap.empty, List.fold_right (fun l -> ISet.add l) nd.node_locals ISet.empty, [] in
466 488
  (* memories, init instructions, node calls, local variables (including memories), step instrs *)
467
  let m, init, j, locals, s = translate_eqs nd init_args (List.rev eqs_rev) in
489
  let m, init, j, locals, s = translate_eqs nd init_args sorted_eqs in
468 490
  let mmap = Utils.IMap.fold (fun i n res -> (i, n)::res) j [] in
469 491
  {
470 492
    mname = nd;
src/main_lustre_compiler.ml
107 107
    let header = load_lusi true lusi_name in
108 108
    let _, declared_types_env, declared_clocks_env = check_lusi header in
109 109
        
110
    (* checking stateless status compatibility *)
111
    Stateless.check_compat header;
112 110

  
113 111
    (* checking type compatibility with computed types*)
114 112
    Typing.check_env_compat header declared_types_env computed_types_env;
......
116 114
    
117 115
    (* checking clocks compatibility with computed clocks*)
118 116
    Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
119
    Clock_calculus.uneval_prog_generics prog
117
    Clock_calculus.uneval_prog_generics prog;
118

  
119
    (* checking stateless status compatibility *)
120
    Stateless.check_compat header
120 121

  
121 122
    with Sys_error _ -> ( 
122 123
      (* Printing lusi file is necessary *)
......
199 200
  (* Sorting nodes *)
200 201
  let prog = SortProg.sort prog in
201 202

  
202
  (* Checking stateless/stateful status *)
203
  check_stateless_decls prog;
204

  
205 203
  (* Typing *)
206 204
  let computed_types_env = type_decls type_env prog in
207 205
  
208 206
  (* Clock calculus *)
209 207
  let computed_clocks_env = clock_decls clock_env prog in
210 208

  
209
  (* Checking stateless/stateful status *)
210
  check_stateless_decls prog;
211

  
211 212
  (* Perform global inlining *)
212 213
  let prog =
213 214
    if !Options.global_inline && 
src/normalization.ml
65 65
 match expr.expr_desc with
66 66
 | Expr_arrow (e1, e2) ->
67 67
    let loc = expr.expr_loc in
68
    let ck = expr.expr_clock in
68
    let ck = List.hd (Clocks.clock_list_of_clock expr.expr_clock) in
69 69
    { expr with expr_desc = Expr_ite (expr_once loc ck, e1, e2) }
70 70
 | _                   -> assert false
71 71

  
......
129 129

  
130 130
(* Create an alias for [expr], if none exists yet *)
131 131
let mk_expr_alias node (defs, vars) expr =
132
(*Format.eprintf "mk_expr_alias %a %a %a@." Printers.pp_expr expr Types.print_ty expr.expr_type Clocks.print_ck expr.expr_clock;*)
132 133
  match get_expr_alias defs expr with
133 134
  | Some eq ->
134 135
    let aliases = List.map (fun id -> List.find (fun v -> v.var_id = id) vars) eq.eq_lhs in
......
387 388
  *)
388 389
  let diff_vars = List.filter (fun v -> not (List.mem v node.node_locals) ) new_locals in
389 390
  let norm_traceability = {
390
    annots = 
391
    annots =
391 392
      List.map 
392 393
	(fun v -> 
393 394
	  let expr = substitute_expr diff_vars defs (
394
	    let eq = List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs in
395
	    let eq = try
396
		       List.find (fun eq -> eq.eq_lhs = [v.var_id]) defs 
397
	      with Not_found -> (Format.eprintf "var not found %s@." v.var_id; assert false) in
395 398
	    eq.eq_rhs) in 
396 399
	  let pair = mkeexpr expr.expr_loc (mkexpr expr.expr_loc (Expr_tuple [expr_of_ident v.var_id expr.expr_loc; expr])) in 
397 400
	  ["horn_backend";"trace"], pair 
398
    ) 
401
	)
399 402
    diff_vars ;
400 403
    annot_loc = Location.dummy_loc
401 404
  }
src/scheduling.ml
32 32
type schedule_report =
33 33
{
34 34
  (* a schedule computed wrt the dependency graph *)
35
  schedule : ident list;
35
  schedule : ident list list;
36 36
  (* the set of unused variables (no output or mem depends on them) *)
37 37
  unused_vars : ISet.t;
38 38
  (* the table mapping each local var to its in-degree *)
......
51 51
   - [frontier] is the set of unsorted root variables so far, not belonging in [pending]
52 52
   - [sort] is the resulting topological order
53 53
*)
54

  
55
(* Checks whether the currently scheduled variable [choice]
56
   is an output of a call, possibly among others *)
57
let is_call_output choice g =
58
  List.for_all ExprDep.is_instance_var (IdentDepGraph.succ g choice)
59

  
54 60
(* Adds successors of [v] in graph [g] in [pending] or [frontier] sets, wrt [eq_equiv],
55 61
   then removes [v] from [g] 
56 62
*)
......
71 77
(* Chooses the next var to be sorted, taking priority into account.
72 78
   Modifies [pending] and [frontier] accordingly.
73 79
*)
74
let next_element eq_equiv g sort pending frontier =
80
let next_element eq_equiv g sort call pending frontier =
75 81
  begin
76 82
    if ISet.is_empty !pending
77 83
    then
......
82 88
	let (p, f) = ISet.partition (eq_equiv choice) !frontier in
83 89
	pending := p;
84 90
	frontier := f;
91
	call := is_call_output choice g;
85 92
	add_successors eq_equiv g choice pending frontier;
86
	if not (ExprDep.is_ghost_var choice) then sort := choice :: !sort
93
	if not (ExprDep.is_ghost_var choice)
94
	then sort := [choice] :: !sort
87 95
      end
88 96
    else
89 97
      begin
......
91 99
      (*Format.eprintf "-2-> %s@." choice;*)
92 100
	pending := ISet.remove choice !pending;
93 101
	add_successors eq_equiv g choice pending frontier;
94
	if not (ExprDep.is_ghost_var choice) then sort := choice :: !sort
102
	if not (ExprDep.is_ghost_var choice)
103
	then sort := (if !call
104
		      then (choice :: List.hd !sort) :: List.tl !sort
105
		      else [choice] :: !sort)
95 106
      end
96 107
  end
97 108

  
......
101 112
let topological_sort eq_equiv g =
102 113
  let roots = graph_roots g in
103 114
  assert (roots <> []);
115
  let call = ref false in
104 116
  let frontier = ref (List.fold_right ISet.add roots ISet.empty) in
105 117
  let pending = ref ISet.empty in
106 118
  let sorted = ref [] in
......
110 122
      (*Format.eprintf "frontier = {%a}, pending = {%a}@."
111 123
	(fun fmt -> ISet.iter (fun e -> Format.pp_print_string fmt e)) !frontier
112 124
	(fun fmt -> ISet.iter (fun e -> Format.pp_print_string fmt e)) !pending;*)
113
      next_element eq_equiv g sorted pending frontier;
125
      next_element eq_equiv g sorted call pending frontier;
114 126
    done;
115 127
    IdentDepGraph.clear g;
116 128
    !sorted
......
146 158

  
147 159
    let disjoint = Disjunction.clock_disjoint_map (get_node_vars n) in
148 160
    
149
    Log.report ~level:5 
161
    Log.report ~level:2 
150 162
      (fun fmt -> 
151 163
	Format.fprintf fmt
152 164
	  "clock disjoint map for node %s: %a" 
......
154 166
	  Disjunction.pp_disjoint_map disjoint
155 167
      );
156 168

  
157
    let reuse = Liveness.compute_reuse_policy n sort disjoint gg in
158
    Log.report ~level:5 
169
    let reuse = Hashtbl.create 23 (*Liveness.compute_reuse_policy n sort disjoint gg*) in
170
    Log.report ~level:2 
159 171
      (fun fmt -> 
160 172
	Format.fprintf fmt
161 173
	  "reuse policy for node %s: %a" 
......
181 193
    prog
182 194
    ([],IMap.empty)
183 195

  
196
let pp_eq_schedule fmt vl =
197
  match vl with
198
  | []  -> assert false
199
  | [v] -> Format.fprintf fmt "%s" v
200
  | _   -> Format.fprintf fmt "(%a)" (fprintf_list ~sep:" , " (fun fmt v -> Format.fprintf fmt "%s" v)) vl
201
 
184 202
let pp_schedule fmt node_schs =
185 203
 IMap.iter
186 204
   (fun nd report ->
187 205
     Format.fprintf fmt "%s schedule: %a@."
188 206
       nd
189
       (fprintf_list ~sep:" ; " (fun fmt v -> Format.fprintf fmt "%s" v)) report.schedule)
207
       (fprintf_list ~sep:" ; " pp_eq_schedule) report.schedule)
190 208
   node_schs
191 209

  
192 210
let pp_fanin_table fmt node_schs =
src/types.ml
239 239
 | Ttuple _         -> true
240 240
 | _                -> false
241 241

  
242
let rec is_nested_tuple_type ty =
243
 match (repr ty).tdesc with
244
 | Ttuple tl        -> List.exists is_tuple_type tl
245
 | _                -> false
246

  
247 242
let map_tuple_type f ty =
248 243
  let ty = dynamic_type ty in
249 244
  match ty.tdesc with
src/typing.ml
244 244
  | Dimension.Unify _ ->
245 245
    raise (Error (loc, Type_clash (ty1,ty2)))
246 246

  
247
(* ty1 is a subtype of ty2 *)
248
(*
249
let rec sub_unify sub ty1 ty2 =
250
  match (repr ty1).tdesc, (repr ty2).tdesc with
251
  | Ttuple tl1         , Ttuple tl2         ->
252
    if List.length tl1 <> List.length tl2
253
    then raise (Unify (ty1, ty2))
254
    else List.iter2 (sub_unify sub) tl1 tl2
255
  | Ttuple [t1]        , _                  -> sub_unify sub t1 ty2
256
  | _                  , Ttuple [t2]        -> sub_unify sub ty1 t2
257
  | Tstruct tl1        , Tstruct tl2        ->
258
    if List.map fst tl1 <> List.map fst tl2
259
    then raise (Unify (ty1, ty2))
260
    else List.iter2 (fun (_, t1) (_, t2) -> sub_unify sub t1 t2) tl1 tl2
261
  | Tclock t1          , Tclock t2          -> sub_unify sub t1 t2
262
  | Tclock t1          , _   when sub       -> sub_unify sub t1 ty2
263
  | Tstatic (d1, t1)   , Tstatic (d2, t2)   ->
264
    begin
265
      sub_unify sub t1 t2;
266
      Dimension.eval Basic_library.eval_env (fun c -> None) d1;
267
      Dimension.eval Basic_library.eval_env (fun c -> None) d2;
268
      Dimension.unify d1 d2
269
    end
270
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub t1 ty2
271
  | _                                       -> unify ty1 ty2
272
*)
273

  
274 247
let rec type_struct_const_field loc (label, c) =
275 248
  if Hashtbl.mem field_table label
276 249
  then let tydec = Hashtbl.find field_table label in
......
330 303
  if const_expected && not const_real
331 304
  then raise (Error (loc, Not_a_constant))
332 305

  
333
let rec type_standard_args env in_main const expr_list =
334
  let ty_list =
335
    List.map
336
      (fun e -> let ty = dynamic_type (type_expr env in_main const e) in
337
		match get_clock_base_type ty with
338
		| None    -> ty
339
		| Some ty -> ty)
340
      expr_list in
341
  let ty_res = new_var () in
342
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
343
  ty_res
306
let rec type_add_const env const arg targ =
307
  if const
308
  then let d =
309
	 if is_dimension_type targ
310
	 then dimension_of_expr arg
311
	 else Dimension.mkdim_var () in
312
       let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
313
       Dimension.eval Basic_library.eval_env eval_const d;
314
       let real_static_type = Type_predef.type_static d (Types.dynamic_type targ) in
315
       (match Types.get_static_value targ with
316
       | None    -> ()
317
       | Some d' -> try_unify targ real_static_type arg.expr_loc);
318
       real_static_type
319
  else targ
344 320

  
345 321
(* emulates a subtyping relation between types t and (d : t),
346 322
   used during node applications and assignments *)
347 323
and type_subtyping_arg env in_main ?(sub=true) const real_arg formal_type =
348 324
  let loc = real_arg.expr_loc in
349 325
  let const = const || (Types.get_static_value formal_type <> None) in
350
  let real_type = type_expr env in_main const real_arg in
351
  let real_type =
352
    if const
353
    then let d =
354
	   if is_dimension_type real_type
355
	   then dimension_of_expr real_arg
356
	   else Dimension.mkdim_var () in
357
	 let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
358
	 Dimension.eval Basic_library.eval_env eval_const d;
359
	 let real_static_type = Type_predef.type_static d (Types.dynamic_type real_type) in
360
	 (match Types.get_static_value real_type with
361
	 | None    -> ()
362
	 | Some d' -> try_unify real_type real_static_type loc);
363
	 real_static_type
364
    else real_type in
326
  let real_type = type_add_const env const real_arg (type_expr env in_main const real_arg) in
365 327
  (*Format.eprintf "subtyping const %B real %a:%a vs formal %a@." const Printers.pp_expr real_arg Types.print_ty real_type Types.print_ty formal_type;*)
366 328
  try_unify ~sub:sub formal_type real_type loc
367 329

  
......
375 337
   it in many calls
376 338
*)
377 339
and type_appl env in_main loc const f args =
378
  let args = expr_list_of_expr args in
379
  if Basic_library.is_internal_fun f && List.exists is_tuple_expr args
340
  let targs = List.map (type_expr env in_main const) args in
341
  if Basic_library.is_internal_fun f && List.exists is_tuple_type targs
380 342
  then
381 343
    try
382
      let args = Utils.transpose_list (List.map expr_list_of_expr args) in
383
      Types.type_of_type_list (List.map (type_call env in_main loc const f) args)
344
      let targs = Utils.transpose_list (List.map type_list_of_type targs) in
345
      Types.type_of_type_list (List.map (type_simple_call env in_main loc const f) targs)
384 346
    with
385 347
      Utils.TransposeError (l, l') -> raise (Error (loc, WrongMorphism (l, l')))
386 348
  else
387
    type_call env in_main loc const f args
349
    type_dependent_call env in_main loc const f (List.combine args targs)
388 350

  
389
(* type a (single) call. [args] is here a list of arguments. *)
390
and type_call env in_main loc const f args =
351
(* type a call with possible dependent types. [targs] is here a list of (argument, type) pairs. *)
352
and type_dependent_call env in_main loc const f targs =
391 353
  let tins, touts = new_var (), new_var () in
392 354
  let tfun = Type_predef.type_arrow tins touts in
393 355
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
394 356
  let tins = type_list_of_type tins in
395
  if List.length args <> List.length tins then
396
    raise (Error (loc, WrongArity (List.length tins, List.length args)))
357
  if List.length targs <> List.length tins then
358
    raise (Error (loc, WrongArity (List.length tins, List.length targs)))
397 359
  else
398
    List.iter2 (type_subtyping_arg env in_main const) args tins;
360
    begin
361
      List.iter2 (fun (a,t) ti ->
362
	let t' = type_add_const env (const || Types.get_static_value ti <> None) a t
363
	in try_unify ~sub:true ti t' a.expr_loc) targs tins;
364
      touts
365
    end
366

  
367
(* type a simple call without dependent types 
368
   but possible homomorphic extension.
369
   [targs] is here a list of arguments' types. *)
370
and type_simple_call env in_main loc const f targs =
371
  let tins, touts = new_var (), new_var () in
372
  let tfun = Type_predef.type_arrow tins touts in
373
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
374
  (*Format.eprintf "try unify %a %a@." Types.print_ty tins Types.print_ty (type_of_type_list targs);*)
375
  try_unify ~sub:true tins (type_of_type_list targs) loc;
399 376
  touts
400 377

  
401 378
(** [type_expr env in_main expr] types expression [expr] in environment
......
425 402
    expr.expr_type <- ty;
426 403
    ty 
427 404
  | Expr_array elist ->
428
    let ty_elt = type_standard_args env in_main const elist in
405
    let ty_elt = new_var () in
406
    List.iter (fun e -> try_unify ty_elt (type_appl env in_main expr.expr_loc const "uminus" [e]) e.expr_loc) elist;
429 407
    let d = Dimension.mkdim_int expr.expr_loc (List.length elist) in
430 408
    let ty = Type_predef.type_array d ty_elt in
431 409
    expr.expr_type <- ty;
......
441 419
    let eval_const id = Types.get_static_value (Env.lookup_value (fst env) id) in
442 420
    type_subtyping_arg env in_main true (expr_of_dimension d) Type_predef.type_int;
443 421
    Dimension.eval Basic_library.eval_env eval_const d;
444
    let ty_elt = type_standard_args env in_main const [e1] in
422
    let ty_elt = type_appl env in_main expr.expr_loc const "uminus" [e1] in
445 423
    let ty = Type_predef.type_array d ty_elt in
446 424
    expr.expr_type <- ty;
447 425
    ty
......
451 429
    ty
452 430
  | Expr_ite (c, t, e) ->
453 431
    type_subtyping_arg env in_main const c Type_predef.type_bool;
454
    let ty = type_standard_args env in_main const [t; e] in
432
    let ty = type_appl env in_main expr.expr_loc const "+" [t; e] in
455 433
    expr.expr_type <- ty;
456 434
    ty
457 435
  | Expr_appl (id, args, r) ->
......
466 444
	Type_predef.type_clock 
467 445
	  (type_const expr.expr_loc (Const_tag l)) in
468 446
      type_subtyping_arg env in_main ~sub:false const expr_x typ_l);
469
    let touts = type_appl env in_main expr.expr_loc const id args in
447
    let touts = type_appl env in_main expr.expr_loc const id (expr_list_of_expr args) in
470 448
    expr.expr_type <- touts;
471 449
    touts
472 450
  | Expr_fby (e1,e2)
473 451
  | Expr_arrow (e1,e2) ->
474 452
    (* fby/arrow is not legal in a constant expression *)
475 453
    check_constant expr.expr_loc const false;
476
    let ty = type_standard_args env in_main const [e1; e2] in
454
    let ty = type_appl env in_main expr.expr_loc const "+" [e1; e2] in
477 455
    expr.expr_type <- ty;
478 456
    ty
479 457
  | Expr_pre e ->
480 458
    (* pre is not legal in a constant expression *)
481 459
    check_constant expr.expr_loc const false;
482
    let ty = type_standard_args env in_main const [e] in
460
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e] in
483 461
    expr.expr_type <- ty;
484 462
    ty
485 463
  | Expr_when (e1,c,l) ->
......
488 466
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
489 467
    let expr_c = expr_of_ident c expr.expr_loc in
490 468
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
491
    (*update_clock env in_main c expr.expr_loc typ_l;*)
492
    let ty = type_standard_args env in_main const [e1] in
469
    let ty = type_appl env in_main expr.expr_loc const "uminus" [e1] in
493 470
    expr.expr_type <- ty;
494 471
    ty
495 472
  | Expr_merge (c,hl) ->
......
499 476
    let expr_c = expr_of_ident c expr.expr_loc in
500 477
    let typ_l = Type_predef.type_clock typ_in in
501 478
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
502
    (*update_clock env in_main c expr.expr_loc typ_l;*)
503 479
    expr.expr_type <- typ_out;
504 480
    typ_out
505 481
  in 
......
524 500
    else (typ_in, typ_out)
525 501
  with Unify (t1, t2) ->
526 502
    raise (Error (loc, Type_clash (t1,t2)))
527
(*
528
and update_clock env in_main id loc typ =
529
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
530
 try
531
   let vdecl = List.find (fun v -> v.var_id = id) (snd env)
532
   in vdecl.var_type <- typ
533
 with
534
   Not_found ->
535
   raise (Error (loc, Unbound_value ("clock " ^ id)))
536
*)
503

  
537 504
(** [type_eq env eq] types equation [eq] in environment [env] *)
538 505
let type_eq env in_main undefined_vars eq =
539 506
  (* Check undefined variables, type lhs *)

Also available in: Unified diff