Project

General

Profile

Download (14 KB) Statistics
| Branch: | Tag: | Revision:
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT - LIFL             *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(*  This file was originally from the Prelude compiler              *)
11
(*                                                                  *)
12
(********************************************************************)
13

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

    
17
open Format
18

    
19
(* (\* Clock type sets, for subtyping. *\) *)
20
(* type clock_set = *)
21
(*     CSet_all *)
22
(*   | CSet_pck of int*rat *)
23

    
24
(* Clock carriers basically correspond to the "c" in "x when c" *)
25
type carrier_desc =
26
  | Carry_const of ident
27
  | Carry_name
28
  | Carry_var
29
  | Carry_link of carrier_expr
30

    
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
}
44

    
45
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
46
and clock_desc =
47
  | Carrow of clock_expr * clock_expr
48
  | Ctuple of clock_expr list
49
  | Con of clock_expr * carrier_expr * ident
50
  (* | Pck_up of clock_expr * int *)
51
  (* | Pck_down of clock_expr * int *)
52
  (* | Pck_phase of clock_expr * rat *)
53
  (* | Pck_const of int * rat *)
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 *)
61
  | Ccarrying of carrier_expr * clock_expr
62

    
63
type error =
64
  | Clock_clash of clock_expr * clock_expr
65
  (* | Not_pck *)
66
  (* | Clock_set_mismatch of clock_expr * clock_set *)
67
  | Cannot_be_polymorphic of clock_expr
68
  | Invalid_imported_clock of clock_expr
69
  | Invalid_const of clock_expr
70
  | Factor_zero
71
  | Carrier_mismatch of carrier_expr * carrier_expr
72
  | Carrier_extrusion of clock_expr * carrier_expr
73
  | Clock_extrusion of clock_expr * clock_expr
74

    
75
exception Unify of clock_expr * clock_expr
76

    
77
exception Mismatch of carrier_expr * carrier_expr
78

    
79
exception Scope_carrier of carrier_expr
80

    
81
exception Scope_clock of clock_expr
82

    
83
exception Error of Location.t * error
84

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

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

    
117
let new_id = ref (-1)
118

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

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

    
125
let new_var scoped = new_ck Cvar scoped
126

    
127
let new_univar () = new_ck Cunivar false
128

    
129
let new_carrier_id = ref (-1)
130

    
131
let new_carrier desc scoped =
132
  incr new_carrier_id;
133
  { carrier_desc = desc; carrier_id = !new_carrier_id; carrier_scoped = scoped }
134

    
135
let new_carrier_name () = new_carrier Carry_name true
136

    
137
let rec repr = function { cdesc = Clink ck'; _ } -> repr ck' | ck -> ck
138

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

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

    
148
let rename_carrier_static rename cr =
149
  match (carrier_repr cr).carrier_desc with
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
156

    
157
let rec rename_static rename ck =
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. *)
176
let rec simplify ck =
177
  match ck.cdesc with
178
  | Carrow (ck1, ck2) ->
179
    new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
180
  | Ctuple cl ->
181
    new_ck (Ctuple (List.map simplify cl)) ck.cscoped
182
  | Con (ck', c, l) ->
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
190

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

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

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

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

    
213
let clock_current 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))
225

    
226
let clock_of_impnode_clock ck =
227
  let ck = repr ck in
228
  match ck.cdesc with
229
  | Carrow _ | Clink _ | Cvar | Cunivar ->
230
    failwith "internal error clock_of_impnode_clock"
231
  | Ctuple cklist ->
232
    List.hd cklist
233
  | Con (_, _, _) | Ccarrying (_, _) ->
234
    ck
235

    
236
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
237
let rec is_polymorphic ck =
238
  match ck.cdesc with
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

    
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 *)
258
let constrained_vars_of_clock ck =
259
  let rec aux vars ck =
260
    match ck.cdesc with
261
    | Cvar ->
262
      vars
263
    | Carrow (ck1, ck2) ->
264
      let l = aux vars ck1 in
265
      aux l ck2
266
    | Ctuple ckl ->
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'
276
  in
277
  aux [] ck
278

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

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

    
288
(* Returns the clock root of a clock *)
289
let rec root ck =
290
  let ck = repr ck in
291
  match ck.cdesc with
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"
298

    
299
(* Returns the branch of clock [ck] in its clock tree *)
300
let branch ck =
301
  let rec branch ck acc =
302
    match (repr ck).cdesc with
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 []
315

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

    
319
(* Computes the (longest) common prefix of two branches *)
320
let rec common_prefix br1 br2 =
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 []
327

    
328
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
329
let rec disjoint_branches br1 br2 =
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)
335

    
336
(* Disjunction relation between variables based upon their static clocks. *)
337
let disjoint ck1 ck2 =
338
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
339

    
340
let print_cvar fmt cvar =
341
  match cvar.cdesc with
342
  | Cvar ->
343
    (* if cvar.cscoped then fprintf fmt "[_%s]" (name_of_type cvar.cid) else *)
344
    fprintf fmt "_%s" (name_of_type cvar.cid)
345
  | Cunivar ->
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"
350

    
351
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
352
   complexity. *)
353
let print_ck fmt ck =
354
  let rec aux fmt ck =
355
    match ck.cdesc with
356
    | Carrow (ck1, ck2) ->
357
      fprintf fmt "%a -> %a" aux ck1 aux ck2
358
    | Ctuple cklist ->
359
      fprintf fmt "(%a)" (fprintf_list ~sep:" * " aux) cklist
360
    | Con (ck, c, l) ->
361
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
362
    | Cvar ->
363
      (* if ck.cscoped then fprintf fmt "[_%s]" (name_of_type ck.cid) else *)
364
      fprintf fmt "_%s" (name_of_type ck.cid)
365
    | Cunivar ->
366
      (* if ck.cscoped then fprintf fmt "['%s]" (name_of_type ck.cid) else *)
367
      fprintf fmt "'%s" (name_of_type ck.cid)
368
    | Clink ck' ->
369
      aux fmt ck'
370
    | Ccarrying (cr, ck') ->
371
      fprintf fmt "(%a:%a)" print_carrier cr aux ck'
372
  in
373
  let cvars = constrained_vars_of_clock ck in
374
  aux fmt ck;
375
  if cvars <> [] then
376
    fprintf fmt " (where %a)" (fprintf_list ~sep:", " print_cvar) cvars
377

    
378
(* prints only the Con components of a clock, useful for printing nodes *)
379
let rec print_ck_suffix fmt ck =
380
  match ck.cdesc with
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
386
  | Clink ck' ->
387
    print_ck_suffix fmt ck'
388
  | Ccarrying (_, ck') ->
389
    fprintf fmt "%a" print_ck_suffix ck'
390

    
391
let pp_error fmt = function
392
  | Clock_clash (ck1, ck2) ->
393
    reset_names ();
394
    fprintf fmt "Expected clock %a, got clock %a@." print_ck ck1 print_ck ck2
395
  | Carrier_mismatch (cr1, cr2) ->
396
    fprintf fmt "Name clash. Expected clock %a, got clock %a@." print_carrier
397
      cr1 print_carrier cr2
398
  | Cannot_be_polymorphic ck ->
399
    reset_names ();
400
    fprintf fmt "The main node cannot have a polymorphic clock: %a@." print_ck
401
      ck
402
  | Invalid_imported_clock ck ->
403
    reset_names ();
404
    fprintf fmt "Not a valid imported node clock: %a@." print_ck ck
405
  | Invalid_const ck ->
406
    reset_names ();
407
    fprintf fmt "Clock %a is not a valid periodic clock@." print_ck ck
408
  | Factor_zero ->
409
    fprintf fmt "Cannot apply clock transformation with factor 0@."
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
420

    
421
let const_of_carrier cr =
422
  match (carrier_repr cr).carrier_desc with
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

    
430
let uneval const cr =
431
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
432
  let cr = carrier_repr cr in
433
  match cr.carrier_desc with
434
  | Carry_var ->
435
    cr.carrier_desc <- Carry_const const
436
  | Carry_name ->
437
    cr.carrier_desc <- Carry_const const
438
  | _ ->
439
    assert false
440

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

    
444
(* Carrier are not renamed. They corresponds to enumerated type constants *)
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 *)
449

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

    
453
and rename_clock_desc fvar cd =
454
  let re = rename_clock_expr fvar in
455
  match cd with
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

    
469
(* Local Variables: *)
470
(* compile-command:"make -C .." *)
471
(* End: *)
(12-12/66)