Clean up

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 0edd1b2586ee5dfee7141b8b59aff2901b3c1255..95c6a6a649178a295f524388fcfdab5271ebfc60 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -35,24 +35,23 @@ type problem = {
 exception Done of (var * t) list (* substitution *);;\r
 exception Fail of int * string;;\r
 \r
-let string_of_t p =\r
-  let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
+let string_of_t =\r
+  let string_of_bvar =\r
+   let bound_vars = ["x"; "y"; "z"; "w"; "q"] in\r
+   let bvarsno = List.length bound_vars in\r
+   fun nn -> if nn < bvarsno then List.nth bound_vars nn else "x" ^ (string_of_int (nn - bvarsno + 1)) in\r
   let rec string_of_term_w_pars level = function\r
     | V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
-     let nn = level - v-1 in\r
-      if nn < 5 then List.nth bound_vars nn else "x" ^ (string_of_int (nn-4))\r
+       string_of_bvar (level - v-1)\r
     | A _\r
-    | L _ as t -> "(" ^ string_of_term_no_pars_lam level t ^ ")"\r
+    | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
     | B -> "BOT"\r
     | P -> "PAC"\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
+    | 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
-  and string_of_term_no_pars_lam level = function\r
-    | L t -> "λ" ^ string_of_term_w_pars (level+1) (V 0) ^ ". " ^ (string_of_term_no_pars_lam (level+1) t)\r
-    | _ as t -> string_of_term_no_pars level t\r
   and string_of_term_no_pars level = function\r
-    | L _ as t -> string_of_term_no_pars_lam level t\r
+    | L t -> "λ" ^ string_of_bvar level ^ ". " ^ string_of_term_no_pars (level+1) t\r
     | _ as t -> string_of_term_no_pars_app level t\r
   in string_of_term_no_pars 0\r
 ;;\r
@@ -60,8 +59,8 @@ let string_of_t p =
 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 p.div);\r
-  "[CV] " ^ (string_of_t p p.conv);\r
+  "[DV] " ^ string_of_t p.div;\r
+  "[CV] " ^ string_of_t p.conv;\r
  ] in\r
  String.concat "\n" lines\r
 ;;\r
@@ -86,15 +85,9 @@ let rec is_inert =
 let is_var = function V _ -> true | _ -> false;;\r
 let is_lambda = function L _ -> true | _ -> false;;\r
 \r
-let rec head_of_inert = function\r
- | V n -> n\r
- | A(t, _) -> head_of_inert t\r
- | _ -> assert false\r
-;;\r
-\r
-let rec args_no = function\r
- | V _ -> 0\r
- | A(t, _) -> 1 + args_no t\r
+let rec get_inert = function\r
+ | V n -> (n,0)\r
+ | A(t, _) -> let hd,args = get_inert t in hd,args+1\r
  | _ -> assert false\r
 ;;\r
 \r
@@ -105,7 +98,7 @@ let rec subst level delift sub =
  | A (t1,t2) ->\r
   let t1 = subst level delift sub t1 in\r
   let t2 = subst level delift sub t2 in\r
-  if t1 = B || t2 = B then B else mk_app t1 t2\r
+  mk_app t1 t2\r
  | B -> B\r
  | P -> P\r
 and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with\r
@@ -113,11 +106,11 @@ and mk_app t1 t2 = let t1 = if t1 = P then L P else t1 in match t1 with
  | L t1 -> subst 0 true (0, t2) t1\r
  | t1 -> A (t1, t2)\r
 and lift n =\r
- let rec aux n' =\r
+ let rec aux lev =\r
   function\r
-  | V m -> V (if m >= n' then m + n else m)\r
-  | L t -> L (aux (n'+1) t)\r
-  | A (t1, t2) -> A (aux n' t1, aux n' t2)\r
+  | 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
   | B -> B\r
   | P -> P\r
  in aux 0\r
@@ -125,13 +118,12 @@ and lift n =
 let subst = subst 0 false;;\r
 \r
 let subst_in_problem (sub: var * t) (p: problem) =\r
-print_endline ("-- SUBST " ^ string_of_t p (V (fst sub)) ^ " |-> " ^ string_of_t p (snd sub));\r
- let p = {p with stepped=(fst sub)::p.stepped} in\r
- let conv = subst sub p.conv in\r
- let div = subst sub p.div in\r
- let p = {p with div; conv} in\r
- (* print_endline ("after sub: \n" ^ string_of_problem p); *)\r
- {p with sigma=sub::p.sigma}\r
+print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (snd sub));\r
+ {p with\r
+  div=subst sub p.div;\r
+  conv=subst sub p.conv;\r
+  stepped=(fst sub)::p.stepped;\r
+  sigma=sub::p.sigma}\r
 ;;\r
 \r
 let get_subterm_with_head_and_args hd_var n_args =\r
@@ -139,7 +131,8 @@ let get_subterm_with_head_and_args hd_var n_args =
  | V _ | B | P -> None\r
  | L t -> aux (lev+1) t\r
  | A(t1,t2) as t ->\r
-   if head_of_inert t1 = hd_var + lev && n_args <= 1 + args_no t1 (* why `1+' ?*)\r
+   let hd_var', n_args' = get_inert t1 in\r
+   if hd_var' = hd_var + lev && n_args <= 1 + n_args'\r
     then Some (lift ~-lev t)\r
     else match aux lev t2 with\r
     | None -> aux lev t1\r
@@ -156,11 +149,9 @@ let get_subterm_with_head_and_args hd_var n_args =
 \r
 let sanity p =\r
  print_endline (string_of_problem p); (* non cancellare *)\r
- if p.div = B then raise (Done p.sigma);\r
- if not (is_inert p.div) then problem_fail p "p.div converged";\r
  if p.conv = B then problem_fail p "p.conv diverged";\r
- (* let p = if is_var p.div then simple_explode p else p in *)\r
- p\r
+ if p.div = B then raise (Done p.sigma);\r
+ if not (is_inert p.div) then problem_fail p "p.div converged"\r
 ;;\r
 \r
 let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;\r
@@ -169,20 +160,20 @@ let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
  It does NOT perform any check, may fail if done unsafely *)\r
 let eat p =\r
 print_cmd "EAT" "";\r
- let var = head_of_inert p.div in\r
- let n = args_no p.div in\r
+ let var, n = get_inert p.div in\r
  let rec aux m t =\r
   if m = 0\r
    then lift n t\r
    else L (aux (m-1) t) in\r
  let subst = var, aux n B in\r
- sanity (subst_in_problem subst p)\r
+ let p = subst_in_problem subst p in\r
+ sanity p; 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 var = head_of_inert p.div in\r
- print_cmd "STEP" ("on " ^ string_of_t p (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let var, _ = get_inert p.div in\r
+ print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
  let rec aux' p m t =\r
   if m < 0\r
    then p, t\r
@@ -198,7 +189,8 @@ let step k n p =
    else L (aux (m-1) t) in\r
  let t = aux k t in\r
  let subst = var, t in\r
- sanity (subst_in_problem subst p)\r
+ let p = subst_in_problem subst p in\r
+ sanity p; p\r
 ;;\r
 \r
 let parse strs =\r
@@ -230,7 +222,7 @@ let problem_of div conv =
    (print_endline ("after subst in problem " ^ string_of_problem p); p)\r
   with Not_found -> p in\r
  (* initial sanity check *)\r
- sanity p\r
+ sanity p; p\r
 ;;\r
 \r
 let exec div conv cmds =\r
@@ -258,7 +250,7 @@ let find_eta_difference p t n_args =
  let rec aux t u k = match t, u with\r
  | V _, V _ -> assert false (* div subterm of conv *)\r
  | A(t1,t2), A(u1,u2) ->\r
-    if not (eta_eq t2 u2) then (print_endline((string_of_t p t2) ^ " <> " ^ (string_of_t p u2)); k)\r
+    if not (eta_eq t2 u2) then (print_endline((string_of_t t2) ^ " <> " ^ (string_of_t u2)); k)\r
     else aux t1 u1 (k-1)\r
  | _, _ -> assert false\r
  in aux p.div t n_args\r
@@ -272,10 +264,10 @@ let rec no_leading_lambdas = function
 let compute_max_lambdas_at hd_var j =\r
  let rec aux hd = function\r
  | A(t1,t2) ->\r
-    (if head_of_inert t1 = hd && args_no t1 = j\r
-      then max (\r
-       if is_inert t2 && head_of_inert t2 = hd\r
-        then j - args_no t2\r
+    (if get_inert t1 = (hd, j)\r
+      then max ( (*FIXME*)\r
+       if is_inert t2 && let hd', j' = get_inert t2 in hd' = hd\r
+        then let hd', j' = get_inert t2 in j - j'\r
         else no_leading_lambdas t2)\r
       else id) (max (aux hd t1) (aux hd t2))\r
  | L t -> aux (hd+1) t\r
@@ -285,8 +277,7 @@ let compute_max_lambdas_at hd_var j =
 ;;\r
 \r
 let rec auto p =\r
- let hd_var = head_of_inert p.div in\r
- let n_args = args_no p.div in\r
+ let hd_var, n_args = get_inert p.div in\r
  match get_subterm_with_head_and_args hd_var n_args p.conv with\r
  | None ->\r
     (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())\r