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

* Stop the typing at the first solution. This avoids two expensive subtyping tests

  to detect that we have the most precise solution
* Apply clean_type more agressively but on smaller types, for each of the partial solutions
  rather than on the (big) intersection of all the solutions.
* Small optimisation in substitutefree: do not do anything if the type has no variables
parent 14cd9c55
......@@ -2569,9 +2569,10 @@ struct
descr (solve new_t)
end
let substitutefree t =
let h = Hashtbl.create 17 in
let substitutefree =
let idx = ref 0 in
fun t -> if no_var t then t else
let h = Hashtbl.create 17 in
let subst h d =
try Hashtbl.find h d
with Not_found -> begin
......@@ -3255,18 +3256,20 @@ let apply_raw s t =
let sl = Tallying.tallying [ (s,t) ] in
let new_res =
List.fold_left (fun tacc constr_lst ->
cap tacc (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) gamma constr_lst)) any sl
cap tacc (Positive.clean_type (List.fold_left (fun tacc subst ->
Positive.substitute tacc subst) gamma constr_lst))) any sl
in
let new_res = Positive.clean_type new_res in
if subtype new_res !result && not (subtype !result new_res)
then begin
(* Uncomment only if we are looking for the most-precise solution *)
(* if subtype new_res !result && not (subtype !result new_res)
then begin
(* strictly improved the result, continue *)
Format.printf "Found a partial solution at %i, %i: %a@\n@."
i j Print.print new_res;
result := new_res
end
else raise (Found(new_res,i,j,sl))
Format.printf "Found a partial solution at %i, %i: %a@\n@."
i j Print.print new_res;
result := new_res
end
else
*)
raise (Found(new_res,i,j,sl))
with
Tallying.Step1Fail -> (assert (i == 0 && j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
| Tallying.Step2Fail -> () (* continue *)
......
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