From 4b197ed247d1f30ff40fa59f85b070766f305bea Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 15 Dec 2015 11:15:00 +0100 Subject: Extraction: replace unused variable names by _ in funs and matchs (fix #2842) This is done via a unique pass which seems roughly linear in practice, even on big developments like CompCert. There's a List.nth in an env at each MLrel, that could be made logarithmic if necessary via Okasaki's skew list for instance. Another approach would be to keep names (as a form of documentation), but prefix them by _ to please OCaml's warnings. For now, let's be radical and use the _ pattern. --- plugins/extraction/modutil.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'plugins/extraction/modutil.ml') diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index e8383bda59..6f354b1ce5 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -263,10 +263,12 @@ let dfix_to_mlfix rv av i = order to preserve the global interface, later [depcheck_se] will get rid of them if possible *) +let optim_ast t = dump_unused_vars (normalize t) + let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> - let a = normalize (ast_glob_subst !s a) in + let a = optim_ast (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; let d = match optimize_fix a with @@ -276,7 +278,7 @@ let rec optim_se top to_appear s = function in (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> - let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in + let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in (* This fake body ensures that no fixpoint will be auto-inlined. *) let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do -- cgit v1.2.3 From 3c535011374382bc205a68b1cb59cfa7247d544a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 15 Dec 2015 17:46:25 +0100 Subject: Extraction: fix a few little glitches with my last commit (replacing unused vars by _) --- plugins/extraction/modutil.ml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'plugins/extraction/modutil.ml') diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 6f354b1ce5..c3dc286cd1 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -263,29 +263,28 @@ let dfix_to_mlfix rv av i = order to preserve the global interface, later [depcheck_se] will get rid of them if possible *) -let optim_ast t = dump_unused_vars (normalize t) - let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> - let a = optim_ast (ast_glob_subst !s a) in + let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap'.add r a !s; - let d = match optimize_fix a with + let d = match dump_unused_vars (optimize_fix a) with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) | a -> Dterm (r, a, t) in (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> - let av = Array.map (fun a -> optim_ast (ast_glob_subst !s a)) av in + let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in (* This fake body ensures that no fixpoint will be auto-inlined. *) let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s done; - (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) + let av' = Array.map dump_unused_vars av in + (l,SEdecl (Dfix (rv, av', tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} in (l,SEmodule m) :: (optim_se top to_appear s lse) -- cgit v1.2.3