From ea2c84fbe45361b8e3e13e5eb54d25854d58cf48 Mon Sep 17 00:00:00 2001
From: acondolu <andrea.condoluci@unibo.it>
Date: Wed, 30 May 2018 14:17:18 +0200
Subject: [PATCH] Moved function, fix indentation, removed parsing of bombs
---
ocaml/andrea.ml | 25 ++++++++++---------------
1 file changed, 10 insertions(+), 15 deletions(-)
diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index bd2ad09..8535988 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_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
(* 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) ->
--
2.39.2