From a7ed091b6842cc78f0480504e84c3cfa261860bd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 13:38:51 +0200
Subject: Move is_prim... to Inductiveops and correct Scheme

Now scheme will not try to build ill-typed dependent analyses
on recursive records with primitive projections but report
a proper error.

Minor change of the API (adding one error case to recursion_scheme_error).
---
 pretyping/indrec.ml        | 9 ++++++++-
 pretyping/indrec.mli       | 7 +++++--
 pretyping/inductiveops.ml  | 5 +++++
 pretyping/inductiveops.mli | 5 ++++-
 4 files changed, 22 insertions(+), 4 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 0c80bd0193..012c975498 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -36,6 +36,7 @@ type dep_flag = bool
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
   | NotMutualInScheme of inductive * inductive
+  | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -483,6 +484,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 let build_case_analysis_scheme env sigma pity dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
+  if dep && Inductiveops.is_primitive_record_without_eta mib then
+    raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 let is_in_prop mip =
@@ -492,7 +495,7 @@ let is_in_prop mip =
 
 let build_case_analysis_scheme_default env sigma pity kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  let dep = not (is_in_prop mip) in
+  let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 (**********************************************************************)
@@ -553,6 +556,8 @@ let check_arities env listdepkind =
 let build_mutual_induction_scheme env sigma = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
+      if dep && Inductiveops.is_primitive_record_without_eta mib then
+        raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
       let (sp,tyi) = mind in
       let listdepkind =
 	((mind,u),mib,mip,dep,s)::
@@ -572,6 +577,8 @@ let build_mutual_induction_scheme env sigma = function
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
+  if dep && Inductiveops.is_primitive_record_without_eta mib then
+    raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
   let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
     sigma, List.hd l
 
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index f0736d2dda..192b64a5ed 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -16,6 +16,7 @@ open Evd
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive
   | NotMutualInScheme of inductive * inductive
+  | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive
 
 exception RecursionSchemeError of recursion_scheme_error
 
@@ -28,13 +29,15 @@ type dep_flag = bool
 val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive ->
       dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma
 
-(** Build a dependent case elimination predicate unless type is in Prop *)
+(** Build a dependent case elimination predicate unless type is in Prop
+   or is a recursive record with primitive projections. *)
 
 val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive ->
       sorts_family -> (constr, 'r) Sigma.sigma
 
 (** Builds a recursive induction scheme (Peano-induction style) in the same
-   sort family as the inductive family; it is dependent if not in Prop *)
+   sort family as the inductive family; it is dependent if not in Prop
+   or a recursive record with primitive projections.  *)
 
 val build_induction_scheme : env -> evar_map -> pinductive ->
       dep_flag -> sorts_family -> evar_map * constr
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index fbad0d949d..64932145e1 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,6 +269,11 @@ let projection_nparams_env env p =
 
 let projection_nparams p = projection_nparams_env (Global.env ()) p
 
+let is_primitive_record_without_eta mib =
+  match mib.mind_record with
+  | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite
+  | _ -> false
+
 (* Annotation for cases *)
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index d25f8a8378..6c49099a8f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -126,7 +126,10 @@ val allowed_sorts : env -> inductive -> sorts_family list
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
-  constr -> types -> types
+				     constr -> types -> types
+
+(** Recursive records with primitive projections do not have eta-conversion *)
+val is_primitive_record_without_eta : mutual_inductive_body -> bool
 
 (** Extract information from an inductive family *)
 
-- 
cgit v1.2.3


From f77c2b488ca552b2316d4ebab1c051cb5a1347ab Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 13:49:50 +0200
Subject: Renaming to more generic has_dependent_elim test

---
 pretyping/indrec.ml        | 8 ++++----
 pretyping/inductiveops.ml  | 6 +++---
 pretyping/inductiveops.mli | 6 ++++--
 3 files changed, 11 insertions(+), 9 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 012c975498..45eaae1244 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -484,7 +484,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 let build_case_analysis_scheme env sigma pity dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity)));
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
@@ -495,7 +495,7 @@ let is_in_prop mip =
 
 let build_case_analysis_scheme_default env sigma pity kind =
   let (mib,mip) = lookup_mind_specif env (fst pity) in
-  let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in
+  let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in
   mis_make_case_com dep env sigma pity (mib,mip) kind
 
 (**********************************************************************)
@@ -556,7 +556,7 @@ let check_arities env listdepkind =
 let build_mutual_induction_scheme env sigma = function
   | ((mind,u),dep,s)::lrecspec ->
       let (mib,mip) = lookup_mind_specif env mind in
-      if dep && Inductiveops.is_primitive_record_without_eta mib then
+      if dep && not (Inductiveops.has_dependent_elim mib) then
         raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind)));
       let (sp,tyi) = mind in
       let listdepkind =
@@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function
 
 let build_induction_scheme env sigma pind dep kind =
   let (mib,mip) = lookup_mind_specif env (fst pind) in
-  if dep && Inductiveops.is_primitive_record_without_eta mib then
+  if dep && not (Inductiveops.has_dependent_elim mib) then
     raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind)));
   let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in
     sigma, List.hd l
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 64932145e1..e4f98e7301 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -269,10 +269,10 @@ let projection_nparams_env env p =
 
 let projection_nparams p = projection_nparams_env (Global.env ()) p
 
-let is_primitive_record_without_eta mib =
+let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite
-  | _ -> false
+  | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite
+  | _ -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 6c49099a8f..7ef848f0de 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -122,14 +122,16 @@ val inductive_has_local_defs : inductive -> bool
 
 val allowed_sorts : env -> inductive -> sorts_family list
 
+(** (Co)Inductive records with primitive projections do not have eta-conversion,
+    hence no dependent elimination. *)
+val has_dependent_elim : mutual_inductive_body -> bool
+
 (** Primitive projections *)
 val projection_nparams : projection -> int
 val projection_nparams_env : env -> projection -> int
 val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 				     constr -> types -> types
 
-(** Recursive records with primitive projections do not have eta-conversion *)
-val is_primitive_record_without_eta : mutual_inductive_body -> bool
 
 (** Extract information from an inductive family *)
 
-- 
cgit v1.2.3


From f8a5cb590352a617de38fdd8ba5ffff7691d9841 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 May 2016 15:17:28 +0200
Subject: Disallow dependent case on prim records w/o eta

---
 pretyping/cases.ml         | 12 +++---------
 pretyping/indrec.ml        | 25 ++++---------------------
 pretyping/inductiveops.ml  | 29 +++++++++++++++++++++++++++++
 pretyping/inductiveops.mli |  8 ++++++++
 4 files changed, 44 insertions(+), 30 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 985ad4b0d3..447a4c487c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
 
 *)
 
-let mk_case pb (ci,pred,c,brs) =
-  let mib = lookup_mind (fst ci.ci_ind) pb.env in
-    match mib.mind_record with
-    | Some (Some (_, cs, pbs)) ->
-      Reduction.beta_appvect brs.(0) 
-	(Array.map (fun p -> mkProj (Projection.make p true, c)) cs)
-    | _ -> mkCase (ci,pred,c,brs)
-
 (**********************************************************************)
 (* Main compiling descent *)
 let rec compile pb =
@@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) =
 	      pred current indt (names,dep) tomatch in
 	  let ci = make_case_info pb.env (fst mind) pb.casestyle in
 	  let pred = nf_betaiota !(pb.evdref) pred in
-	  let case = mk_case pb (ci,pred,current,brvals) in
+	  let case =
+	    make_case_or_project pb.env indf ci pred current brvals
+	  in
 	  Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred;
 	  { uj_val = applist (case, inst);
 	    uj_type = prod_applist typ inst }
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 45eaae1244..39aeb41f77 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -43,6 +43,7 @@ exception RecursionSchemeError of recursion_scheme_error
 let make_prod_dep dep env = if dep then mkProd_name env else mkProd
 let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c)
 
+
 (*******************************************)
 (* Building curryfied elimination          *)
 (*******************************************)
@@ -376,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 		      (Anonymous,depind',concl))
 		  arsign'
 	      in
-	      let obj = 
-		let projs = get_projections env indf in
-		  match projs with
-		  | None -> (mkCase (ci, pred,
-				     mkRel 1,
-				     branches))
-		  | Some ps -> 
-		    let branch = branches.(0) in
-		    let ctx, br = decompose_lam_assum branch in
-		    let n, subst = 
-		      List.fold_right (fun decl (i, subst) ->
-			match decl with
-			| LocalAssum (na,t) ->
-			    let t = mkProj (Projection.make ps.(i) true, mkRel 1) in
-			    i + 1, t :: subst
-			| LocalDef (na,b,t) ->
-			    i, mkRel 0 :: subst)
-			ctx (0, [])
-		    in
-		    let term = substl subst br in
-		      term
+	      let obj =
+		Inductiveops.make_case_or_project env indf ci pred
+						  (mkRel 1) branches
 	      in
 		it_mkLambda_or_LetIn_name env obj
 		  (Termops.lift_rel_context nrec deparsign)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index e4f98e7301..3fbed4b252 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -343,6 +343,35 @@ let get_projections env (ind,params) =
     | Some (Some (id, projs, pbs)) -> Some projs
     | _ -> None
 
+let make_case_or_project env indf ci pred c branches =
+  let projs = get_projections env indf in
+  match projs with
+  | None -> (mkCase (ci, pred, c, branches))
+  | Some ps ->
+     assert(Array.length branches == 1);
+     let () =
+       let _, _, t = destLambda pred in
+       let (ind, _), _ = dest_ind_family indf in
+       let mib, _ = Inductive.lookup_mind_specif env ind in
+       if (* dependent *) not (noccurn 1 t) &&
+          not (has_dependent_elim mib) then
+       errorlabstrm "make_case_or_project"
+		    Pp.(str"Dependent case analysis not allowed" ++
+		     str" on inductive type " ++ Names.MutInd.print (fst ind))
+     in
+     let branch = branches.(0) in
+     let ctx, br = decompose_lam_assum branch in
+     let n, subst =
+       List.fold_right
+         (fun decl (i, subst) ->
+	  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, substl subst b :: subst))
+	 ctx (0, [])
+     in substl subst br
+
 (* substitution in a signature *)
 
 let substnl_rel_context subst n sign =
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 7ef848f0de..7bd616591f 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -180,6 +180,14 @@ val type_case_branches_with_names :
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
 
+(** Make a case or substitute projections if the inductive type is a record
+    with primitive projections.
+    Fail with an error if the elimination is dependent while the
+    inductive type does not allow dependent elimination. *)
+val make_case_or_project :
+  env -> inductive_family -> case_info ->
+  (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr
+
 (*i Compatibility
 val make_default_case_info : env -> case_style -> inductive -> case_info
 i*)
-- 
cgit v1.2.3


From df24a81b255190493281ffdeeef36754b076e9cd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 4 Jul 2016 14:36:31 +0200
Subject: Fix reopened bug #3317.

---
 pretyping/inductiveops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 3fbed4b252..214e19fecf 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -360,7 +360,7 @@ let make_case_or_project env indf ci pred c branches =
 		     str" on inductive type " ++ Names.MutInd.print (fst ind))
      in
      let branch = branches.(0) in
-     let ctx, br = decompose_lam_assum branch in
+     let ctx, br = decompose_lam_n_assum (Array.length ps) branch in
      let n, subst =
        List.fold_right
          (fun decl (i, subst) ->
-- 
cgit v1.2.3