From a5d76aabf64c2226b8bd8084be02f140f48c767b Mon Sep 17 00:00:00 2001 From: acondolu Date: Thu, 13 Jul 2017 18:24:07 +0200 Subject: [PATCH] Added safety check for step on n-th argument with n > 1 Avoid stepping on n if there is a div/number that would be turned into a Lambda --- ocaml/lambda4.ml | 22 ++++++++++++++-------- 1 file changed, 14 insertions(+), 8 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index e9aa59d..ead0b54 100644 --- a/ocaml/lambda4.ml +++ b/ocaml/lambda4.ml @@ -480,14 +480,19 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l)) else `Continue p + +let safe_arity_of_var p x = + (* Compute the minimum number of arguments when x is in head + position at p.div or p.ps *) + let aux = function + | `Var(y,_) -> if x = y then 0 else max_int + | `I((y,_),args) -> if x = y then Listx.length args else max_int + | _ -> max_int in + let tms = ((match p.div with None -> [] | Some t -> [(t :> i_n_var)]) @ p.ps) in + List.fold_left (fun acc t -> Pervasives.min acc (aux t)) max_int tms +;; + let instantiate p x perm n = - let arity_of_x = max_arity_tms x (all_terms p) in - (if arity_of_x = None then failwithProblem p "step on var non occurring in problem"); - let arity_of_x = Util.option_get(arity_of_x) in - (if arity_of_x = min_int then failwithProblem p "step on fake variable"); - (if arity_of_x <= 0 then failwithProblem p "step on var of non-positive arity"); - (if perm < 1 || perm > arity_of_x then - failwithProblem p ("Tried to permutate variable "^ string_of_var x ^" beyond its max arity")); let n = (prerr_endline "WARNING: using constant initialSpecialK"); p.initialSpecialK in let arities = Array.to_list (Array.make (n+1) min_int) in let p,vars = make_fresh_vars p arities in @@ -575,7 +580,8 @@ in*) if special_k < n then prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@"); let arity_of_x = Util.option_get (max_arity_tms x (all_terms p)) in - x,arity_of_x,special_k + let safe_arity_of_x = safe_arity_of_var p x in + x, min arity_of_x safe_arity_of_x, special_k let rec auto_eat (n,p) = prerr_endline "{{{{{{{{ Computing measure before auto_instantiate }}}}}}"; -- 2.39.2