commandes Extract Constant/Inductive; message d'erreur pour les axiomes

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

7 files changed, 238 insertions, 126 deletions

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index 1f71ef2f2..a5e7c81af 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -16,5 +16,24 @@ Grammar vernac vernac : ast :=
 | extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
               [ (ExtractionFile $f ($LIST $l)) ]
 | extr_module [ "Extraction" "Module" identarg($m) "." ] ->
-              [ (ExtractionModule $m) ].
+              [ (ExtractionModule $m) ]
 
+| extract_constant 
+     [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ]
+  -> [ (EXTRACT_CONSTANT $x $y) ]
+
+| extract_inductive 
+     [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."]
+  -> [ (EXTRACT_INDUCTIVE $x $y) ]
+
+with mindnames : ast :=
+  mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ]
+        -> [(VERNACARGLIST $id ($LIST $idl))]
+
+with idorstring_list: List :=
+  ids_nil  [ ] -> [ ]
+| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ]
+
+with idorstring : ast :=
+  ids_ident  [ identarg($id) ] -> [ $id ]
+| ids_string [ stringarg($s) ] -> [ $s ].
diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO
index 3bef00804..58f655b48 100644
--- a/contrib/extraction/TODO
+++ b/contrib/extraction/TODO
@@ -3,3 +3,8 @@
 
  3. Axiomes
 
+ 4. Cofix : seulement en Haskell
+
+ 5. Syntaxe Haskell
+
+ 6. Reset sur les commandes Extract Constant/Inductive
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 45f76a311..7eddb932c 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -1,130 +1,90 @@
 
 open Pp
+open Util
 open Term
 open Lib
 open Extraction
 open Miniml
 open Mlutil
 
-(*s Topological sort of global CIC references. 
-    We introduce graphs of global references; a graph is a map
-    from edges to the set of their immediate successors. *)
-
-module Refmap = 
-  Map.Make(struct type t = global_reference let compare = compare end)
-
-module Refset = 
-  Set.Make(struct type t = global_reference let compare = compare end)
-
-type graph = Refset.t Refmap.t
-
-let empty = Refmap.empty
-
-let add_arc x y g =
-  let s = try Refmap.find x g with Not_found -> Refset.empty in
-  let g' = Refmap.add x (Refset.add y s) g in
-  if not (Refmap.mem y g') then Refmap.add y Refset.empty g' else g'
-
-exception Found of global_reference
-
-let maximum g =
-  try 
-    Refmap.iter (fun x s -> if s = Refset.empty then raise (Found x)) g;
-    assert false
-  with Found m -> 
-    m
-
-let remove m g =
-  let g' = 
-    Refmap.fold (fun x s -> Refmap.add x (Refset.remove m s)) g Refmap.empty
-  in
-  Refmap.remove m g'
-
-let sorted g =
-  let rec sorted_aux acc g =
-    if g = Refmap.empty then
-      acc
-    else
-      let max = maximum g in
-      sorted_aux (max :: acc) (remove max g)
+(*s Recursive computation of the global references to extract. 
+    We use a set of functions visiting the extracted objects in
+    a depth-first way ([visit_type], [visit_ast] and [visit_decl]).
+    We maintain an (imperative) structure [extracted_env] containing
+    the set of already visited references and the list of 
+    references to extract. The entry point is the function [visit_reference]:
+    it first normalizes the reference, and then check it has already been 
+    visisted; if not, it adds it to the set of visited references, then
+    recursively traverses its extraction and finally adds it to the 
+    list of references to extract. *) 
+
+type extracted_env = {
+  mutable visited : Refset.t;
+  mutable to_extract : global_reference list 
+}
+
+let empty () = { visited = ml_extractions (); to_extract = [] }
+
+let rec visit_reference eenv r =
+  let r' = match r with
+    | ConstructRef ((sp,_),_) -> IndRef (sp,0)
+    | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0)
+    | _ -> r
   in
-  sorted_aux [] g
-
-(*s Computation of the global references appearing in an AST of a 
-    declaration. *)
-
-let globals_of_type t =
-  let rec collect s = function
-    | Tglob r -> Refset.add r s
-    | Tapp l -> List.fold_left collect s l
-    | Tarr (t1,t2) -> collect (collect s t1) t2
-    | Tvar _ | Tprop | Tarity -> s
+  if not (Refset.mem r' eenv.visited) then begin
+    (* we put [r'] in [visited] first to avoid loops in inductive defs *)
+    eenv.visited <- Refset.add r' eenv.visited;
+    visit_decl eenv (extract_declaration r);
+    eenv.to_extract <- r' :: eenv.to_extract
+  end
+
+and visit_type eenv t =
+  let rec visit = function
+    | Tglob r -> visit_reference eenv r
+    | Tapp l -> List.iter visit l
+    | Tarr (t1,t2) -> visit t1; visit t2
+    | Tvar _ | Tprop | Tarity -> ()
   in
-  collect Refset.empty t
-
-let globals_of_ast a =
-  let rec collect s = function
-    | MLglob r -> Refset.add r s
-    | MLapp (a,l) -> List.fold_left collect (collect s a) l
-    | MLlam (_,a) -> collect s a
-    | MLletin (_,a,b) -> collect (collect s a) b
-    | MLcons (r,_,l) -> List.fold_left collect (Refset.add r s) l
+  visit t
+
+and visit_ast eenv a =
+  let rec visit = function
+    | MLglob r -> visit_reference eenv r
+    | MLapp (a,l) -> visit a; List.iter visit l
+    | MLlam (_,a) -> visit a
+    | MLletin (_,a,b) -> visit a; visit b
+    | MLcons (r,_,l) -> visit_reference eenv r; List.iter visit l
     | MLcase (a,br) -> 
-	Array.fold_left 
-	  (fun s (r,_,a) -> collect (Refset.add r s) a) (collect s a) br
-    | MLfix (_,_,l) -> List.fold_left collect s l
-    | MLcast (a,t) -> Refset.union (collect s a) (globals_of_type t)
-    | MLmagic a -> collect s a
-    | MLrel _ | MLprop | MLarity | MLexn _ -> s
+	visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br
+    | MLfix (_,_,l) -> List.iter visit l
+    | MLcast (a,t) -> visit a; visit_type eenv t
+    | MLmagic a -> visit a
+    | MLrel _ | MLprop | MLarity | MLexn _ -> ()
   in
-  collect Refset.empty a
+  visit a
 
-let globals_of_inductive inds =
-  let globals_of_constructor ie (r,tl) =
-    List.fold_left 
-      (fun (i,e) t -> Refset.add r i, Refset.union (globals_of_type t) e) ie tl
-  in
-  let globals_of_ind (i,e) (_,r,cl) = 
-    List.fold_left globals_of_constructor (Refset.add r i, e) cl
-  in
-  let (i,e) = List.fold_left globals_of_ind (Refset.empty,Refset.empty) inds in
-  Refset.diff e i
+and visit_inductive eenv inds =
+  let visit_constructor (_,tl) = List.iter (visit_type eenv) tl in
+  let visit_ind (_,_,cl) = List.iter visit_constructor cl in
+  List.iter visit_ind inds
 
-let globals_of_decl = function
+and visit_decl eenv = function
   | Dtype inds ->
-      globals_of_inductive inds
-  | Dabbrev (r,_,t) ->
-      Refset.remove r (globals_of_type t)
-  | Dglob (r,a) ->
-      Refset.remove r (globals_of_ast a)
-
-(*s Recursive extraction of a piece of environment. *)
+      visit_inductive eenv inds
+  | Dabbrev (_,_,t) ->
+      visit_type eenv t
+  | Dglob (_,a) ->
+      visit_ast eenv a
 
-let add_dependency r r' g = 
-  let normalize = function
-    | ConstructRef ((sp,_),_) -> IndRef (sp,0)
-    | IndRef (sp,i) as r -> if i = 0 then r else IndRef (sp,0)
-    | r -> r
-  in
-  add_arc (normalize r') (normalize r) g
+(*s Recursive extracted environment for a list of reference: we just
+    iterate [visit_reference] on the list, starting with an empty
+    extracted environment, and we return the reversed list of 
+    references in the field [to_extract]. *)
 
 let extract_env rl =
-  let rec extract graph seen todo = 
-    if Refset.equal todo Refset.empty then
-      sorted graph
-    else 
-      let r = Refset.choose todo in
-      let todo' = Refset.remove r todo in
-      if Refset.mem r seen then
-	extract graph seen todo'
-      else
-	let d = extract_declaration r in
-	let deps = globals_of_decl d in
-	let graph' = Refset.fold (add_dependency r) deps graph in
-	extract graph' (Refset.add r seen) (Refset.union todo' deps)
-  in
-  extract empty Refset.empty (List.fold_right Refset.add rl Refset.empty)
-
+  let eenv = empty () in
+  List.iter (visit_reference eenv) rl;
+  List.rev eenv.to_extract
 
 (*s Registration of vernac commands for extraction. *)
 
@@ -139,7 +99,7 @@ module Pp = Ocaml.Make(ToplevelParams)
 open Vernacinterp
 
 let _ = 
-  overwriting_vinterp_add "Extraction"
+  vinterp_add "Extraction"
     (function 
        | [VARG_CONSTR ast] ->
 	   (fun () -> 
@@ -160,8 +120,13 @@ let _ =
 		      | Eprop -> message "prop")
        | _ -> assert false)
 
+let no_such_reference q =
+  errorlabstrm "reference_of_varg" 
+    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
+
 let reference_of_varg = function
-  | VARG_QUALID q -> Nametab.locate q
+  | VARG_QUALID q -> 
+      (try Nametab.locate q with Not_found -> no_such_reference q)
   | _ -> assert false
 
 let decl_of_vargl vl =
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 85a448057..2788fa811 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -250,6 +250,12 @@ let decompose_lam_eta n env c =
 let rec abstract_n n a = 
   if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a))
 
+(*s Error message when extraction ends on an axiom. *)
+
+let axiom_message sp =
+  errorlabstrm "axiom_message"
+    [< 'sTR "You must specify an extraction for axiom"; 'sPC; 
+       pr_sp sp; 'sPC; 'sTR "first" >]
 
 
 (*s Tables to keep the extraction of inductive types and constructors. *)
@@ -602,10 +608,12 @@ and extract_constant sp =
   try
     Gmap.find sp !constant_table
   with Not_found ->
-    (* TODO: Axioms *)
     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
+    let body = match cb.const_body with 
+      | Some c -> c 
+      | None -> axiom_message sp
+    in
     let e = extract_constr_with_type (Global.env()) [] body typ in
     constant_table := Gmap.add sp e !constant_table;
     e
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 7f5b23901..8bc026dae 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1,4 +1,8 @@
 
+open Pp
+open Names
+open Term
+open Declarations
 open Util
 open Miniml
 
@@ -177,3 +181,92 @@ let uncurrify_decl = function
  | Dglob (id, a) -> Dglob (id, uncurrify_ast a)
  | d -> d
 
+(*s Table for direct ML extractions. *)
+
+module Refset = 
+  Set.Make(struct type t = global_reference let compare = compare end)
+
+module Refmap = 
+  Map.Make(struct type t = global_reference let compare = compare end)
+
+let extractions = ref (Refmap.empty, Refset.empty)
+
+let ml_extractions () = snd !extractions
+
+let add_ml_extraction r s = 
+  let (map,set) = !extractions in
+  extractions := (Refmap.add r s map, Refset.add r set)
+
+let is_ml_extraction r = Refset.mem r (snd !extractions)
+
+let find_ml_extraction r = Refmap.find r (fst !extractions)
+
+(*s Registration for rollback. *)
+
+open Summary
+
+let _ = declare_summary "ML extractions"
+	  { freeze_function = (fun () -> !extractions);
+	    unfreeze_function = ((:=) extractions);
+	    init_function = 
+	      (fun () -> extractions := (Refmap.empty, Refset.empty));
+	    survive_section = true }
+
+(*s Grammar entries. *)
+
+open Vernacinterp
+
+let string_of_varg = function
+  | VARG_IDENTIFIER id -> string_of_id id
+  | VARG_STRING s -> s
+  | _ -> assert false
+
+let no_such_reference q =
+  errorlabstrm "reference_of_varg" 
+    [< Nametab.pr_qualid q; 'sTR ": no such reference" >]
+
+let reference_of_varg = function
+  | VARG_QUALID q -> 
+      (try Nametab.locate q with Not_found -> no_such_reference q)
+  | _ -> assert false
+
+(*s \verb!Extract Constant qualid => string! *)
+
+let extract_constant r s = match r with
+  | ConstRef _ -> 
+      add_ml_extraction r s
+  | _ -> 
+      errorlabstrm "extract_constant"
+	[< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >]
+
+let _ = 
+  vinterp_add "EXTRACT_CONSTANT"
+    (function 
+       | [id; s] -> 
+	   (fun () -> 
+	      extract_constant (reference_of_varg id) (string_of_varg s))
+       | _ -> assert false)
+
+(*s \verb!Extract Inductive qualid => string [ string ... string ]! *)
+
+let extract_inductive r (id2,l2) = match r with
+  | IndRef ((sp,i) as ip) ->
+      add_ml_extraction r id2;
+      let mib = Global.lookup_mind sp in
+      let n = Array.length mib.mind_packets.(i).mind_consnames in
+      if n <> List.length l2 then
+	error "not the right number of constructors";
+      list_iter_i
+	(fun j s -> add_ml_extraction (ConstructRef (ip,succ j)) s) l2
+  | _ -> 
+      errorlabstrm "extract_inductive"
+	[< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >]
+
+let _ = 
+  vinterp_add "EXTRACT_INDUCTIVE"
+    (function 
+       | [q1; VARG_VARGLIST (id2 :: l2)] ->
+	   (fun () -> 
+	      extract_inductive (reference_of_varg q1) 
+		(string_of_varg id2, List.map string_of_varg l2))
+       | _ -> assert false)
diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli
index b60a3fdf9..7b7a20dd2 100644
--- a/contrib/extraction/mlutil.mli
+++ b/contrib/extraction/mlutil.mli
@@ -1,8 +1,15 @@
 
+open Names
+open Term
 open Miniml
 
-val anonymous : Names.identifier
-val prop_name : Names.identifier
+(*s Special identifiers. [prop_name] is to be used for propositions
+    and will be printed as [_] in concrete (Caml) code. *)
+
+val anonymous : identifier
+val prop_name : identifier
+
+(*s Utility functions over ML terms. *)
 
 val occurs : int -> ml_ast -> bool
 
@@ -16,3 +23,11 @@ val betared_decl : ml_decl -> ml_decl
 
 val uncurrify_ast : ml_ast -> ml_ast
 val uncurrify_decl : ml_decl -> ml_decl
+
+(*s Table for the extraction to ML values. *)
+
+module Refset : Set.S with type elt = global_reference
+
+val find_ml_extraction : global_reference -> string
+
+val ml_extractions : unit -> Refset.t
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1037772e2..6c073d42e 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -125,6 +125,13 @@ let pr_binding = function
 
 module Make = functor(P : Mlpp_param) -> struct
 
+let pp_reference f r = 
+  try let s = find_ml_extraction r in [< 'sTR s >]
+  with Not_found -> f r
+ 
+let pp_type_global = pp_reference P.pp_type_global
+let pp_global = pp_reference P.pp_global
+
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
@@ -143,7 +150,7 @@ let rec pp_type par t =
 	[< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; 
 	   pp_rec false t2; close_par par >]
     | Tglob r -> 
-	P.pp_type_global r
+	pp_type_global r
     | Tprop ->
 	string "prop"
     | Tarity ->
@@ -184,14 +191,14 @@ let rec pp_expr par env args =
 		 'sPC;
 		 pp_expr false env' [] a2 >] 
     | MLglob r -> 
-	apply (P.pp_global r)
+	apply (pp_global r)
     | MLcons (r,_,[]) ->
-	P.pp_global r
+	pp_global r
     | MLcons (r,_,[a]) ->
-	[< open_par par; P.pp_global r; 'sPC;
+	[< open_par par; pp_global r; 'sPC;
 	   pp_expr true env [] a; close_par par >]
     | MLcons (r,_,args') ->
-	[< open_par par; P.pp_global r; 'sPC;
+	[< open_par par; pp_global r; 'sPC;
 	   pp_tuple (pp_expr true env []) args'; close_par par >]
     | MLcase (t, pv) ->
       	apply
@@ -224,7 +231,7 @@ and pp_pat env pv =
       | MLcase _ -> true
       | _        -> false 
     in
-    hOV 2 [< P.pp_global name;
+    hOV 2 [< pp_global name;
 	     begin match ids with 
 	       | [] -> [< >]
 	       | _  -> [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >]
@@ -292,7 +299,7 @@ let pp_parameters l =
 
 let pp_one_inductive (pl,name,cl) =
   let pp_constructor (id,l) =
-    [< P.pp_global id;
+    [< pp_global id;
        match l with
          | [] -> [< >] 
 	 | _  -> [< 'sTR " of " ;
@@ -300,7 +307,7 @@ let pp_one_inductive (pl,name,cl) =
 		      (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >]
     >]
   in
-    [< pp_parameters pl; P.pp_global name; 'sTR " ="; 
+    [< pp_parameters pl; pp_global name; 'sTR " ="; 
        if cl = [] then
 	 [< 'sTR " unit (* empty inductive *)" >]
        else
@@ -326,7 +333,7 @@ let pp_decl = function
       hOV 0 (pp_inductive i)
   | Dabbrev (r, l, t) ->
       hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; 
-	       P.pp_type_global r; 'sPC; 'sTR "="; 'sPC; 
+	       pp_type_global r; 'sPC; 'sTR "="; 'sPC; 
 	       pp_type false  t; 'fNL >]
   | Dglob (r, MLfix (_,[_],[def])) ->
       let id = P.rename_global r in
@@ -334,7 +341,7 @@ let pp_decl = function
       [<  hOV 2 (pp_fix false env' None ([id],[def]) []) >]
   | Dglob (r, a) ->
       hOV 0 [< 'sTR "let "; 
-	       pp_function (empty_env ()) (P.pp_global r) a; 'fNL >]
+	       pp_function (empty_env ()) (pp_global r) a; 'fNL >]
 
 let pp_type = pp_type false
 let pp_ast a = pp_ast (betared_ast (uncurrify_ast a))