cas des constructeurs singletons. Messages d'erreur. Revision de test_extraction.v

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

9 files changed, 186 insertions, 56 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 130868591..20c558c50 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -225,6 +225,9 @@ let pp_comment s = match lang () with
 let pp_logical_ind r = 
   pp_comment (Printer.pr_global r ++ str " : logical inductive")
 
+let pp_singleton_ind r = 
+  pp_comment (Printer.pr_global r ++ str " : singleton inductive constructor")
+
 (*s Extraction to a file. *)
 
 let extract_to_file f prm decls =
@@ -255,7 +258,10 @@ let extract_to_file f prm decls =
   let ft = Pp_control.with_output_to cout in
   if not prm.modular then 
     List.iter (fun r -> pp_with ft (pp_logical_ind r)) 
-      (List.filter declaration_is_logical_ind prm.to_appear); 
+      (List.filter decl_is_logical_ind prm.to_appear); 
+  if not prm.modular then 
+    List.iter (fun r -> pp_with ft (pp_singleton_ind r)) 
+      (List.filter decl_is_singleton prm.to_appear); 
   pp_with ft (preamble prm used_modules (decl_print_prop decls));
   begin 
     try
@@ -267,7 +273,7 @@ let extract_to_file f prm decls =
   if f <> None then close_out cout;  
 
 (*i 
-  (* names resolution *)
+  (* DO NOT REMOVE: used when making names resolution *)
   let cout = open_out (f^".ren") in 
   let ft = Pp_control.with_output_to cout in
   Hashtbl.iter 
diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli
index 6835d2e97..12424612c 100644
--- a/contrib/extraction/common.mli
+++ b/contrib/extraction/common.mli
@@ -24,6 +24,9 @@ val short_module : global_reference -> identifier
 
 val pp_logical_ind : global_reference -> std_ppcmds
 
+val pp_singleton_ind : global_reference -> std_ppcmds
+
 val extract_to_file : 
   string option -> extraction_params -> ml_decl list -> unit
 
+
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 9838a79f0..78d89b669 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -224,8 +224,10 @@ let extract_reference r =
   if is_ml_extraction r then
     print_user_extract r 
   else
-    if declaration_is_logical_ind r then 
+    if decl_is_logical_ind r then 
       msgnl (pp_logical_ind r) 
+    else if decl_is_singleton r then 
+      msgnl (pp_singleton_ind r) 
     else
       let prm = 
 	{ modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in
@@ -249,8 +251,8 @@ let _ =
 		(* Otherwise, output the ML type or expression *)
 		| _ ->
 		    match extract_constr (Global.env()) c with
-		      | Emltype (t,_,_) -> msgnl (pp_type t)
-		      | Emlterm a -> msgnl (pp_ast (normalize a)))
+		      | Emltype (t,_,_) -> msgnl (pp_type t ++ fnl ())
+		      | Emlterm a -> msgnl (pp_ast (normalize a) ++ fnl ()))
        | _ -> assert false)
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index a52000341..58bcd927e 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -289,11 +289,11 @@ let eta_expanse_w_prop e s =
 let axiom_message sp =
   errorlabstrm "axiom_message"
     (str "You must specify an extraction for axiom" ++ spc () ++ 
-       pr_sp sp ++ spc () ++ str "first")
+       pr_sp sp ++ spc () ++ str "first.")
 
 let section_message () = 
   errorlabstrm "section_message"
-    (str "You can't extract within a section. Close it and try again")
+    (str "You can't extract within a section. Close it and try again.")
 
 (*s Tables to keep the extraction of inductive types and constructors. *)
 
@@ -995,9 +995,16 @@ let extract_declaration r = match r with
   | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp
   | VarRef _ -> assert false
 
-(*s Check whether a global reference corresponds to a logical inductive. *)
+(*s Check if a global reference corresponds to a logical inductive. *)
 
-let declaration_is_logical_ind = function 
+let decl_is_logical_ind = function 
   | IndRef ip -> extract_inductive ip = Iprop 
   | ConstructRef cp -> extract_constructor cp  = Cprop
   | _ -> false
+
+(*s Check if a global reference corresponds to the constructor of 
+  a singleton inductive. *)
+
+let decl_is_singleton = function 
+  | ConstructRef cp -> is_singleton_constructor cp 
+  | _ -> false 
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index 87f97641c..e3a747ce0 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -40,4 +40,9 @@ val extract_declaration : global_reference -> ml_decl
 
 (*s Check whether a global reference corresponds to a logical inductive. *)
 
-val declaration_is_logical_ind : global_reference -> bool
+val decl_is_logical_ind : global_reference -> bool
+
+(*s Check if a global reference corresponds to the constructor of 
+  a singleton inductive. *)
+
+val decl_is_singleton : global_reference -> bool
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 52798cb58..d9286f441 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -319,7 +319,6 @@ let rec permut_case_fun br acc =
   done; 
   (ids,br)
   
-  
 (*s Generalized iota-reduction. *)
 
 (* Definition of a generalized iota-redex: it's a [MLcase(e,_)] 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index b385bd619..57a198d13 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -369,7 +369,6 @@ let pp_coind il =
    fnl () ++ str "and " ++ 
    prlist_with_sep (fun () -> (fnl () ++ str "and ")) (pp_one_ind "__") il ++
    fnl ())
- 
 
 (*s Pretty-printing of a declaration. *)
 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 0cafb9460..21e74334d 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -64,7 +64,7 @@ let is_constant r = match r with
 let check_constant r = 
   if (is_constant r) then r 
   else errorlabstrm "extract_constant"
-	(Printer.pr_global r ++ spc () ++ str "is not a constant") 
+	(Printer.pr_global r ++ spc () ++ str "is not a constant.") 
 
 let string_of_varg = function
   | VARG_IDENTIFIER id -> string_of_id id
@@ -73,7 +73,7 @@ let string_of_varg = function
 
 let no_such_reference q =
   errorlabstrm "reference_of_varg" 
-    (Nametab.pr_qualid q ++ str ": no such reference")
+    (str "There is no such reference " ++ Nametab.pr_qualid q ++ str ".")
 
 let reference_of_varg = function
   | VARG_QUALID q -> 
@@ -262,7 +262,7 @@ let extract_inductive r (id2,l2) = match r with
       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";
+	error "Not the right number of constructors.";
       add_anonymous_leaf (in_ml_extraction (r,id2));
       list_iter_i
 	(fun j s -> 
@@ -271,7 +271,7 @@ let extract_inductive r (id2,l2) = match r with
 	   add_anonymous_leaf (in_ml_extraction (r,s))) l2
   | _ -> 
       errorlabstrm "extract_inductive"
-	(Printer.pr_global r ++ spc () ++ str "is not an inductive type")
+	(Printer.pr_global r ++ spc () ++ str "is not an inductive type.")
 
 let _ = 
   vinterp_add "ExtractInductive"
diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v
index d59a149e5..a2a17d20b 100644
--- a/contrib/extraction/test_extraction.v
+++ b/contrib/extraction/test_extraction.v
@@ -7,50 +7,62 @@
 (***********************************************************************)
 
 Extraction nat.
+(* type nat = 
+    O 
+  | S of nat 
+*)
 
 Extraction [x:nat]x.
+(* fun x -> x *)
 
 Inductive c [x:nat] : nat -> Set :=
     refl : (c x x)                  
   | trans : (y,z:nat)(c x y)->(le y z)->(c x z).
 Extraction c.
+(* type c =
+    Refl
+  | Trans of nat * nat * c
+*)
 
 Extraction [f:nat->nat][x:nat](f x).
+(* fun f x -> f x *)
 
 Extraction [f:nat->Set->nat][x:nat](f x nat).
+(* fun f x -> f x *)
 
 Extraction [f:(nat->nat)->nat][x:nat][g:nat->nat](f g).
+(* fun f x g -> f g *)
 
-Extraction (pair nat nat (S O) O).
+Extraction (pair ? ? (S O) O).
+(* Pair ((S O), O) *)
 
 Definition cf :=  [x:nat][_:(le x O)](S x).
 Extraction (cf O (le_n O)).  
+(* cf O *)
 
 Extraction ([X:Set][x:X]x nat).
+(* fun x -> x *)
 
 Definition d := [X:Type]X.
+Extraction d. (* type 'x d = 'x *)
+Extraction (d Set). (* arity d *)
+Extraction [x:(d Set)]O. (* O *)
+Extraction (d nat). (* nat d *)
 
-Extraction d.
-Extraction (d Set).
-Extraction [x:(d Set)]O.
-Extraction (d nat).
+Extraction ([x:(d Type)]O Type).  (* O *)
 
-Extraction ([x:(d Type)]O Type). 
+Extraction ([x:(d Type)]x).  (* 'x *)
 
-Extraction ([x:(d Type)]x). 
-
-Extraction ([X:Type][x:X]x Set nat).
+Extraction ([X:Type][x:X]x Set nat). (* nat *)
 
 Definition id' := [X:Type][x:X]x.      
-Extraction id'.
-Extraction (id' Set nat).
+Extraction id'. (* let id' x = x *)
+Extraction (id' Set nat). (* nat *)
 
-Extraction let t = nat in (id' Set t). 
+Extraction let t = nat in (id' Set t).  (* nat *)
 
 Definition Ensemble := [U:Type]U->Prop.
-
 Definition Empty_set := [U:Type][x:U]False.
-
 Definition Add := [U:Type][A:(Ensemble U)][x:U][y:U](A y) \/ x==y.
 
 Inductive Finite [U:Type] : (Ensemble U) -> Set :=
@@ -59,12 +71,18 @@ Inductive Finite [U:Type] : (Ensemble U) -> Set :=
       (A: (Ensemble U)) (Finite U A) -> 
       (x: U) ~ (A x) -> (Finite U (Add U A x)).
 Extraction Finite.
+(* type 'u finite =
+    Empty_is_finite
+  | Union_is_finite of 'u finite * 'u
+*)
 
-Extraction ([X:Type][x:X]O Type Type).
+Extraction ([X:Type][x:X]O Type Type). (* O *)
 
-Extraction let n=O in let p=(S n) in (S p).
+Extraction let n=O in let p=(S n) in (S p). (* S (S O) *)
 
-Extraction (x:(X:Type)X->X)(x Type Type).
+Extraction (x:(X:Type)X->X)(x Type Type). (* ('X -> 'X) -> 'x *)
+
+(** Mutual Inductive *)
 
 Inductive tree : Set := 
    Node : nat -> forest -> tree
@@ -73,6 +91,12 @@ with forest : Set :=
  | Cons : tree -> forest -> forest .
 
 Extraction tree.
+(* type tree =
+    Node of nat * forest
+and forest =
+    Leaf of nat
+  | Cons of tree * forest
+*)
 
 Fixpoint tree_size [t:tree] : nat :=
          Cases t of (Node a f) => (S (forest_size f)) end
@@ -83,78 +107,151 @@ with forest_size [f:forest] : nat :=
          end.
 
 Extraction tree_size.
+(* let tree_size x =
+  let rec tree_size0 = function
+    Node (a, f) -> S (forest_size f)
+  and forest_size = function
+    Leaf b -> S O
+  | Cons (t, f') -> plus (tree_size0 t) (forest_size f')
+  in tree_size0 x 
+*)
 
 Extraction Cases (left True True I) of (left x)=>(S O) | (right x)=>O end.
+(* S O *)
 
-Extraction sumbool_rec.
-
-Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O.
-
-Extraction horibilis.
+Extraction sumbool_rect.
+(* let sumbool_rect f0 f = function
+  Left -> f0 prop
+| Right -> f prop
+*)
 
 Inductive predicate : Type := 
   | Atom : Prop -> predicate
   | EAnd  : predicate -> predicate -> predicate.
-
 Extraction predicate.
+(* type predicate =
+    Atom
+  | EAnd of predicate * predicate
+*)
+
+(** Eta-expansions of inductive constructor *)
 
-(* eta-expansions *)
 Inductive titi : Set := tata : nat->nat->nat->nat->titi.
 Extraction (tata O).
+(* fun x1 x0 x -> Tata (O, x1, x0, x) *)
 Extraction (tata O (S O)).
+(* fun x0 x -> Tata (O, (S O), x0, x) *)
 
 Inductive eta : Set := eta_c : nat->Prop->nat->Prop->eta.
 Extraction eta_c.
+(* type eta =
+    Eta_c of nat * nat
+*)
 Extraction (eta_c O).
+(* fun x -> Eta_c (O, x) *)
 Extraction (eta_c O True).
+(* fun x -> Eta_c (O, x) *)
 Extraction (eta_c O True O).
+(* Eta_c (O, O) *)
+
+
+(** Example of singleton inductive type *)
 
 Inductive bidon [A:Prop;B:Type] : Set := tb : (x:A)(y:B)(bidon A B). 
 Definition fbidon := [A,B:Type][f:A->B->(bidon True nat)][x:A][y:B](f x y).
-
 Extraction bidon.
+(* type 'b bidon = 'b *)
+Extraction tb.
+(* tb : singleton inductive constructor *)
 Extraction fbidon.
+(* let fbidon f x y =
+  f x y
+*)
 Extraction (fbidon True nat (tb True nat)).
+(* fun x0 x -> fbidon (fun _ x1 -> x1) x0 x *)
+Definition fbidon2 := (fbidon True nat (tb True nat)).
+Extraction fbidon2. 
+(* let fbidon2 x =
+  x 
+*)
+(** NB: first argument of fbidon2 has type [True], so it disappears. *)
+
+(** mutual inductive on many sorts *)
 
-(* mutual inductive on many sorts *)
 Inductive 
   test0 : Prop := ctest0 : test0 
 with 
   test1 : Set := ctest1 : test0-> test1.  
 Extraction test0.
+(* test0 : logical inductive *)
+Extraction test1. 
+(* type test1 =
+    Ctest1
+*)
+
+(** logical singleton *)
 
 Extraction eq.
-Extraction eq_rec.
+(* eq : logical inductive *)
+Extraction eq_rect.
+(* let eq_rect x f y =
+  f
+*)
 
-(* example with more arguments that given by the type *)
+(** example with more arguments that given by the type *)
 
 Extraction (nat_rec [n:nat]nat->nat [n:nat]O [n:nat][f:nat->nat]f O O).
+(* nat_rec (fun n -> O) (fun n f -> f) O O *)
+
 
-(* propagation of type parameters *)
+(** propagation of type parameters *)
 
 Inductive tp1 : Set := 
   T : (C:Set)(c:C)tp2 -> tp1 with tp2 : Set  := T' : tp1->tp2.
+Extraction tp1.
+(* type 'c tp1 =
+    T of 'c * 'c tp2
+and 'c tp2 =
+    T' of 'c tp1
+*) 
 
 Inductive tp1bis : Set := 
   Tbis : tp2bis -> tp1bis 
 with tp2bis : Set  := T'bis : (C:Set)(c:C)tp1bis->tp2bis.
+Extraction tp1bis.
+(* type 'c tp1bis =
+    Tbis of 'c tp2bis
+and 'c tp2bis =
+    T'bis of 'c * 'c tp1bis
+*)
 
-(* casts *)
+(** casts *)
 
 Extraction (True :: Type).
+(* arity *)
 
-(* example needing Obj.magic *)
-
+(* examples needing Obj.magic *)
 (* hybrids *)
 
+Definition horibilis := [b:bool]<[b:bool]if b then Type else nat>if b then Set else O.
+Extraction horibilis.
+(* let horibilis = function
+  True -> arity
+| False -> O
+*)
+
 Definition PropSet := [b:bool]if b then Prop else Set.
-Extraction PropSet.
+Extraction PropSet. (* type 'flex propSet = 'flex *)
 
 Definition natbool := [b:bool]if b then nat else bool.
-Extraction natbool.
+Extraction natbool. (* type 'flex natbool = 'flex *)
 
 Definition zerotrue := [b:bool]<natbool>if b then O else true.
-Extraction zerotrue.
+Extraction zerotrue. 
+(* let zerotrue = function
+  True -> O
+| False -> True
+*)
 
 Definition natProp := [b:bool]<[_:bool]Type>if b then nat else Prop.
 
@@ -162,26 +259,38 @@ Definition natTrue := [b:bool]<[_:bool]Type>if b then nat else True.
 
 Definition zeroTrue := [b:bool]<natProp>if b then O else True.
 Extraction zeroTrue.
+(* let zeroTrue = function
+  True -> O
+| False -> arity
+*)
 
 Definition natTrue2 := [b:bool]<[_:bool]Type>if b then nat else True.
 
 Definition zeroprop := [b:bool]<natTrue>if b then O else I.
 Extraction zeroprop.
+(* let zeroprop = function
+  True -> O
+| False -> prop
+*)
 
-(* instanciations Type -> Prop *)
+(** instanciations Type -> Prop *)
 
-(* polymorphic f applied several times *)
+(** polymorphic f applied several times *)
 
 Extraction (pair ? ? (id' nat O) (id' bool true)).
+(* Pair ((id' O), (id' True)) *)
 
-(* ok *)
+(** ok *)
 
 Extraction 
-([id':(X:Type)X->X](pair ? ? (id' nat O) (id' bool true)) [X:Type][x:X]x).
+([i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)) [X:Type][x:X]x).
+(* let i = fun x -> x in Pair ((i O), (i True)) *)
+
 
 (* still ok via optim beta -> let *)
 
-Extraction [id':(X:Type)X->X](pair ? ? (id' nat O) (id' bool true)).
+Extraction [i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)).
+(* fun i -> Pair ((i O), (i True)) *)
 
 (* problem: fun f -> (f 0, f true) not legal in ocaml *)
 (* solution: fun f -> (f 0, Obj.magic f true) *)