Fixed: was using compare in place of eta_eq

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 6ceb9f387d516d401301f821c8d3e6cb16960f54..ed43936638020efe31958242c0edd27b11834f60 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -113,7 +113,7 @@ let make_fresh_vars p arities =
 
 let simple_expand_match ps =
  let rec aux_nob level = function
-  | #i_num_var as t -> aux_i_num_var level t
+  | #i_num_var as t -> (aux_i_num_var level t :> nf)
   | `Lam(b,t) -> `Lam(b,aux (level+1) t)
   | `Pacman as t -> t
  and aux level = function
@@ -121,20 +121,20 @@ let simple_expand_match ps =
   | #nf_nob as t -> aux_nob level t
  and aux_i_num_var level = function
   | `Match(u,v,bs_lift,bs,args) as torig ->
-    let u = aux_i_num_var level u in
+    let (u : i_num_var) = aux_i_num_var level u in
     bs := List.map (fun (n, x) -> n, aux 0 x) !bs;
     (try
        (match u with
          | #i_n_var as u ->
-            let i = index_of (lift (-level) u) (ps :> nf list) (* can raise Not_found *)
-            in let t = mk_match (`N i) v bs_lift bs (args :> nf list) in
+            let i = index_of ~eq:eta_eq (lift (-level) u) (ps :> nf list) in (* can raise Not_found *)
+            let t = cast_to_i_num_var (mk_match (`N i) v bs_lift bs (args :> nf list)) in
             if t <> torig then
-            aux level (t :> nf)
-           else raise Not_found
+             aux_i_num_var level t
+            else raise Not_found
          | _ -> raise Not_found)
       with Not_found ->
-       mk_appl (`Match(cast_to_i_num_var u,v,bs_lift,bs,[])) (List.map (aux_nob level) args))
-  | `I(v,args) -> mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args))
+       cast_to_i_num_var (mk_appl (`Match(u,v,bs_lift,bs,[])) (List.map (aux_nob level) args)))
+  | `I(v,args) -> cast_to_i_num_var (mk_appl (`Var v) (List.map (aux_nob level) (Listx.to_list args)))
   | `N _ | `Var _ as t -> t
  in aux_i_num_var 0
 ;;
@@ -157,7 +157,7 @@ let super_simplify ({div; ps; conv} as p) =
   let div = option_map (fun div ->
    let divs = super_simplify_ps p.ps ([div] :> i_n_var list) in
     List.hd divs) div in
-  {p with div=option_map cast_to_i_var div; ps=List.map cast_to_i_n_var ps; conv=List.map cast_to_i_n_var conv}
+  {p with div=option_map cast_to_i_var div; ps; conv}
 
 let cast_to_ps_with_match =
  function
@@ -573,7 +573,7 @@ let choose_step (n,p) =
   with
    Not_found ->
     let arity_of_x = max_arity_tms x (all_terms p) in
-    assert (Util.option_get arity_of_x > 0); 
+    assert (Util.option_get arity_of_x > 0);
     x in
 (* Instantiate in decreasing order of compute_special_k
 1:15m14s 2:13m14s 3:4m55s 4:4m43s 5:4m34s 6:6m28s 7:3m31s