; 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 =
(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");
+ 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 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
;;
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 *)
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;;