From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 11 Jul 2017 14:36:23 +0000 (+0200)
Subject: instantiate takes an additional argument which is the number of the argument to the... 
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=83ecb91196b7e8e351e9a8fb43653f67ae9867fc;p=fireball-separation.git

instantiate takes an additional argument which is the number of the argument to the variable on which to step
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 570691e..f95ddce 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -454,23 +454,32 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
  else
   `Continue p
 
-let instantiate p x n =
+let instantiate p x perm 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 = 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");
+ 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
- (* 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 *)
  let arities = Array.to_list (Array.make (n+1) min_int) in
  let p,vars = make_fresh_vars p arities in
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
+ (* AC FIXME:
+    1) what is arity of other_vars?
+    2) are lambdas true or false?
+ *)
+ (* other_vars are the variables which are delayed and re-applied to the match *)
+ let other_vars = Array.mapi (fun n () -> `Var(n+1,-666)) (Array.make (perm-1) ()) in
+ let other_vars = Array.to_list other_vars in
  (* 666, since it will be replaced anyway during subst: *)
- let inst = `Lam(false,`Match(`I((0,min_int),Listx.map (lift 1) args),(x,666),1,bs,[])) in
+ let inst = `Match(`I((0,min_int),Listx.map (lift perm) args),(x,-666),perm,bs,other_vars) in
+ (* Add a number of 'perm' leading lambdas *)
+ let inst = Array.fold_left (fun t () -> `Lam(false, t)) inst (Array.make perm ()) in
  let p = {p with deltas=bs::p.deltas} in
  subst_in_problem x inst p
 ;;
@@ -541,7 +550,7 @@ in*)
      compute_special_k (Listx.from_list (all_terms p :> nf list) )in
  if special_k < n then
   prerr_endline ("@@@@ NEW INSTANTIATE PHASE (" ^ string_of_int special_k ^ ") @@@@");
- let p = instantiate p x special_k in
+ let p = instantiate p x 1 special_k in
  special_k,p
 
 
@@ -680,7 +689,7 @@ let main problems =
     | `DoneWith -> assert false (*aux (eat p) n l*) (* CSC: TODO *)
     | `Step x ->
         let x = var_of_string x in
-        aux (instantiate p x n) n l
+        aux (instantiate p x 1 n) n l
     | `Auto -> aux (auto p n) n l
  in
   List.iter