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

Merge branch 'new-variables-issue-26' into debug-typechecking-issue-27

* new-variables-issue-26:
  Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
  Properly check constraints on monomprhic variable during constraint generation: when a constraint 'a < t or t < 'a with 'a being monomorphic occurs during constraint generation, we check whether it holds for all 'a, that is we use plain subtyping. (It generalizes the fact that 'a < Any or Empty < 'a hold for monomorphic variables, but also accounts for constraints such as 'a < 'a | t and so on).

Conflicts:
	types/types.ml
parents 0f2c54a2 e8ebd69d
......@@ -137,69 +137,69 @@ module BoolChars : BoolVar.S with
module BoolAbstracts : BoolVar.S with
type s = Abstracts.t = BoolVar.Make(Abstracts)
module TLV = struct
module Set = struct
include Set.Make(
struct
type t = (Var.var * bool)
let compare (v1,p1) (v2,p2) =
let c = Var.compare v1 v2 in
if c == 0 then
if p1 == p2 then 0
else if p1 then 1 else -1
else c
end)
let pp_aux ppf pp_elem s =
let f ppf = function
|(v,true) -> Format.fprintf ppf "%a" pp_elem v
|(v,false) -> Format.fprintf ppf "~ %a" pp_elem v
in
Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s)
let dump ppf s = pp_aux ppf Var.dump s
let pp ppf s = pp_aux ppf Var.pp s
let printf = pp Format.std_formatter
end
(* tlv : top level variables
* fv : all free variables in the subtree *)
type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool }
let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false }
let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true }
(* return the max of top level variables *)
let max x = Set.max_elt x.tlv
let pair x y = {
tlv = Set.empty ;
fv = Var.Set.union x.fv y.fv ;
isvar = false
}
let record x = {
tlv = Set.empty ;
fv = x.fv ;
isvar = false
}
(* true if it contains only one variable *)
let is_single t = t.isvar || ((Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1))
let no_variables t = Var.Set.is_empty t.fv
let has_toplevel t = Set.cardinal t.tlv > 0
let pp ppf x = Set.pp ppf x.tlv
let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv
let printf = pp Format.std_formatter
let mem v x = Set.mem v x.tlv
end
(* module TLV = struct *)
(* module Set = struct *)
(* include Set.Make( *)
(* struct *)
(* type t = (Var.var * bool) *)
(* let compare (v1,p1) (v2,p2) = *)
(* let c = Var.compare v1 v2 in *)
(* if c == 0 then *)
(* if p1 == p2 then 0 *)
(* else if p1 then 1 else -1 *)
(* else c *)
(* end) *)
(* let pp_aux ppf pp_elem s = *)
(* let f ppf = function *)
(* |(v,true) -> Format.fprintf ppf "%a" pp_elem v *)
(* |(v,false) -> Format.fprintf ppf "~ %a" pp_elem v *)
(* in *)
(* Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s) *)
(* let dump ppf s = pp_aux ppf Var.dump s *)
(* let pp ppf s = pp_aux ppf Var.pp s *)
(* let printf = pp Format.std_formatter *)
(* end *)
(* (\* tlv : top level variables *)
(* * fv : all free variables in the subtree *\) *)
(* type t = { tlv : Set.t ; fv : Var.Set.t; isvar : bool } *)
(* let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(* let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true } *)
(* (\* return the max of top level variables *\) *)
(* let max x = Set.max_elt x.tlv *)
(* let pair x y = { *)
(* tlv = Set.empty ; *)
(* fv = Var.Set.union x.fv y.fv ; *)
(* isvar = false *)
(* } *)
(* let record x = { *)
(* tlv = Set.empty ; *)
(* fv = x.fv ; *)
(* isvar = false *)
(* } *)
(* (\* true if it contains only one variable *\) *)
(* let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1) *)
(* let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0) *)
(* let has_toplevel t = Set.cardinal t.tlv > 0 *)
(* let pp ppf x = Set.pp ppf x.tlv *)
(* let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv *)
(* let printf = pp Format.std_formatter *)
(* let mem v x = Set.mem v x.tlv *)
(* end *)
module rec Descr :
sig
......@@ -233,9 +233,6 @@ sig
* absent . It is used for optional arguments in functions as ?Int
* is the union of Int ^ undef where undef is a type with absent : true *)
absent: bool;
(* maintains the list of all toplevel type variables in s
* and a flag that is true if s contains only variables, false otherwise *)
toplvars : TLV.t
}
include Custom.T with type t = s
val empty: t
......@@ -253,12 +250,11 @@ struct
record: BoolRec.t;
abstract: BoolAbstracts.t;
absent: bool;
toplvars : TLV.t
}
type t = s
let dump ppf d =
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n%a"
Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n"
BoolAtoms.dump d.atoms
BoolIntervals.dump d.ints
BoolChars.dump d.chars
......@@ -268,7 +264,6 @@ struct
BoolPair.dump d.xml
BoolAbstracts.dump d.abstract
d.absent
TLV.dump d.toplvars
let empty = {
times = BoolPair.empty;
......@@ -279,8 +274,7 @@ struct
atoms = BoolAtoms.empty;
chars = BoolChars.empty;
abstract = BoolAbstracts.empty;
absent= false;
toplvars = TLV.empty
absent = false;
}
(*
......@@ -297,7 +291,6 @@ struct
chars = BoolChars.full;
abstract = BoolAbstracts.full;
absent= false;
toplvars = TLV.any
}
let check a =
......@@ -430,30 +423,15 @@ let non_constructed_or_absent =
{ non_constructed with absent = true }
(* Descr.t type constructors *)
let times x y = { empty with
times = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with
xml = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with
arrow = BoolPair.atom (`Atm (Pair.atom (x,y)));
toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let record label t =
{ empty with
record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t)));
toplvars = TLV.record (descr t).toplvars }
let tlv_from_rec (_, l) =
let rec aux acc = function
| (_, n) :: rest -> aux (TLV.pair acc (descr n).toplvars) rest
| [] -> acc in
aux TLV.empty (Ident.LabelMap.get l)
{ empty with record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
let record_fields x =
{ empty with record = BoolRec.atom (`Atm (Rec.atom x));
toplvars = tlv_from_rec x }
{ empty with record = BoolRec.atom (`Atm (Rec.atom x)) }
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
......@@ -467,71 +445,25 @@ let var a = {
atoms = BoolAtoms.vars a;
chars = BoolChars.vars a;
abstract = BoolAbstracts.vars a;
absent= false;
toplvars = TLV.singleton (a,true)
absent = false;
}
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
let update_tlv x y t =
let open TLV in
let tlv t =
let aux get bdd : Set.t =
let l =
List.fold_left (fun acc (p,n) ->
let acc1 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,true))
|_ -> acc
) Set.empty p
in
let acc2 =
List.fold_left (fun acc -> function
|(`Var v) as x -> Set.union acc (Set.singleton (x,false))
|_ -> assert false
) acc1 n
in acc2::acc
) [] (get bdd)
in
match l with
|[] -> Set.empty
|[h] -> h
|h::l -> List.fold_left Set.union h l
in
List.fold_left Set.union
(aux BoolChars.get t.chars)
[
(aux BoolIntervals.get t.ints);
(aux BoolAtoms.get t.atoms);
(aux BoolPair.get t.arrow);
(aux BoolPair.get t.xml);
(aux BoolRec.get t.record)
]
in
let fv t =
if Descr.is_empty t || equal t Descr.any then Var.Set.empty
else Var.Set.union x.toplvars.fv y.toplvars.fv
in
let toplvars = { tlv = tlv t ; fv = fv t ; isvar = t.toplvars.isvar } in
{ t with toplvars = toplvars }
;;
let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars
let all_vars t = t.toplvars.TLV.fv
let all_tlv t = t.toplvars.TLV.tlv
module type BVS =
sig
type elem
type t
val get : t -> (elem list* elem list) list
end
let is_closed delta t = (no_var t) || (Var.Set.is_empty (Var.Set.diff (all_vars t) delta))
let cup x y =
if x == y then x else
let t = {
{
times = BoolPair.cup x.times y.times;
xml = BoolPair.cup x.xml y.xml;
arrow = BoolPair.cup x.arrow y.arrow;
......@@ -540,15 +472,12 @@ let cup x y =
atoms = BoolAtoms.cup x.atoms y.atoms;
chars = BoolChars.cup x.chars y.chars;
abstract = BoolAbstracts.cup x.abstract y.abstract;
absent= x.absent || y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
absent = x.absent || y.absent;
}
let cap x y =
if x == y then x else
let t = {
{
ints = BoolIntervals.cap x.ints y.ints;
times = BoolPair.cap x.times y.times;
xml = BoolPair.cap x.xml y.xml;
......@@ -558,14 +487,11 @@ let cap x y =
chars = BoolChars.cap x.chars y.chars;
abstract = BoolAbstracts.cap x.abstract y.abstract;
absent= x.absent && y.absent;
toplvars = TLV.empty
} in
let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
}
let diff x y =
if x == y then empty else
let t = {
{
times = BoolPair.diff x.times y.times;
xml = BoolPair.diff x.xml y.xml;
arrow = BoolPair.diff x.arrow y.arrow;
......@@ -575,10 +501,7 @@ let diff x y =
chars = BoolChars.diff x.chars y.chars;
abstract = BoolAbstracts.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
toplvars = TLV.empty
} in
let isvar = (equal x any && is_var y) || (is_var x && equal y empty) in
update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}
}
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
......@@ -1084,6 +1007,122 @@ let subtype d1 d2 = is_empty (diff d1 d2)
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
(* functions on variables need the subtyping relation *)
let get_variables =
let memo_descr = DescrHash.create 17 in
fun t ->
let get_vars_conj get_atom pos acc l =
List.fold_left (fun acc e ->
get_atom pos acc e) acc l
in
let get_vars_bdd (type s) (type e)
(module BV : BVS with type elem = e and type t = s)
get_atom _pos acc bdd
=
List.fold_left (fun ((tlvp, tlvn, vars) as acc) (p, n) ->
let acc' = get_vars_conj get_atom true acc p in
get_vars_conj get_atom false acc' n
) acc (BV.get bdd)
in
let get_vars_boolvar get_atom pos (tlvp, tlvn, vars) = function
| (`Var v ) as x when pos -> Var.Set.add x tlvp, tlvn, Var.Set.add x vars
| (`Var v ) as x -> tlvp, Var.Set.add x tlvn, Var.Set.add x vars
| `Atm x ->
let _, _, vars' = get_atom pos (Var.Set.empty, Var.Set.empty, vars) x
in
tlvp, tlvn, vars'
in
let get_nothing _ acc _ = acc in
let rec get_pair pos acc (t1, t2) =
let acc1 = get_variables pos acc (descr t1) in
get_variables pos acc1 (descr t2)
and get_record pos acc (_, lmap) =
LabelMap.fold (fun _ t acc -> get_variables pos acc (descr t)) lmap acc
and get_bdd_pair pos = get_vars_bdd (module Pair) (get_pair) pos
and get_bdd_record pos = get_vars_bdd (module Rec) (get_record) pos
and get_bv_pairs pos = get_vars_bdd (module BoolPair)
(get_vars_boolvar get_bdd_pair) pos
and get_bv_recs pos = get_vars_bdd (module BoolRec)
(get_vars_boolvar get_bdd_record) pos
and get_variables pos (tvpos,tvneg,vars) t =
let tpos, tneg, tvars =
try
let r = DescrHash.find memo_descr t in
r
with
Not_found ->
let acc = Var.Set.(empty,empty,empty) in
DescrHash.add memo_descr t acc;
let acc = get_vars_bdd (module BoolIntervals)
(get_vars_boolvar get_nothing) pos acc t.ints in
let acc = get_vars_bdd (module BoolChars)
(get_vars_boolvar get_nothing) pos acc t.chars in
let acc = get_vars_bdd (module BoolAtoms)
(get_vars_boolvar get_nothing) pos acc t.atoms in
let acc = get_vars_bdd (module BoolAbstracts)
(get_vars_boolvar get_nothing) pos acc t.abstract in
let acc = get_bv_pairs pos acc t.times in
let acc = get_bv_pairs pos acc t.xml in
let acc = get_bv_pairs pos acc t.arrow in
let acc = get_bv_recs pos acc t.record in
DescrHash.replace memo_descr t acc;
acc
in
(Var.Set.union tvpos tpos,
Var.Set.union tvneg tneg,
Var.Set.union tvars vars)
in
try
DescrHash.find memo_descr t
with
Not_found ->
let res = get_variables true Var.Set.(empty,empty,empty) t in
DescrHash.add memo_descr t res;
res
let check_var =
let aux t =
let tvpos, tvneg, tvars = get_variables t in
match Var.Set.(cardinal tvpos, cardinal tvneg, cardinal tvars) with
1, 0, 1 -> let v = Var.Set.choose tvpos in
if equiv (var v) t then `Pos v else `NotVar
| 0, 1, 1 -> let v = Var.Set.choose tvneg in
if equiv (diff any (var v)) t then `Neg v else `NotVar
| _ -> `NotVar
in
let memo_descr = DescrHash.create 17 in
fun t -> try DescrHash.find memo_descr t with
Not_found ->
let res = aux t in
DescrHash.add memo_descr t res;
res
let is_var t = match check_var t with `NotVar -> false | _ -> true
let no_var t =
let _, _, s = get_variables t in Var.Set.is_empty s
let has_tlv t =
let p, n, _ = get_variables t in
not Var.Set.(is_empty p && is_empty n)
let all_vars t =
let _, _, s = get_variables t in s
let all_tlv t =
let p , n, _ = get_variables t in Var.Set.union p n
let is_closed delta t =
Var.Set.(is_empty (diff (all_vars t) delta))
let extract_variable t =
match check_var t with
`Pos v -> v, true
| `Neg v -> v, false
| _ -> assert false
module Cache = struct
type 'a cache =
......@@ -3458,7 +3497,7 @@ module Tallying = struct
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if is_var t then begin
let (beta,_) = TLV.max t.toplvars in
let (beta,_) = extract_variable t in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
aux alpha (s,t) acc1
......@@ -3584,7 +3623,7 @@ module Tallying = struct
let codomain ll =
List.fold_left (fun acc e ->
CS.E.fold (fun _ v acc ->
Var.Set.union v.toplvars.TLV.fv acc
Var.Set.union (all_vars v) acc
) e acc
) Var.Set.empty ll
......
module V = struct
type t = { id : string; repr : string }
let dump ppf t =
......
......@@ -30,6 +30,7 @@ module Set : sig
val cardinal : t -> int
val from_list : var list -> t
val fold : ('a -> var -> 'a) -> 'a -> t -> 'a
val choose : t -> var
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