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

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index acfec515c9ea75b6cca5f2b7678163e656fb97b0..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 =
@@ -110,7 +111,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
   | [] -> acc
   | t::todo_ps ->
 (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
-     let t = subst false x inst (t :> nf) in
+     let t = subst false false x inst (t :> nf) in
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
      let freshno,new_t,acc_new_ps =
       expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t
@@ -124,7 +125,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
    | t::todo_conv ->
 (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
       (* try *)
-       let t = subst false x inst (t :> nf) in
+       let t = subst false false x inst (t :> nf) in
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
        let freshno,new_t,acc_new_ps =
         expand_match (freshno,ps,acc_new_ps) t
@@ -137,7 +138,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
    function
    | None -> freshno, None, acc_new_ps
    | Some t ->
-      let t = subst false x inst (t :> nf) in
+      let t = subst false false x inst (t :> nf) in
       let freshno,new_t,acc_new_ps =
        expand_match (freshno,ps,acc_new_ps) t
       in
@@ -151,7 +152,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
          match u with
          | `N i -> acc_new_ps,i
          | _ ->
-            let ps = List.map (fun t -> cast_to_i_num_var (subst false x inst (t:> nf))) (acc_ps@acc_new_ps) in
+            let ps = List.map (fun t -> cast_to_i_num_var (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
             let super_simplified_ps = super_simplify_ps ps ps in
 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;
@@ -419,17 +420,19 @@ 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");
- (* AC: FIXME compute arities correctly below! *)
- let arities = Num.compute_arities x (n+1) (all_terms p :> nf list) 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 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 p,zero = make_fresh_var p in *)
- (* let zero = Listx.Nil zero in *)
- (* let args = if n = 0 then zero else Listx.append zero (Listx.from_list vars) in *)
  let args = Listx.from_list (vars :> nf list) in
  let bs = ref [] in
- let inst = `Lam(false,`Match(`I((0,0),Listx.map (lift 1) args),(x,arity_of_x),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
 ;;
@@ -727,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 *)
@@ -742,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;;