From cf59c212d1883fba82d65b9329faf9e3b1579c3e Mon Sep 17 00:00:00 2001 From: lukstafi Date: Wed, 11 Mar 2015 16:46:16 +0100 Subject: [PATCH] Fix to eliminating universal variables in term abduction (i.e. choice 6). --- examples/mutual_recursion_eval_docs.ml.target | 6 ++--- src/Abduction.ml | 27 ++++++++++++++----- src/Infer.ml | 2 +- src/InvarGenTTest.ml | 17 +++++------- 4 files changed, 31 insertions(+), 21 deletions(-) diff --git a/examples/mutual_recursion_eval_docs.ml.target b/examples/mutual_recursion_eval_docs.ml.target index d37b15e..23daeb5 100644 --- a/examples/mutual_recursion_eval_docs.ml.target +++ b/examples/mutual_recursion_eval_docs.ml.target @@ -35,7 +35,7 @@ type ex3 = be easier to only expose the external one. *) let (calc, eval) (*: type a . ((calc -> ex3) * (a term -> a))*) = (** [eval] has to expose its "helper" function. *) - let rec eval : type b . ((calc -> ex3) * (b term -> b)) = + let rec eval : type a . ((calc -> ex3) * (a term -> a)) = let rec calc : (calc -> ex3) = ((function Lit i -> let xcase = i in Ex3 xcase | Plus (x, y) -> @@ -58,7 +58,7 @@ let (calc, eval) (*: type a . ((calc -> ex3) * (a term -> a))*) = let Ex3 r = calc x in is_zero r | If (b, t, e) -> (if snd eval b then snd eval t else snd eval e) | Pair (x, y) -> (snd eval x, snd eval y) - | Fst p -> let ((x, y): (b * _)) = snd eval p in x - | Snd p -> let ((x, y): (_ * b)) = snd eval p in y): b term -> b)) in + | Fst p -> let ((x, y): (a * _)) = snd eval p in x + | Snd p -> let ((x, y): (_ * a)) = snd eval p in y): a term -> a)) in eval diff --git a/src/Abduction.ml b/src/Abduction.ml index 034df44..691d98e 100644 --- a/src/Abduction.ml +++ b/src/Abduction.ml @@ -12,7 +12,7 @@ let guess_eqs_nonvar = ref true let prefer_guess = ref false let neg_before_abd = ref true let num_neg_since = ref 1 -let term_neg_since = ref 1 +let term_neg_since = ref (* 1 *)0 let more_general = ref false let richer_answers = ref false let no_num_abduction = ref false @@ -201,9 +201,15 @@ let revert_uni q ~bvs ~dissociate ans prem cand = if !rich_return_type then rich_return_type_heur bvs ans cand else cand in - (*[* Format.printf "revert_uni: res=%a@\n%!" pr_subst - (varmap_of_assoc cand); *]*) - tu_sb @ c_sb, cand + let rev_sb = List.filter + (fun (lhs, (rhs, _)) -> not (VarSet.exists univar (fvs_typ rhs))) + (tu_sb @ c_sb) in + (*[* Format.printf "revert_uni: revert sb=@ %a@\nres=%a@\n%!" + (pr_sep_list "; " + (fun ppf (lhs,(rhs,_)) -> + Format.fprintf ppf "%a:=%a" pr_ty lhs pr_ty rhs)) rev_sb + pr_subst (varmap_of_assoc cand); *]*) + rev_sb, cand let cand_var_eqs q bvs cnj_typ = let cands = List.filter @@ -960,13 +966,22 @@ let abd q ~bvs ~xbvs ?orig_ren ?b_of_v ~upward_of ~nonparam_vars let neg_validate (vs, ans) = (* Returns the number of negative constraints not contradicted by the answer, i.e. the closer to 0 the better. *) + (*[* Format.printf "Abd.neg_validate: for ans=@ %a@\n%!" + pr_subst ans; *]*) List.fold_left (fun acc (cnj, _) -> acc + try + (*[* Format.printf + "Abd.neg_validate: checking cnj_typ=@ %a@\n%!" + pr_subst cnj.cnj_typ; *]*) ignore - (combine_sbs ~use_quants:false q [cnj.cnj_typ; ans]); 1 - with Contradiction _ -> 0) + (combine_sbs ~use_quants:false q [cnj.cnj_typ; ans]); + (*[* Format.printf "not contradicted@\n%!"; *]*) + 1 + with Contradiction _ -> + (*[* Format.printf "success: contradicted@\n%!"; *]*) + 0) 0 neg_cns_pre in let neg_term = (* Select [bvs] variables equated with constructors participating in diff --git a/src/Infer.ml b/src/Infer.ml index 55374c7..cf8f82d 100644 --- a/src/Infer.ml +++ b/src/Infer.ml @@ -864,7 +864,7 @@ let annotate_expr q res_sb chi_sb nice_sb e : texpr = (*[* Format.printf "a1s,a2s=%s@\nres_sb=%a@\nnice_sb=%a@\n%!" (String.concat "; " (List.map (fun (a1,a2)->var_str a1^","^var_str a2) - (varmap_to_assoc ann))) + ann)) pr_subst res_sb pr_hvsubst nice_sb; *]*) assert false in let t1 = hvsubst_typ nice_sb (fst (VarMap.find a1 res_sb)) diff --git a/src/InvarGenTTest.ml b/src/InvarGenTTest.ml index 479bcc7..e520dfa 100644 --- a/src/InvarGenTTest.ml +++ b/src/InvarGenTTest.ml @@ -257,7 +257,6 @@ let tests = "InvarGenT" >::: [ test_case ~test_annot:true "equational_reas" ()); "mutual_recursion_eval-annot" >:: (fun () -> - todo "FIXME"; skip_if !debug "debug"; test_case ~test_annot:true "mutual_recursion_eval_docs" ()); "concat_strings-export" >:: @@ -343,13 +342,11 @@ let tests = "InvarGenT" >::: [ test_case "non_pointwise_split" ()); "non_pointwise-avl_small_rec" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "non_pointwise_avl_small_rec" ()); "non_pointwise-avl_small" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "non_pointwise_avl_small" ()); (* "non_pointwise-vary" >:: (fun () -> @@ -365,18 +362,15 @@ let tests = "InvarGenT" >::: [ test_case "avl_delmin_simpler" ()); "non_pointwise-avl_delmin-modified" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "non_pointwise_avl_delmin_modified" ()); "non_pointwise-avl_delmin" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "non_pointwise_avl_delmin" ()); "non_pointwise-avl_delmin2" >:: (fun () -> - todo "FIXME"; - (* skip_if !debug "debug"; *) + skip_if !debug "debug"; test_case "non_pointwise_avl_delmin2" ()); "non_pointwise-fd_comp" >:: (fun () -> @@ -672,6 +666,7 @@ let tests = "InvarGenT" >::: [ test_case ~test_annot:true "liquid_simplex" ()); "liquid_simplex-harder" >:: (fun () -> + todo "FIXME"; skip_if !debug "debug"; skip_if !short_tests_only "long test: 53s"; test_case "liquid_simplex_harder" ());