1 files changed, 83 insertions, 45 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 3fa674d3..73062328 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Term
 open Declarations
 open Names
@@ -40,21 +38,19 @@ let toplevel_env () =
 	in l,seb
     | _ -> failwith "caught"
   in
-  match current_toplevel () with
-    | _ -> SEBstruct (List.rev (map_succeed get_reference seg))
- 
+  SEBstruct (List.rev (map_succeed get_reference seg))
+
 
 let environment_until dir_opt =
   let rec parse = function
     | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
     | [] -> []
     | d :: l ->
-      let mb = Global.lookup_module (MPfile d) in
-      (* If -dont-load-proof has been used, mod_expr is None,
-         we try with mod_type *)
-      let meb = Option.default mb.mod_type mb.mod_expr in
-      if dir_opt = Some d then [MPfile d, meb]
-      else (MPfile d, meb) :: (parse l)
+	match (Global.lookup_module (MPfile d)).mod_expr with
+	  | Some meb ->
+	      if dir_opt = Some d then [MPfile d, meb]
+	      else (MPfile d, meb) :: (parse l)
+	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
 
@@ -68,6 +64,9 @@ module type VISIT = sig
   (* Add the module_path and all its prefixes to the mp visit list *)
   val add_mp : module_path -> unit
 
+  (* Same, but we'll keep all fields of these modules *)
+  val add_mp_all : module_path -> unit
+
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ind : mutual_inductive -> unit
@@ -81,6 +80,7 @@ module type VISIT = sig
   val needed_ind : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
+  val needed_mp_all : module_path -> bool
 end
 
 module Visit : VISIT = struct
@@ -88,16 +88,26 @@ module Visit : VISIT = struct
      (for inductives and modules names) and a Cset_env for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
+      { mutable ind : KNset.t; mutable con : KNset.t;
+	mutable mp : MPset.t; mutable mp_all : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
+  let v = { ind = KNset.empty ; con = KNset.empty ;
+	    mp = MPset.empty; mp_all = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+  let reset () =
+    v.ind <- KNset.empty;
+    v.con <- KNset.empty;
+    v.mp <- MPset.empty;
+    v.mp_all <- MPset.empty
   let needed_ind i = KNset.mem (user_mind i) v.ind
   let needed_con c = KNset.mem (user_con c) v.con
-  let needed_mp mp = MPset.mem mp v.mp
+  let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
+  let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_mp_all mp =
+    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp;
+    v.mp_all <- MPset.add mp v.mp_all
   let add_ind i =
     let kn = user_mind i in
     v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
@@ -120,12 +130,17 @@ let check_arity env cb =
 
 let check_fix env cb i =
   match cb.const_body with
-    | None -> raise Impossible
-    | Some lbody ->
-	match kind_of_term (Declarations.force lbody) with
+    | Def lbody ->
+	(match kind_of_term (Declarations.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible
+	  | _ -> raise Impossible)
+    | Undef _ | OpaqueDef _ -> raise Impossible
+
+let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
+  na1 = na2 &&
+  array_equal eq_constr ca1 ca2 &&
+  array_equal eq_constr ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
@@ -139,7 +154,8 @@ let factor_fix env l cb msb =
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
-	       if check <> check_fix env cb' (j+1) then raise Impossible;
+	       let check' = check_fix env cb' (j+1) in
+	       if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
     labels, recd, msb''
@@ -157,7 +173,8 @@ let rec seb2mse = function
 
 let expand_seb env mp seb =
   let seb,_,_,_ =
-    Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+    let inl = Some (Flags.get_inline_level()) in
+    Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb)
   in seb
 
 (** When possible, we use the nicer, shorter, algebraic type structures
@@ -200,9 +217,8 @@ let rec extract_sfb_spec env mp = function
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let kn = make_kn mp empty_dirpath l in
-      let mind = mind_of_kn kn in
-      let s = Sind (kn, extract_inductive env mind) in
+      let mind = make_mind mp empty_dirpath l in
+      let s = Sind (mind, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
@@ -223,7 +239,7 @@ let rec extract_sfb_spec env mp = function
 *)
 
 and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
-  | SEBident mp -> Visit.add_mp mp; MTident mp
+  | SEBident mp -> Visit.add_mp_all mp; MTident mp
   | SEBwith(seb',With_definition_body(idl,cb))->
       let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
       let mt = extract_seb_spec env mp1 (seb,seb') in
@@ -231,7 +247,7 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
 	 | None -> mt
 	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
   | SEBwith(seb',With_module_body(idl,mp))->
-      Visit.add_mp mp;
+      Visit.add_mp_all mp;
       MTwith(extract_seb_spec env mp1 (seb,seb'),
 	     ML_With_module(idl,mp))
   | SEBfunctor (mbid, mtb, seb_alg') ->
@@ -283,11 +299,10 @@ let rec extract_sfb env mp all = function
 	 else ms)
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
-      let kn = make_kn mp empty_dirpath l in
-      let mind = mind_of_kn kn in
+      let mind = make_mind mp empty_dirpath l in
       let b = Visit.needed_ind mind in
       if all || b then
-	let d = Dind (kn, extract_inductive env mind) in
+	let d = Dind (mind, extract_inductive env mind) in
 	if (not b) && (logical_decl d) then ms
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
@@ -312,7 +327,7 @@ and extract_seb env mp all = function
       extract_seb env mp all (expand_seb env mp seb)
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
-      Visit.add_mp mp; MEident mp
+      Visit.add_mp_all mp; MEident mp
   | SEBapply (meb, meb',_) ->
       MEapply (extract_seb env mp true meb,
 	       extract_seb env mp true meb')
@@ -346,11 +361,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 let mono_environment refs mpl =
   Visit.reset ();
   List.iter Visit.add_ref refs;
-  List.iter Visit.add_mp mpl;
+  List.iter Visit.add_mp_all mpl;
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
-    (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l
+    (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m))
+    l
 
 (**************************************)
 (*S Part II : Input/Output primitives *)
@@ -488,13 +504,18 @@ let print_structure_to_file (fn,si,mo) dry struc =
 let reset () =
   Visit.reset (); reset_tables (); reset_renaming_tables Everything
 
-let init modular =
+let init modular library =
   check_inside_section (); check_inside_module ();
   set_keywords (descr ()).keywords;
   set_modular modular;
+  set_library 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. *)
 
@@ -503,7 +524,8 @@ let rec locate_ref = function
   | r::l ->
       let q = snd (qualid_of_reference r) in
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Nametab.locate q) with Not_found -> None in
+      and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
+      in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
@@ -518,25 +540,41 @@ let rec locate_ref = function
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
 let full_extr f (refs,mps) =
-  init false;
+  init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
-  let struc = optimize_struct refs (mono_environment refs mps) in
-  warning_axioms ();
+  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warns ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
 let full_extraction f lr = full_extr f (locate_ref lr)
 
+(*s Separate extraction is similar to recursive extraction, with the output
+   decomposed in many files, one per Coq .v file *)
+
+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
+  warns ();
+  let print = function
+    | (MPfile dir as mp, sel) as e ->
+	print_structure_to_file (module_filename mp) false [e]
+    | _ -> assert false
+  in
+  List.iter print struc;
+  reset ()
+
 (*s Simple extraction in the Coq toplevel. The vernacular command
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r = match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
-      init false;
-      let struc = optimize_struct [r] (mono_environment [r] []) in
+      init false false;
+      let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
-      warning_axioms ();
+      warns ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
       print_one_decl struc (modpath_of_r r) d;
       reset ()
@@ -547,12 +585,12 @@ let simple_extraction r = match locate_ref [r] with
   \verb!(Recursive) Extraction Library! [M]. *)
 
 let extraction_library is_rec m =
-  init true;
+  init true true;
   let dir_m =
     let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
-  Visit.add_mp (MPfile dir_m);
+  Visit.add_mp_all (MPfile dir_m);
   let env = Global.env () in
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,meb) =
@@ -561,8 +599,8 @@ let extraction_library is_rec m =
     else l
   in
   let struc = List.fold_left select [] l in
-  let struc = optimize_struct [] struc in
-  warning_axioms ();
+  let struc = optimize_struct ([],[]) struc in
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in