From a9010048c40c85b0f5e9c5fedaf2609121e71b89 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau <mattam@mattam.org>
Date: Tue, 24 May 2016 20:32:35 +0200
Subject: primproj: warning and avoid error.

When defining a (co)recursive inductive with primitive projections on,
which lacks eta-conversion and hence dependent elimination, build only
the associated non-dependent elimination principles, and warn about
this. Also make the printing of the status of an inductive
w.r.t. projections and eta conversion explicit in Print and About.
---
 toplevel/indschemes.ml | 24 +++++++++++++++++++++---
 1 file changed, 21 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 32e0eb53b..8ae2140a6 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -213,11 +213,20 @@ let try_declare_beq_scheme kn =
 
 let declare_beq_scheme = declare_beq_scheme_with []
 
+let is_primitive_record_without_eta mib =
+  match mib.mind_record with
+  | Some (Some _) -> mib.mind_finite <> BiFinite
+  | _ -> false
+
 (* Case analysis schemes *)
 let declare_one_case_analysis_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
-  let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in
+  let dep =
+    if kind == InProp then case_scheme_kind_from_prop
+    else if is_primitive_record_without_eta mib then
+      case_scheme_kind_from_type
+    else case_dep_scheme_kind_from_type in
   let kelim = elim_sorts (mib,mip) in
     (* in case the inductive has a type elimination, generates only one
        induction scheme, the other ones share the same code with the
@@ -237,15 +246,23 @@ let kinds_from_type =
    InProp,ind_dep_scheme_kind_from_type;
    InSet,rec_dep_scheme_kind_from_type]
 
+let nondep_kinds_from_type =
+  [InType,rect_scheme_kind_from_type;
+   InProp,ind_scheme_kind_from_type;
+   InSet,rec_scheme_kind_from_type]
+
 let declare_one_induction_scheme ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let kind = inductive_sort_family mip in
   let from_prop = kind == InProp in
+  let primwithouteta = is_primitive_record_without_eta mib in
   let kelim = elim_sorts (mib,mip) in
   let elims =
     List.map_filter (fun (sort,kind) ->
       if Sorts.List.mem sort kelim then Some kind else None)
-      (if from_prop then kinds_from_prop else kinds_from_type) in
+      (if from_prop then kinds_from_prop
+       else if primwithouteta then nondep_kinds_from_type
+       else kinds_from_type) in
   List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
     elims
 
@@ -502,7 +519,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
 let declare_default_schemes kn =
   let mib = Global.lookup_mind kn in
   let n = Array.length mib.mind_packets in
-  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+     && mib.mind_typing_flags.check_guarded then
     declare_induction_schemes kn;
   if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
   if is_eq_flag() then try_declare_beq_scheme kn;
-- 
cgit v1.2.3