Commit 496c41bd authored by Kim Nguyễn's avatar Kim Nguyễn

Revert "Implement a cache for the positive equation solver (partial results are stored in nodes)"

This reverts commit a8ba6ab6.

This commit introduces a regression where suprious type variables are introduced in the final type.
parent a8ba6ab6
......@@ -41,7 +41,7 @@ let balance ( Unbalanced('a) -> Rtree('a) ; 'b & RBtree('a) -> 'b & RBtree('a) )
| x -> x
;;
let [] = []
(* *)
(* Version 2: restrict the first branch to Unbalanced trees whatever *)
(* type it contains *)
......@@ -182,8 +182,8 @@ let cardinal ( RBtree('a) -> Int ) (* better type: [] -> 0, Any\[] -> [1--*] *
raise "impossible"
| <(c) elem=e>[ l r ] ->
(<black elem=e>[ l (balance (redify r)) ], (c = `black))
(*
let remove(x : 'a)(t : RBtree('a) ) : RBtree('a) =
let remove_aux(RBtree('a) -> (RBtree('a),Bool) )
| [] ->
......@@ -206,5 +206,4 @@ let remove(x : 'a)(t : RBtree('a) ) : RBtree('a) =
let tree = <(c) elem=z>[ ll r] in
if d then bubble_left tree else (tree, `false)
in
let (sol,_) = remove_aux t in sol
*)
let (sol,_) = remove_aux t in sol
\ No newline at end of file
......@@ -64,7 +64,6 @@ sig
val mapi: (Elem.t -> 'a -> 'b) -> 'a map -> 'b map
val constant: 'a -> t -> 'a map
val num: int -> t -> int map
val init : (Elem.t -> 'a) -> t -> 'a map
val map_to_list: ('a -> 'b) -> 'a map -> 'b list
val mapi_to_list: (Elem.t -> 'a -> 'b) -> 'a map -> 'b list
val assoc: Elem.t -> 'a map -> 'a
......@@ -98,9 +97,9 @@ module Make(X : Custom.T) = struct
let hash l = hash 1 l
let rec compare l1 l2 =
if l1 == l2 then 0
if l1 == l2 then 0
else match (l1,l2) with
| x1::l1, x2::l2 ->
| x1::l1, x2::l2 ->
let c = Elem.compare x1 x2 in if c <> 0 then c
else compare l1 l2
| [],_ -> -1
......@@ -116,7 +115,7 @@ module Make(X : Custom.T) = struct
external get: t -> Elem.t list = "%identity"
let singleton x = [ x ]
let pick = function x::_ -> Some x | _ -> None
let pick = function x::_ -> Some x | _ -> None
let choose = function x::_ -> x | _ -> raise Not_found
let length = List.length
......@@ -126,13 +125,13 @@ module Make(X : Custom.T) = struct
let rec disjoint l1 l2 =
if l1 == l2 then l1 == [] else
match (l1,l2) with
| (t1::q1, t2::q2) ->
| (t1::q1, t2::q2) ->
let c = Elem.compare t1 t2 in
if c < 0 then disjoint q1 l2
else if c > 0 then disjoint l1 q2
else false
| _ -> true
let rec cup l1 l2 =
if l1 == l2 then l1 else
match (l1,l2) with
......@@ -145,7 +144,7 @@ module Make(X : Custom.T) = struct
| (l1,[]) -> l1
let add x l = cup [x] l
let rec split l1 l2 =
match (l1,l2) with
| (t1::q1, t2::q2) ->
......@@ -154,8 +153,8 @@ module Make(X : Custom.T) = struct
else if c < 0 then let (l1,i,l2) = split q1 l2 in (t1::l1,i,l2)
else let (l1,i,l2) = split l1 q2 in (l1,i,t2::l2)
| _ -> (l1,[],l2)
let rec diff l1 l2 =
if l1 == l2 then [] else
match (l1,l2) with
......@@ -178,7 +177,7 @@ module Make(X : Custom.T) = struct
else cap l1 q2
| _ -> []
let rec subset l1 l2 =
(l1 == l2) ||
match (l1,l2) with
......@@ -197,8 +196,8 @@ module Make(X : Custom.T) = struct
else if c < 0 then false
else subset l1 q2
| [],_ -> true | _ -> false
let from_list l =
let from_list l =
let rec initlist = function
| [] -> []
| e::rest -> [e] :: initlist rest in
......@@ -210,14 +209,14 @@ module Make(X : Custom.T) = struct
| [l] -> l
| llist -> mergeall (merge2 llist) in
mergeall (initlist l)
let map f l =
from_list (List.map f l)
let rec mem l x =
match l with
| [] -> false
| t::q ->
| t::q ->
let c = Elem.compare x t in
(c = 0) || ((c > 0) && (mem q x))
......@@ -248,7 +247,7 @@ module Make(X : Custom.T) = struct
let rec assoc_remove_aux v r = function
| ((x,y) as a)::l ->
let c = Elem.compare x v in
if c = 0 then (r := Some y; l)
if c = 0 then (r := Some y; l)
else if c < 0 then a :: (assoc_remove_aux v r l)
else raise Not_found
| [] -> raise Not_found
......@@ -324,7 +323,7 @@ module Make(X : Custom.T) = struct
let rec mem x l =
match l with
| [] -> false
| (t,_)::q ->
| (t,_)::q ->
let c = Elem.compare x t in
(c = 0) || ((c > 0) && (mem x q))
......@@ -346,7 +345,7 @@ module Make(X : Custom.T) = struct
else restrict l1 q2
| _ -> []
let from_list f l =
let from_list f l =
let rec initlist = function
| [] -> []
| e::rest -> [e] :: initlist rest in
......@@ -359,7 +358,7 @@ module Make(X : Custom.T) = struct
| llist -> mergeall (merge2 llist) in
mergeall (initlist l)
let from_list_disj l =
let from_list_disj l =
let rec initlist = function
| [] -> []
| e::rest -> [e] :: initlist rest in
......@@ -375,7 +374,7 @@ module Make(X : Custom.T) = struct
let rec map_from_slist f = function
| x::l -> (x,f x)::(map_from_slist f l)
| [] -> []
let rec collide f l1 l2 =
match (l1,l2) with
| (_,y1)::l1, (_,y2)::l2 -> f y1 y2; collide f l1 l2
......@@ -411,14 +410,10 @@ module Make(X : Custom.T) = struct
| (x,y)::l -> (f y)::(map_to_list f l)
| [] -> []
let rec init f = function
[] -> []
| x :: l -> (x, f x) :: (init f l)
let rec assoc v = function
| (x,y)::l ->
let c = Elem.compare x v in
if c = 0 then y
if c = 0 then y
else if c < 0 then assoc v l
else raise Not_found
| [] -> raise Not_found
......@@ -431,7 +426,7 @@ module Make(X : Custom.T) = struct
| [] -> assert false
let rec compare f l1 l2 =
if l1 == l2 then 0
if l1 == l2 then 0
else match (l1,l2) with
| (x1,y1)::l1, (x2,y2)::l2 ->
let c = Elem.compare x1 x2 in if c <> 0 then c
......@@ -453,13 +448,13 @@ module Make(X : Custom.T) = struct
let rec check f = function
| (x,a)::((y,b)::_ as tl) ->
| (x,a)::((y,b)::_ as tl) ->
Elem.check x; f a;
assert (Elem.compare x y < 0); check f tl
| [x,a] -> Elem.check x; f a
| _ -> ()
end (* Map *)
end (* Map *)
module MakeMap(Y : Custom.T) = struct
......@@ -469,10 +464,10 @@ module Make(X : Custom.T) = struct
in types.ml... *)
let hash x = Map.hash Y.hash x
let compare x y = Map.compare Y.compare x y
let equal x y = Map.equal Y.equal x y
let equal x y = Map.equal Y.equal x y
let check l = Map.check Y.check l
let dump ppf l =
let dump ppf l =
List.iter (fun (x,y) ->
Format.fprintf ppf "(%a->%a)" Elem.dump x Y.dump y) l
......@@ -512,7 +507,7 @@ module FiniteCofinite(X : Custom.T) = struct
let compare l1 l2 =
match (l1,l2) with
| Finite l1, Finite l2
| Finite l1, Finite l2
| Cofinite l1, Cofinite l2 -> SList.compare l1 l2
| Finite _, Cofinite _ -> -1
| _ -> 1
......@@ -560,11 +555,11 @@ module FiniteCofinite(X : Custom.T) = struct
let neg = function
| Finite s -> Cofinite s
| Cofinite s -> Finite s
let contains x = function
| Finite s -> SList.mem s x
| Cofinite s -> not (SList.mem s x)
let disjoint s t =
match (s,t) with
| (Finite s, Finite t) -> SList.disjoint s t
......@@ -586,79 +581,79 @@ struct
let sample = function
| Cofinite _ -> None
| Finite l -> (match T.get l with
| Finite l -> (match T.get l with
| [] -> raise Not_found
| (x,y)::_ -> Some (x, SymbolSet.sample y))
let get = function
| Finite l -> `Finite (T.get l)
| Cofinite l -> `Cofinite (T.get l)
let check = function
| Finite l | Cofinite l -> TMap.check l
let dump ppf = function
| Finite s -> Format.fprintf ppf "Finite[%a]" TMap.dump s
| Cofinite s -> Format.fprintf ppf "Cofinite[%a]" TMap.dump s
let empty = Finite T.empty
let any = Cofinite T.empty
let any_in_ns ns = Finite (T.singleton ns SymbolSet.any)
let finite l =
let l =
T.filter
let l =
T.filter
(fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
l in
Finite l
let cofinite l =
let l =
T.filter
let l =
T.filter
(fun _ x -> match x with SymbolSet.Finite [] -> false | _ -> true)
l in
Cofinite l
let atom (ns,x) = Finite (T.singleton ns (SymbolSet.atom x))
let cup s t =
match (s,t) with
| (Finite s, Finite t) -> finite (T.merge SymbolSet.cup s t)
| (Finite s, Cofinite t) -> cofinite (T.sub SymbolSet.diff t s)
| (Cofinite s, Finite t) -> cofinite (T.sub SymbolSet.diff s t)
| (Cofinite s, Cofinite t) -> cofinite (T.cap SymbolSet.cap s t)
let cap s t =
match (s,t) with
| (Finite s, Finite t) -> finite (T.cap SymbolSet.cap s t)
| (Finite s, Cofinite t) -> finite (T.sub SymbolSet.diff s t)
| (Cofinite s, Finite t) -> finite (T.sub SymbolSet.diff t s)
| (Cofinite s, Cofinite t) -> cofinite (T.merge SymbolSet.cup s t)
let diff s t =
match (s,t) with
| (Finite s, Cofinite t) -> finite (T.cap SymbolSet.cap s t)
| (Finite s, Finite t) -> finite (T.sub SymbolSet.diff s t)
| (Cofinite s, Cofinite t) -> finite (T.sub SymbolSet.diff t s)
| (Cofinite s, Finite t) -> cofinite (T.merge SymbolSet.cup s t)
let is_empty = function
| Finite l -> T.is_empty l
| _ -> false
| _ -> false
let hash = function
| Finite l -> 1 + 17 * (TMap.hash l)
| Cofinite l -> 2 + 17 * (TMap.hash l)
let compare l1 l2 =
match (l1,l2) with
| Finite l1, Finite l2
| Finite l1, Finite l2
| Cofinite l1, Cofinite l2 -> TMap.compare l1 l2
| Finite _, Cofinite _ -> -1
| _ -> 1
let equal t1 t2 =
let equal t1 t2 =
compare t1 t2 = 0
let symbol_set ns = function
......@@ -668,12 +663,12 @@ struct
(try SymbolSet.neg (T.assoc ns s) with Not_found -> SymbolSet.any)
let contains (ns,x) = function
| Finite s ->
| Finite s ->
(try SymbolSet.contains x (T.assoc ns s) with Not_found -> false)
| Cofinite s ->
| Cofinite s ->
(try not (SymbolSet.contains x (T.assoc ns s)) with Not_found -> true)
let disjoint s t =
let disjoint s t =
is_empty (cap t s) (* TODO: OPT *)
end
......@@ -64,7 +64,6 @@ sig
val mapi: (Elem.t -> 'a -> 'b) -> 'a map -> 'b map
val constant: 'a -> t -> 'a map
val num: int -> t -> int map
val init : (Elem.t -> 'a) -> t -> 'a map
val map_to_list: ('a -> 'b) -> 'a map -> 'b list
val mapi_to_list: (Elem.t -> 'a -> 'b) -> 'a map -> 'b list
val assoc: Elem.t -> 'a map -> 'a
......@@ -104,7 +103,7 @@ module FiniteCofinite(X : Custom.T) : FiniteCofinite with type elem = X.t
module FiniteCofiniteMap(X : Custom.T)(SymbolSet : FiniteCofinite) :
sig
include Custom.T
val empty: t
val any: t
val any_in_ns: X.t -> t
......@@ -118,7 +117,7 @@ sig
val contains: X.t * SymbolSet.elem -> t -> bool
val disjoint: t -> t -> bool
val get: t -> [ `Finite of (X.t * SymbolSet.t) list
val get: t -> [ `Finite of (X.t * SymbolSet.t) list
| `Cofinite of (X.t * SymbolSet.t) list ]
val sample: t -> (X.t * SymbolSet.elem option) option
......
......@@ -2636,8 +2636,7 @@ module Positive = struct
|`Xml of v * v
|`Record of bool * (bool * Ns.Label.t * v) list
]
and v = { mutable def : rhs; mutable node : node option;
mutable descr : Descr.t option}
and v = { mutable def : rhs; mutable node : node option; }
module MemoHash = Hashtbl.Make( struct
type t = v
......@@ -2671,23 +2670,21 @@ module Positive = struct
aux ppf v
let printf = pp Format.std_formatter
let rec make_descr seen v =
match v.descr with
| Some d -> d
| None ->
if List.memq v seen then empty
else
let seen = v :: seen in
match v.def with
if List.memq v seen then empty
else
let seen = v :: seen in
match v.def with
|`Type d -> d
|`Variable d -> var d
|`Variable d -> var d
|`Cup vl -> List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
|`Cap vl -> List.fold_left (fun acc v -> cap acc (make_descr seen v)) any vl
|`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)
|`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 =
match v.node with
......@@ -2700,13 +2697,13 @@ module Positive = struct
n
(* We shadow the corresponding definitions in the outer module *)
let forward () = { def = `Cup []; node = None; descr = None }
let forward () = { def = `Cup []; node = None; }
let def v d = v.def <- d
let cons d = let v = forward () in def v d; v
let ty d = cons (`Type d)
let var d = cons (`Variable d)
let neg v = cons (`Neg v)
let cup vl = cons (`Cup vl)
let rec cup vl = cons (`Cup vl)
let cap vl = cons (`Cap vl)
let times v1 v2 = cons (`Times (v1,v2))
let arrow v1 v2 = cons (`Arrow (v1,v2))
......@@ -2765,7 +2762,6 @@ module Positive = struct
and decompose_type t =
try DescrHash.find memo t
with Not_found ->
let r =
if no_var t then ty t
else
match check_var t with
......@@ -2785,153 +2781,136 @@ module Positive = struct
@@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
in
node_t.def <- (cup descr_t).def; node_t
in
r.descr <- Some t;
r
in
decompose_type t
let solve v = (*match v.descr with
None -> *)internalize (make_node v)
(*| Some t -> T.cons t *)
end
let solve v = internalize (make_node v)
(* [map_var f v] applies returns the type
[v{ 'a <- f 'a}] for all ['a] in [v]
*)
let map_var subst v =
let memo = MemoHash.create 17 in
let rec aux v subst =
try MemoHash.find memo v
with Not_found ->
let node_v = forward () in
let () = MemoHash.add memo v node_v in
let new_v =
match v.def with
|`Type d -> `Type d
(* |`Variable d when Var.Set.mem d delta -> v.def *)
|`Variable d -> (subst d).def
|`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
|`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
|`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
in
aux v subst
module Substitution =
struct
module Map = Var.Set.Map
type t = Descr.t Map.map
type order = int Map.map
let identity = Map.empty
let add v t m =
if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
else Map.add v t m
let of_list l =
List.fold_left (fun acc (v, t) -> add v t acc) identity l
module Memo = Hashtbl.Make
(struct
type subst = t
type t = Descr.t * subst
let equal ((t1, l1) as k1) ((t2, l2) as k2) =
k1 == k2
|| ((t1 == t2 || Descr.equal t1 t2)
&& (l1 == l2 || Map.equal Descr.equal l1 l2))
let apply_subst ?(subst=(fun v -> var v)) ?(after=(fun x -> x)) t =
if no_var t then t else
let res = map_var subst (decompose t) in
let res = after res in
descr (solve res)
(* Given a type t and a polymorphic variable 'a occuring in t,
returns the type s which is the solution of 'a = t *)
let solve_rectype t alpha =
let x = forward () in
let subst d = if Var.equal d alpha then x else var d in
apply_subst ~subst:subst ~after:(fun y -> define x y;x) t
(* Pre-condition : alpha \not\in \delta *)
module MemoSubst =
struct
include Hashtbl.Make (struct
type t = descr * (Var.t * descr) list
let hash (t, l) =
(Descr.hash t + 31 * Map.hash Descr.hash l) land 0x3fff_ffff
end)
let global_memo = Memo.create 17
List.fold_left
(fun acc (v,t) -> Var.hash v + 17 * Descr.hash t + 31 * acc)
(Descr.hash t) l
let equal (t1, l1) (t2, l2) =
Descr.equal t1 t2 && (try List.for_all2 (fun (v1, t1) (v2, t2) ->
Var.equal v1 v2 && Descr.equal t1 t2) l1 l2 with _ -> false)
end)
let rec apply_subst ?(after = (fun x -> x)) ?(do_var= fun x -> Positive.ty x) t subst =
let open Positive in
if subst == identity then descr (solve t) else
let memo = MemoHash.create 17 in
let todo = ref [] in
let rec aux v =
let found, update, v =
match v.descr with
| None -> false, None, v
| Some d ->
let vars = all_vars d in
if Var.Set.is_empty vars then true, None, ty d
else
let subst' = Map.restrict subst vars in
let key = (d, subst') in
try
let d = Memo.find global_memo key in
true, None , ty d
with
Not_found ->
false, Some (key), v
in
if found then v else
let res =
try MemoHash.find memo v
with Not_found ->
match v.def with
|`Variable d ->
let res =
(try
do_var (Map.assoc d subst)
with Not_found -> { forward () with def = v.def })
in
MemoHash.add memo v res; res
| x ->
let node_v = forward () in
let () = MemoHash.add memo v node_v in
let res =
match x with
| `Type _ -> x
| `Cup vl -> `Cup (List.map (fun v -> aux v) vl)
| `Cap vl -> `Cap (List.map (fun v -> aux v) vl)
| `Times (v1,v2) -> `Times (aux v1, aux v2)
| `Arrow (v1,v2) -> `Arrow (aux v1, aux v2)
| `Xml (v1,v2) -> `Xml (aux v1, aux v2)
| `Record (b, flst) ->
`Record (b, List.map (fun (b,l,v) -> (b,l,aux v)) flst)
| `Neg v -> `Neg (aux v)
| `Variable _ -> assert false
in
node_v.def <- res;
node_v
in
let () =
match update with
None -> ()
| Some key -> todo := (key, res) :: !todo
end
let memo_subst = MemoSubst.create 17
let rec substitute_list t l =
if no_var t || l == [] then t else
let k = (t,l) in
try
MemoSubst.find memo_subst k
with Not_found ->
let r =
let subst d =
try
ty
@@ snd
@@ List.find (fun (alpha,_) -> Var.equal d alpha) l
with Not_found -> var d
in
res
in
let res = aux t in
let res = after res in
let tres = descr (solve res) in
List.iter (fun ((d, subst) as key, res) ->
match res.node with
Some t -> begin
try
let (cu, name, al) =
DescrMap.find d !Print.named
in
let nal = List.map (fun (v,t) -> v,apply_subst ~do_var ~after (Positive.decompose t) subst) al
in
Print.register_global (cu, name, nal) d
with Not_found -> () end;
Memo.add global_memo key (descr t)
| _ -> () ) !todo;
tres
apply_subst ~subst:subst t
in
let () =
try
let (cu, name, subst) = DescrMap.find t !Print.named in
let _nsubst =
List.map (fun (v, vt) -> v, substitute_list vt l) subst
in
Print.register_global (cu, name, _nsubst) r;
with Not_found -> ()
in
MemoSubst.add memo_subst k r;
r
let apply t l =
if no_var t then t else
apply_subst (Positive.decompose t) (of_list l)
let apply_single t s = apply t [s]
let substitute t s = substitute_list t [s]
let refresh_type delta t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.fresh v)) vars in
apply_subst (Positive.decompose t) subst
let substitute_kind delta kind t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.set_kind kind v)) vars in
apply_subst (Positive.decompose t) subst
let substitute_free delta t =
let h = Hashtbl.create 17 in
let subst d =
if Var.Set.mem delta d then var d else
try
Hashtbl.find h d
with Not_found ->
let x = var (Var.fresh d) in
Hashtbl.add h d x ;
x
in
apply_subst ~subst:subst t
let substitute_kind delta kind t =
let subst d =
if Var.Set.mem delta d then var d else
var (Var.set_kind kind d)
in
apply_subst ~subst:subst t
(* We cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
latter but the variance annotation tells us that A is invariant. *)
let collect_variables delta v =
let open Positive in
(* 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. We do not need to memoize on delta as
the memoization is local and delta does not change *)
let module Memo =
Hashtbl.Make (struct
type t = bool * Positive.v
type t = bool * v
let hash = Hashtbl.hash
let equal (a,b) (c,d) = a == c && b == d
end)
......@@ -2947,8 +2926,8 @@ struct
in
let vars = Hashtbl.create 17 in
let memo = Memo.create 17 in
let t_emp = Positive.cup [] in
let t_any = Positive.ty any in