X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Flambda4.ml;h=788fe5983357dddd15e531364f8203664570ed86;hb=52947a60467ebb10cec57ffc1725644ad605c671;hp=ead0b5466856989e31d914ae1598e64e646244eb;hpb=a5d76aabf64c2226b8bd8084be02f140f48c767b;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index ead0b54..788fe59 100644
--- 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
 ;;
@@ -144,18 +144,22 @@ 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}
 
-let cast_to_ps =
+let cast_to_ps_with_match =
  function
     #i_num_var as y -> (y : i_num_var)
   | `Bottom | `Pacman -> raise (Backtrack "BOT/PAC in ps")
@@ -201,12 +205,17 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
    function
    | None -> freshno, None, acc_new_ps
    | Some t ->
+      let t = subst false false x inst (t :> nf) in
       try
-       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
-        freshno,Some(cast_to_i_var new_t),acc_new_ps
-      with Bottom -> freshno, None, acc_new_ps
-         | Pacman -> raise (Backtrack "Pacman in div")
+        (* backtrack if it is a number or a variable *)
+        match new_t with
+         | `N _   -> raise (Backtrack "div=`N")
+         | `Var _
+         | `I _ as new_t -> freshno, Some(new_t), acc_new_ps
+      with
+       | Bottom -> freshno, None, acc_new_ps
+       | Pacman -> raise (Backtrack "div=PAC")
 
   and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t =
    match t with
@@ -216,12 +225,12 @@ 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_ps (subst false false x inst (t:> nf))) (acc_ps@acc_new_ps) in
-            let super_simplified_ps = super_simplify_ps ps ps in
+            let ps = List.map (fun t -> cast_to_ps_with_match (subst false false x inst (t:> nf))) (acc_ps@acc_new_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;*)
-            match index_of_opt ~eq:eta_eq super_simplified_ps u with
+            match index_of_opt ~eq:eta_eq super_simplified_ps (u :> i_num_var) with
                Some i -> acc_new_ps, i
              | None -> acc_new_ps@[u], len_ps + List.length acc_new_ps
         in
@@ -241,10 +250,10 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
    | `Pacman -> raise Pacman
    | #i_n_var as x ->
       let x = simple_expand_match (acc_ps@acc_new_ps) x in
-      freshno,cast_to_i_num_var x,acc_new_ps in
+      freshno,cast_to_i_n_var x,acc_new_ps in
 
- let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) (ps :> i_num_var list) in
- let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) (conv :> i_num_var list) in
+ let freshno,old_ps,new_ps = aux_ps (freshno,[],[]) ps in
+ let freshno,conv,new_ps = aux_conv old_ps (freshno,[],new_ps) conv in
  let freshno,div,new_ps = aux_div old_ps (freshno,new_ps) (div :> i_num_var option) in
 
  let ps = List.map cast_to_i_n_var (old_ps @ new_ps) in
@@ -562,7 +571,10 @@ let choose_step (n,p) =
        prerr_endline ("INSTANTIATING AND HOPING " ^ string_of_var x);
        x
   with
-   Not_found -> x in
+   Not_found ->
+    let arity_of_x = max_arity_tms x (all_terms p) in
+    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
 let x =