Commit 2b579d64 authored by Pietro Abate's avatar Pietro Abate

Minor changes

parent fa57e39e
......@@ -2929,9 +2929,10 @@ module Tallying = struct
(* we require that types are semantically equivalent and not structurally
* equivalent *)
let semantic_compare t1 t2 =
if Descr.equal t1 t2 then 0
else if equiv t1 t2 then 0
else Descr.compare t1 t2
let c = Descr.compare t1 t2 in
if c = 0 then 0 else
if equiv t1 t2 then 0
else c
(* constraint set : map to store constraints of the form (s <= alpha <= t) *)
module M = struct
......@@ -2980,14 +2981,7 @@ module Tallying = struct
Not_found -> inf, sup
in
if Var.Set.mem v delta then map
(* if ((equal inf empty) && (equal sup any)) ||
(equal (var v) inf && equal (var v) sup) then
map
else
raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
*)
else
VarMap.add v (new_i, new_s) map
else VarMap.add v (new_i, new_s) map
let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
let fold = VarMap.fold
......@@ -2996,7 +2990,7 @@ module Tallying = struct
end
(* equation set : (s < alpha < t) stored as
* { alpha -> ((s v beta) ^ t) } with beta fresh *)
{ alpha -> ((s v beta) ^ t) } with beta fresh *)
module E = struct
include Map.Make(struct
type t = Var.var
......@@ -3004,9 +2998,9 @@ module Tallying = struct
end)
let pp ppf e =
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
) ppf (bindings e)
Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
) ppf (bindings e)
end
......@@ -3401,7 +3395,7 @@ module Tallying = struct
let solve s =
let aux alpha (s,t) acc =
(* we cannot solve twice the same variable *)
(* we cannot solve twice the same variable *)
assert(not(CS.E.mem alpha acc));
let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in
let b = var (Var.fresh ~pre ()) in
......@@ -3648,7 +3642,7 @@ let apply_raw delta s t =
with FoundApply (res, i, j, sl) ->
(* we remove gamma from the substitution list as it is only used
here by the algorithm *)
let sl = (Tallying.filter (fun v -> not(Var.equal v vgamma)) sl) in
(* let sl = (Tallying.filter (fun v -> not(Var.equal v vgamma)) sl) in *)
(sl, get ai i, get aj j, res)
in
loop 0
......
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