Merge PR #7908: Projections use index representation

11 files changed, 81 insertions, 90 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 4846a9af8c..df747692a4 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -202,16 +202,6 @@ type inline = int option
 (** A constant can have no body (axiom/parameter), or a
     transparent body, or an opaque one *)
 
-(** Projections are a particular kind of constant: 
-    always transparent. *)
-
-type projection_body = {
-  proj_ind : inductive;
-  proj_npars : int;
-  proj_arg : int;
-  proj_type : constr; (* Type under params *)
-}
-
 type constant_def =
   | Undef of inline
   | Def of constr_substituted
@@ -254,7 +244,7 @@ type wf_paths = recarg Rtree.t
 type record_info =
 | NotRecord
 | FakeRecord
-| PrimRecord of (Id.t * Constant.t array * projection_body array) array
+| PrimRecord of (Id.t * Label.t array * constr array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
diff --git a/checker/closure.ml b/checker/closure.ml
index 2dcc1a9840..5706011607 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -273,7 +273,7 @@ let update v1 (no,t) =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
@@ -497,8 +497,8 @@ let rec zip m stk =
     | ZcaseT(ci,p,br,e)::s ->
         let t = FCaseT(ci, p, m, br, e) in
         zip {norm=neutr m.norm; term=t} s
-    | Zproj (i,j,cst) :: s -> 
-        zip {norm=neutr m.norm; term=FProj (cst,m)} s
+    | Zproj p :: s ->
+        zip {norm=neutr m.norm; term=FProj (Projection.make p true,m)} s
     | Zfix(fx,par)::s ->
         zip fx (par @ append_stack [|m|] s)
     | Zshift(n)::s ->
@@ -618,21 +618,25 @@ let drop_parameters depth n argstk =
 
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
-    match mib.mind_record with
-    | PrimRecord info when mib.mind_finite <> CoFinite ->
-      let (_, projs, pbs) = info.(snd ind) in
-	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
-	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
-      let pars = mib.mind_nparams in
-      let right = fapp_stack (f, s') in
-      let (depth, args, s) = strip_update_shift_app m s in
-      (** Try to drop the params, might fail on partially applied constructors. *)
-      let argss = try_drop_parameters depth pars args in
-	let hstack =
-	  Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
-			     term = FProj (Projection.make p false, right) }) projs in
-	argss, [Zapp hstack]	
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+  (* disallow eta-exp for non-primitive records *)
+  if not (mib.mind_finite == BiFinite) then raise Not_found;
+  match Declarations.inductive_make_projections ind mib with
+  | Some projs ->
+    (* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
+       arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
+    let pars = mib.mind_nparams in
+    let right = fapp_stack (f, s') in
+    let (depth, args, s) = strip_update_shift_app m s in
+    (** Try to drop the params, might fail on partially applied constructors. *)
+    let argss = try_drop_parameters depth pars args in
+    let hstack =
+      Array.map (fun p ->
+          { norm = Red; (* right can't be a constructor though *)
+            term = FProj (Projection.make p false, right) })
+        projs
+    in
+    argss, [Zapp hstack]
+  | None -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
@@ -669,8 +673,7 @@ let contract_fix_vect fix =
   (subs_cons(Array.init nfix make_body, env), thisbody)
 
 let unfold_projection env p =
-  let pb = lookup_projection p env in
-  Zproj (pb.proj_npars, pb.proj_arg, p)
+  Zproj (Projection.repr p)
 
 (*********************************************************************)
 (* A machine that inspects the head of a term until it finds an
@@ -748,9 +751,9 @@ let rec knr info m stk =
             let stk' = par @ append_stack [|rarg|] s in
             let (fxe,fxbd) = contract_fix_vect fx.term in
             knit info fxe fxbd stk'
-       | (depth, args, Zproj (n, m, cst)::s) ->
-	    let rargs = drop_parameters depth n args in
-	    let rarg = project_nth_arg m rargs in
+       | (depth, args, Zproj p::s) ->
+            let rargs = drop_parameters depth (Projection.Repr.npars p) args in
+            let rarg = project_nth_arg (Projection.Repr.arg p) rargs in
 	    kni info rarg s
        | (_,args,s) -> (m,args@s))
   | FCoFix _ when red_set info.i_flags fIOTA ->
diff --git a/checker/closure.mli b/checker/closure.mli
index 49b07f730d..cec785699d 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -103,7 +103,7 @@ type fterm =
 type stack_member =
   | Zapp of fconstr array
   | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * Projection.t
+  | Zproj of Projection.Repr.t
   | Zfix of fconstr * stack
   | Zshift of int
   | Zupdate of fconstr
diff --git a/checker/declarations.ml b/checker/declarations.ml
index a744a02279..0540227ccb 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -214,11 +214,7 @@ let rec map_kn f f' c =
     match c with
       | Const (kn, u) -> (try snd (f' kn u) with No_subst -> c)
       | Proj (p,t) -> 
-          let p' = 
-	    Projection.map (fun kn ->
-			    try fst (f' kn Univ.Instance.empty)
-			    with No_subst -> kn) p
-	  in
+          let p' = Projection.map f p in
 	  let t' = func t in
 	    if p' == p && t' == t then c
 	    else Proj (p', t')
@@ -495,6 +491,16 @@ let eq_recarg r1 r2 = match r1, r2 with
 
 let eq_wf_paths = Rtree.equal eq_recarg
 
+let inductive_make_projections ind mib =
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> None
+  | PrimRecord infos ->
+    let projs = Array.mapi (fun proj_arg lab ->
+        Names.Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab)
+        (pi2 infos.(snd ind))
+    in
+    Some projs
+
 (**********************************************************************)
 (* Representation of mutual inductive types in the kernel             *)
 (*
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 7458b3e0b0..ce852644ef 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -25,6 +25,9 @@ val dest_subterms : wf_paths -> wf_paths list array
 val eq_recarg : recarg -> recarg -> bool
 val eq_wf_paths : wf_paths -> wf_paths -> bool
 
+val inductive_make_projections : Names.inductive -> mutual_inductive_body ->
+  Names.Projection.Repr.t array option
+
 (* Modules *)
 
 val empty_delta_resolver : delta_resolver
diff --git a/checker/environ.ml b/checker/environ.ml
index ba1eb0ddb4..74cf237763 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,7 +7,6 @@ open Declarations
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
-  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
@@ -35,7 +34,6 @@ let empty_oracle = {
 let empty_env = {
   env_globals =
   { env_constants = Cmap_env.empty;
-    env_projections = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
     env_inductives_eq = KNmap.empty;
     env_modules = MPmap.empty;
@@ -166,9 +164,6 @@ let evaluable_constant cst env =
   try let _  = constant_value env (cst, Univ.Instance.empty) in true
   with Not_found | NotEvaluableConst _ -> false
 
-let lookup_projection p env =
-  Cmap_env.find (Projection.constant p) env.env_globals.env_projections
-
 (* Mutual Inductives *)
 let scrape_mind env kn=
   try
@@ -191,14 +186,6 @@ let add_mind kn mib env =
     Printf.ksprintf anomaly ("Inductive %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
-  let new_projections = match mib.mind_record with
-    | NotRecord | FakeRecord -> env.env_globals.env_projections
-    | PrimRecord projs ->
-      Array.fold_left (fun accu (id, kns, pbs) ->
-      Array.fold_left2 (fun accu kn pb ->
-          Cmap_env.add kn pb accu) accu kns pbs)
-        env.env_globals.env_projections projs
-  in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
     env.env_globals.env_inductives_eq
@@ -207,10 +194,22 @@ let add_mind kn mib env =
   let new_globals =
     { env.env_globals with
       env_inductives = new_inds;
-      env_projections = new_projections;
       env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
+let lookup_projection p env =
+  let mind,i = Projection.inductive p in
+  let mib = lookup_mind mind env in
+  match mib.mind_record with
+  | NotRecord | FakeRecord -> CErrors.anomaly ~label:"lookup_projection" Pp.(str "not a projection")
+  | PrimRecord infos ->
+    let _,labs,typs = infos.(i) in
+    let parg = Projection.arg p in
+    if not (Label.equal labs.(parg) (Projection.label p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect label on projection")
+    else if not (Int.equal mib.mind_nparams (Projection.npars p))
+    then CErrors.anomaly ~label:"lookup_projection" Pp.(str "incorrect param number on projection")
+    else typs.(parg)
 
 (* Modules *)
 
diff --git a/checker/environ.mli b/checker/environ.mli
index acb29d7d2d..af1b2a6228 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -5,7 +5,6 @@ open Cic
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
-  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
@@ -58,7 +57,8 @@ exception NotEvaluableConst of const_evaluation_result
 val constant_value : env -> Constant.t puniverses -> constr
 val evaluable_constant : Constant.t -> env -> bool
 
-val lookup_projection : Projection.t -> env -> projection_body
+(** NB: here in the checker we check the inferred info (npars, label) *)
+val lookup_projection : Projection.t -> env -> constr
 
 (* Inductives *)
 val mind_equiv : env -> inductive -> inductive -> bool
diff --git a/checker/reduction.ml b/checker/reduction.ml
index 16c7012138..d36c0ef2c9 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -43,7 +43,7 @@ let compare_stack_shape stk1 stk2 =
     | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2
     | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2
     | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2
-    | (Zproj (n1,m1,p1)::s1, Zproj (n2,m2,p2)::s2) ->
+    | (Zproj p1::s1, Zproj p2::s2) ->
         Int.equal bal 0 && compare_rec 0 s1 s2
     | ((ZcaseT(c1,_,_,_))::s1,
        (ZcaseT(c2,_,_,_))::s2) ->
@@ -55,7 +55,7 @@ let compare_stack_shape stk1 stk2 =
 
 type lft_constr_stack_elt =
     Zlapp of (lift * fconstr) array
-  | Zlproj of Names.Projection.t * lift
+  | Zlproj of Names.Projection.Repr.t * lift
   | Zlfix of (lift * fconstr) * lft_constr_stack
   | Zlcase of case_info * lift * fconstr * fconstr array
 and lft_constr_stack = lft_constr_stack_elt list
@@ -74,8 +74,8 @@ let pure_stack lfts stk =
             | (Zshift n,(l,pstk)) -> (el_shft n l, pstk)
             | (Zapp a, (l,pstk)) ->
                 (l,zlapp (Array.map (fun t -> (l,t)) a) pstk)
-	    | (Zproj (n,m,c), (l,pstk)) ->
-		(l, Zlproj (c,l)::pstk)
+            | (Zproj p, (l,pstk)) ->
+                (l, Zlproj (p,l)::pstk)
             | (Zfix(fx,a),(l,pstk)) ->
                 let (lfx,pa) = pure_rec l a in
                 (l, Zlfix((lfx,fx),pa)::pstk)
@@ -133,7 +133,7 @@ let convert_universes univ u u' =
   if Univ.Instance.check_eq univ u u' then ()
   else raise NotConvertible
 
-let compare_stacks f fmind lft1 stk1 lft2 stk2 =
+let compare_stacks f fmind fproj lft1 stk1 lft2 stk2 =
   let rec cmp_rec pstk1 pstk2 =
     match (pstk1,pstk2) with
       | (z1::s1, z2::s2) ->
@@ -143,10 +143,8 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 =
             | (Zlfix(fx1,a1),Zlfix(fx2,a2)) ->
                 f fx1 fx2; cmp_rec a1 a2
 	    | (Zlproj (c1,l1),Zlproj (c2,l2)) -> 
-               if not (Names.Constant.UserOrd.equal
-		       (Names.Projection.constant c1)
-		       (Names.Projection.constant c2)) then 
-		raise NotConvertible
+               if not (fproj c1 c2) then
+                raise NotConvertible
             | (Zlcase(ci1,l1,p1,br1),Zlcase(ci2,l2,p2,br2)) ->
                 if not (fmind ci1.ci_ind ci2.ci_ind) then
 		  raise NotConvertible;
@@ -257,7 +255,7 @@ let rec no_case_available = function
   | Zupdate _ :: stk -> no_case_available stk
   | Zshift _ :: stk -> no_case_available stk
   | Zapp _ :: stk -> no_case_available stk
-  | Zproj (_,_,_) :: _ -> false
+  | Zproj _ :: _ -> false
   | ZcaseT _ :: _ -> false
   | Zfix _ :: _ -> true
 
@@ -300,6 +298,10 @@ let eq_table_key univ =
       Constant.UserOrd.equal c1 c2 &&
       Univ.Instance.check_eq univ u1 u2)
 
+let proj_equiv_infos infos p1 p2 =
+  Int.equal (Projection.Repr.arg p1) (Projection.Repr.arg p2) &&
+  mind_equiv (infos_env infos) (Projection.Repr.inductive p1) (Projection.Repr.inductive p2)
+
 (* Conversion between  [lft1]term1 and [lft2]term2 *)
 let rec ccnv univ cv_pb infos lft1 lft2 term1 term2 =
   eqappr univ cv_pb infos (lft1, (term1,[])) (lft2, (term2,[]))
@@ -523,7 +525,7 @@ and eqappr univ cv_pb infos (lft1,st1) (lft2,st2) =
 and convert_stacks univ infos lft1 lft2 stk1 stk2 =
   compare_stacks
     (fun (l1,t1) (l2,t2) -> ccnv univ CONV infos l1 l2 t1 t2)
-    (mind_equiv_infos infos)
+    (mind_equiv_infos infos) (proj_equiv_infos infos)
     lft1 stk1 lft2 stk2
 
 and convert_vect univ infos lft1 lft2 v1 v2 =
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 3f7f844704..0916d98ddf 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -12,7 +12,6 @@
 open Util
 open Names
 open Cic
-open Term
 open Declarations
 open Environ
 open Reduction
@@ -123,14 +122,6 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
       env, Univ.make_abstract_instance auctx'
     | _ -> error ()
   in
-  let eq_projection_body p1 p2 =
-    let check eq f = if not (eq (f p1) (f p2)) then error () in
-    check eq_ind (fun x -> x.proj_ind);
-    check (==) (fun x -> x.proj_npars);
-    check (==) (fun x -> x.proj_arg);
-    check (eq_constr) (fun x -> x.proj_type);
-    true
-  in
   let check_inductive_type t1 t2 = check_conv conv_leq env t1 t2 in
 
   let check_packet p1 p2 =
@@ -188,9 +179,9 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
     | FakeRecord, FakeRecord -> true
     | PrimRecord info1, PrimRecord info2 ->
       let check (id1, p1, pb1) (id2, p2, pb2) =
-        Id.equal id1 id2 &&
-        Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-        Array.for_all2 eq_projection_body pb1 pb2
+        (* we don't care about the id, the types are inferred from the inductive
+           (ie checked before now) *)
+        Array.for_all2 Label.equal p1 p2
       in
       Array.equal check info1 info2
     | _, _ -> false
diff --git a/checker/typeops.ml b/checker/typeops.ml
index 19ede4b9a2..138fe8bc95 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -198,14 +198,13 @@ let judge_of_case env ci pj (c,cj) lfj =
 (* Projection. *)
 
 let judge_of_projection env p c ct =
-  let pb = lookup_projection p env in
+  let pty = lookup_projection p env in
   let (ind,u), args =
     try find_rectype env ct
     with Not_found -> error_case_not_inductive env (c, ct)
   in
-    assert(eq_ind pb.proj_ind ind);
-    let ty = subst_instance_constr u pb.proj_type in
-      substl (c :: List.rev args) ty
+  let ty = subst_instance_constr u pty in
+  substl (c :: List.rev args) ty
 
 (* Fixpoints. *)
 
diff --git a/checker/values.ml b/checker/values.ml
index 88cdb644db..e68cd18b87 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 c395aa2dbfc18794b3b7192f3dc5b2e5 checker/cic.mli
+MD5 064cd8d9651d37aebf77fb638b889cad checker/cic.mli
 
 *)
 
@@ -135,7 +135,9 @@ let v_caseinfo =
   v_tuple "case_info" [|v_ind;Int;Array Int;Array Int;v_cprint|]
 
 let v_cast = v_enum "cast_kind" 4
-let v_proj = v_tuple "projection" [|v_cst; v_bool|]
+
+let v_proj_repr = v_tuple "projection_repr" [|v_ind;Int;Int;v_id|]
+let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
 
 let rec v_constr =
   Sum ("constr",0,[|
@@ -223,10 +225,6 @@ let v_cst_def =
   v_sum "constant_def" 0
     [|[|Opt Int|]; [|v_cstr_subst|]; [|v_lazy_constr|]|]
 
-let v_projbody =
-  v_tuple "projection_body"
-    [|v_ind;Int;Int;v_constr|]
-
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle|]
 
@@ -277,7 +275,7 @@ let v_finite = v_enum "recursivity_kind" 3
 
 let v_record_info =
   v_sum "record_info" 2
-    [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
+    [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0