Extract Constant marche avec les axiomes schémas de types

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

5 files changed, 69 insertions, 57 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index ba925b40b5..05ad8f48fe 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -88,6 +88,15 @@ let rec type_sign env c =
 	(is_info_scheme env t)::(type_sign (push_rel_assum (n,t) env) d)
     | _ -> []
 
+let rec type_scheme_nb_args env c = 
+  match kind_of_term (whd_betadeltaiota env none c) with
+    | Prod (n,t,d) -> 
+	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in 
+	if is_info_scheme env t then n+1 else n
+    | _ -> 0
+
+let _ = ugly_hack_arity_nb_args := type_scheme_nb_args
+
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
 let rec type_sign_vl env c = 
@@ -105,7 +114,6 @@ let rec nb_default_params env c =
 	if is_default env t then n+1 else n
     | _ -> 0
 
-
 (*S Management of type variable contexts. *)
 
 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]  
@@ -742,10 +750,8 @@ let extract_constant env kn cb =
     | None -> (* A logical axiom is risky, an informative one is fatal. *) 
         (match flag_of_type env typ with
 	   | (Info,TypeScheme) -> 
-	       if isSort typ then 
-		 if is_custom (long_r r) then Dtype (r, [], Tunknown) 
-		 else error_axiom r
-	       else error_axiom_scheme r
+	       if is_custom (long_r r) then Dtype (r, [], Tunknown) 
+	       else error_axiom r
            | (Info,Default) -> 
 	       if is_custom (long_r r) then 
 		 let t = snd (record_constant_type env kn (Some typ)) in 
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
index 46021af732..ae79dda81e 100644
--- a/contrib/extraction/g_extraction.ml4
+++ b/contrib/extraction/g_extraction.ml4
@@ -82,13 +82,13 @@ END
 
 (* Overriding of a Coq object by an ML one *)
 VERNAC COMMAND EXTEND ExtractionConstant
-| [ "Extract" "Constant" global(x) "=>" mlname(y) ]
-  -> [ extract_constant_inline false x y ]
+| [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
+  -> [ extract_constant_inline false x idl y ]
 END
 
 VERNAC COMMAND EXTEND ExtractionInlinedConstant
 | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
-  -> [ extract_constant_inline true x y ]
+  -> [ extract_constant_inline true x [] y ]
 END
 
 VERNAC COMMAND EXTEND ExtractionInductive
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index d65a467102..5fb08d091c 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -391,6 +391,9 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 let pp_parameters l = 
   (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
 
+let pp_string_parameters l = 
+  (pp_boxed_tuple str l ++ space_if (l<>[])) 
+
 let pp_one_ind prefix ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =
@@ -485,9 +488,12 @@ let pp_decl mp =
 	if is_inline_custom r then failwith "empty phrase"
 	else 
 	  let l = rename_tvars keywords l in 
-	  let def = try str (find_custom r) with not_found -> pp_type false l t 
+	  let ids, def = try 
+	    let ids,s = find_type_custom r in 
+	    pp_string_parameters ids, str s 
+	  with not_found -> pp_parameters l, pp_type false l t
 	  in 
-	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ 
+	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ 
 		 spc () ++ str "=" ++ spc () ++ def)
     | Dterm (r, a, t) -> 
 	if is_inline_custom r then failwith "empty phrase"
@@ -519,15 +525,17 @@ let pp_spec mp =
 	if is_inline_custom r then failwith "empty phrase"
 	else 
 	  let l = rename_tvars keywords vl in 
-	  let def = 
-	    try str "= " ++ str (find_custom r) 
+	  let ids, def = 
+	    try 
+	      let ids, s = find_type_custom r in 
+	      pp_string_parameters ids,  str "= " ++ str s 
 	    with not_found -> 
+	      let ids = pp_parameters l in 
 	      match ot with 
-		| None -> mt () 
-		| Some t -> str "=" ++ spc () ++ pp_type false l t 
+		| None -> ids, mt () 
+		| Some t -> ids, str "=" ++ spc () ++ pp_type false l t 
 	  in 
-	  hov 2 (str "type" ++ spc () ++ pp_parameters l ++ 
-		 pp_global r ++ spc () ++ def)
+	  hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def)
 
 let rec pp_structure_elem mp = function 
   | (_,SEdecl d) -> pp_decl mp d
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 9f0b2cf73a..189bcbbf6e 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -189,9 +189,10 @@ let pr_global r = pr_id (id_of_global r)
 
 let err s = errorlabstrm "Extraction" s
 
-let error_axiom_scheme r = 
-  err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++
-       pr_global r ++ spc () ++ str ".") 
+let error_axiom_scheme r i = 
+  err (str "The type scheme axiom " ++ spc () ++
+       pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ 
+       str " type variable(s).") 
 
 let error_axiom r =
   err (str "You must specify an extraction for axiom" ++ spc () ++ 
@@ -381,30 +382,22 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extract Constant/Inductive. *)
 
-type kind = Term | Type | Ind | Construct 
+let ugly_hack_arity_nb_args = ref (fun _ _ -> 0) 
 
-let check_term_or_type r = match r with 
+let check_term_or_type r ids = match r with 
   | ConstRef sp -> 
       let env = Global.env () in 
       let typ = Environ.constant_type env sp in 
       let typ = Reduction.whd_betadeltaiota env typ in
-      if isSort typ then (r,Type) 
-      else if Reduction.is_arity env typ then error_type_scheme r
-      else (r,Term)
+      if Reduction.is_arity env typ 
+      then 
+	let nargs = !ugly_hack_arity_nb_args env typ in 
+	if List.length ids <> nargs then error_axiom_scheme r nargs
   | _ -> error_constant r
 	
 let customs = ref Refmap.empty
 
-let all_customs () = 
-  Refmap.fold (fun r _ -> Refset.add r) !customs Refset.empty
-
-let term_customs () = 
-  Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l) !customs []
-
-let type_customs () = 
-  Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) !customs []
-    
-let add_custom r k s = customs := Refmap.add r (k,s) !customs
+let add_custom r ids s = customs := Refmap.add r (ids,s) !customs
 
 let is_custom r = Refmap.mem (long_r r) !customs
 
@@ -413,13 +406,15 @@ let is_inline_custom r =
 
 let find_custom r = snd (Refmap.find (long_r r) !customs)
 
+let find_type_custom r = Refmap.find (long_r r) !customs
+
 (* Registration of operations for rollback. *)
 
 let (in_customs,_) = 
   declare_object 
     {(default_object "ML extractions") with 
-       cache_function = (fun (_,(r,k,s)) -> add_custom r k s);
-       load_function = (fun _ (_,(r,k,s)) -> add_custom r k s);
+       cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
+       load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
        export_function = (fun x -> Some x)}
 
 let _ = declare_summary "ML extractions"
@@ -430,26 +425,28 @@ let _ = declare_summary "ML extractions"
 
 (* Grammar entries. *)
 
-let extract_constant_inline inline r s =
+let extract_constant_inline inline r ids s =
   if is_something_opened () then error_section (); 
-  let g,k = check_term_or_type (Nametab.global r) in
+  let g = Nametab.global r in 
+  check_term_or_type g ids;
   Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
-  Lib.add_anonymous_leaf (in_customs (g,k,s))
+  Lib.add_anonymous_leaf (in_customs (g,ids,s))
 
 let extract_inductive r (s,l) =
   if is_something_opened () then error_section (); 
-  let g = Nametab.global r in match g with
-  | IndRef ((kn,i) as ip) ->
-      let mib = Global.lookup_mind kn in
-      let n = Array.length mib.mind_packets.(i).mind_consnames in
-      if n <> List.length l then error_nb_cons (); 
-      Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-      Lib.add_anonymous_leaf (in_customs (g,Ind,s));
-      list_iter_i
-	(fun j s -> 
-	   let g = ConstructRef (ip,succ j) in 
-	   Lib.add_anonymous_leaf (inline_extraction (true,[g]));
-	   Lib.add_anonymous_leaf (in_customs (g,Construct,s))) l
-  | _ -> error_inductive g 
+  let g = Nametab.global r in 
+  match g with
+    | IndRef ((kn,i) as ip) ->
+	let mib = Global.lookup_mind kn in
+	let n = Array.length mib.mind_packets.(i).mind_consnames in
+	if n <> List.length l then error_nb_cons (); 
+	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+	Lib.add_anonymous_leaf (in_customs (g,[],s));
+	list_iter_i
+	  (fun j s -> 
+	     let g = ConstructRef (ip,succ j) in 
+	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
+	     Lib.add_anonymous_leaf (in_customs (g,[],s))) l
+    | _ -> error_inductive g 
 
 
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index e4169a9bfe..3fbdbc209d 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -16,7 +16,7 @@ val id_of_global : global_reference -> identifier
 
 (*s Warning and Error messages. *)
 
-val error_axiom_scheme : global_reference -> 'a
+val error_axiom_scheme : global_reference -> int -> 'a
 val error_axiom : global_reference -> 'a
 val warning_axiom : global_reference -> unit
 val error_section : unit -> 'a
@@ -94,12 +94,12 @@ val to_keep : global_reference -> bool
 
 (*s Table for user-given custom ML extractions. *)
 
+val ugly_hack_arity_nb_args : (Environ.env -> Term.constr -> int) ref
+
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
 val find_custom : global_reference -> string
-val all_customs : unit -> Refset.t
-val type_customs : unit -> (global_reference * string) list
-val term_customs : unit -> (global_reference * string) list
+val find_type_custom : global_reference -> string list * string
 
 (*s Extraction commands. *)
 
@@ -107,7 +107,8 @@ val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
 val print_extraction_inline : unit -> unit
 val reset_extraction_inline : unit -> unit
-val extract_constant_inline : bool -> reference -> string -> unit
+val extract_constant_inline : 
+  bool -> reference -> string list -> string -> unit
 val extract_inductive : reference -> string * string list -> unit