From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 9 Jun 2018 08:19:56 +0000 (+0200)
Subject: Removed eat, p.stepped, p.phase and t.B
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=69f44e4fb3d56f89adcc952514707914886fdd79;p=fireball-separation.git

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

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