diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/detyping.ml | 14 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 14 | ||||
| -rw-r--r-- | pretyping/glob_ops.ml | 10 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 146 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 9 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.ml | 224 | ||||
| -rw-r--r-- | pretyping/inferCumulativity.mli | 10 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 27 | ||||
| -rw-r--r-- | pretyping/reductionops.ml | 80 | ||||
| -rw-r--r-- | pretyping/typing.mli | 1 | ||||
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
14 files changed, 321 insertions, 229 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 23993243f4..754e881398 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -581,12 +581,7 @@ and detype_r d flags avoid env sigma t = | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = - let pb = Environ.lookup_projection p (snd env) in - let pars = pb.Declarations.proj_npars in - let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in - let args = List.make pars hole in - GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), - (args @ [detype d flags avoid env sigma c])) + GProj (p, detype d flags avoid env sigma c) in if fst flags || !Flags.in_debugger || !Flags.in_toplevel then try noparams () @@ -1002,6 +997,13 @@ let rec subst_glob_constr subst = DAst.map (function let r1' = subst_glob_constr subst r1 in let k' = Miscops.smartmap_cast_type (subst_glob_constr subst) k in if r1' == r1 && k' == k then raw else GCast (r1',k') + + | GProj (p,c) as raw -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_glob_constr subst c in + if kn' == kn && c' == c then raw else GProj(Projection.make kn' b, c') ) (* Utilities to transform kernel cases to simple pattern-matching problem *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 41c4616f79..dc3acbc3e2 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -353,19 +353,7 @@ let exact_ise_stack2 env evd f sk1 sk2 = let check_leq_inductives evd cumi u u' = let u = EConstr.EInstance.kind evd u in let u' = EConstr.EInstance.kind evd u' in - let length_ind_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi) - in - let ind_sbcst = Univ.ACumulativityInfo.subtyp_context cumi in - if not ((length_ind_instance = Univ.Instance.length u) && - (length_ind_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - begin - let comp_subst = (Univ.Instance.append u u') in - let comp_cst = Univ.AUContext.instantiate comp_subst ind_sbcst in - Evd.add_constraints evd comp_cst - end + Evd.add_constraints evd (Reduction.get_cumulativity_constraints CUMUL cumi u u') let rec evar_conv_x ts env evd pbty term1 term2 = let term1 = whd_head_evar evd term1 in diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 093f1f0b68..a21137a05c 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -133,8 +133,10 @@ let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with Miscops.intro_pattern_naming_eq nam1 nam2 | GCast (c1, t1), GCast (c2, t2) -> f c1 c2 && cast_type_eq f t1 t2 + | GProj (p1, t1), GProj (p2, t2) -> + Projection.equal p1 p2 && f t1 t2 | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | - GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _), _ -> false + GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ | GCast _ | GProj _), _ -> false let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c @@ -180,6 +182,8 @@ let map_glob_constr_left_to_right f = DAst.map (function let comp1 = f c in let comp2 = Miscops.map_cast_type f k in GCast (comp1,comp2) + | GProj (p,c) -> + GProj (p, f c) | (GVar _ | GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) as x -> x ) @@ -212,6 +216,8 @@ let fold_glob_constr f acc = DAst.with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f acc t | CastCoerce -> acc in f acc c + | GProj(_,c) -> + f acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc ) @@ -253,6 +259,8 @@ let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function let acc = match k with | CastConv t | CastVM t | CastNative t -> f v acc t | CastCoerce -> acc in f v acc c + | GProj(_,c) -> + f v acc c | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> acc)) let iter_glob_constr f = fold_glob_constr (fun () -> f) () diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 78e6bc6f14..275a079d5d 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -84,7 +84,7 @@ let mis_is_recursive_subset listind rarg = List.exists (fun ra -> match dest_recarg ra with - | Mrec (_,i) -> Int.List.mem i listind + | Mrec (_,i) -> Int.List.mem i listind | _ -> false) rvec in Array.exists one_is_rec (dest_subterms rarg) @@ -361,20 +361,20 @@ let make_case_or_project env sigma indf ci pred c branches = if (* dependent *) not (Vars.noccurn sigma 1 t) && not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" - Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na, t) -> - let t = mkProj (Projection.make ps.(i) true, c) in - (i + 1, t :: subst) - | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) - ctx (0, []) + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, Vars.substl subst b :: subst)) + ctx (0, []) in Vars.substl subst br (* substitution in a signature *) @@ -511,25 +511,25 @@ let is_predicate_explicitly_dep env sigma pred arsign = let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> - srec (push_rel_assum (na, t) env) b arsign + srec (push_rel_assum (na, t) env) b arsign | Lambda (na,_,t), _ -> (* The following code has an impact on the introduction names - given by the tactics "case" and "inversion": when the - elimination is not dependent, "case" uses Anonymous for - inductive types in Prop and names created by mkProd_name for - inductive types in Set/Type while "inversion" uses anonymous - for inductive types both in Prop and Set/Type !! - - Previously, whether names were created or not relied on - whether the predicate created in Indrec.make_case_com had a - dependent arity or not. To avoid different predicates - printed the same in v8, all predicates built in indrec.ml - got a dependent arity (Aug 2004). The new way to decide - whether names have to be created or not is to use an - Anonymous or Named variable to enforce the expected - dependency status (of course, Anonymous implies non - dependent, but not conversely). + given by the tactics "case" and "inversion": when the + elimination is not dependent, "case" uses Anonymous for + inductive types in Prop and names created by mkProd_name for + inductive types in Set/Type while "inversion" uses anonymous + for inductive types both in Prop and Set/Type !! + + Previously, whether names were created or not relied on + whether the predicate created in Indrec.make_case_com had a + dependent arity or not. To avoid different predicates + printed the same in v8, all predicates built in indrec.ml + got a dependent arity (Aug 2004). The new way to decide + whether names have to be created or not is to use an + Anonymous or Named variable to enforce the expected + dependency status (of course, Anonymous implies non + dependent, but not conversely). From Coq > 8.2, using or not the the effective dependency of the predicate is parametrable! *) @@ -600,15 +600,15 @@ let rec instantiate_universes env evdref scl is = function let ctx,_ = Reduction.dest_arity env ty in let u = Univ.Universe.make l in let s = - (* Does the sort of parameter [u] appear in (or equal) + (* Does the sort of parameter [u] appear in (or equal) the sort of inductive [is] ? *) if univ_level_mem l is then scl (* constrained sort: replace by scl *) else (* unconstrained sort: replace by fresh universe *) let evm, s = Evd.new_sort_variable Evd.univ_flexible !evdref in - let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in - evdref := evm; s + let evm = Evd.set_leq_sort env evm s (Sorts.sort_of_univ u) in + evdref := evm; s in (LocalAssum (na,mkArity(ctx,s))) :: instantiate_universes env evdref scl is (sign, exp) | sign, [] -> sign (* Uniform parameters are exhausted *) @@ -656,93 +656,3 @@ let control_only_guard env c = iter_constr_with_full_binders push_rel iter env c in iter env c - -(* inference of subtyping condition for inductive types *) - -let infer_inductive_subtyping_arity_constructor - (env, evd, csts) (subst : constr -> constr) (arcn : types) is_arity (params : Context.Rel.t) = - let numchecked = ref 0 in - let numparams = Context.Rel.nhyps params in - let update_contexts (env, evd, csts) csts' = - (Environ.add_constraints csts' env, Evd.add_constraints evd csts', Univ.Constraint.union csts csts') - in - let basic_check (env, evd, csts) tp = - let result = - if !numchecked >= numparams then - let csts' = - Reduction.infer_conv_leq ~evars:(Evd.existential_opt_value evd) env (Evd.universes evd) tp (subst tp) - in update_contexts (env, evd, csts) csts' - else - (env, evd, csts) - in - numchecked := !numchecked + 1; result - in - let infer_typ typ ctxs = - match typ with - | LocalAssum (_, typ') -> - begin - try - let (env, evd, csts) = basic_check ctxs typ' in (Environ.push_rel typ env, evd, csts) - with Reduction.NotConvertible -> - anomaly ~label:"inference of record/inductive subtyping relation failed" - (Pp.str "Can't infer subtyping for record/inductive type") - end - | _ -> anomaly (Pp.str "") - in - let arcn' = Term.it_mkProd_or_LetIn arcn params in - let typs, codom = Reduction.dest_prod env arcn' in - let last_contexts = Context.Rel.fold_outside infer_typ typs ~init:(env, evd, csts) in - if not is_arity then basic_check last_contexts codom else last_contexts - -let infer_inductive_subtyping env evd mind_ent = - let { Entries.mind_entry_params = params; - Entries.mind_entry_inds = entries; - Entries.mind_entry_universes = ground_univs; - } = mind_ent - in - let uinfind = - match ground_univs with - | Entries.Monomorphic_ind_entry _ - | Entries.Polymorphic_ind_entry _ -> ground_univs - | Entries.Cumulative_ind_entry cumi -> - begin - let uctx = Univ.CumulativityInfo.univ_context cumi in - let sbsubst = Univ.CumulativityInfo.subtyping_susbst cumi in - let dosubst = subst_univs_level_constr sbsubst in - let instance_other = - Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) - in - let constraints_other = - Univ.subst_univs_level_constraints - sbsubst (Univ.UContext.constraints uctx) - in - let uctx_other = Univ.UContext.make (instance_other, constraints_other) in - let env = Environ.push_context uctx env in - let env = Environ.push_context uctx_other env in - let evd = - Evd.merge_universe_context - evd (UState.of_context_set (Univ.ContextSet.of_context uctx_other)) - in - let (_, _, subtyp_constraints) = - List.fold_left - (fun ctxs indentry -> - let _, params = Typeops.infer_local_decls env params in - let ctxs' = infer_inductive_subtyping_arity_constructor - ctxs dosubst indentry.Entries.mind_entry_arity true params - in - List.fold_left - (fun ctxs cons -> - infer_inductive_subtyping_arity_constructor - ctxs dosubst cons false params - ) - ctxs' indentry.Entries.mind_entry_lc - ) (env, evd, Univ.Constraint.empty) entries - in - Entries.Cumulative_ind_entry - (Univ.CumulativityInfo.make - (Univ.CumulativityInfo.univ_context cumi, - Univ.UContext.make - (Univ.UContext.instance (Univ.CumulativityInfo.subtyp_context cumi), - subtyp_constraints))) - end - in {mind_ent with Entries.mind_entry_universes = uinfind;} diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 58b1ce6c3f..55149552aa 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -199,12 +199,3 @@ val type_of_inductive_knowing_conclusion : (********************) val control_only_guard : env -> types -> unit - -(* inference of subtyping condition for inductive types *) -(* for debugging purposes only to be removed *) -val infer_inductive_subtyping_arity_constructor : Environ.env * Evd.evar_map * Univ.Constraint.t -> -(constr -> constr) -> -types -> bool -> Context.Rel.t -> Environ.env * Evd.evar_map * Univ.Constraint.t - -val infer_inductive_subtyping : Environ.env -> Evd.evar_map -> Entries.mutual_inductive_entry -> - Entries.mutual_inductive_entry diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml new file mode 100644 index 0000000000..a0a8276c5c --- /dev/null +++ b/pretyping/inferCumulativity.ml @@ -0,0 +1,224 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Reduction +open Declarations +open Constr +open Univ +open Util + +(** Throughout this module we modify a map [variances] from local + universes to [Variance.t]. It starts as a trivial mapping to + [Irrelevant] and every time we encounter a local universe we + restrict it accordingly. *) + +let infer_level_eq u variances = + if LMap.mem u variances + then LMap.set u Variance.Invariant variances + else variances + +let infer_level_leq u variances = + match LMap.find u variances with + | exception Not_found -> variances + | varu -> LMap.set u (Variance.sup varu Variance.Covariant) variances + +let infer_generic_instance_eq variances u = + Array.fold_left (fun variances u -> infer_level_eq u variances) + variances (Instance.to_array u) + +let variance_pb cv_pb var = + let open Variance in + match cv_pb, var with + | _, Irrelevant -> Irrelevant + | _, Invariant -> Invariant + | CONV, Covariant -> Invariant + | CUMUL, Covariant -> Covariant + +let infer_cumulative_ind_instance cv_pb cumi variances u = + Array.fold_left2 (fun variances varu u -> + match LMap.find u variances with + | exception Not_found -> variances + | varu' -> + LMap.set u (Variance.sup varu' (variance_pb cv_pb varu)) variances) + variances (ACumulativityInfo.variance cumi) (Instance.to_array u) + +let infer_inductive_instance cv_pb env variances ind nargs u = + let mind = Environ.lookup_mind (fst ind) env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (inductive_cumulativity_arguments (mind,snd ind)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance cv_pb cumi variances u + +let infer_constructor_instance_eq env variances ((mi,ind),ctor) nargs u = + let mind = Environ.lookup_mind mi env in + match mind.mind_universes with + | Monomorphic_ind _ -> assert (Instance.is_empty u); variances + | Polymorphic_ind _ -> infer_generic_instance_eq variances u + | Cumulative_ind cumi -> + if not (Int.equal (constructor_cumulativity_arguments (mind,ind,ctor)) nargs) + then infer_generic_instance_eq variances u + else infer_cumulative_ind_instance CONV cumi variances u + +let infer_sort cv_pb variances s = + match cv_pb with + | CONV -> + LSet.fold infer_level_eq (Universe.levels (Sorts.univ_of_sort s)) variances + | CUMUL -> + LSet.fold infer_level_leq (Universe.levels (Sorts.univ_of_sort s)) variances + +let infer_table_key infos variances c = + let open Names in + match c with + | ConstKey (_, u) -> + infer_generic_instance_eq variances u + | VarKey _ | RelKey _ -> variances + +let rec infer_fterm cv_pb infos variances hd stk = + Control.check_for_interrupt (); + let open CClosure in + let hd,stk = whd_stack infos hd stk in + match fterm_of hd with + | FAtom a -> + begin match kind a with + | Sort s -> infer_sort cv_pb variances s + | Meta _ -> infer_stack infos variances stk + | _ -> assert false + end + | FEvar ((_,args),e) -> + let variances = infer_stack infos variances stk in + infer_vect infos variances (Array.map (mk_clos e) args) + | FRel _ -> variances + | FFlex fl -> + let variances = infer_table_key infos variances fl in + infer_stack infos variances stk + | FProj (_,c) -> + let variances = infer_fterm CONV infos variances c [] in + infer_stack infos variances stk + | FLambda _ -> + let (_,ty,bd) = destFLambda mk_clos hd in + let variances = infer_fterm CONV infos variances ty [] in + infer_fterm CONV infos variances bd [] + | FProd (_,dom,codom) -> + let variances = infer_fterm CONV infos variances dom [] in + infer_fterm cv_pb infos variances codom [] + | FInd (ind, u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_inductive_instance cv_pb (info_env infos) variances ind nargs u + in + infer_stack infos variances stk + | FConstruct (ctor,u) -> + let variances = + if Instance.is_empty u then variances + else + let nargs = stack_args_size stk in + infer_constructor_instance_eq (info_env infos) variances ctor nargs u + in + infer_stack infos variances stk + | FFix ((_,(_,tys,cl)),e) | FCoFix ((_,(_,tys,cl)),e) -> + let n = Array.length cl in + let variances = infer_vect infos variances (Array.map (mk_clos e) tys) in + let le = Esubst.subs_liftn n e in + let variances = infer_vect infos variances (Array.map (mk_clos le) cl) in + infer_stack infos variances stk + + (* Removed by whnf *) + | FLOCKED | FCaseT _ | FCast _ | FLetIn _ | FApp _ | FLIFT _ | FCLOS _ -> assert false + +and infer_stack infos variances (stk:CClosure.stack) = + match stk with + | [] -> variances + | z :: stk -> + let open CClosure in + let variances = match z with + | Zapp v -> infer_vect infos variances v + | Zproj _ -> variances + | Zfix (fx,a) -> + let variances = infer_fterm CONV infos variances fx [] in + infer_stack infos variances a + | ZcaseT (ci,p,br,e) -> + let variances = infer_fterm CONV infos variances (mk_clos e p) [] in + infer_vect infos variances (Array.map (mk_clos e) br) + | Zshift _ -> variances + | Zupdate _ -> variances + in + infer_stack infos variances stk + +and infer_vect infos variances v = + Array.fold_left (fun variances c -> infer_fterm CONV infos variances c []) variances v + +let infer_term cv_pb env variances c = + let open CClosure in + let reds = RedFlags.red_add_transparent betaiotazeta Names.full_transparent_state in + let infos = create_clos_infos reds env in + infer_fterm cv_pb infos variances (CClosure.inject c) [] + +let infer_arity_constructor env variances arcn is_arity params = + let numchecked = ref 0 in + let numparams = Context.Rel.nhyps params in + let basic_check env variances tp = + let variances = + if !numchecked >= numparams then + infer_term CUMUL env variances tp + else + variances + in + numchecked := !numchecked + 1; variances + in + let infer_typ typ (env,variances) = + match typ with + | Context.Rel.Declaration.LocalAssum (_, typ') -> + (Environ.push_rel typ env, basic_check env variances typ') + | Context.Rel.Declaration.LocalDef _ -> assert false + in + let arcn' = Term.it_mkProd_or_LetIn arcn params in + let typs, codom = Reduction.dest_prod env arcn' in + let env, variances = Context.Rel.fold_outside infer_typ typs ~init:(env, variances) in + (* If we have Inductive foo@{i j} : ... -> Type@{i} := C : ... -> foo Type@{j} + i is irrelevant, j is invariant. *) + if not is_arity then basic_check env variances codom else variances + +let infer_inductive env mie = + let open Entries in + let { mind_entry_params = params; + mind_entry_inds = entries; } = mie + in + let univs = + match mie.mind_entry_universes with + | Monomorphic_ind_entry _ + | Polymorphic_ind_entry _ as univs -> univs + | Cumulative_ind_entry cumi -> + let uctx = CumulativityInfo.univ_context cumi in + let uarray = Instance.to_array @@ UContext.instance uctx in + let env = Environ.push_context uctx env in + let variances = + Array.fold_left (fun variances u -> LMap.add u Variance.Irrelevant variances) + LMap.empty uarray + in + let variances = List.fold_left (fun variances entry -> + let _, params = Typeops.infer_local_decls env params in + let variances = infer_arity_constructor + env variances entry.mind_entry_arity true params + in + List.fold_left + (fun variances cons -> + infer_arity_constructor + env variances cons false params) + variances entry.mind_entry_lc) + variances + entries + in + let variances = Array.map (fun u -> LMap.find u variances) uarray in + Cumulative_ind_entry (CumulativityInfo.make (uctx, variances)) + in + { mie with mind_entry_universes = univs } diff --git a/pretyping/inferCumulativity.mli b/pretyping/inferCumulativity.mli new file mode 100644 index 0000000000..a5037ea475 --- /dev/null +++ b/pretyping/inferCumulativity.mli @@ -0,0 +1,10 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> + Entries.mutual_inductive_entry diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 41e09004c6..1bec4a6f15 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -137,8 +137,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef (Projection.constant p) - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern @@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) + | GProj(p,c) -> + PProj(p, pat_of_raw metas vars c) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> err ?loc (Pp.str "Non supported pattern.")) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 92dab24e26..8809558ff7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -737,6 +737,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_sort ?loc evdref s in inh_conv_coerce_to_tycon ?loc env evdref j tycon + | GProj (p, c) -> + (* TODO: once GProj is used as an input syntax, use bidirectional typing here *) + let cj = pretype empty_tycon env evdref lvar c in + judge_of_projection env.ExtraEnv.env !evdref p cj + | GApp (f,args) -> let fj = pretype empty_tycon env evdref lvar f in let floc = loc_of_glob_constr f in diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index 1da5b4567f..ae4ad0be7d 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -4,6 +4,7 @@ Locusops Pretype_errors Reductionops Inductiveops +InferCumulativity Vnorm Arguments_renaming Nativenorm diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 9ff9a75b3e..ab1f3cd320 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -298,29 +298,40 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x) (*s High-level declaration of a canonical structure *) -let error_not_structure ref = +let error_not_structure ref description = user_err ~hdr:"object_declare" - (Id.print (basename_of_global ref) ++ str" is not a structure object.") + (str"Could not declare a canonical structure " ++ + (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ + str(description))) let check_and_decompose_canonical_structure ref = - let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in + let sp = + match ref with + ConstRef sp -> sp + | _ -> error_not_structure ref "Expected an instance of a record or structure." + in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref in + | None -> error_not_structure ref "Could not find its value in the global environment." in let body = snd (splay_lam (Global.env()) Evd.empty (EConstr.of_constr vc)) (** FIXME *) in let body = EConstr.Unsafe.to_constr body in let f,args = match kind body with | App (f,args) -> f,args - | _ -> error_not_structure ref in + | _ -> + error_not_structure ref "Expected a record or structure constructor applied to arguments." in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref in - let s = try lookup_structure indsp with Not_found -> error_not_structure ref in + | _ -> error_not_structure ref "Expected an instance of a record or structure." in + let s = + try lookup_structure indsp + with Not_found -> + error_not_structure ref + ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref; + error_not_structure ref "Got too few arguments to the record or structure constructor."; (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 1893018a95..418ea271cd 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1324,79 +1324,17 @@ let sigma_compare_instances ~flex i0 i1 sigma = | Univ.UniverseInconsistency _ -> raise Reduction.NotConvertible -let sigma_check_inductive_instances cv_pb uinfind u u' sigma = - let len_instance = - Univ.AUContext.size (Univ.ACumulativityInfo.univ_context uinfind) - in - let ind_sbctx = Univ.ACumulativityInfo.subtyp_context uinfind in - if not ((len_instance = Univ.Instance.length u) && - (len_instance = Univ.Instance.length u')) then - anomaly (Pp.str "Invalid inductive subtyping encountered!") - else - let comp_cst = - let comp_subst = (Univ.Instance.append u u') in - Univ.AUContext.instantiate comp_subst ind_sbctx - in - let comp_cst = - match cv_pb with - Reduction.CONV -> - let comp_subst = (Univ.Instance.append u' u) in - let comp_cst' = Univ.AUContext.instantiate comp_subst ind_sbctx in - Univ.Constraint.union comp_cst comp_cst' - | Reduction.CUMUL -> comp_cst - in - try Evd.add_constraints sigma comp_cst - with Evd.UniversesDiffer - | Univ.UniverseInconsistency _ -> - raise Reduction.NotConvertible - -let sigma_conv_inductives - cv_pb (mind, ind) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_param_arity = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - if not (num_param_arity = sv1 && num_param_arity = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances cv_pb cumi u1 u2 sigma - -let sigma_conv_constructors - (mind, ind, cns) u1 sv1 u2 sv2 sigma = - try sigma_compare_instances ~flex:false u1 u2 sigma with - Reduction.NotConvertible -> - match mind.Declarations.mind_universes with - | Declarations.Monomorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Polymorphic_ind _ -> - raise Reduction.NotConvertible - | Declarations.Cumulative_ind cumi -> - let num_cnstr_args = - let nparamsctxt = - mind.Declarations.mind_nparams + - mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs - in - nparamsctxt + - mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1) - in - if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then - raise Reduction.NotConvertible - else - sigma_check_inductive_instances Reduction.CONV cumi u1 u2 sigma +let sigma_check_inductive_instances csts sigma = + try Evd.add_constraints sigma csts + with Evd.UniversesDiffer + | Univ.UniverseInconsistency _ -> + raise Reduction.NotConvertible let sigma_univ_state = - { Reduction.compare = sigma_compare_sorts; - Reduction.compare_instances = sigma_compare_instances; - Reduction.conv_inductives = sigma_conv_inductives; - Reduction.conv_constructors = sigma_conv_constructors} + let open Reduction in + { compare_sorts = sigma_compare_sorts; + compare_instances = sigma_compare_instances; + compare_cumul_instances = sigma_check_inductive_instances; } let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y = diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 9f084ae8df..153a48a710 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -53,3 +53,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index b21fbf0eb2..c93b41786b 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk = let (mib,mip) = Inductive.lookup_mind_specif env ind in let nparams = mib.mind_nparams in let params,realargs = Util.Array.chop nparams allargs in + let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in let pT = - hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in + hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in let pT = whd_all env pT in let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in (* Calcul du type des branches *) |