Clean-up step function; move code

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 93d69a83d9e82bcec96c33c519a86b95f60f66df..bd2ad0919520b15bebb73d849d81413afc02488c 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -1,5 +1,6 @@
 let (++) f g x = f (g x);;\r
 let id x = x;;\r
+let rec fold_nat f x n = if n = 0 then x else f (fold_nat f x (n-1)) n ;;\r
 \r
 let print_hline = Console.print_hline;;\r
 \r
@@ -22,17 +23,8 @@ let eta_eq =
  in aux 0 0\r
 ;;\r
 \r
-type problem = {\r
-   orig_freshno: int\r
- ; freshno : int\r
- ; div : t\r
- ; conv : t\r
- ; sigma : (var * t) list (* substitutions *)\r
- ; stepped : var list\r
-}\r
-\r
-exception Done of (var * t) list (* substitution *);;\r
-exception Fail of int * string;;\r
+(* does NOT lift t *)\r
+let mk_lams = fold_nat (fun x _ -> L x) ;;\r
 \r
 let string_of_t =\r
   let string_of_bvar =\r
@@ -54,6 +46,15 @@ let string_of_t =
   in string_of_term_no_pars 0\r
 ;;\r
 \r
+type problem = {\r
+   orig_freshno: int\r
+ ; freshno : int\r
+ ; div : t\r
+ ; conv : t\r
+ ; sigma : (var * t) list (* substitutions *)\r
+ ; stepped : var list\r
+}\r
+\r
 let string_of_problem p =\r
  let lines = [\r
   "[stepped] " ^ String.concat " " (List.map string_of_int p.stepped);\r
@@ -63,6 +64,9 @@ let string_of_problem p =
  String.concat "\n" lines\r
 ;;\r
 \r
+exception Done of (var * t) list (* substitution *);;\r
+exception Fail of int * string;;\r
+\r
 let problem_fail p reason =\r
  print_endline "!!!!!!!!!!!!!!! FAIL !!!!!!!!!!!!!!!";\r
  print_endline (string_of_problem p);\r
@@ -150,11 +154,7 @@ let print_cmd s1 s2 = print_endline (">> " ^ s1 ^ " " ^ s2);;
 let eat p =\r
 print_cmd "EAT" "";\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
+ let subst = var, mk_lams B n in\r
  let p = subst_in_problem subst p in\r
  sanity p; p\r
 ;;\r
@@ -162,21 +162,15 @@ print_cmd "EAT" "";
 (* step on the head of div, on the k-th argument, with n fresh vars *)\r
 let step k n p =\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
-    else\r
-     let p, v = freshvar p in\r
-     let p, t = aux' p (m-1) t in\r
-      p, A(t, V (v + k + 1)) in\r
- let p, t = aux' p n (V 0) in\r
- let rec aux' m t = if m < 0 then t else A(aux' (m-1) t, V (k-m)) in\r
- let rec aux m t =\r
-  if m < 0\r
-   then aux' (k-1) t\r
-   else L (aux (m-1) t) in\r
- let t = aux k t in\r
+print_cmd "STEP" ("on " ^ string_of_t (V var) ^ " (of:" ^ string_of_int n ^ ")");\r
+ let p, t = (* apply fresh vars *)\r
+  fold_nat (fun (p, t) _ ->\r
+    let p, v = freshvar p in\r
+    p, A(t, V (v + k + 1))\r
+  ) (p, V 0) n in\r
+ let t = (* apply unused bound variables V_{k-1}..V_1 *)\r
+  fold_nat (fun t m -> A(t, V (k-m+1))) t k in\r
+ let t = mk_lams t (k+1) in (* make leading lambdas *)\r
  let subst = var, t in\r
  let p = subst_in_problem subst p in\r
  sanity p; p\r
@@ -266,7 +260,7 @@ let rec auto p =
     (try problem_fail (eat p) "Auto did not complete the problem"  with Done _ -> ())\r
  | Some t ->\r
   let j = find_eta_difference p t n_args - 1 in\r
-  let k = max\r
+  let k = 1 + max\r
    (compute_max_lambdas_at hd_var j p.div)\r
     (compute_max_lambdas_at hd_var j p.conv) in\r
   let p = step j k p in\r
@@ -309,11 +303,11 @@ let auto' a b = auto (problem_of a (conv_join b));;
 exec\r
  "x x"\r
  (conv_join["x y"; "y y"; "y x"])\r
- [ step 0 0; eat ]\r
+ [ step 0 1; eat ]\r
 ;;\r
 \r
 interactive "x y"\r
- "@ (x x) (y x) (y z)" [step 0 0; step 0 1; eat]\r
+ "@ (x x) (y x) (y z)" [step 0 1; step 0 2; eat]\r
 ;;\r
 \r
 *)\r