Instantiate now uses a global initialSpecialK (ignoring the local one)

This fixes the bug in the previous commit, and makes the problem pass

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 304df8a9300615f58af67cd7bae1668da62b9a48..77449b4681a7887cde71c8cbd170588b8a53241a 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -12,6 +12,7 @@ type problem =
  ; ps: i_n_var list (* the n-th inert must become n *)
  ; sigma: (int * nf) list (* the computed substitution *)
  ; deltas: (int * nf) list ref list (* collection of all branches *)
+ ; initialSpecialK: int
 };;
 
 let all_terms p =
@@ -422,6 +423,7 @@ let instantiate p x n =
  (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 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 *)
@@ -728,7 +730,7 @@ let magic_conv ~div ~conv ~nums cmds =
  if match div with None -> false | Some div -> List.exists (eta_subterm div) (tms@conv)
  then (
   prerr_endline "--- TEST SKIPPED ---";
-  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]}, 0, []
+  {freshno=0; div=None; conv=[]; ps=[]; sigma=[]; deltas=[]; initialSpecialK=0}, 0, []
  ) else
   let tms = sort_uniq ~compare:eta_compare tms in
   let special_k = compute_special_k (Listx.from_list all_tms) in (* compute initial special K *)
@@ -743,7 +745,7 @@ let magic_conv ~div ~conv ~nums cmds =
    let dummy = `Var (max_int / 2, -666) in
     [ ref (Array.to_list (Array.init (List.length ps) (fun i -> i, dummy))) ] in
 
-  {freshno; div; conv; ps; sigma=[] ; deltas}, special_k, cmds
+  {freshno; div; conv; ps; sigma=[] ; deltas; initialSpecialK=special_k}, special_k, cmds
 ;;
 
 let magic strings cmds = magic_conv None [] strings cmds;;