diff options
-rw-r--r-- | checker/cic.mli | 2 | ||||
-rw-r--r-- | checker/declarations.ml | 2 | ||||
-rw-r--r-- | checker/indtypes.ml | 2 | ||||
-rw-r--r-- | checker/inductive.ml | 6 | ||||
-rw-r--r-- | dev/doc/changes.txt | 2 | ||||
-rw-r--r-- | interp/constrextern.ml | 4 | ||||
-rw-r--r-- | interp/constrintern.ml | 26 | ||||
-rw-r--r-- | kernel/declarations.mli | 10 | ||||
-rw-r--r-- | kernel/declareops.ml | 2 | ||||
-rw-r--r-- | kernel/indtypes.ml | 2 | ||||
-rw-r--r-- | kernel/inductive.ml | 8 | ||||
-rw-r--r-- | kernel/inductive.mli | 2 | ||||
-rw-r--r-- | parsing/g_xml.ml4 | 6 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 2 | ||||
-rw-r--r-- | plugins/funind/glob_term_to_relation.ml | 4 | ||||
-rw-r--r-- | plugins/funind/glob_termops.ml | 2 | ||||
-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 | ||||
-rw-r--r-- | tactics/eqschemes.ml | 14 | ||||
-rw-r--r-- | tactics/equality.ml | 4 | ||||
-rw-r--r-- | tactics/hipattern.ml4 | 4 | ||||
-rw-r--r-- | tactics/tactics.ml | 4 |
29 files changed, 228 insertions, 133 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 484d64973..cd6d0afee 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -254,7 +254,7 @@ type one_inductive_body = { mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *) + mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) mind_kelim : sorts_family list; (** List of allowed elimination sorts *) diff --git a/checker/declarations.ml b/checker/declarations.ml index c705a707f..d38df793f 100644 --- a/checker/declarations.ml +++ b/checker/declarations.ml @@ -557,7 +557,7 @@ let subst_mind_packet sub mbp = mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; + mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 14710c10b..49d78a7a6 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -160,7 +160,7 @@ let typecheck_arity env params inds = if ind.mind_nrealargs <> nrealargs then failwith "bad number of real inductive arguments"; let nrealargs_ctxt = rel_context_length ar_ctxt - nparamdecls in - if ind.mind_nrealargs_ctxt <> nrealargs_ctxt then + if ind.mind_nrealdecls <> nrealargs_ctxt then failwith "bad length of real inductive arguments signature"; (* We do not need to generate the universe of full_arity; if later, after the validation of the inductive definition, diff --git a/checker/inductive.ml b/checker/inductive.ml index 9d739b04c..f6cc5c565 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -59,7 +59,7 @@ let make_inductive_subst mib u = Univ.make_universe_subst u mib.mind_universes else Univ.empty_level_subst -let inductive_params_ctxt (mib,u) = +let inductive_paramdecls (mib,u) = let subst = make_inductive_subst mib u in subst_univs_level_context subst mib.mind_params_ctxt @@ -361,10 +361,10 @@ let extended_rel_list n hyps = reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (Ind ind, - List.map (lift mip.mind_nrealargs_ctxt) params + List.map (lift mip.mind_nrealdecls) params @ extended_rel_list 0 realargs) (* This exception is local *) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index a919b86c2..036bf1d5e 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -85,6 +85,8 @@ renamed into replace_term_occ_modulo and replace_term_occ_decl_modulo). +- API of Inductiveops made more uniform (see commit log or file itself). + ========================================= = CHANGES BETWEEN COQ V8.3 AND COQ V8.4 = ========================================= diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 5ce7f8f91..9c2f8bcd3 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -165,7 +165,7 @@ let in_debugger = ref false let add_patt_for_params ind l = if !in_debugger then l else - Util.List.addn (fst (Inductiveops.inductive_nargs ind)) (CPatAtom (Loc.ghost,None)) l + Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CPatAtom (Loc.ghost,None)) l let drop_implicits_in_patt cst nb_expl args = let impl_st = (implicits_of_global cst) in @@ -275,7 +275,7 @@ let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat = not explicit application. *) match pat with | PatCstr(loc,cstrsp,args,na) - when !in_debugger||Inductiveops.mis_constructor_has_local_defs cstrsp -> + when !in_debugger||Inductiveops.constructor_has_local_defs cstrsp -> let c = extern_reference loc Id.Set.empty (ConstructRef cstrsp) in let args = List.map (extern_cases_pattern_in_scope scopes vars) args in CPatCstr (loc, c, add_patt_for_params (fst cstrsp) args, []) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 195bd31fe..95d902fd4 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -876,12 +876,11 @@ let check_or_pat_variables loc ids idsl = (** Use only when params were NOT asked to the user. @return if letin are included *) let check_constructor_length env loc cstr len_pl pl0 = - let nargs = Inductiveops.mis_constructor_nargs cstr in let n = len_pl + List.length pl0 in - if Int.equal n nargs then false else - (Int.equal n ((fst (Inductiveops.inductive_nargs (fst cstr))) + Inductiveops.constructor_nrealhyps cstr)) || + if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else + (Int.equal n (Inductiveops.constructor_nalldecls cstr) || (error_wrong_numarg_constructor_loc loc env cstr - (nargs - (Inductiveops.inductive_nparams (fst cstr)))) + (Inductiveops.constructor_nrealargs cstr))) let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 = let impl_list = if Int.equal len_pl1 0 @@ -902,26 +901,23 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2 in aux 0 (impl_list,pl2) let add_implicits_check_constructor_length env loc c len_pl1 pl2 = - let nargs = Inductiveops.mis_constructor_nargs c in - let nargs' = (fst (Inductiveops.inductive_nargs (fst c))) - + Inductiveops.constructor_nrealhyps c in + let nargs = Inductiveops.constructor_nallargs c in + let nargs' = Inductiveops.constructor_nalldecls c in let impls_st = implicits_of_global (ConstructRef c) in add_implicits_check_length (error_wrong_numarg_constructor_loc loc env c) nargs nargs' impls_st len_pl1 pl2 let add_implicits_check_ind_length env loc c len_pl1 pl2 = - let (mib,mip) = Global.lookup_inductive c in - let nparams = mib.Declarations.mind_nparams in - let nargs = mip.Declarations.mind_nrealargs + nparams in - let nparams', nrealargs' = inductive_nargs_env env c in + let nallargs = inductive_nallargs_env env c in + let nalldecls = inductive_nalldecls_env env c in let impls_st = implicits_of_global (IndRef c) in add_implicits_check_length (error_wrong_numarg_inductive_loc loc env c) - nargs (nrealargs' + nparams') impls_st len_pl1 pl2 + nallargs nalldecls impls_st len_pl1 pl2 (** Do not raise NotEnoughArguments thanks to preconditions*) let chop_params_pattern loc ind args with_letin = let nparams = if with_letin - then fst (Inductiveops.inductive_nargs ind) + then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in assert (nparams <= List.length args); let params,args = List.chop nparams args in @@ -942,8 +938,8 @@ let find_constructor loc add_params ref = cstr, (function (ind,_ as c) -> match add_params with |Some nb_args -> let nb = - if Int.equal nb_args (Inductiveops.constructor_nrealhyps c) - then fst (Inductiveops.inductive_nargs ind) + if Int.equal nb_args (Inductiveops.constructor_nrealdecls c) + then Inductiveops.inductive_nparamdecls ind else Inductiveops.inductive_nparams ind in List.make nb ([], [(Id.Map.empty, PatVar(Loc.ghost,Anonymous))]) diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 85dac4bfc..f76f401b4 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -123,18 +123,18 @@ type one_inductive_body = { mind_nrealargs : int; (** Number of expected real arguments of the type (no let, no params) *) - mind_nrealargs_ctxt : int; (** Length of realargs context (with let, no params) *) + mind_nrealdecls : int; (** Length of realargs context (with let, no params) *) mind_kelim : sorts_family list; (** List of allowed elimination sorts *) mind_nf_lc : types array; (** Head normalized constructor types so that their conclusion is atomic *) - mind_consnrealdecls : int array; - (** Length of the signature of the constructors (with let, w/o params) + mind_consnrealargs : int array; + (** Number of expected proper arguments of the constructors (w/o params) (not used in the kernel) *) - mind_consnrealargs : int array; - (** Length of the signature of the constructors (w/o let, w/o params) + mind_consnrealdecls : int array; + (** Length of the signature of the constructors (with let, w/o params) (not used in the kernel) *) mind_recargs : wf_paths; (** Signature of recursive arguments in the constructors *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9d2382f6e..4524b55bb 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -216,7 +216,7 @@ let subst_mind_packet sub mbp = mind_arity = subst_ind_arity sub mbp.mind_arity; mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; - mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; + mind_nrealdecls = mbp.mind_nrealdecls; mind_kelim = mbp.mind_kelim; mind_recargs = subst_wf_paths sub mbp.mind_recargs (*wf_paths*); mind_nb_constant = mbp.mind_nb_constant; diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 9c83ba1a9..89d2d7b67 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -728,7 +728,7 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re mind_arity = arkind; mind_arity_ctxt = ar_sign; mind_nrealargs = rel_context_nhyps ar_sign - nparamargs; - mind_nrealargs_ctxt = rel_context_length ar_sign - nparamdecls; + mind_nrealdecls = rel_context_length ar_sign - nparamdecls; mind_kelim = kelim; mind_consnames = Array.of_list cnames; mind_consnrealdecls = consnrealdecls; diff --git a/kernel/inductive.ml b/kernel/inductive.ml index f08843a17..163bc3a42 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -55,7 +55,7 @@ let make_inductive_subst mib u = make_universe_subst u mib.mind_universes else Univ.empty_level_subst -let inductive_params_ctxt (mib,u) = +let inductive_paramdecls (mib,u) = let subst = make_inductive_subst mib u in Vars.subst_univs_level_context subst mib.mind_params_ctxt @@ -347,10 +347,10 @@ let extended_rel_list n hyps = reln [] 1 hyps let build_dependent_inductive ind (_,mip) params = - let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, - List.map (lift mip.mind_nrealargs_ctxt) params + List.map (lift mip.mind_nrealdecls) params @ extended_rel_list 0 realargs) (* This exception is local *) @@ -427,7 +427,7 @@ let type_case_branches env (pind,largs) pj c = let p = pj.uj_val in let () = is_correct_arity env c pj pind specif params in let lc = build_branches_type pind specif params p in - let ty = build_case_type env (snd specif).mind_nrealargs_ctxt p c realargs in + let ty = build_case_type env (snd specif).mind_nrealdecls p c realargs in (lc, ty) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 05b0248b9..8bd1a5605 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -39,7 +39,7 @@ val make_inductive_subst : mutual_inductive_body -> universe_instance -> univers val inductive_instance : mutual_inductive_body -> universe_instance val inductive_context : mutual_inductive_body -> universe_context -val inductive_params_ctxt : mutual_inductive_body puniverses -> rel_context +val inductive_paramdecls : mutual_inductive_body puniverses -> rel_context val instantiate_inductive_constraints : mutual_inductive_body -> universe_level_subst -> constraints diff --git a/parsing/g_xml.ml4 b/parsing/g_xml.ml4 index 99cfa7083..621aab8a0 100644 --- a/parsing/g_xml.ml4 +++ b/parsing/g_xml.ml4 @@ -146,8 +146,8 @@ let compute_branches_lengths ind = let (_,mip) = Inductive.lookup_mind_specif (Global.env()) ind in mip.Declarations.mind_consnrealdecls -let compute_inductive_nargs ind = - Inductiveops.inductive_nargs ind +let compute_inductive_ndecls ind = + snd (Inductiveops.inductive_ndecls ind) (* Interpreting constr as a glob_constr *) @@ -188,7 +188,7 @@ let rec interp_xml_constr = function let brs = List.map_i (fun i c -> (i,vars.(i),interp_xml_pattern c)) 0 yl in let mat = simple_cases_matrix_of_branches ind brs in - let nparams,n = compute_inductive_nargs ind in + let n = compute_inductive_ndecls ind in let nal,rtn = return_type_of_predicate ind n p in GCases (loc,RegularStyle,rtn,[tm,nal],mat) | XmlTag (loc,"MUTIND",al,[]) -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 73c050bb2..70aaa0c0f 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -65,7 +65,7 @@ let rec decompose_term env sigma t= let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in - let nargs=mis_constructor_nargs_env env (canon_ind,i_con) in + let nargs=constructor_nallargs_env env (canon_ind,i_con) in Constructor {ci_constr= ((canon_ind,i_con),u); ci_arity=nargs; ci_nhyps=nargs-oib.mind_nparams} diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index cce6aff28..618717cde 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -793,7 +793,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = and extract_case env mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = mis_constr_nargs_env env ip in + let ni = constructors_nrealargs_env env ip in let br_size = Array.length br in assert (Int.equal (Array.length ni) br_size); if Int.equal br_size 0 then begin diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 41970fce8..40abdb68b 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -304,7 +304,7 @@ let build_constructors_of_type ind' argl = Impargs.implicits_of_global constructref in let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) construct in @@ -388,7 +388,7 @@ let rec pattern_to_term_and_type env typ = function mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) constr in diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 5efaf7954..4cdea414e 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -427,7 +427,7 @@ let rec pattern_to_term = function mkGVar id | PatCstr(loc,constr,patternl,_) -> let cst_narg = - Inductiveops.mis_constructor_nargs_env + Inductiveops.constructor_nallargs_env (Global.env ()) constr in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 3f1bead36..737c9fa1b 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 7793216d5..f754f9f3f 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 92a29fce7..8bff91602 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 dba151014..a12fe6b67 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 313bf6110..ed243bebe 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 1efc29c8f..10ff968cf 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 9609a959b..e5023e858 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 669fbfb46..8f5a7e39a 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) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 7a536b35a..9cf2baf6f 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -67,10 +67,10 @@ let with_context_set ctx (b, ctx') = (b, Univ.ContextSet.union ctx ctx') let build_dependent_inductive ind (mib,mip) = - let realargs,_ = List.chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in + let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in applist (mkIndU ind, - extended_rel_list mip.mind_nrealargs_ctxt mib.mind_params_ctxt + extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt @ extended_rel_list 0 realargs) let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s @@ -104,7 +104,7 @@ let get_sym_eq_data env (ind,u) = error "Not an inductive type with a single constructor."; let subst = Inductive.make_inductive_subst mib u in let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in - let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in + let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in @@ -140,7 +140,7 @@ let get_non_sym_eq_data env (ind,u) = error "Not an inductive type with a single constructor."; let subst = Inductive.make_inductive_subst mib u in let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in - let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in + let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported"; let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in @@ -737,7 +737,7 @@ let build_congr env (eq,refl,ctx) ind = let i = 1 in let arityctxt = Vars.subst_univs_level_context subst mip.mind_arity_ctxt in let paramsctxt = Vars.subst_univs_level_context subst mib.mind_params_ctxt in - let realsign,_ = List.chop mip.mind_nrealargs_ctxt arityctxt in + let realsign,_ = List.chop mip.mind_nrealdecls arityctxt in if List.exists (fun (_,b,_) -> not (Option.is_empty b)) realsign then error "Inductive equalities with local definitions in arity not supported."; let env_with_arity = push_rel_context arityctxt env in @@ -769,12 +769,12 @@ let build_congr env (eq,refl,ctx) ind = (Anonymous, applist (mkIndU indu, - extended_rel_list (2*mip.mind_nrealargs_ctxt+3) + extended_rel_list (2*mip.mind_nrealdecls+3) paramsctxt @ extended_rel_list 0 realsign), mkApp (eq, [|mkVar varB; - mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) b|]); + mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]); mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))), mkVar varH, [|mkApp (refl, diff --git a/tactics/equality.ml b/tactics/equality.ml index 63bb84613..e3ea08656 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -634,7 +634,7 @@ let find_positions env sigma t1 t2 = let hd2,args2 = whd_betadeltaiota_stack env sigma t2 in match (kind_of_term hd1, kind_of_term hd2) with | Construct (sp1,_), Construct (sp2,_) - when Int.equal (List.length args1) (mis_constructor_nargs_env env sp1) + when Int.equal (List.length args1) (constructor_nallargs_env env sp1) -> let sorts' = Sorts.List.intersect sorts (allowed_sorts env (fst sp1)) @@ -642,7 +642,7 @@ let find_positions env sigma t1 t2 = (* both sides are fully applied constructors, so either we descend, or we can discriminate here. *) if eq_constructor sp1 sp2 then - let nrealargs = constructor_nrealargs env sp1 in + let nrealargs = constructor_nrealargs_env env sp1 in let rargs1 = List.lastn nrealargs args1 in let rargs2 = List.lastn nrealargs args2 in List.flatten diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4 index a8bcec288..dc78229f6 100644 --- a/tactics/hipattern.ml4 +++ b/tactics/hipattern.ml4 @@ -159,7 +159,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) t = let (hdapp,args) = decompose_app t in let res = match kind_of_term hdapp with | Ind (ind,u) -> - let car = mis_constr_nargs ind in + let car = constructors_nrealargs ind in let (mib,mip) = Global.lookup_inductive ind in if Array.for_all (fun ar -> Int.equal ar 1) car && not (mis_is_recursive (ind,mib,mip)) @@ -277,7 +277,7 @@ let match_with_equation t = let is_inductive_equality ind = let (mib,mip) = Global.lookup_inductive ind in let nconstr = Array.length mip.mind_consnames in - Int.equal nconstr 1 && Int.equal (constructor_nrealargs (Global.env()) (ind,1)) 0 + Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0 let match_with_equality_type t = let (hdapp,args) = decompose_app t in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bf64e15e9..07ac0ba9f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1033,7 +1033,7 @@ let descend_in_conjunctions tac exit c gl = let sign,ccl = decompose_prod_assum t in match match_with_tuple ccl with | Some (_,_,isrec) -> - let n = (mis_constr_nargs ind).(0) in + let n = (constructors_nrealargs ind).(0) in let sort = elimination_sort_of_goal gl in let id = fresh_id [] (Id.of_string "H") gl in let IndType (indf,_) = pf_apply find_rectype gl ccl in @@ -1485,7 +1485,7 @@ let intro_or_and_pattern loc bracketed ll thin tac id = let c = mkVar id in let t = Tacmach.New.pf_type_of gl c in let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in - let nv = mis_constr_nargs ind in + let nv = constructors_nrealargs ind in let ll = fix_empty_or_and_pattern (Array.length nv) ll in check_or_and_pattern_size loc ll (Array.length nv); Tacticals.New.tclTHENLASTn |