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

6 files changed, 33 insertions, 22 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 67946e3a28..237ffb55b8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -677,11 +677,6 @@ let rec extern inctx scopes vars r =
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,Default bk,t],c)
 	
-  | RRecord (loc,w,l) ->
-      let t' = Option.map (extern inctx scopes vars) w in
-      let l' = List.map (fun (id, c) -> (id, extern inctx scopes vars c)) l in
-      CRecord (loc, t', l')
-
   | RCases (loc,sty,rtntypopt,tml,eqns) ->
       let vars' = 
 	List.fold_right (name_fold Idset.add)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dd94bf42d1..660da55255 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -948,8 +948,38 @@ let internalise sigma globalenv env allow_patvar lvar c =
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CRecord (loc, w, fs) ->
-	RRecord (loc, Option.map (intern env) w, 
-		List.map (fun (id, c) -> (id, intern env c)) fs)
+	let id, _ = List.hd fs in
+	let record = 
+	  let (id,_,_,_),_ = intern_applied_reference intern env lvar [] (Ident id) in
+	    match id with
+	    | RRef (loc, ref) -> 
+		(try Recordops.find_projection ref
+		  with Not_found -> user_err_loc (loc, "intern", str"Not a projection"))
+	    | c -> user_err_loc (loc_of_rawconstr id, "intern", str"Not a projection")
+	in
+	let args =
+	  let pars = list_make record.Recordops.s_EXPECTEDPARAM (CHole (loc, None)) in	    
+	  let fields, rest = 
+	    List.fold_left (fun (args, rest as acc) (na, b) ->
+	      if b then 
+		try 
+		  let id = out_name na in
+		  let _, t = List.assoc id rest in
+		    t :: args, List.remove_assoc id rest
+		with _ -> CHole (loc, Some (Evd.QuestionMark (Evd.Define true))) :: args, rest
+	      else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) fs) record.Recordops.s_PROJKIND
+	  in 
+	    if rest <> [] then 
+	      let id, (loc, t) = List.hd rest in
+		user_err_loc (loc,"intern",(str "Unknown field name " ++ pr_id id))
+	    else pars @ List.rev fields
+	in
+	let constrname = 
+	  Qualid (loc, shortest_qualid_of_global Idset.empty (ConstructRef record.Recordops.s_CONST)) 
+	in
+	let app = CAppExpl (loc, (None, constrname), args) in
+	  intern env app
+
     | CCases (loc, sty, rtnpo, tms, eqns) ->
         let tms,env' = List.fold_right
           (fun citm (inds,env) ->
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 0bfc109ab3..d48c85616c 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -98,8 +98,6 @@ let free_vars_of_rawconstr ?(bound=Idset.empty) =
 	let vs' = vars bound vs ty in 
 	let bound' = add_name_to_ids bound na in 
 	vars bound' vs' c
-    | RRecord (loc,w,l) -> List.fold_left (vars bound) vs 
-	(Option.List.cons w (List.map snd l))
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bound vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in 
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 2479f1f04e..f49c42a55d 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -57,7 +57,6 @@ let rec unloc = function
   | RLambda (_,na,bk,ty,c) -> RLambda (dummy_loc,na,bk,unloc ty,unloc c)
   | RProd (_,na,bk,ty,c) -> RProd (dummy_loc,na,bk,unloc ty,unloc c)
   | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c)
-  | RRecord (_,w,l) -> RRecord (dummy_loc,w,l)
   | RCases (_,sty,rtntypopt,tml,pl) ->
       RCases (dummy_loc,sty,
         (Option.map unloc rtntypopt),
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 3dc77dd604..2cbe539819 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -37,7 +37,6 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ARecord of aconstr option * (identifier * aconstr) list
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list
@@ -83,8 +82,6 @@ let rawconstr_of_aconstr_with_binders loc g f e = function
       let e,na = name_fold_map g e na in RProd (loc,na,Explicit,f e ty,f e c)
   | ALetIn (na,b,c) ->
       let e,na = name_fold_map g e na in RLetIn (loc,na,f e b,f e c)
-  | ARecord (b,l) ->
-      RRecord (loc, Option.map (f e) b, List.map (fun (id, x) -> ((loc,id),f e x)) l)
   | ACases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
@@ -149,7 +146,7 @@ let compare_rawconstr f t1 t2 = match t1,t2 with
       f ty1 ty2 & f c1 c2
   | RHole _, RHole _ -> true
   | RSort (_,s1), RSort (_,s2) -> s1 = s2
-  | (RLetIn _ | RRecord _ | RCases _ | RRec _ | RDynamic _
+  | (RLetIn _ | RCases _ | RRec _ | RDynamic _
     | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _),_
   | _,(RLetIn _ | RCases _ | RRec _ | RDynamic _
       | RPatVar _ | REvar _ | RLetTuple _ | RIf _ | RCast _)
@@ -195,7 +192,6 @@ let aconstr_and_vars_of_rawconstr a =
   | RLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
   | RProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
   | RLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
-  | RRecord (_,w,l) -> ARecord (Option.map aux w,List.map (fun ((_,id), x) -> id, aux x) l)
   | RCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = found := idl@(!found); (pat,aux rhs) in
       ACases (sty,Option.map aux rtntypopt,
@@ -323,12 +319,6 @@ let rec subst_aconstr subst bound raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  ALetIn (n,r1',r2')
 
-  | ARecord (r1,r2) -> 
-      let r1' = Option.smartmap (subst_aconstr subst bound) r1 
-      and r2' = list_smartmap (fun (id, x) -> id,subst_aconstr subst bound x) r2 in
-	if r1' == r1 && r2' == r2 then raw else
-	  ARecord (r1',r2')
-
   | ACases (sty,rtntypopt,rl,branches) -> 
       let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
       and rl' = list_smartmap
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b6e2927bbd..2d293eacbf 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -33,7 +33,6 @@ type aconstr =
   | ALambda of name * aconstr * aconstr
   | AProd of name * aconstr * aconstr
   | ALetIn of name * aconstr * aconstr
-  | ARecord of aconstr option * (identifier * aconstr) list
   | ACases of case_style * aconstr option *
       (aconstr * (name * (inductive * int * name list) option)) list *
       (cases_pattern list * aconstr) list