Commit 9f389c21 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Try an early simplification of types.

parent 3f63d285
......@@ -2546,9 +2546,7 @@ struct
(* returns a recursive type where all occurrences of alpha n t
* are substituted with a recursive variable X and all fresh variables
* in covariant position are substituted with empty and contravariant
* position with any *)
* are substituted with a recursive variable X *)
let substituterec t alpha =
let subst x d =
if Var.equal d alpha then x
......@@ -2605,9 +2603,9 @@ struct
end)
in
let vars = Hashtbl.create 17 in
let memo = Memo.create 17 in
let t_emp = ty empty in
let t_any = ty any in
let memo = Memo.create 17 in
let t_emp = cup [] in
let t_any = cap [] in
let idx = ref 0 in
(* we memoize based on the pair (pos, v), since v can occur both
......@@ -2623,7 +2621,7 @@ struct
let td = Hashtbl.find vars d in
if ((td == t_emp) && not pos)
|| ((td == t_any) && pos)
then (* polarity problem, replace the binding by a new,
then (* polarity conflict, replace the binding by a new,
pretty-printed variable *)
begin
let id = pretty_name !idx "" in
......@@ -2659,20 +2657,33 @@ struct
descr (solve new_t)
end
let clean_type t =
if no_var t then t else
if not (subtype t Arrow.any) then clean_variables t
else
let _, u_arrow = Arrow.get t in
let rec uniq = function
| ([] | [ _ ]) as l -> l
| t1 :: ((t2 :: _) as l1) ->
if equiv t1 t2 then uniq l1 else t1 :: uniq l1
let clean_type t =
if no_var t then t else
let t = clean_variables t in
let arrow_t, non_arrow_t =
{ empty with arrow = t.arrow },
{ t with arrow = empty.arrow }
in
let _, u_arrow = Arrow.get arrow_t in
List.fold_left (fun acc i_arrow ->
T.cup acc (
(List.fold_left (fun acc (dom, cdom) ->
let conj_arrow = (List.fold_left (fun acc (dom, cdom) ->
let indiv_arrow = T.arrow (T.cons dom) (T.cons cdom) in
let pretty_arrow = clean_variables indiv_arrow in
T.cap acc pretty_arrow
) T.any i_arrow)
indiv_arrow::acc
) [] i_arrow)
in
let sorted_conj = List.sort (fun t1 t2 -> if equiv t1 t2 then 0 else
compare t1 t2) conj_arrow
in
List.fold_left (T.cap) T.any (uniq sorted_conj)
)
) T.empty u_arrow
) non_arrow_t u_arrow
end
......@@ -3231,6 +3242,7 @@ let apply_raw s t =
let get a i = if i < 0 then any else (!a).(i) in
let gamma = var (Var.mk "Gamma") in
let cgamma = cons gamma in
(* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
let ai = ref [| |]
and aj = ref [| |] in
let result = ref any in
......@@ -3244,20 +3256,24 @@ let apply_raw s t =
cap tacc (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
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))
with
Tallying.Step1Fail -> raise (Tallying.UnSatConstr "apply_raw step1")
Tallying.Step1Fail -> (assert (i == 0 && j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
| Tallying.Step2Fail -> () (* continue *)
in
let rec loop i =
try
Format.printf "Starting expansion %i @\n@." i;
set ai (i) (cap (Positive.substitutefree s) (get ai (i-1)));
set aj (i) (cap (Positive.substitutefree t) (get aj (i-1)));
set ai i (cap (Positive.substitutefree s) (get ai (i-1)));
set aj i (cap (Positive.substitutefree t) (get aj (i-1)));
for j = 0 to i-1 do
tallying j i;
tallying i j;
......@@ -3275,7 +3291,6 @@ let apply_raw s t =
let apply_full s t =
let _,_,_,res = apply_raw s t in
let res = Positive.clean_type res in
Format.printf "result: %a@\n@." Print.print res;
res
......
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