From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 13 Jul 2017 09:00:36 +0000 (+0200)
Subject: Fixed try in aux_conv + Added test in pure for divergence of conv
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=941130623a83c8c3f7e4afcce4189f12c2bd18e0;p=fireball-separation.git

Fixed try in aux_conv + Added test in pure for divergence of conv
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 583d99e..1be77d1 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -10,6 +10,8 @@ open Num
 *)
 let num_more_args = 2;;
 
+let convergent_dummy = `N(-1);;
+
 type discriminating_set = (int * nf) list;;
 
 type problem =
@@ -35,9 +37,8 @@ let first bound p var f =
   if i > bound then
    raise (Backtrack ("no more alternatives for " ^ string_of_var var))
   else
-   try(try
+   try
     f p i
-   with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom"))
    with Backtrack s ->
 prerr_endline ("!!BACKTRACK!! " ^ s);
      List.iter (fun (r,l) -> r := l) (List.combine p.deltas (List.hd p.trail)) ;
@@ -79,7 +80,7 @@ let string_of_problem label ({freshno; div; conv; ps; deltas} as p) =
  ^"(* DIVERGENT  *)" ^ nl
  ^"     "^ (match div with None -> "None" | Some div -> "(Some\""^ print ~l (div :> nf) ^"\")") ^ nl
  ^"  (* CONVERGENT *) [" ^ nl ^ "  "
- ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = `N (-1) then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
+ ^ String.concat "\n  " (List.map (fun t -> "(* _ *) " ^ (if t = convergent_dummy then "" else "\""^ print ~l (t :> nf) ^"\";")) conv) ^
  (if conv = [] then "" else nl)
  ^ "] (* NUMERIC    *) [" ^ nl ^ " "
  ^ String.concat "\n " (List.mapi (fun i t -> " (* "^ string_of_int i ^" *) \"" ^ print ~l (t :> nf) ^ "\";") ps)
@@ -168,7 +169,9 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
      let t = subst false false x inst (t :> nf) in
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
      let freshno,new_t,acc_new_ps =
-      expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t
+      try
+       expand_match (freshno,acc_ps@`Var(max_int/3,-666)::todo_ps,acc_new_ps) t
+      with Pacman | Bottom -> raise (Backtrack "Pacman/Bottom in ps")
      in
       aux_ps (freshno,acc_ps@[new_t],acc_new_ps) todo_ps
 
@@ -178,11 +181,13 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
    | [] -> acc
    | t::todo_conv ->
    (*prerr_endline ("EXPAND t:" ^ print (t :> nf));*)
-      let t = try
-       subst false false x inst (t :> nf)
-      with Pacman -> `N(-1) in (* DUMMY CONVERGENT *)
+      let t = subst false false x inst (t :> nf) in
 (*prerr_endline ("SUBSTITUTED t:" ^ print (t :> nf));*)
-      let freshno,new_t,acc_new_ps = expand_match (freshno,ps,acc_new_ps) t in
+      let freshno,new_t,acc_new_ps =
+       try
+        expand_match (freshno,ps,acc_new_ps) t
+       with Pacman -> freshno,convergent_dummy,acc_new_ps
+          | Bottom -> raise (Backtrack "Bottom in conv") in
       aux_conv ps (freshno,acc_conv@[new_t],acc_new_ps) todo_conv
 
   (* cut&paste from aux' above *)
@@ -195,6 +200,7 @@ prerr_endline ("# INST0: " ^ string_of_var x ^ " := " ^ print ~l inst));*)
        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")
 
   and expand_match ((freshno,acc_ps,acc_new_ps) as acc) t =
    match t with
@@ -444,10 +450,10 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map string_of_var l))
      let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
       t)
     with Not_found -> match hd_of t with
-     | None -> assert (t = `N ~-1); t
+     | None -> assert (t = convergent_dummy); t
      | Some h ->
       prerr_endline ("FREEZING " ^ string_of_var h);
-      `N ~-1 (* convergent dummy*)
+      convergent_dummy
    ) (List.combine showstoppers_conv p.conv) in
  List.iter
   (fun bs ->
@@ -758,7 +764,8 @@ in
      List.iter (fun n ->
        prerr_endline ("_::: " ^ (Pure.print n));
        let t = Pure.mwhd (e',n,[]) in
-       prerr_endline ("_:: " ^ (Pure.print t))
+       prerr_endline ("_:: " ^ (Pure.print t));
+       assert (t <> Pure.B)
      ) conv ;
      List.iteri (fun i n ->
        prerr_endline ((string_of_int i) ^ "::: " ^ (Pure.print n));