1 files changed, 129 insertions, 25 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 97aa82e4..0fa573b9 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -51,7 +51,7 @@ let arities_of_constructors env (ind,u as indu) =
 type inductive_family = pinductive * constr list
 
 let make_ind_family (mis, params) = (mis,params)
-let dest_ind_family (mis,params) = (mis,params)
+let dest_ind_family (mis,params) : inductive_family = (mis,params)
 
 let map_ind_family f (mis,params) = (mis, List.map f params)
 
@@ -269,16 +269,14 @@ let allowed_sorts env (kn,i as ind) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_kelim
 
-let projection_nparams_env env p = 
-  let pb = lookup_projection p env in
-    pb.proj_npars
+let projection_nparams_env _ p = Projection.npars p
 
-let projection_nparams p = projection_nparams_env (Global.env ()) p
+let projection_nparams p = Projection.npars p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == BiFinite
-  | _ -> true
+  | PrimRecord _ -> mib.mind_finite == BiFinite
+  | NotRecord | FakeRecord -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
@@ -303,7 +301,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : Context.Rel.t;
+  cs_args : Constr.rel_context;
   cs_concl_realargs : constr array
 }
 
@@ -343,41 +341,39 @@ let get_constructors env (ind,params) =
   Array.init (Array.length mip.mind_consnames)
     (fun j -> get_constructor (ind,mib,mip,params) (j+1))
 
-let get_projections env (ind,params) =
-  let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
-    match mib.mind_record with
-    | Some (Some (id, projs, pbs)) -> Some projs
-    | _ -> None
+let get_projections = Environ.get_projections
 
 let make_case_or_project env sigma indf ci pred c branches =
   let open EConstr in
-  let projs = get_projections env indf in
+  let projs = get_projections env (fst (fst indf)) in
   match projs with
   | None -> (mkCase (ci, pred, c, branches))
   | Some ps ->
      assert(Array.length branches == 1);
+     let na, ty, t = destLambda sigma pred in
      let () =
-       let _, _, t = destLambda sigma pred in
        let (ind, _), _ = dest_ind_family indf in
        let mib, _ = Inductive.lookup_mind_specif env ind in
        if (* dependent *) not (Vars.noccurn sigma 1 t) &&
           not (has_dependent_elim mib) then
        user_err ~hdr:"make_case_or_project"
                     Pp.(str"Dependent case analysis not allowed" ++
-                     str" on inductive type " ++ Names.MutInd.print (fst ind))
+                     str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
      in
      let branch = branches.(0) in
      let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
-     let n, subst =
+     let n, len, ctx =
        List.fold_right
-         (fun decl (i, subst) ->
+         (fun decl (i, j, ctx) ->
           match decl with
-          | LocalAssum (na, t) ->
-             let t = mkProj (Projection.make ps.(i) true, c) in
-             (i + 1, t :: subst)
-          | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst))
-         ctx (0, [])
-     in Vars.substl subst br
+          | LocalAssum (na, ty) ->
+             let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+             (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+          | LocalDef (na, b, ty) ->
+             (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+         ctx (0, 1, [])
+     in
+     mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
 
 (* substitution in a signature *)
 
@@ -454,6 +450,110 @@ let build_branch_type env sigma dep p cs =
 
 (**************************************************)
 
+(** From a rel context describing the constructor arguments,
+    build an expansion function.
+    The term built is expecting to be substituted first by
+    a substitution of the form [params, x : ind params] *)
+let compute_projections env (kn, i as ind) =
+  let open Term in
+  let mib = Environ.lookup_mind kn env in
+  let u = match mib.mind_universes with
+  | Monomorphic_ind _ -> Instance.empty
+  | Polymorphic_ind auctx -> make_abstract_instance auctx
+  | Cumulative_ind acumi ->
+    make_abstract_instance (ACumulativityInfo.univ_context acumi)
+  in
+  let x = match mib.mind_record with
+  | NotRecord | FakeRecord ->
+    anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  | PrimRecord info-> Name (pi1 (info.(i)))
+  in
+  let pkt = mib.mind_packets.(i) in
+  let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
+  let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
+  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
+  let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
+  (** We build a substitution smashing the lets in the record parameters so
+      that typechecking projections requires just a substitution and not
+      matching with a parameter context. *)
+  let indty =
+    (* [ty] = [Ind inst] is typed in context [params] *)
+    let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+    let indu = mkIndU (ind, u) in
+    let ty = mkApp (indu, inst) in
+    (* [Ind inst] is typed in context [params-wo-let] *)
+    ty
+  in
+  let ci =
+    let print_info =
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
+      { ci_ind     = ind;
+        ci_npar    = nparamargs;
+        ci_cstr_ndecls = pkt.mind_consnrealdecls;
+        ci_cstr_nargs = pkt.mind_consnrealargs;
+        ci_pp_info = print_info }
+  in
+  let len = List.length ctx in
+  let compat_body ccl i =
+    (* [ccl] is defined in context [params;x:indty] *)
+    (* [ccl'] is defined in context [params;x:indty;x:indty] *)
+    let ccl' = liftn 1 2 ccl in
+    let p = mkLambda (x, lift 1 indty, ccl') in
+    let branch = it_mkLambda_or_LetIn (mkRel (len - i)) ctx in
+    let body = mkCase (ci, p, mkRel 1, [|lift 1 branch|]) in
+      it_mkLambda_or_LetIn (mkLambda (x,indty,body)) params
+  in
+  let projections decl (proj_arg, j, pbs, subst) =
+    match decl with
+    | LocalDef (na,c,t) ->
+        (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *)
+        let c = liftn 1 j c in
+        (* From [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)]
+           to [params, x:I |- c(params,proj1 x,..,projj x)] *)
+        let c1 = substl subst c in
+        (* From [params, x:I |- subst:field1,..,fieldj]
+           to [params, x:I |- subst:field1,..,fieldj+1] where [subst]
+           is represented with instance of field1 last *)
+        let subst = c1 :: subst in
+        (proj_arg, j+1, pbs, subst)
+    | LocalAssum (na,t) ->
+      match na with
+      | Name id ->
+        let lab = Label.of_id id in
+        let kn = Projection.Repr.make ind ~proj_npars:mib.mind_nparams ~proj_arg lab in
+        (* from [params, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj] *)
+        let t = liftn 1 j t in
+        (* from [params, x:I, field1,..,fieldj |- t(params,field1,..,fieldj)]
+           to [params-wo-let, x:I |- t(params,proj1 x,..,projj x)] *)
+        (* from [params, x:I, field1,..,fieldj |- t(field1,..,fieldj)]
+           to [params, x:I |- t(proj1 x,..,projj x)] *)
+        let ty = substl subst t in
+        let term = mkProj (Projection.make kn true, mkRel 1) in
+        let fterm = mkProj (Projection.make kn false, mkRel 1) in
+        let compat = compat_body ty (j - 1) in
+        let etab = it_mkLambda_or_LetIn (mkLambda (x, indty, term)) params in
+        let etat = it_mkProd_or_LetIn (mkProd (x, indty, ty)) params in
+        let body = (etab, etat, compat) in
+        (proj_arg + 1, j + 1, body :: pbs, fterm :: subst)
+      | Anonymous ->
+        anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
+  in
+  let (_, _, pbs, subst) =
+    List.fold_right projections ctx (0, 1, [], [])
+  in
+  Array.rev_of_list pbs
+
+let legacy_match_projection env ind =
+  Array.map pi3 (compute_projections env ind)
+
+let compute_projections ind mib =
+  let ans = compute_projections ind mib in
+  Array.map (fun (prj, ty, _) -> (prj, ty)) ans
+
+(**************************************************)
+
 let extract_mrectype sigma t =
   let open EConstr in
   let (t, l) = decompose_app sigma t in
@@ -629,6 +729,10 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
         env evdref scl ar.template_level (ctx,ar.template_param_levels) in
       !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
+let type_of_projection_constant env (p,u) =
+  let pty = lookup_projection p env in
+  Vars.subst_instance_constr u pty
+
 let type_of_projection_knowing_arg env sigma p c ty =
   let c = EConstr.Unsafe.to_constr c in
   let IndType(pars,realargs) =
@@ -637,7 +741,7 @@ let type_of_projection_knowing_arg env sigma p c ty =
       raise (Invalid_argument "type_of_projection_knowing_arg_type: not an inductive type")
   in
   let (_,u), pars = dest_ind_family pars in
-  substl (c :: List.rev pars) (Typeops.type_of_projection_constant env (p,u))
+  substl (c :: List.rev pars) (type_of_projection_constant env (p,u))
 
 (***********************************************)
 (* Guard condition *)