Commit 8845353e authored by Pietro Abate's avatar Pietro Abate
Browse files

Remove debugging messages from the norm function

parent c18b8b05
......@@ -2306,40 +2306,22 @@ module Tallying = struct
(* check if there exists a toplevel varaible : fun (pos,neg) *)
let toplevel single norm_rec mem (p,n) = match (p,n) with
|([],(`Var x)::neg) ->
(
Format.printf "single 1 = %a\n" Print.print (single (false,x,[],neg));
CS.singleton (false,`Var x,single (false,x,p,n))
)
|((`Var x)::pos,[]) ->
Format.printf "single 2 = %a\n" Print.print (single (true,x,pos,[]));
CS.singleton (true ,`Var x,single (true,x,pos,[]))
|((`Var x)::pos, (`Var y)::neg) ->
(* XXX this compare must be changed *)
if Pervasives.compare (`Var x) (`Var y) < 0 then
(
Format.printf "single 3 = %a\n" Print.print (single (true,x,pos,n));
CS.singleton (true,`Var x,single (true,x,pos,n))
)
else
(
Format.printf "single 4 = %a\n" Print.print (single (false,y,p,neg));
CS.singleton (false, `Var y,single (false,y,p,neg))
)
|([`Atm a], (`Var x)::neg) ->
(
Format.printf "!! single 5 = %a\n" Print.print (single (false,x,p,neg));
CS.singleton (false,`Var x,single (false,x,p,neg))
)
|((`Var x)::pos, [`Atm _]) -> failwith "impossible5"
(*
Format.printf "!! single = %a\n" Print.print (single (pos,[],[],n));
CS.singleton (true ,`Var x,single (pos,[],[],n))
*)
|([`Atm t], []) -> norm_rec (t,mem)
|([],[`Atm t]) -> failwith "impossible0" (* norm_rec (t,mem) *)
|([],[]) -> failwith "impossible"
......@@ -2352,9 +2334,6 @@ module Tallying = struct
try
let aux_base single norm_aux acc l =
List.fold_left (fun acc (pos,neg) ->
(*
Format.printf "top cap = %a V %a = %a\n" CS.print acc CS.print (toplevel single norm_aux m (pos,neg)) CS.print (CS.cap acc (toplevel single norm_aux m (pos,neg)));
*)
CS.cap acc (toplevel single norm_aux m (pos,neg))
) acc l
in
......@@ -2419,24 +2398,17 @@ module Tallying = struct
match neg with
|[] -> CS.S.empty
|(t1,t2) :: n ->
Format.printf "t1 = %a\n" Print.print (descr t1);
let con1 = norm (descr t1, mem) in
Format.printf "neg con1 = %a\n" CS.print con1;
let con2 = aux (descr t1) (diff any (descr t2)) pos in
Format.printf "neg con2 = %a\n" CS.print con2;
let con0 = norm_arrow pos n in
CS.cup (CS.cup con1 con2) con0
and aux t1 acc = function
|[] -> CS.S.empty
|(s1,s2) :: p ->
let t1s1 = diff t1 (descr s1) in
Format.printf "t1 \\ s1 = %a\n" Print.print t1s1;
let acc1 = cap acc (descr s2) in
let con1 = norm (t1s1, mem) in
Format.printf "pos con1 = %a\n" CS.print con1;
Format.printf "- t2 ^ acc ^ s2 = %a\n" Print.print acc1;
let con2 = norm (acc1, mem) in
Format.printf "pos con2 = %a\n" CS.print con2;
let con10 = aux t1s1 acc p in
let con20 = aux t1 acc1 p in
let con11 = CS.cup con1 con10 in
......@@ -2462,7 +2434,8 @@ module Tallying = struct
|(false,v) -> acc
) cs CS.sat
let merge c = merge (c,DescrSet.empty)
let merge c =
CS.S.fold (fun cs acc -> CS.cup acc (merge (cs,DescrSet.empty))) c CS.sat
(*
let solve cs =
......
......@@ -365,7 +365,7 @@ module Tallying : sig
end
val norm : t -> CS.cset
val merge : CS.S.elt -> CS.cset
val merge : CS.cset -> CS.cset
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