Code clean-up

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

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index bc8855d3006462351046fe3fe956aa21fd5d7e8c..788fe5983357dddd15e531364f8203664570ed86 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 (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