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

Comment some debug statements.

parent ac1f6ab4
......@@ -2954,8 +2954,8 @@ module Tallying = struct
(* norm generates a constraint set for the costraint t <= 0 *)
let rec norm (t,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;
if DescrSet.mem t mem || is_empty t then begin
(*Format.printf "Sat for type %a\n%!" Print.print t; *)
CS.sat end else begin
(*
if is_empty t then CS.sat
......@@ -3000,28 +3000,19 @@ module Tallying = struct
let z1 = diff t1 (descr s1) in
let z2 = diff t2 (descr s2) in
let con1 = norm (z1, mem) in
Format.printf "*1norm[%a \\ %a] = %a\n" Print.print t1 Print.print (descr s1) CS.pp_s con1;
let con2 = norm (z2, mem) in
Format.printf "*2norm[%a \\ %a] = %a\n" Print.print t2 Print.print (descr s2) CS.pp_s con2;
let con10 = aux z1 t2 rest in
Format.printf "norm[con10] = %a\n" CS.pp_s con10;
let con20 = aux t1 z2 rest in
Format.printf "norm[con20] = %a\n" CS.pp_s con20;
let con11 = CS.union con1 con10 in
Format.printf "norm[con11] = %a\n" CS.pp_s con11;
let con22 = CS.union con2 con20 in
Format.printf "norm[con22] = %a\n" CS.pp_s con22;
CS.prod con11 con22
end
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
Format.printf "3norm[%a] = %a\n" Print.print t1 CS.pp_s con1;
let con2 = norm (t2, mem) in
Format.printf "4norm[%a] = %a\n" Print.print t2 CS.pp_s con2;
let con0 = aux t1 t2 neg in
Format.printf "norm[con0] = %a\n" CS.pp_s con0;
CS.union (CS.union con1 con2) con0
in
big_prod norm_prod CS.sat (Pair.get t)
......@@ -3264,11 +3255,11 @@ module Tallying = struct
let tallying l =
let n = List.fold_left (fun acc (s,t) ->
Format.printf ">>>> Calling tallying on pair:\n>>%a\n>>%a\n@."
Print.print s Print.print t;
let d = diff s t in
(* if is_empty d then CS.sat else *) CS.prod acc (norm d)) CS.sat l in
Format.printf "Norm : %a\n" CS.pp_s n;
if is_empty d then CS.sat else
if no_var d then CS.unsat else
CS.prod acc (norm d)) CS.sat l in
(* Format.printf "Norm : %a\n" CS.pp_s n;*)
if CS.S.is_empty n then raise Step1Fail else
let m = CS.S.fold (fun c acc -> try CS.ES.union (solve (merge c)) acc with UnSatConstr _ -> acc) n CS.ES.empty in
(* Format.printf "Union/Merge : %a \n" CS.ES.print m;*)
......@@ -3294,14 +3285,10 @@ exception KeepGoing
let apply_raw s t =
DescrHash.clear Tallying.memo_norm;
Format.printf ">>>> Calling apply_raw on pair:\ns>>%a\nt>>%a\nwith substitutefree(s)=%a@."
Print.print s Print.print t Print.print (Positive.substitutefree s);
let q = Queue.create () in
let gamma = var (Var.mk ~variance:`Covariant "Gamma") in
let rec aux (i,acc1) (j,acc2) t1 t2 () =
let acc1 = Lazy.force acc1 and acc2 = Lazy.force acc2 in
Format.printf ">>>> Calling apply_raw_aux on :\nacc1>>%a\nacc2>>%a\nt1>>%a\nt2>>%a\n@."
Print.print acc1 Print.print acc2 Print.print t1 Print.print t2;
try (Tallying.tallying [(acc1,arrow (cons acc2) (cons gamma))]) , (acc1, acc2)
with
|Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
......@@ -3315,7 +3302,8 @@ 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 not(Queue.is_empty q) do
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
try
incr counter; (* don't know about termination... *)
if (!counter mod 100 == 0) then Format.printf "Warning: %i iterations during application typing\n%!" !counter;
......@@ -3327,10 +3315,6 @@ let apply_raw s t =
let apply_full s t =
let subst_lst,(s,t) = apply_raw s t in
Format.printf ">>> Found substitution: %a\nfor function: %a\nand argument: %a\n%!"
Tallying.CS.pp_sl subst_lst
Print.print s
Print.print t;
let ss =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
......
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