diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-05-25 13:38:51 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-07-06 14:38:04 +0200 |
commit | a7ed091b6842cc78f0480504e84c3cfa261860bd (patch) | |
tree | 7122a406caabadd0ed0de01044593294a990a6de | |
parent | a9010048c40c85b0f5e9c5fedaf2609121e71b89 (diff) |
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).
-rw-r--r-- | pretyping/indrec.ml | 9 | ||||
-rw-r--r-- | pretyping/indrec.mli | 7 | ||||
-rw-r--r-- | pretyping/inductiveops.ml | 5 | ||||
-rw-r--r-- | pretyping/inductiveops.mli | 5 | ||||
-rw-r--r-- | toplevel/himsg.ml | 7 | ||||
-rw-r--r-- | toplevel/indschemes.ml | 10 |
6 files changed, 31 insertions, 12 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0c80bd019..012c97549 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 f0736d2dd..192b64a5e 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 fbad0d949..64932145e 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 d25f8a837..6c49099a8 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 *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1e4c3c8f1..b3eae3765 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1147,6 +1147,11 @@ let error_not_allowed_case_analysis isrec kind i = strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) (fst i) ++ str "." +let error_not_allowed_dependent_analysis isrec i = + str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + strbrk " is not allowed for inductive definition " ++ + pr_inductive (Global.env()) i ++ str "." + let error_not_mutual_in_scheme ind ind' = if eq_ind ind ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ @@ -1178,6 +1183,8 @@ let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (isrec,k,i) -> error_not_allowed_case_analysis isrec k i | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' + | NotAllowedDependentAnalysis (isrec, i) -> + error_not_allowed_dependent_analysis isrec i (* Pattern-matching errors *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8ae2140a6..ecee2e540 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -213,18 +213,13 @@ 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 if is_primitive_record_without_eta mib then + else if Inductiveops.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 @@ -255,7 +250,7 @@ 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 primwithouteta = Inductiveops.is_primitive_record_without_eta mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> @@ -409,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort = let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in - (* let decltype = refresh_universes decltype in *) let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref |