From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 13 Jul 2017 16:52:32 +0000 (+0200)
Subject: return type of simplify_match improved (no `Match in output)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f635df1a27defb6e7c0aa290b4d040a16f748bf2;p=fireball-separation.git

return type of simplify_match improved (no `Match in output)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index ead0b54..9ed3394 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -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}
 
-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