]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Bug fix: x (y z) where y was conv_dangerous did not make x so
authoracondolu <andrea.condoluci@unibo.it>
Tue, 11 Jul 2017 11:22:41 +0000 (13:22 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Tue, 11 Jul 2017 11:22:41 +0000 (13:22 +0200)
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.

ocaml/lambda4.ml

index 2400fb81b8c6874b297f0d663e26d18f51211a35..35f03ca8bf4af09dc6bde54560cc789edbff12e7 100644 (file)
@@ -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 =