From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 13 Jul 2017 16:24:07 +0000 (+0200)
Subject: Added safety check for step on n-th argument with n > 1
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a5d76aabf64c2226b8bd8084be02f140f48c767b;p=fireball-separation.git

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
---

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 }}}}}}";