Fixing the bug when eating triggers the reduction of a match

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 456dd5b9ec96ae9b62ee68c185067f97cfaa3d5d..c28f723ee57880f87c9554219224586124a80025 100644 (file)
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -287,7 +287,8 @@ List.iter (fun x -> prerr_endline ("IN2: " ^ print (fst x :> nf))) super_simplif
  p
 ;;
 
-exception Dangerous
+exception TriggerMatchReduction of int;;
+exception Dangerous;;
 
 let arity_of arities hd =
  let pos,_,nargs = List.find (fun (_,hd',_) -> hd=hd') arities in
@@ -322,68 +323,73 @@ and dangerous_inert arities showstoppers k args more_args =
 (* cut & paste from above *)
 let rec dangerous_conv p arities showstoppers =
  function
-    `N _
+  | `N _
   | `Var _
   | `Lam _
-  | `Pacman -> []
-  | `Match(t,_,liftno,bs,args) ->
+  | `Pacman -> ()
+  | `Match(t,_,liftno,bs,args) -> (
       (* CSC: XXX partial dependency on the encoding *)
-      (match t with
-          `N _ -> concat_map (dangerous_conv p arities showstoppers) args
-        | `Match _ as t -> dangerous_conv p arities showstoppers t @ concat_map (dangerous_conv p arities showstoppers) args
+       try (match t with
+        | `N _ -> List.iter (dangerous_conv p arities showstoppers) args
+        | `Match _ as t -> dangerous_conv p arities showstoppers t; List.iter (dangerous_conv p arities showstoppers) args
         | `Var(x,_) -> dangerous_inert_conv p arities showstoppers x [] args 2
         | `I((x,_),args') -> dangerous_inert_conv p arities showstoppers x (Listx.to_list args') args 2
-      )
+        ) with TriggerMatchReduction x -> (
+           match Util.find_opt (fun (n, t) -> if hd_of (List.nth p.ps n) = Some x then Some t else None) !bs with
+            | None -> ()
+            | Some t -> (
+               match t with
+                | `Bottom -> raise Dangerous
+                | #nf_nob as t -> dangerous_conv p arities showstoppers t
+               )
+           )
+       )
   | `I((k,_),args) -> dangerous_inert_conv p arities showstoppers k (Listx.to_list args) [] 0
 
 and dangerous_inert_conv p arities showstoppers k args match_args more_args =
  let all_args = args @ match_args in
- let dangerous_args = concat_map (dangerous_conv p arities showstoppers) all_args in
+ List.iter (dangerous_conv p arities showstoppers) all_args;
  let all_args = (all_args :> nf list) in
- if dangerous_args = [] then (
- if List.mem k showstoppers then k :: concat_map free_vars all_args else
- try
-  let arity = arity_of arities k in
+ if List.mem k showstoppers then raise Dangerous else
+  try
+   let arity = arity_of arities k in
 prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var p.var_names k ^ " listlenargs=" ^ (string_of_int (List.length args)) ^ " more_args=" ^ string_of_int more_args);
-  if more_args > 0 (* match argument*) && List.length args = arity then []
-  else if List.length all_args + more_args > arity then k :: concat_map free_vars all_args else []
- with
-  Not_found -> []
- ) else k :: concat_map free_vars all_args
+   if more_args > 0 (* match argument*) && List.length args = arity then raise (TriggerMatchReduction k)
+    else if List.length all_args + more_args > arity then raise Dangerous else ()
+  with
+   Not_found -> ()
 
 (* inefficient algorithm *)
-let rec edible ({div; conv; ps} as p) arities showstoppers =
- let rec aux showstoppers =
-  function
-     [] -> showstoppers
+let rec edible p arities showstoppers =
+ let rec aux f showstoppers tms = function
+   | [] -> showstoppers
    | x::xs when List.exists (fun y -> hd_of x = Some y) showstoppers ->
       (* se la testa di x e' uno show-stopper *)
       let new_showstoppers = sort_uniq (showstoppers @ free_vars (x :> nf)) in
       (* aggiungi tutte le variabili libere di x *)
       if List.length showstoppers <> List.length new_showstoppers then
-       aux new_showstoppers ps
+       aux f new_showstoppers tms tms
       else
-       aux showstoppers xs
+       aux f showstoppers tms xs
    | x::xs ->
       match hd_of x with
-         None -> aux showstoppers xs
+         None -> aux f showstoppers tms xs
        | Some h ->
           try
-           dangerous arities showstoppers (x : i_n_var :> nf_nob) ;
-           aux showstoppers xs
+           f showstoppers (x :> nf_nob) ;
+           aux f showstoppers tms xs
           with
            Dangerous ->
-            aux (sort_uniq (h::showstoppers)) ps
+            aux f (sort_uniq (h::showstoppers)) tms tms
   in
-    let showstoppers = sort_uniq (aux showstoppers ps) in
-    let dangerous_conv =
-     List.map (dangerous_conv p arities showstoppers) (conv :> nf_nob list) in
+   let showstoppers = sort_uniq (aux (dangerous arities) showstoppers p.ps p.ps) in
+   let dangerous_conv = sort_uniq (aux (dangerous_conv p arities) showstoppers p.conv p.conv) in
 
-prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
+(* prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
+List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *)
 
-    let showstoppers' = showstoppers @ List.concat dangerous_conv in
-    let showstoppers' = sort_uniq (match div with
+    let showstoppers' = showstoppers @ dangerous_conv in
+    let showstoppers' = sort_uniq (match p.div with
      | None -> showstoppers'
      | Some div ->
        if List.exists ((=) (hd_of_i_var div)) showstoppers'
@@ -474,13 +480,13 @@ prerr_endline ("# [INST_IN_EAT] eating: " ^ string_of_var p.var_names hd ^ " :=
     let x = hd_of_i_var div in
     let inst = make_lams `Bottom n in
     subst_in_problem x inst p in
- let dangerous_conv = showstoppers_conv in
+(*let dangerous_conv = showstoppers_conv in
 prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
+List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; *)
  let conv =
-   List.map (function s,t ->
+   List.map (function t ->
     try
-     if s <> [] then t else (
+     if let hd = hd_of t in hd <> None && not (List.mem (Util.option_get hd) showstoppers_conv) then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
      let _ = List.find (fun h -> hd_of t = Some h) inedible in
       t)
@@ -489,7 +495,7 @@ List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.
      | Some h ->
       prerr_endline ("FREEZING " ^ string_of_var p.var_names h);
       convergent_dummy
-   ) (List.combine showstoppers_conv p.conv) in
+   ) p.conv in
  List.iter
   (fun bs ->
     bs :=