Nouvelle syntaxe pour écrire des records (co)inductifs :

CoInductive stream (A:Type) := { hd : A ; tl : stream A }.

Inductive nelist (A:Type) := { hd : A ; tl : option (nelist A) }.

L'affichage n'est pas encore poli. Il reste à choisir l'exact destin de 
la syntaxe qui était apparue dans la 8.2beta pour les records 
coinductifs (qui consistait à utiliser "Record" au lieu de "CoInductive" 
comme maintenant).
VernacRecord et VernacInductive semblent maintenant faire doublon, il 
doit y avoir moyen de les fusionner.
Les records mutuellement inductifs restent aussi à faire.





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

11 files changed, 132 insertions, 89 deletions

diff --git a/CHANGES b/CHANGES
index f0de89eac..64f51f1d7 100644
--- a/CHANGES
+++ b/CHANGES
@@ -20,8 +20,8 @@ Language
   arguments in terms.
 - Sort of Record/Structure, Inductive and CoInductive defaults to Type
   if omitted.
-- Record/Structure now usable for defining coinductive types
-  (e.g. "Record stream := { hd : nat; tl : stream }.")
+- (Co)Inductive types can be defined as records 
+  (e.g. "CoInductive stream := { hd : nat; tl : stream }.")
 - New syntax "Theorem id1:t1 ... with idn:tn" for proving mutually dependent
   statements.
 - Support for sort-polymorphism on constants denoting inductive types.
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index ec456aae6..b7cee7390 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -855,7 +855,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
     [rawlist], named ident.
     FIXME: params et cstr_expr (arity) *)
 let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
-    (rawlist:(identifier * rawconstr) list):inductive_expr =
+    (rawlist:(identifier * rawconstr) list) =
   let lident = dummy_loc, shift.ident in
   let bindlist , cstr_expr = (* params , arities *)
     merge_rec_params_and_arity prms1 prms2 shift mkSet in
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index 7534ce2ca..48a96f8b6 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1226,9 +1226,14 @@ let do_build_inductive
     | UserError(s,msg) as e ->
 	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) -> (a , b, c , Vernacexpr.Constructors l),ntn )
+	                  rel_inds
+	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds))
+	    ++ fnl () ++
 	    msg
 	in
 	observe (msg);
@@ -1236,9 +1241,14 @@ let do_build_inductive
     | e -> 
 	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) -> (a , b, c , Vernacexpr.Constructors l),ntn )
+	                  rel_inds
+	in
 	let msg = 		     
 	  str "while trying to define"++ spc () ++
-	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,rel_inds)) ++ fnl () ++
+	    Ppvernac.pr_vernac (Vernacexpr.VernacInductive(true,repacked_rel_inds)) 
+	    ++ fnl () ++
 	    Cerrors.explain_exn e
 	in
  	observe msg;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index f0ea35d92..3f8adb92f 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -224,7 +224,7 @@ GEXTEND Gram
       | "CoInductive" -> false ] ]
   ;
   record_token:
-    [ [ IDENT "Record" -> true | IDENT "Structure" -> false ] ]
+    [ [ IDENT "Record" -> (true,true) | IDENT "Structure" -> (false,true) ]]
   ;
   (* Simple definitions *)
   def_body:
@@ -249,13 +249,18 @@ GEXTEND Gram
   inductive_definition:
     [ [ id = identref; indpar = binders_let; 
         c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
-        ":="; lc = constructor_list; ntn = decl_notation ->
-	  ((id,indpar,c,lc),ntn) ] ]
-  ;
-  constructor_list:
-    [ [ "|"; l = LIST1 constructor SEP "|" -> l
-      | l = LIST1 constructor SEP "|" -> l
-      |  -> [] ] ]
+        ":="; lc = constructor_list_or_record_decl; ntn = decl_notation ->
+	   ((id,indpar,c,lc),ntn) ] ]
+  ;
+  constructor_list_or_record_decl:
+    [ [ "|"; l = LIST1 constructor SEP "|" -> Constructors l
+      | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" -> 
+	      Constructors ((c id)::l)
+      | id = identref ; c = constructor_type -> Constructors [ c id ]
+      | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> 
+	     RecordDecl (Some cstr,fs) 
+      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs) 
+      |  -> Constructors [] ] ]
   ;
 (*
   csort:
@@ -346,12 +351,19 @@ GEXTEND Gram
     [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> 
         (oc,(idl,c)) ] ]
   ;
+
+  constructor_type:
+    [[ l = binders_let; 
+      t= [ coe = of_type_with_opt_coercion; c = lconstr ->
+	            fun l id -> (coe,(id,mkCProdN loc l c))
+            |  ->
+		 fun l id -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ]
+	 -> t l
+     ]]
+;
+
   constructor:
-    [ [ id = identref; l = binders_let; 
-        coe = of_type_with_opt_coercion; c = lconstr ->
-	  (coe,(id,mkCProdN loc l c))
-      | id = identref; l = binders_let ->
-	  (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ]
+    [ [ id = identref; c=constructor_type -> c id ] ]
   ;
   of_type_with_opt_coercion:
     [ [ ":>" -> true
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 2233bbd6a..e2237450c 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -412,6 +412,27 @@ let pr_lident_constr sep (i,c) = pr_lident i ++ sep ++ pr_constrarg c in
 let pr_instance_def sep (i,l,c) = pr_lident i ++ prlist_with_sep spc pr_lident l 
   ++ sep ++ pr_constrarg c in
 
+ let pr_record_field = function
+   | (oc,AssumExpr (id,t)) ->
+       hov 1 (pr_lname id ++
+		(if oc then str" :>" else str" :") ++ spc() ++
+		pr_lconstr_expr t)
+   | (oc,DefExpr(id,b,opt)) -> 
+       (match opt with
+	  | Some t ->
+	      hov 1 (pr_lname id ++
+		       (if oc then str" :>" else str" :") ++ spc() ++
+		       pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
+	  | None ->
+	      hov 1 (pr_lname id ++ str" :=" ++ spc() ++
+		       pr_lconstr b))
+in
+
+let pr_record_decl c fs = 
+    pr_opt pr_lident c ++ str"{"  ++
+    hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
+in
+
 let rec pr_vernac = function
   
   (* Proof management *)
@@ -565,12 +586,15 @@ let rec pr_vernac = function
                (if coe then str":>" else str":") ++
                 pr_spc_lconstr c) in
       let pr_constructor_list l = match l with
-        | [] -> mt()
-        | _ ->
+        | Constructors [] -> mt()
+        | Constructors l ->
             pr_com_at (begin_of_inductive l) ++
             fnl() ++
             str (if List.length l = 1 then "   " else " | ") ++
-            prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l in
+            prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l 
+       | RecordDecl (c,fs) ->   
+	    spc() ++
+	    pr_record_decl c fs in
       let pr_oneind key ((id,indpar,s,lc),ntn) =
 	hov 0 (
           str key ++ spc() ++
@@ -644,30 +668,12 @@ let rec pr_vernac = function
 	
 
   (* Gallina extensions *)
-  | VernacRecord (b,(oc,name),ps,s,c,fs) ->
-      let pr_record_field = function
-        | (oc,AssumExpr (id,t)) ->
-            hov 1 (pr_lname id ++
-            (if oc then str" :>" else str" :") ++ spc() ++
-            pr_lconstr_expr t)
-        | (oc,DefExpr(id,b,opt)) -> (match opt with
-	    | Some t ->
-                hov 1 (pr_lname id ++
-                (if oc then str" :>" else str" :") ++ spc() ++
-                pr_lconstr_expr t ++ str" :=" ++ pr_lconstr b)
-	    | None ->
-                hov 1 (pr_lname id ++ str" :=" ++ spc() ++
-                pr_lconstr b)) in
+  | VernacRecord ((b,coind),(oc,name),ps,s,c,fs) ->
       hov 2
         (str (if b then "Record" else "Structure") ++
          (if oc then str" > " else str" ") ++ pr_lident name ++ 
           pr_and_type_binders_arg ps ++ str" :" ++ spc() ++ 
-	  pr_lconstr_expr s ++ str" := " ++
-         (match c with
-           | None -> mt()
-           | Some sc -> pr_lident sc) ++
-	spc() ++ str"{"  ++
-        hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}"))
+	  pr_lconstr_expr s ++ str" := " ++ pr_record_decl c fs)
   | VernacBeginSection id -> hov 2 (str"Section" ++ spc () ++ pr_lident id)
   | VernacEndSegment id -> hov 2 (str"End" ++ spc() ++ pr_lident id)
   | VernacRequire (exp,spe,l) -> hov 2
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4eca304c2..b3e646858 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -230,7 +230,7 @@ let new_class id par ar sup props =
       | _ ->
 	  let idb = id_of_string ("Build_" ^ (string_of_id (snd id))) in
 	  let idarg = Nameops.next_ident_away (snd id) (ids_of_context (Global.env())) in
-	  let kn = Record.declare_structure (snd id) idb arity_imps
+	  let kn = Record.declare_structure false (snd id) idb arity_imps
 	    params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields)
 	  in
 	    IndRef (kn,0), (List.map2 (fun (id, _, _) y -> (Nameops.out_name id, y))
diff --git a/toplevel/command.mli b/toplevel/command.mli
index a1e976c79..386663538 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -67,7 +67,8 @@ val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_ty
 val check_mutuality : Environ.env -> definition_object_kind ->
   (identifier * types) list -> unit
 
-val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
+val build_mutual : ((lident * local_binder list * constr_expr * constructor_expr list) * 
+		                decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
   bool -> Entries.mutual_inductive_entry -> 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 75a0c1293..8d3dd67e7 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -217,7 +217,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
       (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
-let declare_structure id idbuild paramimpls params arity fieldimpls fields
+let declare_structure finite id idbuild paramimpls params arity fieldimpls fields
     ?(kind=StructureComponent) ?name is_coe coers =
   let nparams = List.length params and nfields = List.length fields in
   let args = extended_rel_list nfields params in
@@ -227,14 +227,12 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields
     { mind_entry_typename = id;
       mind_entry_arity = arity;
       mind_entry_consnames = [idbuild];
-      mind_entry_lc = [type_constructor] } in
-  let declare_as_coind =
-    (* CoInd if recursive; otherwise Ind to have compat on _ind schemes *) 
-    dependent (mkRel (nparams+1)) (it_mkProd_or_LetIn mkProp fields) in
+      mind_entry_lc = [type_constructor] }
+  in
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = not declare_as_coind;
+      mind_entry_finite = 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 *)
@@ -246,7 +244,7 @@ let declare_structure id idbuild paramimpls params arity fieldimpls fields
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
-let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+let definition_structure (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
   let extract_name acc = function
       Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
@@ -258,5 +256,5 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let implpars, params, implfs, fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
   let implfs = List.map 
     (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs in
-    declare_structure idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
+    declare_structure finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
   
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 7799162df..9ac96641a 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -26,7 +26,7 @@ val declare_projections :
   bool list -> manual_explicitation list list -> rel_context -> 
   bool list * constant option list
 
-val declare_structure : identifier -> identifier -> 
+val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *)
   Term.constr -> (* arity *)
   Impargs.manual_explicitation list list -> Sign.rel_context -> (* fields *)
@@ -36,5 +36,5 @@ val declare_structure : identifier -> identifier ->
   mutual_inductive
 
 val definition_structure :
-  lident with_coercion * local_binder list *
+  bool (*coinductive?*)*lident with_coercion * local_binder list *
   (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d1c972e2b..5a28d60cf 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -371,15 +371,49 @@ let vernac_assumption kind l nl=
 	  if global then Dumpglob.dump_definition lid false "ax" 
 	  else Dumpglob.dump_definition lid true "var") idl;
       declare_assumption idl is_coe kind [] c false false nl) l
+	  
+let vernac_record finite struc binders sort nameopt cfs =
+  let const = match nameopt with 
+    | None -> add_prefix "Build_" (snd (snd struc))
+    | Some (_,id as lid) ->
+	Dumpglob.dump_definition lid false "constr"; id in
+  let sigma = Evd.empty in
+  let env = Global.env() in
+  let s = interp_constr sigma env sort in
+  let s = Reductionops.whd_betadeltaiota env sigma s in
+  let s = match kind_of_term s with
+    | Sort s -> s
+    | _ -> user_err_loc
+        (constr_loc sort,"definition_structure", str "Sort expected.") in
+    if Dumpglob.dump () then (
+      Dumpglob.dump_definition (snd struc) false "rec";
+      List.iter (fun (_, x) ->
+	match x with
+	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
+	| _ -> ()) cfs);
+    ignore(Record.definition_structure (finite,struc,binders,cfs,const,s))
       
-let vernac_inductive f indl = 
+let vernac_inductive finite indl = 
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, cstrs), _) ->
-      Dumpglob.dump_definition lid false "ind";
-      List.iter (fun (_, (lid, _)) ->
-	Dumpglob.dump_definition lid false "constr") cstrs)
+      match cstrs with 
+	| Constructors cstrs ->
+	    Dumpglob.dump_definition lid false "ind";
+	    List.iter (fun (_, (lid, _)) ->
+			 Dumpglob.dump_definition lid false "constr") cstrs
+	| _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
-  build_mutual indl f
+  match indl with
+  | [ ( id , bl , c ,RecordDecl (oc,fs) ), None ] -> 
+            vernac_record finite (false,id) bl c oc fs
+  | [ ( _ , _ , _ , RecordDecl _ ) , _ ] -> 
+            Util.error "where clause not supported for (co)inductive records"
+  | _ -> let unpack = function 
+              | ( id , bl , c , Constructors l ) , ntn  -> ( id , bl , c , l ) , ntn
+	      | _ -> Util.error "Cannot handle mutually (co)inductive records."
+            in
+            let indl = List.map unpack indl in
+            Command.build_mutual indl finite
 
 let vernac_fixpoint l b = 
   if Dumpglob.dump () then
@@ -527,27 +561,6 @@ let vernac_include = function
 	  
 (**********************)
 (* Gallina extensions *)
-	  
-let vernac_record struc binders sort nameopt cfs =
-  let const = match nameopt with 
-    | None -> add_prefix "Build_" (snd (snd struc))
-    | Some (_,id as lid) ->
-	Dumpglob.dump_definition lid false "constr"; id in
-  let sigma = Evd.empty in
-  let env = Global.env() in
-  let s = interp_constr sigma env sort in
-  let s = Reductionops.whd_betadeltaiota env sigma s in
-  let s = match kind_of_term s with
-    | Sort s -> s
-    | _ -> user_err_loc
-        (constr_loc sort,"definition_structure", str "Sort expected.") in
-    if Dumpglob.dump () then (
-      Dumpglob.dump_definition (snd struc) false "rec";
-      List.iter (fun (_, x) ->
-	match x with
-	| AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
-	| _ -> ()) cfs);
-    ignore(Record.definition_structure (struc,binders,cfs,const,s))
 
   (* Sections *)
 
@@ -1314,7 +1327,7 @@ let interp c = match c with
 
   | VernacEndSegment lid -> vernac_end_segment lid
 
-  | VernacRecord (_,id,bl,s,idopt,fs) -> vernac_record id bl s idopt fs
+  | VernacRecord ((_,finite),id,bl,s,idopt,fs) -> vernac_record finite id bl s idopt fs
   | VernacRequire (export,spec,qidl) -> vernac_require export spec qidl
   | VernacImport (export,qidl) -> vernac_import export qidl
   | VernacCanonical qid -> vernac_canonical qid
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 19b913708..ca539f28a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -146,14 +146,6 @@ type onlyparsing_flag = bool (* true = Parse only;  false = Print also     *)
 
 type sort_expr = Rawterm.rawsort
 
-type decl_notation = (string * constr_expr * scope_name option) option
-type simple_binder = lident list  * constr_expr
-type class_binder = lident * constr_expr list
-type 'a with_coercion = coercion_flag * 'a
-type constructor_expr = (lident * constr_expr) with_coercion
-type inductive_expr =
-     lident * local_binder list * constr_expr * constructor_expr list
-
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
   | DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -163,6 +155,17 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
+type decl_notation = (string * constr_expr * scope_name option) option
+type simple_binder = lident list  * constr_expr
+type class_binder = lident * constr_expr list
+type 'a with_coercion = coercion_flag * 'a
+type constructor_expr = (lident * constr_expr) with_coercion
+type constructor_list_or_record_decl_expr =
+  | Constructors of constructor_expr list
+  | RecordDecl of lident option * local_decl_expr with_coercion list
+type inductive_expr =
+     lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr
+
 type module_binder = bool option * lident list * module_type_ast
 
 type grammar_production =
@@ -212,7 +215,7 @@ type vernac_expr =
   | VernacCombinedScheme of lident * lident list
 
   (* Gallina extensions *)
-  | VernacRecord of bool (* = Record or Structure *)
+  | VernacRecord of (bool*bool) (* = Record or Structure * Inductive or CoInductive *)
       * lident with_coercion * local_binder list
       * constr_expr * lident option * local_decl_expr with_coercion list
   | VernacBeginSection of lident