diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 32 |
1 files changed, 20 insertions, 12 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 66cd4cba9e..8b8295c64b 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -194,7 +194,11 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = +let relevance_of_inductive env ind = + let _, mip = lookup_mind_specif env ind in + mip.mind_relevant + +let type_of_inductive_gen ?(polyprop=true) env ((_,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -301,12 +305,12 @@ let build_dependent_inductive ind (_,mip) params = @ Context.Rel.to_extended_list mkRel 0 realargs) (* This exception is local *) -exception LocalArity of (Sorts.family * Sorts.family * arity_error) option +exception LocalArity of (Sorts.family list * Sorts.family * Sorts.family * arity_error) option let check_allowed_sort ksort specif = if not (CList.exists (Sorts.family_equal ksort) (elim_sorts specif)) then let s = inductive_sort_family (snd specif) in - raise (LocalArity (Some(ksort,s,error_elim_explain ksort s))) + raise (LocalArity (Some(elim_sorts specif, ksort,s,error_elim_explain ksort s))) let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in @@ -320,7 +324,7 @@ let is_correct_arity env c pj ind specif params = srec (push_rel (LocalAssum (na1,a1)) env) t ar' (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) - let env' = push_rel (LocalAssum (na1,a1)) env in + let env' = push_rel (LocalAssum (na1,a1)) env in let ksort = match kind (whd_all env' a2) with | Sort s -> Sorts.family s | _ -> raise (LocalArity None) in @@ -336,7 +340,7 @@ let is_correct_arity env c pj ind specif params = in try srec env pj.uj_type (List.rev arsign) with LocalArity kinds -> - error_elim_arity env ind (elim_sorts specif) c pj kinds + error_elim_arity env ind c pj kinds (************************************************************************) @@ -379,13 +383,14 @@ let type_case_branches env (pind,largs) pj c = (************************************************************************) (* Checking the case annotation is relevant *) -let check_case_info env (indsp,u) ci = +let check_case_info env (indsp,u) r ci = let (mib,mip as spec) = lookup_mind_specif env indsp in if not (eq_ind indsp ci.ci_ind) || not (Int.equal mib.mind_nparams ci.ci_npar) || not (Array.equal Int.equal mip.mind_consnrealdecls ci.ci_cstr_ndecls) || not (Array.equal Int.equal mip.mind_consnrealargs ci.ci_cstr_nargs) || + not (ci.ci_relevance == r) || is_primitive_record spec then raise (TypeError(env,WrongCaseInfo((indsp,u),ci))) @@ -574,7 +579,9 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let mib = Environ.lookup_mind mind env in let ntypes = mib.mind_ntypes in let push_ind specif env = - let decl = LocalAssum (Anonymous, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in + let r = specif.mind_relevant in + let anon = Context.make_annot Anonymous r in + let decl = LocalAssum (anon, hnf_prod_applist env (type_of_inductive env ((mib,specif),u)) lpar) in push_rel decl env in let env = Array.fold_right push_ind mib.mind_packets env in @@ -595,7 +602,8 @@ let rec ienv_decompose_prod (env,_ as ienv) n c = let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0)) let dummy_implicit_sort = mkType (Universe.make dummy_univ) let lambda_implicit_lift n a = - let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in + let anon = Context.make_annot Anonymous Sorts.Relevant in + let lambda_implicit a = mkLambda (anon, dummy_implicit_sort, a) in iterate lambda_implicit n (lift n a) (* This removes global parameters of the inductive types in lc (for @@ -1021,7 +1029,7 @@ let check_one_fix renv recpos trees def = check_rec_call (assign_var_spec renv (1,recArgsDecrArg)) [] body else match kind body with - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> check_rec_call renv [] a; let renv' = push_var_renv renv (x,a) in check_nested_fix_body renv' (decr-1) recArgsDecrArg b @@ -1054,7 +1062,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = match kind (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then - let env' = push_rel (LocalAssum (x,a)) env in + let env' = push_rel (LocalAssum (x,a)) env in if Int.equal n (k + 1) then (* get the inductive type of the fixpoint *) let (mind, _) = @@ -1111,7 +1119,7 @@ let rec codomain_is_coind env c = let b = whd_all env c in match kind b with | Prod (x,a,b) -> - codomain_is_coind (push_rel (LocalAssum (x,a)) env) b + codomain_is_coind (push_rel (LocalAssum (x,a)) env) b | _ -> (try find_coinductive env b with Not_found -> @@ -1149,7 +1157,7 @@ let check_one_cofix env nbfix def deftype = | _ -> anomaly_ill_typed () in process_args_of_constr (realargs, lra) - | Lambda (x,a,b) -> + | Lambda (x,a,b) -> let () = assert (List.is_empty args) in if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in |