Revision 7ecdb0aa src/causality.ml
src/causality.ml  

447  447 
(* Module used to compute static disjunction of variables based upon their clocks. *) 
448  448 
module Disjunction = 
449  449 
struct 
450 
(* map: var > list of disjoint vars, sorted in increasing branch length, 

451 
maybe removing shorter branches *) 

452 
type clock_map = (ident, ident list) Hashtbl.t 

450 
module ClockedIdentModule = 

451 
struct 

452 
type t = var_decl 

453 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock 

454 
let compare v1 v2 = compare (root_branch v2) (root_branch v1) 

455 
end 

456  
457 
module CISet = Set.Make(ClockedIdentModule) 

453  458  
454 
let rec add_vdecl map vdecls = 

455 
match vdecls with 

456 
 [] > () 

457 
 vdecl :: q > begin 

458 
Hashtbl.add map vdecl.var_id (List.fold_left (fun r v > if Clocks.disjoint v.var_clock vdecl.var_clock then v.var_id::r else r) [] q); 

459 
add_vdecl map q 

460 
end 

459 
(* map: var > list of disjoint vars, sorted in increasing branch length order, 

460 
maybe removing shorter branches *) 

461 
type clock_map = (ident, var_decl list) Hashtbl.t 

461  462  
462  463 
let clock_disjoint_map vdecls = 
463 
let root_branch vdecl = Clocks.root vdecl.var_clock, Clocks.branch vdecl.var_clock in 

464  464 
let map = Hashtbl.create 23 in 
465  465 
begin 
466 
add_vdecl map (List.sort (fun v1 v2 > compare (root_branch v1) (root_branch v2)) vdecls); 

466 
List.iter 

467 
(fun v1 > let disj_v1 = 

468 
List.fold_left 

469 
(fun res v2 > if Clocks.disjoint v1.var_clock v2.var_clock then CISet.add v2 res else res) 

470 
CISet.empty 

471 
vdecls in 

472 
(* disjoint vdecls are stored in increasing branch length order *) 

473 
Hashtbl.add map v1.var_id disj_v1) 

474 
vdecls; 

467  475 
map 
468  476 
end 
469  477  
478 
(* replace variable [v] by [v'] in disjunction [map]. Then: 

479 
 the mapping v > ... disappears 

480 
 the mapping v' becomes v' > (map v) inter (map v') 

481 
 other mappings become x > (map x) \ (if v in x then v else v') 

482 
*) 

483 
let replace_in_disjoint_map map v v' = 

484 
begin 

485 
Hashtbl.remove map v.var_id; 

486 
Hashtbl.replace map v'.var_id (CISet.inter (Hashtbl.find map v.var_id) (Hashtbl.find map v'.var_id)); 

487 
Hashtbl.iter (fun x map_x > Hashtbl.replace map x (CISet.remove (if CISet.mem v map_x then v else v') map_x)) map; 

488 
end 

489  
470  490 
let pp_disjoint_map fmt map = 
471  491 
begin 
472  492 
Format.fprintf fmt "{ /* disjoint map */@."; 
473 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Format.pp_print_string) v) map;


493 
Hashtbl.iter (fun k v > Format.fprintf fmt "%s # { %a }@." k (Utils.fprintf_list ~sep:", " Printers.pp_var_name) (CISet.elements v)) map;


474  494 
Format.fprintf fmt "}@." 
475  495 
end 
476  496 
end 
Also available in: Unified diff