Revision 45f0f48d
Added by Xavier Thirioux almost 6 years ago
| 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
...