diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 29 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 2 | ||||
| -rw-r--r-- | pretyping/reductionops.mli | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 11 | ||||
| -rw-r--r-- | pretyping/typing.mli | 6 |
6 files changed, 37 insertions, 19 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 121d7dcc1b..b104db0267 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -947,7 +947,7 @@ let specialize_predicate newtomatchs (names,(depna,_)) arsign cs tms ccl = snd (List.fold_left (expand_arg tms) (1,ccl''') newtomatchs) let find_predicate loc env evdref p current (IndType (indf,realargs)) dep tms = - let pred= abstract_predicate env !evdref indf current dep tms p in + let pred = abstract_predicate env !evdref indf current dep tms p in (pred, whd_betaiota !evdref (applist (pred, realargs@[current]))) @@ -1169,7 +1169,9 @@ and match_current pb tomatch = find_predicate pb.caseloc pb.env pb.evdref pb.pred current indt (names,dep) pb.tomatch in let ci = make_case_info pb.env mind pb.casestyle in - let case = mkCase (ci,nf_betaiota Evd.empty pred,current,brvals) in + let pred = nf_betaiota !(pb.evdref) pred in + let case = mkCase (ci,pred,current,brvals) in + Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; let inst = List.map mkRel deps in { uj_val = applist (case, inst); uj_type = substl inst typ } diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 69ee8d0290..7762d18f65 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -559,10 +559,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct let fj = pretype (mk_tycon fty) env_f evdref lvar d in let f = it_mkLambda_or_LetIn fj.uj_val fsign in let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) in - { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind LetStyle in + Typing.check_allowed_sort env !evdref ind cj.uj_val p; + mkCase (ci, p, cj.uj_val,[|f|]) in + { uj_val = v; uj_type = substl (realargs@[cj.uj_val]) ccl } | None -> let tycon = lift_tycon cs.cs_nargs tycon in @@ -578,9 +579,10 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ccl = refresh_universes ccl in let p = it_mkLambda_or_LetIn (lift (nar+1) ccl) psign in let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis LetStyle in - mkCase (ci, p, cj.uj_val,[|f|]) + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind LetStyle in + Typing.check_allowed_sort env !evdref ind cj.uj_val p; + mkCase (ci, p, cj.uj_val,[|f|]) in { uj_val = v; uj_type = ccl }) | GIf (loc,c,(na,po),b1,b2) -> @@ -611,10 +613,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ccl = nf_evar !evdref pj.utj_val in let pred = it_mkLambda_or_LetIn ccl psign in let typ = lift (- nar) (beta_applist (pred,[cj.uj_val])) in - let jtyp = inh_conv_coerce_to_tycon loc env evdref {uj_val = pred; - uj_type = typ} tycon - in - jtyp.uj_val, jtyp.uj_type + pred, typ | None -> let p = match tycon with | Some (None, ty) -> ty @@ -644,9 +643,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct let b1 = f cstrs.(0) b1 in let b2 = f cstrs.(1) b2 in let v = - let mis,_ = dest_ind_family indf in - let ci = make_case_info env mis IfStyle in - mkCase (ci, pred, cj.uj_val, [|b1;b2|]) + let ind,_ = dest_ind_family indf in + let ci = make_case_info env ind IfStyle in + let pred = nf_evar !evdref pred in + Typing.check_allowed_sort env !evdref ind cj.uj_val pred; + mkCase (ci, pred, cj.uj_val, [|b1;b2|]) in { uj_val = v; uj_type = p } diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 834c27969e..e8acd67caf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -770,7 +770,7 @@ let splay_arity env sigma c = | Sort s -> l,s | _ -> invalid_arg "splay_arity" -let sort_of_arity env c = snd (splay_arity env Evd.empty c) +let sort_of_arity env sigma c = snd (splay_arity env sigma c) let splay_prod_n env sigma n = let rec decrec env m ln c = if m = 0 then (ln,c) else diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 1a90b23f21..3ffc587ef8 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -152,7 +152,7 @@ val hnf_lam_applist : env -> evar_map -> constr -> constr list -> constr val splay_prod : env -> evar_map -> constr -> (name * constr) list * constr val splay_lam : env -> evar_map -> constr -> (name * constr) list * constr val splay_arity : env -> evar_map -> constr -> (name * constr) list * sorts -val sort_of_arity : env -> constr -> sorts +val sort_of_arity : env -> evar_map -> constr -> sorts val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr val splay_prod_assum : diff --git a/pretyping/typing.ml b/pretyping/typing.ml index b40605f228..85abe2569b 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -68,6 +68,16 @@ let e_judge_of_case env evdref ci pj cj lfj = { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } +let check_allowed_sort env sigma ind c p = + let pj = Retyping.get_judgment_of env sigma p in + let ksort = family_of_sort (sort_of_arity env sigma pj.uj_type) in + let specif = Global.lookup_inductive ind in + let sorts = elim_sorts specif in + if not (List.exists ((=) ksort) sorts) then + let s = inductive_sort_family (snd specif) in + error_elim_arity env ind sorts c pj + (Some(ksort,s,error_elim_explain ksort s)) + let e_judge_of_cast env evdref cj k tj = let expected_type = tj.utj_val in if not (Evarconv.e_cumul env evdref cj.uj_type expected_type) then @@ -218,4 +228,3 @@ let solve_evars env evd c = let c = (execute env evdref c).uj_val in (* side-effect on evdref *) nf_evar !evdref c - diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 1e75d375d9..e2fd6a9d84 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Names open Term open Environ open Evd @@ -27,3 +28,8 @@ val meta_type : evar_map -> metavariable -> types (** Solve existential variables using typing *) val solve_evars : env -> evar_map -> constr -> constr + +(** Raise an error message if incorrect elimination for this inductive *) +(** (first constr is term to match, second is return predicate) *) +val check_allowed_sort : env -> evar_map -> inductive -> constr -> constr -> + unit |