- Ajout de la possibilité d'utiliser la notation Record pour les

  coinductifs à un constructeur (suggestion de Georges). 
- Si pas de sorte ou arité mentionnée dans Inductive/CoInductive/Record,
  Type est utilisé comme défaut.



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

5 files changed, 47 insertions, 20 deletions

diff --git a/CHANGES b/CHANGES
index afcffda32c..18a522f7ab 100644
--- a/CHANGES
+++ b/CHANGES
@@ -15,6 +15,13 @@ Libraries
   incompatibilities].
 - Boolean operators moved from module Bool to module Datatypes.
 
+Language
+
+- 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 }.")
+
 Notations and implicit arguments
 
 - New options "Set Maximal Implicit Insertion", "Set Reversible Pattern
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 94e39621e9..f7078aa000 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -149,8 +149,9 @@ GEXTEND Gram
   ;
   gallina_ext:
     [ [ b = record_token; oc = opt_coercion; name = identref;
-        ps = LIST0 binder_let; ":";
-	s = lconstr; ":="; cstr = OPT identref; "{";
+        ps = LIST0 binder_let; 
+	s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ];
+	":="; cstr = OPT identref; "{";
         fs = LIST0 record_field SEP ";"; "}" ->
 	  VernacRecord (b,(oc,name),ps,s,cstr,fs)
 (* Non port�� ?
@@ -224,7 +225,8 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr;
+    [ [ id = identref; indpar = LIST0 binder_let; 
+        c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ];
         ":="; lc = constructor_list; ntn = decl_notation ->
 	  ((id,indpar,c,lc),ntn) ] ]
   ;
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 668b3a1eb4..d01c5679cc 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -989,14 +989,18 @@ let assums_of_rel_context sign =
         | None -> (na, t)::l)
     sign ~init:[]
 
-let lift_rel_context n sign =
-  let rec liftrec k = function
-    | (na,c,t)::sign ->
-	(na,option_map (liftn n k) c,type_app (liftn n k) t)
-	::(liftrec (k-1) sign)
+let map_rel_context_with_binders f sign =
+  let rec aux k = function
+    | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
     | [] -> []
   in
-  liftrec (rel_context_length sign) sign
+  aux (rel_context_length sign) sign
+
+let substl_rel_context l =
+  map_rel_context_with_binders (fun k -> substnl l (k-1))
+
+let lift_rel_context n =
+  map_rel_context_with_binders (liftn n)
 
 let fold_named_context_both_sides f l ~init = list_fold_right_and_left f l init
 
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 27e86a6ca5..17207cf577 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -218,6 +218,9 @@ val rename_bound_var : env -> identifier list -> types -> types
 val process_rel_context : (rel_declaration -> env -> env) -> env -> env
 val assums_of_rel_context : rel_context -> (name * constr) list
 val lift_rel_context : int -> rel_context -> rel_context
+val substl_rel_context : constr list -> rel_context -> rel_context
+val map_rel_context_with_binders : 
+  (int -> constr -> constr) -> rel_context -> rel_context
 val fold_named_context_both_sides :
   ('a -> named_declaration -> named_declaration list -> 'a) ->
     named_context -> init:'a -> 'a
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 1ca84d375d..5cb8b29042 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -41,15 +41,17 @@ let interp_decl sigma env = function
       let j = interp_constr_judgment Evd.empty env c in
       (id,Some j.uj_val, refresh_universes j.uj_type)
 
-let typecheck_params_and_fields ps fs =
+let typecheck_params_and_fields id t ps fs =
   let env0 = Global.env () in
   let env1,newps = interp_context Evd.empty env0 ps in
+  let fullarity = it_mkProd_or_LetIn t newps in
+  let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) d ->
          let decl = interp_decl Evd.empty env d in
          (push_rel decl env, decl::newfs))
-      (env1,[]) fs
+      (env_ar,[]) fs
   in
   newps, newfs
 
@@ -75,17 +77,17 @@ let warning_or_error coe indsp err =
     | BadTypedProj (fi,ctx,te) ->
 	match te with
 	  | ElimArity (_,_,_,_,Some (_,_,NonInformativeToInformative)) ->
-              (str (string_of_id fi) ++ 
+              (pr_id fi ++ 
 		str" cannot be defined because it is informative and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
 		str " is not.")   
 	  | ElimArity (_,_,_,_,Some (_,_,StrongEliminationOnNonSmallType)) ->
-	      (str (string_of_id fi) ++ 
+	      (pr_id fi ++ 
 		str" cannot be defined because it is large and " ++
 		Printer.pr_inductive (Global.env()) indsp ++
 		str " is not.")
 	  | _ -> 
-	      (str " cannot be defined because it is not typable")
+              (pr_id fi ++ str " cannot be defined because it is not typable")
   in
   if coe then errorlabstrm "structure" st;
   Options.if_verbose ppnl (hov 0 (str"Warning: " ++ st))
@@ -124,6 +126,10 @@ let subst_projection fid l c =
     raise (NotDefinable (MissingProj (fid,List.rev !bad_projs)));
   c''
 
+let instantiate_possibly_recursive_type indsp paramdecls fields =
+  let subst = list_map_i (fun i _ -> mkRel i) 1 paramdecls in
+  substl_rel_context (subst@[mkInd indsp]) fields
+
 (* We build projections *)
 let declare_projections indsp coers fields =
   let env = Global.env() in
@@ -133,6 +139,7 @@ let declare_projections indsp coers fields =
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Termops.named_hd (Global.env()) r Anonymous in
+  let fields = instantiate_possibly_recursive_type indsp paramdecls fields in
   let lifted_fields = lift_rel_context 1 fields in
   let (_,kinds,sp_projs,_) =
     List.fold_left2
@@ -198,22 +205,26 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let allnames =  idstruc::(List.fold_left extract_name [] fs) in
   if not (list_distinct allnames) then error "Two objects have the same name";
   (* Now, younger decl in params and fields is on top *)
-  let params,fields = typecheck_params_and_fields ps fs in
-  let args = extended_rel_list (List.length fields) params in
-  let ind = applist (mkRel (1+List.length params+List.length fields), args) in
+  let params,fields = typecheck_params_and_fields idstruc (mkSort s) ps fs in
+  let nparams = List.length params and nfields = List.length fields in
+  let args = extended_rel_list nfields params in
+  let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
     { mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       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
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = true;
+      mind_entry_finite = not declare_as_coind;
       mind_entry_inds = [mie_ind] } in
-  let sp = declare_mutual_with_eliminations true mie in
-  let rsp = (sp,0) in (* This is ind path of idstruc *)
+  let kn = declare_mutual_with_eliminations true mie in
+  let rsp = (kn,0) in (* This is ind path of idstruc *)
   let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build Global;