X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Fandrea.ml;h=07cf670c134c75c5787c332302ca1b8c265fa186;hb=ade21b2ea3af70e54e030c62f8b46a996f9ca8fb;hp=93d69a83d9e82bcec96c33c519a86b95f60f66df;hpb=2917b01cd638d1ef0786f085fdf27cb68a183329;p=fireball-separation.git

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 93d69a8..07cf670 100644
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -1,8 +1,11 @@
 let (++) f g x = f (g x);;
 let id x = x;;
+let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;
 
 let print_hline = Console.print_hline;;
 
+open Pure
+
 type var = int;;
 type t =
  | V of var
@@ -11,6 +14,8 @@ type t =
  | B (* bottom *)
 ;;
 
+let delta = L(A(V 0, V 0));;
+
 let eta_eq =
  let rec aux l1 l2 t1 t2 = match t1, t2 with
   | L t1, L t2 -> aux l1 l2 t1 t2
@@ -22,17 +27,8 @@ let eta_eq =
  in aux 0 0
 ;;
 
-type problem = {
-   orig_freshno: int
- ; freshno : int
- ; div : t
- ; conv : t
- ; sigma : (var * t) list (* substitutions *)
- ; stepped : var list
-}
-
-exception Done of (var * t) list (* substitution *);;
-exception Fail of int * string;;
+(* does NOT lift t *)
+let mk_lams = fold_nat (fun x _ -> L x) ;;
 
 let string_of_t =
   let string_of_bvar =
@@ -54,6 +50,16 @@ let string_of_t =
   in string_of_term_no_pars 0
 ;;
 
+type problem = {
+   orig_freshno: int
+ ; freshno : int
+ ; 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);
@@ -63,6 +69,9 @@ let string_of_problem p =
  String.concat "\n" lines
 ;;
 
+exception Done of (var * t) list (* substitution *);;
+exception Fail of int * string;;
+
 let problem_fail p reason =
  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";
  print_endline (string_of_problem p);
@@ -83,6 +92,11 @@ let rec is_inert =
 let is_var = function V _ -> true | _ -> false;;
 let is_lambda = function L _ -> true | _ -> false;;
 
+let rec no_leading_lambdas = function
+ | L t -> 1 + no_leading_lambdas t
+ | _ -> 0
+;;
+
 let rec get_inert = function
  | V n -> (n,0)
  | A(t, _) -> let hd,args = get_inert t in hd,args+1
@@ -92,16 +106,17 @@ let rec get_inert = function
 let rec subst level delift sub =
  function
  | V v -> if v = level + fst sub then lift level (snd sub) else V (if delift && v > level then v-1 else v)
- | L t -> L (subst (level + 1) delift sub t)
+ | L t -> let t = subst (level + 1) delift sub t in if t = B then B else L t
  | A (t1,t2) ->
   let t1 = subst level delift sub t1 in
   let t2 = subst level delift sub t2 in
   mk_app t1 t2
  | B -> B
-and mk_app t1 t2 = match t1 with
- | B | _ when t2 = B -> B
+and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B
+ else match t1 with
+ | B -> B
  | L t1 -> subst 0 true (0, t2) t1
- | t1 -> A (t1, t2)
+ | _ -> A (t1, t2)
 and lift n =
  let rec aux lev =
   function
@@ -136,47 +151,111 @@ let get_subterm_with_head_and_args hd_var n_args =
  in aux 0
 ;;
 
+let rec purify = function
+ | L t -> Pure.L (purify t)
+ | A (t1,t2) -> Pure.A (purify t1, purify t2)
+ | V n -> Pure.V n
+ | B -> Pure.B
+;;
+
+let check p sigma =
+ print_endline "Checking...";
+ let div = purify p.div in
+ let conv = purify p.conv in
+ let sigma = List.map (fun (v,t) -> v, purify t) sigma in
+ let freshno = List.fold_right (fun (x,_) -> max x) sigma 0 in
+ let env = Pure.env_of_sigma freshno sigma in
+ assert (Pure.diverged (Pure.mwhd (env,div,[])));
+ assert (not (Pure.diverged (Pure.mwhd (env,conv,[]))));
+ ()
+;;
+
 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"
 ;;
 
+(* drops the arguments of t after the n-th *)
+let inert_cut_at n t =
+ let rec aux t =
+  match t with
+  | V _ as t -> 0, t
+  | A(t1,_) as t ->
+    let k', t' = aux t1 in
+     if k' = n then n, t'
+      else k'+1, t
+  | _ -> assert false
+ in snd (aux t)
+;;
+
+let find_eta_difference p t n_args =
+ let t = inert_cut_at n_args t in
+ let rec aux t u k = match t, u with
+ | V _, V _ -> assert false (* div subterm of conv *)
+ | A(t1,t2), A(u1,u2) ->
+    if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k)
+    else aux t1 u1 (k-1)
+ | _, _ -> assert false
+ in aux p.div t n_args
+;;
+
+let compute_max_lambdas_at hd_var j =
+ let rec aux hd = function
+ | A(t1,t2) ->
+    (if get_inert t1 = (hd, j)
+      then max ( (*FIXME*)
+       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd
+        then let hd', j' = get_inert t2 in j - j'
+        else no_leading_lambdas t2)
+      else id) (max (aux hd t1) (aux hd t2))
+ | L t -> aux (hd+1) t
+ | V _ -> 0
+ | _ -> assert false
+ in aux hd_var
+;;
+
 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
 
 (* 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, n = get_inert p.div in
- let rec aux m t =
-  if m = 0
-   then lift n t
-   else L (aux (m-1) t) in
- let subst = var, aux n B in
+ let var, k = get_inert p.div in
+ let phase = p.phase in
+ let p, t =
+  match phase with
+  | `One ->
+      let n = 1 + max
+       (compute_max_lambdas_at var k p.div)
+       (compute_max_lambdas_at var k 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 0) n in
+      let p = {p with phase=`Two} in p, A(t, delta)
+  | `Two -> p, delta in
+ let subst = var, mk_lams t k in
  let p = subst_in_problem subst p in
+ let p = if phase = `One then {p with div = (match p.div with A(t,_) -> t | _ -> assert false)} else p in
  sanity p; p
 ;;
 
 (* step on the head of div, on the k-th argument, with n fresh vars *)
 let step k n p =
  let var, _ = get_inert p.div in
- print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");
- let rec aux' p m t =
-  if m < 0
-   then p, t
-    else
-     let p, v = freshvar p in
-     let p, t = aux' p (m-1) t in
-      p, A(t, V (v + k + 1)) in
- let p, t = aux' p n (V 0) in
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in
- let rec aux m t =
-  if m < 0
-   then aux' (k-1) t
-   else L (aux (m-1) t) in
- let t = aux k t in
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");
+ let p, t = (* apply fresh vars *)
+  fold_nat (fun (p, t) _ ->
+    let p, v = freshvar p in
+    p, A(t, V (v + k + 1))
+  ) (p, V 0) n in
+ let t = (* apply unused bound variables V_{k-1}..V_1 *)
+  fold_nat (fun t m -> A(t, V (k-m+1))) t k in
+ 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
@@ -188,22 +267,16 @@ let parse strs =
   | Parser_andrea.App (t1, t2) ->
    if level = 0 then mk_app (aux level t1) (aux level t2)
     else A(aux level t1, aux level t2)
-  | Parser_andrea.Var v -> V v
-  in let (tms, free) = Parser_andrea.parse_many strs
-  in (List.map (aux 0) tms, free)
+  | Parser_andrea.Var v -> V v in
+  let (tms, free) = Parser_andrea.parse_many strs in
+  (List.map (aux 0) tms, free)
 ;;
 
 let problem_of div conv =
  print_hline ();
- let all_tms, var_names = parse ([div; conv]) in
- let div, conv = List.hd all_tms, List.hd (List.tl all_tms) in
+ let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in
  let varno = List.length var_names in
- let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in
- (* activate bombs *)
- let p = try
-  let subst = Util.index_of "BOMB" var_names, L B in
-   subst_in_problem subst p
-  with Not_found -> p in
+ let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]; phase=`One} in
  (* initial sanity check *)
  sanity p; p
 ;;
@@ -216,57 +289,20 @@ let exec div conv cmds =
  | Done _ -> ()
 ;;
 
-let inert_cut_at n t =
- let rec aux t =
-  match t with
-  | V _ as t -> 0, t
-  | A(t1,_) as t ->
-    let k', t' = aux t1 in
-     if k' = n then n, t'
-      else k'+1, t
-  | _ -> assert false
- in snd (aux t)
-;;
-
-let find_eta_difference p t n_args =
- let t = inert_cut_at n_args t in
- let rec aux t u k = match t, u with
- | V _, V _ -> assert false (* div subterm of conv *)
- | A(t1,t2), A(u1,u2) ->
-    if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k)
-    else aux t1 u1 (k-1)
- | _, _ -> assert false
- in aux p.div t n_args
-;;
-
-let rec no_leading_lambdas = function
- | L t -> 1 + no_leading_lambdas t
- | _ -> 0
-;;
-
-let compute_max_lambdas_at hd_var j =
- let rec aux hd = function
- | A(t1,t2) ->
-    (if get_inert t1 = (hd, j)
-      then max ( (*FIXME*)
-       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd
-        then let hd', j' = get_inert t2 in j - j'
-        else no_leading_lambdas t2)
-      else id) (max (aux hd t1) (aux hd t2))
- | L t -> aux (hd+1) t
- | V _ -> 0
- | _ -> assert false
- in aux hd_var
-;;
-
 let rec auto p =
  let hd_var, n_args = get_inert p.div in
  match get_subterm_with_head_and_args hd_var n_args p.conv with
  | None ->
-    (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())
+   (try
+    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 auto p
+    with Done sigma -> sigma)
  | Some t ->
   let j = find_eta_difference p t n_args - 1 in
-  let k = max
+  let k = 1 + max
    (compute_max_lambdas_at hd_var j p.div)
     (compute_max_lambdas_at hd_var j p.conv) in
   let p = step j k p in
@@ -302,18 +338,22 @@ let rec conv_join = function
  | x::xs -> conv_join xs ^ " ("^ x ^")"
 ;;
 
-let auto' a b = auto (problem_of a (conv_join b));;
+let auto' a b =
+ let p = problem_of a (conv_join b) in
+ let sigma = auto p in
+ check p sigma
+;;
 
 (* Example usage of exec, interactive:
 
 exec
  "x x"
  (conv_join["x y"; "y y"; "y x"])
- [ step 0 0; eat ]
+ [ step 0 1; eat ]
 ;;
 
 interactive "x y"
- "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat]
+ "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]
 ;;
 
 *)