From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 13:17:06 +0000 (+0200)
Subject: Added check for eta_subterm in `solve'
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=276d4f75cbe40801f2d9faa82ac82d1c82204e55;p=fireball-separation.git

Added check for eta_subterm in `solve'

Reverted sanity to old syntax
---

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index 534100d..d9bc389 100644
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -17,7 +17,7 @@ type t =
 
 let delta = L(A(V 0, V 0));;
 
-let eta_eq =
+let eta_eq' =
  let rec aux l1 l2 t1 t2 = match t1, t2 with
   | L t1, L t2 -> aux l1 l2 t1 t2
   | L t1, t2 -> aux l1 (l2+1) t1 t2
@@ -26,7 +26,16 @@ let eta_eq =
   | C a, C b -> a = b
   | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2
   | _, _ -> false
- in aux 0 0
+ in aux ;;
+let eta_eq = eta_eq' 0 0;;
+
+(* is arg1 eta-subterm of arg2 ? *)
+let eta_subterm u =
+ let rec aux lev t = eta_eq' lev 0 u t || match t with
+ | L t -> aux (lev+1) t
+ | A(t1, t2) -> aux lev t1 || aux lev t2
+ | _ -> false
+ in aux 0
 ;;
 
 (* does NOT lift t *)
@@ -186,7 +195,8 @@ let sanity p =
  if p.conv = B then problem_fail p "p.conv diverged";
  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"
+ if not (is_inert p.div) then problem_fail p "p.div converged";
+ p
 ;;
 
 (* drops the arguments of t after the n-th *)
@@ -253,7 +263,7 @@ print_cmd "EAT" "";
  let p = subst_in_problem subst p in
  sanity p;
  let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in
- sanity p; p
+ sanity p
 ;;
 
 (* step on the head of div, on the k-th argument, with n fresh vars *)
@@ -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 *)
  let subst = var, t in
  let p = subst_in_problem subst p in
- sanity p; p
+ sanity p
+;;
 ;;
 
 let parse strs =
@@ -290,7 +301,7 @@ let problem_of div conv =
  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; p
+ sanity p
 ;;
 
 let exec div conv cmds =
@@ -393,4 +404,9 @@ auto' "x a a a a (x (x. x x) @ @ (_._.x. x x) x) b b b" [
 print_hline();
 print_endline "ALL DONE. "
 
-let solve = auto';;
+let solve div convs =
+ let p = problem_of div (conv_join convs) in
+ if eta_subterm p.div p.conv
+  then print_endline "!!! div is subterm of conv. Problem was not run !!!"
+  else check p (auto p)
+;;