Commit 0a8cd35e authored by Pietro Abate's avatar Pietro Abate
Browse files

Add delta to Types.Tallying.{norm,merge}

- delta is not yet used to do anything meaningful
- remove optional argument ?fresh from Var.mk (legacy not used)
- print -> pp,printf refactoring
parent 727e0b21
......@@ -222,7 +222,7 @@ let test_norm =
(Printf.sprintf " %s \\ %s" s t) >:: (fun _ ->
let s = parse_typ s in
let t = parse_typ t in
let result = Tallying.norm (diff s t) in
let result = Tallying.norm Var.Set.empty (diff s t) in
let elem s = MSet.of_list (Tallying.CS.S.elements s) in
MSet.assert_equal (elem expected) (elem result)
)
......@@ -264,7 +264,7 @@ let test_merge =
let result =
try
Tallying.CS.S.fold (fun c acc ->
Tallying.CS.union (Tallying.merge c) acc
Tallying.CS.union (Tallying.merge Var.Set.empty c) acc
) s Tallying.CS.S.empty
with Tallying.UnSatConstr _ -> Tallying.CS.unsat
in
......
......@@ -151,17 +151,16 @@ module TLV = struct
else if p1 then 1 else -1
else c
end)
let print sep ppf s =
let aux1 ppf = function
|(v,true) -> Format.fprintf ppf "%a" Var.pp v
|(v,false) -> Format.fprintf ppf "~ %a" Var.pp v
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
let rec aux ppf = function
|[] -> ()
|[h] -> aux1 ppf h
|h::l -> Format.fprintf ppf "%a %s %a" aux1 h sep aux l
in
aux ppf (elements s)
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
......@@ -195,10 +194,10 @@ module TLV = struct
let has_toplevel t = Set.cardinal t.tlv > 0
let print ppf x = Set.print ";" ppf x.tlv
let dump ppf x =
Format.fprintf ppf "<fv = {%a} ; tlv = {%a}>"
Var.Set.pp x.fv (Set.print ";") x.tlv
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
......@@ -2620,7 +2619,7 @@ struct
try Hashtbl.find h d
with Not_found -> begin
let id = Printf.sprintf "_%s_%d" (Var.id d) !idx in
let x = var (Var.mk ~fresh:false ~repr:(Var.id d) id) in
let x = var (Var.mk ~repr:(Var.id d) id) in
incr idx;
Hashtbl.add h d x ;
x
......@@ -2668,7 +2667,7 @@ struct
(* polarity conflict, replace the binding by a new, pretty-printed variable *)
if ((td == t_emp) && not pos) || ((td == t_any) && pos) then begin
let id = pretty_name !idx "" in
let x = var (Var.mk ~fresh:false id) in
let x = var (Var.mk id) in
incr idx;
Hashtbl.replace vars d x ;
end
......@@ -2945,9 +2944,9 @@ module Tallying = struct
let merge = M.inter
end
let normatoms (t,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
let normchars (t,_,_) = if Chars.is_empty t then CS.sat else CS.unsat
let normints (t,_,_) = if Intervals.is_empty t then CS.sat else CS.unsat
let single_aux constr (b,v,p,n) =
let aux f constr l =
......@@ -2980,7 +2979,7 @@ 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 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 (Neg (t,`Var x))
......@@ -3001,7 +3000,7 @@ module Tallying = struct
let t = single (false,x,p,neg) in
CS.singleton (Neg (t,`Var x))
|([`Atm t], []) -> norm_rec (t,mem)
|([`Atm t], []) -> norm_rec (t,delta,mem)
|_,_ -> assert false
let big_prod f acc l =
......@@ -3011,7 +3010,7 @@ module Tallying = struct
) acc l
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,mem) =
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; *)
......@@ -3027,7 +3026,7 @@ module Tallying = struct
else if no_var t then CS.unsat
else begin
let mem = DescrSet.add t mem in
let aux single norm_aux acc l = big_prod (toplevel single norm_aux mem) acc l in
let aux single norm_aux acc l = big_prod (toplevel delta single norm_aux mem) acc l in
let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
......@@ -3051,15 +3050,15 @@ module Tallying = struct
* prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
* ([t2\s2] v prod'(t1,t2\s2,n))
* *)
and normpair (t,mem) =
and normpair (t,delta,mem) =
let norm_prod pos neg =
let rec aux t1 t2 = function
|[] -> CS.unsat
|(s1,s2) :: rest -> begin
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
let con1 = norm (z1, mem) in
let con2 = norm (z2, mem) in
let con1 = norm (z1, delta, mem) in
let con2 = norm (z2, delta, mem) in
let con10 = aux z1 t2 rest in
let con20 = aux t1 z2 rest in
let con11 = CS.union con1 con10 in
......@@ -3069,14 +3068,14 @@ module Tallying = struct
in
(* cap_product return the intersection of all (fst pos,snd pos) *)
let (t1,t2) = cap_product any any pos in
let con1 = norm (t1, mem) in
let con2 = norm (t2, mem) in
let con1 = norm (t1, delta, mem) in
let con2 = norm (t2, delta, mem) in
let con0 = aux t1 t2 neg in
CS.union (CS.union con1 con2) con0
in
big_prod norm_prod CS.sat (Pair.get t)
and normrec (t,mem) =
and normrec (t,delta,mem) =
let norm_rec ((oleft,left),rights) =
let rec aux accus seen = function
|[] -> CS.sat
......@@ -3086,11 +3085,11 @@ module Tallying = struct
snd (Array.fold_left (fun (i,acc) t ->
let di = diff accus.(i) t in
let accus' = Array.copy accus in accus'.(i) <- di ;
(i+1,CS.prod acc (CS.prod (norm (di,mem)) (aux accus' [] right)))
(i+1,CS.prod acc (CS.prod (norm (di,delta,mem)) (aux accus' [] right)))
) (0,CS.sat) field
)
in
let c = Array.fold_left (fun acc t -> CS.union (norm (t,mem)) acc) CS.sat left in
let c = Array.fold_left (fun acc t -> CS.union (norm (t,delta,mem)) acc) CS.sat left in
CS.prod (aux left [] rights) c
in
List.fold_left (fun acc (_,p,n) ->
......@@ -3110,12 +3109,12 @@ module Tallying = struct
P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
*)
and normarrow (t,mem) =
and normarrow (t,delta,mem) =
let rec norm_arrow pos neg =
match neg with
|[] -> CS.unsat
|(t1,t2) :: n ->
let con1 = norm (descr t1, mem) in (* [t1] *)
let con1 = norm (descr t1, delta, mem) in (* [t1] *)
let con2 = aux (descr t1) (diff any (descr t2)) pos in
let con0 = norm_arrow pos n in
CS.union (CS.union con1 con2) con0
......@@ -3124,8 +3123,8 @@ module Tallying = struct
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, mem) in (* [t1 \ s1] *)
let con2 = norm (acc1, mem) in (* [(Any \ t2) ^ s2] *)
let con1 = norm (t1s1, delta, mem) in (* [t1 \ s1] *)
let con2 = norm (acc1, delta, mem) in (* [(Any \ t2) ^ s2] *)
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.union con1 con10 in
......@@ -3135,16 +3134,18 @@ module Tallying = struct
big_prod norm_arrow CS.sat (Pair.get t)
let memo_norm = DescrHash.create 17
let norm t =
(* XXX here I hash over a set . this might lead to a
* conflict in the hash function if the set is too large *)
let norm delta t =
try DescrHash.find memo_norm t
with Not_found -> begin
let res = norm (t,DescrSet.empty) in
let res = norm (t,delta,DescrSet.empty) in
DescrHash.add memo_norm t res; res
end
exception UnSatConstr of string
let rec merge (m, mem) =
let rec merge (m,delta,mem) =
let res =
CS.M.fold (fun v (inf, sup) acc ->
(* no need to add new constraints *)
......@@ -3155,16 +3156,16 @@ module Tallying = struct
else begin
DescrHash.add mem x ();
let n =
let n = norm x in if CS.S.is_empty n then raise (UnSatConstr "merge2") else n
let n = norm delta x in if CS.S.is_empty n then raise (UnSatConstr "merge2") else n
in
let c1 = CS.prod (CS.S.singleton m) n in
let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1, mem))) c1 CS.S.empty in
let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1,delta,mem))) c1 CS.S.empty in
CS.union c2 acc
end) m CS.S.empty
in
if CS.S.is_empty res then CS.S.singleton m else res
let merge m = merge (m,DescrHash.create 17)
let merge delta m = merge (m,delta,DescrHash.create 17)
(* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
let solve s =
......@@ -3202,7 +3203,7 @@ module Tallying = struct
if CS.E.is_empty e then sol
else begin
let (alpha,t) = CS.E.min_binding e in
(* Format.printf "Unify -> %a = %a\n" Var.pp alpha Print.print t; *)
(* Format.printf "Unify -> %a = %a\n" Var.pp alpha Print.pp_type t; *)
let e1 = CS.E.remove alpha e in
(* Format.printf "e1 = %a\n" CS.print_e e1; *)
(* remove from E \ { (alpha,t) } every occurrences of alpha
......@@ -3210,7 +3211,11 @@ module Tallying = struct
(* substituterec remove also all previously introduced fresh variables *)
let x = Positive.substituterec t alpha in
(* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
let es = CS.E.fold (fun beta s acc -> CS.E.add beta (Positive.substitute s (alpha,x)) acc) e1 CS.E.empty in
let es =
CS.E.fold (fun beta s acc ->
CS.E.add beta (Positive.substitute s (alpha,x)) acc
) e1 CS.E.empty
in
(* Format.printf "es = %a\n" CS.print_e es; *)
aux ((CS.E.add alpha x sol)) es
end
......@@ -3229,13 +3234,13 @@ module Tallying = struct
let d = diff s t in
if is_empty d then CS.sat
else if no_var d then CS.unsat
else CS.prod acc (norm d)
else CS.prod acc (norm delta d)
) CS.sat l
in
if Pervasives.(n = CS.unsat) then raise Step1Fail else
let m =
CS.S.fold (fun c acc ->
try CS.ES.union (solve (merge c)) acc
try CS.ES.union (solve (merge delta c)) acc
with UnSatConstr _ -> acc
) n CS.ES.empty
in
......@@ -3245,7 +3250,7 @@ module Tallying = struct
CS.ES.fold (fun e acc ->
let si = unify e in
(* XXX maybe we can eliminate solution earlier. Is it safe to do it here ? *)
(* si is a solution only if (dom(si) /\ delta = emptyset) *)
(* it is a solution only if (dom(si) /\ delta = emptyset) *)
if Var.Set.is_empty (Var.Set.inter (dom(si)) delta) then
CS.ES.add si acc
else acc
......
......@@ -419,8 +419,8 @@ module Tallying : sig
val prod : s -> s -> s
end
val norm : t -> CS.s
val merge : CS.m -> CS.s
val norm : Var.Set.t -> t -> CS.s
val merge : Var.Set.t -> CS.m -> CS.s
val solve : CS.s -> CS.es
val unify : CS.sigma -> CS.sigma
......
module V = struct
type t = { fresh : bool; id : string; repr : string }
type t = { id : string; repr : string }
let dump ppf t =
let r = if t.repr = t.id then "" else Format.sprintf ";repr=%s" t.repr in
Format.fprintf ppf "{id=%s;fresh=%b%s}" t.id t.fresh r
Format.fprintf ppf "{id=%s;%s}" t.id r
let compare x y = Pervasives.compare x.id y.id
let equal x y = Pervasives.compare x.id y.id = 0
let hash x = Hashtbl.hash x.id
let check _ = ()
let make_id ?(fresh=false) ?repr id =
let make_id ?repr id =
match repr with
|None -> { id = id ; fresh = fresh ; repr = id }
|Some r -> { id = id ; fresh = fresh ; repr = r }
|None -> { id = id ; repr = id }
|Some r -> { id = id ; repr = r }
end
type var = [ `Var of V.t ]
type t = var
let id (`Var x) = x.V.id
let dump ppf (`Var x) = Format.fprintf ppf "%a" V.dump x
let pp ppf (`Var x) = Format.fprintf ppf "'%s" x.V.repr
let compare (`Var x) (`Var y) = V.compare x y
......@@ -24,31 +26,21 @@ let equal v1 v2 = (compare v1 v2) = 0
let hash (`Var x) = V.hash x
let check _ = ()
let mk ?fresh ?repr id = `Var (V.make_id ?fresh ?repr id)
let mk ?repr id = `Var (V.make_id ?repr id)
let fresh : ?pre: string -> unit -> [> var ] =
let counter = ref 0 in
fun ?(pre="_fresh_") -> fun _ ->
let id = (Printf.sprintf "%s%d" pre !counter) in
let v = mk ~fresh:true id in
let v = mk id in
incr counter;
v
;;
let id (`Var x) = x.V.id
let is_fresh (`Var x) = x.V.fresh
module Set = struct
include Set.Make(struct type t = var let compare = compare end)
let aux_print sep printer ppf s =
let rec aux ppf = function
|[] -> ()
|[h] -> printer ppf h
|h::l -> Format.fprintf ppf "%a %s %a" printer h sep aux l
in
aux ppf (elements s)
let dump ppf s = aux_print ";" dump ppf s
let pp ppf s = aux_print ";" pp ppf s
let dump ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") dump ppf (elements s)
let pp ppf s = Utils.pp_list ~sep:";" ~delim:("{","}") pp ppf (elements s)
let printf = pp Format.std_formatter
let is_empty s = equal s empty
let from_list l = List.fold_left (fun acc x -> add x acc) empty l
end
......
module V : sig
include Custom.T
val make_id : ?fresh:bool -> ?repr:string -> string -> t
val make_id : ?repr:string -> string -> t
end
type var = [ `Var of V.t ]
......@@ -8,15 +8,15 @@ type var = [ `Var of V.t ]
include Custom.T with type t = var
val pp : Format.formatter -> var -> unit
val mk : ?fresh:bool -> ?repr:string -> string -> var
val mk : ?repr:string -> string -> var
val fresh : ?pre:string -> unit -> var
val id : var -> string
val is_fresh : var -> bool
module Set : sig
include Set.S with type elt = var
val dump : Format.formatter -> t -> unit
val pp : Format.formatter -> t -> unit
val printf : t -> unit
val is_empty : t -> bool
val from_list : elt list -> t
end
......
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