From a4d48ce98d7ae0cf07c653ed75700ed6f182936a Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Mon, 30 Nov 2015 16:40:46 +0100 Subject: Extraction: check for remaining implicits after dead code removal (fix #4243) --- plugins/extraction/modutil.ml | 22 +++++++++++++--------- 1 file changed, 13 insertions(+), 9 deletions(-) (limited to 'plugins/extraction/modutil.ml') diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 8158ac647e..53c9f59878 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -404,12 +404,16 @@ let optimize_struct to_appear struc = List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse)) struc in - ignore (struct_ast_search check_implicits opt_struc); - if library () then - List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc - else begin - reset_needed (); - List.iter add_needed (fst to_appear); - List.iter add_needed_mp (snd to_appear); - depcheck_struct opt_struc - end + let mini_struc = + if library () then + List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc + else + begin + reset_needed (); + List.iter add_needed (fst to_appear); + List.iter add_needed_mp (snd to_appear); + depcheck_struct opt_struc + end + in + ignore (struct_ast_search check_implicits mini_struc); + mini_struc -- cgit v1.2.3 From ec5455d7351c05a58ae99d5a300dc8576f8c9360 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Fri, 4 Dec 2015 18:39:47 +0100 Subject: Extraction: nicer implementation of Implicits Instead of the original hacks (embedding implicits in string msg in MLexn !) we now use a proper construction MLdummy (Kimplicit (r,i)) to replace the use of the i-th argument of constant or constructor r when this argument has been declared as implicit. A new option Set/Unset Extraction SafeImplicits controls what happens when some implicits still occur after an extraction : fail in safe mode, or otherwise produce some code nonetheless. This code is probably buggish if the implicits are actually used to do anything relevant (match, function call, etc), but it might also be fine if the implicits are just passed along. And anyway, this unsafe mode could help figure what's going on. Note: the MLdummy now expected a kill_reason, just as Tdummy. These kill_reason are now Ktype, Kprop (formerly Kother) and Kimplicit. Some minor refactoring on the fly. --- plugins/extraction/modutil.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) (limited to 'plugins/extraction/modutil.ml') diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 53c9f59878..e8383bda59 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -387,16 +387,15 @@ let is_prefix pre s = in is_prefix_aux 0 -let check_implicits = function - | MLexn s -> - if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then - begin - if is_prefix "UNBOUND" s then assert false; - if is_prefix "IMPLICIT" s then - error_non_implicit (String.sub s 9 (String.length s - 9)); - end; - false - | _ -> false +exception RemainingImplicit of kill_reason + +let check_for_remaining_implicits struc = + let check = function + | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k) + | _ -> false + in + try ignore (struct_ast_search check struc) + with RemainingImplicit k -> err_or_warn_remaining_implicit k let optimize_struct to_appear struc = let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in @@ -415,5 +414,5 @@ let optimize_struct to_appear struc = depcheck_struct opt_struc end in - ignore (struct_ast_search check_implicits mini_struc); + let () = check_for_remaining_implicits mini_struc in mini_struc -- cgit v1.2.3 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 From 86f5c0cbfa64c5d0949365369529c5b607878ef8 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 20 Jan 2016 17:25:10 +0100 Subject: Update copyright headers. --- plugins/extraction/modutil.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/extraction/modutil.ml') diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index c3dc286cd1..b5e8b48044 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*