Project

General

Profile

Revision 45f0f48d src/clocks.ml

View differences:

src/clocks.ml
15 15
open Utils
16 16
open Format
17 17

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

  
23 23
(* Clock carriers basically correspond to the "c" in "x when c" *)
24 24
type carrier_desc =
......
44 44
  | Carrow of clock_expr * clock_expr
45 45
  | Ctuple of clock_expr list
46 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 *)
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 53
  | Clink of clock_expr (* During unification, make links instead of substitutions *)
54 54
  | Ccarrying of carrier_expr * clock_expr
55 55

  
56 56
type error =
57 57
  | Clock_clash of clock_expr * clock_expr
58
  | Not_pck
59
  | Clock_set_mismatch of clock_expr * clock_set
58
  (* | Not_pck *)
59
  (* | Clock_set_mismatch of clock_expr * clock_set *)
60 60
  | Cannot_be_polymorphic of clock_expr
61 61
  | Invalid_imported_clock of clock_expr
62 62
  | Invalid_const of clock_expr
......
66 66
  | Clock_extrusion of clock_expr * clock_expr
67 67

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

  
75
let print_ckset fmt s =
76
  match s with
77
  | CSet_all -> ()
78
  | CSet_pck (k,q) ->
79
      let (a,b) = simplify_rat q in
80
      if k = 1 && a = 0 then
81
        fprintf fmt "<:P"
82
      else
83
        fprintf fmt "<:P_(%i,%a)" k print_rat (a,b)
84

  
85 74
let rec print_carrier fmt cr =
86 75
 (* (if cr.carrier_scoped then fprintf fmt "[%t]" else fprintf fmt "%t") (fun fmt -> *)
87 76
  match cr.carrier_desc with
......
104 93
      (fprintf_list ~sep:" * " print_ck_long) cklist
105 94
  | Con (ck,c,l) ->
106 95
    fprintf fmt "%a on %s(%a)" print_ck_long ck l print_carrier c
107
  | Pck_up (ck,k) ->
108
    fprintf fmt "%a*^%i" print_ck_long ck k
109
  | Pck_down (ck,k) ->
110
    fprintf fmt "%a/^%i" print_ck_long ck k
111
  | Pck_phase (ck,q) ->
112
    fprintf fmt "%a~>%a" print_ck_long ck print_rat (simplify_rat q)
113
  | Pck_const (n,p) ->
114
    fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
115
  | Cvar cset ->
116
    fprintf fmt "'_%i%a" ck.cid print_ckset cset
117
  | Cunivar cset ->
118
    fprintf fmt "'%i%a" ck.cid print_ckset cset
96
  | Cvar -> fprintf fmt "'_%i" ck.cid 
97
  | Cunivar -> fprintf fmt "'%i" ck.cid 
119 98
  | Clink ck' ->
120 99
    fprintf fmt "link %a" print_ck_long ck'
121 100
  | Ccarrying (cr,ck') ->
......
129 108
let new_ck desc scoped =
130 109
  incr new_id; {cdesc=desc; cid = !new_id; cscoped = scoped}
131 110

  
132
let new_var scoped =
133
  new_ck (Cvar CSet_all) scoped
111
let new_var scoped = new_ck Cvar scoped
134 112

  
135
let new_univar () =
136
  new_ck (Cunivar CSet_all) false
113
let new_univar () = new_ck Cunivar false
137 114

  
138 115
let new_carrier_id = ref (-1)
139 116

  
......
187 164

  
188 165
(* Removes all links in a clock. Only used for clocks
189 166
   simplification though. *)
190
let rec deep_repr ck =
167
let rec simplify ck =
191 168
  match ck.cdesc with
192 169
  | Carrow (ck1,ck2) ->
193
      new_ck (Carrow (deep_repr ck1, deep_repr ck2)) ck.cscoped
170
      new_ck (Carrow (simplify ck1, simplify ck2)) ck.cscoped
194 171
  | Ctuple cl ->
195
      new_ck (Ctuple (List.map deep_repr cl)) ck.cscoped
172
      new_ck (Ctuple (List.map simplify cl)) ck.cscoped
196 173
  | Con (ck', c, l) ->
197
      new_ck (Con (deep_repr ck', c, l)) ck.cscoped
198
  | Pck_up (ck',k) ->
199
      new_ck (Pck_up (deep_repr ck',k)) ck.cscoped
200
  | Pck_down (ck',k) ->
201
      new_ck (Pck_down (deep_repr ck',k)) ck.cscoped
202
  | Pck_phase (ck',q) ->
203
      new_ck (Pck_phase (deep_repr ck',q)) ck.cscoped
204
  | Pck_const (_,_) | Cvar _ | Cunivar _ -> ck
205
  | Clink ck' -> deep_repr ck'
206
  | Ccarrying (cr,ck') -> new_ck (Ccarrying (cr, deep_repr ck')) ck.cscoped
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
207 178

  
208 179
(** Splits ck into the [lhs,rhs] of an arrow clock. Expects an arrow clock
209 180
    (ensured by language syntax) *)
......
233 204
let clock_of_impnode_clock ck =
234 205
  let ck = repr ck in
235 206
  match ck.cdesc with
236
  | Carrow _ | Clink _ | Cvar _ | Cunivar _ ->
207
  | Carrow _ | Clink _ | Cvar | Cunivar ->
237 208
      failwith "internal error clock_of_impnode_clock"
238 209
  | Ctuple cklist -> List.hd cklist
239
  | Con (_,_,_) | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_)
240
  | Pck_const (_,_) | Ccarrying (_,_) -> ck
241

  
242
(** [intersect set1 set2] returns the intersection of clock subsets
243
    [set1] and [set2]. *)
244
let intersect set1 set2 =
245
  match set1,set2 with
246
  | CSet_all,_ -> set2
247
  | _,CSet_all -> set1
248
  | CSet_pck (k,q), CSet_pck (k',q') ->
249
      let k'',q'' = lcm k k',max_rat q q' in
250
      CSet_pck (k'',q'')
251

  
252
(** [can_be_pck ck] returns true if [ck] "may be" a pclock (the uncertainty is
253
    due to clock variables) *)
254
let rec can_be_pck ck =
255
  match (repr ck).cdesc with
256
  | Pck_up (_,_) | Pck_down (_,_) | Pck_phase (_,_) | Pck_const (_,_)
257
  | Cvar _ | Cunivar _ ->
258
      true
259
  | Ccarrying (_,ck') -> can_be_pck ck
260
  | _ -> false
261

  
262
(** [is_concrete_pck ck] returns true if [ck] is a concrete [pck] (pck
263
    transformations applied to a pck constant) *)
264
let rec is_concrete_pck ck =
265
  match ck.cdesc with
266
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
267
  | Cvar _ | Cunivar _ -> false
268
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_concrete_pck ck'
269
  | Pck_phase (ck',_) -> is_concrete_pck ck'
270
  | Pck_const (_,_) -> true
271
  | Clink ck' -> is_concrete_pck ck'
272
  | Ccarrying (_,ck') -> false
210
  | Con (_,_,_) 
211
  | Ccarrying (_,_) -> ck
212

  
273 213

  
274 214
(** [is_polymorphic ck] returns true if [ck] is polymorphic. *)
275 215
let rec is_polymorphic ck =
276 216
  match ck.cdesc with
277
  | Cvar _ | Pck_const (_,_) -> false
217
  | Cvar -> false
278 218
  | Carrow (ck1,ck2) -> (is_polymorphic ck1) || (is_polymorphic ck2)
279 219
  | Ctuple ckl -> List.exists (fun c -> is_polymorphic c) ckl
280 220
  | Con (ck',_,_) -> is_polymorphic ck'
281
  | Pck_up (ck',_) | Pck_down (ck',_) -> is_polymorphic ck'
282
  | Pck_phase (ck',_) -> is_polymorphic ck'
283
  | Cunivar _ -> true
221
  | Cunivar  -> true
284 222
  | Clink ck' -> is_polymorphic ck'
285 223
  | Ccarrying (_,ck') -> is_polymorphic ck'
286 224

  
......
290 228
let rec constrained_vars_of_clock ck =
291 229
  let rec aux vars ck =
292 230
    match ck.cdesc with
293
    | Pck_const (_,_) ->
294
        vars
295
    | Cvar cset ->
296
        begin
297
          match cset with
298
          | CSet_all -> vars
299
          | _ ->
300
              list_union [ck] vars
301
        end
231
    | Cvar -> vars
302 232
    | Carrow (ck1,ck2) ->
303 233
        let l = aux vars ck1 in
304 234
        aux l ck2
......
307 237
          (fun acc ck' -> aux acc ck') 
308 238
          vars ckl
309 239
    | Con (ck',_,_) -> aux vars ck'
310
    | Pck_up (ck',_) | Pck_down (ck',_) -> aux vars ck'
311
    | Pck_phase (ck',_) -> aux vars ck'
312
    | Cunivar cset ->
313
        begin
314
          match cset with
315
          | CSet_all -> vars
316
          | _ -> list_union [ck] vars
317
        end
240
    | Cunivar -> vars
318 241
    | Clink ck' -> aux vars ck'
319 242
    | Ccarrying (_,ck') -> aux vars ck'
320 243
  in
321 244
  aux [] ck
322 245

  
323
(** [period ck] returns the period of [ck]. Expects a constant pclock
324
    expression belonging to the correct clock set. *)
325
let rec period ck =
326
  let rec aux ck =
327
    match ck.cdesc with
328
    | Carrow (_,_) | Ctuple _ | Con (_,_,_)
329
    | Cvar _ | Cunivar _ ->
330
        failwith "internal error: can only compute period of const pck"
331
    | Pck_up (ck',k) ->
332
        (aux ck')/.(float_of_int k)
333
    | Pck_down (ck',k) ->
334
        (float_of_int k)*.(aux ck')
335
    | Pck_phase (ck',_) ->
336
        aux ck'
337
    | Pck_const (n,_) ->
338
        float_of_int n
339
    | Clink ck' -> aux ck'
340
    | Ccarrying (_,ck') -> aux ck'
341
  in
342
  int_of_float (aux ck)
343

  
344
(** [phase ck] returns the phase of [ck]. It is not expressed as a
345
    fraction of the period, but instead as an amount of time. Expects a
346
    constant expression belonging to the correct P_k *)
347
let phase ck =
348
  let rec aux ck =
349
  match ck.cdesc with
350
  | Carrow (_,_) | Ctuple _ | Con (_,_,_)
351
  | Cvar _ | Cunivar _ ->
352
      failwith "internal error: can only compute phase of const pck"
353
  | Pck_up (ck',_) ->
354
      aux ck'
355
  | Pck_down (ck',k) ->
356
      aux ck'
357
  | Pck_phase (ck',(a,b)) ->
358
      let n = period ck' in
359
      let (a',b') = aux ck' in
360
      sum_rat (a',b') (n*a,b)
361
  | Pck_const (n,(a,b)) ->
362
      (n*a,b)
363
  | Clink ck' -> aux ck'
364
  | Ccarrying (_,ck') -> aux ck'
365
  in
366
  let (a,b) = aux ck in
367
  simplify_rat (a,b)
368

  
369 246
let eq_carrier cr1 cr2 =
370 247
  match (carrier_repr cr1).carrier_desc, (carrier_repr cr2).carrier_desc with
371 248
 | Carry_const id1, Carry_const id2 -> id1 = id2
......
380 257
  match ck.cdesc with
381 258
  | Ctuple (ck'::_)
382 259
  | Con (ck',_,_) | Clink ck' | Ccarrying (_,ck') -> root ck'
383
  | Pck_up _ | Pck_down _ | Pck_phase _ | Pck_const _ | Cvar _ | Cunivar _ -> ck
260
  | Cvar | Cunivar -> ck
384 261
  | Carrow _ | Ctuple _ -> failwith "Internal error root"
385 262

  
386 263
(* Returns the branch of clock [ck] in its clock tree *)
......
419 296
let disjoint ck1 ck2 =
420 297
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
421 298

  
422
(** [normalize pck] returns the normal form of clock [pck]. *)
423
let normalize pck =
424
  let changed = ref true in
425
  let rec aux pck =
426
    match pck.cdesc with
427
    | Pck_up ({cdesc=Pck_up (pck',k')},k) ->
428
        changed:=true;
429
        new_ck (Pck_up (aux pck',k*k')) pck.cscoped
430
    | Pck_up ({cdesc=Pck_down (pck',k')},k) ->
431
        changed:=true;
432
        new_ck (Pck_down (new_ck (Pck_up (aux pck',k)) pck.cscoped,k')) pck.cscoped
433
    | Pck_up ({cdesc=Pck_phase (pck',(a,b))},k) ->
434
        changed:=true;
435
        new_ck (Pck_phase (new_ck (Pck_up (aux pck',k)) pck.cscoped,(a*k,b))) pck.cscoped
436
    | Pck_down ({cdesc=Pck_down (pck',k')},k) ->
437
        changed:=true;
438
        new_ck (Pck_down (aux pck',k*k')) pck.cscoped
439
    | Pck_down ({cdesc=Pck_phase (pck',(a,b))},k) ->
440
        changed:=true;
441
        new_ck (Pck_phase (new_ck (Pck_down (aux pck',k)) pck.cscoped,(a,b*k))) pck.cscoped
442
    | Pck_phase ({cdesc=Pck_phase (pck',(a',b'))},(a,b)) ->
443
        changed:=true;
444
        let (a'',b'') = sum_rat (a,b) (a',b') in
445
        new_ck (Pck_phase (aux pck',(a'',b''))) pck.cscoped
446
    | Pck_up (pck',k') ->
447
        new_ck (Pck_up (aux pck',k')) pck.cscoped
448
    | Pck_down (pck',k') ->
449
        new_ck (Pck_down (aux pck',k')) pck.cscoped
450
    | Pck_phase (pck',k') ->
451
        new_ck (Pck_phase (aux pck',k')) pck.cscoped
452
    | Ccarrying (cr,ck') ->
453
        new_ck (Ccarrying (cr, aux ck')) pck.cscoped
454
    | _ -> pck
455
  in
456
  let nf=ref pck in
457
  while !changed do
458
    changed:=false;
459
    nf:=aux !nf
460
  done;
461
  !nf
462

  
463
(** [canonize pck] reduces transformations of [pck] and removes
464
    identity transformations. Expects a normalized periodic clock ! *)
465
let canonize pck =
466
  let rec remove_id_trans pck =
467
    match pck.cdesc with
468
    | Pck_up (pck',1) | Pck_down (pck',1) | Pck_phase (pck',(0,_)) ->
469
        remove_id_trans pck'
470
    | _ -> pck
471
  in
472
  let pck =
473
    match pck.cdesc with
474
    | Pck_phase ({cdesc=Pck_down ({cdesc=Pck_up (v,k)},k')},k'') ->
475
        let gcd = gcd k k' in
476
        new_ck (Pck_phase
477
                  (new_ck (Pck_down
478
                             (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd))
479
                     pck.cscoped,k''))
480
          pck.cscoped
481
    | Pck_down ({cdesc=Pck_up (v,k)},k') ->
482
        let gcd = gcd k k' in
483
        new_ck (Pck_down (new_ck (Pck_up (v,k/gcd)) pck.cscoped,k'/gcd)) pck.cscoped
484
    | _ -> pck
485
  in
486
  remove_id_trans pck
487

  
488
(** [simplify pck] applies pclocks simplifications to [pck] *)
489
let simplify pck =
490
  if (is_concrete_pck pck) then
491
    let n = period pck in
492
    let (a,b) = phase pck in
493
    let phase' = simplify_rat (a,b*n) in 
494
    new_ck (Pck_const (n,phase')) pck.cscoped
495
  else
496
    let pck' = deep_repr pck in
497
    let nf_pck = normalize pck' in
498
    canonize nf_pck
499
        
500 299
let print_cvar fmt cvar =
501 300
  match cvar.cdesc with
502
  | Cvar cset ->
301
  | Cvar ->
503 302
 (*
504 303
      if cvar.cscoped
505 304
      then
506
	fprintf fmt "[_%s%a]"
305
	fprintf fmt "[_%s]"
507 306
	  (name_of_type cvar.cid)
508
	  print_ckset cset
509 307
      else
510 308
 *)
511
	fprintf fmt "_%s%a"
309
	fprintf fmt "_%s"
512 310
	  (name_of_type cvar.cid)
513
	  print_ckset cset
514
  | Cunivar cset ->
311
  | Cunivar ->
515 312
 (*
516 313
      if cvar.cscoped
517 314
      then
518
	fprintf fmt "['%s%a]"
315
	fprintf fmt "['%s]"
519 316
	  (name_of_type cvar.cid)
520
	  print_ckset cset
521 317
      else
522 318
 *)
523
	fprintf fmt "'%s%a"
319
	fprintf fmt "'%s"
524 320
	  (name_of_type cvar.cid)
525
	  print_ckset cset
526 321
  | _ -> failwith "Internal error print_cvar"
527 322

  
528 323
(* Nice pretty-printing. Simplifies expressions before printing them. Non-linear
529 324
   complexity. *)
530 325
let print_ck fmt ck =
531 326
  let rec aux fmt ck =
532
    let ck = simplify ck in
533 327
    match ck.cdesc with
534 328
    | Carrow (ck1,ck2) ->
535 329
      fprintf fmt "%a -> %a" aux ck1 aux ck2
......
538 332
	(fprintf_list ~sep:" * " aux) cklist
539 333
    | Con (ck,c,l) ->
540 334
      fprintf fmt "%a on %s(%a)" aux ck l print_carrier c
541
    | Pck_up (ck,k) ->
542
      fprintf fmt "%a*.%i" aux ck k
543
    | Pck_down (ck,k) ->
544
      fprintf fmt "%a/.%i" aux ck k
545
    | Pck_phase (ck,q) ->
546
      fprintf fmt "%a->.%a" aux ck print_rat (simplify_rat q)
547
    | Pck_const (n,p) ->
548
      fprintf fmt "(%i,%a)" n print_rat (simplify_rat p)
549
    | Cvar cset ->
335
    | Cvar ->
550 336
(*
551 337
      if ck.cscoped
552 338
      then
......
554 340
      else
555 341
*)
556 342
	fprintf fmt "_%s" (name_of_type ck.cid)
557
    | Cunivar cset ->
343
    | Cunivar ->
558 344
(*
559 345
      if ck.cscoped
560 346
      then
......
575 361

  
576 362
(* prints only the Con components of a clock, useful for printing nodes *)
577 363
let rec print_ck_suffix fmt ck =
578
  let ck = simplify ck in
579 364
  match ck.cdesc with
580 365
  | Carrow _
581 366
  | Ctuple _
582
  | Cvar _
583
  | Cunivar _   -> ()
367
  | Cvar 
368
  | Cunivar    -> ()
584 369
  | Con (ck,c,l) ->
585 370
    fprintf fmt "%a when %s(%a)" print_ck_suffix ck l print_carrier c
586 371
  | Clink ck' ->
587 372
    print_ck_suffix fmt ck'
588 373
  | Ccarrying (cr,ck') ->
589 374
    fprintf fmt "%a" print_ck_suffix ck'
590
  | _ -> assert false
375

  
591 376

  
592 377
let pp_error fmt = function
593 378
  | Clock_clash (ck1,ck2) ->
......
595 380
      fprintf fmt "Expected clock %a, got clock %a@."
596 381
      print_ck ck1
597 382
      print_ck ck2
598
  | Not_pck ->
599
    fprintf fmt "The clock of this expression must be periodic@."
600 383
  | Carrier_mismatch (cr1, cr2) ->
601 384
     fprintf fmt "Name clash. Expected clock %a, got clock %a@."
602 385
       print_carrier cr1
603 386
       print_carrier cr2
604
  | Clock_set_mismatch (ck,cset) ->
605
      reset_names ();
606
    fprintf fmt "Clock %a is not included in clock set %a@."
607
      print_ck ck
608
      print_ckset cset
609 387
  | Cannot_be_polymorphic ck ->
610 388
      reset_names ();
611 389
    fprintf fmt "The main node cannot have a polymorphic clock: %a@."
......
630 408
      print_ck ck
631 409

  
632 410
let const_of_carrier cr =
633
 match (carrier_repr cr).carrier_desc with
634
 | Carry_const id -> id
635
 | Carry_name
636
 | Carry_var
637
 | Carry_link _ -> (Format.eprintf "internal error: const_of_carrier %a@." print_carrier cr; assert false) (* TODO check this Xavier *)
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 *)
638 416
 
639 417
let uneval const cr =
640 418
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)

Also available in: Unified diff