Commit bf2f41db authored by Pietro Abate's avatar Pietro Abate
Browse files

Remove commented/wrong code and variance annotations

parent d0b41871
......@@ -1651,34 +1651,7 @@ struct
|l -> add (Intersection (alloc (List.rev l)))
) (get bdd)
in
(*
(* variables are printed if displayvars OR if x is not a toplevel variable *)
let prepare_boolvar displayvars displayatoms get is_full print tlv bdd =
List.iter (fun (p,n) ->
let pp pol l =
List.fold_left (fun acc -> function
|(`Var v) as x ->
if displayvars || not(TLV.mem (x,pol) tlv) then
(Atomic (fun ppf -> Format.fprintf ppf "%s%a" (if pol then "" else "~ ") Var.print x))::acc
else acc
|`Atm bdd when is_full bdd ->
if not(displayvars) then
(print bdd) @ acc
else acc
|`Atm bdd ->
if pol then
if displayatoms then (print bdd) @ acc else acc
else
assert false
) [] l
in
match (pp p)@(pp n) with
|[] -> ()
|l -> add (Intersection (alloc (List.rev l)))
) (get bdd)
in
*)
if (non_empty seq) then add (Regexp (decompile seq));
let displayatoms = true in
......@@ -1999,8 +1972,10 @@ struct
Print.assign_name t;
t;;
let trace msg = (* output_string stderr (msg ^ "\n");
flush stderr *) ();;
let trace msg =
(* output_string stderr (msg ^ "\n");
flush stderr *)
();;
let print_to_string f =
let b = Buffer.create 1024 in
......@@ -2466,10 +2441,8 @@ struct
let decompose_aux ?noderec constr l =
cup (List.map (fun (p,n) -> (aux_bdd ?noderec constr (p,n))) l)
in
try
DescrHash.find memo_decompose t
(*begin match DescrHash.find memo_decompose t with | None -> forward () | Some s -> s end *)
with Not_found -> begin
try DescrHash.find memo_decompose t with Not_found -> begin
let node_s = forward () in
DescrHash.add memo_decompose t node_s;
let s =
......@@ -2538,13 +2511,8 @@ struct
* position with any *)
let substituterec t alpha =
let subst x d =
if Var.equal d alpha then x else
(*if Var.is_fresh d then begin
match Var.variance d with
| `Covariant -> ty empty
| `ContraVariant -> ty any
| _ -> var d
end else*) var d
if Var.equal d alpha then x
else var d
in
if no_var t then t
else begin
......@@ -2568,7 +2536,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 ~variance:(Var.variance d) id) in
let x = var (Var.mk ~fresh:false id) in
incr idx;
Hashtbl.add h d x ;
x
......@@ -2577,7 +2545,6 @@ struct
let new_t = substitute_aux (decompose t) (subst h) in
descr(solve new_t)
(* Kim: we cannot use the variance annotation of variables to simplify them,
since variables are shared amongst types. If we have two types
A -> A and (A,A) (produced by the algorithm) then we can still simplify the
......@@ -2590,9 +2557,10 @@ struct
| (b1, v1) :: ll -> (b1==b && v1==v) || (memq_pair key ll)
in
let memo = ref [] in
let rec aux pos v = (* we memoize based on the pair (pos, v),
since v can occur both positively and negatively.
and we want to manage the variables differently in both cases *)
(* we memoize based on the pair (pos, v), since v can occur both
* positively and negatively. and we want to manage the variables
* differently in both cases *)
let rec aux pos v =
if not (memq_pair (pos,v) !memo) then
let () = memo := (pos,v) :: !memo in
match v.def with
......@@ -2612,7 +2580,6 @@ struct
let rcontra = Var.Set.diff !contra !cova in
rcova, rcontra
let clean_variables t =
if no_var t then t
else begin
......@@ -2640,7 +2607,7 @@ struct
try Hashtbl.find h d
with Not_found -> begin
let id = pretty_name !idx "" in
let x = var (Var.mk ~fresh:false ~variance:(Var.variance d) id) in
let x = var (Var.mk ~fresh:false id) in
incr idx;
Hashtbl.add h d x ;
x
......@@ -2727,7 +2694,8 @@ module Tallying = struct
VarMap.for_all (fun v (i1, s1) ->
try let i2, s2 = VarMap.find v map2 in
subtype i1 i2 && subtype s2 s1
with Not_found -> false) map1
with Not_found -> false
) map1
let print ppf map = print_lst (fun ppf (v, (i,s)) ->
Format.fprintf ppf "%a <= %a <= %a" Print.print i
......@@ -2962,29 +2930,6 @@ module Tallying = struct
CS.prod acc (f pos neg)
) acc l
(* Kim: these three functions are used in the (commented) reference
implementation of norm_arrow below *)
let rec remove e = function [] -> []
| x :: ll -> if e == x then ll else x :: (remove e ll)
let rec rev_map_concat f l1 l2 =
match l1 with
[] -> l2
| e :: ll1 -> rev_map_concat f ll1 ((f e) :: l2)
let partition l =
let rec loop l rpart =
match l with
[] -> [ [],rpart ]
| e :: ll ->
let parts = loop ll (e::rpart) in
rev_map_concat (fun (l1,l2) -> (e::l1,remove e l2)) parts parts
in loop l []
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,mem) =
(* if we already evaluated it, it is sat *)
......@@ -3108,50 +3053,6 @@ module Tallying = struct
CS.prod con11 con22
in
big_prod norm_arrow CS.sat (Pair.get t)
(* Kim: REFERENCE norm_arrow from the paper
bad because it materialises all subsets of P and then iterates
let norm_arrow pos neg_ =
let part = partition pos in
List.fold_left (fun acc_n (sn, tn) ->
CS.union acc_n (
List.fold_left (fun acc (pp', copp') ->
CS.prod acc
(CS.union
(norm (List.fold_left (fun acc (sp, _) -> cap (neg (descr sp)) acc) (descr sn) pp', mem))
(norm (List.fold_left (fun acc (_, tp) -> cap (diff (descr tp) (descr tn)) acc) any copp', mem))
)
) CS.sat part)
) CS.unsat neg_
in
big_prod norm_arrow CS.sat (Pair.get t)
*)
(*
and normarrow (t,mem) =
let rec norm_arrow pos neg =
match neg with
|[] -> CS.unsat
|(t1,t2)::n ->
let con1 = norm (descr t1, mem) in
let con2 = aux (descr t1) any (descr t2) pos in
let con0 = norm_arrow pos n in
CS.union (CS.union con1 con2) con0
and aux t1 acc t2 p =
match p with
|[] -> CS.unsat
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, mem) in
let con2 = norm (diff acc1 t2, mem) in
let con10 = aux t1s1 acc t2 p in
let con20 = aux t1 acc1 t2 p in
let con11 = CS.union con1 con10 in
let con22 = CS.union con2 con20 in
CS.prod con11 con22
in
big_prod norm_arrow CS.sat (Pair.get t)
*)
let memo_norm = DescrHash.create 17
let norm t =
......@@ -3166,9 +3067,8 @@ module Tallying = struct
let rec merge (m, mem) =
let res =
CS.M.fold (fun v (inf, sup) acc ->
if subtype inf sup
then (* no need to add new constraints *)
acc
(* no need to add new constraints *)
if subtype inf sup then acc
else
let x = diff inf sup in
if DescrHash.mem mem x then acc
......@@ -3192,54 +3092,12 @@ module Tallying = struct
(* we cannot solve twice the same variable *)
if CS.E.mem alpha acc then assert false else
let pre = Printf.sprintf "_fr_%s_" (Var.id alpha) in
let b = var (Var.fresh ~pre ~variance:(Var.variance alpha) ()) in
(* Kim: I don't think we need all this, the general case handles everything.
(* 0 <= alpha <= 1 --> alpha = fresh *)
if equal s empty && equal t any then
CS.E.add alpha b acc
(* s <= alpha <= 0 --> alpha = empty *)
else if equal t empty then CS.E.add alpha empty acc
(* 1 <= alpha <= t --> alpha = t *)
else if equal s any then CS.E.add alpha t acc
(* s <= alpha <= 1 --> alpha = ( s v fresh ) *)
else if equal t any then
CS.E.add alpha (cup s b) acc
(* 0 <= alpha <= t --> alpha = ( t ^ fresh ) *)
else if equal s empty then
CS.E.add alpha (cap b t) acc
else
*)
let b = var (Var.fresh ~pre ()) in
(* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
CS.E.add alpha (cap (cup s b) t) acc
in
let aux1 m =
let cache = Hashtbl.create (CS.M.cardinal m) in
(* CS.M.fold (fun (b,alpha) s acc ->
if Hashtbl.mem cache alpha then acc else begin
Hashtbl.add cache alpha ();
try
let t = CS.M.find (not b,alpha) m in
(* if t containts only a toplevel variable and nothing else
* means that the constraint is of the form (alpha,beta). *)
if is_var t then begin
let (beta,_) = TLV.max t.toplvars in
let acc1 = aux beta (empty,any) acc in
(* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
if b then aux alpha (empty,t) acc1
else aux alpha (t,any) acc1
end else
(* alpha = ( s v fresh) ^ t *)
if b then aux alpha (t,s) acc else aux alpha (s,t) acc;
with Not_found ->
(* upper bond or lower bound is missing, we replace it
* with a constratint of the form empty <= alpha <= s | s <= alpha <= any *)
if b then aux alpha (empty,s) acc else aux alpha (s,any) acc
end
) m CS.E.empty
*)
CS.M.fold (fun alpha (s,t) acc ->
if Hashtbl.mem cache alpha then acc else begin
Hashtbl.add cache alpha ();
......@@ -3321,7 +3179,7 @@ let apply_raw s t =
*)
(*DescrHash.clear Tallying.memo_norm; *)
let q = Queue.create () in
let gamma = var (Var.mk ~variance:`Covariant "Gamma") in
let gamma = var (Var.mk "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
try (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]) , (acc1, acc2)
......@@ -3337,8 +3195,9 @@ let apply_raw s t =
Queue.add (aux (0,lazy(s)) (1,lazy(Positive.substitutefree t)) s t) q;
let result = ref ([],(any,any)) in
let counter = ref 0 in
while (* I removed the condition to stop at the first solution since, at least for map even
it is only partial *) not(Queue.is_empty q) do
(* I removed the condition to stop at the first solution since,
at least for map even it is only partial *)
while not(Queue.is_empty q) do
try
incr counter; (* don't know about termination... *)
if (!counter mod 10 == 0) then Format.printf "Warning: %i iterations during application typing\n%!" !counter;
......@@ -3347,7 +3206,6 @@ let apply_raw s t =
done;
!result
let apply_full s t =
let subst_lst,(s,t) = apply_raw s t in
let ss =
......@@ -3365,7 +3223,8 @@ let apply_full s t =
let ss = Positive.clean_type ss in
let tt = Positive.clean_type tt in
let res = Positive.clean_type res in
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n\n%!" Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res
Format.printf "sl = %a\nfunction type = %a\nargument type = %a\nresult type = %a\n\n%!"
Tallying.CS.pp_sl subst_lst Print.print ss Print.print tt Print.print res; res
let apply s t = fst (apply_raw s t)
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