Ajout notation c.(f) en v8 pour les projections de Record

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

4 files changed, 27 insertions, 9 deletions

diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 74ecdaaa3d..487f45057c 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -144,7 +144,7 @@ let (imply_intro1: pbp_rule) = function
 
 let make_var id = CRef (Ident(zz, id))
 
-let make_app f l = CApp (zz,f,List.map (fun x -> (x,None)) l)
+let make_app f l = CApp (zz,(false,f),List.map (fun x -> (x,None)) l)
 
 let make_pbp_pattern x =
   make_app (make_var (id_of_string "PBP_META"))
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b83ce2d71e..14caa9f98e 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -308,10 +308,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
        CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
-   | CAppExpl(_, r, l) ->
+   | CAppExpl(_, (_,r), l) -> (* TODO: proj notation *)
        CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)),
 	       xlate_formula_ne_list l)
-   | CApp(_, f, l) ->
+   | CApp(_, (_,f), l) -> (* TODO: proj notation *)
        CT_appc(xlate_formula f, xlate_formula_expl_ne_list l)
    | CCases (_,po,tml,eqns)-> CT_cases(xlate_formula_opt po, 
                          xlate_formula_ne_list tml,
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e2d4036f43..b0c3df6076 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -41,9 +41,16 @@ type struc_typ = {
   s_PARAM : int;
   s_PROJ : constant option list }
 
-let structure_table = (ref [] : (inductive * struc_typ) list ref)
+let structure_table = ref (Indmap.empty : struc_typ Indmap.t)
+let projection_table = ref KNmap.empty
 
-let cache_structure (_,x) = structure_table := x :: (!structure_table)
+let option_fold_right f p e = match p with Some a -> f a e | None -> e
+
+let cache_structure (_,(ind,struc)) =
+  structure_table := Indmap.add ind struc !structure_table;
+  projection_table := 
+    List.fold_right (option_fold_right (fun proj -> KNmap.add proj struc))
+      struc.s_PROJ !projection_table
 
 let subst_structure (_,subst,((kn,i),struc as obj)) = 
   let kn' = subst_kn subst kn in
@@ -65,7 +72,11 @@ let (inStruc,outStruc) =
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
 
-let find_structure indsp = List.assoc indsp !structure_table
+let find_structure indsp = Indmap.find indsp !structure_table
+
+let find_projection_nparams = function
+  | ConstRef cst -> (KNmap.find cst !projection_table).s_PARAM
+  | _ -> raise Not_found
 
 (*s Un "object" est une fonction construisant une instance d'une structure *)
 
@@ -144,11 +155,15 @@ let (inObjDef1,outObjDef1) =
 
 let objdef_info o = List.assoc o !object_table
 
-let freeze () = !structure_table, !object_table
+let freeze () =
+  !structure_table, !projection_table, !object_table
 
-let unfreeze (s,o) = structure_table := s; object_table := o
+let unfreeze (s,p,o) = 
+  structure_table := s; projection_table := p; object_table := o
 
-let init () = structure_table := []; object_table:=[]
+let init () =
+  structure_table := Indmap.empty; projection_table := KNmap.empty;
+  object_table:=[]
 
 let _ = init()
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index e5ffe4fd24..f758776de4 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -37,6 +37,9 @@ val add_new_struc :
    [isp] if it corresponds to a structure, otherwise fails with [Not_found] *)
 val find_structure : inductive -> struc_typ
 
+(* raise [Not_found] if not a projection *)
+val find_projection_nparams : global_reference -> int
+
 type obj_typ = {
   o_DEF : constr;
   o_TABS : constr list; (* dans l'ordre *)