From: acondolu Date: Sun, 10 Jun 2018 14:38:56 +0000 (+0200) Subject: Improved backtracking in Simple X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1f8f8e52c38e1897e9b5ea106721d6a4dd88c284;p=fireball-separation.git Improved backtracking in Simple - Removed Fail exception, replaced by combination of Failure, Backtrack, Unseparable - Added label to problem --- diff --git a/ocaml/simple.ml b/ocaml/simple.ml index 16b4e69..60b4e87 100644 --- a/ocaml/simple.ml +++ b/ocaml/simple.ml @@ -70,6 +70,7 @@ let string_of_t = type problem = { orig_freshno: int ; freshno : int + ; label : string ; div : t ; conv : t ; sigma : (var * t) list (* substitutions *) @@ -85,12 +86,18 @@ let string_of_problem p = exception B;; exception Done of (var * t) list (* substitution *);; -exception Fail of int * string;; +exception Unseparable of string;; +exception Backtrack of string;; + +let rec try_all label f = function + | x::xs -> (try f x with Backtrack _ -> try_all label f xs) + | [] -> raise (Backtrack label) +;; let problem_fail p reason = print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!"; print_endline (string_of_problem p); - raise (Fail (-1, reason)) + failwith reason ;; let freshvar ({freshno} as p) = @@ -176,7 +183,7 @@ print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t); let sigma = sub :: p.sigma in let div, g = try subst sub p.div with B -> raise (Done sigma) in assert (g = []); - let conv, f = try subst sub p.conv with B -> raise (Fail(-1, "p.conv diverged")) in + let conv, f = try subst sub p.conv with B -> raise (Backtrack "p.conv diverged") in assert (g = []); {p with div; conv; sigma} ;; @@ -212,16 +219,18 @@ let check p sigma = let sigma = List.map (fun (v,t) -> v, purify t) sigma in let freshno = List.fold_right (max ++ fst) sigma 0 in let env = Pure.env_of_sigma freshno sigma in - assert (Pure.diverged (Pure.mwhd (env,div,[]))); - print_endline " D diverged."; - assert (not (Pure.diverged (Pure.mwhd (env,conv,[])))); - print_endline " C converged."; + (if not (Pure.diverged (Pure.mwhd (env,div,[]))) + then failwith "D converged in Pure"); + print_endline "- D diverged."; + (if Pure.diverged (Pure.mwhd (env,conv,[])) + then failwith "C diverged in Pure"); + print_endline "- C converged."; () ;; let sanity p = print_endline (string_of_problem p); (* non cancellare *) - if not (is_inert p.div) then problem_fail p "p.div converged"; + if not (is_inert p.div) then raise (Backtrack "p.div converged"); (* Trailing constant args can be removed because do not contribute to eta-diff *) let rec remove_trailing_constant_args = function | A(t1, t2) when is_constant t2 -> remove_trailing_constant_args t1 @@ -353,24 +362,16 @@ let auto p = if List.exists (fun t -> snd (get_inert t) >= n_args) tms then ( (* let tms = List.sort (fun t1 t2 -> - compare (snd (get_inert t1)) (snd (get_inert t2))) tms in *) - List.iter (fun t -> try + try_all "no similar terms" (fun t -> let js = find_eta_difference p t in (* print_endline (String.concat ", " (List.map string_of_int js)); *) - if js = [] then problem_fail p "no eta difference found (div subterm of conv?)"; let js = List.rev js in - List.iter + try_all "no eta difference" (fun j -> - try let k = 1 + max (compute_max_lambdas_at hd_var j p.div) (compute_max_lambdas_at hd_var j p.conv) in - ignore (aux (step j k p)) - with Fail(_, s) -> - print_endline ("Backtracking (eta_diff) because: " ^ s)) js; - raise (Fail(-1, "no eta difference")) - with Fail(_, s) -> - print_endline ("Backtracking (get_subterms) because: " ^ s)) tms; - raise (Fail(-1, "no similar terms")) + aux (step j k p)) js) tms ) else problem_fail (finish p) "Finish did not complete the problem" @@ -395,15 +396,26 @@ let problem_of (label, div, convs, ps, var_names) = | Some div -> aux 0 (div :> Num.nf) | None -> assert false in let varno = List.length var_names in - {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]} + {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; label} ;; let solve p = - if is_constant p.div - then print_endline "!!! div is stuck. Problem was not run !!!" - else if eta_subterm p.div p.conv - then print_endline "!!! div is subterm of conv. Problem was not run !!!" - else let p = sanity p (* initial sanity check *) in check p (auto p) + let c = if String.length p.label > 0 then String.sub (p.label) 0 1 else "" in + let module M = struct exception Okay end in + try + if eta_subterm p.div p.conv + then raise (Unseparable "div is subterm of conv") + else + let p = sanity p (* initial sanity check *) in + check p (auto p); + raise M.Okay + with + | M.Okay -> if c = "?" then + failwith "The problem succeeded, but was supposed to be unseparable" + | e when c = "!" -> + failwith ("The problem was supposed to be separable, but: "^Printexc.to_string e) + | e -> + print_endline ("The problem failed, as expected ("^Printexc.to_string e^")") ;; Problems.main (solve ++ problem_of); diff --git a/ocaml/simple.mli b/ocaml/simple.mli index fba2470..67bee91 100644 --- a/ocaml/simple.mli +++ b/ocaml/simple.mli @@ -1,5 +1,5 @@ type problem -exception Fail of int * string +exception Unseparable of string val solve : problem -> unit val problem_of : string * Num.i_var option * Num.i_n_var list * Num.i_n_var list * diff --git a/ocaml/simple_test.ml b/ocaml/simple_test.ml index ed2c81c..9e79ee9 100644 --- a/ocaml/simple_test.ml +++ b/ocaml/simple_test.ml @@ -58,9 +58,10 @@ let main = print_endline str; try (solve ++ problem_of ++ Parser.problem_of_string) ("$" ^ str) - with Simple.Fail _ as e -> - let str = "$ failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in + with Failure _ as e -> + let str = "$! failing test problem \n# Failed because: " ^ Printexc.to_string e ^ str in Printf.fprintf oc "%s\n" str + | Unseparable _ -> () ) num ; close_out oc; print_endline ("\n\n---- " ^ file);