From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 7 Jun 2018 16:06:05 +0000 (+0200)
Subject: Trailing constant args in p.div are removed by sanity
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0858d26f10c77f0b014ebef5e605b8da2512a8c7;p=fireball-separation.git

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 44b9aa2..b2e8234 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -218,6 +218,11 @@ let sanity p =
  if p.div = B then raise (Done p.sigma);
  if p.phase = `Two && p.div = delta then raise (Done p.sigma);
  if not (is_inert p.div) then problem_fail p "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
+ | _ as t -> t in
+ let p = {p with div=remove_trailing_constant_args p.div} in
  p
 ;;
 
@@ -391,16 +396,15 @@ 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
- let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in
- (* initial sanity check *)
- sanity p
+ {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One}
 ;;
 
 let solve p =
- if is_stuck p.div then print_endline "!!! div is stuck. Problem was not run !!!"
+ 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 check p (auto p)
+  else let p = sanity p (* initial sanity check *) in check p (auto p)
 ;;
 
 Problems.main (solve ++ problem_of);