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, 24 insertions, 65 deletions

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index eb4c73791..6854a4a7c 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -603,12 +603,6 @@ let rec subst_rawconstr subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RRecord (loc,w,rl) ->
-      let w' = Option.smartmap (subst_rawconstr subst) w 
-      and rl' = list_smartmap (fun (id, x) -> (id, subst_rawconstr subst x)) rl in
-	if w == w' && rl == rl' then raw else
-	  RRecord (loc,w',rl')
-
   | RCases (loc,sty,rtno,rl,branches) -> 
       let rtno' = Option.smartmap (subst_rawconstr subst) rtno
       and rl' = list_smartmap (fun (a,x as y) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 83594466e..7400cdd9c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -586,45 +586,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	      mkCase (ci, pred, cj.uj_val, [|b1;b2|])
 	  in
 	    { uj_val = v; uj_type = p }
-	
-    | RRecord (loc,w,l) ->
-	let cw = Option.map (pretype tycon env evdref lvar) w in
-	let cj = match cw with
-	  | None -> 
-	      (match tycon with
-	      | None -> user_err_loc (loc,"pretype",(str "Unnable to infer the record type."))
-	      | Some (_, ty) -> {uj_val=ty;uj_type=ty})
-	  | Some cj -> cj
-	in
-	let constructor = 
-	  let (IndType (indf,realargs)) = 
-	    try find_rectype env (evars_of !evdref) cj.uj_type
-	    with Not_found ->
-	      error_case_not_inductive_loc loc env (evars_of !evdref) cj
-	  in
-	  let cstrs = get_constructors env indf in 
-	    if Array.length cstrs <> 1 then 
-	      user_err_loc (loc,"pretype",(str "Inductive is not a singleton."))
-	    else
-	      let info = cstrs.(0) in
-	      let fields, rest = 
-		List.fold_left (fun (args, rest as acc) (na, b, t) ->
-		  if b = None then 
-		    try 
-		      let id = out_name na in
-		      let _, t = List.assoc id rest in
-			t :: args, List.remove_assoc id rest
-		    with _ -> RHole (loc, Evd.QuestionMark (Evd.Define false)) :: args, rest
-		  else acc) ([], List.map (fun ((loc, id), t) -> id, (loc, t)) l) info.cs_args
-	      in
-		if rest <> [] then 
-		  let id, (loc, t) = List.hd rest in
-		    user_err_loc (loc,"pretype",(str "Unknown field name " ++ pr_id id))
-		else
-		  RApp (loc,
-		       RDynamic (loc, constr_in (applistc (mkConstruct info.cs_cstr) info.cs_params)),
-		       fields)
-	in pretype tycon env evdref lvar constructor
 	  
     | RCases (loc,sty,po,tml,eqns) ->
 	Cases.compile_cases loc sty
@@ -644,8 +605,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 		  (* ... except for Correctness *)
 		let v = mkCast (cj.uj_val, k, tj.utj_val) in
 		  { uj_val = v; uj_type = tj.utj_val }
-	in
-	  inh_conv_coerce_to_tycon loc env evdref cj tycon
+	in inh_conv_coerce_to_tycon loc env evdref cj tycon
 
     | RDynamic (loc,d) ->
 	if (tag d) = "constr" then
@@ -732,13 +692,12 @@ module Pretyping_F (Coercion : Coercion.S) = struct
   let ise_pretype_gen fail_evar sigma env lvar kind c =
     let evdref = ref (Evd.create_evar_defs sigma) in
     let c = pretype_gen_aux evdref env lvar kind c in
-    let evd,_ = consider_remaining_unif_problems env !evdref in
       if fail_evar then 
-	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env evd in
+	let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env !evdref in
 	let c = Evarutil.nf_isevar evd c in
 	  check_evars env Evd.empty evd c;
 	  evd, c
-      else evd, c
+      else !evdref, c
 
   (** Entry points of the high-level type synthesis algorithm *)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index b2e770f65..4d3348407 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -62,7 +62,6 @@ type rawconstr =
   | RLambda of loc * name * binding_kind * rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
@@ -115,7 +114,6 @@ let map_rawconstr f = function
   | RLambda (loc,na,bk,ty,c) -> RLambda (loc,na,bk,f ty,f c)
   | RProd (loc,na,bk,ty,c) -> RProd (loc,na,bk,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
-  | RRecord (loc,c,l) -> RRecord (loc,Option.map f c,List.map (fun (id,c) -> id, f c) l)
   | RCases (loc,sty,rtntypopt,tml,pl) ->
       RCases (loc,sty,Option.map f rtntypopt,
         List.map (fun (tm,x) -> (f tm,x)) tml,
@@ -176,8 +174,6 @@ let occur_rawconstr id =
     | RLambda (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,bk,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RRecord (loc,w,l) -> Option.cata occur false w
-	or List.exists (fun (_, c) -> occur c) l
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	(occur_option rtntypopt)
         or (List.exists (fun (tm,_) -> occur tm) tml)
@@ -224,8 +220,6 @@ let free_rawvars  =
 	let vs' = vars bounded vs ty in 
 	let bounded' = add_name_to_ids bounded na in 
        vars bounded' vs' c
-    | RRecord (loc,f,args) -> 
-	List.fold_left (vars bounded) vs (Option.List.cons f (List.map snd args))
     | RCases (loc,sty,rtntypopt,tml,pl) ->
 	let vs1 = vars_option bounded vs rtntypopt in 
 	let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in 
@@ -286,7 +280,6 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_,_) -> loc
   | RProd (loc,_,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
-  | RRecord (loc,_,_) -> loc
   | RCases (loc,_,_,_,_) -> loc
   | RLetTuple (loc,_,_,_,_) -> loc
   | RIf (loc,_,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 5115e2d59..3628e2a50 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -66,7 +66,6 @@ type rawconstr =
   | RLambda of loc * name * binding_kind *  rawconstr * rawconstr
   | RProd of loc * name * binding_kind * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RRecord of loc * rawconstr option * ((loc * identifier) * rawconstr) list
   | RCases of loc * case_style * rawconstr option * tomatch_tuples * cases_clauses
   | RLetTuple of loc * name list * (name * rawconstr option) * 
       rawconstr * rawconstr
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a9fcaa4c4..99f439224 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -32,9 +32,9 @@ open Reductionops
    projection ou bien une fonction constante (associée à un LetIn) *)
 
 type struc_typ = {
-  s_CONST : identifier; 
+  s_CONST : constructor; 
   s_EXPECTEDPARAM : int;
-  s_PROJKIND : bool list;
+  s_PROJKIND : (name * bool) list;
   s_PROJ : constant option list }
 
 let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
@@ -61,8 +61,9 @@ let subst_structure (_,subst,((kn,i),id,kl,projs as obj)) =
      (Option.smartmap (fun kn -> fst (subst_con subst kn)))
     projs
   in
-    if projs' == projs && kn' == kn then obj else
-      ((kn',i),id,kl,projs')
+  let id' = fst (subst_constructor subst id) in
+    if projs' == projs && kn' == kn && id' == id then obj else
+      ((kn',i),id',kl,projs')
 
 let discharge_structure (_,(ind,id,kl,projs)) =
   Some (Lib.discharge_inductive ind, id, kl,
@@ -88,6 +89,10 @@ let find_projection_nparams = function
   | ConstRef cst -> (Cmap.find cst !projection_table).s_EXPECTEDPARAM
   | _ -> raise Not_found
 
+let find_projection = function
+  | ConstRef cst -> Cmap.find cst !projection_table
+  | _ -> raise Not_found
+
 
 (************************************************************************)
 (*s A canonical structure declares "canonical" conversion hints between *)
@@ -135,7 +140,7 @@ let canonical_projections () =
     !object_table []
 
 let keep_true_projections projs kinds =
-  map_succeed (function (p,true) -> p | _ -> failwith "")
+  map_succeed (function (p,(_,true)) -> p | _ -> failwith "")
     (List.combine projs kinds)
 
 let cs_pattern_of_constr t =
@@ -237,7 +242,7 @@ let check_and_decompose_canonical_structure ref =
     | Construct (indsp,1) -> indsp
     | _ -> error_not_structure ref in
   let s = try lookup_structure indsp with Not_found -> error_not_structure ref in
-  let ntrue_projs = List.length (List.filter (fun x -> x) s.s_PROJKIND) in
+  let ntrue_projs = List.length (List.filter (fun (_, x) -> x) s.s_PROJKIND) in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref;
   (sp,indsp)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 020687009..638cc4304 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -21,8 +21,14 @@ open Library
 (*s A structure S is a non recursive inductive type with a single
    constructor (the name of which defaults to Build_S) *)
 
+type struc_typ = {
+  s_CONST : constructor; 
+  s_EXPECTEDPARAM : int;
+  s_PROJKIND : (name * bool) list;
+  s_PROJ : constant option list }
+
 val declare_structure : 
-  inductive * identifier * bool list * constant option list -> unit
+  inductive * constructor * (name * bool) list * constant option list -> unit
 
 (* [lookup_projections isp] returns the projections associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
@@ -32,6 +38,9 @@ val lookup_projections : inductive -> constant option list
 (* raise [Not_found] if not a projection *)
 val find_projection_nparams : global_reference -> int
 
+(* raise [Not_found] if not a projection *)
+val find_projection : global_reference -> struc_typ
+
 (*s A canonical structure declares "canonical" conversion hints between *)
 (*  the effective components of a structure and the projections of the  *)
 (*  structure *)