new_arity = old_arity + 1

[fireball-separation.git] / ocaml / lambda4.ml

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 8498513a86be7d7a24ad5bc79539414deadc224c..304df8a9300615f58af67cd7bae1668da62b9a48 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -419,7 +419,9 @@ let instantiate p x n =
  (if hd_of_i_var (cast_to_i_var !bomb) = x
    then failwithProblem p ("BOMB (" ^ string_of_nf !bomb ^ ") cannot be instantiated!"));
  let arity_of_x = max_arity_tms x (all_terms p) in
- (if arity_of_x < 0 then failwithProblem p "step on a var of negative arity");
+ (if arity_of_x = None then failwithProblem p "step on var non occurring in problem");
+ (if Util.option_get(arity_of_x) = min_int then failwithProblem p "step on fake variable");
+ (if Util.option_get(arity_of_x) <= 0 then failwithProblem p "step on var of non-positive arity");
  (* AC: Once upon a time, it was:
     let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) in *)
  (* let arities = Array.to_list (Array.make (n+1) 0) in *)
@@ -427,8 +429,8 @@ let instantiate p x n =
  let p,vars = make_fresh_vars p arities in
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
- (* min_int, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,n+1),Listx.map (lift 1) args),(x,min_int),1,bs,[])) in
+ (* 666, since it will be replaced anyway during subst: *)
+ let inst = `Lam(false,`Match(`I((0,n+2),Listx.map (lift 1) args),(x,666),1,bs,[])) in
  let p = {p with deltas=bs::p.deltas} in
  subst_in_problem x inst p
 ;;