X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=ocaml%2Flambda4.ml;h=35f03ca8bf4af09dc6bde54560cc789edbff12e7;hb=fb028533f111b1e218c4ccb4620c204f31a2b2ed;hp=2400fb81b8c6874b297f0d663e26d18f51211a35;hpb=ba587b3b30282e7ec4638221b4fd9ed66be19a41;p=fireball-separation.git

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index 2400fb8..35f03ca 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -272,21 +272,24 @@ let rec dangerous_conv arities showstoppers =
       (match t with
           `N _ -> concat_map (dangerous_conv arities showstoppers) args
         | `Match _ as t -> dangerous_conv arities showstoppers t @ concat_map (dangerous_conv arities showstoppers) args
-        | `Var(x,_) -> dangerous_inert_conv arities showstoppers x args 2
-        | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args') (List.length args + 2)
+        | `Var(x,_) -> dangerous_inert_conv arities showstoppers x [] args 2
+        | `I((x,_),args') -> dangerous_inert_conv arities showstoppers x (Listx.to_list args') args 2
       )
-  | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) 0
+  | `I((k,_),args) -> dangerous_inert_conv arities showstoppers k (Listx.to_list args) [] 0
 
-and dangerous_inert_conv arities showstoppers k args more_args =
- concat_map (dangerous_conv arities showstoppers) args @
- if List.mem k showstoppers then k :: concat_map free_vars args else
+and dangerous_inert_conv arities showstoppers k args match_args more_args =
+ let all_args = args @ match_args in
+ let dangerous_args = concat_map (dangerous_conv arities showstoppers) all_args 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
 prerr_endline ("dangerous_inert_conv: ar=" ^ string_of_int arity ^ " k="^string_of_var 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 args + more_args > arity then k :: concat_map free_vars args else []
+  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
 
 (* inefficient algorithm *)
 let rec edible arities div ps conv showstoppers =