Commit 9c70e7b8 authored by Pietro Abate's avatar Pietro Abate

Fix types substututions printers

Conflicts:
	types/types.ml
parent 7f09389f
......@@ -452,6 +452,7 @@ let var a = {
let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let all_vars t = t.toplvars.TLV.f
(* XXX this function could be potentially costly. There should be
* better way to take trace of top level variables in a type *)
......@@ -2591,9 +2592,13 @@ module Tallying = struct
|Pos (v,s) -> S.singleton (M.singleton (true,v) s)
|Neg (s,v) -> S.singleton (M.singleton (false,v) s)
let print = S.print
let print_m = M.print
let print_e = E.print
let pp_s = S.print
let pp_m = M.print
let pp_e = E.print
let pp_sl ppf ll =
print_lst (fun ppf l ->
(print_lst (fun ppf (v,t) -> Format.fprintf ppf "(%a/%a)" Var.print v Print.print t) ppf l)
) ppf ll
(* Inv : a map contains only on binding for each variable *)
let merge m1 m2 =
......@@ -2981,7 +2986,7 @@ module Tallying = struct
let tallying l =
let n = List.fold_left (fun acc (s,t) -> CS.prod acc (norm(diff s t))) CS.sat l in
Format.printf "Norm : %a\n" CS.print n;
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;
......
......@@ -389,9 +389,10 @@ module Tallying : sig
type es = ES.t
type sl = (Var.var * t) list list
val print : Format.formatter -> s -> unit
val print_m : Format.formatter -> m -> unit
val print_e : Format.formatter -> e -> unit
val pp_s : Format.formatter -> s -> unit
val pp_m : Format.formatter -> m -> unit
val pp_e : Format.formatter -> e -> unit
val pp_sl : Format.formatter -> sl -> unit
val merge : m -> m -> m
val singleton : constr -> s
......
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