From 08d2b663e5089ed046ef771bfb2555a31e525f1c Mon Sep 17 00:00:00 2001 From: acondolu Date: Mon, 10 Jul 2017 14:43:43 +0200 Subject: [PATCH] Instantiate now uses a global initialSpecialK (ignoring the local one) This fixes the bug in the previous commit, and makes the problem pass --- ocaml/lambda4.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml index 304df8a..77449b4 100644 --- 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;; -- 2.39.2