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