diff options
| -rw-r--r-- | printing/prettyp.ml | 8 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 2 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 24 |
4 files changed, 31 insertions, 7 deletions
diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f6e99c7e..f71719cb9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -224,12 +224,12 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () - | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index de2818902..99c2d8210 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -95,6 +95,10 @@ let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index c36797059..77f927f2d 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -13,9 +13,11 @@ open Ind_tables val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind +val rect_scheme_kind_from_type : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind +val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind 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; |