Commit ae786716 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Preliminary work on pretty-printing of types. Try to split a type as a union

of sequence|non_variable|(toplevelvar ^ rest)
with special cases when non_variable or sequence are empty and toplevelvar or rest are any
(or any combination of thoses).

Add the examples of the part2 paper in a test file.
parent 7f7b54c8
let pretty (x : Int) : String = string_of x;;
let even (Int -> Bool; ('a\Int) -> ('a\Int))
| x & Int -> (x mod 2) = 0
| x -> x
;;
let mmap (f : 'a -> 'b) (l : [ ('a) *] ) : [ ('b) *] =
match l with
[] -> []
| (e, ll) -> (f e, mmap f ll)
;;
let map_even = mmap even
;;
let g ( (Int -> Int) -> Int -> Int;
(Bool -> Bool) -> Bool -> Bool) x -> x
;;
let id ('a -> 'a) x -> x;;
let gid = g id;;
let id2g = id (id g);;
let churchtrue (x : 'a) (y : 'b) : 'a = x in churchtrue 42;;
let max (x : 'a) (y : 'a) : 'a = if x >> y then x else y;;
max 42;;
type RBtree = Btree | Rtree
type Btree = <blk elem='a>[ RBtree RBtree ] | []
type Rtree = <red elem='a>[ Btree Btree ]
type Unbal = <blk elem='a>( [ Wrong RBtree ]
| [ RBtree Wrong ])
type Wrong = <red elem='a>( [ Rtree Btree ]
| [ Btree Rtree ])
let balance ( Unbal ->Rtree ; ('b \ Unbal) ->('b \ Unbal) )
| <blk (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
| <blk (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
| <blk (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
| <blk (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ]
-> <red (y)>[ <blk (x)>[ a b ] <blk (z)>[ c d ] ]
| x -> x
;;
......@@ -1801,133 +1801,244 @@ struct
(empty, d)
in
let add u = slot.def <- u :: slot.def in
(*
alpha ^ ( union )
alpha / ( union ) only if alpha is not present in at most 2
We split the non_sequence type as follows to have a better display :
t = t_nv | (tlv^ tv)
t_nv : part of the types without any variables
tlv : intersection of toplevel variables that are common to all non empty kinds
tv : the rest of the type
*)
let if_no_var (type s) (module BV : BoolVar.S with type t = s) bdd =
try
BV.iter (function `Var _ -> raise Not_found | _ -> ()) bdd;
bdd
with
_ -> BV.empty
in
let if_eq empty t1 t2 = if t1 == t2 then empty else t2 in
let not_var = { empty with
chars = if_no_var (module BoolChars) not_seq.chars;
ints = if_no_var (module BoolIntervals) not_seq.ints;
atoms = if_no_var (module BoolAtoms) not_seq.atoms;
times = if_no_var (module BoolPair) not_seq.times;
xml = if_no_var (module BoolPair) not_seq.xml;
arrow = if_no_var (module BoolPair) not_seq.arrow;
record = if_no_var (module BoolRec) not_seq.record;
abstract = if_no_var (module BoolAbstracts) not_seq.abstract
}
in
let not_seq = { not_seq with
chars = if_eq BoolChars.empty not_var.chars not_seq.chars;
ints = if_eq BoolIntervals.empty not_var.ints not_seq.ints;
atoms = if_eq BoolAtoms.empty not_var.atoms not_seq.atoms;
times = if_eq BoolPair.empty not_var.times not_seq.times;
xml = if_eq BoolPair.empty not_var.xml not_seq.xml;
arrow = if_eq BoolPair.empty not_var.arrow not_seq.arrow;
record = if_eq BoolRec.empty not_var.record not_seq.record;
abstract = if_eq BoolAbstracts.empty not_var.abstract not_seq.abstract;
}
in
let all_vars_in_line l =
List.fold_left (fun acc e ->
match e with
| `Var _ as x -> Var.Set.add x acc
| _ -> acc) Var.Set.empty l
in
let inter s1 s2 =
match s1, s2 with
None, None -> None
| None, Some s | Some s, None -> Some s
| Some s1, Some s2 -> Some (Var.Set.inter s1 s2)
in
let get_set = function None -> Var.Set.empty | Some s -> s in
let factorize_tlv get bdd acc =
List.fold_left (fun (p_acc,n_acc) (p,n) ->
(inter p_acc (Some (all_vars_in_line p)),
inter n_acc (Some (all_vars_in_line n)))
) acc (get bdd)
in
let prepare_boolvar get is_full print tlv bdd =
let ll =
List.fold_left (fun acc (p,n) ->
let (_,l1) =
List.fold_left (fun (has_tlv,acc) -> function
|(`Var v) (* as x when (TLV.mem (x,true) tlv) *) -> (true,acc)
(* |(`Var v) as x -> (has_tlv,(Atomic (fun ppf -> Var.pp ppf x))::acc) *)
|`Atm bdd ->
begin match has_tlv,acc with
|true,[] -> if is_full bdd then (has_tlv,[]) else (has_tlv,print bdd)
|false,[] -> (has_tlv,print bdd)
|_,_ -> (has_tlv,acc @ (print bdd))
end
) (false,[]) p
in
let l2 =
List.fold_left (fun acc -> function
|(`Var v) (* as x when (TLV.mem (x,false) tlv) *) -> acc
(* |(`Var v) as x -> (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.pp x))::acc *)
|`Atm bdd -> assert false
) [] n
in
match (l1@l2) with
|[] -> acc
|l -> l::acc
) [] (get bdd)
let tv_acc = factorize_tlv BoolChars.get not_seq.chars (None, None) in
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
List.iter (fun l -> add (Intersection (alloc (List.rev l)))) ll
List.fold_left (fun acc (p,n) ->
(cup (cap (inter_tlv (fun x -> x) tv_pos p)
(inter_tlv (fun x -> diff full x) tv_neg n)) acc)
) empty (get bdd)
in
let printed_topvar, not_seq =
if Var.Set.is_empty tv_pos && Var.Set.is_empty tv_neg then [], not_seq
else
(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
if (non_empty seq) then add (Regexp (decompile seq));
if has_tlv not_seq then begin
let l =
TLV.Set.fold (fun ((`Var v) as x,p) acc ->
let s =
if p then (Atomic (fun ppf -> Var.pp ppf x))
else (Atomic (fun ppf -> Format.fprintf ppf "~ %a" Var.pp x))
in s::acc
) (all_tlv not_seq) []
let cons constr empty = function
[] -> empty
| [ t ] -> t
| 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
add (Intersection (alloc l))
end;
(* base types *)
prepare_boolvar BoolChars.get (Chars.equal Chars.full) (fun bdd ->
match Chars.is_char bdd with
| Some c -> [Char c]
| None -> [Union(alloc (List.map (fun x -> (Atomic x)) (Chars.print bdd)))]
) not_seq.toplvars not_seq.chars;
prepare_boolvar BoolIntervals.get (Intervals.equal Intervals.full) (fun bdd ->
match Intervals.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) not_seq.toplvars not_seq.ints;
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
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
prepare_boolvar BoolAtoms.get (Atoms.equal Atoms.full) (fun bdd ->
match Atoms.print bdd with
|[x] when (Atoms.equal bool bdd) ->
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) not_seq.toplvars not_seq.atoms;
(* pairs *)
prepare_boolvar BoolPair.get (Pair.equal Pair.full) (fun x ->
List.map (fun (t1,t2) ->
Pair (prepare t1, prepare t2)
) (Product.partition any x)
) not_seq.toplvars not_seq.times;
(* xml pairs *)
prepare_boolvar BoolPair.get (Pair.equal Pair.full) (fun x ->
List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found ->
let tag =
match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
| Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
| _ -> `Type (prepare t1)
in
assert (equal { t2 with times = empty.times } empty);
List.map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)
) not_seq.toplvars not_seq.xml;
(* arrows *)
prepare_boolvar BoolPair.get (Pair.equal Pair.full) (fun x ->
List.map (fun (p,n) ->
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
(Arrows (p,n))
) (Pair.get x)) not_seq.toplvars not_seq.arrow;
(* records *)
prepare_boolvar BoolRec.get (Rec.equal Rec.full) (fun x ->
List.map (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) not_seq.toplvars not_seq.record;
prepare_boolvar BoolAbstracts.get (Abstracts.equal Abstracts.full) (fun bdd ->
match Abstracts.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) not_seq.toplvars not_seq.abstract;
if not_seq.absent then add (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT"));
slot.def <- List.rev slot.def;
slot
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
(* 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 ->
match Intervals.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) tt.ints u_acc
in
let bool =
Atoms.cup
(Atoms.atom (Atoms.V.mk_ascii "false"))
(Atoms.atom (Atoms.V.mk_ascii "true"))
in
let u_acc = prepare_boolvar BoolAtoms.get (fun bdd ->
match Atoms.print bdd with
|[x] when (Atoms.equal bool bdd) ->
[Atomic (fun ppf -> Format.fprintf ppf "Bool")]
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) tt.atoms u_acc
in
(* pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.map (fun (t1,t2) ->
Pair (prepare t1, prepare t2)
) (Product.partition any x)
) tt.times u_acc
in
(* xml pairs *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.flatten (
List.map (fun (t1,t2) ->
try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
with Not_found ->
let tag =
match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
| Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
| _ -> `Type (prepare t1)
in
assert (equal { t2 with times = empty.times } empty);
List.map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair x)
)
) tt.xml u_acc
in
(* arrows *)
let u_acc = prepare_boolvar BoolPair.get (fun x ->
List.map (fun (p,n) ->
let aux (t,s) = prepare (descr t), prepare (descr s) in
let p = List.map aux p and n = List.map aux n in
(Arrows (p,n))
) (Pair.get x)) tt.arrow u_acc
in
(* records *)
let u_acc = prepare_boolvar BoolRec.get (fun x ->
List.map (fun (r,some,none) ->
let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
(Record (r,some,none))
) (Record.get { empty with record = BoolRec.atom (`Atm x) })) tt.record u_acc
in
let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd ->
match Abstracts.print bdd with
|[x] -> [Atomic x]
|l -> [Union(alloc (List.map (fun x -> (Atomic x)) l))]
) tt.abstract u_acc
in
let u_acc =
if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc
else u_acc
in
fix u_acc
in
let printed = if is_empty not_var then [] else print_descr not_var in
let printed = printed @ printed_seq in
if is_empty not_seq then (slot.def <- printed @ slot.def ; slot)
else
let printed_not_seq = print_descr not_seq in
begin
match printed_topvar with
[] -> if subtype any not_seq then slot.def <- (Neg (alloc [])) :: slot.def
else slot.def <- printed @ printed_not_seq @ slot.def
| _ -> if subtype any not_seq then slot.def <- ((intersection printed_topvar) :: printed) @ slot.def
else
slot.def <- (intersection ((union printed_not_seq) :: printed_topvar)) :: (printed @ slot.def)
end;
slot
and decompile d =
let aux t =
......@@ -2021,6 +2132,8 @@ struct
| Char c -> Chars.V.print ppf c
| Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
| Atomic a -> a ppf
| Intersection { def = ([ Neg b ; a ] | [ a; Neg b]) } ->
Format.fprintf ppf "@[%a@] \\ (@[%a@])" (do_print pri) a (do_print_slot pri) b
| Intersection { def = [ a ] }
| Union { def = [ a ] } -> Format.fprintf ppf "@[%a@]" (do_print pri) a
| Intersection a -> Format.fprintf ppf "@[%a@]" (do_print_slot ~sep:"&" 2) a
......@@ -3041,12 +3154,7 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,delta,mem) =
Format.eprintf "In norm %a@\n" Print.pp_type t;
Format.eprintf "Mem is: @\n";
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "------------------@\n";
(* if we already evaluated it, it is sat *)
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end
......@@ -3062,14 +3170,7 @@ module Tallying = struct
else if (*no_var t*) Var.Set.subset t.toplvars.TLV.fv delta
then CS.unsat
else begin
Format.eprintf "Mem before is: @\n";
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "------------------@\n";
let mem = DescrSet.add t mem in
Format.eprintf "Mem after adding %a is: @\n" Print.pp_type t;
DescrSet.iter (fun e -> Format.eprintf "%a@\n" Print.pp_type e) mem;
Format.eprintf "=============================@\n";
let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
......@@ -3393,7 +3494,6 @@ let squaresubtype delta s t =
| Tallying.Step2Fail -> () (* continue *)
in
let rec loop i =
Format.eprintf "Tallying at step %i@\n" i;
try
let ss =
if i = 0 then s
......
module V = struct
type t = { id : string; repr : string }
let dump ppf t =
let dump ppf t =
let r = if t.repr = t.id then "" else Format.sprintf ";repr=%s" t.repr in
Format.fprintf ppf "{id=%s;%s}" t.id r
let compare x y = Pervasives.compare x.id y.id
......@@ -48,6 +48,7 @@ module Set = struct
let inter = cap
let cardinal = length
let mem t v = mem v t
let fold = fold
end
type 'a pairvar = [ `Atm of 'a | var ]
......
......@@ -18,7 +18,7 @@ module Set : sig
val pp : Format.formatter -> t -> unit
val printf : t -> unit
val is_empty : t -> bool
val empty : t
val empty : t
val singleton : var -> t
val union : t -> t -> t
val diff : t -> t -> t
......@@ -28,6 +28,7 @@ module Set : sig
val subset : t -> t -> bool
val cardinal : t -> int
val from_list : var list -> t
val fold : ('a -> var -> 'a) -> 'a -> t -> 'a
end
type 'a pairvar = [ `Atm of 'a | var ]
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment