From: acondolu <andrea.condoluci@unibo.it>
Date: Tue, 11 Jul 2017 11:22:41 +0000 (+0200)
Subject: Bug fix: x (y z) where y was conv_dangerous did not make x so
X-Git-Tag: weak-reduction-separation~63
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fb028533f111b1e218c4ccb4620c204f31a2b2ed;p=fireball-separation.git

Bug fix: x (y z) where y was conv_dangerous did not make x so

Additional fix to last commit: args' where no longer checked for dangerous
variables. Fixed by passing three arguments to dangerous_invert_conv in
place of two.
---

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 =