000001| (** Abstract datatype and operations for (nested local) environments *)
000002|
000003| module PairSet = Set.Make(struct type t = int * (int list)
000004| let compare = (*[1]*)Pervasives.compare end)
000005|
000006| type elem = PairSet.t
000007|
000008| (* eq : elem -> elem -> bool *)
000009| let eq = (*[1]*)PairSet.equal
000010|
000011| (* leq : elem -> elem -> bool *)
000012| let leq env0 env1 = (*[13686]*)PairSet.subset env0 env1
000013|
000014| (* join : elem -> elem -> elem *)
000015| let join env0 env1 = (*[61142]*)PairSet.union env0 env1
000016|
000017| (* meet : elem -> elem -> elem *)
000019|
000020| (* bot : elem *)
000021| let bot = (*[1]*)PairSet.empty
000022|
000023|
000024| (** {3 Lattice operations } *)
000025|
000026| (* is_bot : EL -> bool *)
000027| let is_bot env = (*[8219]*)leq env bot
000028|
000029| (* init : label -> label -> elem *)
000030| let init lenvlab genvlab = (*[1]*)PairSet.add (lenvlab,[genvlab]) bot
000031|
000032| (* fold : ((int * int list) -> 'a -> 'a) -> elem -> 'a -> 'a *)
000033| let fold = (*[1]*)PairSet.fold
000034|
000035| (* enter_scope : EL -> label -> EL *)
000036| let enter_scope env lab =
000037| (*[671]*)fold (fun (envlab,scopechain) envpairs -> (*[749]*)PairSet.add (lab,envlab::scopechain) envpairs)
000038| env PairSet.empty
000039|
000040|
000041| (** {3 Pretty printing routines } *)
000042|
000043| (* pprint : EL -> unit *)
000044| let pprint elat =
000045| (* pprint_list : int list -> unit *)
000046| let pprint_list is =
000047| begin
000048| Format.printf "[@[<h 1>";
000049| ignore (List.fold_left (fun first i ->
000050| if first
000051| then (Format.print_int i; false)
000052| else
000053| begin
000054| Format.printf ",";
000055| Format.print_space ();
000056| Format.print_int i;
000057| false
000058| end) true is);
000059| Format.printf "@]]";
000060| end in
000061| (* pprint_pair : int * int list -> unit *)
000062| let pprint_pair (i,is) =
000063| begin
000064| Format.printf "(%i," i;
000065| pprint_list is;
000066| Format.printf ")"
000067| end in
000068| begin
000069| Format.printf "{ @[<h 1>";
000070| ignore (fold (fun p first ->
000071| if first
000072| then (pprint_pair p; false)
000073| else
000074| begin
000075| Format.printf ",";
000076| Format.print_space ();
000077| pprint_pair p;
000078| false
000079| end) elat true);
000080| Format.printf "@] }";
000081| end
000082|
000083| (* to_string : elem -> string *)
000084| let to_string el =
000085| let buf = Buffer.create 64 in
000086| let out,flush = Format.get_formatter_output_functions () in (* save previous outputters *)
000087| begin
000088| Format.set_formatter_output_functions (Buffer.add_substring buf) (fun () -> ());
000089| pprint el;
000090| Format.print_flush ();
000091| Format.set_formatter_output_functions out flush; (* restore previous outputters *)
000092| Buffer.contents buf
000093| end
000018| let meet env0 env1 = (*[0]*)PairSet.inter env0 env1