X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=95b036c8390ecab479cff47425467e546c1768fc;hb=588a00cd5ae861a2f366df992f758f285265a34a;hp=570691e1be16101622515e0d8c55a70bceda31bc;hpb=eb8bb784b35d303a1c239f30008cba79f658f4b3;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 570691e..95b036c 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -454,77 +454,82 @@ 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
+ (* other_vars are the variables which are delayed and re-applied to the match *)
+ let other_vars = Array.mapi (fun n () -> `Var(n+1,min_int)) (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
 ;;
 
 let compute_special_k tms =
-  let rec aux k (t: nf) = Pervasives.max k (match t with
-    | `Lam(b,t) -> aux (k + if b then 1 else 0) t
-    | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
-    | `Match(t, _, liftno, bs, args) ->
-        List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
-    | `N _ -> 0
-    | `Var _ -> 0
-  ) in Listx.max (Listx.map (aux 0) tms)
+ let rec aux k (t: nf) = Pervasives.max k (match t with
+ | `Lam(b,t) -> aux (k + if b then 1 else 0) t
+ | `I(n, tms) -> Listx.max (Listx.map (aux 0) tms)
+ | `Match(t, _, liftno, bs, args) ->
+     List.fold_left max 0 (List.map (aux 0) ((t :> nf)::args@List.map snd !bs))
+ | `N _
+ | `Var _ -> 0
+ ) in Listx.max (Listx.map (aux 0) tms)
 ;;
 
 let auto_instantiate (n,p) =
-  let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
+ let p, showstoppers_step, showstoppers_eat = critical_showstoppers p in
  let x =
   match showstoppers_step, showstoppers_eat with
-    | [], y::_ ->
-      prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
-    | [], [] ->
+  | [], y::_ ->
+     prerr_endline ("INSTANTIATING CRITICAL TO EAT " ^ string_of_var y); y
+  | [], [] ->
      let heads =
       (* Choose only variables still alive (with arity > 0) *)
       List.sort compare (filter_map (
        fun t -> match t with `Var _ -> None | x -> if arity_of_hd x <= 0 then None else hd_of x
       ) ((match p.div with Some t -> [(t :> i_n_var)] | _ -> []) @ p.ps)) in
      (match heads with
-         [] -> (
-          try
+      | [] ->
+         (try
            fst (List.find (((<) 0) ++ snd) (concat_map free_vars' (p.conv :> nf list)))
           with
-           Not_found -> assert false
-          )
-       | x::_ ->
-          prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
-          x)
+           Not_found -> assert false)
+      | x::_ ->
+         prerr_endline ("INSTANTIATING TO EAT " ^ string_of_var x);
+         x)
   | x::_, _ ->
       prerr_endline ("INSTANTIATING " ^ string_of_var x);
       x in
 (* Strategy that  decreases the special_k to 0 first (round robin)
 1:11m42 2:14m5 3:11m16s 4:14m46s 5:12m7s 6:6m31s *)
-let x =
- try
-  match hd_of (List.find (fun t ->
-   compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
-   ) (all_terms p)) with
-      None -> assert false
+ let x =
+  try
+   match
+    hd_of (List.find (fun t ->
+     compute_special_k (Listx.Nil (t :> nf)) > 0 && arity_of_hd t > 0
+     ) (all_terms p))
+   with
+    | None -> assert false
     | Some x ->
        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
        x
- with
-  Not_found -> x
-in
+  with
+   Not_found -> x in
 (* Instantiate in decreasing order of compute_special_k
 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s
 let x =
@@ -541,7 +546,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
 
 
@@ -550,25 +555,23 @@ let rec auto_eat (n,p) =
  let m = problem_measure p in
  let (n,p') = auto_instantiate (n,p) in
  match eat p' with
-   `Finished p -> p
+ | `Finished p -> p
  | `Continue p ->
      prerr_endline "{{{{{{{{ Computing measure inafter auto_instantiate }}}}}}";
-     let m' = problem_measure p in
-     let delta = compare m m' in
-     print_endline ("compare " ^ string_of_measure m' ^ " " ^ string_of_measure m ^ "= " ^ string_of_int delta);
+     let delta = problem_measure p - m in
      (* let delta = m - problem_measure p' in *)
-     if delta <= 0 then (
-      failwith
-      (* prerr_endline *)
-      ("Measure did not decrease (delta=" ^ string_of_int delta ^ ")"))
-     else prerr_endline ("$ Measure decreased by " ^ string_of_int delta);
+     if delta >= 0
+      then
+       (failwith
+       ("Measure did not decrease (+=" ^ string_of_int delta ^ ")"))
+      else prerr_endline ("$ Measure decreased of " ^ string_of_int delta);
      auto_eat (n,p)
 ;;
 
 let auto p n =
  prerr_endline ("@@@@ FIRST INSTANTIATE PHASE (" ^ string_of_int n ^ ") @@@@");
  match eat p with
-   `Finished p -> p
+ | `Finished p -> p
  | `Continue p -> auto_eat (n,p)
 ;;
 
@@ -680,7 +683,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