Project

General

Profile

Revision 59294251

View differences:

src/basic_library.ml
48 48
      "&&", (static_op type_bin_bool_op);
49 49
      "||", (static_op type_bin_bool_op);
50 50
      "xor", (static_op type_bin_bool_op);
51
      "equi", (static_op type_bin_bool_op);
51 52
      "impl", (static_op type_bin_bool_op);
52 53
      "<", (static_op type_bin_comp_op);
53 54
      "<=", (static_op type_bin_comp_op);
......
67 68
      ["uminus"; "not"] init_env in
68 69
  let env' = 
69 70
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
70
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
71
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
71 72
  env'
72 73

  
73 74
module DE = Env
......
79 80
      ["uminus"; "not"] init_env in
80 81
  let env' = 
81 82
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
82
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
83
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
83 84
  let env' = 
84 85
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
85 86
      [] env' in
......
99 100
    "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b)  | _ -> assert false);
100 101
    "||", (function [Dbool a; Dbool b] -> Dbool (a||b)  | _ -> assert false);
101 102
    "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
103
    "equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false);
102 104
    "impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false);
103 105
    "<", (function [Dint a; Dint b] -> Dbool (a<b)      | _ -> assert false);
104 106
    ">", (function [Dint a; Dint b] -> Dbool (a>b)      | _ -> assert false);
......
113 115
    VE.initial
114 116
    defs
115 117

  
116
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
117

  
118
let homomorphic_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"uminus";"not"]
118
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"equi";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
119 119

  
120 120
let is_internal_fun x =
121 121
  List.mem x internal_funs
122 122

  
123

  
124 123
let pp_c i pp_val fmt vl =
125 124
  match i, vl with
126 125
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
......
128 127
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
129 128
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
130 129
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
131
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
132
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
130
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
131
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
132
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
133 133
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
134 134
    | _ -> failwith i
135 135

  
......
140 140
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
141 141
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
142 142
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
143
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
144
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
145
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
143 146
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
144 147
    | _ -> assert false
145 148

  
......
152 155
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
153 156
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
154 157
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
155
  (* | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2 *)
158
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
159
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
160
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
156 161
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
157 162
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
158 163
  | _ -> assert false
src/clock_calculus.ml
776 776
      (try_generalize ck vdecl.var_loc; ck)
777 777
    else
778 778
 *)
779
      if Types.is_clock_type vdecl.var_type
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 782
  vdecl.var_clock <- ck;
......
808 808
  Log.report ~level:3 (fun fmt -> print_ck fmt ck_node);
809 809
  (* Local variables may contain first-order carrier variables that should be generalized.
810 810
     That's not the case for types. *)
811
  try_generalize ck_node loc;
812
(*
811 813
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_inputs;
812
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;
814
  List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_outputs;*)
813 815
  (*List.iter (fun vdecl -> try_generalize vdecl.var_clock vdecl.var_loc) nd.node_locals;*)
814 816
  (* TODO : Xavier pourquoi ai je cette erreur ? *)
815 817
(*  if (is_main && is_polymorphic ck_node) then
......
889 891
*)
890 892
let uneval_vdecl_generics vdecl =
891 893
 (*Format.eprintf "Clock_calculus.uneval_vdecl_generics %a@." Printers.pp_node_var vdecl;*)
892
 if Types.is_clock_type vdecl.var_type
894
 if Types.get_clock_base_type vdecl.var_type <> None
893 895
 then
894 896
   match get_carrier_name vdecl.var_clock with
895 897
   | None    -> (Format.eprintf "internal error: %a@." print_ck vdecl.var_clock; assert false)
src/corelang.ml
460 460
let node_eq id node =
461 461
 List.find (fun eq -> List.mem id eq.eq_lhs) node.node_eqs
462 462

  
463
(* Consts unfoooolding *)
464
let is_const i consts = 
465
  List.exists (fun c -> c.const_id = i) consts
466

  
467
let get_const i consts =
468
  let c = List.find (fun c -> c.const_id = i) consts in
469
  c.const_value
470

  
471
let rec expr_unfold_consts consts e = 
472
{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }
473

  
474
and expr_desc_unfold_consts consts e =
475
  let unfold = expr_unfold_consts consts in
476
  match e with
477
  | Expr_const _ -> e
478
  | Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e
479
  | Expr_array el -> Expr_array (List.map unfold el)
480
  | Expr_access (e1, d) -> Expr_access (unfold e1, d)
481
  | Expr_power (e1, d) -> Expr_power (unfold e1, d)
482
  | Expr_tuple el -> Expr_tuple (List.map unfold el)
483
  | Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e)
484
  | Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) 
485
  | Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2)
486
  (* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *)
487
  (* | Expr_tail e' -> Expr_tail (unfold e') *)
488
  | Expr_pre e' -> Expr_pre (unfold e')
489
  | Expr_when (e', i, l)-> Expr_when (unfold e', i, l)
490
  | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl)
491
  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')
492
  | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) 
493
  | Expr_dclock (e', i) -> Expr_dclock (unfold e', i)
494
  | Expr_phclock _ -> e  
495

  
496
let eq_unfold_consts consts eq =
497
  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }
498

  
499
let node_unfold_consts consts node = 
500
  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }
501

  
502
let get_consts prog = 
503
  List.fold_left (
504
    fun consts decl ->
505
      match decl.top_decl_desc with
506
	| Consts clist -> clist@consts
507
	| Node _ | ImportedNode _ | Open _ -> consts  
508
  ) [] prog
509

  
510

  
511 463
let get_nodes prog = 
512 464
  List.fold_left (
513 465
    fun nodes decl ->
......
516 468
	| Consts _ | ImportedNode _ | Open _ -> nodes  
517 469
  ) [] prog
518 470

  
519
let prog_unfold_consts prog =
520
  let consts = get_consts prog in
521
    List.map (
522
      fun decl -> match decl.top_decl_desc with 
523
	| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}
524
	| _       -> decl
525
    ) prog 
471
let get_consts prog = 
472
  List.fold_left (
473
    fun consts decl ->
474
      match decl.top_decl_desc with
475
	| Consts clist -> clist@consts
476
	| Node _ | ImportedNode _ | Open _ -> consts  
477
  ) [] prog
526 478

  
527 479

  
528 480

  
src/corelang.mli
235 235
val pp_prog_clock : Format.formatter -> program -> unit
236 236

  
237 237
val get_nodes : program -> node_desc list
238
val get_consts : program -> const_desc list
239
val prog_unfold_consts: program -> program
238
 val get_consts : program -> const_desc list 
239
(* val prog_unfold_consts: program -> program *)
240

  
240 241
val expr_replace_var: (ident -> ident) -> expr -> expr
241 242
val eq_replace_rhs_var: (ident -> bool) -> (ident -> ident) -> eq -> eq
242 243

  
src/dimension.ml
319 319
	inst_dim_vars := (dim.dim_id, var)::!inst_dim_vars;
320 320
	var
321 321

  
322
let rec unify dim1 dim2 =
323
  let dim1 = repr dim1 in
324
  let dim2 = repr dim2 in
325
  if dim1.dim_id = dim2.dim_id then () else
326
  match dim1.dim_desc, dim2.dim_desc with
327
  | Dunivar, _
328
  | _      , Dunivar -> assert false
329
  | Dvar   , Dvar    ->
330
      if dim1.dim_id < dim2.dim_id
331
      then dim2.dim_desc <- Dlink dim1
332
      else dim1.dim_desc <- Dlink dim2
333
  | Dvar   , _ when not (occurs dim1 dim2) ->
334
      dim1.dim_desc <- Dlink dim2
335
  | _      , Dvar when not (occurs dim2 dim1) ->
336
      dim2.dim_desc <- Dlink dim1
337
  | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
338
      begin
339
        unify i1 i2;
340
	unify t1 t2;
341
	unify e1 e2
342
      end
343
  | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
344
      List.iter2 unify args1 args2
345
  | Dbool b1, Dbool b2 when b1 = b2 -> ()
346
  | Dint i1 , Dint i2 when i1 = i2 -> ()
347
  | Dident id1, Dident id2 when id1 = id2 -> ()
348
  | _ -> raise (Unify (dim1, dim2))
349

  
350
(* unification with the constraint that dim1 is an instance of dim2 *)
351
let rec semi_unify dim1 dim2 =
352
  let dim1 = repr dim1 in
353
  let dim2 = repr dim2 in
354
  if dim1.dim_id = dim2.dim_id then () else
355
  match dim1.dim_desc, dim2.dim_desc with
356
  | Dunivar, _
357
  | _      , Dunivar -> assert false
358
  | Dvar   , Dvar    ->
359
      if dim1.dim_id < dim2.dim_id
360
      then dim2.dim_desc <- Dlink dim1
361
      else dim1.dim_desc <- Dlink dim2
362
  | Dvar   , _  -> raise (Unify (dim1, dim2))
363
  | _      , Dvar when not (occurs dim2 dim1) ->
364
      dim2.dim_desc <- Dlink dim1
365
  | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
366
      begin
367
        semi_unify i1 i2;
368
	semi_unify t1 t2;
369
	semi_unify e1 e2
370
      end
371
  | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
372
      List.iter2 semi_unify args1 args2
373
  | Dbool b1, Dbool b2 when b1 = b2 -> ()
374
  | Dint i1 , Dint i2 when i1 = i2 -> ()
375
  | Dident id1, Dident id2 when id1 = id2 -> ()
376
  | _ -> raise (Unify (dim1, dim2))
322
(** destructive unification of [dim1] and [dim2].
323
   Raises [Unify (t1,t2)] if the types are not unifiable.
324
   if [semi] unification is required,
325
   [dim1] should furthermore be an instance of [dim2] *)
326
let unify ?(semi=false) dim1 dim2 =
327
  let rec unif dim1 dim2 =
328
    let dim1 = repr dim1 in
329
    let dim2 = repr dim2 in
330
    if dim1.dim_id = dim2.dim_id then () else
331
      match dim1.dim_desc, dim2.dim_desc with
332
      | Dunivar, _
333
      | _      , Dunivar -> assert false
334
      | Dvar   , Dvar    ->
335
	if dim1.dim_id < dim2.dim_id
336
	then dim2.dim_desc <- Dlink dim1
337
	else dim1.dim_desc <- Dlink dim2
338
      | Dvar   , _ when (not semi) && not (occurs dim1 dim2) ->
339
	dim1.dim_desc <- Dlink dim2
340
      | _      , Dvar when not (occurs dim2 dim1) ->
341
	dim2.dim_desc <- Dlink dim1
342
      | Dite(i1, t1, e1), Dite(i2, t2, e2) ->
343
	begin
344
          unif i1 i2;
345
	  unif t1 t2;
346
	  unif e1 e2
347
	end
348
      | Dappl(f1, args1), Dappl(f2, args2) when f1 = f2 && List.length args1 = List.length args2 ->
349
	List.iter2 unif args1 args2
350
      | Dbool b1, Dbool b2 when b1 = b2 -> ()
351
      | Dint i1 , Dint i2 when i1 = i2 -> ()
352
      | Dident id1, Dident id2 when id1 = id2 -> ()
353
      | _ -> raise (Unify (dim1, dim2))
354
  in unif dim1 dim2
377 355

  
378 356
let rec expr_replace_var fvar e = 
379 357
 { e with dim_desc = expr_replace_desc fvar e.dim_desc }
src/machine_code.ml
280 280
    in
281 281
    aux [] eqs
282 282

  
283
(* specialize predefined (polymorphic) operators
284
   wrt their instances, so that the C semantics 
285
   is preserved *)
286
let specialize_to_c expr =
287
 match expr.expr_desc with
288
 | Expr_appl (id, e, r) ->
289
   if List.exists (fun e -> Types.is_bool_type e.expr_type) (expr_list_of_expr e)
290
   then let id =
291
	  match id with
292
	  | "="  -> "equi"
293
	  | "!=" -> "xor"
294
	  | _    -> id in
295
	{ expr with expr_desc = Expr_appl (id, e, r) }
296
   else expr
297
 | _ -> expr
298

  
299
let specialize_op expr =
300
  match !Options.output with
301
  | "C" -> specialize_to_c expr
302
  | _   -> expr
303

  
283 304
let rec translate_expr node ((m, si, j, d, s) as args) expr =
305
 let expr = specialize_op expr in
284 306
 match expr.expr_desc with
285 307
 | Expr_const v                     -> Cst v
286 308
 | Expr_ident x                     -> translate_ident node args x
......
295 317
 | Expr_merge   (x, _)              -> raise NormalizationError
296 318
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
297 319
   let nd = node_from_name id in
298
   (match e.expr_desc with
299
   | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr node args) el)
300
   | _             -> Fun (node_name nd, [translate_expr node args e]))
320
   Fun (node_name nd, List.map (translate_expr node args) (expr_list_of_expr e))
301 321
 | Expr_ite (g,t,e) -> (
302 322
   (* special treatment depending on the active backend. For horn backend, ite
303 323
      are preserved in expression. While they are removed for C or Java
......
354 374
     j,
355 375
     d,
356 376
     control_on_clock node args eq.eq_rhs.expr_clock (MStateAssign (var_x, translate_expr node args e2)) :: s)
357
  | p  , Expr_appl (f, arg, r)                  ->
377

  
378
  | p  , Expr_appl (f, arg, r) when not (Basic_library.is_internal_fun f) ->
358 379
    let var_p = List.map (fun v -> node_var v node) p in
359 380
    let el =
360 381
      match arg.expr_desc with
......
370 391
    Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock;
371 392
    (m,
372 393
     (if Stateless.check_node node_f then si else MReset o :: si),
373
     (if Basic_library.is_internal_fun f then j else Utils.IMap.add o call_f j),
394
     Utils.IMap.add o call_f j,
374 395
     d,
375 396
     reset_instance node args o r eq.eq_rhs.expr_clock @
376 397
       (control_on_clock node args call_ck (MStep (var_p, o, vl))) :: s)
......
393 414
  | [x], _                                       -> (
394 415
    let var_x = node_var x node in
395 416
    (m, si, j, d, 
396
     control_on_clock node args eq.eq_rhs.expr_clock (translate_act node args (var_x, eq.eq_rhs)) :: s)
417
     control_on_clock 
418
       node
419
       args
420
       eq.eq_rhs.expr_clock
421
       (translate_act node args (var_x, eq.eq_rhs)) :: s
422
    )
397 423
  )
398 424
  | _                                            ->
399 425
    begin
......
404 430
let translate_eqs node args eqs =
405 431
  List.fold_right (fun eq args -> translate_eq node args eq) eqs args;;
406 432

  
407
let translate_decl nd =
433
let translate_decl nd sch =
408 434
  (*Log.report ~level:1 (fun fmt -> Printers.pp_node fmt nd);*)
409
  let nd, sch = Scheduling.schedule_node nd in
410 435
  let split_eqs = Splitting.tuple_split_eq_list nd.node_eqs in
411 436
  let eqs_rev, remainder = 
412 437
    List.fold_left 
......
462 487
    mannot = nd.node_annot;
463 488
  }
464 489

  
465

  
466
let translate_prog decls =
490
(** takes the global delcarations and the scheduling associated to each node *)
491
let translate_prog decls node_schs =
467 492
  let nodes = get_nodes decls in 
468
   (* What to do with Imported/Sensor/Actuators ? *)
469
   (*arrow_machine ::*)  List.map translate_decl nodes
493
  List.map 
494
    (fun node -> 
495
      let sch = List.assoc node.node_id node_schs in
496
      translate_decl node sch 
497
    ) nodes
470 498

  
471 499
let get_machine_opt name machines =  
472 500
  List.fold_left 
src/main_lustre_compiler.ml
99 99
  let new_cenv = clock_decls Basic_library.clock_env header in   (* Clock calculus *)
100 100
  header, new_tenv, new_cenv
101 101

  
102
let load_n_check_lusi source_name lusi_name prog computed_types_env computed_clocks_env= 
103
  try 
104
    let _ = open_in lusi_name in
105
    let header = load_lusi true lusi_name in
106
    let _, declared_types_env, declared_clocks_env = check_lusi header in
107
    
108
      (* checking type compatibility with computed types*)
109
    Typing.check_env_compat header declared_types_env computed_types_env;
110
    Typing.uneval_prog_generics prog;
111
    
112
      (* checking clocks compatibility with computed clocks*)
113
      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
114
      Clock_calculus.uneval_prog_generics prog;
115

  
116
      (* checking stateless status compatibility *)
117
      Stateless.check_compat header
118
    with Sys_error _ -> ( 
119
      (* Printing lusi file is necessary *)
120
      report ~level:1 
121
	(fun fmt -> 
122
	  fprintf fmt 
123
	    ".. generating lustre interface file %s@," lusi_name);
124
      let lusi_out = open_out lusi_name in
125
      let lusi_fmt = formatter_of_out_channel lusi_out in
126
      Typing.uneval_prog_generics prog;
127
      Clock_calculus.uneval_prog_generics prog;
128
      Printers.pp_lusi_header lusi_fmt source_name prog
129
    )
130
    | (Types.Error (loc,err)) as exc ->
131
      eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@."
132
	Types.pp_error err;
133
      raise exc
134
    | Clocks.Error (loc, err) as exc ->
135
      eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@."
136
	Clocks.pp_error err;
137
      raise exc
138
    | Stateless.Error (loc, err) as exc ->
139
      eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
140
	Stateless.pp_error err;
141
      raise exc
102 142
    
103 143
let rec compile basename extension =
144

  
104 145
  (* Loading the input file *)
105 146
  let source_name = basename^extension in
106 147
  Location.input_name := source_name;
107 148
  let lexbuf = Lexing.from_channel (open_in source_name) in
108 149
  Location.init lexbuf source_name;
150

  
109 151
  (* Parsing *)
110 152
  report ~level:1 
111 153
    (fun fmt -> fprintf fmt "@[<v>.. parsing file %s@," source_name);
......
122 164
	Location.pp_loc loc;
123 165
      raise exc
124 166
  in
167

  
125 168
  (* Extracting dependencies *)
126 169
  report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. extracting dependencies@,");
127 170
  let dependencies = 
......
136 179
      try
137 180
	let basename = (if local then s else Version.prefix ^ "/include/lustrec/" ^ s ) ^ ".lusi" in 
138 181
	report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>Library %s@," basename);
139
	  let comp_dep, lusi_type_env, lusi_clock_env = check_lusi (load_lusi false basename) in 
182
	let comp_dep, lusi_type_env, lusi_clock_env = check_lusi (load_lusi false basename) in 
140 183
	report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
141 184
	
142
	  (s, local, comp_dep)::compilation_dep,
143
	  Env.overwrite type_env lusi_type_env,
144
	  Env.overwrite clock_env lusi_clock_env      
185
	(s, local, comp_dep)::compilation_dep,
186
	Env.overwrite type_env lusi_type_env,
187
	Env.overwrite clock_env lusi_clock_env      
145 188
      with Sys_error msg -> (
146 189
	eprintf "Failure: impossible to load library %s.@.%s@." s msg;
147 190
	exit 1
......
149 192
    )  ([], Basic_library.type_env, Basic_library.clock_env) dependencies
150 193
  in
151 194
  report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
152

  
153
  (* Unfold consts *)
154
  (*let prog = Corelang.prog_unfold_consts prog in*)
155

  
195
  
156 196
  (* Sorting nodes *)
157 197
  let prog = SortProg.sort prog in
158 198
  
......
201 241
    end;
202 242
  *)
203 243

  
244
  (* Compatibility with Lusi *)
204 245
  (* Checking the existence of a lusi (Lustre Interface file) *)
205 246
  let lusi_name = basename ^ ".lusi" in
206
  let _ = 
207
    try 
208
      let _ = open_in lusi_name in
209
      let header = load_lusi true lusi_name in
210
      let _, declared_types_env, declared_clocks_env = check_lusi header in
211

  
212
      (* checking type compatibility with computed types*)
213
      Typing.check_env_compat header declared_types_env computed_types_env;
214
      Typing.uneval_prog_generics prog;
215

  
216
      (* checking clocks compatibility with computed clocks*)
217
      Clock_calculus.check_env_compat header declared_clocks_env computed_clocks_env;
218
      Clock_calculus.uneval_prog_generics prog;
219

  
220
      (* checking stateless status compatibility *)
221
      Stateless.check_compat header
222
    with Sys_error _ -> ( 
223
      (* Printing lusi file is necessary *)
224
      report ~level:1 
225
	(fun fmt -> 
226
	  fprintf fmt 
227
	    ".. generating lustre interface file %s@," lusi_name);
228
      let lusi_out = open_out lusi_name in
229
      let lusi_fmt = formatter_of_out_channel lusi_out in
230
      Typing.uneval_prog_generics prog;
231
      Clock_calculus.uneval_prog_generics prog;
232
      Printers.pp_lusi_header lusi_fmt source_name prog
233
    )
234
    | (Types.Error (loc,err)) as exc ->
235
      eprintf "Type mismatch between computed type and declared type in lustre interface file: %a@."
236
	Types.pp_error err;
237
      raise exc
238
    | Clocks.Error (loc, err) as exc ->
239
      eprintf "Clock mismatch between computed clock and declared clock in lustre interface file: %a@."
240
	Clocks.pp_error err;
241
      raise exc
242
    | Stateless.Error (loc, err) as exc ->
243
      eprintf "Stateless status mismatch between defined status and declared status in lustre interface file: %a@."
244
	Stateless.pp_error err;
245
      raise exc
246
  in
247
  load_n_check_lusi source_name lusi_name prog computed_types_env computed_clocks_env;
247 248

  
248 249
  (* Computes and stores generic calls for each node,
249 250
     only useful for ANSI C90 compliant generic node compilation *)
......
252 253

  
253 254
  (* Normalization phase *)
254 255
  report ~level:1 (fun fmt -> fprintf fmt ".. normalization@,");
255
  let normalized_prog = Normalization.normalize_prog prog in
256
  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog normalized_prog);
256
  let prog = Normalization.normalize_prog prog in
257
  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@," Printers.pp_prog prog);
258

  
257 259
  (* Checking array accesses *)
258 260
  if !Options.check then
259 261
    begin
260 262
      report ~level:1 (fun fmt -> fprintf fmt ".. array access checks@,");
261
      Access.check_prog normalized_prog;
263
      Access.check_prog prog;
262 264
    end;
263 265

  
266
  (* Computation of node equation scheduling. It also break dependency cycles. *)
267
  let prog, node_schs = Scheduling.schedule_prog prog in
268

  
269
 (* Optimization of prog: 
270
    - Unfold consts 
271
    - eliminate trivial expressions
272
 *)
273
  let prog = 
274
    if !Options.optimization >= 2 then 
275
      Optimize_prog.prog_unfold_consts prog 
276
    else
277
      prog
278
  in
279

  
264 280
  (* DFS with modular code generation *)
265 281
  report ~level:1 (fun fmt -> fprintf fmt ".. machines generation@,");
266
  let machine_code = Machine_code.translate_prog normalized_prog in
282
  let machine_code = Machine_code.translate_prog prog node_schs in
267 283
  report ~level:2 (fun fmt -> fprintf fmt "@[<v 2>@ %a@]@,"
268 284
    (Utils.fprintf_list ~sep:"@ " Machine_code.pp_machine)
269 285
    machine_code);
286

  
287
  (* Optimize machine code *)
288
  let machine_code = 
289
    if !Options.optimization >= 2 then
290
      Optimize_machine.optimize_machines machine_code
291
    else
292
      machine_code
293
  in
270 294
  
271 295
  (* Creating destination directory if needed *)
272 296
  if not (Sys.file_exists !Options.dest_dir) then (
......
307 331
	    | Some f -> Some (formatter_of_out_channel (open_out f))
308 332
	  in
309 333
	  report ~level:1 (fun fmt -> fprintf fmt ".. C code generation@,");
310
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename normalized_prog machine_code dependencies
334
	  C_backend.translate_to_c header_fmt source_fmt makefile_fmt spec_fmt_opt basename prog machine_code dependencies
311 335
	end
312 336
    | "java" ->
313 337
      begin
......
324 348
	let source_file = destname ^ ".smt2" in (* Could be changed *)
325 349
	let source_out = open_out source_file in
326 350
	let fmt = formatter_of_out_channel source_out in
327
	Horn_backend.translate fmt basename normalized_prog machine_code
351
	Horn_backend.translate fmt basename prog machine_code
328 352
      end
353
    | "lustre" -> assert false (*
354
      begin
355
	let source_file = destname ^ ".lustrec.lus" in (* Could be changed *)
356
	let source_out = open_out source_file in
357
	let fmt = formatter_of_out_channel source_out in
358
(*	Lustre_backend.translate fmt basename normalized_prog machine_code *)
359
	()
360
      end*)
361

  
329 362
    | _ -> assert false
330 363
  in
331 364
  report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
src/options.ml
35 35
let verbose_level = ref 1
36 36
let global_inline = ref false
37 37
let witnesses = ref false
38
let optimization = ref 2
38 39

  
39 40
let options =
40 41
  [ "-d", Arg.Set_string dest_dir,
......
48 49
    "generates a C encoding of the specification instead of ACSL contracts and annotations. Only meaningful for the C backend";
49 50
    "-java", Arg.Unit (fun () -> output := "java"), "generates Java output instead of C";
50 51
    "-horn", Arg.Unit (fun () -> output := "horn"), "generates Horn clauses encoding output instead of C";
52
    "-lustre", Arg.Unit (fun () -> output := "lustre"), "generates Lustre output, performing all active optimizations";
51 53
    "-inline", Arg.Set global_inline, "inline all node calls (require a main node)";
52 54
    "-witnesses", Arg.Set witnesses, "enable production of witnesses during compilation";
53 55
    "-print_types", Arg.Set print_types, "prints node types";
54 56
    "-print_clocks", Arg.Set print_clocks, "prints node clocks";
57
    "-O", Arg.Set_int optimization, " changes optimization level <default: 2>";
55 58
    "-verbose", Arg.Set_int verbose_level, " changes verbose level <default: 1>";
56 59
    "-version", Arg.Unit (fun () -> print_endline version), " displays the version";]
57 60

  
src/scheduling.ml
125 125
    pp_error Format.err_formatter v;
126 126
    raise exc
127 127

  
128
let schedule_prog prog =
129
  List.fold_right (
130
    fun top_decl (accu_prog, sch_map)  ->
131
      match top_decl.top_decl_desc with
132
	| Node nd -> 
133
	  let nd', sch = schedule_node nd in
134
	  {top_decl with top_decl_desc = Node nd'}::accu_prog, (nd.node_id, sch)::sch_map
135
	| _ -> top_decl::accu_prog, sch_map
136
    ) 
137
    prog
138
    ([],[])
139

  
128 140

  
129 141
(* Local Variables: *)
130 142
(* compile-command:"make -C .." *)
src/type_predef.ml
41 41

  
42 42
let type_unary_poly_op =
43 43
  let univ = new_univar () in
44
  new_ty (Tarrow (univ, univ))
44
  type_arrow univ univ
45 45

  
46 46
let type_bin_int_op =
47
  new_ty (Tarrow (new_ty (Ttuple [type_int;type_int]), type_int))
47
  type_arrow (type_tuple [type_int;type_int]) type_int
48 48

  
49 49
let type_bin_bool_op =
50
  new_ty (Tarrow (new_ty (Ttuple [type_bool;type_bool]), type_bool))
50
  type_arrow (type_tuple [type_bool;type_bool]) type_bool
51 51

  
52 52
let type_ite_op =
53 53
  let univ = new_univar () in
54
  new_ty (Tarrow ((new_ty (Ttuple [type_bool;univ;univ])), univ))
54
  type_arrow (type_tuple [type_bool;univ;univ]) univ
55 55

  
56 56
let type_bin_poly_op =
57 57
  let univ = new_univar () in
58
  new_ty (Tarrow ((new_ty (Ttuple [univ;univ])), univ))
58
  type_arrow (type_tuple [univ;univ]) univ
59 59

  
60 60
let type_bin_comp_op =
61 61
  let univ = new_univar () in
......
63 63

  
64 64
let type_univ_bool_univ =
65 65
  let univ = new_univar () in
66
  new_ty (Tarrow ((new_ty (Ttuple [univ;type_bool])), univ))
66
  type_arrow (type_tuple [univ;type_bool]) univ
67 67

  
68 68
let type_bool_univ3 =
69 69
  let univ = new_univar () in
70
  new_ty (Tarrow ((new_ty (Ttuple [type_bool;univ;univ])), univ))
70
  type_arrow (type_tuple [type_bool;univ;univ]) univ
71 71

  
72 72
let type_access =
73 73
  let d = Dimension.mkdim Location.dummy_loc Dimension.Dunivar in
src/types.ml
35 35
  | Tbool
36 36
  | Trat (* Actually unused for now. Only place where it can appear is
37 37
            in a clock declaration *)
38
  | Tclock of type_expr (* An type expression explicitely tagged as carrying a clock *)
38
  | Tclock of type_expr (* A type expression explicitely tagged as carrying a clock *)
39 39
  | Tarrow of type_expr * type_expr
40 40
  | Ttuple of type_expr list
41 41
  | Tenum of ident list
......
55 55
  | Unbound_type of ident
56 56
  | Not_a_dimension
57 57
  | Not_a_constant
58
  | Assigned_constant of ident
58 59
  | WrongArity of int * int
59 60
  | WrongMorphism of int * int
60 61
  | Type_clash of type_expr * type_expr
......
119 120
  | Tbool ->
120 121
    fprintf fmt "bool"
121 122
  | Tclock t ->
122
    fprintf fmt "%a clock" print_ty t
123
    fprintf fmt "%a clock" print_node_ty t
123 124
  | Tstatic (_, t) ->
124 125
    fprintf fmt "%a" print_node_ty t
125 126
  | Tconst t ->
......
127 128
  | Trat ->
128 129
    fprintf fmt "rat"
129 130
  | Tarrow (ty1,ty2) ->
130
    fprintf fmt "%a -> %a" print_ty ty1 print_ty ty2
131
    fprintf fmt "%a -> %a" print_node_ty ty1 print_node_ty ty2
131 132
  | Ttuple tylist ->
132 133
    fprintf fmt "(%a)"
133
      (Utils.fprintf_list ~sep:"*" print_ty) tylist
134
      (Utils.fprintf_list ~sep:"*" print_node_ty) tylist
134 135
  | Tenum taglist ->
135 136
    fprintf fmt "enum {%a }"
136 137
      (Utils.fprintf_list ~sep:", " pp_print_string) taglist
......
138 139
    fprintf fmt "struct {%a }"
139 140
      (Utils.fprintf_list ~sep:"; " print_node_struct_ty_field) fieldlist
140 141
  | Tarray (e, ty) ->
141
    fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
142
    fprintf fmt "%a^%a" print_node_ty ty Dimension.pp_dimension e
142 143
  | Tlink ty ->
143
      print_ty fmt ty
144
      print_node_ty fmt ty
144 145
  | Tunivar ->
145 146
    fprintf fmt "'%s" (name_of_type ty.tid)
146 147

  
......
155 156
    fprintf fmt "Multiple definitions of variable %s@." id
156 157
  | Not_a_constant ->
157 158
    fprintf fmt "This expression is not a constant@."
159
  | Assigned_constant id ->
160
    fprintf fmt "The constant %s cannot be assigned@." id
158 161
  | Not_a_dimension ->
159 162
    fprintf fmt "This expression is not a valid dimension@."
160 163
  | WrongArity (ar1, ar2) ->
......
201 204
  | Tstruct fl -> (try Some (List.assoc label fl) with Not_found -> None)
202 205
  | _          -> None
203 206

  
204
let is_clock_type ty =
207
let is_numeric_type ty =
208
 match (repr ty).tdesc with
209
 | Tint
210
 | Treal -> true
211
 | _     -> false
212

  
213
let is_bool_type ty =
214
 match (repr ty).tdesc with
215
 | Tbool -> true
216
 | _     -> false
217

  
218
let get_clock_base_type ty =
205 219
 match (repr ty).tdesc with
206
 | Tclock _ -> true
207
 | _        -> false
220
 | Tclock ty -> Some ty
221
 | _         -> None
208 222

  
209 223
let rec is_dimension_type ty =
210 224
 match (repr ty).tdesc with
src/typing.ml
159 159
    let def_t = get_type_definition t in
160 160
    eq_ground t1 def_t
161 161
  | Tarrow (t1,t2), Tarrow (t1',t2') -> eq_ground t1 t1' && eq_ground t2 t2'
162
  | Tclock t1', _ -> eq_ground t1' t2
163
  | _, Tclock t2' -> eq_ground t1 t2'
162
  | Tclock t1', Tclock t2' -> eq_ground t1' t2'
164 163
  | Tstatic (e1, t1'), Tstatic (e2, t2')
165 164
  | Tarray (e1, t1'), Tarray (e2, t2') -> Dimension.is_eq_dimension e1 e2 && eq_ground t1' t2'
166 165
  | _ -> false
167 166

  
168
(** [unify t1 t2] unifies types [t1] and [t2]. Raises [Unify
169
    (t1,t2)] if the types are not unifiable.*)
170
(* Standard destructive unification *)
171
let rec unify t1 t2 =
172
  let t1 = repr t1 in
173
  let t2 = repr t2 in
174
  if t1=t2 then
175
    ()
176
  else
177
    (* No type abbreviations resolution for now *)
178
    match t1.tdesc,t2.tdesc with
179
      (* This case is not mandory but will keep "older" types *)
180
    | Tvar, Tvar ->
167
(** [unify t1 t2] unifies types [t1] and [t2]
168
    using standard destructive unification.
169
    Raises [Unify (t1,t2)] if the types are not unifiable.
170
    [t1] is a expected/formal/spec type, [t2] is a computed/real/implem type,
171
    so in case of unification error: expected type [t1], got type [t2].
172
    If [sub]-typing is allowed, [t2] may be a subtype of [t1].
173
    If [semi] unification is required,
174
    [t1] should furthermore be an instance of [t2]
175
    and constants are handled differently.*)
176
let unify ?(sub=false) ?(semi=false) t1 t2 =
177
  let rec unif t1 t2 =
178
    let t1 = repr t1 in
179
    let t2 = repr t2 in
180
    if t1=t2 then
181
      ()
182
    else
183
      match t1.tdesc,t2.tdesc with
184
      (* strictly subtyping cases first *)
185
      | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
186
	unif t1 t2
187
      | _ , Tstatic (d2, t2) when sub && (get_static_value t1 = None) ->
188
	unif t1 t2
189
      (* This case is not mandatory but will keep "older" types *)
190
      | Tvar, Tvar ->
181 191
        if t1.tid < t2.tid then
182 192
          t2.tdesc <- Tlink t1
183 193
        else
184 194
          t1.tdesc <- Tlink t2
185
    | (Tvar, _) when (not (occurs t1 t2)) ->
195
      | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
186 196
        t1.tdesc <- Tlink t2
187
    | (_,Tvar) when (not (occurs t2 t1)) ->
188
        t2.tdesc <- Tlink t1
189
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
190
      begin
191
        unify t1 t1';
192
	unify t2 t2'
193
      end
194
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
195
      List.iter2 unify tl tl'
196
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
197
      List.iter2 (fun (_, t) (_, t') -> unify t t') fl fl'
198
    | Tclock _, Tstatic _
199
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
200
    | Tclock t1', _ -> unify t1' t2
201
    | _, Tclock t2' -> unify t1 t2'
202
    | Tint, Tint | Tbool, Tbool | Trat, Trat
203
    | Tunivar, _ | _, Tunivar -> ()
204
    | (Tconst t, _) ->
205
      let def_t = get_type_definition t in
206
      unify def_t t2
207
    | (_, Tconst t)  ->
208
      let def_t = get_type_definition t in
209
      unify t1 def_t
210
    | Tenum tl, Tenum tl' when tl == tl' -> ()
211
    | Tstatic (e1, t1'), Tstatic (e2, t2')
212
    | Tarray (e1, t1'), Tarray (e2, t2') ->
213
      begin
214
	unify t1' t2';
215
	Dimension.eval Basic_library.eval_env (fun c -> None) e1;
216
	Dimension.eval Basic_library.eval_env (fun c -> None) e2;
217
	Dimension.unify e1 e2;
218
      end
219
    | _,_ -> raise (Unify (t1, t2))
220

  
221
(** [semi_unify t1 t2] checks whether type [t1] is an instance of type [t2]. Raises [Unify
222
    (t1,t2)] if the types are not semi-unifiable.*)
223
(* Standard destructive semi-unification *)
224
let rec semi_unify t1 t2 =
225
  let t1 = repr t1 in
226
  let t2 = repr t2 in
227
  if t1=t2 then
228
    ()
229
  else
230
    (* No type abbreviations resolution for now *)
231
    match t1.tdesc,t2.tdesc with
232
      (* This case is not mandory but will keep "older" types *)
233
    | Tvar, Tvar ->
234
        if t1.tid < t2.tid then
235
          t2.tdesc <- Tlink t1
236
        else
237
          t1.tdesc <- Tlink t2
238
    | (Tvar, _) -> raise (Unify (t1, t2))
239
    | (_,Tvar) when (not (occurs t2 t1)) ->
197
      | _, Tvar when (not (occurs t2 t1)) ->
240 198
        t2.tdesc <- Tlink t1
241
    | Tarrow (t1,t2), Tarrow (t1',t2') ->
242
      begin
243
        semi_unify t1 t1';
244
	semi_unify t2 t2'
245
      end
246
    | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
247
      List.iter2 semi_unify tl tl'
248
    | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
249
      List.iter2 (fun (_, t) (_, t') -> semi_unify t t') fl fl'
250
    | Tclock _, Tstatic _
251
    | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
252
    | Tclock t1', _ -> semi_unify t1' t2
253
    | _, Tclock t2' -> semi_unify t1 t2'
254
    | Tint, Tint | Tbool, Tbool | Trat, Trat
255
    | Tunivar, _ | _, Tunivar -> ()
256
    | (Tconst t, _) ->
257
      let def_t = get_type_definition t in
258
      semi_unify def_t t2
259
    | (_, Tconst t)  ->
260
      let def_t = get_type_definition t in
261
      semi_unify t1 def_t
262
    | Tenum tl, Tenum tl' when tl == tl' -> ()
263

  
264
    | Tstatic (e1, t1'), Tstatic (e2, t2')
265
    | Tarray (e1, t1'), Tarray (e2, t2') ->
266
      begin
267
	semi_unify t1' t2';
268
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e1;
269
	Dimension.eval Basic_library.eval_env (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c)) e2;
270
	Dimension.semi_unify e1 e2;
271
      end
272
    | _,_ -> raise (Unify (t1, t2))
199
      | Tarrow (t1,t2), Tarrow (t1',t2') ->
200
	begin
201
          unif t2 t2';
202
	  unif t1' t1
203
	end
204
      | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
205
	List.iter2 unif tl tl'
206
      | Ttuple [t1]        , _                  -> unif t1 t2
207
      | _                  , Ttuple [t2]        -> unif t1 t2
208
      | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
209
	List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
210
      | Tclock _, Tstatic _
211
      | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
212
      | Tclock t1', Tclock t2' -> unif t1' t2'
213
      | Tint, Tint | Tbool, Tbool | Trat, Trat
214
      | Tunivar, _ | _, Tunivar -> ()
215
      | (Tconst t, _) ->
216
	let def_t = get_type_definition t in
217
	unif def_t t2
218
      | (_, Tconst t)  ->
219
	let def_t = get_type_definition t in
220
	unif t1 def_t
221
      | Tenum tl, Tenum tl' when tl == tl' -> ()
222
      | Tstatic (e1, t1'), Tstatic (e2, t2')
223
      | Tarray (e1, t1'), Tarray (e2, t2') ->
224
	let eval_const =
225
	  if semi
226
	  then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
227
	  else (fun c -> None) in
228
	begin
229
	  unif t1' t2';
230
	  Dimension.eval Basic_library.eval_env eval_const e1;
231
	  Dimension.eval Basic_library.eval_env eval_const e2;
232
	  Dimension.unify ~semi:semi e1 e2;
233
	end
234
      | _,_ -> raise (Unify (t1, t2))
235
  in unif t1 t2
273 236

  
274 237
(* Expected type ty1, got type ty2 *)
275
let try_unify ty1 ty2 loc =
276
  try
277
    unify ty1 ty2
278
  with
279
  | Unify _ ->
280
    raise (Error (loc, Type_clash (ty1,ty2)))
281
  | Dimension.Unify _ ->
282
    raise (Error (loc, Type_clash (ty1,ty2)))
283

  
284
let try_semi_unify ty1 ty2 loc =
238
let try_unify ?(sub=false) ?(semi=false) ty1 ty2 loc =
285 239
  try
286
    semi_unify ty1 ty2
240
    unify ~sub:sub ~semi:semi ty1 ty2
287 241
  with
288 242
  | Unify _ ->
289 243
    raise (Error (loc, Type_clash (ty1,ty2)))
......
291 245
    raise (Error (loc, Type_clash (ty1,ty2)))
292 246

  
293 247
(* ty1 is a subtype of ty2 *)
248
(*
294 249
let rec sub_unify sub ty1 ty2 =
295 250
  match (repr ty1).tdesc, (repr ty2).tdesc with
296 251
  | Ttuple tl1         , Ttuple tl2         ->
......
314 269
    end
315 270
  | Tstatic (r_d, t1)  , _         when sub -> sub_unify sub t1 ty2
316 271
  | _                                       -> unify ty1 ty2
317

  
318
let try_sub_unify sub ty1 ty2 loc =
319
  try
320
    sub_unify sub ty1 ty2
321
  with
322
  | Unify _ ->
323
    raise (Error (loc, Type_clash (ty1,ty2)))
324
  | Dimension.Unify _ ->
325
    raise (Error (loc, Type_clash (ty1,ty2)))
272
*)
326 273

  
327 274
let rec type_struct_const_field loc (label, c) =
328 275
  if Hashtbl.mem field_table label
......
383 330
  then raise (Error (loc, Not_a_constant))
384 331

  
385 332
let rec type_standard_args env in_main const expr_list =
386
  let ty_list = List.map (fun e -> dynamic_type (type_expr env in_main const e)) expr_list in
333
  let ty_list =
334
    List.map
335
      (fun e -> let ty = dynamic_type (type_expr env in_main const e) in
336
		match get_clock_base_type ty with
337
		| None    -> ty
338
		| Some ty -> ty)
339
      expr_list in
387 340
  let ty_res = new_var () in
388 341
  List.iter2 (fun e ty -> try_unify ty_res ty e.expr_loc) expr_list ty_list;
389 342
  ty_res
......
409 362
	 real_static_type
410 363
    else real_type in
411 364
  (*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;*)
412
  try_sub_unify sub real_type formal_type loc
365
  try_unify ~sub:sub formal_type real_type loc
413 366

  
414 367
and type_ident env in_main loc const id =
415 368
  type_expr env in_main const (expr_of_ident id loc)
......
439 392
  type_subtyping_arg env in_main const (expr_of_ident f loc) tfun;
440 393
  let tins = type_list_of_type tins in
441 394
  if List.length args <> List.length tins then
442
    raise (Error (loc, WrongArity (List.length args, List.length tins)))
395
    raise (Error (loc, WrongArity (List.length tins, List.length args)))
443 396
  else
444 397
    List.iter2 (type_subtyping_arg env in_main const) args tins;
445 398
  touts
......
534 487
    let typ_l = Type_predef.type_clock (type_const expr.expr_loc (Const_tag l)) in
535 488
    let expr_c = expr_of_ident c expr.expr_loc in
536 489
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
537
    update_clock env in_main c expr.expr_loc typ_l;
490
    (*update_clock env in_main c expr.expr_loc typ_l;*)
538 491
    let ty = type_standard_args env in_main const [e1] in
539 492
    expr.expr_type <- ty;
540 493
    ty
......
545 498
    let expr_c = expr_of_ident c expr.expr_loc in
546 499
    let typ_l = Type_predef.type_clock typ_in in
547 500
    type_subtyping_arg env in_main ~sub:false const expr_c typ_l;
548
    update_clock env in_main c expr.expr_loc typ_l;
501
    (*update_clock env in_main c expr.expr_loc typ_l;*)
549 502
    expr.expr_type <- typ_out;
550 503
    typ_out
551 504
  | Expr_uclock (e,k) | Expr_dclock (e,k) ->
......
578 531
    else (typ_in, typ_out)
579 532
  with Unify (t1, t2) ->
580 533
    raise (Error (loc, Type_clash (t1,t2)))
581

  
534
(*
582 535
and update_clock env in_main id loc typ =
583 536
 (*Log.report ~level:1 (fun fmt -> Format.fprintf fmt "update_clock %s with %a@ " id print_ty typ);*)
584 537
 try
......
587 540
 with
588 541
   Not_found ->
589 542
   raise (Error (loc, Unbound_value ("clock " ^ id)))
590

  
543
*)
591 544
(** [type_eq env eq] types equation [eq] in environment [env] *)
592 545
let type_eq env in_main undefined_vars eq =
593 546
  (* Check undefined variables, type lhs *)
......
601 554
    with Not_found ->
602 555
      raise (Error (eq.eq_loc, Already_defined id))
603 556
  in
557
  (* check assignment of declared constant, assignment of clock *)
558
  let ty_lhs =
559
    type_of_type_list
560
      (List.map2 (fun ty id ->
561
	if get_static_value ty <> None
562
	then raise (Error (eq.eq_loc, Assigned_constant id)) else
563
	match get_clock_base_type ty with
564
	| None -> ty
565
	| Some ty -> ty)
566
	 (type_list_of_type ty_lhs) eq.eq_lhs) in
604 567
  let undefined_vars =
605 568
    List.fold_left (fun uvars v -> define_var v uvars) undefined_vars eq.eq_lhs in
606 569
  (* Type rhs wrt to lhs type with subtyping, i.e. a constant rhs value may be assigned
......
802 765
				    raise (Error (loc, Declared_but_undefined k))) in
803 766
    (*Types.print_ty Format.std_formatter decl_type_k;
804 767
    Types.print_ty Format.std_formatter computed_t;*)
805
    try_semi_unify decl_type_k computed_t Location.dummy_loc
768
    try_unify ~sub:true ~semi:true decl_type_k computed_t Location.dummy_loc
806 769
		    )
807 770

  
808 771
(* Local Variables: *)
test/test-compile.sh
116 116
    fi	
117 117
	# Cheching witness
118 118
    pushd $build > /dev/null
119
    $LUSTREC -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus -verbose 0
119
    $LUSTREC -verbose 0 -horn -d $build/${name}_witnesses -node check $build/${name}_witnesses/inliner_witness.lus 
120 120
    popd > /dev/null
121 121
    z3="`z3 -T:10 $build/${name}_witnesses/inliner_witness.smt2 | xargs`"
122 122
    if [ "x`echo $z3 | grep unsat`" == "xunsat" ]; then
......
126 126
    elif [ "x`echo $z3 | xargs | grep -o unknown`" == "xunknown" ]; then
127 127
	rinlining="UNKNOWN";
128 128
    else
129
	rinlining="INVALID"
130
	exit 1
129
	rinlining="INVALID/TIMEOUT"
131 130
    fi  
132 131
    if [ $verbose -gt 0 ]; then
133 132
	echo "lustrec inlined ($rlustrec2), gcc ($rgcc2), inlining valid ($rinlining), $dir, ${name}.lus, node $main" | column -t -s',' | tee -a $report;

Also available in: Unified diff