mise en place fichiers extraction

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

8 files changed, 1006 insertions, 6 deletions

diff --git a/contrib/extraction/close_env.mli b/contrib/extraction/close_env.mli
new file mode 100644
index 0000000000..066bb2a6d1
--- /dev/null
+++ b/contrib/extraction/close_env.mli
@@ -0,0 +1,9 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+
+val close : global_reference list -> global_reference list
+
+val module_env : identifier -> global_reference list
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f7ff1af88b..f90bf1a6ad 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -1,11 +1,193 @@
 
 (*i $Id$ i*)
 
+open Pp
+open Util
 open Names
 open Term
+open Declarations
+open Environ
+open Reduction
 open Miniml
+open Mlimport
 
-let extract spl = 
-  failwith "TODO"
+(*s Renaming issues. We distinguish between globals and locals. A global table
+    keeps the renamings of globals. And the functor argument will provide
+    functions to renamed other identifiers. *)
 
+(* We keep a table of renamings for the globals.
+   Then every renaming function will be called with its own "avoid list"
+   and the list of already known globals. *)
 
+let globals_renaming = ref ([] : (identifier * identifier) list)
+
+let globals = ref ([] : identifier list)
+
+let reset_globals_renaming () =
+  globals_renaming := [] ;
+  globals          := []
+
+let add_global_renaming ((_,id') as r) = 
+  globals_renaming :=   r::!globals_renaming ;
+  globals          := id'::!globals
+
+let get_global_name id =
+  try  List.assoc id !globals_renaming
+  with Not_found -> anomalylabstrm "Fwtoml.get_global_name"
+    (hOV 0 [< 'sTR "Found a global " ; pr_id id ;
+              'sTR " without renaming" >])
+
+(*s Informations on inductive types: we keep them in a table in order
+    to have quick access to constructor names and arities. *)
+
+type packet_info = { 
+  packet_name    : identifier ;
+  packet_ncons   : int ;
+  packet_cnames  : identifier array ;
+  packet_arities : int array }
+
+let mind_table =
+  (Hashtbl.create 17 : (section_path * int , packet_info) Hashtbl.t)
+
+let reset_mind_table () =
+  Hashtbl.clear mind_table
+
+let store_mind_info key info =
+  Hashtbl.add mind_table key info
+
+let get_mind_info key =
+  Hashtbl.find mind_table key
+
+(*s [name_of_oper] returns the ML name of a global reference. *)
+
+let name_of_oper gr =
+  if is_ml_import gr then
+    find_ml_import gr
+  else if is_ml_extract gr then
+    find_ml_extract gr
+  else match gr with
+    | ConstRef sp -> 
+	get_global_name (basename sp)
+    | IndRef ind ->
+	let info = get_mind_info ind in info.packet_name
+    | ConstructRef (ind,j) ->
+	let info = get_mind_info ind in info.packet_cnames.(j-1)
+    | VarRef _ -> 
+	assert false
+
+(* Other renaming functions are provided within the functor argument. *)
+
+type renaming_function = identifier list -> name -> identifier
+
+module type Renaming = sig
+  val rename_type_parameter : renaming_function
+  val rename_type : renaming_function
+  val rename_term : renaming_function
+  val rename_global_type : renaming_function
+  val rename_global_constructor : renaming_function
+  val rename_global_term : renaming_function
+end
+
+(*s The extraction functor. *)
+
+module type Translation = sig
+  val extract : bool -> global_reference list -> ml_decl list
+end
+
+module Make = functor (R : Renaming) -> struct
+
+  (* The renaming functions must take globals into account *)
+
+  let ren_type_parameter av n = R.rename_type_parameter (!globals @ av) n
+  let ren_type av n = R.rename_type (!globals @ av) n
+  let ren_term av n = R.rename_term (!globals @ av) n
+				  
+  let ren_global_type id = R.rename_global_type !globals (Name id)
+  let ren_global_constructor i = R.rename_global_constructor !globals (Name i)
+  let ren_global_term id = R.rename_global_term !globals (Name id)
+
+  (* Extraction of a type *)
+
+  let prop = id_of_string "prop"
+
+  type type_extraction =
+    | MLtype of ml_type * ml_typeid list * ml_typeid list
+    | Arity
+
+  let extract_type c =
+    let rec extract_rec env pl fl c args = match kind_of_term (whd_beta c) with
+      | IsProd (n, t, d) ->
+	  assert (args = []);
+	  let env' = push_rel (n,None,t) env in
+	  (match extract_rec env pl fl t [] with
+	     | Arity ->
+		 let id = ren_type_parameter pl n in
+		 extract_rec env' (id :: pl) fl d []
+	     | MLtype (t', pl', fl') ->
+		 (match extract_rec env' pl' fl' d [] with
+		    | Arity -> Arity
+		    | MLtype (d', pl'', fl'') -> 
+			MLtype (Tarr (t', d'), pl'', fl'')))
+      | IsSort (Prop Null) ->
+	  assert (args = []);
+	  MLtype (Tglob prop, [], [])
+      | IsSort _ ->
+	  assert (args = []);
+	  Arity
+      | IsApp (d, args') ->
+	  extract_rec env pl fl d (Array.to_list args' @ args)
+      | _ -> 
+	  assert false
+    in
+    extract_rec (Global.env()) [] [] c []
+
+  (* Extraction of a constr *)
+
+  let extract_constr c = 
+    let rec extract_rec env c = match kind_of_term (whd_beta c) with
+      | _ -> 
+	  failwith "todo"
+      | IsSort _ | IsXtra _ | IsVar _ | IsMeta _ ->
+          assert false 
+    in
+    extract_rec (Global.env()) c
+
+  (* Extraction of a constant *)
+
+  let extract_constant sp cb =
+    let id = basename sp in
+    let typ = cb.const_type in
+    let redtyp = whd_betadeltaiota (Global.env()) Evd.empty typ in
+    let body = match cb.const_body with Some c -> c | None -> assert false in
+    if isSort redtyp then begin
+      let id' = ren_global_type id in
+      add_global_renaming (id,id');
+      if is_Prop redtyp then
+	Dabbrev (id', [], Tglob prop)
+      else
+	match extract_type body with
+	  | Arity -> error "not an ML type"
+	  | MLtype (t, vl, fl) -> Dabbrev (id', vl@fl, t)
+    end else begin
+      let id' = ren_global_term id in
+      add_global_renaming (id,id'); 
+      let t = extract_constr body in
+      Dglob (id', t)
+    end
+      
+  (* Extraction of an inductive *)
+
+  let extract_inductive mib =
+    failwith "todo"
+    (* Dtype ... *)
+
+  (* Extraction of a declaration i.e. a constant or an inductive *)
+
+  let extract_decl = function
+    | ConstRef sp -> extract_constant sp (Global.lookup_constant sp)
+    | IndRef (sp,_) -> extract_inductive (Global.lookup_mind sp)
+    | VarRef _ | ConstructRef _ -> assert false
+
+  let extract cofix = List.map extract_decl
+
+end
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 71c9c9be27..485290b033 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -2,7 +2,32 @@
 (*i $Id$ i*)
 
 open Names
+open Term
 open Miniml
 
-val extract : section_path list -> ml_decl list
+(*s Renaming issues. *)
+
+val get_global_name : identifier -> identifier
+
+type renaming_function = identifier list -> name -> identifier
+
+module type Renaming = sig
+  val rename_type_parameter : renaming_function
+  val rename_type : renaming_function
+  val rename_term : renaming_function
+  val rename_global_type : renaming_function
+  val rename_global_constructor : renaming_function
+  val rename_global_term : renaming_function
+end
+
+(*s The extraction functor. It returns a single function [extract]
+    translating a piece of CIC environment into a list of ML declarations.
+    The boolean indicates whether cofix are allowed or not. *)
+
+module type Translation = sig
+  val extract : bool -> global_reference list -> ml_decl list
+end
+
+module Make : functor (R : Renaming) -> Translation
+
 
diff --git a/contrib/extraction/genpp.ml b/contrib/extraction/genpp.ml
new file mode 100644
index 0000000000..27390de44f
--- /dev/null
+++ b/contrib/extraction/genpp.ml
@@ -0,0 +1,140 @@
+
+(*i $Id$ i*)
+
+open Pp_control
+open Pp
+open System
+open Util
+open Names
+open Vernacinterp
+open Mlimport
+open Miniml
+open Genpp
+
+(*s Utility functions. *)
+
+let open_par = function true -> [< 'sTR"(" >] | false -> [< >]
+let close_par = function true -> [< 'sTR")" >] | false -> [< >]
+
+(* uncurry_list : ('a -> std_pcmds) -> 'a list -> std_ppcmds
+ * formats a list [x1;...;xn] in its uncurried form (x1,...,xn). *)
+
+let uncurry_list f = function
+    []  -> [< >]
+  | [x] -> [< (f x) >]
+  | xl  -> [< 'sTR"(" ;
+      	      prlist_with_sep (fun () -> [< 'sTR", " >]) (fun x -> (f x)) xl ;
+	      'sTR")"
+      	    >]
+
+let uncurry_list2 f = function
+    []  -> [< >]
+  | [x] -> [< (f x) >]
+  | xl  -> [< 'sTR"(" ;
+      	      hOV 0 [< prlist_with_sep
+			 (fun () -> [< 'sTR"," ; 'sPC >]) 
+			 (fun x -> (f x)) xl  ;
+		       'sTR")" >]
+      	    >]
+
+type extraction_params = {
+  needed : identifier list;
+  expand : identifier list;
+  expansion : bool;
+  exact : bool
+  }
+
+let list_ids = 
+  List.map (function (VARG_IDENTIFIER id) -> id | _ -> assert false)
+
+let rec parse_rem op = function
+    VARG_STRING "noopt" :: r -> 
+      parse_rem 
+	{ needed = op.needed; expand = op.expand; 
+	  expansion = false; exact = op.exact } r
+  | VARG_STRING "exact" :: r -> 
+      parse_rem 
+	{ needed = op.needed; expand = op.expand; 
+	  expansion = op.expansion; exact = true } r
+  | VARG_STRING "expand" :: VARG_VARGLIST l :: r ->
+      parse_rem { needed = op.needed; expand = op.expand @ list_ids l;
+		  expansion = op.expansion; exact = op.exact } r
+  | [] -> op
+  | _ -> assert false
+
+let parse_param = function
+    VARG_VARGLIST l :: r ->
+      parse_rem { needed = list_ids l; expand = []; 
+		  expansion = true; exact = false } r
+  | _ -> assert false
+
+module type ExtractionParams = sig
+  val opt : extraction_params -> ml_decl list -> ml_decl list
+  val suffixe : string
+  val cofix : bool
+  val pp_of_env : ml_decl list -> std_ppcmds
+  module Renaming : Extraction.Renaming
+end
+
+module Make = functor (M : ExtractionParams) -> struct
+
+  module Translation = Extraction.Make(M.Renaming)
+
+  let change_names =
+    map_succeed 
+      (fun id -> try Extraction.get_global_name id 
+       with Anomaly _ -> failwith "caught") 
+      
+  let exact prm env =
+    let keep = function
+      | Dtype il -> 
+	  List.exists (fun (_,id,_) -> List.mem id prm.needed) il
+      | Dabbrev (id,_,_) -> List.mem id prm.needed
+      | Dglob (id,_) -> List.mem id prm.needed
+    in
+    map_succeed 
+      (fun d -> if not (keep d) then failwith "caught" else d) env
+      
+  let pp cicenv prm =
+    let mlenv = Translation.extract M.cofix cicenv in
+    let needed' = change_names prm.needed in
+    let expand' = change_names prm.expand in
+    let prm' = 
+      { needed = needed' ; expand = expand' ; 
+	expansion = prm.expansion ; exact = prm.exact }
+    in
+    let env = M.opt prm' mlenv in
+    let env = if prm'.exact then exact prm' env else env in
+    M.pp_of_env env
+
+  let pp_recursive prm =
+    let gl = List.map (Nametab.sp_of_id CCI) prm.needed in
+    let cicenv = Close_env.close gl in
+    pp cicenv prm
+
+  let write file strm =
+    let chan = open_trapping_failure open_out file M.suffixe in
+    let ft = with_output_to chan in
+    (try  pP_with ft strm ; pp_flush_with ft ()
+     with e -> pp_flush_with ft () ; close_out chan; raise e);
+    close_out chan
+
+  let write_extraction_file file prm =
+    (* TODO: comment tester qu'il n'y a pas de section ouverte et
+	 pemettre pour autant la compilation (donc une section
+	 particuliere qui est le module) if Lib.cwd() <> [] then
+	 errorlabstrm "Genpp.Pp_to_file.write_extraction_file" [< 'sTR
+	 "There are still open sections !" >]; *)
+    let strm = pp_recursive prm in
+    write file strm
+
+  let write_extraction_module m =
+    let cicenv = Close_env.module_env m in
+    let idl = List.map (Environ.id_of_global (Global.env())) cicenv in
+    let prm = 
+      { needed = idl; expand = []; expansion = false; exact = true } in
+    let strm = pp cicenv prm in
+    let file = string_of_id m in
+    write file strm
+	
+end
diff --git a/contrib/extraction/genpp.mli b/contrib/extraction/genpp.mli
new file mode 100644
index 0000000000..1bd795c090
--- /dev/null
+++ b/contrib/extraction/genpp.mli
@@ -0,0 +1,59 @@
+
+(*i $Id$ i*)
+
+(*s This module defines the generic part of the code production, as a
+    functor [Make] taking extraction parameters as argument (of type
+    [ExtractionParams]), including a renaming functor (of type
+    [Extraction.Renaming]) and returning a module to output the
+    code. *)
+
+open Pp
+open Names
+open Miniml
+open Vernacinterp
+
+(*s Some utility functions, used in instance modules ([Caml], [Ocaml] and 
+    [Haskell]). *)
+
+val open_par : bool -> std_ppcmds
+val close_par : bool -> std_ppcmds
+
+val uncurry_list : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val uncurry_list2 : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+
+(*s Extraction parameters parsed on the command line. *)
+
+type extraction_params = {
+  needed : identifier list;		(*r constants to keep *)
+  expand : identifier list;		(*r constants to expand *)
+  expansion : bool;			(*r do we expand *)
+  exact : bool				(*r without recursivity *)
+}
+
+val parse_param : vernac_arg list -> extraction_params
+
+(*s The whole bunch of extraction parameters has the following signature. *)
+
+module type ExtractionParams = 
+  sig
+    (* optimisation function *)
+    val opt : extraction_params -> ml_decl list -> ml_decl list
+    (* file suffix *)
+    val suffixe : string
+    (* co-inductive types are (not) allowed *)
+    val cofix : bool
+    (* pretty-print function *)
+    val pp_of_env : ml_decl list -> std_ppcmds
+    (* the renaming functions *)
+    module Renaming : Extraction.Renaming
+  end
+
+(*s The functor itself. *)
+
+module Make : functor (M : ExtractionParams) ->
+  sig
+    module Translation : Extraction.Translation
+    val pp_recursive : extraction_params -> std_ppcmds
+    val write_extraction_file : string -> extraction_params -> unit
+    val write_extraction_module : identifier -> unit
+  end
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 2a2a5c83d8..8cca3b4913 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -5,9 +5,7 @@ open Names
 
 (* identifiers of type are either parameters or type names. *)
 
-type ml_typeid = 
-  | Tparam of identifier
-  | Tname  of identifier
+type ml_typeid = identifier
 
 (* ML type expressions. *)
 
diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml
new file mode 100644
index 0000000000..7f8150f106
--- /dev/null
+++ b/contrib/extraction/mlimport.ml
@@ -0,0 +1,497 @@
+
+(*i $Id$ i*)
+
+open Pp
+
+(* TODO : move this function to another file, like more_util. *)
+
+let list0n = 
+  let rec gen acc = function
+      -1 -> acc
+    | n  -> gen (n::acc) (n-1)
+  in 
+  gen []
+
+(* get a fresh name if necessary *)
+let rec next_global_ident id =
+  if not (is_global id) then id else next_global_ident (lift_ident id)
+
+(*s Importing ML objects, and linking axioms to terms. *)
+
+(* A table to keep the ML imports. *)
+
+let ml_import_tab = (Hashtabl.create 17 : (sorts oper, identifier) Hashtabl.t)
+
+let mL_INDUCTIVES = ref ([] : section_path list)
+
+let add_ml_inductive_import sp =
+  if not (List.mem sp !mL_INDUCTIVES) then
+    mL_INDUCTIVES := sp :: !mL_INDUCTIVES
+
+let add_ml_import imp id =
+  Hashtabl.add ml_import_tab imp id ;
+  match imp with
+    MutInd (sp,_) -> add_ml_inductive_import sp
+  | _ -> ()
+
+let find_ml_import imp = Hashtabl.find ml_import_tab imp
+
+let is_ml_import op =
+  try let _ = find_ml_import op in true with Not_found -> false
+
+let sp_is_ml_import sp =
+     (is_ml_import (Const sp))
+  or (is_ml_import (MutInd (sp,0)))
+  or (is_ml_import (MutConstruct ((sp,0),1)))
+
+let sp_prod = path_of_string "#Datatypes#prod.fw"
+
+let sp_is_ml_import_or_prod sp =
+  (sp = sp_prod) or (sp_is_ml_import sp)
+
+let inMLImport,outMLImport =
+  declare_object ("MLIMPORT",
+     {load_function = (fun _ -> ());
+      cache_function         = (fun (_,(imp,id)) -> add_ml_import imp id) ;
+      specification_function = (fun x -> x) })
+
+(* A table to keep the extractions to ML objects *)
+
+let ml_extract_tab = (Hashtabl.create 17 : (sorts oper, identifier) Hashtabl.t)
+
+let add_ml_extract op id =
+  Hashtabl.add ml_extract_tab op id;
+  match op with 
+      MutInd (sp,_) -> add_ml_inductive_import sp
+    | _ -> ()
+
+let find_ml_extract = Hashtabl.find ml_extract_tab
+
+let is_ml_extract op = 
+  try let _ = find_ml_extract op in true with Not_found -> false
+
+let sp_is_ml_extract sp =
+     (is_ml_extract (Const sp))
+  or (is_ml_extract (MutInd (sp,0)))
+  or (is_ml_extract (MutConstruct ((sp,0),1)))
+
+let inMLExtract,outMLExtract =
+  declare_object ("MLEXTRACT",
+     {load_function = (fun _ -> ());
+      cache_function         = (fun (_,(op,id)) -> add_ml_extract op id) ;
+      specification_function = (fun x -> x) })
+
+let is_import_or_extract sp = sp_is_ml_import sp or sp_is_ml_extract sp
+
+(* Those two tables are rolled-back *)
+
+let freeze () =
+  (Hashtabl.freeze ml_import_tab, !mL_INDUCTIVES,
+   Hashtabl.freeze ml_extract_tab)
+
+let unfreeze (ft,stk,et) =
+  Hashtabl.unfreeze ft ml_import_tab;
+  mL_INDUCTIVES := stk;
+  Hashtabl.unfreeze et ml_extract_tab
+
+let _ = declare_summary "MLIMPORT-TABLE"
+  { freeze_function   = freeze ;
+    unfreeze_function = unfreeze ;
+    init_function     = (fun () -> Hashtabl.clear ml_import_tab;
+      	       	       	       	   mL_INDUCTIVES := [];
+				   Hashtabl.clear ml_extract_tab) }
+
+(* Replace CCI section_path with FW section_path in a term. *)
+
+let whd_fwify = function
+    DOPN(Const sp,cl)               -> DOPN(Const (fwsp_of sp),cl)
+  | DOPN(MutInd(sp,i),cl)           -> DOPN(MutInd (fwsp_of sp,i),cl)
+  | DOPN(MutConstruct((sp,j),i),cl) -> DOPN(MutConstruct((fwsp_of sp,j),i),cl)
+  | x                               -> x
+
+let fwify = strong whd_fwify
+
+let fwsp_of_id id =
+  try Nametab.fw_sp_of_id id
+  with Not_found -> errorlabstrm "fwsp_of_id"
+       [< 'sTR(string_of_id id) ; 'sTR" is not a defined informative object" >]
+
+
+(**************************************************************************)
+(*                      ML Import file__name : type.                      *)
+(**************************************************************************)
+
+(***** constants__make_parameter_body *****)
+let make_fw_parameter_body (hyps,jt) =
+  match level_of_type jt with
+    (Prop Pos) | (Type _) ->
+      {cONSTKIND = FW;
+       cONSTHYPS=hyps;
+       cONSTBODY=None;
+       cONSTEVAL = None;
+       cONSTOPAQUE = true;
+       cONSTTYPE= jt;
+       cONSTIMPARGS = NO_IMPL }
+  | _ -> errorlabstrm "make_fw_parameter_body" 
+         [< Printer.fprtype jt ; 'sTR " is not an informative term." >]
+
+
+(***** constants__infexecute_parameter *****)
+let fw_infexecute_parameter fhyps name t =
+  let sp = Lib.make_path OBJ name in
+  let (u,j) = fexecute_type_with_univ empty_evd fhyps sp t in
+  let ids = auto_save_variables() in
+  let fhyps' = thin_to_level fhyps (body_of_type j) in
+    (u,[FW,make_fw_parameter_body (fhyps',j)])
+
+
+(***** declare__machine_parameter *****)
+let fw_machine_parameter fhyps (name,cty) =
+  let (u',cmap) = fw_infexecute_parameter fhyps name cty in
+    add_named_object (name,OBJ) (inConstant(cmap,NeverDischarge,u'))
+
+
+(***** command__parameter_def_var *****)
+let fw_parameter id com =
+  let tcci = fconstr_of_com empty_evd (initial_fsign()) com in
+  let tfw = fwify tcci in
+  let _,fhyps = initial_assumptions() in
+  fw_machine_parameter fhyps (id,tfw)
+
+
+let ml_import id' id com =
+  fw_parameter id com ;
+  let sp = Lib.make_path FW id in
+  add_anonymous_object (inMLImport (Const sp, id')) ;
+  mSGNL [< 'sTR(string_of_id id) ; 'sTR" imported." >]
+
+
+let id_of_varg = function
+    VARG_IDENTIFIER id -> id
+  | VARG_STRING s -> (try id_of_string s with _ -> id_of_string (" "^s))
+  | _ -> invalid_arg "id_of_varg"
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("ML_IMPORT", function
+   [id'; VARG_IDENTIFIER id; VARG_COMMAND com] -> 
+     (fun () -> ml_import (id_of_varg id') id com)
+ | _ -> anomaly "ML_IMPORT called with bad arguments.")
+
+
+
+(**************************************************************************)
+(*                         Link ident := Fw-term.                         *)
+(**************************************************************************)
+
+let not_an_axiom id =
+  errorlabstrm "ml_import__fw_link"
+  [< 'sTR(string_of_id id) ; 'sTR" is not an FW axiom." >]
+
+
+let not_have_type env cb' cb =
+  let c = match cb'.cONSTBODY with
+      Some {contents=COOKED x} -> x
+    | _ -> anomaly "ml_import__not_have_type: should be a constant" in
+    errorlabstrm "Ml_import.not_convertible"
+  [< pENV [< 'sTR"In environment " >] env ; 'fNL ;
+     'sTR"The term: " ; pFTERMINENV(env,c) ; 'sPC ; 
+     'sTR"does not have type" ; 'sPC ; pFTYPEINENV(env,cb.cONSTTYPE) ;
+     'sTR"." ; 'fNL ;
+     'sTR"Actually, it has type" ; 'sPC ; pFTYPEINENV(env,cb'.cONSTTYPE) >]
+
+
+let fw_infexecute_constant fhyps id c =
+  let sp = Lib.make_path OBJ id in
+  let (u,j) = fexecute_with_univ empty_evd fhyps sp c in
+  let ids = auto_save_variables() in
+  let fhyps' = thin_to_level fhyps j._KIND in
+    (u,[FW, make_constant_body FW false (fhyps',j)])
+
+
+let fw_link id com =
+
+  (*** First we check that id corresponds to an informative axiom. ***)
+  let sp = fwsp_of_id id in
+  let osp = objsp_of sp in
+  let (cmap,s,u) = match Lib.leaf_object_tag osp with
+                     "CONSTANT" -> outConstant (Lib.map_leaf osp)
+		   | _ -> not_an_axiom id in
+  let cb = try Listmap.map cmap FW
+           with Not_found -> not_an_axiom id in
+  if cb.cONSTBODY <> None then not_an_axiom id ;
+
+  (*** Then we execute the term com. ***)
+  let (hyps,fhyps) = initial_assumptions() in
+  let tcci = fconstr_of_com empty_evd hyps com in
+  let tfw = fwify tcci in
+  let (u',cmap') = fw_infexecute_constant fhyps id tfw in
+  let cb' = Listmap.map cmap' FW in
+
+  (*** We check that the type of com is convertible with cb.CONSTTYPE ***)
+  if (not (conv empty_evd 
+	     (body_of_type cb.cONSTTYPE) 
+	     (body_of_type cb'.cONSTTYPE))) then
+    not_have_type (gLOB fhyps) cb' cb ;
+
+  (*** At last, we transform the original axiom into a constant. ***)
+(**lib__remap (osp,lib__LEAF (inConstant(listmap__remap cmap FW cb',s,u))); **)
+  cb.cONSTBODY <- cb'.cONSTBODY ;
+  cb.cONSTOPAQUE <- false ;
+
+  let c = match cb'.cONSTBODY with
+      Some {contents=COOKED x} -> x
+    | _ -> anomaly "ml_import__fw_link: should be a constant" in
+  mSGNL (hOV 0 [< 'sTR"Constant " ; print_id id ; 'sTR" linked to" ; 'sPC ;
+		  pFTERM c >])
+
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("LINK", function
+   [VARG_IDENTIFIER id; VARG_COMMAND com] -> (fun () -> fw_link id com)
+ | _ -> anomaly "ML_IMPORT called with bad arguments.")
+
+
+
+(**************************************************************************)
+(*       ML Inductive name [ c1 ... cn ] == <Inductive Definition>.       *)
+(**************************************************************************)
+(*                     ML Inductive name1 [ c1,1 ... c1,n1 ]              *)
+(*                                  ...                                   *)
+(*                    	       	    namek [ ck,1 ... ck,nk ]              *)
+(*                     == <Mutual Inductive Definition>.                  *)
+(**************************************************************************)
+
+(***** declare__machine_minductive *****)
+let fw_machine_minductive fhyps nparams mispecvec finite = 
+  if Array.length mispecvec = 0 then anomaly "fw_machine_minductive" 
+  else 
+   let mindidvec = 
+     Array.map (fun  (indid,_,_,_,_) -> indid) mispecvec
+   and arlcvec = 
+     Array.map (fun  (_,_,indarity,indconstructors,_) ->
+      	       	       	 (indarity,indconstructors)) mispecvec
+   and namesvec = 
+     Array.map (fun  (indid,indstamp,_,_,consnames) -> 
+      	       	       	 (indstamp,indid,consnames)) mispecvec in
+
+  let sp = Lib.make_path OBJ mindidvec.(0) in
+  let (u',mimap) = with_universes 
+      (execute_minductive fhyps nparams namesvec finite)
+                               (sp,initial_universes,arlcvec) in
+
+  (***  declare_minductive (mindidvec,mimap,u')  ***)
+  add_named_object (mindidvec.(0),OBJ) (inMutualInductive (mimap,u'))
+  (***  do_vect declare_eliminations mindidvec  ***)
+
+
+(***** trad__fconstruct *****)
+let fw_fconstruct sigma fsign com =
+  let c = fconstr_of_com sigma fsign com in
+  Mach.fexecute_type sigma fsign c
+
+
+(***** command__build_mutual *****)
+let fw_build_mutual lparams lnamearconstrs finite =
+
+  let lrecnames = List.map (fun (x,_,_)->x)  lnamearconstrs
+  and nparams = List.length lparams
+  and sign0 = initial_fsign() in
+
+  let (ind_sign,arityl) = List.fold_left 
+    (fun (sign,arl) (recname,arityc,_) -> 
+      let arity = fw_fconstruct empty_evd sign0 (mkProdCit lparams arityc) in
+      (add_sign (recname,arity) sign, (arity::arl)))
+      (sign0,[]) lnamearconstrs in
+
+  let mispecvec = Array.of_list 
+    (List.map2 (fun ar (name,_,lname_constr) -> 
+    let consconstrl = List.map 
+     (fun (_,constr) -> 
+      	let c = fconstr_of_com empty_evd ind_sign 
+		  (mkProdCit lparams constr)
+      	in fwify c) lname_constr in
+    (name,Anonymous,ar,
+        put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl),
+              Array.of_list (List.map fst lname_constr)))
+    (List.rev arityl) lnamearconstrs) in
+
+  let _,fhyps = initial_assumptions() in
+  fw_machine_minductive fhyps nparams mispecvec finite
+
+
+let not_same_number_types () =
+  errorlabstrm "ml_import__ml_import_inductive"
+  [< 'sTR"Not the same number of types." >]
+
+let not_same_number_constructors (id,id') =
+  errorlabstrm "ml_import__ml_import_inductive"
+    (hOV 0
+       [< 'sTR"The ML type" ; 'sPC ; print_id id ;
+          'sTR" and the FW type" ; 'sPC ; print_id id' ; 'sPC ;
+          'sTR"do not have the same number" ;
+      	  'sPC ; 'sTR"of constructors." >])
+
+let ml_import_inductive names lparams lnamearconstrs finite =
+
+  let assoc_list =
+    if (List.length names) <> (List.length lnamearconstrs) then
+      not_same_number_types ()
+    else
+      List.fold_right2 (fun (id,l) (id',_,l') acc ->
+      	  if (List.length l)<>(List.length l') then
+	    not_same_number_constructors (id,id')
+	  else
+	    ( (id,id'), List.combine l (List.map fst l') )::acc ) 
+            names lnamearconstrs [] in
+
+  fw_build_mutual lparams lnamearconstrs finite;
+
+  List.iter
+      (fun i ->
+      	  let (mlid,id), l = List.nth assoc_list i in
+      	  let sp = Lib.make_path FW id in
+	  add_anonymous_object (inMLImport (MutInd (sp,i), mlid)) ;
+	  List.iter (fun j ->
+      	      let (mlid,id) = List.nth l (j-1) in
+      	      add_anonymous_object
+      	       	       	   (inMLImport (MutConstruct ((sp,i),j), mlid)) )
+	  (List.tl (list0n (List.length l))) )
+      (list0n ((List.length assoc_list) - 1)) ;
+
+  pPNL [< 'sTR"ML inductive type(s) " ;
+      	  prlist_with_sep (fun () -> [< 'sTR"," ; 'sPC >])
+	                  (fun (id,_) -> [< 'sTR(string_of_id id) >]) names ;
+         'sTR" imported." >]
+  
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("ML_ONEINDUCTIVE",
+    function [VARG_VARGLIST nl;
+         VARG_IDENTIFIER s;
+         VARG_COMMAND c;
+         VARG_BINDERLIST binders;
+         VARG_BINDERLIST constructors] ->
+        if List.length nl <> 1 then not_same_number_types () ;
+	(match nl with
+	     [VARG_VARGLIST (v::l)] ->
+	       let cnames = List.map id_of_varg l in
+               let la = join_binders binders in
+               let li = List.map (fun (l,c) -> (List.hd l,c)) constructors in
+        	 (function () -> ml_import_inductive [id_of_varg v,cnames] 
+		      la [(s,c,li)] true)
+	   | _ -> assert false)
+      | _ -> anomaly "ML_ONEINDUCTIVE called with bad arguments.")
+
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("ML_MUTUALINDUCTIVE",
+    function [VARG_VARGLIST l;
+      	 VARG_BINDERLIST binders;
+      	 VARG_VARGLIST indl] ->
+	let names = 
+	  List.map (function (VARG_VARGLIST (v::ll)) ->
+      	       	      id_of_varg v, List.map id_of_varg ll
+		      | _ -> assert false) l in
+        let la = join_binders binders in
+        let lnamearconstructs = 
+          List.map (function (VARG_VARGLIST [VARG_IDENTIFIER arid;
+      	       	       	       	   VARG_COMMAND arc;
+      	       	       	       	   VARG_BINDERLIST lconstr])
+                	-> (arid,arc,
+			    List.map (fun (l,c) -> (List.hd l,c)) lconstr)
+		      | _ -> assert false)
+      	      indl in
+        (function () -> ml_import_inductive names la lnamearconstructs true)
+      | _ -> anomaly "ML_MUTUALINDUCTIVE called with bad arguments.")
+
+
+
+(**************************************************************************)
+(*                       Extract Constant id => id                        *)
+(*        Extract Inductive (id [id ... id])+ => (id [id ... id])+        *)
+(**************************************************************************)
+
+let extract_constant id id' =
+  try
+    let sp = Nametab.sp_of_id FW id in
+      (match global_operator sp id with
+	   Const _,_ -> add_anonymous_object (inMLExtract (Const sp,id'))
+	 | _ -> raise Not_found)
+  with Not_found ->
+    errorlabstrm "Ml_import.extract_constant"
+      [< pID id; 'sPC; 'sTR"is not an FW constant" >]
+
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("EXTRACT_CONSTANT",
+  function 
+      [VARG_IDENTIFIER id; id'] -> 
+	fun () -> extract_constant id (id_of_varg id')
+    | _ -> assert false)
+
+
+let extract_inductive id (id2,l2) =
+  try
+    let sp = Nametab.sp_of_id FW id in
+      (match global_operator sp id with
+	  MutInd (sp,i),_ -> 
+	    add_anonymous_object (inMLExtract (MutInd (sp,i),id2));
+	    (* TODO: verifier le nombre de constructeurs *)
+	    List.iter
+	      (fun (id,j) -> 
+		 add_anonymous_object 
+		   (inMLExtract (MutConstruct ((sp,i),j),id)))
+	      (List.combine l2 (List.tl (list0n (List.length l2))))
+	| _ -> raise Not_found)
+  with Not_found ->
+    errorlabstrm "Ml_import.extract_inductive"
+      [< pID id; 'sPC; 'sTR"is not an FW inductive type" >]
+
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("EXTRACT_INDUCTIVE",
+  function 
+      [VARG_IDENTIFIER id1; VARG_VARGLIST (id2::l2)] ->
+	fun () -> extract_inductive id1 (id_of_varg id2,List.map id_of_varg l2)
+    | _ -> assert false)
+
+
+(**************************************************************************)
+(*                            Fw Print ident.                             *)
+(*                     To see FW constants or axioms.                     *)
+(**************************************************************************)
+
+let fprint_recipe = function
+    Some{contents=COOKED c} -> pFTERM c
+  | Some{contents=RECIPE _} -> [< 'sTR"<recipe>" >]
+  | None -> [< 'sTR"<uncookable>" >]
+
+
+let fprint_name id =
+  try let sp = Nametab.sp_of_id FW id in
+      let obj = Lib.map_leaf (objsp_of sp) in
+      (match object_tag obj with
+       	 "CONSTANT" ->
+      	     let (cmap,_,_) = outConstant obj in
+	     let {cONSTBODY=val_0;cONSTTYPE=typ} = Listmap.map cmap FW in
+	     hOV 0 (match val_0 with
+	        None -> [< 'sTR"*** [ "; 'sTR(string_of_id id);  'sTR " : ";
+                           'cUT ; fprtype typ ; 'sTR" ]"; 'fNL >] 
+	      | _    -> [< 'sTR(string_of_id id); 'sTR" = " ; 
+                           fprint_recipe val_0 ;
+	                   'fNL ; 'sTR "     : "; fprtype typ ; 'fNL >] )
+
+       | "MUTUALINDUCTIVE" ->
+       	     let (cmap,_) = outMutualInductive obj in
+	     [< print_mutual FW (Listmap.map cmap FW) ; 'fNL >]
+  
+       | _ -> invalid_arg "fprint_name" )
+  with Not_found | Invalid_argument _ -> errorlabstrm "ml_import__fprint_name"
+                    [< 'sTR(string_of_id id) ; 'sTR" is not an FW constant." >]
+
+
+(*** TODO: remove overwriting ***)
+let _ = overwriting_vinterp_add("FWPRINT",
+    function [VARG_IDENTIFIER id] -> (function () -> mSG(fprint_name id))
+      | _ -> anomaly "FWPRINT called with bad arguments.")
+
diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli
new file mode 100644
index 0000000000..ac32f5139f
--- /dev/null
+++ b/contrib/extraction/mlimport.mli
@@ -0,0 +1,90 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+
+val is_ml_import : global_reference -> bool
+val find_ml_import : global_reference -> identifier
+
+val find_ml_extract : global_reference -> identifier
+val is_ml_extract : global_reference -> bool
+
+(*
+val list0n : int -> int list
+val next_global_ident : Names.identifier -> Names.identifier
+val ml_import_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
+val mL_INDUCTIVES : Names.section_path list ref
+val add_ml_inductive_import : Names.section_path -> unit
+val add_ml_import : Term.sorts Term.oper -> Names.identifier -> unit
+val sp_is_ml_import : Names.section_path -> bool
+val sp_prod : Names.section_path
+val sp_is_ml_import_or_prod : Names.section_path -> bool
+val inMLImport : Term.sorts Term.oper * Names.identifier -> Libobject.obj
+val outMLImport : Libobject.obj -> Term.sorts Term.oper * Names.identifier
+val ml_extract_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
+val add_ml_extract : Term.sorts Term.oper -> Names.identifier -> unit
+val sp_is_ml_extract : Names.section_path -> bool
+val inMLExtract : Term.sorts Term.oper * Names.identifier -> Libobject.obj
+val outMLExtract : Libobject.obj -> Term.sorts Term.oper * Names.identifier
+val is_import_or_extract : Names.section_path -> bool
+val freeze :
+  unit ->
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
+  Names.section_path list *
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t
+val unfreeze :
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
+  Names.section_path list *
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t -> unit
+val whd_fwify : 'a Term.oper Generic.term -> 'a Term.oper Generic.term
+val fwify : Reduction.reduction_function
+val fwsp_of_id : Names.identifier -> Names.section_path
+val make_fw_parameter_body :
+  Term.type_judgement Names.signature * Term.type_judgement ->
+  Constrtypes.constant_body
+val fw_infexecute_parameter :
+  Term.context ->
+  Names.identifier ->
+  Term.constr ->
+  Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
+val fw_machine_parameter :
+  Term.context -> Names.identifier * Term.constr -> unit
+val fw_parameter : Names.identifier -> CoqAst.t -> unit
+val ml_import : Names.identifier -> Names.identifier -> CoqAst.t -> unit
+val id_of_varg : Vernacinterp.vernac_arg -> Names.identifier
+val not_an_axiom : Names.identifier -> 'a
+val not_have_type :
+  Term.environment ->
+  Constrtypes.constant_body -> Constrtypes.constant_body -> 'a
+val fw_infexecute_constant :
+  Term.context ->
+  Names.identifier ->
+  Term.constr ->
+  Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
+val fw_link : Names.identifier -> CoqAst.t -> unit
+val fw_machine_minductive :
+  Term.context ->
+  int ->
+  (Names.identifier * Names.name * Term.type_judgement * Term.constr *
+   Names.identifier array)
+  array -> bool -> unit
+val fw_fconstruct :
+  'a Evd.evar_map -> Term.context -> CoqAst.t -> Term.type_judgement
+val fw_build_mutual :
+  (Names.identifier * CoqAst.t) list ->
+  (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
+  bool -> unit
+val not_same_number_types : unit -> 'a
+val not_same_number_constructors : Names.identifier * Names.identifier -> 'a
+val ml_import_inductive :
+  (Names.identifier * Names.identifier list) list ->
+  (Names.identifier * CoqAst.t) list ->
+  (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
+  bool -> unit
+val extract_constant : Names.identifier -> Names.identifier -> unit
+val extract_inductive :
+  Names.identifier -> Names.identifier * Names.identifier list -> unit
+val fprint_recipe : Constrtypes.recipe ref option -> Pp.std_ppcmds
+val fprint_name : Names.identifier -> Pp.std_ppcmds
+*)