Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / lib / clocks.ml @ 9b0432bc

History | View | Annotate | Download (14 KB)

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
(** Clocks definitions and a few utility functions on clocks. *)
15
open Utils
16
open Format
17

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

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

    
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
[@@deriving show]
37
     
38
type clock_expr =
39
    {mutable cdesc: clock_desc;
40
     mutable cscoped: bool;
41
     cid: int}
42

    
43
(* pck stands for periodic clock. Easier not to separate pck from other clocks *)
44
and clock_desc =
45
  | Carrow of clock_expr * clock_expr (* clock of a node *)
46
  | Ctuple of clock_expr list (* clock of a tuple expression *)
47
  | Con of clock_expr * carrier_expr * ident
48
  (* | Pck_up of clock_expr * int *)
49
  (* | Pck_down of clock_expr * int *)
50
  (* | Pck_phase of clock_expr * rat *)
51
  (* | Pck_const of int * rat *)
52
  | Cvar (* of clock_set *) (* Monomorphic clock variable *)
53
  | Cunivar (* of clock_set *) (* Polymorphic clock variable *)
54
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
55
  | Ccarrying of carrier_expr * clock_expr
56
[@@deriving show]
57
type error =
58
  | Clock_clash of clock_expr * clock_expr
59
  (* | Not_pck *)
60
  (* | Clock_set_mismatch of clock_expr * clock_set *)
61
  | Cannot_be_polymorphic of clock_expr
62
  | Invalid_imported_clock of clock_expr
63
  | Invalid_const of clock_expr
64
  | Factor_zero
65
  | Carrier_mismatch of carrier_expr * carrier_expr
66
  | Carrier_extrusion of clock_expr * carrier_expr
67
  | Clock_extrusion of clock_expr * clock_expr
68

    
69
exception Unify of clock_expr * clock_expr
70
exception Mismatch of carrier_expr * carrier_expr
71
exception Scope_carrier of carrier_expr
72
exception Scope_clock of clock_expr
73
exception Error of Location.t * error
74

    
75
let rec print_carrier fmt cr =
76
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
77
  match cr.carrier_desc with
78
  | Carry_const id -> fprintf fmt "%s" id
79
  | Carry_name ->
80
      fprintf fmt "_%s" (name_of_carrier cr.carrier_id)
81
  | Carry_var ->
82
    fprintf fmt "'%s" (name_of_carrier cr.carrier_id)
83
  | Carry_link cr' ->
84
    print_carrier fmt cr'
85

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

    
104
let new_id = ref (-1)
105

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

    
109
let new_ck desc scoped =
110
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
111

    
112
let new_var scoped = new_ck Cvar scoped
113

    
114
let new_univar () = new_ck Cunivar false
115

    
116
let new_carrier_id = ref (-1)
117

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

    
123
let new_carrier_name () =
124
  new_carrier Carry_name true
125

    
126
let rec repr =
127
  function
128
      {cdesc=Clink ck'} ->
129
        repr ck'
130
    | ck -> ck
131

    
132
let rec carrier_repr =
133
  function {carrier_desc = Carry_link cr'} -> carrier_repr cr'
134
    | cr -> cr
135

    
136

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

    
142
let rename_carrier_static rename cr =
143
  match (carrier_repr cr).carrier_desc with
144
  | Carry_const id -> { cr with carrier_desc = Carry_const (rename id) }
145
  | _              -> (Format.eprintf "internal error: Clocks.rename_carrier_static %a@." print_carrier cr; assert false)
146

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

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

    
158
(* Removes all links in a clock. Only used for clocks
159
   simplification though. *)
160
let rec simplify ck =
161
  match ck.cdesc with
162
  | Carrow (ck1,ck2) ->
163
      new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
164
  | Ctuple cl ->
165
      new_ck (Ctuple (List.map simplify cl)) ck.cscoped
166
  | Con (ck', c, l) ->
167
      new_ck (Con (simplify ck', c, l)) ck.cscoped
168
  | Cvar | Cunivar -> ck
169
  | Clink ck' -> simplify ck'
170
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
171

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

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

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

    
191
let clock_on ck cr l =
192
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
193

    
194
let clock_current ck =
195
 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
196

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

    
206

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

    
218
(** [constrained_vars_of_clock ck] returns the clock variables subject
219
    to sub-typing constraints appearing in clock [ck]. Removes duplicates *)
220
(* Used mainly for debug, non-linear complexity. *)
221
let rec constrained_vars_of_clock ck =
222
  let rec aux vars ck =
223
    match ck.cdesc with
224
    | Cvar -> vars
225
    | Carrow (ck1,ck2) ->
226
        let l = aux vars ck1 in
227
        aux l ck2
228
    | Ctuple ckl ->
229
        List.fold_left
230
          (fun acc ck' -> aux acc ck') 
231
          vars ckl
232
    | Con (ck',_,_) -> aux vars ck'
233
    | Cunivar -> vars
234
    | Clink ck' -> aux vars ck'
235
    | Ccarrying (_,ck') -> aux vars ck'
236
  in
237
  aux [] ck
238

    
239
let eq_carrier cr1 cr2 =
240
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
241
 | Carry_const id1, Carry_const id2 -> id1 = id2
242
 | _                                -> cr1.carrier_id = cr2.carrier_id
243

    
244
let eq_clock ck1 ck2 =
245
 (repr ck1).cid = (repr ck2).cid
246

    
247
(* Returns the clock root of a clock *)
248
let rec root ck =
249
  let ck = repr ck in
250
  match ck.cdesc with
251
  | Ctuple (ck'::_)
252
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
253
  | Cvar | Cunivar -> ck
254
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
255

    
256
(* Returns the branch of clock [ck] in its clock tree *)
257
let rec branch ck =
258
  let rec branch ck acc =
259
    match (repr ck).cdesc with
260
    | Ccarrying (_, ck) -> branch ck acc
261
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
262
    | Ctuple (ck::_)    -> branch ck acc
263
    | Ctuple _
264
    | Carrow _          -> assert false
265
    | _                 -> acc
266
  in branch ck [];;
267

    
268
let clock_of_root_branch r br =
269
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
270

    
271
(* Computes the (longest) common prefix of two branches *)
272
let rec common_prefix br1 br2 =
273
 match br1, br2 with
274
 | []          , _
275
 | _           , []           -> []
276
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
277
   if eq_carrier cr1 cr2 && (l1 = l2)
278
   then (cr1, l1) :: common_prefix q1 q2
279
   else []
280

    
281
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
282
let rec disjoint_branches br1 br2 =
283
 match br1, br2 with
284
 | []          , _
285
 | _           , []           -> false
286
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
287

    
288
(* Disjunction relation between variables based upon their static clocks. *)
289
let disjoint ck1 ck2 =
290
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
291

    
292
let print_cvar fmt cvar =
293
  match cvar.cdesc with
294
  | Cvar ->
295
 (*
296
      if cvar.cscoped
297
      then
298
	fprintf fmt "[_%s]"
299
	  (name_of_type cvar.cid)
300
      else
301
 *)
302
	fprintf fmt "_%s"
303
	  (name_of_type cvar.cid)
304
  | Cunivar ->
305
 (*
306
      if cvar.cscoped
307
      then
308
	fprintf fmt "['%s]"
309
	  (name_of_type cvar.cid)
310
      else
311
 *)
312
	fprintf fmt "'%s"
313
	  (name_of_type cvar.cid)
314
  | _ -> failwith "Internal error print_cvar"
315

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

    
355
(* prints only the Con components of a clock, useful for printing nodes *)
356
let rec print_ck_suffix fmt ck =
357
  match ck.cdesc with
358
  | Carrow _
359
  | Ctuple _
360
  | Cvar 
361
  | Cunivar    -> ()
362
  | Con (ck,c,l) ->
363
     if !Options.kind2_print then
364
       print_ck_suffix fmt ck
365
     else
366
       fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
367
  | Clink ck' ->
368
    print_ck_suffix fmt ck'
369
  | Ccarrying (cr,ck') ->
370
    fprintf fmt "%a" print_ck_suffix ck'
371

    
372

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

    
406
let const_of_carrier cr =
407
  match (carrier_repr cr).carrier_desc with
408
  | Carry_const id -> id
409
  | Carry_name
410
  | Carry_var
411
  | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
412
 
413
let uneval const cr =
414
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)
415
  let cr = carrier_repr cr in
416
  match cr.carrier_desc with
417
  | Carry_var -> cr.carrier_desc <- Carry_const const
418
  | Carry_name -> cr.carrier_desc <- Carry_const const
419
  | _         -> assert false
420

    
421

    
422
(* Used in rename functions in Corelang. We have to propagate the renaming to
423
   ids of variables clocking the signals *)
424

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

    
437
     
438
let rec rename_clock_expr fvar c =
439
  { c with cdesc = rename_clock_desc fvar c.cdesc }
440
and rename_clock_desc fvar cd =
441
  let re = rename_clock_expr fvar in
442
  match cd with
443
  | Carrow (c1, c2) -> Carrow (re c1, re c2)
444
  | Ctuple cl -> Ctuple (List.map re cl)
445
  | Con (c1, car, id) -> Con (re c1, car, fvar id)
446
  | Cvar 
447
  | Cunivar -> cd
448
  | Clink c -> Clink (re c)
449
  | Ccarrying (car, c) -> Ccarrying (car, re c)
450
    
451
(* Local Variables: *)
452
(* compile-command:"make -C .." *)
453
(* End: *)