diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 | ||||
| -rw-r--r-- | pretyping/classops.ml | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 2 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 169 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 66 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 |
8 files changed, 174 insertions, 77 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3f1bead369..737c9fa1b0 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -265,7 +265,7 @@ let rec find_row_ind = function let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in - let arsign = get_full_arity_sign env indu in + let arsign = inductive_alldecls_env env indu in let hole_source = match tmloc with | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in @@ -1636,7 +1636,7 @@ let build_inversion_problem loc env sigma tms t = | Construct (cstr,u) -> PatCstr (Loc.ghost,cstr,[],Anonymous), acc | App (f,v) when isConstruct f -> let cstr,u = destConstruct f in - let n = constructor_nrealargs env cstr in + let n = constructor_nrealargs_env env cstr in let l = List.lastn n (Array.to_list v) in let l,acc = List.fold_map' reveal_pattern l acc in PatCstr (Loc.ghost,cstr,l,Anonymous), acc @@ -1764,7 +1764,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign = | IsInd (term,IndType(indf,realargs),_) -> let indf' = if dolift then lift_inductive_family n indf else indf in let ((ind,u),_) = dest_ind_family indf' in - let nparams_ctxt,nrealargs_ctxt = inductive_nargs_env env0 ind in + let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in let arsign = fst (get_arity env0 indf') in let realnal = match t with diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 7793216d57..f754f9f3fe 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -300,7 +300,7 @@ let get_coercion_constructor coe = in match kind_of_term c with | Construct (cstr,u) -> - (cstr, Inductiveops.constructor_nrealargs (Global.env()) cstr -1) + (cstr, Inductiveops.constructor_nrealargs cstr -1) | _ -> raise Not_found diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 92a29fce70..8bff916028 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -36,7 +36,7 @@ let print_universes = Flags.univ_print let encode_inductive r = let indsp = global_inductive r in - let constr_lengths = mis_constr_nargs indsp in + let constr_lengths = constructors_nrealargs indsp in (indsp,constr_lengths) (* Parameterization of the translation from constr to ast *) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index dba151014c..a12fe6b67c 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -70,7 +70,7 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = (RecursionSchemeError (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) in - let ndepar = mip.mind_nrealargs_ctxt + 1 in + let ndepar = mip.mind_nrealdecls + 1 in (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) (* mais pas très joli ... (mais manque get_sort_of à ce niveau) *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 313bf6110c..ed243bebe6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -104,86 +104,159 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j = let univsubst = make_inductive_subst mib u in substl (List.init ntypes make_Ik) (subst_univs_level_constr univsubst specif.(j-1)) -(* Arity of constructors excluding parameters and local defs *) +(* Number of constructors *) -let mis_constr_nargs indsp = - let (mib,mip) = Global.lookup_inductive indsp in - let recargs = dest_subterms mip.mind_recargs in - Array.map List.length recargs +let nconstructors ind = + let (_,mip) = Global.lookup_inductive ind in + Array.length mip.mind_consnames -let mis_constr_nargs_env env (kn,i) = - let mib = Environ.lookup_mind kn env in - let mip = mib.mind_packets.(i) in - let recargs = dest_subterms mip.mind_recargs in - Array.map List.length recargs +let nconstructors_env env ind = + let (_,mip) = Inductive.lookup_mind_specif env ind in + Array.length mip.mind_consnames -(* Arity of constructors excluding local defs *) +(* Arity of constructors excluding parameters, excluding local defs *) -let mis_constructor_nargs (indsp,j) = +let constructors_nrealargs ind = + let (_,mip) = Global.lookup_inductive ind in + mip.mind_consnrealargs + +let constructors_nrealargs_env env ind = + let (_,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_consnrealargs + +(* Arity of constructors excluding parameters, including local defs *) + +let constructors_nrealdecls ind = + let (_,mip) = Global.lookup_inductive ind in + mip.mind_consnrealdecls + +let constructors_nrealdecls_env env ind = + let (_,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_consnrealdecls + +(* Arity of constructors including parameters, excluding local defs *) + +let constructor_nallargs (indsp,j) = let (mib,mip) = Global.lookup_inductive indsp in - recarg_length mip.mind_recargs j + mib.mind_nparams + mip.mind_consnrealargs.(j-1) + mib.mind_nparams -let mis_constructor_nargs_env env ((kn,i),j) = +let constructor_nallargs_env env ((kn,i),j) = let mib = Environ.lookup_mind kn env in let mip = mib.mind_packets.(i) in - recarg_length mip.mind_recargs j + mib.mind_nparams + mip.mind_consnrealargs.(j-1) + mib.mind_nparams -(* Arity of constructors with arg and defs *) +(* Arity of constructors including params, including local defs *) -let mis_constructor_nhyps (indsp,j) = +let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *) let (mib,mip) = Global.lookup_inductive indsp in - mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) -let mis_constructor_nhyps_env env ((kn,i),j) = +let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *) let mib = Environ.lookup_mind kn env in let mip = mib.mind_packets.(i) in - mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) + +(* Arity of constructors excluding params, excluding local defs *) + +let constructor_nrealargs (ind,j) = + let (_,mip) = Global.lookup_inductive ind in + mip.mind_consnrealargs.(j-1) -let constructor_nrealargs env (ind,j) = +let constructor_nrealargs_env env (ind,j) = let (_,mip) = Inductive.lookup_mind_specif env ind in - recarg_length mip.mind_recargs j + mip.mind_consnrealargs.(j-1) -let constructor_nrealhyps (ind,j) = - let (mib,mip) = Global.lookup_inductive ind in +(* Arity of constructors excluding params, including local defs *) + +let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *) + let (_,mip) = Global.lookup_inductive ind in mip.mind_consnrealdecls.(j-1) -let get_full_arity_sign env (ind,u) = - let (mib,mip) = Inductive.lookup_mind_specif env ind in - let subst = Inductive.make_inductive_subst mib u in - Vars.subst_univs_level_context subst mip.mind_arity_ctxt +let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *) + let (_,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_consnrealdecls.(j-1) -let nconstructors ind = - let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in - Array.length mip.mind_consnames +(* Length of arity, excluding params, including local defs *) -let mis_constructor_has_local_defs (indsp,j) = - let (mib,mip) = Global.lookup_inductive indsp in - let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in - let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in - not (Int.equal l1 l2) +let inductive_nrealdecls ind = + let (_,mip) = Global.lookup_inductive ind in + mip.mind_nrealdecls -let inductive_has_local_defs ind = +let inductive_nrealdecls_env env ind = + let (_,mip) = Inductive.lookup_mind_specif env ind in + mip.mind_nrealdecls + +(* Full length of arity (w/o local defs) *) + +let inductive_nallargs ind = let (mib,mip) = Global.lookup_inductive ind in - let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealargs_ctxt in - let l2 = mib.mind_nparams + mip.mind_nrealargs in - not (Int.equal l1 l2) + mib.mind_nparams + mip.mind_nrealargs + +let inductive_nallargs_env env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mib.mind_nparams + mip.mind_nrealargs (* Length of arity (w/o local defs) *) let inductive_nparams ind = - (fst (Global.lookup_inductive ind)).mind_nparams + let (mib,mip) = Global.lookup_inductive ind in + mib.mind_nparams + +let inductive_nparams_env env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + mib.mind_nparams + +(* Length of arity (with local defs) *) + +let inductive_nparamdecls ind = + let (mib,mip) = Global.lookup_inductive ind in + rel_context_length mib.mind_params_ctxt + +let inductive_nparamdecls_env env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + rel_context_length mib.mind_params_ctxt + +(* Full length of arity (with local defs) *) + +let inductive_nalldecls ind = + let (mib,mip) = Global.lookup_inductive ind in + rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls + +let inductive_nalldecls_env env ind = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls -let inductive_params_ctxt (ind,u) = +(* Others *) + +let inductive_paramdecls (ind,u) = let (mib,mip) = Global.lookup_inductive ind in - Inductive.inductive_params_ctxt (mib,u) + Inductive.inductive_paramdecls (mib,u) + +let inductive_paramdecls_env env (ind,u) = + let (mib,mip) = Inductive.lookup_mind_specif env ind in + Inductive.inductive_paramdecls (mib,u) -let inductive_nargs ind = +let inductive_alldecls (ind,u) = let (mib,mip) = Global.lookup_inductive ind in - (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt) + let subst = Inductive.make_inductive_subst mib u in + Vars.subst_univs_level_context subst mip.mind_arity_ctxt -let inductive_nargs_env env ind = +let inductive_alldecls_env env (ind,u) = let (mib,mip) = Inductive.lookup_mind_specif env ind in - (rel_context_length (mib.mind_params_ctxt), mip.mind_nrealargs_ctxt) + let subst = Inductive.make_inductive_subst mib u in + Vars.subst_univs_level_context subst mip.mind_arity_ctxt + +let constructor_has_local_defs (indsp,j) = + let (mib,mip) = Global.lookup_inductive indsp in + let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in + let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in + not (Int.equal l1 l2) + +let inductive_has_local_defs ind = + let (mib,mip) = Global.lookup_inductive ind in + let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in + let l2 = mib.mind_nparams + mip.mind_nrealargs in + not (Int.equal l1 l2) let allowed_sorts env (kn,i as ind) = let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -192,7 +265,7 @@ let allowed_sorts env (kn,i as ind) = (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in - let print_info = { ind_nargs = mip.mind_nrealargs_ctxt; style = style } in + let print_info = { ind_nargs = mip.mind_nrealdecls; style = style } in { ci_ind = ind; ci_npar = mib.mind_nparams; ci_cstr_ndecls = mip.mind_consnrealdecls; diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 1efc29c8fd..10ff968cf8 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -52,46 +52,70 @@ val mis_is_recursive : val mis_nf_constructor_type : pinductive * mutual_inductive_body * one_inductive_body -> int -> constr -(** {6 Extract information from an inductive name} +(** {6 Extract information from an inductive name} *) +(** @return number of constructors *) +val nconstructors : inductive -> int +val nconstructors_env : env -> inductive -> int -Functions without env lookup in the globalenv. *) +(** @return arity of constructors excluding parameters, excluding local defs *) +val constructors_nrealargs : inductive -> int array +val constructors_nrealargs_env : env -> inductive -> int array -(** Arity of constructors excluding parameters and local defs *) -val mis_constr_nargs : inductive -> int array -val mis_constr_nargs_env : env -> inductive -> int array +(** @return arity of constructors excluding parameters, including local defs *) +val constructors_nrealdecls : inductive -> int array +val constructors_nrealdecls_env : env -> inductive -> int array -val nconstructors : inductive -> int +(** @return the arity, excluding params, including local defs *) +val inductive_nrealdecls : inductive -> int +val inductive_nrealdecls_env : env -> inductive -> int -(** @return the lengths of parameters signature and real arguments signature - with letin *) -val inductive_nargs : inductive -> int * int -val inductive_nargs_env : env -> inductive -> int * int +(** @return the arity, including params, excluding local defs *) +val inductive_nallargs : inductive -> int +val inductive_nallargs_env : env -> inductive -> int -(** @return nb of params without letin *) +(** @return the arity, including params, including local defs *) +val inductive_nalldecls : inductive -> int +val inductive_nalldecls_env : env -> inductive -> int + +(** @return nb of params without local defs *) val inductive_nparams : inductive -> int -val inductive_params_ctxt : pinductive -> rel_context +val inductive_nparams_env : env -> inductive -> int + +(** @return nb of params with local defs *) +val inductive_nparamdecls : inductive -> int +val inductive_nparamdecls_env : env -> inductive -> int + +(** @return params context *) +val inductive_paramdecls : pinductive -> rel_context +val inductive_paramdecls_env : env -> pinductive -> rel_context + +(** @return full arity context, hence with letin *) +val inductive_alldecls : pinductive -> rel_context +val inductive_alldecls_env : env -> pinductive -> rel_context + +(** {7 Extract information from a constructor name} *) (** @return param + args without letin *) -val mis_constructor_nargs : constructor -> int -val mis_constructor_nargs_env : env -> constructor -> int +val constructor_nallargs : constructor -> int +val constructor_nallargs_env : env -> constructor -> int (** @return param + args with letin *) -val mis_constructor_nhyps : constructor -> int -val mis_constructor_nhyps_env : env -> constructor -> int +val constructor_nalldecls : constructor -> int +val constructor_nalldecls_env : env -> constructor -> int (** @return args without letin *) -val constructor_nrealargs : env -> constructor -> int +val constructor_nrealargs : constructor -> int +val constructor_nrealargs_env : env -> constructor -> int (** @return args with letin *) -val constructor_nrealhyps : constructor -> int +val constructor_nrealdecls : constructor -> int +val constructor_nrealdecls_env : env -> constructor -> int (** Is there local defs in params or args ? *) -val mis_constructor_has_local_defs : constructor -> bool +val constructor_has_local_defs : constructor -> bool val inductive_has_local_defs : inductive -> bool -val get_full_arity_sign : env -> pinductive -> rel_context - val allowed_sorts : env -> inductive -> sorts_family list (** Extract information from an inductive family *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 9609a959b6..e5023e8582 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -498,7 +498,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar t = Evarutil.evd_comb1 (Evd.fresh_inductive_instance env) evdref (mind,0) in let args = - let ctx = smash_rel_context (Inductiveops.inductive_params_ctxt ind) in + let ctx = smash_rel_context (Inductiveops.inductive_paramdecls ind) in List.fold_right (fun (n, b, ty) (* par *)args -> let ty = substl args ty in let ev = e_new_evar evdref env ~src:(loc,k) ty in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 669fbfb46e..8f5a7e39a1 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -111,7 +111,7 @@ let e_type_case_branches env evdref (ind,largs) pj c = let p = pj.uj_val in let univ = e_is_correct_arity env evdref c pj ind specif params in let lc = build_branches_type ind specif params p in - let n = (snd specif).Declarations.mind_nrealargs_ctxt in + let n = (snd specif).Declarations.mind_nrealdecls in let ty = whd_betaiota !evdref (Reduction.betazeta_appvect (n+1) p (Array.of_list (realargs@[c]))) in (lc, ty, univ) |