From: acondolu <andrea.condoluci@unibo.it>
Date: Fri, 14 Jul 2017 12:31:30 +0000 (+0200)
Subject: Code clean-up
X-Git-Tag: weak-reduction-separation~42
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a505b0100d9fa4016c2301c8127267bf4439243b;p=fireball-separation.git

Code clean-up

Less casts and casts in the right place

(cherry picked from commit 6bf723ba426a04a3ae5d36baf8a9fe4bffebc635)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index c376f01..97228ed 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -102,24 +102,24 @@ let make_fresh_vars p arities =
 
 let simple_expand_match ps =
  let rec aux 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)
  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 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 ->
-       `Match(cast_to_i_num_var u,v,bs_lift,bs,List.map (aux level) args))
-  | `I(v,args) -> `I(v,Listx.map (aux level) args)
+       cast_to_i_num_var (mk_appl (`Match(u,v,bs_lift,bs,[])) (List.map (aux level) args)))
+  | `I(v,args) -> cast_to_i_num_var (mk_appl (`Var v) (List.map (aux level) (Listx.to_list args)))
   | `N _ | `Var _ as t -> t
  in aux_i_num_var 0
 ;;
@@ -129,16 +129,20 @@ let fixpoint f =
 ;;
 
 let rec super_simplify_ps ps =
+ fixpoint (List.map (fun x -> cast_to_i_n_var (simple_expand_match ps (x :> i_num_var))))
+;;
+
+let rec super_simplify_ps_with_match ps =
  fixpoint (List.map (cast_to_i_num_var ++ (simple_expand_match ps)))
 ;;
 
 let super_simplify ({div; ps; conv} as p) =
-  let ps = super_simplify_ps p.ps (p.ps :> i_num_var list) in
-  let conv = super_simplify_ps ps (p.conv :> i_num_var list) in
+  let ps = super_simplify_ps p.ps p.ps in
+  let conv = super_simplify_ps ps p.conv in
   let div = option_map (fun div ->
-   let divs = super_simplify_ps p.ps ([div] :> i_num_var list) in
+   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}
 
 exception ExpandedToLambda;;
 
@@ -193,7 +197,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
          | `N i -> acc_new_ps,i
          | _ ->
             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
+            let super_simplified_ps = super_simplify_ps_with_match ps ps in
 (*prerr_endline ("CERCO u:" ^ print (fst u :> nf));
 List.iter (fun x -> prerr_endline ("IN: " ^ print (fst x :> nf))) ps;
 List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplified_ps;*)