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

Merge branch 'debug-typechecking-issue-27-for-merge'

* debug-typechecking-issue-27-for-merge:
  Remove debugging code.
  Add patricia.cd file from Issue #21
  Check constraints on monomorphic variables at the right place.
  Fix a pretty printing error for ground types (the negative part was not shown due to "worth_complement" being called twice).
  Rework the type variable infrastructure. Remove it from the type structure and have the auxiliary function cache the results as needed.
  Debugging annotations.
parents 924ac464 4eeac845
(* Patricia trees
Chris Okasaki and Andrew Gill's paper Fast Mergeable Integer Maps
http://ittc.ku.edu/~andygill/papers/IntMap98.pdf
*)
type Leaf = <leaf key=Caml_int> 'a
type Branch = <brch pre=Caml_int bit=Caml_int>[ (Leaf|Branch) (Leaf|Branch) ]
type Dict = [] | Branch | Leaf
let lowest_bit (x: Caml_int): Caml_int = Pervasives.land x ((0 - x):?Caml_int)
let branching_bit (p0: Caml_int)(p1: Caml_int): Caml_int = lowest_bit (Pervasives.lxor p0 p1)
let mask (p: Caml_int) (m: Caml_int): Caml_int =
Pervasives.land p (Pervasives.pred m)
let matchPrefix (k: Caml_int)(p: Caml_int)(m: Caml_int): Bool =
mask p m = k
let zero_bit (k: Caml_int)(m: Caml_int): Bool = Pervasives.land k m = 0
let lookup (k: Caml_int)(d: Dict) : ['a?] =
match d with
| [] -> []
| <brch pre=p bit=m>[ t0 t1 ] ->
if not (matchPrefix k p m) then []
else if zero_bit k m then lookup k t0
else lookup k t1
| <leaf key=j> x -> if j=k then [ x ] else []
let join (p0: Caml_int, t0: Dict\[],p1: Caml_int,t1: Dict\[]): Leaf | Branch =
let m = branching_bit p0 p1 in
if zero_bit p0 m then
<brch pre=(mask p0 m) bit=m>[t0 t1]
else
<brch pre=(mask p0 m) bit=m>[t1 t0]
let insert (c: 'a -> 'a -> 'a) (k: Caml_int) (x: 'a) (t: Dict): Leaf|Branch =
let ins (Leaf|Branch -> Leaf|Branch ; [] -> Leaf )
| [] -> <leaf key=k> x
| (<leaf key=j>y)&t ->
if j=k then <leaf key=k>(c x y)
else join (k,<leaf key=k>x,j,t)
| (<brch pre=p bit=m>[ t0 t1 ])&t ->
if matchPrefix k p m then
if zero_bit k m then <brch pre=p bit=m>[ (ins t0) t1 ]
else <brch pre=p bit=m>[ t0 (ins t1) ]
else join (k,<leaf key=k>x,p,t)
in ins t
......@@ -137,70 +137,6 @@ 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.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
(* each kind is represented as a union of itersection of types
......@@ -233,9 +169,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 +186,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 +200,6 @@ struct
BoolPair.dump d.xml
BoolAbstracts.dump d.abstract
d.absent
TLV.dump d.toplvars
let empty = {
times = BoolPair.empty;
......@@ -279,8 +210,7 @@ struct
atoms = BoolAtoms.empty;
chars = BoolChars.empty;
abstract = BoolAbstracts.empty;
absent= false;
toplvars = TLV.empty
absent = false;
}
(*
......@@ -291,13 +221,12 @@ struct
times = BoolPair.full;
xml = BoolPair.full;
arrow = BoolPair.full;
record= BoolRec.full;
record = BoolRec.full;
ints = BoolIntervals.full;
atoms = BoolAtoms.full;
chars = BoolChars.full;
abstract = BoolAbstracts.full;
absent= false;
toplvars = TLV.any
absent = false;
}
let check a =
......@@ -405,7 +334,8 @@ type descr = Descr.t
type node = Node.t
include Descr
let forward_print = ref (fun _ _ -> assert false)
let dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print
let make () =
incr count;
......@@ -430,30 +360,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 +382,16 @@ 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
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,32 +400,26 @@ 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;
record= BoolRec.cap x.record y.record;
record = BoolRec.cap x.record y.record;
arrow = BoolPair.cap x.arrow y.arrow;
atoms = BoolAtoms.cap x.atoms y.atoms;
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 +429,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 =
......@@ -954,7 +805,8 @@ let rec slot d =
then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
else try DescrHash.find memo d
else try
DescrHash.find memo d
with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in
DescrHash.add memo d s;
......@@ -1084,6 +936,134 @@ 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 *)
module type BVS =
sig
type elem
type t
val get : t -> (elem list* elem list) list
end
let get_variables main_memo temp_memo 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
DescrHash.find main_memo t
with
Not_found -> begin
try DescrHash.find temp_memo t with
Not_found ->
let acc = Var.Set.(empty,empty,empty) in
DescrHash.add temp_memo 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 temp_memo t acc;
acc
end
in
(Var.Set.union tvpos tpos,
Var.Set.union tvneg tneg,
Var.Set.union tvars vars)
in
get_variables true Var.Set.(empty,empty,empty) t
let get_variables =
let main_memo = DescrHash.create 17 in
fun t ->
try DescrHash.find main_memo t
with Not_found ->
let res = get_variables main_memo (DescrHash.create 17) t in
DescrHash.add main_memo 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 =
......@@ -1771,7 +1751,7 @@ struct
trivial_pair d.arrow && trivial_rec d.record)
let worth_complement d =
let aux f x y = if f x y = 0 then 1 else 0 in
let aux f x y = if f x y = 0 then 1 else 0 in
let n =
aux BoolAtoms.compare d.atoms any.atoms +
aux BoolChars.compare d.chars any.chars +
......@@ -1875,8 +1855,9 @@ struct
false, res
with Not_found -> true, [ Key.empty , any ]
in
if found_any then (slot.def <- [Neg (alloc [])];slot)
else
if found_any then begin
(slot.def <- [Neg (alloc [])];slot)
end else
let merge_column_with (v1,t1) l =
List.fold_left (fun (accv, accl) ((v2,t2) as x) ->
if equal t1 t2 then (v2::accv, accl) else (accv,x::accl))
......@@ -1964,7 +1945,7 @@ struct
| l, [] -> [ inter_nd l ]
| l1, l2 -> [ Diff (alloc [inter_nd l1], alloc l2) ]
in
if subtype any tt then print_topvars true [] else
(*if subtype any tt then print_topvars true [] else*)
let tt, positive =
if worth_complement tt then
diff any tt, false
......@@ -3011,7 +2992,7 @@ module Tallying = struct
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold
let empty = VarMap.empty
let for_all = VarMap.for_all
end
(* equation set : (s < alpha < t) stored as
......@@ -3132,7 +3113,7 @@ module Tallying = struct
add merged acc2
)
s2 acc1) s1 []
let filter = List.filter
end
type s = S.t
......@@ -3150,27 +3131,13 @@ module Tallying = struct
type sl = sigma list
let singleton delta c =
let constr, do_check, t1, t2 =
let singleton _delta c =
let constr =
match c with
|Pos (v,s) ->
if Var.Set.mem v delta then M.empty, true, (var v), s
else M.singleton v (empty,s), false, empty, empty
|Neg (s,v) ->
if Var.Set.mem v delta then M.empty, true, s, (var v)
else M.singleton v (s,any), false, empty, empty
|Pos (v,s) -> M.singleton v (empty,s)
|Neg (s,v) -> M.singleton v (s,any)
in
let res = S.singleton constr in
if do_check then
if subtype t1 t2 then res
else
raise (UnSatConstr
(Format.sprintf
"Constraint (%s) <= (%s) on monomorphic variable failed"
(Utils.string_of_formatter Print.pp_type t1)
(Utils.string_of_formatter Print.pp_type t2)
))
else res
S.singleton constr
let pp_s = S.pp
let pp_m = M.pp
......@@ -3221,7 +3188,8 @@ module Tallying = struct
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
(* check if there exists a toplevel varaible : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n = match (p,n) with
let toplevel delta single norm_rec mem p n =
match (p,n) with
|([],(`Var x)::neg) ->
let t = single (false,x,[],neg) in
CS.singleton delta (Neg (t,`Var x))
......@@ -3252,37 +3220,43 @@ module Tallying = struct
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,delta,mem) =
(* 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
else begin
if DescrSet.mem t mem || is_empty t then CS.sat
else if is_var t then begin
(* if there is only one variable then is it A <= 0 or 1 <= A *)
if is_var t then