Commit 32925cd8 authored by Kim Nguyễn's avatar Kim Nguyễn

Refactoring of the Type_tallying module, using more sensible name and removing unneeded functions.

parent 5d9c8545
......@@ -26,7 +26,7 @@ type iface = (Types.descr * Types.descr) list
type sigma =
| Identity (* this is basically as Types.Tallying.CS.sat *)
| List of Type_tallying.Constr.sl
| List of Types.t Type_tallying.VarMap.map list
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......@@ -104,7 +104,7 @@ module Print = struct
) ppf
in
function
|List ll -> Type_tallying.Constr.pp_sl ppf ll
|List ll -> Type_tallying.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%a,%a,%a)" pp_vloc x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......
......@@ -26,7 +26,7 @@ type iface = (Types.t * Types.t) list
type sigma =
| Identity
| List of Type_tallying.Constr.sl
| List of Types.t Type_tallying.VarMap.map list
| Comp of (sigma * sigma)
| Sel of (var_loc * iface * sigma)
......
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Type_tallying.Constr.sl
| List of Types.t Type_tallying.VarMap.map list
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......@@ -313,7 +313,7 @@ module Print = struct
) ppf
in
function
|List ll -> Type_tallying.Constr.pp_sl ppf ll
|List ll -> Type_tallying.pp_sl ppf ll
|Comp(s1,s2) -> Format.fprintf ppf "Comp(%a,%a)" pp_sigma s1 pp_sigma s2
|Sel(x,iface,s) -> Format.fprintf ppf "Sel(%d,%a,%a)" x pp_aux iface pp_sigma s
|Identity -> Format.fprintf ppf "Id"
......
......@@ -3,7 +3,7 @@ open Encodings
type iface = (Types.t * Types.t) list
type sigma =
| List of Type_tallying.Constr.sl
| List of Types.t Type_tallying.VarMap.map list
| Comp of (sigma * sigma)
| Sel of (int * iface * sigma)
| Identity
......
......@@ -73,6 +73,7 @@ sig
val compare: ('a -> 'a -> int) -> 'a map -> 'a map -> int
val hash: ('a -> int) -> 'a map -> int
val equal: ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
val remove_min : 'a map -> (Elem.t * 'a) * 'a map
end
module MakeMap(Y : Custom.T) : sig
include Custom.T with type t = Y.t Map.map
......@@ -468,6 +469,10 @@ module Make(X : Custom.T) = struct
| [x,a] -> Elem.check x; f a
| _ -> ()
let remove_min = function
e :: l -> e, l
| _ -> failwith "SortedList.Map.min_binding"
end (* Map *)
......
......@@ -73,6 +73,7 @@ sig
val compare: ('a -> 'a -> int) -> 'a map -> 'a map -> int
val hash: ('a -> int) -> 'a map -> int
val equal: ('a -> 'a -> bool) -> 'a map -> 'a map -> bool
val remove_min : 'a map -> (Elem.t * 'a) * 'a map
end
module MakeMap(Y : Custom.T) : sig
include Custom.T with type t = Y.t Map.map
......
......@@ -7,275 +7,220 @@ let cap_product any_left any_right l =
(fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
(any_left,any_right)
l
type constr =
| Pos of (Var.t * Types.t) (** alpha <= t | alpha \in P *)
| Neg of (Types.t * Var.t) (** t <= alpha | alpha \in N *)
exception UnSatConstr of string
module VarMap = Var.Set.Map
module Constr = struct
let semantic_compare t1 t2 =
let inf12 = Types.subtype t1 t2 in
let inf21 = Types.subtype t2 t1 in
if inf12 && inf21 then 0
else if inf12 then -1 else if inf21 then 1 else
let c = Types.compare t1 t2 in
assert (c <> 0);
c
(* Line : is a conjunction of constraints represented as map from variables to
lower and upper bounds:
(s <= alpha <= t)
*)
module Line = struct
type t = (Types.t * Types.t) VarMap.map
let singleton = VarMap.singleton
let length = VarMap.length
(* 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,
there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
*)
let subsumes map1 map2 =
List.for_all (fun (v,(i1, s1)) ->
try let i2, s2 = VarMap.assoc v map2 in
subtype i1 i2 && subtype s2 s1
with Not_found -> false
) (VarMap.get map1)
let print ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.print v Print.pp_type s
) ppf (VarMap.get map)
let compare map1 map2 =
VarMap.compare (fun (i1,s1) (i2,s2) ->
let c = semantic_compare i1 i2 in
if c == 0 then semantic_compare s1 s2
else c) map1 map2
let add delta v (inf, sup) map =
if Var.Set.mem delta v then map
else
let new_i, new_s =
try
let old_i, old_s = VarMap.assoc v map in
cup old_i inf,
cap old_s sup
with
Not_found -> inf, sup
in
VarMap.replace v (new_i, new_s) map
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold
let empty = VarMap.empty
let for_all f m = List.for_all (fun (k,v) -> f k v) (VarMap.get m)
end
(* equation set : (s < alpha < t) stored as
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module E = struct
include Map.Make(struct
type t = Var.t
let compare = Var.compare
end)
let pp ppf e =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.print v Print.pp_type t
) ppf (bindings e)
end
(* Set of equation sets *)
module ES = struct
include Set.Make(struct
type t = Types.t E.t
let compare = E.compare semantic_compare
end)
let pp ppf s = Utils.pp_list ~delim:("{","}") E.pp ppf (elements s)
end
(* Set of constraint sets *)
module S = struct
(* A set of constraint-sets is just a list of constraint-sets,
that are pairwise "non-subsumable"
*)
type t = Line.t list
let elements t = t
let empty = []
let add m l =
let rec loop m l acc =
match l with
[] -> m :: acc
| mm :: ll ->
if Line.subsumes m mm then List.rev_append ll (m::acc)
else if Line.subsumes mm m then List.rev_append ll (mm::acc)
else loop m ll (mm::acc)
in
loop m l []
let singleton m = add m empty
let pp ppf s = Utils.pp_list ~delim:("{","}") Line.print ppf s
let fold f l a = List.fold_left (fun e a -> f a e) a l
let pp_s ppf s =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.print v Print.pp_type t
) ppf (VarMap.get s)
let pp_sl ppf l =
Utils.pp_list ~delim:("{","}") pp_s ppf l
type constr = Types.t * Types.t (* lower and
upper bounds *)
(* A comparison function between types that
is compatible with subtyping. If types are
not in a subtyping relation, use implementation
defined order
*)
let compare_type t1 t2 =
let inf12 = Types.subtype t1 t2 in
let inf21 = Types.subtype t2 t1 in
if inf12 && inf21 then 0
else if inf12 then -1 else if inf21 then 1 else
let c = Types.compare t1 t2 in
assert (c <> 0);
c
(* A line is a conjunction of constraints *)
module Line = struct
type t = constr VarMap.map
let singleton = VarMap.singleton
let is_empty = VarMap.is_empty
let length = VarMap.length
(* 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,
there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
*)
let subsumes map1 map2 =
List.for_all (fun (v,(i1, s1)) ->
try let i2, s2 = VarMap.assoc v map2 in
subtype i1 i2 && subtype s2 s1
with Not_found -> false
) (VarMap.get map1)
let print ppf map =
Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.print v Print.pp_type s
) ppf (VarMap.get map)
let compare map1 map2 =
VarMap.compare (fun (i1,s1) (i2,s2) ->
let c = compare_type i1 i2 in
if c == 0 then compare_type s1 s2
else c) map1 map2
let add v (inf, sup) map =
let new_i, new_s =
try
let old_i, old_s = VarMap.assoc v map in
cup old_i inf,
cap old_s sup
with
Not_found -> inf, sup
in
VarMap.replace v (new_i, new_s) map
let is_empty l = l == []
let join map1 map2 = VarMap.fold add map1 map2
let fold = VarMap.fold
let empty = VarMap.empty
let for_all f m = List.for_all (fun (k,v) -> f k v) (VarMap.get m)
end
(* Square union : *)
let union s1 s2 =
match s1, s2 with
[], _ -> s2
| _, [] -> s1
| _ ->
(* 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
- if e1 subsumes an element e2 of s2, add e1 to the
result and remove e2 from s2
- if an element e2 of s2 subsumes e1, add e2 to the
result and remove e2 from s2 (and discard e1)
once we are done for all e1, add the remaining elements from
s2 to the result.
*)
let append e1 s2 result =
let rec loop s2 accs2 =
match s2 with
[] -> accs2, e1::result
| e2 :: ss2 ->
if Line.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
else if Line.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
else loop ss2 (e2::accs2)
in
loop s2 []
in
let rec loop s1 s2 result =
match s1 with
[] -> List.rev_append s2 result
| e1 :: ss1 ->
let new_s2, new_result = append e1 s2 result in
loop ss1 new_s2 new_result
module ConstrSet =
struct
(* A set of constraint-sets is just a list of Lines,
that are pairwise "non-subsumable"
*)
type t = Line.t list
let elements t = t
let empty = []
let add m l =
let rec loop m l acc =
match l with
[] -> m :: acc
| mm :: ll ->
if Line.subsumes m mm then List.rev_append ll (m::acc)
else if Line.subsumes mm m then List.rev_append ll (mm::acc)
else loop m ll (mm::acc)
in
loop m l []
let unsat = empty
let sat = [ Line.empty ]
let is_unsat m = m == []
let is_sat m = match m with
[ l ] when Line.is_empty l -> true
| _ -> false
let print ppf s = Utils.pp_list ~delim:("{","}") Line.print ppf s
let fold f l a = List.fold_left (fun e a -> f a e) a l
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
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
- if e1 subsumes an element e2 of s2, add e1 to the
result and remove e2 from s2
- if an element e2 of s2 subsumes e1, add e2 to the
result and remove e2 from s2 (and discard e1)
once we are done for all e1, add the remaining elements from
s2 to the result.
*)
let append e1 s2 result =
let rec loop s2 accs2 =
match s2 with
[] -> accs2, e1::result
| e2 :: ss2 ->
if Line.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
else if Line.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
else loop ss2 (e2::accs2)
in
loop s1 s2 []
(* Square intersection *)
let inter delta s1 s2 =
loop s2 []
in
let rec loop s1 s2 result =
match s1 with
[] -> List.rev_append s2 result
| e1 :: ss1 ->
let new_s2, new_result = append e1 s2 result in
loop ss1 new_s2 new_result
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 Line.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).
*)
(* Perform the cartesian product. For each constraint m1 in s1,
m2 in s2, we add Line.join 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 ->
let merged = if Line.subsumes m1 m2 then m2
else if Line.subsumes m2 m1 then m1
else Line.inter delta m1 m2
else Line.join m1 m2
in
add merged acc2
)
s2 acc1) s1 []
let filter = List.filter
end
type s = S.t
type m = Line.t
type es = ES.t
type sigma = Types.t E.t
module SUB = SortedList.FiniteCofinite(struct
type t = Types.t E.t
let compare = E.compare compare
let equal = E.equal equal
let hash = Hashtbl.hash
let dump = E.pp
let check _ = ()
end)
type sl = sigma list
let singleton c =
let constr =
match c with
|Pos (v,s) -> Line.singleton v (empty,s)
|Neg (s,v) -> Line.singleton v (s,any)
in
S.singleton constr
let pp_s = S.pp
let pp_m = Line.print
let pp_e = E.pp
let pp_sl ppf ll = Utils.pp_list ~delim:("{","}") E.pp ppf ll
let singleton c =
let cstr = match c with
`pos (v, s) -> Line.singleton v (Types.empty, s)
| `neg (s, v) -> Line.singleton v (s, Types.any)
in
[ cstr ]
end
let sat = S.singleton Line.empty
let unsat = S.empty
let union = S.union
let prod delta = S.inter delta
let merge delta = Line.inter delta
end
let normatoms _ _ t = if Atoms.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normchars _ _ t = if Chars.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normints _ _ t = if Intervals.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normabstract _ _ t = if Abstracts.is_empty t then ConstrSet.sat else ConstrSet.unsat
let normatoms (t,_,_) = if Atoms.is_empty t then Constr.sat else Constr.unsat
let normchars (t,_,_) = if Chars.is_empty t then Constr.sat else Constr.unsat
let normints (t,_,_) = if Intervals.is_empty t then Constr.sat else Constr.unsat
let normabstract (t,_,_) = if Abstracts.is_empty t then Constr.sat else Constr.unsat
let single_aux constr (b,v,p,n) =
let aux f constr l =
List.fold_left (fun acc ->
function
|`Var a -> cap acc (f(var a))
|`Atm a -> cap acc (f(constr a))
) any l
let single (type a) (module V : VarType with type Atom.t = a) b v lpos lneg =
let aux dir l =
List.fold_left (fun acc va ->
cap acc (dir (
match va with
`Var v -> var v
| (`Atm _) as a -> V.(inj (atom a)))))
any l
in
let id = (fun x -> x) in
let t = cap (aux id constr p) (aux neg constr n) in
(* t = bigdisj ... alpha \in P --> alpha <= neg t *)
(* t = bigdisj ... alpha \in N --> t <= alpha *)
if b then (neg t) else t
let single_atoms = single_aux atom
let single_abstract = single_aux abstract
let single_chars = single_aux char
let single_ints = single_aux interval
let t = cap (aux id lpos) (aux neg lneg) in
if b then neg t else t
let single_times = single_aux (fun p -> VarTimes.(inj (atom (`Atm p))))
(* check if there exists a toplevel variable : fun (pos,neg) *)
let single_xml = single_aux (fun p -> VarXml.(inj (atom (`Atm p))))
let single_record = single_aux (fun p -> VarRec.(inj (atom (`Atm p))))
let single_arrow = single_aux (fun p -> VarArrow.(inj (atom (`Atm p))))
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
let toplevel (type a) (module V : VarType with type Atom.t = a)
delta norm_rec mem lpos lneg
=
let _compare delta v1 v2 =
let monov1 = Var.Set.mem delta v1 in
let monov2 = Var.Set.mem delta v2 in
......@@ -284,50 +229,57 @@ let toplevel delta single norm_rec mem p n =
else
if monov1 then 1 else -1
in
match (p,n) with
|([], (`Var x)::neg) ->
let t = single (false,x,[],neg) in
Constr.singleton (Neg (t, x))
let singleton c =
match c with
`neg (t, x) when Var.Set.mem delta x
&& not(subtype t (var x)) -> ConstrSet.unsat
| `pos (x, t) when Var.Set.mem delta x
&& not(subtype (var x) t) -> ConstrSet.unsat
|((`Var x)::pos,[]) ->
let t = single (true,x,pos,[]) in
Constr.singleton (Pos (x,t))
| _ -> ConstrSet.singleton c
in
match lpos, lneg with
[], (`Var x)::neg ->
let t = single (module V) false x [] neg in
singleton (`neg (t, x))
| (`Var x)::pos,[] ->
let t = single (module V) true x pos [] in
singleton (`pos (x,t))
|((`Var x)::pos, (`Var y)::neg) ->
| (`Var x)::pos, (`Var y)::neg ->
if _compare delta x y < 0 then
let t = single (true,x,pos,n) in
Constr.singleton (Pos (x,t))
let t = single (module V) true x pos lneg in
singleton (`pos (x,t))
else
let t = single (false,y,p,neg) in
Constr.singleton (Neg (t, y))
let t = single (module V) false y lpos neg in
singleton (`neg (t, y))
|([`Atm a], (`Var x)::neg) ->
let t = single (false,x,p,neg) in
Constr.singleton (Neg (t,x))
| [`Atm _ ], (`Var x)::neg ->
let t = single (module V) false x lpos neg in
singleton (`neg (t, x))
|([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false
| [ `Atm t ], [ ] -> norm_rec delta mem t
| __ -> assert false
let big_prod delta f acc l =
let big_prod f acc l =
List.fold_left (fun acc (pos,neg) ->
(* if Constr.S.is_empty acc then acc else *)
Constr.prod delta acc (f pos neg)
ConstrSet.inter acc (f pos neg)
) acc l
module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))
let memo_norm = NormMemoHash.create 17
let () = Format.pp_set_margin Format.err_formatter 100
let rec norm (t,delta,mem) =
let rec norm delta mem t =
DEBUG normrec (
Format.eprintf
" @[Entering norm rec(%a):@\n" Print.pp_type t);
let res =
try
(* If we find it in the global hashtable, we are finished *)
(* If we find it in the global hashtable,
we are finished *)
let res = NormMemoHash.find memo_norm (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in global table @]@\n");
......@@ -338,7 +290,7 @@ let rec norm (t,delta,mem) =
let finished, cst = NormMemoHash.find mem (t, delta) in
DEBUG normrec (Format.eprintf
"@[ - Result found in local table, finished = %b @]@\n" finished);
if finished then cst else Constr.sat
if finished then cst else ConstrSet.sat
with
Not_found ->
begin
......@@ -346,59 +298,54 @@ let rec norm (t,delta,mem) =
(* base cases *)
if is_empty t then begin
DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
Constr.sat
ConstrSet.sat
end else if no_var t then begin
DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
Constr.unsat
ConstrSet.unsat
end else if is_var t then begin
let (v,p) = Variable.extract t in
if Var.Set.mem delta v then begin
DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
Constr.unsat (* if it is monomorphic, unsat *)
ConstrSet.unsat (* if it is monomorphic, unsat *)
end else begin
DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
Constr.singleton s
(* otherwise, create a single constraint according to its polarity *)
let s = if p then (`pos (v,empty)) else (`neg (any,v)) in
ConstrSet.singleton s
end
end else begin (* type is not empty and is not a variable *)
DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
let mem = NormMemoHash.add mem (t,delta) (false, Constr.sat); mem in
let mem = NormMemoHash.add mem (t,delta) (false, ConstrSet.sat); mem in
let t = Iter.simplify t in
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 Constr.sat VarAtoms.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_chars normchars acc VarChars.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_ints normints acc VarIntervals.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_times normpair acc VarTimes.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_xml normpair acc VarXml.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_arrow normarrow acc VarArrow.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" Constr.pp_s acc);
let acc = aux single_abstract normabstract acc VarAbstracts.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" Constr.pp_s acc);
(* XXX normrec is not tested at all !!! *)
let acc = aux single_record normrec acc VarRec.(get (proj t)) in
DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" Constr.pp_s acc);
let acc = (* Simplify the constraints on that type *)
Constr.S.filter
(fun m -> Constr.Line.for_all (fun v (s, t) ->
if Var.Set.mem delta v then
(* constraint on a monomorphic variables must be trivial *)
let x = var v in subtype s x && subtype x t
else true (*
subtype s t || (non_empty (cap s t)) *)
) m)
acc
let aux (type a) (module V : VarType with type Atom.t = a)
norm_constr acc t
=
big_prod (toplevel
(module V)