Added check for eta_subterm in `solve'

Reverted sanity to old syntax

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 534100d4f0787961fb688461dd34f52d82314bed..d9bc38917910db68afe1c226d3ae153e85a4e4b4 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -17,7 +17,7 @@ type t =
 \r
 let delta = L(A(V 0, V 0));;\r
 \r
-let eta_eq =\r
+let eta_eq' =\r
  let rec aux l1 l2 t1 t2 = match t1, t2 with\r
   | L t1, L t2 -> aux l1 l2 t1 t2\r
   | L t1, t2 -> aux l1 (l2+1) t1 t2\r
@@ -26,7 +26,16 @@ let eta_eq =
   | C a, C b -> a = b\r
   | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
   | _, _ -> false\r
- in aux 0 0\r
+ in aux ;;\r
+let eta_eq = eta_eq' 0 0;;\r
+\r
+(* is arg1 eta-subterm of arg2 ? *)\r
+let eta_subterm u =\r
+ let rec aux lev t = eta_eq' lev 0 u t || match t with\r
+ | L t -> aux (lev+1) t\r
+ | A(t1, t2) -> aux lev t1 || aux lev t2\r
+ | _ -> false\r
+ in aux 0\r
 ;;\r
 \r
 (* does NOT lift t *)\r
@@ -186,7 +195,8 @@ let sanity p =
  if p.conv = B then problem_fail p "p.conv diverged";\r
  if p.div = B then raise (Done p.sigma);\r
  if p.phase = `Two && p.div = delta then raise (Done p.sigma);\r
- if not (is_inert p.div) then problem_fail p "p.div converged"\r
+ if not (is_inert p.div) then problem_fail p "p.div converged";\r
+ p\r
 ;;\r
 \r
 (* drops the arguments of t after the n-th *)\r
@@ -253,7 +263,7 @@ print_cmd "EAT" "";
  let p = subst_in_problem subst p in\r
  sanity p;\r
  let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in\r
- sanity p; p\r
+ sanity p\r
 ;;\r
 \r
 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
@@ -270,7 +280,8 @@ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")")
  let t = mk_lams t (k+1) in (* make leading lambdas *)\r
  let subst = var, t in\r
  let p = subst_in_problem subst p in\r
- sanity p; p\r
+ sanity p\r
+;;\r
 ;;\r
 \r
 let parse strs =\r
@@ -290,7 +301,7 @@ let problem_of div conv =
  let varno = List.length var_names in\r
  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in\r
  (* initial sanity check *)\r
- sanity p; p\r
+ sanity p\r
 ;;\r
 \r
 let exec div conv cmds =\r
@@ -393,4 +404,9 @@ auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
 print_hline();\r
 print_endline "ALL DONE. "\r
 \r
-let solve = auto';;\r
+let solve div convs =\r
+ let p = problem_of div (conv_join convs) in\r
+ if eta_subterm p.div p.conv\r
+  then print_endline "!!! div is subterm of conv. Problem was not run !!!"\r
+  else check p (auto p)\r
+;;\r