Extraction: opaque terms are not traversed anymore by default

 In signatures, opaque terms are always seen as parameters.
 In implementations, a flag Set/Unset Extraction AccessOpaque
 allows to customize things:
  - Set : opacity is ignored (this is the old behavior)
  - Unset : opaque terms are extracted as axioms (default now)

 Some warnings are anyway emitted when extraction encounters
 informative opaque terms.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13999 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 108 insertions, 84 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index c4dce1c7b..126305566 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -487,6 +487,10 @@ let init modular library =
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
+let warns () =
+  warning_opaques (access_opaque ());
+  warning_axioms ()
+
 (* From a list of [reference], let's retrieve whether they correspond
    to modules or [global_reference]. Warn the user if both is possible. *)
 
@@ -513,8 +517,7 @@ let full_extr f (refs,mps) =
   init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
@@ -527,8 +530,7 @@ let separate_extraction lr =
   init true false;
   let refs,mps = locate_ref lr in
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	print_structure_to_file (module_filename mp) false [e]
@@ -546,8 +548,7 @@ let simple_extraction r = match locate_ref [r] with
       init false false;
       let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
-      warning_opaques ();
-      warning_axioms ();
+      warns ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
       print_one_decl struc (modpath_of_r r) d;
       reset ()
@@ -573,8 +574,7 @@ let extraction_library is_rec m =
   in
   let struc = List.fold_left select [] l in
   let struc = optimize_struct ([],[]) struc in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 992f8fca6..979240663 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -203,7 +203,7 @@ let rec extract_type env db j c args =
 	extract_type env db j d (Array.to_list args' @ args)
     | Lambda (_,_,d) ->
 	(match args with
-	   | [] -> assert false (* otherwise the lambda would be reductible. *)
+	   | [] -> assert false (* A lambda cannot be a type. *)
 	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
 	assert (args = []);
@@ -243,12 +243,13 @@ let rec extract_type env db j c args =
 	let cb = lookup_constant kn env in
 	let typ = Typeops.type_of_constant_type env cb.const_type in
 	(match flag_of_type env typ with
+	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in
-	       (match body_of_constant cb with
-		  | None -> mlt
-		  | Some _ when is_custom r -> mlt
-		  | Some lbody ->
+	       (match cb.const_body with
+		  | Undef _ | OpaqueDef _ -> mlt
+		  | Def _ when is_custom r -> mlt
+		  | Def lbody ->
 		      let newc = applist (Declarations.force lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
@@ -257,10 +258,11 @@ let rec extract_type env db j c args =
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
 		      if expand env mlt = expand env mlt' then mlt else mlt')
-	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
-	       (match body_of_constant cb with
-		  | None -> Tunknown (* Brutal approximation ... *)
-		  | Some lbody ->
+	   | (Info, Default) ->
+               (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
+	       (match cb.const_body with
+		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
+		  | Def lbody ->
 		      (* We try to reduce. *)
 		      let newc = applist (Declarations.force lbody, args) in
 		      extract_type env db j newc []))
@@ -478,9 +480,9 @@ and mlt_env env r = match r with
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = Typeops.type_of_constant_type env cb.const_type in
-	 match body_of_constant cb with
-	   | None -> None
-	   | Some l_body ->
+	 match cb.const_body with
+	   | Undef _ | OpaqueDef _ -> None
+	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
 		      let body = Declarations.force l_body in
@@ -904,38 +906,45 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 let extract_constant env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  let warn_info_none () = if not (is_custom r) then add_info_axiom r in
-  let warn_info_some () = if is_opaque cb then add_opaque r in
-  match body_of_constant cb with
-    | None ->
-        (match flag_of_type env typ with
-	   | (Info,TypeScheme) ->
-	       warn_info_none ();
-	       let n = type_scheme_nb_args env typ in
-	       let ids = iterate (fun l -> anonymous_name::l) n [] in
-	       Dtype (r, ids, Taxiom)
-           | (Info,Default) ->
-	       warn_info_none ();
-	       let t = snd (record_constant_type env kn (Some typ)) in
-	       Dterm (r, MLaxiom, type_expunge env t)
-           | (Logic,TypeScheme) ->
-	       add_log_axiom r; Dtype (r, [], Tdummy Ktype)
-	   | (Logic,Default) ->
-	       add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
-    | Some body ->
-	(match flag_of_type env typ with
-	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
-	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
-	   | (Info, Default) ->
-	       warn_info_some ();
-	       let e,t = extract_std_constant env kn (force body) typ in
-	       Dterm (r,e,t)
-	   | (Info, TypeScheme) ->
-	       warn_info_some ();
-	       let s,vl = type_sign_vl env typ in
-               let db = db_from_sign s in
-               let t = extract_type_scheme env db (force body) (List.length s)
-	       in Dtype (r, vl, t))
+  let warn_info () = if not (is_custom r) then add_info_axiom r in
+  let warn_log () = if not (constant_has_body cb) then add_log_axiom r
+  in
+  let mk_typ_ax () =
+    let n = type_scheme_nb_args env typ in
+    let ids = iterate (fun l -> anonymous_name::l) n [] in
+    Dtype (r, ids, Taxiom)
+  in
+  let mk_typ c =
+    let s,vl = type_sign_vl env typ in
+    let db = db_from_sign s in
+    let t = extract_type_scheme env db c (List.length s)
+    in Dtype (r, vl, t)
+  in
+  let mk_ax () =
+    let t = snd (record_constant_type env kn (Some typ)) in
+    Dterm (r, MLaxiom, type_expunge env t)
+  in
+  let mk_def c =
+    let e,t = extract_std_constant env kn c typ in
+    Dterm (r,e,t)
+  in
+  match flag_of_type env typ with
+    | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
+    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother)
+    | (Info,TypeScheme) ->
+        (match cb.const_body with
+	  | Undef _ -> warn_info (); mk_typ_ax ()
+	  | Def c -> mk_typ (force c)
+	  | OpaqueDef c ->
+	    add_opaque r;
+	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+    | (Info,Default) ->
+        (match cb.const_body with
+	  | Undef _ -> warn_info (); mk_ax ()
+	  | Def c -> mk_def (force c)
+	  | OpaqueDef c ->
+	    add_opaque r;
+	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -945,9 +954,9 @@ let extract_constant_spec env kn cb =
     | (Logic, Default) -> Sval (r, Tdummy Kother)
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	(match body_of_constant cb with
-	  | None -> Stype (r, vl, None)
-	  | Some body ->
+	(match cb.const_body with
+	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
+	  | Def body ->
 	      let db = db_from_sign s in
 	      let t = extract_type_scheme env db (force body) (List.length s)
 	      in Stype (r, vl, Some t))
@@ -960,9 +969,13 @@ let extract_with_type env cb =
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	let body = Option.get (body_of_constant cb) in
 	let db = db_from_sign s in
-	let t = extract_type_scheme env db (force body) (List.length s) in
+	let c = match cb.const_body with
+	  | Def body -> force body
+	  (* A "with Definition ..." is necessarily transparent *)
+	  | Undef _ | OpaqueDef _ -> assert false
+	in
+	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 35494d3d2..4e08079a3 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -262,16 +262,25 @@ let warning_axioms () =
   end;
   if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
     msg_warning
-      (str "Some of these axioms might by due to option -dont-load-proofs.")
+      (str "Some of these axioms might be due to option -dont-load-proofs.")
 
-let warning_opaques () =
+let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
   if opaques = [] then ()
-  else msg_warning
-    (str "Extraction is accessing the body of the following opaque constants:"
-     ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques)
-     ++ str "." ++ fnl ()
-     ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ())
+  else
+    let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
+    if accessed then
+      msg_warning
+	(str "The extraction is currently set to bypass opacity,\n" ++
+	 str "the following opaque constant bodies have been accessed :" ++
+	 lst ++ str "." ++ fnl ())
+    else
+      msg_warning
+	(str "The extraction now honors the opacity constraints by default,\n" ++
+	 str "the following opaque constants have been extracted as axioms :" ++
+	 lst ++ str "." ++ fnl () ++
+	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+	 ++ fnl ())
 
 let warning_both_mod_and_cst q mp r =
  msg_warning
@@ -374,31 +383,29 @@ let info_file f =
 (* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
-(*s Extraction AutoInline *)
-
-let auto_inline_ref = ref false
+let my_bool_option name initval =
+  let flag = ref initval in
+  let access = fun () -> !flag in
+  let _ = declare_bool_option
+    {optsync = true;
+     optname = "Extraction "^name;
+     optkey = ["Extraction"; name];
+     optread = access;
+     optwrite = (:=) flag }
+  in
+  access
 
-let auto_inline () = !auto_inline_ref
+(*s Extraction AccessOpaque *)
 
-let _ = declare_bool_option
-	  {optsync = true;
-	   optname = "Extraction AutoInline";
-	   optkey = ["Extraction"; "AutoInline"];
-	   optread = auto_inline;
-	   optwrite = (:=) auto_inline_ref}
+let access_opaque = my_bool_option "AccessOpaque" false
 
-(*s Extraction TypeExpand *)
+(*s Extraction AutoInline *)
 
-let type_expand_ref = ref true
+let auto_inline = my_bool_option "AutoInline" false
 
-let type_expand () = !type_expand_ref
+(*s Extraction TypeExpand *)
 
-let _ = declare_bool_option
-	  {optsync = true;
-	   optname = "Extraction TypeExpand";
-	   optkey = ["Extraction"; "TypeExpand"];
-	   optread = type_expand;
-	   optwrite = (:=) type_expand_ref}
+let type_expand = my_bool_option "TypeExpand" true
 
 (*s Extraction Optimize *)
 
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 97c28b154..dc07349ca 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -19,7 +19,7 @@ val safe_basename_of_global : global_reference -> identifier
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
-val warning_opaques : unit -> unit
+val warning_opaques : bool -> unit
 val warning_both_mod_and_cst :
  qualid -> module_path -> global_reference -> unit
 val warning_id : string -> unit
@@ -89,6 +89,10 @@ val remove_opaque : global_reference -> unit
 
 val reset_tables : unit -> unit
 
+(*s AccessOpaque parameter *)
+
+val access_opaque : unit -> bool
+
 (*s AutoInline parameter *)
 
 val auto_inline : unit -> bool