Les records déclarés avec Record ne peuvent plus être récursifs (le

comportement est similaire à la 8.1). Les records récursifs peuvent-être 
déclarés avec Inductive et CoInductive, avec les effets idoines sur leur 
nature.

J'ai fait quelques changements dans VernacInductive pour que tout ceci 
fonctionne bien ensemble. Il reste du nettoyage à faire et probablement 
des ajustement dans le Printing.



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

11 files changed, 75 insertions, 39 deletions

diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index f0e5c6256..7e9ba3f8e 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1370,12 +1370,12 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds))
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds))
 	    ++ fnl () ++
 	    msg
 	in
@@ -1385,12 +1385,12 @@ let do_build_inductive
 	let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
 	let repacked_rel_inds = 
-	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , None, Vernacexpr.Constructors l),ntn )
+	  List.map  (fun ((a , b , c , l),ntn) -> ((false,a) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
 	                  rel_inds
 	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,false,repacked_rel_inds)) 
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(Decl_kinds.Finite,false,repacked_rel_inds)) 
 	    ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 5180bdad2..668a581e1 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -109,7 +109,7 @@ let convert_one_inductive sp tyi =
   let sp = sp_of_global (IndRef (sp, tyi)) in
   (((false,(dummy_loc,basename sp)),
    convert_env(List.rev params),
-   Some (extern_constr true envpar arity), None,
+   Some (extern_constr true envpar arity), Vernacexpr.Inductive_kw ,
    Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
 
 (* This function converts a Mutual inductive definition to a Coqast.t.
@@ -121,7 +121,7 @@ let mutual_to_ast_list sp mib =
   let _, l =
     Array.fold_right
       (fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
-  VernacInductive (mib.mind_finite, false, l)
+  VernacInductive ((if mib.mind_finite then Decl_kinds.Finite else Decl_kinds.CoFinite), false, l)
   :: (implicit_args_to_ast_list sp mipv);;
 
 let constr_to_ast v = 
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 71cef59e2..c8684a9a0 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1984,7 +1984,7 @@ let rec xlate_vernac =
 (* 	xlate_formula (Option.get c1), record_constructor, *)
 (*          build_record_field_list field_list) *)
    | VernacInductive (isind, _, lmi) ->
-      let co_or_ind = if isind then "Inductive" else "CoInductive" in
+      let co_or_ind = if Decl_kinds.recursivity_flag_of_kind isind then "Inductive" else "CoInductive" in
       let strip_mutind = function
           (((_, (_,s)), parameters, c, _, Constructors constructors), notopt) ->
           CT_ind_spec
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 735a8fb07..03b14e31c 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -112,3 +112,18 @@ let strength_of_global = function
 let string_of_strength = function
   | Local -> "Local"
   | Global -> "Global"
+
+
+(* Recursive power *)
+
+(* spiwack: this definition might be of use in the kernel, for now I do not
+                   push them deeper than needed, though. *)
+type recursivity_kind =
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+let recursivity_flag_of_kind = function
+  | Finite | BiFinite -> true
+  | CoFinite -> false
diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli
index 7aa1df0c9..e42cb9621 100644
--- a/library/decl_kinds.mli
+++ b/library/decl_kinds.mli
@@ -82,3 +82,13 @@ val string_of_definition_kind :
 
 val strength_of_global : global_reference -> locality
 val string_of_strength : locality -> string
+
+(* About recursive power of type declarations *)
+
+type recursivity_kind =
+  | Finite (* = inductive *)
+  | CoFinite (* = coinductive *)
+  | BiFinite (* = non-recursive, like in "Record" definitions *)
+
+(* helper, converts to "finiteness flag" booleans *)
+val recursivity_flag_of_kind : recursivity_kind -> bool
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ff6d998e2..03b146648 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -151,6 +151,8 @@ GEXTEND Gram
       (* Gallina inductive declarations *)
       | f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
+	  let (k,f) = f in
+	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (f,false,indl)
       | IDENT "Boxed";"Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           VernacFixpoint (recs,true)
@@ -171,7 +173,7 @@ GEXTEND Gram
 	cfs = [ ":="; l = constructor_list_or_record_decl -> l
 	  | -> RecordDecl (None, []) ] ->
 	  let (recf,indf) = b in
-	    VernacInductive (indf,infer,[((oc,name),ps,s,Some recf,cfs),None])
+	    VernacInductive (indf,infer,[((oc,name),ps,s,recf,cfs),None])
   ] ]
   ;
   typeclass_context:
@@ -214,16 +216,16 @@ GEXTEND Gram
     [ ["Inline" -> true |  -> false] ]
   ;
   finite_token:
-    [ [ "Inductive" -> true
-      | "CoInductive" -> false ] ]
+    [ [ "Inductive" -> (Inductive_kw,Finite)
+      | "CoInductive" -> (CoInductive,CoFinite) ] ]
   ;
   infer_token:
     [ [ "Infer" -> true | -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> (Record,true)
-      | IDENT "Structure" -> (Structure,true) 
-      | IDENT "Class" -> (Class true,true) ] ]
+    [ [ IDENT "Record" -> (Record,BiFinite)
+      | IDENT "Structure" -> (Structure,BiFinite) 
+      | IDENT "Class" -> (Class true,BiFinite) ] ]
   ;
   (* Simple definitions *)
   def_body:
@@ -249,7 +251,7 @@ GEXTEND Gram
     [ [ id = identref; oc = opt_coercion; indpar = binders_let; 
         c = OPT [ ":"; c = lconstr -> c ];
         ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
-	   (((oc,id),indpar,c,None,lc),ntn) ] ]
+	   (((oc,id),indpar,c,lc),ntn) ] ]
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 496af5b6e..7b3491de2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -594,10 +594,9 @@ let rec pr_vernac = function
 	    pr_record_decl b c fs in
       let pr_oneind key (((coe,id),indpar,s,k,lc),ntn) =
 	let kw =
-	  match k with
-	  | None -> str key
-	  | Some b -> str (match b with Record -> "Record" | Structure -> "Structure" 
-	    | Class b -> if b then "Definitional Class" else "Class")
+	  str (match k with Record -> "Record" | Structure -> "Structure"  
+		 | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+		 | Class b -> if b then "Definitional Class" else "Class")
 	in
 	  hov 0 (
 	    kw ++ spc() ++
@@ -608,7 +607,7 @@ let rec pr_vernac = function
 	      str" :=") ++ pr_constructor_list k lc ++ 
 	    pr_decl_notation pr_constr ntn 
       in
-      hov 1 (pr_oneind (if f then "Inductive" else "CoInductive") (List.hd l))
+      hov 1 (pr_oneind (if (Decl_kinds.recursivity_flag_of_kind f) then "Inductive" else "CoInductive") (List.hd l))
       ++ 
       (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3ef7eccad..10d4e5dc6 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -250,10 +250,19 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] }
   in
+  (* spiwack: raises an error if the structure is supposed to be non-recursive,
+        but isn't *)
+  (* there is probably a way to push this to "declare_mutual" *)
+  begin match  finite with
+  | BiFinite -> 
+      if dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) then
+	error "Records declared with the keyword Record or Structure cannot be recursive. Maybe you meant to define an Inductive or CoInductive record."
+  | _ -> ()
+  end;
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = finite;
+      mind_entry_finite = recursivity_flag_of_kind finite;
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_with_eliminations true mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
@@ -333,7 +342,7 @@ let declare_class finite def infer id idbuild paramimpls params arity fieldimpls
 	cref, [proj_name, Some proj_cst]
     | _ ->
 	let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	let ind = declare_structure true infer (snd id) idbuild paramimpls
+	let ind = declare_structure BiFinite infer (snd id) idbuild paramimpls
 	  params (Option.cata (fun x -> x) (new_Type ()) arity) fieldimpls fields
 	  ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) sign
 	in
@@ -386,16 +395,16 @@ let definition_structure (kind,finite,infer,(is_coe,(loc,idstruc)),ps,cfs,idbuil
     States.with_heavy_rollback (fun () ->
       typecheck_params_and_fields idstruc sc ps notations fs) () in
   let sign = structure_signature (fields@params) in
-    match kind with
-    | Record | Structure ->
-	let arity = Option.default (new_Type ()) sc in
-	let implfs = List.map
-	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
-	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
-	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
-	IndRef ind	  
+    match kind with	  
     | Class def ->
 	let gr = declare_class finite def infer (loc,idstruc) idbuild 
 	  implpars params sc implfs fields is_coe coers sign in
 	if infer then search_record declare_class_instance gr sign;
 	gr
+    | _ ->
+	let arity = Option.default (new_Type ()) sc in
+	let implfs = List.map
+	  (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
+	let ind = declare_structure finite infer idstruc idbuild implpars params arity implfs fields is_coe coers sign in
+	if infer then search_record declare_record_instance (ConstructRef (ind,1)) sign;
+	IndRef ind
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 564d4409f..0e23af5c0 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -27,7 +27,8 @@ val declare_projections :
   bool list -> manual_explicitation list list -> rel_context -> 
   (name * bool) list * constant option list
 
-val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier -> identifier -> 
+val declare_structure : Decl_kinds.recursivity_kind -> 
+  bool (*infer?*) -> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *) constr -> (* arity *)
   Impargs.manual_explicitation list list -> rel_context -> (* fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
@@ -37,6 +38,6 @@ val declare_structure : bool (*coinductive?*)-> bool (*infer?*) -> identifier ->
   inductive
 
 val definition_structure :
-  record_kind * bool (*coinductive?*) * bool(*infer?*)* lident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.recursivity_kind * bool(*infer?*)* lident with_coercion * local_binder list *
   (local_decl_expr with_coercion with_notation) list * 
   identifier * constr_expr option -> global_reference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 39a545215..5796d79ee 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -399,17 +399,17 @@ let vernac_inductive finite infer indl =
 	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
   match indl with
-  | [ ( id , bl , c , Some b, RecordDecl (oc,fs) ), None ] -> 
+  | [ ( id , bl , c , b, RecordDecl (oc,fs) ), None ] -> 
       vernac_record (match b with Class true -> Class false | _ -> b)
 	finite infer id bl c oc fs
-  | [ ( id , bl , c , Some (Class true), Constructors [l]), _ ] -> 
+  | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> 
       let f = 
 	let (coe, ((loc, id), ce)) = l in
 	  ((coe, AssumExpr ((loc, Name id), ce)), None)
       in vernac_record (Class true) finite infer id bl c None [f]
-  | [ ( id , bl , c , Some (Class true), _), _ ] -> 
+  | [ ( id , bl , c , Class true, _), _ ] -> 
       Util.error "Definitional classes must have a single method"
-  | [ ( id , bl , c , Some (Class false), Constructors _), _ ] ->
+  | [ ( id , bl , c , Class false, Constructors _), _ ] ->
       Util.error "Inductive classes not supported"
   | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> 
       Util.error "where clause not supported for (co)inductive records"
@@ -418,7 +418,7 @@ let vernac_inductive finite infer indl =
       | _ -> Util.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-      Command.build_mutual indl finite
+      Command.build_mutual indl (recursivity_flag_of_kind finite)
 
 let vernac_fixpoint l b = 
   if Dumpglob.dump () then
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index aa6a48d66..b94526a6e 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -140,7 +140,7 @@ type locality_flag  = bool (* true = Local;         false = Global         *)
 type coercion_flag  = bool (* true = AddCoercion;   false = NoCoercion     *)
 type export_flag    = bool (* true = Export;        false = Import         *)
 type specif_flag    = bool (* true = Specification; false = Implementation *)
-type inductive_flag = bool (* true = Inductive;     false = CoInductive    *)
+type inductive_flag = Decl_kinds.recursivity_kind
 type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
 
@@ -155,7 +155,7 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type record_kind = Record | Structure | Class of bool (* true = definitional, false = inductive *)
+type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
 type decl_notation = (string * constr_expr * scope_name option) option
 type simple_binder = lident list  * constr_expr
 type class_binder = lident * constr_expr list
@@ -166,7 +166,7 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-  lident with_coercion * local_binder list * constr_expr option * record_kind option * 
+  lident with_coercion * local_binder list * constr_expr option * inductive_kind * 
     constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast