From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 12:17:18 +0000 (+0200)
Subject: Moved function, fix indentation, removed parsing of bombs
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=8b5b0fe4101dc977d7c9257e59af49ac32c674d1;p=fireball-separation.git

Moved function, fix indentation, removed parsing of bombs
---

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 6317e65..24db4c9 100644
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -87,6 +87,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
@@ -182,22 +187,16 @@ let parse strs =
   | Parser.App (t1, t2) ->
    if level = 0 then mk_app (aux level t1) (aux level t2)
     else A(aux level t1, aux level t2)
-  | Parser.Var v -> V v
-  in let (tms, free) = Parser.parse_many strs
-  in (List.map (aux 0) tms, free)
+  | Parser.Var v -> V v in
+  let (tms, free) = Parser.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
  (* initial sanity check *)
  sanity p; p
 ;;
@@ -210,6 +209,7 @@ let exec div conv cmds =
  | Done _ -> ()
 ;;
 
+(* drops the arguments of t after the n-th *)
 let inert_cut_at n t =
  let rec aux t =
   match t with
@@ -233,11 +233,6 @@ let find_eta_difference p t n_args =
  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) ->