Trailing constant args in p.div are removed by sanity

Because they cannot contribute to any usable eta-difference

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 44b9aa2a871d74619fdcbe88599580ce4c7b2d70..b2e8234aeb68cd2bfd36cfe7dd44f03cf49a0154 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -218,6 +218,11 @@ let sanity p =
  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
+ (* Trailing constant args can be removed because do not contribute to eta-diff *)\r
+ let rec remove_trailing_constant_args = function\r
+ | A(t1, t2) when is_constant t2 -> remove_trailing_constant_args t1\r
+ | _ as t -> t in\r
+ let p = {p with div=remove_trailing_constant_args p.div} in\r
  p\r
 ;;\r
 \r
@@ -391,16 +396,15 @@ let problem_of (label, div, convs, ps, var_names) =
  | Some div -> aux 0 (div :> Num.nf)\r
  | None -> assert false in\r
  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\r
+ {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One}\r
 ;;\r
 \r
 let solve p =\r
- if is_stuck p.div then print_endline "!!! div is stuck. Problem was not run !!!"\r
+ if is_constant p.div\r
+  then print_endline "!!! div is stuck. Problem was not run !!!"\r
  else 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
+  else let p = sanity p (* initial sanity check *) in check p (auto p)\r
 ;;\r
 \r
 Problems.main (solve ++ problem_of);\r