From: acondolu 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 =