nouveau design ou le renommage sera fait a posteriori

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

7 files changed, 214 insertions, 243 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
new file mode 100644
index 0000000000..74a7455f94
--- /dev/null
+++ b/contrib/extraction/Extraction.v
@@ -0,0 +1,2 @@
+
+Declare ML Module "extraction.cmo".
diff --git a/contrib/extraction/close_env.ml b/contrib/extraction/close_env.ml
new file mode 100644
index 0000000000..2b4c66da6c
--- /dev/null
+++ b/contrib/extraction/close_env.ml
@@ -0,0 +1,11 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+
+let close gl =
+  failwith "todo"
+
+let module_env m = 
+  failwith "todo"
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index f90bf1a6ad..6166481431 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -8,186 +8,156 @@ open Term
 open Declarations
 open Environ
 open Reduction
+open Instantiate
 open Miniml
 open Mlimport
 
-(*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 _ -> 
+(*s Extraction results. *)
+
+type type_var = Varity | Vskip
+
+type signature = (type_var * identifier) list
+
+type type_extraction_result =
+  | Tmltype of ml_type * signature * identifier list
+  | Tarity
+
+type extraction_result =
+  | Emltype of ml_type * signature * identifier list
+  | Emlterm of ml_ast
+
+let flexible_name = id_of_string "flex"
+
+let id_of_name = function
+  | Anonymous -> id_of_string "_"
+  | Name id   -> id
+
+(*s Extraction of a type. *)
+
+let rec extract_type c =
+  let genv = Global.env() in
+  let rec extract_rec env sign fl c args = match kind_of_term (whd_beta c) with
+    | IsProd (n, t, d) ->
+	assert (args = []);
+	let id = id_of_name n in (* FIXME: capture problem *)
+	let env' = push_rel (n,None,t) env in
+	(match extract_rec env sign fl t [] with
+	   | Tarity ->
+	       extract_rec env' ((Varity,id) :: sign) fl d []
+	   | Tmltype (t', _, fl') ->
+	       (match extract_rec env' ((Vskip,id) :: sign) fl' d [] with
+		  | Tarity -> Tarity
+		  | Tmltype (d', sign', fl'') -> 
+		      Tmltype (Tarr (t', d'), sign', fl'')))
+    | IsSort (Prop Null) ->
+	assert (args = []);
+	Tmltype (Tprop, [], [])
+    | IsSort _ ->
+	assert (args = []);
+	Tarity
+    | IsApp (d, args') ->
+	extract_rec env sign fl d (Array.to_list args' @ args)
+    | IsRel n ->
+	(match List.nth sign (pred n) with
+	   | Vskip, id -> Tmltype (Tvar id, sign, id :: fl)
+	   | Varity, id -> Tmltype (Tvar id, sign, fl))
+    | IsConst (sp,a) ->
+	let cty = constant_type genv Evd.empty (sp,a) in
+	if is_arity genv Evd.empty cty then
+	  (match extract_constant sp with
+	     | Emltype (_, sc, flc) ->
+		 assert (List.length sc = List.length args);
+		 let (mlargs,fl') = 
+		   List.fold_left 
+		     (fun ((args,fl) as acc) (v,a) -> match v with
+			| Vskip,_ -> acc
+			| Varity,_ -> match extract_rec env sign fl a [] with
+			    | Tarity -> assert false
+			    | Tmltype (mla,_,fl') -> (mla :: args, fl')
+		     )
+		     ([],fl) (List.combine sc args)
+		 in
+		 let flc = List.map (fun i -> Tvar i) flc in
+		 Tmltype (Tapp ((Tglob (ConstRef sp)) :: mlargs @ flc), 
+			  sign, fl')
+	     | Emlterm _ -> 
+		 assert false)
+	else
+	  failwith "todo: expanse c, reduce and apply recursively"
+    | IsMutInd _ ->
+	failwith "todo"
+    | IsMutCase _ 
+    | IsFix _ ->
+	let id = next_ident_away flexible_name fl in
+	Tmltype (Tvar id, sign, id :: fl)
+    | IsCast (c, _) ->
+	extract_rec env sign fl c args
+    | _ -> 
 	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
+  in
+  extract_rec (Global.env()) [] [] c []
+
+(*s Extraction of a term. *)
+
+and extract_term c =
+  failwith "todo"
+(*i
+  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
+i*)
+
+(*s Extraction of a constr. *)
+
+and extract_constr_with_type c t =
+  let redt = whd_betadeltaiota (Global.env()) Evd.empty t in
+  if isSort redt then begin
+    if is_Prop redt then
+      Emltype (Tprop, [], [])
+    else
+      match extract_type c with
+	| Tarity -> error "not an ML type"
+	| Tmltype (t, sign, fl) -> Emltype (t, sign, fl)
+  end else 
+    let t = extract_term c in
+    Emlterm t
+
+and extract_constr c = 
+  extract_constr_with_type c (Typing.type_of (Global.env()) Evd.empty c)
+
+(*s Extraction of a constant. *)
+
+and extract_constant sp =
+  let cb = Global.lookup_constant sp in
+  let typ = cb.const_type in
+  let body = match cb.const_body with Some c -> c | None -> assert false in
+  extract_constr_with_type body typ
       
-  (* Extraction of an inductive *)
+(*s Extraction of an inductive. *)
+
+and extract_inductive sp =
+  let mib = Global.lookup_mind sp in
+  failwith "todo"
+  (* Dtype ... *)
 
-  let extract_inductive mib =
-    failwith "todo"
-    (* Dtype ... *)
+(*s Extraction of a global reference i.e. a constant or an inductive. *)
 
-  (* Extraction of a declaration i.e. a constant or an inductive *)
+and extract_reference = function
+  | ConstRef sp -> extract_constant sp
+  | IndRef (sp,_) -> extract_inductive sp
+  | VarRef _ | ConstructRef _ -> assert false
 
-  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
+(*s ML declaration from a reference. *)
 
-  let extract cofix = List.map extract_decl
+let params_of_sign = 
+  List.fold_left (fun l v -> match v with Vskip,_ -> l | _,id -> id :: l) []
 
-end
+let extract_declaration r = 
+  let id = basename (Global.sp_of_global r) in (* FIXME *)
+  match extract_reference r with
+    | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt)
+    | Emlterm t -> Dglob (id, t)
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 485290b033..b42091289a 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -5,29 +5,24 @@ open Names
 open Term
 open Miniml
 
-(*s Renaming issues. *)
+(*s Result of an extraction. *)
 
-val get_global_name : identifier -> identifier
+type type_var = Varity | Vskip
 
-type renaming_function = identifier list -> name -> identifier
+type signature = (type_var * identifier) list
 
-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
+type extraction_result =
+  | Emltype of ml_type * signature * identifier list
+  | Emlterm of ml_ast
 
-(*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. *)
+(*s Extraction functions. *)
 
-module type Translation = sig
-  val extract : bool -> global_reference list -> ml_decl list
-end
+val extract_constr : constr -> extraction_result
 
-module Make : functor (R : Renaming) -> Translation
+val extract_reference : global_reference -> extraction_result
+
+(*s ML declaration corresponding to a Coq reference. *)
+
+val extract_declaration : global_reference -> ml_decl
 
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 8cca3b4913..8493b308ec 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -2,6 +2,7 @@
 (*i $Id$ i*)
 
 open Names
+open Term
 
 (* identifiers of type are either parameters or type names. *)
 
@@ -13,7 +14,8 @@ type ml_type =
   | Tvar  of ml_typeid
   | Tapp  of ml_type list
   | Tarr  of ml_type * ml_type
-  | Tglob of identifier
+  | Tglob of global_reference
+  | Tprop
       
 (* ML inductive types. *)
 
@@ -25,7 +27,7 @@ type ml_ast =
   | MLrel   of int
   | MLapp   of ml_ast * ml_ast list
   | MLlam   of identifier * ml_ast
-  | MLglob  of identifier
+  | MLglob  of global_reference
   | MLcons  of int * identifier * ml_ast list
   | MLcase  of ml_ast * (identifier * identifier list * ml_ast) array
   | MLfix   of int * bool * (identifier list) * (ml_ast list)
diff --git a/contrib/extraction/mlimport.ml b/contrib/extraction/mlimport.ml
index 7f8150f106..12e39d0441 100644
--- a/contrib/extraction/mlimport.ml
+++ b/contrib/extraction/mlimport.ml
@@ -2,6 +2,11 @@
 (*i $Id$ i*)
 
 open Pp
+open Names
+open Term
+open Libobject
+open Declare
+open Summary
 
 (* TODO : move this function to another file, like more_util. *)
 
@@ -20,29 +25,29 @@ let rec next_global_ident id =
 
 (* A table to keep the ML imports. *)
 
-let ml_import_tab = (Hashtabl.create 17 : (sorts oper, identifier) Hashtabl.t)
+let ml_import_tab = ref (Gmap.empty : (global_reference, identifier) Gmap.t)
 
-let mL_INDUCTIVES = ref ([] : section_path list)
+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
+  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 ;
+  ml_import_tab := Gmap.add imp id !ml_import_tab;
   match imp with
-    MutInd (sp,_) -> add_ml_inductive_import sp
-  | _ -> ()
+    | IndRef (sp,_) -> add_ml_inductive_import sp
+    | _ -> ()
 
-let find_ml_import imp = Hashtabl.find ml_import_tab imp
+let find_ml_import imp = Gmap.find imp !ml_import_tab
 
 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)))
+     (is_ml_import (ConstRef sp))
+  or (is_ml_import (IndRef (sp,0)))
+  or (is_ml_import (ConstructRef ((sp,0),1)))
 
 let sp_prod = path_of_string "#Datatypes#prod.fw"
 
@@ -51,71 +56,57 @@ let sp_is_ml_import_or_prod 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) })
+     { load_function = (fun _ -> ());
+       open_function = (fun (_,(imp,id)) -> add_ml_import imp id);
+       cache_function = (fun (_,(imp,id)) -> add_ml_import imp id);
+       export_function = (fun x -> Some x) })
 
 (* A table to keep the extractions to ML objects *)
 
-let ml_extract_tab = (Hashtabl.create 17 : (sorts oper, identifier) Hashtabl.t)
+let ml_extract_tab = ref (Gmap.empty : (global_reference, identifier) Gmap.t)
 
 let add_ml_extract op id =
-  Hashtabl.add ml_extract_tab op id;
+  ml_extract_tab := Gmap.add op id !ml_extract_tab;
   match op with 
-      MutInd (sp,_) -> add_ml_inductive_import sp
+    | IndRef (sp,_) -> add_ml_inductive_import sp
     | _ -> ()
 
-let find_ml_extract = Hashtabl.find ml_extract_tab
+let find_ml_extract gr = Gmap.find gr !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)))
+     (is_ml_extract (ConstRef sp))
+  or (is_ml_extract (IndRef (sp,0)))
+  or (is_ml_extract (ConstructRef ((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) })
+     { load_function = (fun _ -> ());
+       open_function = (fun (_,(op,id)) -> add_ml_extract op id);
+       cache_function = (fun (_,(op,id)) -> add_ml_extract op id);
+       export_function = (fun x -> Some 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)
+  (!ml_import_tab, !ml_inductives, !ml_extract_tab)
 
 let unfreeze (ft,stk,et) =
-  Hashtabl.unfreeze ft ml_import_tab;
-  mL_INDUCTIVES := stk;
-  Hashtabl.unfreeze et ml_extract_tab
+  ml_import_tab := ft;
+  ml_inductives := stk;
+  ml_extract_tab := et
 
 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" >]
-
+    init_function     = (fun () -> ml_import_tab := Gmap.empty;
+      	       	       	       	   ml_inductives := [];
+				   ml_extract_tab := Gmap.empty);
+    survive_section = false }
 
 (**************************************************************************)
 (*                      ML Import file__name : type.                      *)
diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli
index ac32f5139f..6e302989fe 100644
--- a/contrib/extraction/mlimport.mli
+++ b/contrib/extraction/mlimport.mli
@@ -4,9 +4,11 @@
 open Names
 open Term
 
+val add_ml_import : global_reference -> identifier -> unit
 val is_ml_import : global_reference -> bool
 val find_ml_import : global_reference -> identifier
 
+val add_ml_extract : global_reference -> identifier -> unit
 val find_ml_extract : global_reference -> identifier
 val is_ml_extract : global_reference -> bool
 
@@ -16,14 +18,12 @@ 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