Project

General

Profile

Revision 3b2bd83d 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') ->
......
123 102

  
124 103
let new_id = ref (-1)
125 104

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

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

  
129
let new_var scoped =
130
  new_ck (Cvar CSet_all) scoped
111
let new_var scoped = new_ck Cvar scoped
131 112

  
132
let new_univar () =
133
  new_ck (Cunivar CSet_all) false
113
let new_univar () = new_ck Cunivar false
134 114

  
135 115
let new_carrier_id = ref (-1)
136 116

  
......
184 164

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

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

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

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

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

  
270 213

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

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

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

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

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

  
383 263
(* Returns the branch of clock [ck] in its clock tree *)
......
416 296
let disjoint ck1 ck2 =
417 297
  eq_clock (root ck1) (root ck2) && disjoint_branches (branch ck1) (branch ck2)
418 298

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

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

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

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

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

  
588 376

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

  
629 410
let const_of_carrier cr =
630
 match (carrier_repr cr).carrier_desc with
631
 | Carry_const id -> id
632
 | Carry_name
633
 | Carry_var
634
 | 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 *)
635 416
 
636 417
let uneval const cr =
637 418
  (*Format.printf "Clocks.uneval %s %a@." const print_carrier cr;*)

Also available in: Unified diff