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

Small refactoring:

- fix typos in comments
- indent code
- move the Positive module further down types.ml, so that there is no
need for forward references when we implement substitutions over record types.
parent d8c31bd9
......@@ -1453,6 +1453,7 @@ struct
in
aux [] [] d
type t = TR.t
let focus = split_normal
let get_this r = { (TR.pi1 r) with absent = false }
......@@ -2167,6 +2168,187 @@ struct
in aux t;;
end
let memo_normalize = ref DescrMap.empty
let rec rec_normalize d =
try DescrMap.find d !memo_normalize
with Not_found ->
let n = make () in
memo_normalize := DescrMap.add d n !memo_normalize;
let times =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal d)
in
let xml =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal ~kind:`XML d)
in
let record = d.record
in
define n { d with times = times; xml = xml; record = record };
n
let normalize n =
descr (internalize (rec_normalize n))
module Arrow =
struct
let check_simple left (s1,s2) =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_line_non_empty (left,right) =
not (List.exists (check_simple left) right)
let sample t =
let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
{ empty with arrow = any.arrow } left
let check_strenghten t s =
if subtype t s then t else raise Not_found
let check_simple_iface left s1 s2 =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_iface iface s =
let rec aux = function
| [] -> false
| (p,n) :: rem ->
((List.for_all (fun (a,b) -> check_simple_iface iface a b) p) &&
(List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
|| (aux rem)
in
aux (Pair.get (BoolPair.leafconj s.arrow))
type t = descr * (descr * descr) list list
let get t =
List.fold_left
(fun ((dom,arr) as accu) (left,right) ->
if check_line_non_empty (left,right)
then
let left = List.map (fun (t,s) -> (descr t, descr s)) left in
let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
(cap dom d, left :: arr)
else accu
)
(any, [])
(Pair.get (BoolPair.leafconj t.arrow))
let domain (dom,_) = dom
let apply_simple t result left =
let rec aux result accu1 accu2 = function
| (t1,s1)::left ->
let result =
let accu1 = diff accu1 t1 in
if non_empty accu1 then aux result accu1 accu2 left
else result
in
let result =
let accu2 = cap accu2 s1 in
aux result accu1 accu2 left
in
result
| [] ->
if subtype accu2 result then result else cup result accu2
in
aux result t any left
let apply (_,arr) t =
List.fold_left (apply_simple t) empty arr
let need_arg (dom, arr) =
List.exists (function [_] -> false | _ -> true) arr
let apply_noarg (_,arr) =
List.fold_left
(fun accu ->
function
| [(t,s)] -> cup accu s
| _ -> assert false
)
empty arr
let any = { empty with arrow = any.arrow }
let is_empty (_,arr) = arr == []
end
module Int = struct
let has_int d i = Intervals.contains i (BoolIntervals.leafconj d.ints)
let get d = d.ints
let any = { empty with ints = any.ints }
let any = { empty with ints = BoolIntervals.full }
end
module Atom = struct
let has_atom d a = Atoms.contains a (BoolAtoms.leafconj d.atoms)
let get d = d.atoms
let any = { empty with atoms = any.atoms }
end
module OldChar = Char
module Char = struct
let has_char d c = Chars.contains c (BoolChars.leafconj d.chars)
let is_empty d = Chars.is_empty (BoolChars.leafconj d.chars)
let get d = d.chars
let any = { empty with chars = any.chars }
end
let rec tuple = function
| [t1;t2] -> times t1 t2
| t::tl -> times t (cons (tuple tl))
| _ -> assert false
let rec_of_list o l =
let map =
LabelMap.from_list (fun _ _ -> assert false)
(List.map
(fun (opt,qname,typ) ->
qname, cons (if opt then Record.or_absent typ else typ))
l)
in
record_fields (o,map)
let empty_closed_record = rec_of_list false []
let empty_open_record = rec_of_list true []
let cond_partition univ qs =
let rec add accu (t,s) =
let t = if subtype t s then t else cap t s in
if (subtype s t) || (is_empty t) then accu else
let rec aux accu u =
let c = cap u t in
if (is_empty c) || (subtype (cap u s) t) then u::accu
else c::(diff u t)::accu
in
List.fold_left aux [] accu
in
List.fold_left add [ univ ] qs
module Positive =
struct
module T = struct
......@@ -2191,6 +2373,10 @@ struct
|`Arrow of v * v
|`Times of v * v
|`Xml of v * v
(* The following is unused at the moment (since
decompose_rec is a no-op). It should work properly once
records are ok at the type/bdd level *)
|`Record of bool * (bool * Ns.Label.t * v) list
]
and v = { mutable def : rhs; mutable node : node option }
......@@ -2206,6 +2392,7 @@ struct
|`Times (v1,v2) -> times (make_node v1) (make_node v2)
|`Arrow (v1,v2) -> arrow (make_node v1) (make_node v2)
|`Xml (v1,v2) -> xml (make_node v1) (make_node v2)
|`Record (b, flst) -> rec_of_list b (List.map (fun (b,l,v) -> (b,l,make_descr seen v)) flst)
|`Neg v -> neg (make_descr seen v)
and make_node v =
......@@ -2229,11 +2416,21 @@ struct
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
let xml v1 v2 = cons (`Xml (v1,v2))
let record b vlst = cons (`Record (b, vlst))
let define v1 v2 = def v1 (`Cup [v2])
let decompose t =
let memo_decompose = DescrHash.create 17 in
let rec decompose t =
let _decompose_records t =
let rec_list = Record.get t in
cup (List.map (fun (map,op,_) ->
record op
(List.map (fun (lab,(pres,t)) ->
(pres,lab, decompose t))
(Ident.LabelMap.get map))
) rec_list)
in
let aux_bdd ?noderec constr (p,n) =
let aux polarity constr l =
cap (
......@@ -2288,6 +2485,11 @@ struct
(fun p -> { empty with xml = BoolPair.atom (`Atm p) }) (BoolPair.get t.xml);
decompose_aux ~noderec:(subpairs times)
(fun p -> { empty with times = BoolPair.atom (`Atm p) }) (BoolPair.get t.times);
(* Kim: Not sure how to reuse the above to decompose
records, so I'm adding my version here: *)
(* Kim: Not working at the moment, seems variables
are not propagated properly in records *)
(* _decompose_records { empty with record = t.record };*)
]
in
define node_s s; node_s
......@@ -2319,7 +2521,10 @@ struct
|`Times (v1,v2) -> `Times (aux v1 subst, aux v2 subst)
|`Arrow (v1,v2) -> `Arrow (aux v1 subst, aux v2 subst)
|`Xml (v1,v2) -> `Xml (aux v1 subst, aux v2 subst)
|`Record (b, flst) ->
`Record (b, List.map (fun (b,l,v) -> (b,l,aux v subst)) flst)
|`Neg v -> `Neg (aux v subst)
in
node_v.def <- new_v;
node_v
......@@ -2334,12 +2539,12 @@ struct
let substituterec t alpha =
let subst x d =
if Var.equal d alpha then x else
if Var.is_fresh d then begin
(*if Var.is_fresh d then begin
match Var.variance d with
| `Covariant -> ty empty
| `ContraVariant -> ty any
| _ -> var d
end else var d
end else*) var d
in
if no_var t then t
else begin
......@@ -2385,8 +2590,8 @@ struct
| (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll)
in
let memo = ref [] in
let rec aux pos v = (* we memoized based on the pair (pos, v),
since v could occur both positively and negatively.
let rec aux pos v = (* we memoize based on the pair (pos, v),
since v can occur both positively and negatively.
and we want to manage the variables differently in both cases *)
if not (memq_pair (pos,v) !memo) then
let () = memo := (pos,v) :: !memo in
......@@ -2399,6 +2604,7 @@ struct
|`Times (v1,v2) -> (aux pos v1); (aux pos v2)
|`Arrow (v1,v2) -> (aux (not pos) v1); (aux pos v2)
|`Xml (v1,v2) -> (aux pos v1); (aux pos v2)
|`Record (_, flst) -> List.iter (fun (_,_,v) -> aux pos v) flst
|`Neg v -> (aux (not pos) v)
in
aux true v;
......@@ -2427,7 +2633,7 @@ struct
let idx = ref 0 in
let rec pretty_name i acc =
let ni,nm = i/26, i mod 26 in
let acc = acc ^ (String.make 1 (Char.chr (Char.code 'A' + nm))) in
let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'A' + nm))) in
if ni == 0 then acc else pretty_name ni acc
in
let subst h d =
......@@ -2443,15 +2649,12 @@ struct
let new_t = (substitute_aux (decompose t) (subst h)) in
descr(solve new_t)
let arrow_get = ref (fun _ -> assert false)
let clean_type t =
if no_var t then t else
let any_arrow = { empty with arrow = BoolPair.full } in
if not (subtype t any_arrow) then
if not (subtype t Arrow.any) then
beautify_variables (clean_variables t)
else
let _, u_arrow = !arrow_get t in
let _, u_arrow = Arrow.get t in
List.fold_left (fun acc i_arrow ->
T.cup acc (
(List.fold_left (fun acc (dom, cdom) ->
......@@ -2464,187 +2667,6 @@ struct
end
let memo_normalize = ref DescrMap.empty
let rec rec_normalize d =
try DescrMap.find d !memo_normalize
with Not_found ->
let n = make () in
memo_normalize := DescrMap.add d n !memo_normalize;
let times =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal d)
in
let xml =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal ~kind:`XML d)
in
let record = d.record
in
define n { d with times = times; xml = xml; record = record };
n
let normalize n =
descr (internalize (rec_normalize n))
module Arrow =
struct
let check_simple left (s1,s2) =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff_t accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap_t accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_line_non_empty (left,right) =
not (List.exists (check_simple left) right)
let sample t =
let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
{ empty with arrow = any.arrow } left
let check_strenghten t s =
if subtype t s then t else raise Not_found
let check_simple_iface left s1 s2 =
let rec aux accu1 accu2 = function
| (t1,t2)::left ->
let accu1' = diff accu1 t1 in
if non_empty accu1' then aux accu1 accu2 left;
let accu2' = cap accu2 t2 in
if non_empty accu2' then aux accu1 accu2 left
| [] -> raise NotEmpty
in
let accu1 = descr s1 in
(is_empty accu1) ||
(try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
let check_iface iface s =
let rec aux = function
| [] -> false
| (p,n) :: rem ->
((List.for_all (fun (a,b) -> check_simple_iface iface a b) p) &&
(List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
|| (aux rem)
in
aux (Pair.get (BoolPair.leafconj s.arrow))
type t = descr * (descr * descr) list list
let get t =
List.fold_left
(fun ((dom,arr) as accu) (left,right) ->
if check_line_non_empty (left,right)
then
let left = List.map (fun (t,s) -> (descr t, descr s)) left in
let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
(cap dom d, left :: arr)
else accu
)
(any, [])
(Pair.get (BoolPair.leafconj t.arrow))
let () = Positive.arrow_get := get
let domain (dom,_) = dom
let apply_simple t result left =
let rec aux result accu1 accu2 = function
| (t1,s1)::left ->
let result =
let accu1 = diff accu1 t1 in
if non_empty accu1 then aux result accu1 accu2 left
else result
in
let result =
let accu2 = cap accu2 s1 in
aux result accu1 accu2 left
in
result
| [] ->
if subtype accu2 result then result else cup result accu2
in
aux result t any left
let apply (_,arr) t =
List.fold_left (apply_simple t) empty arr
let need_arg (dom, arr) =
List.exists (function [_] -> false | _ -> true) arr
let apply_noarg (_,arr) =
List.fold_left
(fun accu ->
function
| [(t,s)] -> cup accu s
| _ -> assert false
)
empty arr
let any = { empty with arrow = any.arrow }
let is_empty (_,arr) = arr == []
end
module Int = struct
let has_int d i = Intervals.contains i (BoolIntervals.leafconj d.ints)
let get d = d.ints
let any = { empty with ints = any.ints }
let any = { empty with ints = BoolIntervals.full }
end
module Atom = struct
let has_atom d a = Atoms.contains a (BoolAtoms.leafconj d.atoms)
let get d = d.atoms
let any = { empty with atoms = any.atoms }
end
module Char = struct
let has_char d c = Chars.contains c (BoolChars.leafconj d.chars)
let is_empty d = Chars.is_empty (BoolChars.leafconj d.chars)
let get d = d.chars
let any = { empty with chars = any.chars }
end
let rec tuple = function
| [t1;t2] -> times t1 t2
| t::tl -> times t (cons (tuple tl))
| _ -> assert false
let rec_of_list o l =
let map =
LabelMap.from_list (fun _ _ -> assert false)
(List.map
(fun (opt,qname,typ) ->
qname, cons (if opt then Record.or_absent typ else typ))
l)
in
record_fields (o,map)
let empty_closed_record = rec_of_list false []
let empty_open_record = rec_of_list true []
let cond_partition univ qs =
let rec add accu (t,s) =
let t = if subtype t s then t else cap t s in
if (subtype s t) || (is_empty t) then accu else
let rec aux accu u =
let c = cap u t in
if (is_empty c) || (subtype (cap u s) t) then u::accu
else c::(diff u t)::accu
in
List.fold_left aux [] accu
in
List.fold_left add [ univ ] qs
module Tallying = struct
type constr =
......@@ -2694,18 +2716,17 @@ module Tallying = struct
in
VarMap.add v (new_i, new_s) map
(* a set of constraint m1 subsumes a set of constraint m2,
that is the solutions for m1 contains the solutions for
(* a set of constraints m1 subsumes a set of constraints m2,
that is the solutions for m1 contains all the solutions for
m2 if:
forall:
i1 <= v <= s1 in m1,
i2 <= v <= s2 in m2 and i1 <= i2 <= v <= s2 <= s1
forall i1 <= v <= s1 in m1,
there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
*)
let subsumes map1 map2 =
VarMap.for_all (fun v (i1, s1) ->
try let i2, s2 = VarMap.find v map2 in
subtype i1 i2 && subtype s2 s1
subtype i1 i2 && subtype s2 s1
with Not_found -> false) map1
let print ppf map = print_lst (fun ppf (v, (i,s)) ->
......@@ -2779,14 +2800,15 @@ module Tallying = struct
let fold f l a = List.fold_left (fun e a -> f a e) a l
let is_empty = function [] -> true | _ -> false
let is_empty l = l == []
(* Square union : *)
let union s1 s2 =
match s1, s2 with
[], _ -> s2
| _, [] -> s1
| _ ->
(* Invariant all elements of s1 (resp s2) are pairwise
(* Invariant: all elements of s1 (resp s2) are pairwise
incomparable (they don't subsume one another)
let e1 be an element of s1:
- if e1 subsumes no element of s2, add e1 to the result
......@@ -2820,14 +2842,26 @@ module Tallying = struct
in
loop s1 s2 []
(* Square intersection *)
let inter s1 s2 =
match s1,s2 with
[], _ | _, [] -> []
| _ ->
(* Perform the cartesian product. For each constraint m1 in s1,
m2 in s2, we add M.inter m1 m2 to the result.
Optimisations:
- we use add to ensure that we do not add something that subsumes
a constraint set that is already in the result
- if m1 subsumes m2, it means that whenever m2 holds, so does m1, so
we only add m2 (note that the condition is reversed w.r.t. union).
*)
fold (fun m1 acc1 ->
fold (fun m2 acc2 ->
add (M.inter m1 m2) acc2
let merged = if M.subsumes m1 m2 then m2
else if M.subsumes m2 m1 then m1
else M.inter m1 m2
in
add merged acc2
)
s2 acc1) s1 []
......@@ -2928,7 +2962,7 @@ module Tallying = struct
CS.prod acc (f pos neg)
) acc l
(* Kim: these three functions are sed in the (commented) reference
(* Kim: these three functions are used in the (commented) reference
implementation of norm_arrow below *)
let rec remove e = function [] -> []
| x :: ll -> if e == x then ll else x :: (remove e ll)
......@@ -3136,9 +3170,7 @@ module Tallying = struct
then (* no need to add new constraints *)
acc
else
if subtype sup inf then raise (UnSatConstr "merge1")
else
let x = diff inf sup in
let x = diff inf sup in
if DescrHash.mem mem x then acc
else begin
DescrHash.add mem x ();
......@@ -3284,7 +3316,10 @@ end
exception KeepGoing
let apply_raw s t =
DescrHash.clear Tallying.memo_norm;
(*Kim: now that we have removed bugs in the normalisation,
it seems we can keep the memoisation table between calls
*)
(*DescrHash.clear Tallying.memo_norm; *)
let q = Queue.create () in
let gamma = var (Var.mk ~variance:`Covariant "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
......@@ -3306,7 +3341,7 @@ let apply_raw s t =
it is only partial *) not(Queue.is_empty q) do
try
incr counter; (* don't know about termination... *)