From 0858d26f10c77f0b014ebef5e605b8da2512a8c7 Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 7 Jun 2018 18:06:05 +0200 Subject: [PATCH] Trailing constant args in p.div are removed by sanity Because they cannot contribute to any usable eta-difference --- ocaml/simple.ml | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) 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); -- 2.39.2