Commit c9debef5 authored by Kim Nguyễn's avatar Kim Nguyễn

Fix a regression where polymorphic variables would not be chosen in favor of...

Fix a regression where polymorphic variables would not be chosen in favor of monomorphic ones during the 'single' phase of constraint generation.
parent 779c1aba
......@@ -223,6 +223,14 @@ let toplevel
then ConstrSet.unsat
else ConstrSet.singleton x cst
in
let var_compare v1 v2 =
let mono1 = Var.Set.mem delta v1 in
let mono2 = Var.Set.mem delta v2 in
match mono1, mono2 with
| false, true -> -1
| true, false -> 1
| _ -> Var.compare v1 v2
in
match lpos, lneg with
[], (`Var x)::neg ->
let t = single (module V) false x [] neg in
......@@ -233,7 +241,9 @@ let toplevel
singleton x (empty, t)
| (`Var x)::pos, (`Var y)::neg ->
if Var.compare x y < 0 then
DEBUG toplevel (Format.eprintf
"@[ - pos/neg case = %a, %a @]@\n" Var.print x Var.print y);
if var_compare x y < 0 then
let t = single (module V) true x pos lneg in
singleton x (empty, t)
else
......
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