Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/clocks.ml
6 6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7 7
(*  under the terms of the GNU Lesser General Public License        *)
8 8
(*  version 2.1.                                                    *)
9
(*                                                                  *) 
9
(*                                                                  *)
10 10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *) 
11
(*                                                                  *)
12 12
(********************************************************************)
13 13

  
14
(** Clocks definitions and a few utility functions on clocks. *)
15 14
open Utils
15
(** Clocks definitions and a few utility functions on clocks. *)
16

  
16 17
open Format
17 18

  
18 19
(* (\* Clock type sets, for subtyping. *\) *)
......
27 28
  | Carry_var
28 29
  | Carry_link of carrier_expr
29 30

  
30
(* Carriers are scoped, to detect clock extrusion. In other words, we
31
   check the scope of a clock carrier before generalizing it. *)
32
and carrier_expr =
33
    {mutable carrier_desc: carrier_desc;
34
     mutable carrier_scoped: bool;
35
     carrier_id: int}
36
     
37
type clock_expr =
38
    {mutable cdesc: clock_desc;
39
     mutable cscoped: bool;
40
     cid: int}
31
(* Carriers are scoped, to detect clock extrusion. In other words, we check the
32
   scope of a clock carrier before generalizing it. *)
33
and carrier_expr = {
34
  mutable carrier_desc : carrier_desc;
35
  mutable carrier_scoped : bool;
36
  carrier_id : int;
37
}
38

  
39
type clock_expr = {
40
  mutable cdesc : clock_desc;
41
  mutable cscoped : bool;
42
  cid : int;
43
}
41 44

  
42 45
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
43 46
and clock_desc =
......
48 51
  (* | Pck_down of clock_expr * int *)
49 52
  (* | Pck_phase of clock_expr * rat *)
50 53
  (* | Pck_const of int * rat *)
51
  | Cvar (* of clock_set *) (* Monomorphic clock variable *)
52
  | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
53
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
54
  | Cvar (* of clock_set *)
55
  (* Monomorphic clock variable *)
56
  | Cunivar
57
  (* of clock_set *)
58
  (* Polymorphic clock variable *)
59
  | Clink of clock_expr
60
  (* During unification, make links instead of substitutions *)
54 61
  | Ccarrying of carrier_expr * clock_expr
55 62

  
56 63
type error =
......
66 73
  | Clock_extrusion of clock_expr * clock_expr
67 74

  
68 75
exception Unify of clock_expr * clock_expr
76

  
69 77
exception Mismatch of carrier_expr * carrier_expr
78

  
70 79
exception Scope_carrier of carrier_expr
80

  
71 81
exception Scope_clock of clock_expr
82

  
72 83
exception Error of Location.t * error
73 84

  
74 85
let rec print_carrier fmt cr =
75
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
86
  (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun
87
     fmt -> *)
76 88
  match cr.carrier_desc with
77
  | Carry_const id -> fprintf fmt "%s" id
89
  | Carry_const id ->
90
    fprintf fmt "%s" id
78 91
  | Carry_name ->
79
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
92
    fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
80 93
  | Carry_var ->
81 94
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
82 95
  | Carry_link cr' ->
83 96
    print_carrier fmt cr'
84 97

  
85
(* Simple pretty-printing, performs no simplifications. Linear
86
   complexity. For debug mainly. *)
98
(* Simple pretty-printing, performs no simplifications. Linear complexity. For
99
   debug mainly. *)
87 100
let rec print_ck_long fmt ck =
88 101
  match ck.cdesc with
89
  | Carrow (ck1,ck2) ->
90
      fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
102
  | Carrow (ck1, ck2) ->
103
    fprintf fmt "%a -> %a" print_ck_long ck1 print_ck_long ck2
91 104
  | Ctuple cklist ->
92
    fprintf fmt "(%a)"
93
      (fprintf_list ~sep:" * " print_ck_long) cklist
94
  | Con (ck,c,l) ->
105
    fprintf fmt "(%a)" (fprintf_list ~sep:" * " print_ck_long) cklist
106
  | Con (ck, c, l) ->
95 107
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
96
  | Cvar -> fprintf fmt "'_%i" ck.cid 
97
  | Cunivar -> fprintf fmt "'%i" ck.cid 
108
  | Cvar ->
109
    fprintf fmt "'_%i" ck.cid
110
  | Cunivar ->
111
    fprintf fmt "'%i" ck.cid
98 112
  | Clink ck' ->
99 113
    fprintf fmt "link %a" print_ck_long ck'
100
  | Ccarrying (cr,ck') ->
114
  | Ccarrying (cr, ck') ->
101 115
    fprintf fmt "(%a:%a)" print_carrier cr print_ck_long ck'
102 116

  
103 117
let new_id = ref (-1)
104 118

  
105
let rec bottom =
106
  { cdesc = Clink bottom; cid = -666; cscoped = false }
119
let rec bottom = { cdesc = Clink bottom; cid = -666; cscoped = false }
107 120

  
108 121
let new_ck desc scoped =
109
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
122
  incr new_id;
123
  { cdesc = desc; cid = !new_id; cscoped = scoped }
110 124

  
111 125
let new_var scoped = new_ck Cvar scoped
112 126

  
......
115 129
let new_carrier_id = ref (-1)
116 130

  
117 131
let new_carrier desc scoped =
118
  incr new_carrier_id; {carrier_desc = desc;
119
                        carrier_id = !new_carrier_id;
120
                        carrier_scoped = scoped}
121

  
122
let new_carrier_name () =
123
  new_carrier Carry_name true
132
  incr new_carrier_id;
133
  { carrier_desc = desc; carrier_id = !new_carrier_id; carrier_scoped = scoped }
124 134

  
125
let rec repr =
126
  function
127
      {cdesc=Clink ck'; _} ->
128
        repr ck'
129
    | ck -> ck
135
let new_carrier_name () = new_carrier Carry_name true
130 136

  
131
let rec carrier_repr =
132
  function {carrier_desc = Carry_link cr'; _} -> carrier_repr cr'
133
    | cr -> cr
137
let rec repr = function { cdesc = Clink ck'; _ } -> repr ck' | ck -> ck
134 138

  
139
let rec carrier_repr = function
140
  | { carrier_desc = Carry_link cr'; _ } ->
141
    carrier_repr cr'
142
  | cr ->
143
    cr
135 144

  
136 145
let get_carrier_name ck =
137
 match (repr ck).cdesc with
138
 | Ccarrying (cr, _) -> Some cr
139
 | _                 -> None
146
  match (repr ck).cdesc with Ccarrying (cr, _) -> Some cr | _ -> None
140 147

  
141 148
let rename_carrier_static rename cr =
142 149
  match (carrier_repr cr).carrier_desc with
143
  | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
144
  | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
150
  | Carry_const id ->
151
    { cr with carrier_desc = Carry_const (rename id) }
152
  | _ ->
153
    Format.eprintf "internal error: Clocks.rename_carrier_static %a@."
154
      print_carrier cr;
155
    assert false
145 156

  
146 157
let rec rename_static rename ck =
147
 match (repr ck).cdesc with
148
 | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
149
 | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
150
 | _                   -> ck
151

  
152
let uncarrier ck =
153
 match ck.cdesc with
154
 | Ccarrying (_, ck') -> ck'
155
 | _                  -> ck
156

  
157
(* Removes all links in a clock. Only used for clocks
158
   simplification though. *)
158
  match (repr ck).cdesc with
159
  | Ccarrying (cr, ck') ->
160
    {
161
      ck with
162
      cdesc =
163
        Ccarrying (rename_carrier_static rename cr, rename_static rename ck');
164
    }
165
  | Con (ck', cr, l) ->
166
    {
167
      ck with
168
      cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l);
169
    }
170
  | _ ->
171
    ck
172

  
173
let uncarrier ck = match ck.cdesc with Ccarrying (_, ck') -> ck' | _ -> ck
174

  
175
(* Removes all links in a clock. Only used for clocks simplification though. *)
159 176
let rec simplify ck =
160 177
  match ck.cdesc with
161
  | Carrow (ck1,ck2) ->
162
      new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
178
  | Carrow (ck1, ck2) ->
179
    new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
163 180
  | Ctuple cl ->
164
      new_ck (Ctuple (List.map simplify cl)) ck.cscoped
181
    new_ck (Ctuple (List.map simplify cl)) ck.cscoped
165 182
  | Con (ck', c, l) ->
166
      new_ck (Con (simplify ck', c, l)) ck.cscoped
167
  | Cvar | Cunivar -> ck
168
  | Clink ck' -> simplify ck'
169
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
183
    new_ck (Con (simplify ck', c, l)) ck.cscoped
184
  | Cvar | Cunivar ->
185
    ck
186
  | Clink ck' ->
187
    simplify ck'
188
  | Ccarrying (cr, ck') ->
189
    new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
170 190

  
171 191
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
172 192
    (ensured by language syntax) *)
173 193
let split_arrow ck =
174 194
  match (repr ck).cdesc with
175
  | Carrow (cin,cout) -> cin,cout
176
  | _ -> failwith "Internal error: not an arrow clock"
195
  | Carrow (cin, cout) ->
196
    cin, cout
197
  | _ ->
198
    failwith "Internal error: not an arrow clock"
177 199

  
178 200
(** Returns the clock corresponding to a clock list. *)
179 201
let clock_of_clock_list ckl =
180
  if (List.length ckl) > 1 then
181
    new_ck (Ctuple ckl) true
182
  else
183
    List.hd ckl
202
  if List.length ckl > 1 then new_ck (Ctuple ckl) true else List.hd ckl
184 203

  
185 204
let clock_list_of_clock ck =
186
 match (repr ck).cdesc with
187
 | Ctuple cl -> cl
188
 | _         -> [ck]
205
  match (repr ck).cdesc with Ctuple cl -> cl | _ -> [ ck ]
189 206

  
190 207
let clock_on ck cr l =
191
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
208
  clock_of_clock_list
209
    (List.map
210
       (fun ck -> new_ck (Con (ck, cr, l)) true)
211
       (clock_list_of_clock ck))
192 212

  
193 213
let clock_current ck =
194
  clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with
195
      | Con(ck',_,_) -> ck'
196
      | _ -> Format.eprintf "internal error: Clocks.clock_current %a@." print_ck_long (repr ck);
197
        assert false) (clock_list_of_clock ck))
214
  clock_of_clock_list
215
    (List.map
216
       (fun ck ->
217
         match (repr ck).cdesc with
218
         | Con (ck', _, _) ->
219
           ck'
220
         | _ ->
221
           Format.eprintf "internal error: Clocks.clock_current %a@."
222
             print_ck_long (repr ck);
223
           assert false)
224
       (clock_list_of_clock ck))
198 225

  
199 226
let clock_of_impnode_clock ck =
200 227
  let ck = repr ck in
201 228
  match ck.cdesc with
202 229
  | Carrow _ | Clink _ | Cvar | Cunivar ->
203
      failwith "internal error clock_of_impnode_clock"
204
  | Ctuple cklist -> List.hd cklist
205
  | Con (_,_,_) 
206
  | Ccarrying (_,_) -> ck
207

  
230
    failwith "internal error clock_of_impnode_clock"
231
  | Ctuple cklist ->
232
    List.hd cklist
233
  | Con (_, _, _) | Ccarrying (_, _) ->
234
    ck
208 235

  
209 236
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
210 237
let rec is_polymorphic ck =
211 238
  match ck.cdesc with
212
  | Cvar -> false
213
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
214
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
215
  | Con (ck',_,_) -> is_polymorphic ck'
216
  | Cunivar  -> true
217
  | Clink ck' -> is_polymorphic ck'
218
  | Ccarrying (_,ck') -> is_polymorphic ck'
219

  
220
(** [constrained_vars_of_clock ck] returns the clock variables subject
221
    to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
239
  | Cvar ->
240
    false
241
  | Carrow (ck1, ck2) ->
242
    is_polymorphic ck1 || is_polymorphic ck2
243
  | Ctuple ckl ->
244
    List.exists (fun c -> is_polymorphic c) ckl
245
  | Con (ck', _, _) ->
246
    is_polymorphic ck'
247
  | Cunivar ->
248
    true
249
  | Clink ck' ->
250
    is_polymorphic ck'
251
  | Ccarrying (_, ck') ->
252
    is_polymorphic ck'
253

  
222 254
(* Used mainly for debug, non-linear complexity. *)
255

  
256
(** [constrained_vars_of_clock ck] returns the clock variables subject to
257
    sub-typing constraints appearing in clock [ck]. Removes duplicates *)
223 258
let constrained_vars_of_clock ck =
224 259
  let rec aux vars ck =
225 260
    match ck.cdesc with
226
    | Cvar -> vars
227
    | Carrow (ck1,ck2) ->
228
        let l = aux vars ck1 in
229
        aux l ck2
261
    | Cvar ->
262
      vars
263
    | Carrow (ck1, ck2) ->
264
      let l = aux vars ck1 in
265
      aux l ck2
230 266
    | Ctuple ckl ->
231
        List.fold_left
232
          (fun acc ck' -> aux acc ck') 
233
          vars ckl
234
    | Con (ck',_,_) -> aux vars ck'
235
    | Cunivar -> vars
236
    | Clink ck' -> aux vars ck'
237
    | Ccarrying (_,ck') -> aux vars ck'
267
      List.fold_left (fun acc ck' -> aux acc ck') vars ckl
268
    | Con (ck', _, _) ->
269
      aux vars ck'
270
    | Cunivar ->
271
      vars
272
    | Clink ck' ->
273
      aux vars ck'
274
    | Ccarrying (_, ck') ->
275
      aux vars ck'
238 276
  in
239 277
  aux [] ck
240 278

  
241 279
let eq_carrier cr1 cr2 =
242 280
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
243
 | Carry_const id1, Carry_const id2 -> id1 = id2
244
 | _                                -> cr1.carrier_id = cr2.carrier_id
281
  | Carry_const id1, Carry_const id2 ->
282
    id1 = id2
283
  | _ ->
284
    cr1.carrier_id = cr2.carrier_id
245 285

  
246
let eq_clock ck1 ck2 =
247
 (repr ck1).cid = (repr ck2).cid
286
let eq_clock ck1 ck2 = (repr ck1).cid = (repr ck2).cid
248 287

  
249 288
(* Returns the clock root of a clock *)
250 289
let rec root ck =
251 290
  let ck = repr ck in
252 291
  match ck.cdesc with
253
  | Ctuple (ck'::_)
254
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
255
  | Cvar | Cunivar -> ck
256
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
292
  | Ctuple (ck' :: _) | Con (ck', _, _) | Clink ck' | Ccarrying (_, ck') ->
293
    root ck'
294
  | Cvar | Cunivar ->
295
    ck
296
  | Carrow _ | Ctuple _ ->
297
    failwith "Internal error root"
257 298

  
258 299
(* Returns the branch of clock [ck] in its clock tree *)
259 300
let branch ck =
260 301
  let rec branch ck acc =
261 302
    match (repr ck).cdesc with
262
    | Ccarrying (_, ck) -> branch ck acc
263
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
264
    | Ctuple (ck::_)     -> branch ck acc
265
    | Ctuple _
266
    | Carrow _          -> assert false
267
    | _                 -> acc
268
  in branch ck [];;
303
    | Ccarrying (_, ck) ->
304
      branch ck acc
305
    | Con (ck, cr, l) ->
306
      branch ck ((cr, l) :: acc)
307
    | Ctuple (ck :: _) ->
308
      branch ck acc
309
    | Ctuple _ | Carrow _ ->
310
      assert false
311
    | _ ->
312
      acc
313
  in
314
  branch ck []
269 315

  
270 316
let clock_of_root_branch r br =
271
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
317
  List.fold_left (fun ck (cr, l) -> new_ck (Con (ck, cr, l)) true) r br
272 318

  
273 319
(* Computes the (longest) common prefix of two branches *)
274 320
let rec common_prefix br1 br2 =
275
 match br1, br2 with
276
 | []          , _
277
 | _           , []           -> []
278
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
279
   if eq_carrier cr1 cr2 && (l1 = l2)
280
   then (cr1, l1) :: common_prefix q1 q2
281
   else []
321
  match br1, br2 with
322
  | [], _ | _, [] ->
323
    []
324
  | (cr1, l1) :: q1, (cr2, l2) :: q2 ->
325
    if eq_carrier cr1 cr2 && l1 = l2 then (cr1, l1) :: common_prefix q1 q2
326
    else []
282 327

  
283 328
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
284 329
let rec disjoint_branches br1 br2 =
285
 match br1, br2 with
286
 | []          , _
287
 | _           , []           -> false
288
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
330
  match br1, br2 with
331
  | [], _ | _, [] ->
332
    false
333
  | (cr1, l1) :: q1, (cr2, l2) :: q2 ->
334
    eq_carrier cr1 cr2 && (l1 <> l2 || disjoint_branches q1 q2)
289 335

  
290 336
(* Disjunction relation between variables based upon their static clocks. *)
291 337
let disjoint ck1 ck2 =
......
294 340
let print_cvar fmt cvar =
295 341
  match cvar.cdesc with
296 342
  | Cvar ->
297
 (*
298
      if cvar.cscoped
299
      then
300
	fprintf fmt "[_%s]"
301
	  (name_of_type cvar.cid)
302
      else
303
 *)
304
	fprintf fmt "_%s"
305
	  (name_of_type cvar.cid)
343
    (* if cvar.cscoped then fprintf fmt "[_%s]" (name_of_type cvar.cid) else *)
344
    fprintf fmt "_%s" (name_of_type cvar.cid)
306 345
  | Cunivar ->
307
 (*
308
      if cvar.cscoped
309
      then
310
	fprintf fmt "['%s]"
311
	  (name_of_type cvar.cid)
312
      else
313
 *)
314
	fprintf fmt "'%s"
315
	  (name_of_type cvar.cid)
316
  | _ -> failwith "Internal error print_cvar"
346
    (* if cvar.cscoped then fprintf fmt "['%s]" (name_of_type cvar.cid) else *)
347
    fprintf fmt "'%s" (name_of_type cvar.cid)
348
  | _ ->
349
    failwith "Internal error print_cvar"
317 350

  
318 351
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
319 352
   complexity. *)
320 353
let print_ck fmt ck =
321 354
  let rec aux fmt ck =
322 355
    match ck.cdesc with
323
    | Carrow (ck1,ck2) ->
356
    | Carrow (ck1, ck2) ->
324 357
      fprintf fmt "%a -> %a" aux ck1 aux ck2
325 358
    | Ctuple cklist ->
326
      fprintf fmt "(%a)" 
327
	(fprintf_list ~sep:" * " aux) cklist
328
    | Con (ck,c,l) ->
359
      fprintf fmt "(%a)" (fprintf_list ~sep:" * " aux) cklist
360
    | Con (ck, c, l) ->
329 361
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
330 362
    | Cvar ->
331
(*
332
      if ck.cscoped
333
      then
334
        fprintf fmt "[_%s]" (name_of_type ck.cid)
335
      else
336
*)
337
	fprintf fmt "_%s" (name_of_type ck.cid)
363
      (* if ck.cscoped then fprintf fmt "[_%s]" (name_of_type ck.cid) else *)
364
      fprintf fmt "_%s" (name_of_type ck.cid)
338 365
    | Cunivar ->
339
(*
340
      if ck.cscoped
341
      then
342
        fprintf fmt "['%s]" (name_of_type ck.cid)
343
      else
344
*)
345
        fprintf fmt "'%s" (name_of_type ck.cid)
366
      (* if ck.cscoped then fprintf fmt "['%s]" (name_of_type ck.cid) else *)
367
      fprintf fmt "'%s" (name_of_type ck.cid)
346 368
    | Clink ck' ->
347
        aux fmt ck'
348
    | Ccarrying (cr,ck') ->
369
      aux fmt ck'
370
    | Ccarrying (cr, ck') ->
349 371
      fprintf fmt "(%a:%a)" print_carrier cr aux ck'
350 372
  in
351 373
  let cvars = constrained_vars_of_clock ck in
352 374
  aux fmt ck;
353 375
  if cvars <> [] then
354
    fprintf fmt " (where %a)"
355
      (fprintf_list ~sep:", " print_cvar) cvars
376
    fprintf fmt " (where %a)" (fprintf_list ~sep:", " print_cvar) cvars
356 377

  
357 378
(* prints only the Con components of a clock, useful for printing nodes *)
358 379
let rec print_ck_suffix fmt ck =
359 380
  match ck.cdesc with
360
  | Carrow _
361
  | Ctuple _
362
  | Cvar 
363
  | Cunivar    -> ()
364
  | Con (ck,c,l) ->
365
     if !Options.kind2_print then
366
       print_ck_suffix fmt ck
367
     else
368
       fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
381
  | Carrow _ | Ctuple _ | Cvar | Cunivar ->
382
    ()
383
  | Con (ck, c, l) ->
384
    if !Options.kind2_print then print_ck_suffix fmt ck
385
    else fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
369 386
  | Clink ck' ->
370 387
    print_ck_suffix fmt ck'
371 388
  | Ccarrying (_, ck') ->
372 389
    fprintf fmt "%a" print_ck_suffix ck'
373 390

  
374

  
375 391
let pp_error fmt = function
376
  | Clock_clash (ck1,ck2) ->
377
      reset_names ();
378
      fprintf fmt "Expected clock %a, got clock %a@."
379
      print_ck ck1
380
      print_ck ck2
392
  | Clock_clash (ck1, ck2) ->
393
    reset_names ();
394
    fprintf fmt "Expected clock %a, got clock %a@." print_ck ck1 print_ck ck2
381 395
  | Carrier_mismatch (cr1, cr2) ->
382
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
383
       print_carrier cr1
384
       print_carrier cr2
396
    fprintf fmt "Name clash. Expected clock %a, got clock %a@." print_carrier
397
      cr1 print_carrier cr2
385 398
  | Cannot_be_polymorphic ck ->
386
      reset_names ();
387
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
388
      print_ck ck
399
    reset_names ();
400
    fprintf fmt "The main node cannot have a polymorphic clock: %a@." print_ck
401
      ck
389 402
  | Invalid_imported_clock ck ->
390
      reset_names ();
391
    fprintf fmt "Not a valid imported node clock: %a@."
392
      print_ck ck
403
    reset_names ();
404
    fprintf fmt "Not a valid imported node clock: %a@." print_ck ck
393 405
  | Invalid_const ck ->
394
      reset_names ();
395
    fprintf fmt "Clock %a is not a valid periodic clock@."
396
      print_ck ck;
406
    reset_names ();
407
    fprintf fmt "Clock %a is not a valid periodic clock@." print_ck ck
397 408
  | Factor_zero ->
398 409
    fprintf fmt "Cannot apply clock transformation with factor 0@."
399
  | Carrier_extrusion (ck,cr) ->
400
    fprintf fmt "This node has clock@.%a@.It is invalid as the carrier %a escapes its scope@."
401
      print_ck ck
402
      print_carrier cr
403
  | Clock_extrusion (ck_node,ck) ->
404
    fprintf fmt "This node has clock@.%a@.It is invalid as the clock %a escapes its scope@."
405
      print_ck ck_node
406
      print_ck ck
410
  | Carrier_extrusion (ck, cr) ->
411
    fprintf fmt
412
      "This node has clock@.%a@.It is invalid as the carrier %a escapes its \
413
       scope@."
414
      print_ck ck print_carrier cr
415
  | Clock_extrusion (ck_node, ck) ->
416
    fprintf fmt
417
      "This node has clock@.%a@.It is invalid as the clock %a escapes its \
418
       scope@."
419
      print_ck ck_node print_ck ck
407 420

  
408 421
let const_of_carrier cr =
409 422
  match (carrier_repr cr).carrier_desc with
410
  | Carry_const id -> id
411
  | Carry_name
412
  | Carry_var
413
  | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
414
 
423
  | Carry_const id ->
424
    id
425
  | Carry_name | Carry_var | Carry_link _ ->
426
    Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr;
427
    assert false
428
(* TODO check this Xavier *)
429

  
415 430
let uneval const cr =
416 431
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
417 432
  let cr = carrier_repr cr in
418 433
  match cr.carrier_desc with
419
  | Carry_var -> cr.carrier_desc <- Carry_const const
420
  | Carry_name -> cr.carrier_desc <- Carry_const const
421
  | _         -> assert false
422

  
434
  | Carry_var ->
435
    cr.carrier_desc <- Carry_const const
436
  | Carry_name ->
437
    cr.carrier_desc <- Carry_const const
438
  | _ ->
439
    assert false
423 440

  
424 441
(* Used in rename functions in Corelang. We have to propagate the renaming to
425 442
   ids of variables clocking the signals *)
426 443

  
427 444
(* Carrier are not renamed. They corresponds to enumerated type constants *)
428
(*
429
let rec rename_carrier f c =
430
  { c with carrier_desc = rename_carrier_desc fvar c.carrier_desc }
431
and rename_carrier_desc f 
432
let re = rename_carrier f
433
  match cd with
434
  | Carry_const id -> Carry_const (f id)
435
  | Carry_link ce -> Carry_link (re ce)
436
  | _ -> cd
437
*)
445
(* let rec rename_carrier f c = { c with carrier_desc = rename_carrier_desc fvar
446
   c.carrier_desc } and rename_carrier_desc f let re = rename_carrier f match cd
447
   with | Carry_const id -> Carry_const (f id) | Carry_link ce -> Carry_link (re
448
   ce) | _ -> cd *)
438 449

  
439
     
440 450
let rec rename_clock_expr fvar c =
441 451
  { c with cdesc = rename_clock_desc fvar c.cdesc }
452

  
442 453
and rename_clock_desc fvar cd =
443 454
  let re = rename_clock_expr fvar in
444 455
  match cd with
445
  | Carrow (c1, c2) -> Carrow (re c1, re c2)
446
  | Ctuple cl -> Ctuple (List.map re cl)
447
  | Con (c1, car, id) -> Con (re c1, car, fvar id)
448
  | Cvar 
449
  | Cunivar -> cd
450
  | Clink c -> Clink (re c)
451
  | Ccarrying (car, c) -> Ccarrying (car, re c)
452
    
456
  | Carrow (c1, c2) ->
457
    Carrow (re c1, re c2)
458
  | Ctuple cl ->
459
    Ctuple (List.map re cl)
460
  | Con (c1, car, id) ->
461
    Con (re c1, car, fvar id)
462
  | Cvar | Cunivar ->
463
    cd
464
  | Clink c ->
465
    Clink (re c)
466
  | Ccarrying (car, c) ->
467
    Ccarrying (car, re c)
468

  
453 469
(* Local Variables: *)
454 470
(* compile-command:"make -C .." *)
455 471
(* End: *)

Also available in: Unified diff