1 files changed, 540 insertions, 0 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
new file mode 100644
index 00000000..ab9c242a
--- /dev/null
+++ b/plugins/extraction/extract_env.ml
@@ -0,0 +1,540 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i $Id$ i*)
+
+open Term
+open Declarations
+open Names
+open Libnames
+open Pp
+open Util
+open Miniml
+open Table
+open Extraction
+open Modutil
+open Common
+open Mod_subst
+
+(***************************************)
+(*S Part I: computing Coq environment. *)
+(***************************************)
+
+let toplevel_env () =
+  let seg = Lib.contents_after None in
+  let get_reference = function
+    | (_,kn), Lib.Leaf o ->
+	let mp,_,l = repr_kn kn in
+	let seb = match Libobject.object_tag o with
+	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
+	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
+	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+	  | "MODULE TYPE" ->
+	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
+	  | _ -> failwith "caught"
+	in l,seb
+    | _ -> failwith "caught"
+  in
+  match current_toplevel () with
+    | _ -> 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 ->
+	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 ())
+
+
+(*s Visit:
+  a structure recording the needed dependencies for the current extraction *)
+
+module type VISIT = sig
+  (* Reset the dependencies by emptying the visit lists *)
+  val reset : unit -> unit
+
+  (* Add the module_path and all its prefixes to the mp visit list *)
+  val add_mp : 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_kn : mutual_inductive -> unit
+  val add_con : constant -> unit
+  val add_ref : global_reference -> unit
+  val add_decl_deps : ml_decl -> unit
+  val add_spec_deps : ml_spec -> unit
+
+  (* Test functions:
+     is a particular object a needed dependency for the current extraction ? *)
+  val needed_kn : mutual_inductive -> bool
+  val needed_con : constant -> bool
+  val needed_mp : module_path -> bool
+end
+
+module Visit : VISIT = struct
+  (* What used to be in a single KNset should now be split into a KNset
+     (for inductives and modules names) and a Cset for constants
+     (and still the remaining MPset) *)
+  type must_visit =
+      { mutable kn : Mindset.t; mutable con : Cset.t; mutable mp : MPset.t }
+  (* the imperative internal visit lists *)
+  let v = { kn = Mindset.empty ; con = Cset.empty ; mp = MPset.empty }
+  (* the accessor functions *)
+  let reset () = v.kn <- Mindset.empty; v.con <- Cset.empty; v.mp <- MPset.empty
+  let needed_kn kn = Mindset.mem kn v.kn
+  let needed_con c = Cset.mem c v.con
+  let needed_mp mp = MPset.mem mp v.mp
+  let add_mp mp =
+    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_kn kn = v.kn <- Mindset.add kn v.kn; add_mp (mind_modpath kn)
+  let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c)
+  let add_ref = function
+    | ConstRef c -> add_con c
+    | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn
+    | VarRef _ -> assert false
+  let add_decl_deps = decl_iter_references add_ref add_ref add_ref
+  let add_spec_deps = spec_iter_references add_ref add_ref add_ref
+end
+
+exception Impossible
+
+let check_arity env cb =
+  let t = Typeops.type_of_constant_type env cb.const_type in
+  if Reduction.is_arity env t then raise Impossible
+
+let check_fix env cb i =
+  match cb.const_body with
+    | None -> raise Impossible
+    | Some 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
+
+let factor_fix env l cb msb =
+  let _,recd as check = check_fix env cb 0 in
+  let n = Array.length (let fi,_,_ = recd in fi) in
+  if n = 1 then [|l|], recd, msb
+  else begin
+    if List.length msb < n-1 then raise Impossible;
+    let msb', msb'' = list_chop (n-1) msb in
+    let labels = Array.make n l in
+    list_iter_i
+      (fun j ->
+	 function
+	   | (l,SFBconst cb') ->
+	       if check <> check_fix env cb' (j+1) then raise Impossible;
+	       labels.(j+1) <- l;
+	   | _ -> raise Impossible) msb';
+    labels, recd, msb''
+  end
+
+(** Expanding a [struct_expr_body] into a version without abbreviations
+    or functor applications. This is done via a detour to entries
+    (hack proposed by Elie)
+*)
+
+let rec seb2mse = function
+  | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
+  | SEBident mp -> Entries.MSEident mp
+  | _ -> failwith "seb2mse: received a non-atomic seb"
+
+let expand_seb env mp seb =
+  let seb,_,_,_ =
+    Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+  in seb
+
+(** When possible, we use the nicer, shorter, algebraic type structures
+    instead of the expanded ones. *)
+
+let my_type_of_mb mb =
+  let m0 = mb.mod_type in
+  match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0
+
+let my_type_of_mtb mtb =
+  let m0 = mtb.typ_expr in
+  match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0
+
+(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
+    To check with Elie. *)
+
+let rec msid_of_seb = function
+  | SEBident mp -> mp
+  | SEBwith (seb,_) -> msid_of_seb seb
+  | _ -> assert false
+
+let env_for_mtb_with env mp seb idl =
+  let sig_b = match seb with
+    | SEBstruct(sig_b) -> sig_b
+    | _ -> assert false
+  in
+  let l = label_of_id (List.hd idl) in
+  let before = fst (list_split_when (fun (l',_) -> l=l') sig_b) in
+  Modops.add_signature mp before empty_delta_resolver env
+
+(* From a [structure_body] (i.e. a list of [structure_field_body])
+   to specifications. *)
+
+let rec extract_sfb_spec env mp = function
+  | [] -> []
+  | (l,SFBconst cb) :: msig ->
+      let kn = make_con mp empty_dirpath l in
+      let s = extract_constant_spec env kn cb 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
+  | (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 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
+  | (l,SFBmodule mb) :: msig ->
+      let specs = extract_sfb_spec env mp msig in
+      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in
+      (l,Smodule spec) :: specs
+  | (l,SFBmodtype mtb) :: msig ->
+      let specs = extract_sfb_spec env mp msig in
+      let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in
+      (l,Smodtype spec) :: specs
+
+(* From [struct_expr_body] to specifications *)
+
+(* Invariant: the [seb] given to [extract_seb_spec] should either come
+   from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
+   This way, any encountered [SEBident] should be a true module type.
+*)
+
+and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
+  | SEBident mp -> Visit.add_mp 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
+      (match extract_with_type env' cb with (* cb peut contenir des kn  *)
+	 | None -> mt
+	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+  | SEBwith(seb',With_module_body(idl,mp))->
+      Visit.add_mp mp;
+      MTwith(extract_seb_spec env mp1 (seb,seb'),
+	     ML_With_module(idl,mp))
+  | SEBfunctor (mbid, mtb, seb_alg') ->
+      let seb' = match seb with
+	| SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb'
+	| _ -> assert false
+      in
+      let mp = MPbound mbid in
+      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in
+      MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb),
+		extract_seb_spec env' mp1 (seb',seb_alg'))
+  | SEBstruct (msig) ->
+      let env' = Modops.add_signature mp1 msig empty_delta_resolver env in
+      MTsig (mp1, extract_sfb_spec env' mp1 msig)
+  | SEBapply _ ->
+      if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb)
+      else assert false
+
+
+
+(* From a [structure_body] (i.e. a list of [structure_field_body])
+   to implementations.
+
+   NB: when [all=false], the evaluation order of the list is
+   important: last to first ensures correct dependencies.
+*)
+
+let rec extract_sfb env mp all = function
+  | [] -> []
+  | (l,SFBconst cb) :: msb ->
+      (try
+	 let vl,recd,msb = factor_fix env l cb msb in
+	 let vc = Array.map (make_con mp empty_dirpath) vl in
+	 let ms = extract_sfb env mp all msb in
+	 let b = array_exists Visit.needed_con vc in
+	 if all || b then
+	   let d = extract_fixpoint env vc recd in
+	   if (not b) && (logical_decl d) then ms
+	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
+	 else ms
+       with Impossible ->
+	 let ms = extract_sfb env mp all msb in
+	 let c = make_con mp empty_dirpath l in
+	 let b = Visit.needed_con c in
+	 if all || b then
+	   let d = extract_constant env c cb in
+	   if (not b) && (logical_decl d) then ms
+	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
+	 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 b = Visit.needed_kn mind in
+      if all || b then
+	let d = Dind (kn, 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
+  | (l,SFBmodule mb) :: msb ->
+      let ms = extract_sfb env mp all msb in
+      let mp = MPdot (mp,l) in
+      if all || Visit.needed_mp mp then
+	(l,SEmodule (extract_module env mp true mb)) :: ms
+      else ms
+  | (l,SFBmodtype mtb) :: msb ->
+      let ms = extract_sfb env mp all msb in
+      let mp = MPdot (mp,l) in
+       if all || Visit.needed_mp mp then
+	(l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms
+      else ms
+
+(* From [struct_expr_body] to implementations *)
+
+and extract_seb env mp all = function
+  | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml ->
+      (* in Haskell/Scheme, we expand everything *)
+      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
+  | SEBapply (meb, meb',_) ->
+      MEapply (extract_seb env mp true meb,
+	       extract_seb env mp true meb')
+  | SEBfunctor (mbid, mtb, meb) ->
+      let mp1 = MPbound mbid in
+      let env' = Modops.add_module (Modops.module_body_of_type  mp1 mtb)
+	env  in
+      MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb),
+		 extract_seb env' mp true meb)
+  | SEBstruct (msb) ->
+      let env' = Modops.add_signature mp msb empty_delta_resolver env in
+      MEstruct (mp,extract_sfb env' mp all msb)
+  | SEBwith (_,_) -> anomaly "Not available yet"
+
+and extract_module env mp all mb =
+  (* [mb.mod_expr <> None ], since we look at modules from outside. *)
+  (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
+  { ml_mod_expr = extract_seb env mp all (Option.get mb.mod_expr);
+    ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
+
+
+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;
+  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
+
+(**************************************)
+(*S Part II : Input/Output primitives *)
+(**************************************)
+
+let descr () = match lang () with
+  | Ocaml -> Ocaml.ocaml_descr
+  | Haskell -> Haskell.haskell_descr
+  | Scheme -> Scheme.scheme_descr
+
+(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
+   Works similarly for the other languages. *)
+
+let default_id = id_of_string "Main"
+
+let mono_filename f =
+  let d = descr () in
+  match f with
+    | None -> None, None, default_id
+    | Some f ->
+	let f =
+	  if Filename.check_suffix f d.file_suffix then
+	    Filename.chop_suffix f d.file_suffix
+	  else f
+	in
+	let id =
+	  if lang () <> Haskell then default_id
+	  else try id_of_string (Filename.basename f)
+	  with _ -> error "Extraction: provided filename is not a valid identifier"
+	in
+	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
+
+(* Builds a suitable filename from a module id *)
+
+let module_filename mp =
+  let f = file_of_modfile mp in
+  let d = descr () in
+  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
+
+(*s Extraction of one decl to stdout. *)
+
+let print_one_decl struc mp decl =
+  let d = descr () in
+  reset_renaming_tables AllButExternal;
+  set_phase Pre;
+  ignore (d.pp_struct struc);
+  set_phase Impl;
+  push_visible mp [];
+  msgnl (d.pp_decl decl);
+  pop_visible ()
+
+(*s Extraction of a ml struct to a file. *)
+
+let formatter dry file =
+  if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
+  else match file with
+    | None -> !Pp_control.std_ft
+    | Some cout ->
+	let ft = Pp_control.with_output_to cout in
+	Option.iter (Format.pp_set_margin ft) (Pp_control.get_margin ());
+	ft
+
+let print_structure_to_file (fn,si,mo) dry struc =
+  let d = descr () in
+  reset_renaming_tables AllButExternal;
+  let unsafe_needs = {
+    mldummy = struct_ast_search ((=) MLdummy) struc;
+    tdummy = struct_type_search Mlutil.isDummy struc;
+    tunknown = struct_type_search ((=) Tunknown) struc;
+    magic =
+      if lang () <> Haskell then false
+      else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
+  in
+  (* First, a dry run, for computing objects to rename or duplicate *)
+  set_phase Pre;
+  let devnull = formatter true None in
+  msg_with devnull (d.pp_struct struc);
+  let opened = opened_libraries () in
+  (* Print the implementation *)
+  let cout = if dry then None else Option.map open_out fn in
+  let ft = formatter dry cout in
+  begin try
+    (* The real printing of the implementation *)
+    set_phase Impl;
+    msg_with ft (d.preamble mo opened unsafe_needs);
+    msg_with ft (d.pp_struct struc);
+    Option.iter close_out cout;
+  with e ->
+    Option.iter close_out cout; raise e
+  end;
+  if not dry then Option.iter info_file fn;
+  (* Now, let's print the signature *)
+  Option.iter
+    (fun si ->
+       let cout = open_out si in
+       let ft = formatter false (Some cout) in
+       begin try
+	 set_phase Intf;
+	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
+	 msg_with ft (d.pp_sig (signature_of_structure struc));
+	 close_out cout;
+       with e ->
+	 close_out cout; raise e
+       end;
+       info_file si)
+    (if dry then None else si)
+
+
+(*********************************************)
+(*s Part III: the actual extraction commands *)
+(*********************************************)
+
+
+let reset () =
+  Visit.reset (); reset_tables (); reset_renaming_tables Everything
+
+let init modular =
+  check_inside_section (); check_inside_module ();
+  set_keywords (descr ()).keywords;
+  set_modular modular;
+  reset ();
+  if modular && lang () = Scheme then error_scheme ()
+
+(* From a list of [reference], let's retrieve whether they correspond
+   to modules or [global_reference]. Warn the user if both is possible. *)
+
+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
+      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
+	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
+	| Some mp, Some r ->
+	    warning_both_mod_and_cst q mp r;
+	    let refs,mps = locate_ref l in refs,mp::mps
+
+(*s Recursive extraction in the Coq toplevel. The vernacular command is
+    \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when
+    extracting to a file with the command:
+    \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
+
+let full_extr f (refs,mps) =
+  init 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 ();
+  print_structure_to_file (mono_filename f) false struc;
+  reset ()
+
+let full_extraction f lr = full_extr f (locate_ref lr)
+
+(*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
+      let d = get_decl_in_structure r struc in
+      warning_axioms ();
+      if is_custom r then msgnl (str "(** User defined extraction *)");
+      print_one_decl struc (modpath_of_r r) d;
+      reset ()
+  | _ -> assert false
+
+
+(*s (Recursive) Extraction of a library. The vernacular command is
+  \verb!(Recursive) Extraction Library! [M]. *)
+
+let extraction_library is_rec m =
+  init 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);
+  let env = Global.env () in
+  let l = List.rev (environment_until (Some dir_m)) in
+  let select l (mp,meb) =
+    if Visit.needed_mp mp
+    then (mp, unpack (extract_seb env mp true meb)) :: l
+    else l
+  in
+  let struc = List.fold_left select [] l in
+  let struc = optimize_struct [] struc in
+  warning_axioms ();
+  let print = function
+    | (MPfile dir as mp, sel) as e ->
+	let dry = not is_rec && dir <> dir_m in
+	print_structure_to_file (module_filename mp) dry [e]
+    | _ -> assert false
+  in
+  List.iter print struc;
+  reset ()