Move Record desugaring to constrintern and add ability to use notations

for record fields (using "someproj : sometype where not := constr" syntax). Only one
notation allowed currently and no redeclaration after the record
declaration either (will be done for typeclasses).


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

5 files changed, 28 insertions, 21 deletions

diff --git a/toplevel/record.ml b/toplevel/record.ml
index 8d3dd67e7..5ebd89789 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -40,9 +40,9 @@ let mk_interning_data env na impls typ =
   let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls
   in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ))
     
-let interp_fields_evars isevars env l =
-  List.fold_left
-    (fun (env, uimpls, params, impls) ((loc, i), b, t) ->
+let interp_fields_evars isevars env nots l =
+  List.fold_left2
+    (fun (env, uimpls, params, impls) no ((loc, i), b, t) ->
       let impl, t' = interp_evars isevars env ~impls Pretyping.IsType t in
       let b' = Option.map (fun x -> snd (interp_evars isevars env ~impls (Pretyping.OfType (Some t')) x)) b in
       let impls = 
@@ -51,8 +51,10 @@ let interp_fields_evars isevars env l =
 	| Name na -> (fst impls, mk_interning_data env na impl t' :: snd impls)
       in
       let d = (i,b',t') in
+	(* Temporary declaration of notations and scopes *)
+	Option.iter (declare_interning_data impls) no;
 	(push_rel d env, impl :: uimpls, d::params, impls))
-    (env, [], [], ([], [])) l    
+    (env, [], [], ([], [])) nots l
 
 let binder_of_decl = function
   | Vernacexpr.AssumExpr(n,t) -> (n,None,t)
@@ -60,14 +62,14 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
-let typecheck_params_and_fields id t ps fs =
+let typecheck_params_and_fields id t ps nots fs =
   let env0 = Global.env () in
   let (env1,newps), imps = 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 evars = ref (Evd.create_evar_defs Evd.empty) in
   let env2,impls,newfs,data =
-    interp_fields_evars evars env_ar (binders_of_decls fs)
+    interp_fields_evars evars env_ar nots (binders_of_decls fs)
   in
   let newps = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newps in
   let newfs = Evarutil.nf_rel_context_evar (Evd.evars_of !evars) newfs in
@@ -213,7 +215,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
 	      (None::sp_projs,NoProjection fi::subst) in
-      (nfi-1,(optci=None)::kinds,sp_projs,subst))
+      (nfi-1,(fi, optci=None)::kinds,sp_projs,subst))
       (List.length fields,[],[],[]) coers (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
@@ -239,12 +241,13 @@ let declare_structure finite id idbuild paramimpls params arity fieldimpls field
   let kinds,sp_projs = declare_projections rsp ~kind ?name coers fieldimpls fields in
   let build = ConstructRef (rsp,1) in
     if is_coe then Class.try_add_new_coercion build Global;
-    Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs);
+    Recordops.declare_structure(rsp,(rsp,1),List.rev kinds,List.rev sp_projs);
     kn
 
 (* [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 (finite,(is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
+  let cfs,notations = List.split cfs in
   let coers,fs = List.split cfs in
   let extract_name acc = function
       Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
@@ -253,8 +256,11 @@ let definition_structure (finite,(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 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 finite idstruc idbuild implpars params (mkSort s) implfs fields is_coe coers
-  
+  let implpars, params, implfs, fields = 
+    States.with_heavy_rollback (fun () ->
+      typecheck_params_and_fields idstruc (mkSort s) ps notations fs) ()
+  in
+  let implfs = 
+    List.map (fun impls -> implpars @ Impargs.lift_implicits (succ (List.length params)) impls) implfs
+  in 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 9ac96641a..7aea948f3 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -24,7 +24,7 @@ open Impargs
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> ?name:identifier ->
   bool list -> manual_explicitation list list -> rel_context -> 
-  bool list * constant option list
+  (name * bool) list * constant option list
 
 val declare_structure : bool (*coinductive?*)-> identifier -> identifier -> 
   manual_explicitation list -> rel_context -> (* params *)
@@ -37,4 +37,4 @@ val declare_structure : bool (*coinductive?*)-> identifier -> identifier ->
 
 val definition_structure :
   bool (*coinductive?*)*lident with_coercion * local_binder list *
-  (local_decl_expr with_coercion) list * identifier * sorts -> kernel_name
+  (local_decl_expr with_coercion with_notation) list * identifier * sorts -> kernel_name
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5a28d60cf..504561100 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -387,7 +387,7 @@ let vernac_record finite struc binders sort nameopt cfs =
         (constr_loc sort,"definition_structure", str "Sort expected.") in
     if Dumpglob.dump () then (
       Dumpglob.dump_definition (snd struc) false "rec";
-      List.iter (fun (_, x) ->
+      List.iter (fun ((_, x), _) ->
 	match x with
 	| Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj"
 	| _ -> ()) cfs);
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ca539f28a..2727100bf 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -159,12 +159,13 @@ 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 'a with_notation = 'a * decl_notation
 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
+  | RecordDecl of lident option * local_decl_expr with_coercion with_notation list
 type inductive_expr =
-     lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr
+  lident * local_binder list * constr_expr * constructor_list_or_record_decl_expr
 
 type module_binder = bool option * lident list * module_type_ast
 
@@ -217,7 +218,7 @@ type vernac_expr =
   (* Gallina extensions *)
   | 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
+      * constr_expr * lident option * local_decl_expr with_coercion with_notation list
   | VernacBeginSection of lident
   | VernacEndSegment of lident
   | VernacRequire of
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 094c93196..82a2a8449 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -166,8 +166,8 @@ let rec uri_of_constr c =
       uri_of_constr b; url_string " in "; uri_of_constr c
   | RCast (_,c, CastConv (_,t)) ->
       uri_of_constr c; url_string ":"; uri_of_constr t
-  | RRecord _ | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
-      error "Whelp does not support records, pattern-matching and (co-)fixpoint."
+  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+      error "Whelp does not support pattern-matching and (co-)fixpoint."
   | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ | RCast (_,_, CastCoerce) ->
       anomaly "Written w/o parenthesis"
   | RPatVar _ | RDynamic _ ->