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

Seal the internal representation of constraint sets.

parent 7b5be392
open Types
open Debug
let cap_t d t = cap d (descr t)
let cap_product any_left any_right l =
......@@ -34,7 +35,21 @@ let compare_type t1 t2 =
(* A line is a conjunction of constraints *)
module Line = struct
module Line : sig
type t
val empty : t
val singleton : Var.t -> constr -> t
val is_empty : t -> bool
val length : t -> int
val subsumes : t -> t -> bool
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val add : Var.t -> constr -> t -> t
val join : t -> t -> t
val fold : (Var.t -> constr -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (Var.t -> constr -> bool) -> t -> bool
end
= struct
type t = constr Var.Map.map
......@@ -84,7 +99,23 @@ module Line = struct
let for_all f m = List.for_all (fun (k,v) -> f k v) (Var.Map.get m)
end
module ConstrSet =
module ConstrSet :
sig
type t
val singleton : Line.t -> t
val single_var : Var.t -> constr -> t
val elements : t -> Line.t list
val unsat : t
val sat : t
val is_unsat : t -> bool
val is_sat : t -> bool
val print : Format.formatter -> t -> unit
val fold : (Line.t -> 'a -> 'a) -> t -> 'a -> 'a
val union : t -> t -> t
val inter : t -> t -> t
val add : Line.t -> t -> t
end
=
struct
(* A set of constraint-sets is just a list of Lines,
......@@ -182,7 +213,8 @@ struct
s2 acc1) s1 []
let filter = List.filter
let singleton v cs = [ (Line.singleton v cs) ]
let single_var v cs = [ (Line.singleton v cs) ]
let singleton e = [ e ]
end
......@@ -221,7 +253,7 @@ let toplevel
if subtype t vx && subtype vx s then
ConstrSet.sat
else ConstrSet.unsat
else ConstrSet.singleton x cst
else ConstrSet.single_var x cst
in
let var_compare v1 v2 =
let mono1 = Var.Set.mem delta v1 in
......@@ -315,7 +347,7 @@ let rec norm delta mem t =
end else begin
_DEBUG "normrec" "@[ - Polymorphic var case @]@\n";
(* otherwise, create a single constraint according to its polarity *)
ConstrSet.singleton v (if p then (empty, empty) else (any, any))
ConstrSet.single_var v (if p then (empty, empty) else (any, any))
end
end else begin (* type is not empty and is not a variable *)
_DEBUG "normrec" "@[ - Inductive case:@]@\n%!";
......@@ -541,18 +573,18 @@ let rec merge delta cache m =
let cache, _ = Cache.find ignore x cache in
let n = norm delta x in
if ConstrSet.is_unsat n then raise (UnSatConstr "merge2");
let c1 = ConstrSet.inter (ConstrSet.(add m empty)) n
let c1 = ConstrSet.inter (ConstrSet.singleton m) n
in
let c2 =
ConstrSet.fold
(fun m1 acc ->
ConstrSet.union acc (merge delta cache m1))
c1 ConstrSet.empty
c1 ConstrSet.unsat
in
ConstrSet.union c2 acc
) m ConstrSet.empty
) m ConstrSet.unsat
in
if ConstrSet.is_unsat res then ConstrSet.(add m empty)
if ConstrSet.is_unsat res then ConstrSet.singleton m
else res
let merge delta m = merge delta Cache.emp m
......
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