Project

General

Profile

Revision 6afa892a

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/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
294 294
 | Expr_when    (e1, _, _)          -> translate_expr node args e1
295 295
 | Expr_merge   (x, _)              -> raise NormalizationError
296 296
 | Expr_appl (id, e, _) when Basic_library.is_internal_fun id ->
297
   let id =
298
     (* need to specialize C (dis)equality operators wrt boolean type
299
        because C boolean truth value is not unique *)
300
     match !Options.output with
301
     | "C" when Types.is_bool_type expr.expr_type ->
302
       if id = "="  then "equi" else
303
       if id = "!=" then "xor"
304
       else id
305
     | _   -> id in
297 306
   let nd = node_from_name id in
298 307
   (match e.expr_desc with
299 308
   | Expr_tuple el -> Fun (node_name nd, List.map (translate_expr node args) el)
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: *)

Also available in: Unified diff