Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / src / clocks.ml @ 45f0f48d

History | View | Annotate | Download (13.4 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

    
37
type clock_expr =
38
    {mutable cdesc: clock_desc;
39
     mutable cscoped: bool;
40
     cid: int}
41

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

    
56
type error =
57
  | Clock_clash of clock_expr * clock_expr
58
  (* | Not_pck *)
59
  (* | Clock_set_mismatch of clock_expr * clock_set *)
60
  | Cannot_be_polymorphic of clock_expr
61
  | Invalid_imported_clock of clock_expr
62
  | Invalid_const of clock_expr
63
  | Factor_zero
64
  | Carrier_mismatch of carrier_expr * carrier_expr
65
  | Carrier_extrusion of clock_expr * carrier_expr
66
  | Clock_extrusion of clock_expr * clock_expr
67

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

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

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

    
103
let new_id = ref (-1)
104

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

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

    
111
let new_var scoped = new_ck Cvar scoped
112

    
113
let new_univar () = new_ck Cunivar false
114

    
115
let new_carrier_id = ref (-1)
116

    
117
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
124

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

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

    
135
(** Splits [ck] into the [lhs,rhs] of an arrow clock. Expects an arrow clock
136
    (ensured by language syntax) *)
137
let split_arrow ck =
138
  match (repr ck).cdesc with
139
  | Carrow (cin,cout) -> cin,cout
140
    (* Functions are not first order, I don't think the var case
141
       needs to be considered here *)
142
  | _ -> failwith "Internal error: not an arrow clock"
143

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

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

    
154
let rec rename_static rename ck =
155
 match (repr ck).cdesc with
156
 | Ccarrying (cr, ck') -> { ck with cdesc = Ccarrying (rename_carrier_static rename cr, rename_static rename ck') }
157
 | Con (ck', cr, l)    -> { ck with cdesc = Con (rename_static rename ck', rename_carrier_static rename cr, l) }
158
 | _                   -> ck
159

    
160
let uncarrier ck =
161
 match ck.cdesc with
162
 | Ccarrying (_, ck') -> ck'
163
 | _                  -> ck
164

    
165
(* Removes all links in a clock. Only used for clocks
166
   simplification though. *)
167
let rec simplify ck =
168
  match ck.cdesc with
169
  | Carrow (ck1,ck2) ->
170
      new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
171
  | Ctuple cl ->
172
      new_ck (Ctuple (List.map simplify cl)) ck.cscoped
173
  | Con (ck', c, l) ->
174
      new_ck (Con (simplify ck', c, l)) ck.cscoped
175
  | Cvar | Cunivar -> ck
176
  | Clink ck' -> simplify ck'
177
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, simplify ck')) ck.cscoped
178

    
179
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
180
    (ensured by language syntax) *)
181
let split_arrow ck =
182
  match (repr ck).cdesc with
183
  | Carrow (cin,cout) -> cin,cout
184
  | _ -> failwith "Internal error: not an arrow clock"
185

    
186
(** Returns the clock corresponding to a clock list. *)
187
let clock_of_clock_list ckl =
188
  if (List.length ckl) > 1 then
189
    new_ck (Ctuple ckl) true
190
  else
191
    List.hd ckl
192

    
193
let clock_list_of_clock ck =
194
 match (repr ck).cdesc with
195
 | Ctuple cl -> cl
196
 | _         -> [ck]
197

    
198
let clock_on ck cr l =
199
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
200

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

    
204
let clock_of_impnode_clock ck =
205
  let ck = repr ck in
206
  match ck.cdesc with
207
  | Carrow _ | Clink _ | Cvar | Cunivar ->
208
      failwith "internal error clock_of_impnode_clock"
209
  | Ctuple cklist -> List.hd cklist
210
  | Con (_,_,_) 
211
  | Ccarrying (_,_) -> ck
212

    
213

    
214
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
215
let rec is_polymorphic ck =
216
  match ck.cdesc with
217
  | Cvar -> false
218
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
219
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
220
  | Con (ck',_,_) -> is_polymorphic ck'
221
  | Cunivar  -> true
222
  | Clink ck' -> is_polymorphic ck'
223
  | Ccarrying (_,ck') -> is_polymorphic ck'
224

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

    
246
let eq_carrier cr1 cr2 =
247
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
248
 | Carry_const id1, Carry_const id2 -> id1 = id2
249
 | _                                -> cr1.carrier_id = cr2.carrier_id
250

    
251
let eq_clock ck1 ck2 =
252
 (repr ck1).cid = (repr ck2).cid
253

    
254
(* Returns the clock root of a clock *)
255
let rec root ck =
256
  let ck = repr ck in
257
  match ck.cdesc with
258
  | Ctuple (ck'::_)
259
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
260
  | Cvar | Cunivar -> ck
261
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
262

    
263
(* Returns the branch of clock [ck] in its clock tree *)
264
let rec branch ck =
265
  let rec branch ck acc =
266
    match (repr ck).cdesc with
267
    | Ccarrying (_, ck) -> branch ck acc
268
    | Con (ck, cr, l)   -> branch ck ((cr, l) :: acc)
269
    | Ctuple (ck::_)    -> branch ck acc
270
    | Ctuple _
271
    | Carrow _          -> assert false
272
    | _                 -> acc
273
  in branch ck [];;
274

    
275
let clock_of_root_branch r br =
276
 List.fold_left (fun ck (cr,l) -> new_ck (Con (ck, cr, l)) true) r br
277

    
278
(* Computes the (longest) common prefix of two branches *)
279
let rec common_prefix br1 br2 =
280
 match br1, br2 with
281
 | []          , _
282
 | _           , []           -> []
283
 | (cr1,l1)::q1, (cr2,l2)::q2 ->
284
   if eq_carrier cr1 cr2 && (l1 = l2)
285
   then (cr1, l1) :: common_prefix q1 q2
286
   else []
287

    
288
(* Tests whether clock branches [br1] nd [br2] are statically disjoint *)
289
let rec disjoint_branches br1 br2 =
290
 match br1, br2 with
291
 | []          , _
292
 | _           , []           -> false
293
 | (cr1,l1)::q1, (cr2,l2)::q2 -> eq_carrier cr1 cr2 && ((l1 <> l2) || disjoint_branches q1 q2);;
294

    
295
(* Disjunction relation between variables based upon their static clocks. *)
296
let disjoint ck1 ck2 =
297
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
298

    
299
let print_cvar fmt cvar =
300
  match cvar.cdesc with
301
  | Cvar ->
302
 (*
303
      if cvar.cscoped
304
      then
305
	fprintf fmt "[_%s]"
306
	  (name_of_type cvar.cid)
307
      else
308
 *)
309
	fprintf fmt "_%s"
310
	  (name_of_type cvar.cid)
311
  | Cunivar ->
312
 (*
313
      if cvar.cscoped
314
      then
315
	fprintf fmt "['%s]"
316
	  (name_of_type cvar.cid)
317
      else
318
 *)
319
	fprintf fmt "'%s"
320
	  (name_of_type cvar.cid)
321
  | _ -> failwith "Internal error print_cvar"
322

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

    
362
(* prints only the Con components of a clock, useful for printing nodes *)
363
let rec print_ck_suffix fmt ck =
364
  match ck.cdesc with
365
  | Carrow _
366
  | Ctuple _
367
  | Cvar 
368
  | Cunivar    -> ()
369
  | Con (ck,c,l) ->
370
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
371
  | Clink ck' ->
372
    print_ck_suffix fmt ck'
373
  | Ccarrying (cr,ck') ->
374
    fprintf fmt "%a" print_ck_suffix ck'
375

    
376

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

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

    
425
(* Local Variables: *)
426
(* compile-command:"make -C .." *)
427
(* End: *)