Moved function, fix indentation, removed parsing of bombs

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index bd2ad0919520b15bebb73d849d81413afc02488c..8535988b7c48fc490342951fd68691f460897811 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -87,6 +87,11 @@ let rec is_inert =
 let is_var = function V _ -> true | _ -> false;;\r
 let is_lambda = function L _ -> true | _ -> false;;\r
 \r
+let rec no_leading_lambdas = function\r
+ | L t -> 1 + no_leading_lambdas t\r
+ | _ -> 0\r
+;;\r
+\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
@@ -182,22 +187,16 @@ let parse strs =
   | Parser_andrea.App (t1, t2) ->\r
    if level = 0 then mk_app (aux level t1) (aux level t2)\r
     else A(aux level t1, aux level t2)\r
-  | Parser_andrea.Var v -> V v\r
-  in let (tms, free) = Parser_andrea.parse_many strs\r
-  in (List.map (aux 0) tms, free)\r
+  | Parser_andrea.Var v -> V v in\r
+  let (tms, free) = Parser_andrea.parse_many strs in\r
+  (List.map (aux 0) tms, free)\r
 ;;\r
 \r
 let problem_of div conv =\r
  print_hline ();\r
- let all_tms, var_names = parse ([div; conv]) in\r
- let div, conv = List.hd all_tms, List.hd (List.tl all_tms) in\r
+ let [@warning "-8"] [div; conv], var_names = parse ([div; conv]) in\r
  let varno = List.length var_names in\r
  let p = {orig_freshno=varno; freshno=1+varno; div; conv; sigma=[]; stepped=[]} in\r
- (* activate bombs *)\r
- let p = try\r
-  let subst = Util.index_of "BOMB" var_names, L B in\r
-   subst_in_problem subst p\r
-  with Not_found -> p in\r
  (* initial sanity check *)\r
  sanity p; p\r
 ;;\r
@@ -210,6 +209,7 @@ let exec div conv cmds =
  | Done _ -> ()\r
 ;;\r
 \r
+(* drops the arguments of t after the n-th *)\r
 let inert_cut_at n t =\r
  let rec aux t =\r
   match t with\r
@@ -233,11 +233,6 @@ let find_eta_difference p t n_args =
  in aux p.div t n_args\r
 ;;\r
 \r
-let rec no_leading_lambdas = function\r
- | L t -> 1 + no_leading_lambdas t\r
- | _ -> 0\r
-;;\r
-\r
 let compute_max_lambdas_at hd_var j =\r
  let rec aux hd = function\r
  | A(t1,t2) ->\r