Commit 46a5262a authored by Pietro Abate's avatar Pietro Abate

Revert "Make fresh variables really fresh"

This reverts commit c9ad3e5c.

Conflicts:
	types/var.ml
	typing/typer.ml
parent f9a38dc0
......@@ -689,8 +689,7 @@ module Witness = struct
~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
~atom:f
let rec node_has n =
function
let rec node_has n = function
| WXml (_,_,s) | WPair (_,_,s) | WFun (_,s) | WRecord (_,_,s) as w ->
if NodeSet.mem n s.wnodes_in then true
else if NodeSet.mem n s.wnodes_out then false
......@@ -702,8 +701,7 @@ module Witness = struct
(* type_has checks if a witness is contained in the union of
* the leafs of a bdd, ignoring all variables. *)
and type_has t =
function
and type_has t = function
| WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints)
| WChar c -> Chars.contains c (BoolChars.leafconj t.chars)
| WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms)
......@@ -807,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;
......@@ -3115,6 +3114,15 @@ module Tallying = struct
type m = M.t
type es = ES.t
type sigma = Descr.s E.t
module SUB = SortedList.FiniteCofinite(struct
type t = Descr.s 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 =
......@@ -3217,7 +3225,7 @@ module Tallying = struct
let rec norm (t,delta,mem) =
(* if we already evaluated it, it is sat *)
let res =
let res =
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 *)
......@@ -3251,7 +3259,7 @@ module Tallying = struct
in
res
end
in
in
(* Format.printf "Normalizing %a yields %a\n%!" Print.pp_type t CS.pp_s res; *) res
(* (t1,t2) = intersection of all (fst pos,snd pos) \in P
......
......@@ -7,29 +7,14 @@ module V = struct
let hash x = Hashtbl.hash (x.id,x.fr)
let check _ = ()
let id x = Ident.U.get_str x.id
let cache = Hashtbl.create 17
let is_fresh x = x.fr > 0
let fresh v =
try
let w = Hashtbl.find cache (id v) in
let w = { w with fr = w.fr + 1 } in
Hashtbl.replace cache (id w) w;
w
with Not_found ->
assert false
let fresh v = { v with fr = v.fr + 1 }
let mk id =
try Hashtbl.find cache id
with Not_found -> begin
let v = { id = Ident.U.mk id; fr = 0 } in
Hashtbl.add cache id v;
v
end
let mk id = { id = Ident.U.mk id; fr = 0 }
let id x = Ident.U.get_str x.id
let pp ppf x = Format.fprintf ppf "'%a" Ident.U.print x.id
(* let pp ppf x = dump ppf x *)
let pp ppf x = dump ppf x
end
include V
......
......@@ -395,8 +395,8 @@ module IType = struct
let l = ref [] in
for i=0 to (Array.length pargs) - 1 do
try
let tt = typ ~err:(fun s -> Error s) (derecurs env a.(i)) in
l := (pargs.(i), tt)::!l
let err s = Error s in
l := (pargs.(i), typ ~err (derecurs env a.(i)))::!l
with
|Error s -> raise_loc_generic loc s
|_ -> assert false
......@@ -469,9 +469,9 @@ module IType = struct
(U.to_string v)
);
let al =
let a = Array.make (List.length pl) (Var.mk "dummy")in
(* XXX here I use pervasive.compare instead of string compare *)
List.iteri (fun i v -> a.(i) <- (List.assoc (U.to_string v) vars)) pl;
let a = Array.make (List.length pl) (Var.mk "dummy") in
(* List.iteri (fun i v -> a.(i) <- (List.assoc (U.to_string v) vars)) pl; *)
List.iteri (fun i v -> a.(i) <- Var.mk (Ident.U.to_string v)) pl;
a
in
(v',t,al)
......
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