Removed eat, p.stepped, p.phase and t.B

diff --git a/ocaml/simple.ml b/ocaml/simple.ml
index c86796e56c8d2a690787cba48f40a536c08b1232..897d6b68a4b736952774d4127e109020f2fb7618 100644 (file)
--- a/ocaml/simple.ml
+++ b/ocaml/simple.ml
@@ -11,7 +11,6 @@ type t =
  | V of var\r
  | A of t * t\r
  | L of t\r
- | B (* bottom *)\r
  | C (* constant *)\r
 ;;\r
 \r
@@ -58,7 +57,6 @@ let string_of_t =
     | C -> "C"\r
     | A _\r
     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
-    | B -> "BOT"\r
   and string_of_term_no_pars_app level = function\r
     | A(t1,t2) -> string_of_term_no_pars_app level t1 ^ " " ^ string_of_term_w_pars level t2\r
     | _ as t -> string_of_term_w_pars level t\r
@@ -74,19 +72,17 @@ type problem = {
  ; div : t\r
  ; conv : t\r
  ; sigma : (var * t) list (* substitutions *)\r
- ; stepped : var list\r
- ; phase : [`One | `Two] (* :'( *)\r
 }\r
 \r
 let string_of_problem p =\r
  let lines = [\r
-  "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
   "[DV] " ^ string_of_t p.div;\r
   "[CV] " ^ string_of_t p.conv;\r
  ] in\r
  String.concat "\n" lines\r
 ;;\r
 \r
+exception B;;\r
 exception Done of (var * t) list (* substitution *);;\r
 exception Fail of int * string;;\r
 \r
@@ -107,14 +103,13 @@ let rec is_inert =
  | A(t,_) -> is_inert t\r
  | V _ -> true\r
  | C\r
- | L _ | B -> false\r
+ | L _ -> false\r
 ;;\r
 \r
 let rec is_constant =\r
  function\r
     C -> true\r
   | V _ -> false\r
-  | B -> assert false\r
   | A(t,_)\r
   | L t -> is_constant t\r
 ;;\r
@@ -141,7 +136,7 @@ let rec no_leading_lambdas v n = function
  | L t -> 1 + no_leading_lambdas (v+1) n t\r
  | A _ as t -> let v', m = get_inert t in if V v = v' then max 0 (n - m) else 0\r
  | V v' -> if v = v' then n else 0\r
- | B | C -> 0\r
+ | C -> 0\r
 ;;\r
 \r
 let rec subst level delift sub =\r
@@ -152,10 +147,9 @@ let rec subst level delift sub =
   let t1 = subst level delift sub t1 in\r
   let t2 = subst level delift sub t2 in\r
   mk_app t1 t2\r
- | C | B as t -> t\r
-and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
+ | C -> C\r
+and mk_app t1 t2 = if t1 = delta && t2 = delta then raise B\r
  else match t1 with\r
- | B -> B\r
  | L t1 -> subst 0 true (0, t2) t1\r
  | _ -> A (t1, t2)\r
 and lift n =\r
@@ -164,7 +158,7 @@ and lift n =
   | V m -> V (if m >= lev then m + n else m)\r
   | L t -> L (aux (lev+1) t)\r
   | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
-  | C  | B as t -> t\r
+  | C -> C\r
  in aux 0\r
 ;;\r
 let subst = subst 0 false;;\r
@@ -174,14 +168,13 @@ print_endline ("-- SUBST " ^ string_of_t (V v) ^ " |-> " ^ string_of_t t);
  {p with\r
   div=subst sub p.div;\r
   conv=subst sub p.conv;\r
-  stepped=v::p.stepped;\r
   sigma=sub::p.sigma}\r
 ;;\r
 \r
 let get_subterms_with_head hd_var =\r
  let rec aux lev inert_done = function\r
- | C | V _ | B -> []\r
  | L t -> aux (lev+1) false t\r
+ | C | V _ -> []\r
  | A(t1,t2) as t ->\r
    let hd_var', n_args' = get_inert t1 in\r
    if not inert_done && hd_var' = V (hd_var + lev)\r
@@ -195,7 +188,6 @@ let rec purify = function
  | A (t1,t2) -> Pure.A (purify t1, purify t2)\r
  | V n -> Pure.V n\r
  | C -> Pure.V (min_int/2)\r
- | B -> Pure.B\r
 ;;\r
 \r
 let check p sigma =\r
@@ -214,9 +206,6 @@ let check p sigma =
 \r
 let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\r
- 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
  (* Trailing constant args can be removed because do not contribute to eta-diff *)\r
  let rec remove_trailing_constant_args = function\r
@@ -265,7 +254,6 @@ let compute_max_lambdas_at hd_var j =
       else id) (max (aux hd t1) (aux hd t2))\r
  | L t -> aux (hd+1) t\r
  | V _ | C -> 0\r
- | _ -> assert false\r
  in aux hd_var\r
 ;;\r
 \r
@@ -283,48 +271,11 @@ let smallest_such_that p =
   aux 0\r
 ;;\r
 \r
-(* eat the arguments of the divergent and explode.\r
- It does NOT perform any check, may fail if done unsafely *)\r
-let eat p =\r
-print_cmd "EAT" "";\r
- let var, k = get_inert p.div in\r
- match var with\r
- | C | L _ | B | A _ -> assert false\r
- | V var ->\r
- let phase = p.phase in\r
- let p =\r
-  match phase with\r
-  | `One ->\r
-      let i =\r
-       match smallest_such_that (fun x -> not (is_constant x)) (args_of_inert p.div) with\r
-          Some i -> i\r
-        | None -> assert false (*CSC: backtrack? *) in\r
-      let n = 1 + max\r
-       (compute_max_lambdas_at var (k-i-1) p.div)\r
-       (compute_max_lambdas_at var (k-i-1) p.conv) in\r
-      (* apply fresh vars *)\r
-      let p, t = fold_nat (fun (p, t) _ ->\r
-        let p, v = freshvar p in\r
-        p, A(t, V (v + k))\r
-      ) (p, V (k-1-i)) n in\r
-      let p = {p with phase=`Two} in\r
-      let t = A(t, delta) in\r
-      let t = fold_nat (fun t m -> if k-m = i then t else  A(t, V (k-m))) t k in\r
-      let subst = var, mk_lams t k in\r
-      let p = subst_in_problem subst p in\r
-      let _, args = get_inert p.div in\r
-      {p with div = inert_cut_at (args-k) p.div}\r
-  | `Two ->\r
-      let subst = var, mk_lams delta k in\r
-      subst_in_problem subst p in\r
- sanity p\r
-;;\r
-\r
 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
 let step k n p =\r
  let hd, _ = get_inert p.div in\r
  match hd with\r
- | C | L _ | B | A _  -> assert false\r
+ | C | L _ | A _  -> assert false\r
  | V var ->\r
 print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (on " ^ string_of_int (k+1) ^ "th)");\r
  let p, t = (* apply fresh vars *)\r
@@ -374,7 +325,6 @@ print_cmd "FINISH" "";
  let m, delta_var = aux div_nargs p.div in\r
  let p = subst_in_problem (delta_var, delta) p in\r
  let p = subst_in_problem (div_hd, mk_lams delta (m-1)) p in\r
- let p = {p with phase=`Two} in\r
  sanity p\r
 ;;\r
 \r
@@ -382,7 +332,7 @@ let auto p =
  let rec aux p =\r
  let hd, n_args = get_inert p.div in\r
  match hd with\r
- | C | L _ | B | A _  -> assert false\r
+ | C | L _ | A _  -> assert false\r
  | V hd_var ->\r
  let tms = get_subterms_with_head hd_var p.conv in\r
  if List.exists (fun t -> snd (get_inert t) >= n_args) tms\r
@@ -408,13 +358,6 @@ let auto p =
      raise (Fail(-1, "no similar terms"))\r
    )\r
   else\r
-    (*\r
-    (let phase = p.phase in\r
-     let p = eat p in\r
-     if phase = `Two\r
-      then problem_fail p "Auto.2 did not complete the problem"\r
-      else aux p)\r
-      *)\r
     problem_fail (finish p) "Finish did not complete the problem"\r
   in\r
   try\r
@@ -425,19 +368,19 @@ let auto p =
 let problem_of (label, div, convs, ps, var_names) =\r
  print_hline ();\r
  let rec aux lev = function\r
- | `Lam(_, t) -> L (aux (lev+1) t)\r
- | `I (v, args) -> Listx.fold_left (fun x y -> mk_app x (aux lev y)) (aux lev (`Var v)) args\r
+ | `Lam(_, t) -> L (aux (lev+1) t, [])\r
+ | `I (v, args) -> Listx.fold_left (fun x y -> fst (mk_app x (aux lev y))) (aux lev (`Var v)) args\r
  | `Var(v,_) -> if v >= lev && List.nth var_names (v-lev) = "C" then C else V v\r
  | `N _ | `Match _ -> assert false in\r
  assert (List.length ps = 0);\r
  let convs = List.rev convs in\r
- let conv = List.fold_left (fun x y -> mk_app x (aux 0 (y :> Num.nf))) (V (List.length var_names)) convs in\r
+ let conv = List.fold_left (fun x y -> fst (mk_app x (aux 0 (y :> Num.nf)))) (V (List.length var_names)) convs in\r
  let var_names = "@" :: var_names in\r
  let div = match div with\r
  | Some div -> aux 0 (div :> Num.nf)\r
  | None -> assert false in\r
  let varno = List.length var_names in\r
- {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One}\r
+ {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]}\r
 ;;\r
 \r
 let solve p =\r