X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fsimple.ml;h=079774e5ac67e5c53feaa53eca9e7e622dd77c76;hb=b0ecd3e4062bb9012ea9623237d0b379bd7646f2;hp=a028b1f269015752f08833999edad20386d1cf52;hpb=b532f22eeae82f364dbc533926ea657df765d1e8;p=fireball-separation.git

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index a028b1f..079774e 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -62,7 +62,7 @@ let string_of_t =
     | _ as t -> string_of_term_w_pars level t
   and string_of_term_no_pars level = function
     | L(t,g) -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t
-       ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_w_pars level) g))
+       ^ (if g = [] then "" else String.concat ", " ("" :: List.map (string_of_term_w_pars (level+1)) g))
     | _ as t -> string_of_term_no_pars_app level t
   in string_of_term_no_pars 0
 ;;
@@ -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
@@ -248,9 +257,11 @@ let inert_cut_at n t =
 let find_eta_difference p t =
  let divargs = args_of_inert p.div in
  let conargs = args_of_inert t in
+ let rec range i j =
+  if j = -1 then [] else i :: range (i+1) (j-1) in
  let rec aux k divargs conargs =
   match divargs,conargs with
-     [],_ -> []
+     [],conargs -> range k (List.length conargs)
    | _::_,[] -> [k]
    | t1::divargs,t2::conargs ->
       (if not (eta_eq t1 t2) then [k] else []) @ aux (k+1) divargs conargs
@@ -353,24 +364,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"
@@ -383,7 +386,7 @@ let auto p =
 let problem_of (label, div, convs, ps, var_names) =
  print_hline ();
  let rec aux lev = function
- | `Lam(_, t) -> L (aux (lev+1) t, [])
+ | `Lam(_, t, g) -> L (aux (lev+1) t, List.map (aux (lev+1)) g)
  | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args
  | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else V v
  | `N _ | `Match _ -> assert false in
@@ -395,15 +398,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);