Commit e2548aaa by Kim Nguyễn

### Further improve the pretty printing and add some test cases in part2.cd

parent 3b42bafb
 ... @@ -42,6 +42,8 @@ let balance ( Unbal ->Rtree ; ('b \ Unbal) ->('b \ Unbal) ) ... @@ -42,6 +42,8 @@ let balance ( Unbal ->Rtree ; ('b \ Unbal) ->('b \ Unbal) ) | x -> x | x -> x ;; ;; let f (_ : ('a | 'b | 'c)) (_ : (Int&'d&'e \1--3 )) : Any = raise "123";; let balance (Unbal ->Rtree ; 'a -> 'a ) let balance (Unbal ->Rtree ; 'a -> 'a ) | [ [ [ a b ] c ] d ] | [ [ [ a b ] c ] d ] | [ [ a [ b c ] ] d ] | [ [ a [ b c ] ] d ] ... ...
 ... @@ -1691,6 +1691,28 @@ struct ... @@ -1691,6 +1691,28 @@ struct | Neg of nd | Neg of nd | Abs of nd | Abs of nd module Key = struct type t = Var.Set.t * Var.Set.t let hash (x, y) = Var.Set.hash x + 17 * Var.Set.hash y let equal ((a,b) as x) ((c,d) as y) = x == y || Var.Set.(equal a c && equal b d) let compare (a, b) (c, d) = let r = Var.Set.compare a c in if r == 0 then Var.Set.compare b d else r end module VarTable = Hashtbl.Make(Key) module KeySet = Set.Make(Key) type matrix = { mchars : BoolChars.t VarTable.t; mints : BoolIntervals.t VarTable.t; matoms : BoolAtoms.t VarTable.t; mtimes : BoolPair.t VarTable.t; mxml : BoolPair.t VarTable.t; marrow : BoolPair.t VarTable.t; mrecord : BoolRec.t VarTable.t; mabstract : BoolAbstracts.t VarTable.t; } let compare x y = x.id - y.id let compare x y = x.id - y.id module S = struct module S = struct ... @@ -1808,250 +1830,230 @@ struct ... @@ -1808,250 +1830,230 @@ struct tlv : intersection of toplevel variables that are common to all non empty kinds tlv : intersection of toplevel variables that are common to all non empty kinds tv : the rest of the type tv : the rest of the type *) *) let split_vars (type s) (module BV : BoolVar.S with type t = s) bdd = List.fold_left (fun (acc_v, acc_nv) (p, n) -> (* Given a bdd match p, n with \/_i (p_i & pvar_i, n_i& nvar_i) (([ `Atm _ ]|[]), ([ `Atm _]| [])) -> we fill a table appropriately where the entries are the (pvar_i,nvar_i) acc_v, BV.cup acc_nv (BV.build [ (p,n)]) and the data the variable-less bdd (p_i \ n_i) | _ -> BV.cup acc_v (BV.build [(p,n)]), acc_nv) (BV.empty,BV.empty) (BV.get bdd) *) in let vchars, nvchars = split_vars (module BoolChars) not_seq.chars in let split_var_atom op init l = let vints, nvints = split_vars (module BoolIntervals) not_seq.ints in List.fold_left (fun (acc_v, acc_a) e -> let vatoms, nvatoms = split_vars (module BoolAtoms) not_seq.atoms in let vtimes, nvtimes = split_vars (module BoolPair) not_seq.times in let vxml, nvxml = split_vars (module BoolPair) not_seq.xml in let varrow, nvarrow = split_vars (module BoolPair) not_seq.arrow in let vrecord, nvrecord = split_vars (module BoolRec) not_seq.record in let vabstract, nvabstract = split_vars (module BoolAbstracts) not_seq.abstract in let not_var = { empty with chars = nvchars; ints = nvints; atoms = nvatoms; times = nvtimes; xml = nvxml; arrow = nvarrow; record = nvrecord; abstract = nvabstract; } in let not_seq = { not_seq with chars = vchars; ints = vints; atoms = vatoms; times = vtimes; xml = vxml; arrow = varrow; record = vrecord; abstract = vabstract; } in let all_vars_in_line l = List.fold_left (fun acc e -> match e with match e with | `Var _ as x -> Var.Set.add x acc `Atm _ -> (acc_v, op e acc_a) | _ -> acc) Var.Set.empty l | `Var _ as x -> (Var.Set.add x acc_v, acc_a) ) (Var.Set.empty, init) l in in let inter s1 s2 = let fill_line (type s) match s1, s2 with (module BV : BoolVar.S with type t = s) (table : s VarTable.t) (bdd : s) = None, None -> None List.iter (fun (p, n) -> | None, Some s | Some s, None -> Some s let v1, a1 = split_var_atom (fun a b -> BV.(cap (atom a) b)) BV.full p in | Some s1, Some s2 -> Some (Var.Set.inter s1 s2) let v2, a2 = split_var_atom (fun a b -> BV.(cup (atom a) b)) BV.empty n in let a = BV.diff a1 a2 in let key = v1, v2 in let new_a = try BV.cup a (VarTable.find table key) with Not_found -> a in VarTable.replace table key new_a) (BV.get bdd); table in in let get_set = function None -> Var.Set.empty | Some s -> s in let not_seq_matrix = let factorize_tlv get bdd acc = { mints = (let h = VarTable.create 17 in fill_line (module BoolIntervals) h not_seq.ints); List.fold_left (fun (p_acc,n_acc) (p,n) -> mchars = (let h = VarTable.create 17 in fill_line (module BoolChars) h not_seq.chars); (inter p_acc (Some (all_vars_in_line p)), matoms = (let h = VarTable.create 17 in fill_line (module BoolAtoms) h not_seq.atoms); inter n_acc (Some (all_vars_in_line n))) mtimes = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.times); ) acc (get bdd) mxml = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.xml); marrow = (let h = VarTable.create 17 in fill_line (module BoolPair) h not_seq.arrow); mrecord = (let h = VarTable.create 17 in fill_line (module BoolRec) h not_seq.record); mabstract = (let h = VarTable.create 17 in fill_line (module BoolAbstracts) h not_seq.abstract); } in in let get_keys table acc = VarTable.fold (fun k _ acc -> let tv_acc = factorize_tlv BoolChars.get not_seq.chars (None, None) in KeySet.add k acc) table acc let tv_acc = factorize_tlv BoolIntervals.get not_seq.ints tv_acc in let tv_acc = factorize_tlv BoolAtoms.get not_seq.atoms tv_acc in let tv_acc = factorize_tlv BoolPair.get not_seq.times tv_acc in let tv_acc = factorize_tlv BoolPair.get not_seq.xml tv_acc in let tv_acc = factorize_tlv BoolPair.get not_seq.arrow tv_acc in let tv_acc = factorize_tlv BoolRec.get not_seq.record tv_acc in let tv_pos, tv_neg = factorize_tlv BoolAbstracts.get not_seq.abstract tv_acc in let tv_pos, tv_neg = get_set tv_pos, get_set tv_neg in let tv_pos, tv_neg = Var.Set.diff tv_pos tv_neg, Var.Set.diff tv_neg tv_pos in let remove_tlv (type s) (module BV : BoolVar.S with type t = s) bdd = let open BV in let inter_tlv pol vset l = List.fold_left (fun acc t -> match t with `Var _ as x when Var.Set.mem x vset -> acc | (`Var _ | `Atm _ ) as x -> cap acc (pol (atom x)) ) full l in in List.fold_left (fun acc (p,n) -> let all_keys = (cup (cap (inter_tlv (fun x -> x) tv_pos p) let m = not_seq_matrix in (inter_tlv (fun x -> diff full x) tv_neg n)) acc) let acc = get_keys m.mints KeySet.empty in ) empty (get bdd) let acc = get_keys m.mchars acc in let acc = get_keys m.matoms acc in let acc = get_keys m.mxml acc in let acc = get_keys m.marrow acc in let acc = get_keys m.mrecord acc in get_keys m.mabstract acc in in let type_tlv = let found_any, all_descrs = diff (Var.Set.fold (fun acc v -> cap acc (var v)) any tv_pos) let m = not_seq_matrix in (Var.Set.fold (fun acc v -> cup acc (var v)) empty tv_neg) let get k m e = try VarTable.find m k with Not_found -> e in let found_any = ref false in let res = KeySet.fold (fun ((v1, v2) as k) acc -> (*Format.eprintf "Processing set: %a, %a@\n%!" Var.Set.pp v1 Var.Set.pp v2; *) if !found_any then acc else if Var.Set.(not (is_empty (inter v1 v2))) then ((*Format.eprintf "Found some variables in common: %a\n@!" Var.Set.pp (Var.Set.inter v1 v2);*) acc) else let tt = { empty with ints = get k m.mints BoolIntervals.empty; chars = get k m.mchars BoolChars.empty; atoms = get k m.matoms BoolAtoms.empty; times = get k m.mtimes BoolPair.empty; xml = get k m.mxml BoolPair.empty; arrow = get k m.marrow BoolPair.empty; record = get k m.mrecord BoolRec.empty; abstract = get k m.mabstract BoolAbstracts.empty; absent = not_seq.absent; } in if is_empty tt then acc else if Var.Set.(is_empty v1 && is_empty v2) && subtype any tt then (found_any := true; acc) else (k, tt) :: acc ) all_keys [] in !found_any, res in in (*Format.eprintf "All descr has size: %i, all_keys has size: %i, found_any=%b@\n%!" (List.length all_descrs) KeySet.(cardinal all_keys) found_any; *) let printed_topvar, not_seq = if found_any then (slot.def <- [Neg (alloc [])];slot) if Var.Set.is_empty tv_pos && Var.Set.is_empty tv_neg then [], not_seq else else let cons constr empty = function let not_seq = cup not_seq (cap not_var type_tlv) in (Var.Set.fold (fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) (Var.Set.fold (fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] tv_neg) tv_pos), { not_seq with chars = remove_tlv (module BoolChars) not_seq.chars; ints = remove_tlv (module BoolIntervals) not_seq.ints; atoms = remove_tlv (module BoolAtoms) not_seq.atoms; times = remove_tlv (module BoolPair) not_seq.times; xml = remove_tlv (module BoolPair) not_seq.xml; arrow = remove_tlv (module BoolPair) not_seq.arrow; record = remove_tlv (module BoolRec) not_seq.record; abstract = remove_tlv (module BoolAbstracts) not_seq.abstract } in let cons constr empty = function [] -> empty [] -> empty | [ t ] -> t | [ t ] -> t | l -> constr (alloc l) | l -> constr (alloc l) in let intersection l = cons (fun x -> Intersection x) (Neg (alloc [])) l in let union l = cons (fun x -> Union x) (Union (alloc [])) l in let prepare_boolvar get print bdd acc = let fold_line acc l = List.fold_left (fun acc t -> match t with | `Var _ as x -> (Atomic (fun ppf -> Var.pp ppf x)) :: acc | `Atm bdd -> (print bdd) @ acc) acc l in List.fold_left (fun acc (p,n) -> let pos_line = fold_line [] p in let neg_line = fold_line [] n in match pos_line, neg_line with [],[] -> acc | [], n -> (Neg (alloc [ (union n) ])) :: acc | p, [] -> (intersection p) :: acc | p, n -> (intersection (p @ (List.map (fun n -> Neg (alloc [ n] )) n))) :: acc ) acc (get bdd) in let printed_seq = if non_empty seq then (Regexp (decompile seq)) :: [] else [] in let print_descr tt = if is_empty tt then [] else let tt, fix = if worth_complement tt then diff any tt, (fun x -> [Neg (alloc x)]) else tt , fun x -> x in in let intersection l = cons (fun x -> Intersection x) (Neg (alloc [])) l in (* base types *) let union l = cons (fun x -> Union x) (Union (alloc [])) l in let u_acc = prepare_boolvar BoolChars.get (fun bdd -> let prepare_boolvar get print bdd acc = match Chars.is_char bdd with let fold_line acc l = List.fold_left (fun acc t -> | Some c -> [Char c] match t with | None -> [Union(alloc (List.map (fun x -> (Atomic x)) (Chars.print bdd)))] | `Var _ as x -> (Atomic (fun ppf -> Var.pp ppf x)) :: acc ) tt.chars [] | `Atm bdd -> (print bdd) @ acc) acc l in List.fold_left (fun acc (p,n) -> let pos_line = fold_line [] p in let neg_line = fold_line [] n in match pos_line, neg_line with [],[] -> acc | [], n -> (Neg (alloc [ (union n) ])) :: acc | p, [] -> (intersection p) :: acc | p, n -> (intersection (p @ (List.map (fun n -> Neg (alloc [ n] )) n))) :: acc ) acc (get bdd) in in let printed_seq = if non_empty seq then (Regexp (decompile seq)) :: [] else [] in let print_descr tv_pos tv_neg tt = if is_empty tt then [] else let printed_topvars = let pneg = Var.Set.fold (fun acc v -> (Neg (alloc [Atomic (fun ppf -> Var.pp ppf v)])) :: acc) [] tv_neg in Var.Set.fold (fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) pneg tv_pos in if subtype any tt then printed_topvars else let tt, fix = if worth_complement tt then diff any tt, (fun x -> [Neg (alloc x)]) else tt , fun x -> x in (* base types *) let u_acc = prepare_boolvar BoolChars.get (fun bdd -> match Chars.is_char bdd with | Some c -> [Char c] | None -> [Union(alloc (List.map (fun x -> (Atomic x)) (Chars.print bdd)))] ) tt.chars [] in let u_acc = prepare_boolvar BoolIntervals.get (fun bdd -> let u_acc = prepare_boolvar BoolIntervals.get (fun bdd -> match Intervals.print bdd with match Intervals.print bdd with |[x] -> [Atomic x] |[x] -> [Atomic x] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] ) tt.ints u_acc ) tt.ints u_acc in in let bool = let bool = Atoms.cup Atoms.cup (Atoms.atom (Atoms.V.mk_ascii "false")) (Atoms.atom (Atoms.V.mk_ascii "false")) (Atoms.atom (Atoms.V.mk_ascii "true")) (Atoms.atom (Atoms.V.mk_ascii "true")) in in let u_acc = prepare_boolvar BoolAtoms.get (fun bdd -> let u_acc = prepare_boolvar BoolAtoms.get (fun bdd -> match Atoms.print bdd with match Atoms.print bdd with |[x] when (Atoms.equal bool bdd) -> |[x] when (Atoms.equal bool bdd) -> [Atomic (fun ppf -> Format.fprintf ppf "Bool")] [Atomic (fun ppf -> Format.fprintf ppf "Bool")] |[x] -> [Atomic x] |[x] -> [Atomic x] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] ) tt.atoms u_acc ) tt.atoms u_acc in in (* pairs *) (* pairs *) let u_acc = prepare_boolvar BoolPair.get (fun x -> let u_acc = prepare_boolvar BoolPair.get (fun x -> List.map (fun (t1,t2) -> List.map (fun (t1,t2) -> Pair (prepare t1, prepare t2) Pair (prepare t1, prepare t2) ) (Product.partition any x) ) (Product.partition any x) ) tt.times u_acc ) tt.times u_acc in in (* xml pairs *) (* xml pairs *) let u_acc = prepare_boolvar BoolPair.get (fun x -> let u_acc = prepare_boolvar BoolPair.get (fun x -> List.flatten ( List.flatten ( List.map (fun (t1,t2) -> List.map (fun (t1,t2) -> try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)] try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)] with Not_found -> with Not_found -> let tag = let tag = match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with | Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a | Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a | _ -> `Type (prepare t1) | _ -> `Type (prepare t1) in in assert (equal { t2 with times = empty.times } empty); assert (equal { t2 with times = empty.times } empty); List.map (fun (ta,tb) -> List.map (fun (ta,tb) -> (Xml (tag, prepare ta, prepare tb)) (Xml (tag, prepare ta, prepare tb)) ) (Product.get t2); ) (Product.get t2); ) (Product.partition any_pair x) ) (Product.partition any_pair x) ) ) ) tt.xml u_acc ) tt.xml u_acc in in (* arrows *) (* arrows *) let u_acc = prepare_boolvar BoolPair.get (fun x -> let u_acc = prepare_boolvar BoolPair.get (fun x -> List.map (fun (p,n) -> List.map (fun (p,n) -> let aux (t,s) = prepare (descr t), prepare (descr s) in let aux (t,s) = prepare (descr t), prepare (descr s) in let p = List.map aux p and n = List.map aux n in let p = List.map aux p and n = List.map aux n in (Arrows (p,n)) (Arrows (p,n)) ) (Pair.get x)) tt.arrow u_acc ) (Pair.get x)) tt.arrow u_acc in in (* records *) (* records *) let u_acc = prepare_boolvar BoolRec.get (fun x -> let u_acc = prepare_boolvar BoolRec.get (fun x -> List.map (fun (r,some,none) -> List.map (fun (r,some,none) -> let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in (Record (r,some,none)) (Record (r,some,none)) ) (Record.get { empty with record = BoolRec.atom (`Atm x) })) tt.record u_acc ) (Record.get { empty with record = BoolRec.atom (`Atm x) })) tt.record u_acc in in let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd -> let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd -> match Abstracts.print bdd with match Abstracts.print bdd with |[x] -> [Atomic x] |[x] -> [Atomic x] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] |l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))] ) tt.abstract u_acc ) tt.abstract u_acc in in let u_acc = let u_acc = if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc else u_acc else u_acc in in fix u_acc let p_t = fix u_acc in in printed_topvars @ p_t let printed = if is_empty not_var then [] else print_descr not_var in in let printed = printed @ printed_seq in let all_printed = if is_empty not_seq then (slot.def <- printed @ slot.def ; slot) List.fold_left (fun acc ((vp,vn),t) -> else match print_descr vp vn t with let printed_not_seq = print_descr not_seq in [] -> acc begin | [p] -> p :: acc match printed_topvar with | l -> (intersection l) :: acc [] -> if subtype any not_seq then slot.def <- (Neg (alloc [])) :: slot.def ) printed_seq all_descrs else slot.def <- printed @ printed_not_seq @ slot.def in | _ -> if subtype any not_seq then slot.def <- ((intersection printed_topvar) :: printed) @ slot.def slot.def <- all_printed @ slot.def; else slot.def <- (intersection ((union printed_not_seq) :: printed_topvar)) :: (printed @ slot.def) end; slot slot and decompile d = and decompile d = let aux t = let aux t = let tr = Product.get t in let tr = Product.get t in ... @@ -2145,7 +2147,7 @@ struct ... @@ -2145,7 +2147,7 @@ struct | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r | Atomic a -> a ppf | Atomic a -> a ppf | Intersection { def = ([ Neg b ; a ] | [ a; Neg b]) } -> | Intersection { def = ([ Neg b ; a ] | [ a; Neg b]) } -> Format.fprintf ppf "@[%a@] \\ (@[%a@])" (do_print pri) a (do_print_slot pri) b Format.fprintf ppf "(@[%a@] \\ (@[%a@]))" (do_print pri) a (do_print_slot pri) b | Intersection { def = [ a ] } | Intersection { def = [ a ] } | Union { def = [ a ] } -> Format.fprintf ppf "@[%a@]" (do_print pri) a | Union { def = [ a ] } -> Format.fprintf ppf "@[%a@]" (do_print pri) a | Intersection a -> Format.fprintf ppf "@[%a@]" (do_print_slot ~sep:"&" 2) a | Intersection a -> Format.fprintf ppf "@[%a@]" (do_print_slot ~sep:"&" 2) a ... ...
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!