diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
Nouveaux types 'constructor' et 'inductive' dans Term;
les fonctions sur les inductifs prennent maintenant des 'inductive' en
paramètres; elle n'ont plus besoin de faire des appels dangereux
aux find_m*type qui centralisent la levée de raise Induc.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
47 files changed, 502 insertions, 528 deletions
@@ -17,7 +17,8 @@ kernel/instantiate.cmi: kernel/environ.cmi kernel/evd.cmi \ kernel/inductive.cmi kernel/names.cmi kernel/term.cmi kernel/names.cmi: lib/pp.cmi kernel/reduction.cmi: kernel/closure.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/generic.cmi kernel/names.cmi kernel/term.cmi kernel/univ.cmi + kernel/generic.cmi kernel/inductive.cmi kernel/names.cmi kernel/term.cmi \ + kernel/univ.cmi kernel/safe_typing.cmi: kernel/constant.cmi kernel/environ.cmi \ kernel/inductive.cmi kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi @@ -70,6 +71,10 @@ parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi \ pretyping/rawterm.cmi kernel/sign.cmi kernel/term.cmi +pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \ + kernel/evd.cmi kernel/generic.cmi kernel/names.cmi lib/pp.cmi \ + pretyping/rawterm.cmi pretyping/retyping.cmi kernel/sign.cmi \ + kernel/term.cmi kernel/type_errors.cmi pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \ kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \ @@ -262,9 +267,9 @@ kernel/term.cmo: kernel/generic.cmi lib/hashcons.cmi kernel/names.cmi \ kernel/term.cmx: kernel/generic.cmx lib/hashcons.cmx kernel/names.cmx \ lib/pp.cmx kernel/univ.cmx lib/util.cmx kernel/term.cmi kernel/type_errors.cmo: kernel/environ.cmi kernel/names.cmi lib/pp.cmi \ - kernel/sign.cmi kernel/term.cmi lib/util.cmi kernel/type_errors.cmi + kernel/sign.cmi kernel/term.cmi kernel/type_errors.cmi kernel/type_errors.cmx: kernel/environ.cmx kernel/names.cmx lib/pp.cmx \ - kernel/sign.cmx kernel/term.cmx lib/util.cmx kernel/type_errors.cmi + kernel/sign.cmx kernel/term.cmx kernel/type_errors.cmi kernel/typeops.cmo: kernel/constant.cmi kernel/environ.cmi kernel/evd.cmi \ kernel/generic.cmi kernel/inductive.cmi kernel/instantiate.cmi \ kernel/names.cmi lib/pp.cmi kernel/reduction.cmi kernel/sign.cmi \ @@ -558,13 +563,13 @@ pretyping/recordops.cmx: pretyping/classops.cmx library/lib.cmx \ library/summary.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \ pretyping/recordops.cmi pretyping/retyping.cmo: kernel/environ.cmi kernel/generic.cmi \ - kernel/inductive.cmi kernel/instantiate.cmi kernel/names.cmi \ - kernel/reduction.cmi kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi \ - lib/util.cmi pretyping/retyping.cmi + kernel/inductive.cmi kernel/names.cmi kernel/reduction.cmi \ + kernel/term.cmi kernel/typeops.cmi kernel/univ.cmi lib/util.cmi \ + pretyping/retyping.cmi pretyping/retyping.cmx: kernel/environ.cmx kernel/generic.cmx \ - kernel/inductive.cmx kernel/instantiate.cmx kernel/names.cmx \ - kernel/reduction.cmx kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx \ - lib/util.cmx pretyping/retyping.cmi + kernel/inductive.cmx kernel/names.cmx kernel/reduction.cmx \ + kernel/term.cmx kernel/typeops.cmx kernel/univ.cmx lib/util.cmx \ + pretyping/retyping.cmi pretyping/syntax_def.cmo: library/lib.cmi library/libobject.cmi \ kernel/names.cmi library/nametab.cmi pretyping/rawterm.cmi \ library/summary.cmi pretyping/syntax_def.cmi @@ -588,13 +593,13 @@ pretyping/typing.cmx: kernel/environ.cmx kernel/generic.cmx kernel/names.cmx \ proofs/clenv.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ kernel/instantiate.cmi proofs/logic.cmi kernel/names.cmi lib/pp.cmi \ parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi kernel/type_errors.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/clenv.cmi + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/clenv.cmi proofs/clenv.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ kernel/instantiate.cmx proofs/logic.cmx kernel/names.cmx lib/pp.cmx \ parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx kernel/type_errors.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/clenv.cmi + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/clenv.cmi proofs/evar_refiner.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \ proofs/logic.cmi kernel/names.cmi lib/pp.cmi proofs/proof_trees.cmi \ kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi kernel/term.cmi \ @@ -606,13 +611,15 @@ proofs/evar_refiner.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \ proofs/logic.cmo: parsing/coqast.cmi library/declare.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \ lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi kernel/typeops.cmi \ - pretyping/typing.cmi lib/util.cmi proofs/logic.cmi + kernel/reduction.cmi kernel/sign.cmi kernel/term.cmi \ + kernel/type_errors.cmi kernel/typeops.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/logic.cmi proofs/logic.cmx: parsing/coqast.cmx library/declare.cmx kernel/environ.cmx \ kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \ lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx kernel/typeops.cmx \ - pretyping/typing.cmx lib/util.cmx proofs/logic.cmi + kernel/reduction.cmx kernel/sign.cmx kernel/term.cmx \ + kernel/type_errors.cmx kernel/typeops.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/logic.cmi proofs/macros.cmo: parsing/ast.cmi parsing/coqast.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi library/summary.cmi \ @@ -623,16 +630,16 @@ proofs/macros.cmx: parsing/ast.cmx parsing/coqast.cmx library/lib.cmx \ kernel/term.cmx lib/util.cmx proofs/macros.cmi proofs/pfedit.cmo: parsing/astterm.cmi kernel/constant.cmi \ library/declare.cmi lib/edit.cmi kernel/environ.cmi kernel/evd.cmi \ - kernel/generic.cmi library/global.cmi library/lib.cmi kernel/names.cmi \ - lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/sign.cmi \ - proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - proofs/pfedit.cmi + kernel/generic.cmi library/global.cmi library/lib.cmi proofs/logic.cmi \ + kernel/names.cmi lib/options.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi pretyping/typing.cmi \ + lib/util.cmi proofs/pfedit.cmi proofs/pfedit.cmx: parsing/astterm.cmx kernel/constant.cmx \ library/declare.cmx lib/edit.cmx kernel/environ.cmx kernel/evd.cmx \ - kernel/generic.cmx library/global.cmx library/lib.cmx kernel/names.cmx \ - lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/sign.cmx \ - proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - proofs/pfedit.cmi + kernel/generic.cmx library/global.cmx library/lib.cmx proofs/logic.cmx \ + kernel/names.cmx lib/options.cmx lib/pp.cmx proofs/proof_trees.cmx \ + kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx pretyping/typing.cmx \ + lib/util.cmx proofs/pfedit.cmi proofs/proof_trees.cmo: parsing/ast.cmi parsing/coqast.cmi kernel/environ.cmi \ kernel/evd.cmi kernel/names.cmi lib/pp.cmi parsing/pretty.cmi \ parsing/printer.cmi kernel/sign.cmi lib/stamps.cmi kernel/term.cmi \ @@ -679,22 +686,24 @@ tactics/auto.cmo: parsing/astterm.cmi tactics/btermdn.cmi proofs/clenv.cmi \ parsing/coqast.cmi library/declare.cmi tactics/dhyp.cmi kernel/evd.cmi \ kernel/generic.cmi library/global.cmi tactics/hiddentac.cmi \ kernel/inductive.cmi library/lib.cmi library/libobject.cmi \ - library/library.cmi kernel/names.cmi lib/options.cmi tactics/pattern.cmi \ - proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi kernel/sign.cmi library/summary.cmi \ - proofs/tacmach.cmi pretyping/tacred.cmi tactics/tacticals.cmi \ - tactics/tactics.cmi kernel/term.cmi pretyping/typing.cmi lib/util.cmi \ - toplevel/vernacinterp.cmi tactics/auto.cmi + library/library.cmi proofs/logic.cmi kernel/names.cmi lib/options.cmi \ + tactics/pattern.cmi proofs/pfedit.cmi lib/pp.cmi parsing/printer.cmi \ + proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ + library/summary.cmi proofs/tacmach.cmi pretyping/tacred.cmi \ + tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi \ + pretyping/typing.cmi lib/util.cmi toplevel/vernacinterp.cmi \ + tactics/auto.cmi tactics/auto.cmx: parsing/astterm.cmx tactics/btermdn.cmx proofs/clenv.cmx \ parsing/coqast.cmx library/declare.cmx tactics/dhyp.cmx kernel/evd.cmx \ kernel/generic.cmx library/global.cmx tactics/hiddentac.cmx \ kernel/inductive.cmx library/lib.cmx library/libobject.cmx \ - library/library.cmx kernel/names.cmx lib/options.cmx tactics/pattern.cmx \ - proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx kernel/sign.cmx library/summary.cmx \ - proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \ - tactics/tactics.cmx kernel/term.cmx pretyping/typing.cmx lib/util.cmx \ - toplevel/vernacinterp.cmx tactics/auto.cmi + library/library.cmx proofs/logic.cmx kernel/names.cmx lib/options.cmx \ + tactics/pattern.cmx proofs/pfedit.cmx lib/pp.cmx parsing/printer.cmx \ + proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ + library/summary.cmx proofs/tacmach.cmx pretyping/tacred.cmx \ + tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx \ + pretyping/typing.cmx lib/util.cmx toplevel/vernacinterp.cmx \ + tactics/auto.cmi tactics/btermdn.cmo: tactics/dn.cmi kernel/term.cmi tactics/termdn.cmi \ tactics/btermdn.cmi tactics/btermdn.cmx: tactics/dn.cmx kernel/term.cmx tactics/termdn.cmx \ @@ -736,15 +745,15 @@ tactics/nbtermdn.cmx: tactics/btermdn.cmx kernel/generic.cmx lib/gmap.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ kernel/term.cmx tactics/termdn.cmx lib/util.cmx tactics/nbtermdn.cmi tactics/pattern.cmo: parsing/astterm.cmi proofs/clenv.cmi kernel/environ.cmi \ - kernel/evd.cmi kernel/generic.cmi library/global.cmi kernel/names.cmi \ - parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ - kernel/sosub.cmi tactics/stock.cmi kernel/term.cmi lib/util.cmi \ - tactics/pattern.cmi + kernel/evd.cmi kernel/generic.cmi library/global.cmi proofs/logic.cmi \ + kernel/names.cmi parsing/pcoq.cmi lib/pp.cmi proofs/proof_trees.cmi \ + kernel/reduction.cmi kernel/sosub.cmi tactics/stock.cmi kernel/term.cmi \ + lib/util.cmi tactics/pattern.cmi tactics/pattern.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/environ.cmx \ - kernel/evd.cmx kernel/generic.cmx library/global.cmx kernel/names.cmx \ - parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ - kernel/sosub.cmx tactics/stock.cmx kernel/term.cmx lib/util.cmx \ - tactics/pattern.cmi + kernel/evd.cmx kernel/generic.cmx library/global.cmx proofs/logic.cmx \ + kernel/names.cmx parsing/pcoq.cmx lib/pp.cmx proofs/proof_trees.cmx \ + kernel/reduction.cmx kernel/sosub.cmx tactics/stock.cmx kernel/term.cmx \ + lib/util.cmx tactics/pattern.cmi tactics/stock.cmo: lib/bij.cmi lib/gmap.cmi lib/gmapl.cmi library/library.cmi \ kernel/names.cmi lib/pp.cmi lib/util.cmi tactics/stock.cmi tactics/stock.cmx: lib/bij.cmx lib/gmap.cmx lib/gmapl.cmx library/library.cmx \ @@ -756,17 +765,17 @@ tactics/tacentries.cmx: proofs/proof_trees.cmx proofs/tacmach.cmx \ tactics/tacticals.cmo: proofs/clenv.cmi parsing/coqast.cmi \ library/declare.cmi kernel/environ.cmi kernel/generic.cmi \ library/global.cmi library/indrec.cmi kernel/inductive.cmi \ - kernel/names.cmi tactics/pattern.cmi lib/pp.cmi parsing/pretty.cmi \ - proofs/proof_trees.cmi kernel/reduction.cmi kernel/sign.cmi \ - proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ + proofs/logic.cmi kernel/names.cmi tactics/pattern.cmi lib/pp.cmi \ + parsing/pretty.cmi proofs/proof_trees.cmi kernel/reduction.cmi \ + kernel/sign.cmi proofs/tacinterp.cmi proofs/tacmach.cmi kernel/term.cmi \ parsing/termast.cmi lib/util.cmi tactics/wcclausenv.cmi \ tactics/tacticals.cmi tactics/tacticals.cmx: proofs/clenv.cmx parsing/coqast.cmx \ library/declare.cmx kernel/environ.cmx kernel/generic.cmx \ library/global.cmx library/indrec.cmx kernel/inductive.cmx \ - kernel/names.cmx tactics/pattern.cmx lib/pp.cmx parsing/pretty.cmx \ - proofs/proof_trees.cmx kernel/reduction.cmx kernel/sign.cmx \ - proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ + proofs/logic.cmx kernel/names.cmx tactics/pattern.cmx lib/pp.cmx \ + parsing/pretty.cmx proofs/proof_trees.cmx kernel/reduction.cmx \ + kernel/sign.cmx proofs/tacinterp.cmx proofs/tacmach.cmx kernel/term.cmx \ parsing/termast.cmx lib/util.cmx tactics/wcclausenv.cmx \ tactics/tacticals.cmi tactics/tactics.cmo: parsing/ast.cmi parsing/astterm.cmi proofs/clenv.cmi \ diff --git a/dev/changements.txt b/dev/changements.txt index da1b10255..d13fb1e83 100644 --- a/dev/changements.txt +++ b/dev/changements.txt @@ -67,7 +67,7 @@ Changements dans les fonctions : mis_lc -> instantiate_lc Ex-Environ - mind_path -> Global.lookup_mind + mind_of_path -> Global.lookup_mind Printer gentermpr -> gen_pr_term @@ -76,6 +76,12 @@ Changements dans les fonctions : type_of_type -> judge_of_type fcn_proposition -> judge_of_prop_contents +Changements dans les inductifs +------------------------------ +Nouveaux types "constructor" et "inductive" dans Term +La plupart des fonctions de typage des inductives prennent maintenant +un inductive au lieu d'un oonstr comme argument. Les seules fonctions +à traduite un constr en inductive sont les find_mrectype and co. Changements dans les grammaires ------------------------------- diff --git a/kernel/environ.ml b/kernel/environ.ml index eaa87b5be..c8c85c76e 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -127,13 +127,10 @@ let lookup_constant sp env = let lookup_mind sp env = Spmap.find sp env.env_globals.env_inductives -let lookup_mind_specif i env = - match i with - | DOPN (MutInd (sp,tyi), args) -> - let mib = lookup_mind sp env in - { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args; - mis_mip = mind_nth_type_packet mib tyi } - | _ -> invalid_arg "lookup_mind_specif" +let lookup_mind_specif ((sp,tyi),args) env = + let mib = lookup_mind sp env in + { mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args; + mis_mip = mind_nth_type_packet mib tyi } let lookup_abst sp env = Spmap.find sp env.env_globals.env_abstractions diff --git a/kernel/environ.mli b/kernel/environ.mli index ffb5861e1..6d38ad819 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -46,7 +46,7 @@ val lookup_var : identifier -> env -> name * typed_type val lookup_rel : int -> env -> name * typed_type val lookup_constant : section_path -> env -> constant_body val lookup_mind : section_path -> env -> mutual_inductive_body -val lookup_mind_specif : constr -> env -> mind_specif +val lookup_mind_specif : inductive -> env -> mind_specif val id_of_global : env -> sorts oper -> identifier diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index da9604699..cdb45e9d4 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -111,7 +111,7 @@ let listrec_mconstr env ntypes nparams i indlc = let hd = array_hd cl and largs = array_tl cl in (match hd with - | Rel k -> + | Rel k -> if k >= n && k<n+ntypes then begin check_correct_par env nparams ntypes n (k-n+1) largs; Mrec(n+ntypes-k-1) @@ -121,17 +121,17 @@ let listrec_mconstr env ntypes nparams i indlc = else Norec else raise (IllFormedInd (NonPos n)) - | (DOPN(MutInd(sp,i),_) as mi) -> + | DOPN(MutInd ind_sp,a) -> if (noccur_bet n ntypes x) then Norec else - Imbr(sp,i,imbr_positive n mi largs) + Imbr(ind_sp,imbr_positive n (ind_sp,a) largs) | err -> if noccur_bet n ntypes x then Norec else raise (IllFormedInd (NonPos n))) | _ -> anomaly "check_pos") - and imbr_positive n mi largs = + and imbr_positive n mi largs = let mispeci = lookup_mind_specif mi env in let auxnpar = mis_nparams mispeci in let (lpar,auxlargs) = array_chop auxnpar largs in @@ -197,10 +197,10 @@ let listrec_mconstr env ntypes nparams i indlc = then Param(n-1-k) else Norec else raise (IllFormedInd (NonPos n)) - | (DOPN(MutInd(sp,i),_) as mi) -> + | DOPN(MutInd ind_sp,a) -> if (noccur_bet n ntypes x) then Norec - else Imbr(sp,i,imbr_positive n mi largs) + else Imbr(ind_sp,imbr_positive n (ind_sp,a) largs) | err -> if noccur_bet n ntypes x then Norec else raise (IllFormedInd (NonPos n))) | _ -> anomaly "check_param_pos") @@ -249,7 +249,7 @@ let listrec_mconstr env ntypes nparams i indlc = let is_recursive listind = let rec one_is_rec rvec = List.exists (function Mrec(i) -> List.mem i listind - | Imbr(_,_,lvec) -> one_is_rec lvec + | Imbr(_,lvec) -> one_is_rec lvec | Norec -> false | Param _ -> false) rvec in diff --git a/kernel/inductive.ml b/kernel/inductive.ml index e46be516a..41342e6d4 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -12,7 +12,7 @@ type recarg = | Param of int | Norec | Mrec of int - | Imbr of section_path * int * (recarg list) + | Imbr of inductive_path * recarg list type mutual_inductive_packet = { mind_consnames : identifier array; @@ -51,11 +51,22 @@ let mis_recarg mis = mis.mis_mip.mind_listrec let mis_typename mis = mis.mis_mip.mind_typename let mis_consnames mis = mis.mis_mip.mind_consnames +(* A light version of mind_specif_of_mind with pre-splitted args *) +type inductive_summary = + {fullmind : constr; + mind : inductive; + nparams : int; + nrealargs : int; + nconstr : int; + params : constr list; + realargs : constr list; + arity : constr} + let is_recursive listind = let rec one_is_rec rvec = List.exists (function | Mrec(i) -> List.mem i listind - | Imbr(_,_,lvec) -> one_is_rec lvec + | Imbr(_,lvec) -> one_is_rec lvec | Norec -> false | Param(_) -> false) rvec in @@ -158,4 +169,8 @@ let mind_check_lc params mie = in List.iter check_lc mie.mind_entry_inds -let inductive_of_constructor (ind_sp,i) = ind_sp +let inductive_path_of_constructor_path (ind_sp,i) = ind_sp +let ith_constructor_path_of_inductive_path ind_sp i = (ind_sp,i) + +let inductive_of_constructor ((ind_sp,i),args) = (ind_sp,args) +let ith_constructor_of_inductive (ind_sp,args) i = ((ind_sp,i),args) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 63e85a539..c28d35c8d 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -14,7 +14,7 @@ type recarg = | Param of int | Norec | Mrec of int - | Imbr of section_path * int * (recarg list) + | Imbr of inductive_path * (recarg list) type mutual_inductive_packet = { mind_consnames : identifier array; @@ -63,6 +63,20 @@ val mis_consnames : mind_specif -> identifier array val mind_nth_type_packet : mutual_inductive_body -> int -> mutual_inductive_packet +(* A light version of mind_specif_of_mind with pre-splitted args + Invariant: We have + -- Hnf (fullmind) = DOPN(AppL,[|MutInd mind;..params..;..realargs..|]) + -- with mind = ((sp,i),localvars) for some sp, i, localvars + *) +type inductive_summary = + {fullmind : constr; + mind : inductive; + nparams : int; + nrealargs : int; + nconstr : int; + params : constr list; + realargs : constr list; + arity : constr} (*s Declaration of inductive types. *) @@ -107,4 +121,11 @@ val mind_extract_params : int -> constr -> (name * constr) list * constr val mind_check_lc : (name * constr) list -> mutual_inductive_entry -> unit -val inductive_of_constructor : constructor_path -> inductive_path +val inductive_of_constructor : constructor -> inductive + +val ith_constructor_of_inductive : inductive -> int -> constructor + +val inductive_path_of_constructor_path : constructor_path -> inductive_path + +val ith_constructor_path_of_inductive_path : + inductive_path -> int -> constructor_path diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5b0fbe61c..84277eb22 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -15,7 +15,6 @@ open Instantiate open Closure exception Redelimination -exception Induc exception Elimconst type 'a reduction_function = env -> 'a evar_map -> constr -> constr @@ -480,9 +479,9 @@ let mind_nparams env i = let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams let reduce_mind_case env mia = - match mia.mconstr with - | DOPN(MutConstruct((indsp,tyindx),i),_) -> - let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in + match mia.mconstr with + | DOPN(MutConstruct (ind_sp,i as cstr_sp),args) -> + let ind = inductive_of_constructor (cstr_sp,args) in let nparams = mind_nparams env ind in let real_cargs = snd (list_chop nparams mia.mcargs) in applist (mia.mlf.(i-1),real_cargs) @@ -1125,47 +1124,42 @@ let whd_programs_stack env sigma = let whd_programs env sigma x = applist (whd_programs_stack env sigma x []) +exception Induc + let find_mrectype env sigma c = let (t,l) = whd_betadeltaiota_stack env sigma c [] in match t with - | DOPN(MutInd (sp,i),_) -> (t,l) + | DOPN(MutInd ind_sp,args) -> ((ind_sp,args),l) | _ -> raise Induc let find_minductype env sigma c = let (t,l) = whd_betadeltaiota_stack env sigma c [] in match t with | DOPN(MutInd (sp,i),_) - when mind_type_finite (lookup_mind sp env) i -> (t,l) + when mind_type_finite (lookup_mind sp env) i -> (destMutInd t,l) | _ -> raise Induc let find_mcoinductype env sigma c = let (t,l) = whd_betadeltaiota_stack env sigma c [] in match t with | DOPN(MutInd (sp,i),_) - when not (mind_type_finite (lookup_mind sp env) i) -> (t,l) + when not (mind_type_finite (lookup_mind sp env) i) -> (destMutInd t,l) | _ -> raise Induc -let minductype_spec env sigma c = - try - let (x,l) = find_minductype env sigma c in - if l<>[] then anomaly "minductype_spec: Not a recursive type 1" else x - with Induc -> - anomaly "minductype_spec: Not a recursive type 2" - -let mrectype_spec env sigma c = - try - let (x,l) = find_mrectype env sigma c in - if l<>[] then anomaly "mrectype_spec: Not a recursive type 1" else x - with Induc -> - anomaly "mrectype_spec: Not a recursive type 2" - -let check_mrectype_spec env sigma c = - try - let (x,l) = find_mrectype env sigma c in - if l<>[] then error "check_mrectype: Not a recursive type 1" else x - with Induc -> - error "check_mrectype: Not a recursive type 2" - +(* raise Induc if not an inductive type *) +let try_mutind_of env sigma ty = + let (mind,largs) = find_mrectype env sigma ty in + let mispec = lookup_mind_specif mind env in + let nparams = mis_nparams mispec in + let (params,realargs) = list_chop nparams largs in + {fullmind = ty; + mind = mind; + nparams = nparams; + nrealargs = List.length realargs; + nconstr = mis_nconstr mispec; + params = params; + realargs = realargs; + arity = Instantiate.mis_arity mispec} exception IsType diff --git a/kernel/reduction.mli b/kernel/reduction.mli index dd06af8ad..6638f30ee 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -14,7 +14,6 @@ open Closure (* Reduction Functions. *) exception Redelimination -exception Induc exception Elimconst type 'a reduction_function = env -> 'a evar_map -> constr -> constr @@ -191,18 +190,25 @@ val whd_ise1 : 'a evar_map -> constr -> constr val nf_ise1 : 'a evar_map -> constr -> constr val whd_ise1_metas : 'a evar_map -> constr -> constr - (*s Obsolete Reduction Functions *) val hnf : env -> 'a evar_map -> constr -> constr * constr list val apprec : 'a stack_reduction_function val red_product : 'a reduction_function -val find_mrectype : - env -> 'a evar_map -> constr -> constr * constr list -val find_minductype : - env -> 'a evar_map -> constr -> constr * constr list -val find_mcoinductype : - env -> 'a evar_map -> constr -> constr * constr list -val check_mrectype_spec : env -> 'a evar_map -> constr -> constr -val minductype_spec : env -> 'a evar_map -> constr -> constr -val mrectype_spec : env -> 'a evar_map -> constr -> constr + +(* [find_m*type env sigma c] coerce [c] to an recursive type (I args). + [find_mrectype], [find_minductype] and [find_mcoinductype] + respectively accepts any recursive type, only an inductive type and + only a coinductive type. + They raise [Induc] if not convertible to a recursive type. *) + +exception Induc +val find_mrectype : env -> 'a evar_map -> constr -> inductive * constr list +val find_minductype : env -> 'a evar_map -> constr -> inductive * constr list +val find_mcoinductype : env -> 'a evar_map -> constr -> inductive * constr list + +(* [try_mutind_of env sigma t] raises [Induc] if [t] is not an inductive type*) +(* The resulting summary is relative to the current env *) +val try_mutind_of : env -> 'a evar_map -> constr -> Inductive.inductive_summary + + diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 2c7829ef9..d7f8b8386 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -57,15 +57,14 @@ let rec execute mf env cstr = else error "Cannot typecheck an unevaluable abstraction" - | IsConst _ -> - (make_judge cstr (type_of_constant env Evd.empty cstr), cst0) + | IsConst c -> + (make_judge cstr (type_of_constant env Evd.empty c), cst0) - | IsMutInd _ -> - (make_judge cstr (type_of_inductive env Evd.empty cstr), cst0) + | IsMutInd ind -> + (make_judge cstr (type_of_inductive env Evd.empty ind), cst0) - | IsMutConstruct (sp,i,j,args) -> - let (typ,kind) = - destCast (type_of_constructor env Evd.empty (((sp,i),j),args)) in + | IsMutConstruct c -> + let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0) | IsMutCase (_,p,c,lf) -> diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 314796ee6..afa8d3ef9 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -44,7 +44,7 @@ val lookup_var : identifier -> safe_environment -> name * typed_type val lookup_rel : int -> safe_environment -> name * typed_type val lookup_constant : section_path -> safe_environment -> constant_body val lookup_mind : section_path -> safe_environment -> mutual_inductive_body -val lookup_mind_specif : constr -> safe_environment -> mind_specif +val lookup_mind_specif : inductive -> safe_environment -> mind_specif val export : safe_environment -> string -> compiled_env val import : compiled_env -> safe_environment -> safe_environment diff --git a/kernel/term.ml b/kernel/term.ml index f2e8d3422..56dd87f8f 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -32,7 +32,7 @@ type 'a oper = (* an extra slot, for putting in whatever sort of operator we need for whatever sort of application *) -and case_info = inductive_path option +and case_info = inductive_path (* Sorts. *) @@ -148,7 +148,7 @@ let mkAppList a l = DOPN (AppL, Array.of_list (a::l)) (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) -let mkConst sp a = DOPN (Const sp, a) +let mkConst (sp,a) = DOPN (Const sp, a) (* Constructs an existential variable *) let mkEvar n a = DOPN (Evar n, a) @@ -158,12 +158,12 @@ let mkAbst sp a = DOPN (Abst sp, a) (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) -let mkMutInd sp i l = (DOPN (MutInd (sp,i), l)) +let mkMutInd (ind_sp,l) = DOPN (MutInd ind_sp, l) (* Constructs the jth constructor of the ith (co)inductive type of the block named sp. The array of terms correspond to the variables introduced in the section *) -let mkMutConstruct sp i j l = (DOPN ((MutConstruct ((sp,i),j),l))) +let mkMutConstruct (cstr_sp,l) = DOPN (MutConstruct cstr_sp,l) (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) let mkMutCase ci p c ac = @@ -439,24 +439,22 @@ let args_of_abst = function (* Destructs a (co)inductive type named sp *) let destMutInd = function - | DOPN (MutInd (sp,i), l) -> (sp,i,l) + | DOPN (MutInd ind_sp, l) -> (ind_sp,l) | _ -> invalid_arg "destMutInd" let op_of_mind = function - | DOPN(MutInd (sp,i),_) -> (sp,i) + | DOPN(MutInd ind_sp,_) -> ind_sp | _ -> anomaly "op_of_mind called with bad args" let args_of_mind = function | DOPN(MutInd _,args) -> args | _ -> anomaly "args_of_mind called with bad args" -let ci_of_mind = function - | DOPN(MutInd(sp,tyi),_) -> Some (sp,tyi) - | _ -> invalid_arg "ci_of_mind" +let ci_of_mind = op_of_mind (* Destructs a constructor *) let destMutConstruct = function - | DOPN (MutConstruct ((sp,i),j),l) -> (sp,i,j,l) + | DOPN (MutConstruct cstr_sp,l) -> (cstr_sp,l) | _ -> invalid_arg "dest" let op_of_mconstr = function @@ -528,6 +526,11 @@ let destUntypedCoFix = function (* Term analysis *) (******************) +type existential = int * constr array +type constant = section_path * constr array +type constructor = constructor_path * constr array +type inductive = inductive_path * constr array + type kindOfTerm = | IsRel of int | IsMeta of int @@ -538,11 +541,11 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsAppL of constr * constr list - | IsConst of section_path * constr array | IsAbst of section_path * constr array - | IsEvar of int * constr array - | IsMutInd of section_path * int * constr array - | IsMutConstruct of section_path * int * int * constr array + | IsEvar of existential + | IsConst of constant + | IsMutInd of inductive + | IsMutConstruct of constructor | IsMutCase of case_info * constr * constr * constr array | IsFix of int array * int * constr array * name list * constr array | IsCoFix of int * constr array * name list * constr array @@ -569,8 +572,8 @@ let kind_of_term c = | DOPN (Const sp, a) -> IsConst (sp,a) | DOPN (Evar sp, a) -> IsEvar (sp,a) | DOPN (Abst sp, a) -> IsAbst (sp, a) - | DOPN (MutInd (sp,i), l) -> IsMutInd (sp,i,l) - | DOPN (MutConstruct ((sp,i), j),l) -> IsMutConstruct (sp,i,j,l) + | DOPN (MutInd ind_sp, l) -> IsMutInd (ind_sp,l) + | DOPN (MutConstruct cstr_sp,l) -> IsMutConstruct (cstr_sp,l) | DOPN (MutCase ci,v) -> IsMutCase (ci,v.(0),v.(1),Array.sub v 2 (Array.length v - 2)) | DOPN ((Fix (recindxs,i),a)) -> @@ -1316,7 +1319,7 @@ module Hoper = | Abst sp -> Abst (hsp sp) | MutInd (sp,i) -> MutInd (hsp sp, i) | MutConstruct ((sp,i),j) -> MutConstruct ((hsp sp,i),j) - | MutCase(Some (sp,i)) -> MutCase(Some (hsp sp, i)) + | MutCase(sp,i) -> MutCase(hsp sp, i) | t -> t let equal o1 o2 = match (o1,o2) with @@ -1327,7 +1330,7 @@ module Hoper = | (MutInd (sp1,i1), MutInd (sp2,i2)) -> sp1==sp2 & i1=i2 | (MutConstruct((sp1,i1),j1), MutConstruct((sp2,i2),j2)) -> sp1==sp2 & i1=i2 & j1=j2 - | (MutCase(Some (sp1,i1)),MutCase(Some (sp2,i2))) -> sp1==sp2 & i1=i2 + | (MutCase(sp1,i1),MutCase(sp2,i2)) -> sp1==sp2 & i1=i2 | _ -> o1=o2 let hash = Hashtbl.hash end) diff --git a/kernel/term.mli b/kernel/term.mli index 2530c18e1..a7f2e6180 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -26,7 +26,7 @@ type 'a oper = | CoFix of int | XTRA of string -and case_info = inductive_path option +and case_info = inductive_path (*s The sorts of CCI. *) @@ -73,6 +73,10 @@ val outcast_type : constr -> typed_type previous ones. *) (* Concrete type for making pattern-matching. *) +type existential = int * constr array +type constant = section_path * constr array +type constructor = constructor_path * constr array +type inductive = inductive_path * constr array type kindOfTerm = | IsRel of int @@ -84,11 +88,11 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsAppL of constr * constr list - | IsConst of section_path * constr array | IsAbst of section_path * constr array - | IsEvar of int * constr array - | IsMutInd of section_path * int * constr array - | IsMutConstruct of section_path * int * int * constr array + | IsEvar of existential + | IsConst of constant + | IsMutInd of inductive + | IsMutConstruct of constructor | IsMutCase of case_info * constr * constr * constr array | IsFix of int array * int * constr array * name list * constr array | IsCoFix of int * constr array * name list * constr array @@ -158,7 +162,7 @@ val mkAppList : constr -> constr list -> constr (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) -val mkConst : section_path -> constr array -> constr +val mkConst : constant -> constr (* Constructs an existential variable *) val mkEvar : int -> constr array -> constr @@ -168,12 +172,12 @@ val mkAbst : section_path -> constr array -> constr (* Constructs the ith (co)inductive type of the block named sp *) (* The array of terms correspond to the variables introduced in the section *) -val mkMutInd : section_path -> int -> constr array -> constr +val mkMutInd : inductive -> constr (* Constructs the jth constructor of the ith (co)inductive type of the block named sp. The array of terms correspond to the variables introduced in the section *) -val mkMutConstruct : section_path -> int -> int -> constr array -> constr +val mkMutConstruct : constructor -> constr (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) val mkMutCase : case_info -> constr -> constr -> constr list -> constr @@ -291,13 +295,13 @@ val path_of_abst : constr -> section_path val args_of_abst : constr -> constr array (* Destructs a (co)inductive type *) -val destMutInd : constr -> section_path * int * constr array +val destMutInd : constr -> inductive val op_of_mind : constr -> inductive_path val args_of_mind : constr -> constr array val ci_of_mind : constr -> case_info (* Destructs a constructor *) -val destMutConstruct : constr -> section_path * int * int * constr array +val destMutConstruct : constr -> constructor val op_of_mconstr : constr -> constructor_path val args_of_mconstr : constr -> constr array diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 02db98b98..3cca1c694 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -33,7 +33,7 @@ type type_error = | NotClean of int * constr | VarNotFound of identifier (* Pattern-matching errors *) - | BadConstructor of constructor_path * inductive_path + | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor_path * int | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 1c0df5a31..66242b7cf 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -35,7 +35,7 @@ type type_error = | NotClean of int * constr | VarNotFound of identifier (* Pattern-matching errors *) - | BadConstructor of constructor_path * inductive_path + | BadConstructor of constructor * inductive | WrongNumargConstructor of constructor_path * int | WrongPredicateArity of constr * int * int | NeedsInversion of constr * constr diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9fb263c59..1254d5ef9 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -81,8 +81,7 @@ let check_hyps id env sigma hyps = (* Instantiation of terms on real arguments. *) -let type_of_constant env sigma c = - let (sp,args) = destConst c in +let type_of_constant env sigma (sp,args) = let cb = lookup_constant sp env in let hyps = cb.const_hyps in check_hyps (basename sp) env sigma hyps; @@ -110,8 +109,8 @@ let instantiate_lc mis = let lc = mis.mis_mip.mind_lc in instantiate_constr (ids_of_sign hyps) lc (Array.to_list mis.mis_args) -let type_of_constructor env sigma ((ind_sp,j),args) = - let mind = DOPN (MutInd ind_sp, args) in +let type_of_constructor env sigma ((ind_sp,j),args as cstr) = + let mind = inductive_of_constructor cstr in let mis = lookup_mind_specif mind env in check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps); let specif = instantiate_lc mis in @@ -137,8 +136,7 @@ let mis_type_mconstructs mis = sAPPVList specif (list_tabulate make_ik ntypes)) let type_mconstructs env sigma mind = - let redmind = check_mrectype_spec env sigma mind in - let mis = lookup_mind_specif redmind env in + let mis = lookup_mind_specif mind env in mis_type_mconstructs mis let mis_type_mconstruct i mispec = @@ -150,21 +148,13 @@ let mis_type_mconstruct i mispec = sAPPViList (i-1) specif (list_tabulate make_Ik ntypes) let type_mconstruct env sigma i mind = - let redmind = check_mrectype_spec env sigma mind in - let (sp,tyi,args) = destMutInd redmind in - let mispec = lookup_mind_specif redmind env in - mis_type_mconstruct i mispec + let mis = lookup_mind_specif mind env in + mis_type_mconstruct i mis -let type_inst_construct env sigma i mind = - try - let (mI,largs) = find_mrectype env sigma mind in - let mispec = lookup_mind_specif mI env in - let nparams = mis_nparams mispec in - let tc = mis_type_mconstruct i mispec in - let (globargs,_) = list_chop nparams largs in +let type_inst_construct env sigma i (mind,globargs) = + let mis = lookup_mind_specif mind env in + let tc = mis_type_mconstruct i mis in hnf_prod_applist env sigma "Typing.type_construct" tc globargs - with Induc -> - error_not_inductive CCI env mind let type_of_existential env sigma c = let (ev,args) = destEvar c in @@ -262,7 +252,7 @@ let find_case_dep_nparams env sigma (c,p) (mind,largs) typP = and t = cast_instantiate_arity mis in let (globargs,la) = list_chop nparams largs in let glob_t = hnf_prod_applist env sigma "find_elim_boolean" t globargs in - let arity = applist(mind,globargs) in + let arity = applist(mkMutInd mind,globargs) in let (dep,_) = is_correct_arity env sigma kelim (c,p) arity (typP,glob_t) in (dep, (nparams, globargs,la)) @@ -297,11 +287,12 @@ let type_one_branch_nodep env sigma (nparams,globargs,p) t = let type_case_branches env sigma ct pt p c = try - let ((mI,largs) as indt) = find_mrectype env sigma ct in + let (mind,largs) = find_mrectype env sigma ct in let (dep,(nparams,globargs,la)) = - find_case_dep_nparams env sigma (c,p) indt pt + find_case_dep_nparams env sigma (c,p) (mind,largs) pt in - let (lconstruct,ltypconstr) = type_mconstructs env sigma mI in + let (lconstruct,ltypconstr) = type_mconstructs env sigma mind in + let mI = mkMutInd mind in if dep then (mI, array_map2 (type_one_branch_dep env sigma (nparams,globargs,p)) @@ -502,8 +493,8 @@ let map_lift_fst = map_lift_fst_n 1 let rec instantiate_recarg sp lrc ra = match ra with - | Mrec(j) -> Imbr(sp,j,lrc) - | Imbr(sp1,k,l) -> Imbr(sp1,k, List.map (instantiate_recarg sp lrc) l) + | Mrec(j) -> Imbr((sp,j),lrc) + | Imbr(ind_sp,l) -> Imbr(ind_sp, List.map (instantiate_recarg sp lrc) l) | Norec -> Norec | Param(k) -> List.nth lrc k @@ -520,10 +511,10 @@ let check_term env mind_recvec f = | (Mrec(i)::lr,DOP2(Lambda,_,DLAM(_,b))) -> let l' = map_lift_fst l in crec (n+1) ((1,mind_recvec.(i))::l') (lr,b) - | (Imbr(sp,i,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> + | (Imbr((sp,i) as ind_sp,lrc)::lr,DOP2(Lambda,_,DLAM(_,b))) -> let l' = map_lift_fst l in let sprecargs = - mis_recargs (lookup_mind_specif (mkMutInd sp i [||]) env) in + mis_recargs (lookup_mind_specif (ind_sp,[||]) env) in let lc = Array.map (List.map (instantiate_recarg sp lrc)) sprecargs.(i) in @@ -618,11 +609,10 @@ let rec check_subterm_rec_meta env sigma vectn k def = error "Bad occurrence of recursive call" | _ -> error "Not enough abstractions in the definition") in let (c,d) = check_occur 1 def in - let (mI, largs) = + let ((sp,tyi),_ as mind, largs) = (try find_minductype env sigma c with Induc -> error "Recursive definition on a non inductive type") in - let (sp,tyi,_) = destMutInd mI in - let mind_recvec = mis_recargs (lookup_mind_specif mI env) in + let mind_recvec = mis_recargs (lookup_mind_specif mind env) in let lcx = mind_recvec.(tyi) in (* n = decreasing argument in the definition; lst = a mapping var |-> recargs @@ -771,7 +761,8 @@ let check_fix env sigma = function (* Co-fixpoints. *) let mind_nparams env i = - let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let mis = lookup_mind_specif i env in + mis.mis_mib.mind_nparams let check_guard_rec_meta env sigma nbfix def deftype = let rec codomain_is_coind c = @@ -781,11 +772,11 @@ let check_guard_rec_meta env sigma nbfix def deftype = (try find_mcoinductype env sigma b with | Induc -> error "The codomain is not a coinductive type" - | _ -> error "Type of Cofix function not as expected") +(* | _ -> error "Type of Cofix function not as expected") ??? *) ) in - let (mI, _) = codomain_is_coind deftype in - let (sp,tyi,_) = destMutInd mI in - let lvlra = (mis_recargs (lookup_mind_specif mI env)) in + let (mind, _) = codomain_is_coind deftype in + let ((sp,tyi),_) = mind in + let lvlra = (mis_recargs (lookup_mind_specif mind env)) in let vlra = lvlra.(tyi) in let rec check_rec_call alreadygrd n vlra t = if noccur_with_meta n nbfix t then @@ -807,9 +798,9 @@ let check_guard_rec_meta env sigma nbfix def deftype = else error "check_guard_rec_meta: ???" - | (DOPN ((MutConstruct((x,y),i)),l), args) -> + | (DOPN (MutConstruct(_,i as cstr_sp),l), args) -> let lra =vlra.(i-1) in - let mI = DOPN(MutInd(x,y),l) in + let mI = inductive_of_constructor (cstr_sp,l) in let _,realargs = list_chop (mind_nparams env mI) args in let rec process_args_of_constr l lra = match l with @@ -825,9 +816,9 @@ let check_guard_rec_meta env sigma nbfix def deftype = (check_rec_call true n newvlra t) && (process_args_of_constr lr lrar) - | (Imbr(sp,i,lrc)::lrar) -> + | (Imbr((sp,i) as ind_sp,lrc)::lrar) -> let mis = - lookup_mind_specif (mkMutInd sp i [||]) env in + lookup_mind_specif (ind_sp,[||]) env in let sprecargs = mis_recargs mis in let lc = (Array.map (List.map diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 55191e284..a7aec8cde 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -27,12 +27,11 @@ val assumption_of_judgment : val relative : env -> int -> unsafe_judgment -val type_of_constant : env -> 'a evar_map -> constr -> typed_type +val type_of_constant : env -> 'a evar_map -> constant -> typed_type -val type_of_inductive : env -> 'a evar_map -> constr -> typed_type +val type_of_inductive : env -> 'a evar_map -> inductive -> typed_type -val type_of_constructor : - env -> 'a evar_map -> (constructor_path * constr array) -> constr +val type_of_constructor : env -> 'a evar_map -> constructor -> constr val type_of_existential : env -> 'a evar_map -> constr -> constr @@ -89,10 +88,12 @@ val make_arity_nodep : val find_case_dep_nparams : env -> 'a evar_map -> constr * constr -> - constr * constr list -> + inductive * constr list -> constr -> bool * (int * constr list * constr list) -val type_inst_construct : env -> 'a evar_map -> int -> constr -> constr +(* The constr list is the global args list *) +val type_inst_construct : + env -> 'a evar_map -> int -> inductive * constr list -> constr val hyps_inclusion : env -> 'a evar_map -> var_context -> var_context -> bool diff --git a/library/declare.ml b/library/declare.ml index 8766467fc..ff46ad72a 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -274,19 +274,19 @@ let is_global id = with Not_found -> false -let mind_path = function - | DOPN(MutInd (sp,0),_) -> sp - | DOPN(MutInd (sp,tyi),_) -> - let mib = Global.lookup_mind sp in - let mip = mind_nth_type_packet mib tyi in - let (pa,_,k) = repr_path sp in - Names.make_path pa (mip.mind_typename) k - | DOPN(MutConstruct ((sp,tyi),ind),_) -> - let mib = Global.lookup_mind sp in - let mip = mind_nth_type_packet mib tyi in - let (pa,_,k) = repr_path sp in - Names.make_path pa (mip.mind_consnames.(ind-1)) k - | _ -> invalid_arg "mind_path" +let path_of_constructor_path ((sp,tyi),ind) = + let mib = Global.lookup_mind sp in + let mip = mind_nth_type_packet mib tyi in + let (pa,_,k) = repr_path sp in + Names.make_path pa (mip.mind_consnames.(ind-1)) k + +let path_of_inductive_path (sp,tyi) = + if tyi = 0 then sp + else + let mib = Global.lookup_mind sp in + let mip = mind_nth_type_packet mib tyi in + let (pa,_,k) = repr_path sp in + Names.make_path pa (mip.mind_typename) k (* Eliminations. *) @@ -294,8 +294,8 @@ let declare_eliminations sp i = let oper = MutInd (sp,i) in let mib = Global.lookup_mind sp in let ids = ids_of_sign mib.mind_hyps in - let mind = DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) in - let mispec = Global.lookup_mind_specif mind in + let ctxt = Array.of_list (List.map (fun id -> VAR id) ids) in + let mispec = Global.lookup_mind_specif ((sp,i),ctxt) in let mindstr = string_of_id (mis_typename mispec) in let declare na c = declare_constant (id_of_string na) diff --git a/library/declare.mli b/library/declare.mli index c4644b465..8541c2092 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -71,4 +71,5 @@ val construct_reference : Environ.env -> path_kind -> identifier -> constr val is_global : identifier -> bool -val mind_path : constr -> section_path +val path_of_inductive_path : inductive_path -> section_path +val path_of_constructor_path : constructor_path -> section_path diff --git a/library/global.mli b/library/global.mli index a61b09c58..e9e42cf5e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -34,7 +34,7 @@ val lookup_var : identifier -> name * typed_type val lookup_rel : int -> name * typed_type val lookup_constant : section_path -> constant_body val lookup_mind : section_path -> mutual_inductive_body -val lookup_mind_specif : constr -> mind_specif +val lookup_mind_specif : inductive -> mind_specif val export : string -> compiled_env val import : compiled_env -> unit @@ -46,10 +46,10 @@ val id_of_global : sorts oper -> identifier (*s Re-exported functions of [Inductive], composed with [lookup_mind_specif]. *) -val mind_is_recursive : constr -> bool -val mind_nconstr : constr -> int -val mind_nparams : constr -> int -val mind_arity : constr -> constr +val mind_is_recursive : inductive -> bool +val mind_nconstr : inductive -> int +val mind_nparams : inductive -> int +val mind_arity : inductive -> constr -val mind_lc_without_abstractions : constr -> constr array +val mind_lc_without_abstractions : inductive -> constr array diff --git a/library/indrec.ml b/library/indrec.ml index d24120bf0..2d1761daf 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -97,8 +97,7 @@ let mis_make_case_com depopt env sigma mispec kinds = in it_lambda_name env (make_lambda_string "P" typP (add_branch 0)) lnamespar -let make_case_com depopt env sigma mind kinds = - let ity = mrectype_spec env sigma mind in +let make_case_com depopt env sigma ity kinds = let mispec = lookup_mind_specif ity env in mis_make_case_com depopt env sigma mispec kinds @@ -356,11 +355,6 @@ let mis_make_indrec env sigma listdepkind mispec = in Array.init nrec make_one_rec -let make_indrec env sigma listdepkind mind = - let ity = minductype_spec env sigma mind in - let mispec = lookup_mind_specif ity env in - mis_make_indrec env sigma listdepkind mispec - let change_sort_arity sort = let rec drec = function | (DOP2(Cast,c,t)) -> drec c @@ -394,24 +388,25 @@ let check_arities listdepkind = 'sTR "is not allowed">]) listdepkind +(* Utilisé pour construire les Scheme *) let build_indrec env sigma = function | (mind,dep,s)::lrecspec -> - let redind = minductype_spec env sigma mind in - let (sp,tyi,_) = destMutInd redind in + let ((sp,tyi),_) = mind in + let mispec = lookup_mind_specif mind env in let listdepkind = - (lookup_mind_specif redind env, dep,s):: - (List.map (function (mind',dep',s') -> - let redind' = minductype_spec env sigma mind' in - let (sp',_,_) = destMutInd redind' in - if sp=sp' then - (lookup_mind_specif redind' env,dep',s') - else - error - "Induction schemes concern mutually inductive types") + (mispec, dep,s):: + (List.map + (function (mind',dep',s') -> + let ((sp',_),_) = mind' in + if sp=sp' then + (lookup_mind_specif mind' env,dep',s') + else + error + "Induction schemes concern mutually inductive types") lrecspec) in let _ = check_arities listdepkind in - make_indrec env sigma listdepkind mind + mis_make_indrec env sigma listdepkind mispec | _ -> assert false @@ -433,7 +428,7 @@ let type_mutind_rec env sigma ct pt p c = let (constrvec,typeconstrvec) = mis_type_mconstructs mispec in let lft = array_map3 (type_rec_branch dep env sigma (vargs,depPvec,0)) constrvec typeconstrvec recargs in - (mI, lft, + (mkMutInd mI, lft, if dep then applist(p,realargs@[c]) else applist(p,realargs) ) else @@ -476,7 +471,7 @@ let norec_branch_scheme env sigma typc = in crec typc -let rec_branch_scheme env sigma j typc recargs = +let rec_branch_scheme env sigma ((sp,j),_) typc recargs = let rec crec (typc,recargs) = match whd_betadeltaiota env sigma typc, recargs with | (DOP2(Prod,c,DLAM(name,t)),(ra::reca)) -> @@ -493,14 +488,12 @@ let rec_branch_scheme env sigma j typc recargs = in crec (typc,recargs) -let branch_scheme env sigma isrec i mind = - let typc = type_inst_construct env sigma i mind in +let branch_scheme env sigma isrec i (mind,args as appmind) = + let typc = type_inst_construct env sigma i appmind in if isrec then - let (mI,_) = find_mrectype env sigma mind in - let (_,j,_) = destMutInd mI in - let mispec = lookup_mind_specif mI env in + let mispec = lookup_mind_specif mind env in let recarg = (mis_recarg mispec).(i-1) in - rec_branch_scheme env sigma j typc recarg + rec_branch_scheme env sigma mind typc recarg else norec_branch_scheme env sigma typc @@ -522,44 +515,33 @@ let build_notdep_pred env sigma mispec nparams globargs pred = in finalpred -let pred_case_ml_fail env sigma isrec ct (i,ft) = - try - let (mI,largs) = find_mrectype env sigma ct in - let (_,j,_) = destMutInd mI in - let mispec = lookup_mind_specif mI env in - let nparams = mis_nparams mispec in - let (globargs,la) = list_chop nparams largs in - let pred = - let recargs = (mis_recarg mispec) in - assert (Array.length recargs <> 0); - let recargi = recargs.(i-1) in - let nbrec = if isrec then count_rec_arg j recargi else 0 in - let nb_arg = List.length (recargs.(i-1)) + nbrec in - let pred = concl_n env sigma nb_arg ft in - if noccur_bet 1 nb_arg pred then - lift (-nb_arg) pred - else - failwith "Dependent" - in - if la = [] then - pred - else (* we try with [_:T1]..[_:Tn](lift n pred) *) - build_notdep_pred env sigma mispec nparams globargs pred - with Induc -> - failwith "Inductive" +let pred_case_ml_fail env sigma isrec (mI,globargs,la) (i,ft) = + let (_,j),_ = mI in + let mispec = lookup_mind_specif mI env in + let nparams = mis_nparams mispec in + let pred = + let recargs = (mis_recarg mispec) in + assert (Array.length recargs <> 0); + let recargi = recargs.(i-1) in + let nbrec = if isrec then count_rec_arg j recargi else 0 in + let nb_arg = List.length (recargs.(i-1)) + nbrec in + let pred = concl_n env sigma nb_arg ft in + if noccur_bet 1 nb_arg pred then + lift (-nb_arg) pred + else + failwith "Dependent" + in + if la = [] then + pred + else (* we try with [_:T1]..[_:Tn](lift n pred) *) + build_notdep_pred env sigma mispec nparams globargs pred let pred_case_ml env sigma isrec (c,ct) lf (i,ft) = - try pred_case_ml_fail env sigma isrec ct (i,ft) - with Failure mes -> - error_ml_case CCI env mes c ct lf.(i-1) ft (* similar to pred_case_ml but does not expect the list lf of braches *) let pred_case_ml_onebranch env sigma isrec (c,ct) (i,f,ft) = - try pred_case_ml_fail env sigma isrec ct (i,ft) - with Failure mes -> - error_ml_case CCI env mes c ct f ft let make_case_ml isrec pred c ci lf = if isrec then diff --git a/library/indrec.mli b/library/indrec.mli index f1d1b5190..4b078c4f1 100644 --- a/library/indrec.mli +++ b/library/indrec.mli @@ -11,12 +11,9 @@ open Evd (* Eliminations. *) -val make_case_dep : env -> 'a evar_map -> constr -> sorts -> constr -val make_case_nodep : env -> 'a evar_map -> constr -> sorts -> constr -val make_case_gen : env -> 'a evar_map -> constr -> sorts -> constr - -val make_indrec : env -> 'a evar_map -> - (mind_specif * bool * sorts) list -> constr -> constr array +val make_case_dep : env -> 'a evar_map -> inductive -> sorts -> constr +val make_case_nodep : env -> 'a evar_map -> inductive -> sorts -> constr +val make_case_gen : env -> 'a evar_map -> inductive -> sorts -> constr val mis_make_indrec : env -> 'a evar_map -> (mind_specif * bool * sorts) list -> mind_specif -> constr array @@ -24,7 +21,7 @@ val mis_make_indrec : env -> 'a evar_map -> val instanciate_indrec_scheme : sorts -> int -> constr -> constr val build_indrec : - env -> 'a evar_map -> (constr * bool * sorts) list -> constr array + env -> 'a evar_map -> (inductive * bool * sorts) list -> constr array val type_rec_branches : bool -> env -> 'c evar_map -> constr -> constr -> constr -> constr -> constr * constr array * constr @@ -42,13 +39,18 @@ i*) val is_mutind : env -> 'a evar_map -> constr -> bool val branch_scheme : - env -> 'a evar_map -> bool -> int -> constr -> constr + env -> 'a evar_map -> bool -> int -> inductive * constr list -> constr + +(* In [inductive * constr list * constr list], the second argument is + the list of global parameters and the third the list of real args *) -val pred_case_ml : env -> 'c evar_map -> bool -> (constr * constr) - -> constr array -> (int*constr) ->constr +val pred_case_ml : env -> 'c evar_map -> bool -> + constr * (inductive * constr list * constr list) + -> constr array -> int * constr ->constr val pred_case_ml_onebranch : env ->'c evar_map -> bool -> - constr * constr ->int * constr * constr -> constr + constr * (inductive * constr list * constr list) + -> int * constr * constr -> constr val make_case_ml : bool -> constr -> constr -> case_info -> constr array -> constr diff --git a/parsing/printer.ml b/parsing/printer.ml index fcda9fb93..392078611 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -38,15 +38,15 @@ let pr_qualified sp id = else [< 'sTR(string_of_path sp) >] -let pr_constant sp = pr_qualified sp (basename sp) +let pr_constant (sp,_) = pr_qualified sp (basename sp) -let pr_existential ev = [< 'sTR ("?" ^ string_of_int ev) >] +let pr_existential (ev,_) = [< 'sTR ("?" ^ string_of_int ev) >] -let pr_inductive (sp,tyi as ind_sp) = +let pr_inductive (sp,tyi as ind_sp,_) = let id = id_of_global (MutInd ind_sp) in pr_qualified sp id -let pr_constructor ((sp,tyi),i as cstr_sp) = +let pr_constructor ((sp,tyi),i as cstr_sp,_) = let id = id_of_global (MutConstruct cstr_sp) in pr_qualified sp id @@ -62,16 +62,16 @@ let globpr k gt = match gt with | Nvar(_,s) -> [< 'sTR s >] | Node(_,"EVAR", (Num (_,ev))::_) -> if !print_arguments then dfltpr gt - else pr_existential ev + else pr_existential (ev,[]) | Node(_,"CONST",(Path(_,sl,s))::_) -> if !print_arguments then dfltpr gt - else pr_constant (section_path sl s) + else pr_constant (section_path sl s,[]) | Node(_,"MUTIND",(Path(_,sl,s))::(Num(_,tyi))::_) -> if !print_arguments then (dfltpr gt) - else pr_inductive (section_path sl s,tyi) + else pr_inductive ((section_path sl s,tyi),[]) | Node(_,"MUTCONSTRUCT",(Path(_,sl,s))::(Num(_,tyi))::(Num(_,i))::_) -> if !print_arguments then (dfltpr gt) - else pr_constructor ((section_path sl s,tyi),i) + else pr_constructor (((section_path sl s,tyi),i),[]) | gt -> dfltpr gt let apply_prec = Some (("Term",(9,0,0)),Extend.L) diff --git a/parsing/printer.mli b/parsing/printer.mli index 217ec6197..0f704c552 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -27,10 +27,10 @@ val pr_ne_env : std_ppcmds -> path_kind -> context -> std_ppcmds val prrawterm : Rawterm.rawconstr -> std_ppcmds val prpattern : Rawterm.pattern -> std_ppcmds -val pr_constant : section_path -> std_ppcmds -val pr_existential : existential_key -> std_ppcmds -val pr_constructor : constructor_path -> std_ppcmds -val pr_inductive : inductive_path -> std_ppcmds +val pr_constant : constant -> std_ppcmds +val pr_existential : existential -> std_ppcmds +val pr_constructor : constructor -> std_ppcmds +val pr_inductive : inductive -> std_ppcmds val pr_sign : var_context -> std_ppcmds val pr_env_opt : context -> std_ppcmds diff --git a/parsing/termast.ml b/parsing/termast.ml index 1e6ff11fc..b33ea0053 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -96,10 +96,12 @@ let occur_id env id0 c = | VAR id -> id=id0 | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) | DOPN (Abst sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl) - | DOPN (MutInd _, cl) as t -> - (basename (mind_path t) = id0) or (array_exists (occur n) cl) - | DOPN (MutConstruct _, cl) as t -> - (basename (mind_path t) = id0) or (array_exists (occur n) cl) + | DOPN (MutInd ind_sp, cl) as t -> + (basename (path_of_inductive_path ind_sp) = id0) + or (array_exists (occur n) cl) + | DOPN (MutConstruct cstr_sp, cl) as t -> + (basename (path_of_constructor_path cstr_sp) = id0) + or (array_exists (occur n) cl) | DOPN(_,cl) -> array_exists (occur n) cl | DOP1(_,c) -> occur n c | DOP2(_,c1,c2) -> (occur n c1) or (occur n c2) @@ -137,10 +139,12 @@ let global_vars_and_consts t = | VAR id -> id::acc | DOPN (Const sp,cl) -> (basename sp)::(Array.fold_left collect acc cl) | DOPN (Abst sp,cl) -> (basename sp)::(Array.fold_left collect acc cl) - | DOPN (MutInd _, cl) as t -> - (basename (mind_path t))::(Array.fold_left collect acc cl) - | DOPN (MutConstruct _, cl) as t -> - (basename (mind_path t))::(Array.fold_left collect acc cl) + | DOPN (MutInd ind_sp, cl) as t -> + (basename (path_of_inductive_path ind_sp)) + ::(Array.fold_left collect acc cl) + | DOPN (MutConstruct cstr_sp, cl) as t -> + (basename (path_of_constructor_path cstr_sp)) + ::(Array.fold_left collect acc cl) | DOPN(_,cl) -> Array.fold_left collect acc cl | DOP1(_,c) -> collect acc c | DOP2(_,c1,c2) -> collect (collect acc c1) c2 @@ -485,23 +489,24 @@ let old_bdize_depcast opcast at_top env t = | IsAbst (sp,cl) -> ope("ABST",((path_section dummy_loc sp):: (array_map_to_list (bdrec avoid env) cl))) - | IsMutInd (sp,tyi,cl) -> + | IsMutInd ((sp,tyi),cl) -> ope("MUTIND",((path_section dummy_loc sp)::(num tyi):: (array_map_to_list (bdrec avoid env) cl))) - | IsMutConstruct (sp,tyi,n,cl) -> + | IsMutConstruct (((sp,tyi),n),cl) -> ope("MUTCONSTRUCT", ((path_section dummy_loc sp)::(num tyi)::(num n):: (array_map_to_list (bdrec avoid env) cl))) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = bdrec avoid env c in - begin match annot with - | None -> + begin + match annot with +(* | None -> (* Pas d'annotation --> affichage avec vieux Case *) let pred = bdrec avoid env p in let bl' = array_map_to_list (bdrec avoid env) bl in ope("MUTCASE",pred::tomatch::bl') - | Some indsp -> + | Some *) indsp -> let (mib,mip as lmis) = mind_specif_of_mind_light indsp in let lc = lc_of_lmis lmis in @@ -714,21 +719,22 @@ let rec detype avoid env t = RRef(dummy_loc,REVar(ev,ids_of_var (Array.map (detype avoid env) cl))) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" - | IsMutInd (sp,tyi,cl) -> + | IsMutInd (ind_sp,cl) -> let ids = ids_of_var (Array.map (detype avoid env) cl) in - RRef (dummy_loc,RInd ((sp,tyi),ids)) - | IsMutConstruct (sp,tyi,n,cl) -> + RRef (dummy_loc,RInd (ind_sp,ids)) + | IsMutConstruct (cstr_sp,cl) -> let ids = ids_of_var (Array.map (detype avoid env) cl) in - RRef (dummy_loc,RConstruct (((sp,tyi),n),ids)) + RRef (dummy_loc,RConstruct (cstr_sp,ids)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in - begin match annot with - | None -> (* Pas d'annotation --> affichage avec vieux Case *) + begin + match annot with +(* | None -> (* Pas d'annotation --> affichage avec vieux Case *) warning "Printing in old Case syntax"; ROldCase (dummy_loc,false,Some (detype avoid env p), tomatch,Array.map (detype avoid env) bl) - | Some indsp -> + | Some *) indsp -> let (mib,mip as lmis) = mind_specif_of_mind_light indsp in let lc = lc_of_lmis lmis in let lcparams = Array.map get_params lc in diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 30c88a227..0d48e9872 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -83,13 +83,14 @@ let prod_name env (n,a,b) = let ctxt_of_ids ids = Array.of_list (List.map (function id -> VAR id) ids) -let mutconstruct_of_constructor (((sp,i),j),args) = - mkMutConstruct sp i j (ctxt_of_ids args) -let mutind_of_constructor (((sp,i),_),args) = mkMutInd sp i (ctxt_of_ids args) -let mutind_of_ind ((sp,i),args) = mkMutInd sp i args - -let ith_constructor i {mind=((sp, tyi), cl)} = mkMutConstruct sp tyi i cl +let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids) +let mutconstruct_of_rawconstructor c = + mkMutConstruct (constructor_of_rawconstructor c) +let inductive_of_rawconstructor c = + inductive_of_constructor (constructor_of_rawconstructor c) +let ith_constructor i mind = + mkMutConstruct (ith_constructor_of_inductive mind i) (* determines whether is a predicate or not *) let is_predicate ind_data = (ind_data.nrealargs > 0) @@ -110,7 +111,7 @@ let lift_lfconstr n (s,c) = (s+n,c) (* Partial check on patterns *) let check_pat_arity env = function | PatCstr (loc, (cstr_sp,ids as c), args, name) -> - let ity = mutind_of_constructor c in + let ity = inductive_of_rawconstructor c in let nparams = mis_nparams (lookup_mind_specif ity env) in let tyconstr = type_of_constructor env Evd.empty (cstr_sp,ctxt_of_ids ids) in @@ -127,10 +128,10 @@ let rec constr_of_pat isevars env = function | PatVar (_,Anonymous) -> VAR (id_of_string "_") (* invalid_arg "constr_of_pat"*) | PatCstr(_,c,args,name) -> - let ity = mutind_of_constructor c in + let ity = inductive_of_rawconstructor c in let mispec = Global.lookup_mind_specif ity in let nparams = mis_nparams mispec in - let c = mutconstruct_of_constructor c in + let c = mutconstruct_of_rawconstructor c in let exl = list_tabulate (fun _ -> @@ -284,7 +285,9 @@ type info_flow = INH | SYNT | INH_FIRST the non-dependent case is applied to an object of dependent type. *) -type tomatch = IsInd of constr * mutind | MayBeNotInd of constr * constr +type tomatch = + | IsInd of constr * inductive_summary + | MayBeNotInd of constr * constr let to_mutind env sigma c t = try IsInd (c,try_mutind_of env sigma t) @@ -475,17 +478,17 @@ let patt_are_var = (fun r -> match row_current r with PatVar _ -> true |_ -> false) -let check_pattern (ind_sp,_) row = +let check_pattern (ind_sp,_ as ind) row = match row_current row with PatVar (_,id) -> () - | PatCstr (loc,(cstr_sp,_),args,name) -> - if inductive_of_constructor cstr_sp <> ind_sp then - error_bad_constructor_loc loc CCI cstr_sp ind_sp + | PatCstr (loc,(cstr_sp,ids),args,name) -> + if inductive_path_of_constructor_path cstr_sp <> ind_sp then + error_bad_constructor_loc loc CCI (cstr_sp,ctxt_of_ids ids) ind let check_patt_are_correct ity mat = List.iter (check_pattern ity) mat (*The only variables that patterns can share with the environment are - parameters of inducive definitions!. Thus patterns should also be + parameters of inductive definitions!. Thus patterns should also be lifted when pushing inthe context. *) @@ -641,7 +644,7 @@ let submat depcase isevars env i ind_data params current mat = let constraints = matching concl_realargs ind_data.realargs in *) let nbargs_iconstr = constructor_numargs ind_data i in - let ci = ith_constructor i ind_data in + let ci = ith_constructor i ind_data.mind in let expand_row r = let build_new_row subpatts name = @@ -670,7 +673,7 @@ let submat depcase isevars env i ind_data params current mat = | Anonymous -> None | Name id -> Some (mychange_name_rel env current id) in (envopt, [build_new_row None name]) - | PatCstr(_,c,largs,alias) when mutconstruct_of_constructor c = ci -> + | PatCstr(_,c,largs,alias) when mutconstruct_of_rawconstructor c = ci -> (* Avant: il y aurait eu un problème si un des largs contenait un "_". Un problème aussi pour inférer les params des constructeurs sous-jacents, car on n'avait pas accès ici @@ -696,7 +699,7 @@ let submat depcase isevars env i ind_data params current mat = type status = - | Match_Current of (constr * mutind * info_flow) (* "(", ")" needed... *) + | Match_Current of (constr * inductive_summary * info_flow) (* "(", ")" needed... *) | Any_Tomatch | All_Variables | Any_Tomatch_Dep | All_Variables_Dep | Solve_Constraint @@ -958,7 +961,7 @@ let abstracted_inductive sigma env ind_data = let params0 = List.map (lift m) params in let args0 = rel_list 0 m in - let t = applist (mutind_of_ind ity, params0@args0) in + let t = applist (mkMutInd ity, params0@args0) in let na = named_hd (Global.env()) t Anonymous in (na,t)::sign, {ind_data with params=params0;realargs=args0} @@ -1016,19 +1019,19 @@ let apply_to_dep env sigma pred = function (* analogue strategy as Christine's MLCASE *) let find_implicit_pred sigma ith_branch_builder env (current,ind_data,_) = - let {fullmind=ct;nconstr=nconstr} = ind_data in + let {nconstr=nconstr;mind=mind;params=params;realargs=realargs} = ind_data in let isrec = false in let rec findtype i = if i > nconstr then raise (CasesError (env, CantFindCaseType current)) else try - (let expti = Indrec.branch_scheme env sigma isrec i ct in + (let expti = Indrec.branch_scheme env sigma isrec i (mind,params) in let _,bri= ith_branch_builder i in let fi = bri.uj_type in let efit = nf_ise1 sigma fi in let pred = Indrec.pred_case_ml_onebranch env sigma isrec - (current,ct) (i,bri.uj_val,efit) in + (current,(mind,params,realargs)) (i,bri.uj_val,efit) in if has_ise sigma pred then error"isevar" else pred) with UserError _ -> findtype (i+1) in findtype 1 @@ -1109,7 +1112,7 @@ let type_one_branch dep env sigma ind_data p im = let (_,vargs) = array_chop (nparams+1) lAV in let c1 = appvect (lift n p,vargs) in if dep then - let co = ith_constructor i ind_data in + let co = ith_constructor i ind_data.mind in applist (c1,[applist(co,((List.map (lift n) params)@(rel_list 0 n)))]) else c1 @@ -1244,7 +1247,7 @@ and build_dep_branch trad env gd bty (current,ind_data,info) i = let l,_ = splay_prod env sigma ty in let lpatt = List.map (fun (na,ty) -> (to_mutind env sigma xtra_tm ty,SYNT)) l in let ngd = pop_and_prepend_tomatch lpatt gd in - let ci_param = applist (ith_constructor i ind_data, params) in + let ci_param = applist (ith_constructor i ind_data.mind, params) in let rnnext_env0,next_mat = submat ngd.case_dep trad.isevars env i ind_data params current ngd.mat in @@ -1322,7 +1325,7 @@ and build_nondep_branch trad env gd next_pred bty mat = ncurgd.mat}) in let nncur = lift k ncur in let lp = List.map (lift k) params in - let ci = applist (ith_constructor i ind_data, lp@(rel_list 0 k)) in + let ci = applist (ith_constructor i ind_data.mind, lp@(rel_list 0 k)) in let rnnext_env0,next_mat=submat ngd.case_dep trad.isevars next_env i ind_data lp nncur ngd.mat in @@ -1411,7 +1414,7 @@ and match_current trad env (current,ind_data,info as cji) gd = match List.map (build_ith_branch gd) (interval 1 nconstr) with [] -> (* nconstr=0 *) (context env), - mkMutCaseA (ci_of_mind (mutind_of_ind ity)) + mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel p) current [||] | (bre1,f)::lenv_f as brl -> @@ -1429,7 +1432,7 @@ and match_current trad env (current,ind_data,info as cji) gd = in check_conv 0; (common_prefix_ctxt (context env) bre1, - mkMutCaseA (ci_of_mind (mutind_of_ind ity)) + mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel (nf_ise1 !(trad.isevars) p)) current lf) in newenv, @@ -1512,7 +1515,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd = (snd (build_ith_branch nenv ngd1 i)).uj_val) (interval 1 nconstr) in let case_exp = - mkMutCaseA (ci_of_mind (mutind_of_ind ity)) (eta_reduce_if_rel np) + mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel np) current (Array.of_list lf) in let (na,ty),_ = uncons_rel_env (context nenv) in let rescase = lambda_name env (na,body_of_type ty,case_exp) in @@ -1524,7 +1527,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd = let lf = List.map (fun i -> (snd (build_ith_branch nenv ngd1 i)).uj_val) (interval 1 nconstr) in - let rescase = mkMutCaseA (ci_of_mind (mutind_of_ind ity)) + let rescase = mkMutCaseA (ci_of_mind (mkMutInd ity)) (eta_reduce_if_rel np) current (Array.of_list lf) in let casetyp = whd_beta nenv !(trad.isevars) (applist (np,args)) in (context nenv),rescase,casetyp @@ -1544,7 +1547,7 @@ and match_current_dep trad env (current,ind_data,info as cji) gd = * this (Rel 1) by initial value will be done by the application *) let case_exp = - mkMutCaseA (ci_of_mind (mutind_of_ind ity)) np1 (Rel 1) (Array.of_list lf) in + mkMutCaseA (ci_of_mind (mkMutInd ity)) np1 (Rel 1) (Array.of_list lf) in let nenv2,rescase = elam_and_popl_named n (context nenv1) case_exp in let casetyp = whd_beta nenv1 !(trad.isevars) (applist (np,args@[(Rel 1)])) in nenv2,rescase,casetyp @@ -1678,7 +1681,7 @@ let check_coercibility isevars env ty indty = let check_pred_correctness isevars env tomatchl pred = let cook n = function | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data)) - -> (applist (mutind_of_ind ity,(List.map (lift n) params) + -> (applist (mkMutInd ity,(List.map (lift n) params) @(rel_list 0 ind_data.nrealargs)), lift n (whd_beta env !isevars (applist (arity,params)))) | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent" @@ -1703,7 +1706,7 @@ let check_pred_correctness isevars env tomatchl pred = let build_expected_arity isdep env sigma tomatchl sort = let cook n = function | IsInd(c,({mind=ity;params=params;realargs=args;arity=arity} as ind_data)) - -> (applist (mutind_of_ind ity,(List.map (lift n) params) + -> (applist (mkMutInd ity,(List.map (lift n) params) @(rel_list 0 ind_data.nrealargs)), lift n (whd_beta env sigma (applist (arity,params)))) | MayBeNotInd (_,_) -> anomaly "Should have been catched in case_dependent" @@ -1795,15 +1798,6 @@ let rec find_row_ind = function | PatVar _ :: l -> find_row_ind l | PatCstr(loc,c,_,_) :: _ -> Some (loc,c) - -let find_pretype mat = - let lpatt = List.map (fun r -> List.hd r.patterns) mat in - match find_row_ind lpatt with - Some (_,c) -> mutind_of_constructor c - | None -> anomalylabstrm "find_pretype" - [<'sTR "Expecting a patt. in constructor form and found empty list">] - - (* We do the unification for all the rows that contain * constructor patterns. This is what we do at the higher level of patterns. * For nested patterns, we do this unif when we ``expand'' the matrix, and we @@ -1825,7 +1819,7 @@ let inh_coerce_to_ind isevars env ty tyi = (push_rel (na,(make_typed ty s)) env, fst (new_isevar isevars env (mkCast ty (mkSort s)) CCI)::evl)) ntys (env,[]) in - let expected_typ = applist (tyi,evarl) in + let expected_typ = applist (mkMutInd tyi,evarl) in (* devrait être indifférent d'exiger leq ou pas puisque pour un inductif cela doit être égal *) if Evarconv.the_conv_x_leq env isevars expected_typ ty then ty @@ -1836,7 +1830,7 @@ let coerce_row trad env row tomatch = let j = trad.pretype mt_tycon env tomatch in match find_row_ind row with Some (cloc,(cstr,_ as c)) -> - (let tyi = mutind_of_constructor c in + (let tyi = inductive_of_rawconstructor c in try let indtyp = inh_coerce_to_ind trad.isevars env j.uj_type tyi in IsInd (j.uj_val,try_mutind_of env !(trad.isevars) j.uj_type) @@ -1844,7 +1838,8 @@ let coerce_row trad env row tomatch = (* 2 cas : pas le bon inductive ou pas un inductif du tout *) try let ind_data = try_mutind_of env !(trad.isevars) j.uj_type in - error_bad_constructor_loc cloc CCI cstr (fst ind_data.mind) + error_bad_constructor_loc cloc CCI + (constructor_of_rawconstructor c) ind_data.mind with Induc -> error_case_not_inductive_loc (loc_of_rawconstr tomatch) CCI env j.uj_val j.uj_type) diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 80fa10520..792a66fe9 100755 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -14,8 +14,8 @@ open Generic (* usage qque peu general: utilise aussi dans record *) type cte_typ = - | NAM_Var of identifier - | NAM_SP of section_path + | NAM_Var of identifier + | NAM_SP of section_path | NAM_Construct of constructor_path let cte_of_constr = function @@ -30,7 +30,7 @@ type cl_typ = | CL_FUN | CL_Var of identifier | CL_SP of section_path - | CL_IND of section_path * int + | CL_IND of inductive_path type cl_info_typ = { cL_STR : string; diff --git a/pretyping/classops.mli b/pretyping/classops.mli index a4bf0ee8f..fe7fb437d 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -16,7 +16,7 @@ type cl_typ = | CL_FUN | CL_Var of identifier | CL_SP of section_path - | CL_IND of section_path * int + | CL_IND of inductive_path type cl_info_typ = { cL_STR : string; diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index f55aaf69a..af42d3cd4 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -80,8 +80,8 @@ let split_evar_to_arrow sigma c = let dsp = path_of_const (body_of_type dom) in let rsp = path_of_const (body_of_type rng) in (sigma3, - mkCast (mkConst dsp args) dummy_sort, - mkCast (mkConst rsp (array_cons (mkRel 1) args)) dummy_sort) + mkCast (mkConst (dsp,args)) dummy_sort, + mkCast (mkConst (rsp,array_cons (mkRel 1) args)) dummy_sort) (* Redefines an evar with a smaller context (i.e. it may depend on less diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 1292ad75c..9944f55a8 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -31,7 +31,7 @@ val error_case_not_inductive_loc : (* Pattern-matching errors *) val error_bad_constructor_loc : - loc -> path_kind -> constructor_path -> inductive_path -> 'b + loc -> path_kind -> constructor -> inductive -> 'b val error_wrong_numarg_constructor_loc : loc -> path_kind -> constructor_path -> int -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 4391a7fe6..59716c5d6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -71,17 +71,18 @@ let it_lambda_name env = List.fold_left (fun c (n,t) -> lambda_name env (n,t,c)) let transform_rec loc env sigma cl (ct,pt) = - let (mI,largs as mind) = find_minductype env sigma ct in + let (mind,largs as appmind) = find_minductype env sigma ct in let p = cl.(0) and c = cl.(1) and lf = Array.sub cl 2 ((Array.length cl) - 2) in - let mispec = lookup_mind_specif mI env in + let mispec = lookup_mind_specif mind env in + let mI = mkMutInd mind in let recargs = mis_recarg mispec in let expn = Array.length recargs in if Array.length lf <> expn then error_number_branches_loc loc CCI env c ct expn; if is_recursive [mispec.mis_tyi] recargs then - let (dep,_) = find_case_dep_nparams env sigma (c,p) mind pt in + let (dep,_) = find_case_dep_nparams env sigma (c,p) appmind pt in let ntypes = mis_nconstr mispec and tyi = mispec.mis_tyi and nparams = mis_nparams mispec in @@ -241,8 +242,8 @@ let pretype_ref loc isevars env = function | RVar id -> pretype_var loc env id | RConst (sp,ids) -> - let cstr = mkConst sp (ctxt_of_ids ids) in - make_judge cstr (type_of_constant env !isevars cstr) + let cst = (sp,ctxt_of_ids ids) in + make_judge (mkConst cst) (type_of_constant env !isevars cst) | RAbst sp -> failwith "Pretype: abst doit disparaître" (* @@ -267,18 +268,17 @@ let pretype_ref loc isevars env = function *) | REVar (sp,ids) -> error " Not able to type terms with dependent subgoals" (* Not able to type goal existential yet - let cstr = mkConst sp (ctxt_of_ids ids) in + let cstr = mkConst (sp,ctxt_of_ids ids) in make_judge cstr (type_of_existential env !isevars cstr) *) -| RInd ((sp,i),ids) -> - let cstr = mkMutInd sp i (ctxt_of_ids ids) in - make_judge cstr (type_of_inductive env !isevars cstr) +| RInd (ind_sp,ids) -> + let ind = (ind_sp,ctxt_of_ids ids) in + make_judge (mkMutInd ind) (type_of_inductive env !isevars ind) -| RConstruct (((sp,i),j) as cstr_sp,ids) -> - let ctxt = ctxt_of_ids ids in - let (typ,kind) = - destCast (type_of_constructor env !isevars (cstr_sp,ctxt)) in - {uj_val=mkMutConstruct sp i j ctxt; uj_type=typ; uj_kind=kind} +| RConstruct (cstr_sp,ids) -> + let cstr = (cstr_sp,ctxt_of_ids ids) in + let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in + {uj_val=mkMutConstruct cstr; uj_type=typ; uj_kind=kind} (* pretype vtcon isevars env constr tries to solve the *) (* existential variables in constr in environment env with the *) @@ -373,8 +373,8 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) | ROldCase (loc,isrec,po,c,lf) -> let cj = pretype mt_tycon env isevars c in - let (mind,_) = - try find_mrectype env !isevars cj.uj_type + let {mind=mind;params=params;realargs=realargs} = + try try_mutind_of env !isevars cj.uj_type with Induc -> error_case_not_inductive CCI env (nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in let pj = match po with @@ -392,12 +392,13 @@ match cstr with (* Où teste-t-on que le résultat doit satisfaire tycon ? *) then error_cant_find_case_type_loc loc env cj.uj_val else try - let expti = Indrec.branch_scheme env !isevars isrec i cj.uj_type in + let expti = + Indrec.branch_scheme env !isevars isrec i (mind,params) in let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in let efjt = nf_ise1 !isevars fj.uj_type in let pred = Indrec.pred_case_ml_onebranch env !isevars isrec - (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in + (cj.uj_val,(mind,params,realargs)) (i,fj.uj_val,efjt) in if has_ise !isevars pred then findtype (i+1) else let pty = Retyping.get_type_of env !isevars pred in diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index e51919f2f..7d5417829 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -10,37 +10,6 @@ open Reduction open Environ open Typeops -(* A light version of mind_specif_of_mind *) - -type mutind_id = inductive_path * constr array - -type mutind = - {fullmind : constr; - mind : mutind_id; - nparams : int; - nrealargs : int; - nconstr : int; - params : constr list; - realargs : constr list; - arity : constr} - -(* raise Induc if not an inductive type *) -let try_mutind_of env sigma ty = - let (mind,largs) = find_mrectype env sigma ty in - let mispec = lookup_mind_specif mind env in - let nparams = mis_nparams mispec in - let (params,realargs) = list_chop nparams largs in - {fullmind = ty; - mind = (let (sp,i,cv) = destMutInd mind in (sp,i),cv); - nparams = nparams; - nrealargs = List.length realargs; - nconstr = mis_nconstr mispec; - params = params; - realargs = realargs; - arity = Instantiate.mis_arity mispec} - - -(******** A light version of type_of *********) type metamap = (int * constr) list let rec is_dep_case env sigma (pt,ar) = @@ -85,13 +54,11 @@ let rec type_of env cstr= | IsVar id -> body_of_type (snd (lookup_var id env)) | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*) - | IsConst _ -> (body_of_type (type_of_constant env sigma cstr)) + | IsConst c -> (body_of_type (type_of_constant env sigma c)) | IsEvar _ -> type_of_existential env sigma cstr - | IsMutInd _ -> (body_of_type (type_of_inductive env sigma cstr)) - | IsMutConstruct (sp,i,j,args) -> - let (typ,kind) = - destCast (type_of_constructor env sigma (((sp,i),j),args)) - in typ + | IsMutInd ind -> (body_of_type (type_of_inductive env sigma ind)) + | IsMutConstruct cstr -> + let (typ,kind) = destCast (type_of_constructor env sigma cstr) in typ | IsMutCase (_,p,c,lf) -> let {realargs=args;arity=arity;nparams=n} = try try_mutind_of env sigma (type_of env c) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 354771e6e..036cd53f0 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -17,27 +17,3 @@ type metamap = (int * constr) list val get_type_of : env -> 'a evar_map -> constr -> constr val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts - -(*i The following should be merged with mind_specif and put elsewhere - Note : it needs Reduction i*) - -(* A light version of [mind_specif] *) - -(* Invariant: We have\\ - -- Hnf (fullmind) = DOPN(AppL,[|coremind;..params..;..realargs..|])\\ - -- with mind = MutInd ((sp,i),localvars) for some sp, i, localvars - *) -type mutind_id = inductive_path * constr array - -type mutind = { - fullmind : constr; - mind : mutind_id; - nparams : int; - nrealargs : int; - nconstr : int; - params : constr list; - realargs : constr list; - arity : constr } - -(* [try_mutind_of sigma t] raise Induc if [t] is not an inductive type *) -val try_mutind_of : env -> 'a Evd.evar_map -> constr -> mutind diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index ad33549ca..92fb27a23 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -55,9 +55,6 @@ let make_elim_fun f largs = with Elimconst | Failure _ -> raise Redelimination -let mind_nparams env i = - let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams - (* F is convertible to DOPN(Fix(recindices,bodynum),bodyvect) make the reduction using this extra information *) @@ -93,10 +90,13 @@ let contract_cofix_use_function f cofix = sAPPViList bodynum (array_last bodyvect) lbodies | _ -> assert false +let mind_nparams env i = + let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let reduce_mind_case_use_function env f mia = match mia.mconstr with - | DOPN(MutConstruct((indsp,tyindx),i),_) -> - let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in + | DOPN(MutConstruct(ind_sp,i as cstr_sp),args) -> + let ind = inductive_of_constructor (cstr_sp,args) in let nparams = mind_nparams env ind in let real_cargs = snd(list_chop nparams mia.mcargs) in applist (mia.mlf.(i-1),real_cargs) @@ -325,7 +325,7 @@ let one_step_reduce env sigma = let reduce_to_mind env sigma t = let rec elimrec t l = match whd_castapp_stack t [] with - | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l) + | (DOPN(MutInd mind,args),_) -> ((mind,args),t,prod_it t l) | (DOPN(Const _,_),_) -> (try let t' = nf_betaiota env sigma (one_step_reduce env sigma t) in @@ -346,6 +346,5 @@ let reduce_to_mind env sigma t = elimrec t [] let reduce_to_ind env sigma t = - let (mind,redt,c) = reduce_to_mind env sigma t in - (Declare.mind_path mind, redt, c) - + let ((ind_sp,_),redt,c) = reduce_to_mind env sigma t in + (Declare.path_of_inductive_path ind_sp, redt, c) diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index a555667e6..bd20e8b7b 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -18,7 +18,7 @@ val nf : 'a reduction_function val one_step_reduce : 'a reduction_function val reduce_to_mind : - env -> 'a evar_map -> constr -> constr * constr * constr + env -> 'a evar_map -> constr -> inductive * constr * constr val reduce_to_ind : env -> 'a evar_map -> constr -> section_path * constr * constr diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 7c32a124c..afc11aaf8 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -42,15 +42,14 @@ let rec execute mf env sigma cstr = else error "Cannot typecheck an unevaluable abstraction" - | IsConst _ -> - make_judge cstr (type_of_constant env sigma cstr) + | IsConst c -> + make_judge cstr (type_of_constant env sigma c) - | IsMutInd _ -> - make_judge cstr (type_of_inductive env sigma cstr) + | IsMutInd ind -> + make_judge cstr (type_of_inductive env sigma ind) - | IsMutConstruct (sp,i,j,args) -> - let (typ,kind) = - destCast (type_of_constructor env sigma (((sp,i),j),args)) in + | IsMutConstruct cstruct -> + let (typ,kind) = destCast (type_of_constructor env sigma cstruct) in { uj_val = cstr; uj_type = typ; uj_kind = kind } | IsMutCase (_,p,c,lf) -> diff --git a/proofs/logic.ml b/proofs/logic.ml index 027ceab4a..353472f01 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -281,14 +281,14 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> if k = 1 then (try - find_minductype env sigma c1 + let _ = find_minductype env sigma c1 in () with Induc -> error "cannot do a fixpoint on a non inductive type") else check_ind (k-1) b | _ -> error "not enough products" in - let _ = check_ind n cl in + check_ind n cl; if mem_sign sign f then error "name already used in the environment"; let a = mk_assumption env sigma cl in let sg = mk_goal info (push_var (f,a) env) cl in @@ -300,7 +300,7 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> if k = 1 then (try - find_minductype env sigma c1 + fst (find_minductype env sigma c1) with Induc -> error "cannot do a fixpoint on a non inductive type") else @@ -308,10 +308,10 @@ let prim_refiner r sigma goal = | _ -> error "not enough products" in let n = (match ln with (Num(_,n))::_ -> n | _ -> assert false) in - let (sp,_,_) = destMutInd (fst (check_ind n cl)) in + let (sp,_) = check_ind n cl in let rec mk_sign sign = function | (ar::lar'),(f::lf'),((Num(_,n))::ln')-> - let (sp',_,_) = destMutInd (fst (check_ind n ar)) in + let (sp',_) = check_ind n ar in if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); @@ -331,12 +331,12 @@ let prim_refiner r sigma goal = | DOP2(Prod,c1,DLAM(_,b)) -> check_is_coind b | b -> (try - let _ = find_mcoinductype env sigma b in true + let _ = find_mcoinductype env sigma b in () with Induc -> error ("All methods must construct elements " ^ "in coinductive types")) in - let _ = List.for_all check_is_coind (cl::lar) in + List.iter check_is_coind (cl::lar); let rec mk_sign sign = function | (ar::lar'),(f::lf') -> if mem_sign sign f then diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 4593e92b7..dff9fe0b2 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -62,8 +62,9 @@ val pf_red_product : goal sigma -> constr -> constr val pf_nf : goal sigma -> constr -> constr val pf_nf_betaiota : goal sigma -> constr -> constr val pf_one_step_reduce : goal sigma -> constr -> constr -val pf_reduce_to_mind : goal sigma -> constr -> constr * constr * constr -val pf_reduce_to_ind : goal sigma -> constr -> section_path * constr * constr +val pf_reduce_to_mind : goal sigma -> constr -> inductive * constr * constr +val pf_reduce_to_ind : + goal sigma -> constr -> section_path * constr * constr val pf_compute : goal sigma -> constr -> constr val pf_unfoldn : (int list * section_path) list -> goal sigma -> constr -> constr diff --git a/tactics/auto.ml b/tactics/auto.ml index e0dec159b..e1c4caad7 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -358,7 +358,7 @@ let _ = begin try let trad = Declare.global_reference CCI in - let rectype = trad c in + let rectype = destMutInd (trad c) in let consnames = mis_consnames (Global.lookup_mind_specif rectype) in let lcons = diff --git a/tactics/pattern.ml b/tactics/pattern.ml index dcc3a5f7b..fc5b6a446 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -219,8 +219,8 @@ let match_with_non_recursive_type t = | IsAppL _ -> let (hdapp,args) = decomp_app t in (match kind_of_term hdapp with - | IsMutInd _ -> - if not (Global.mind_is_recursive hdapp) then + | IsMutInd ind -> + if not (Global.mind_is_recursive ind) then Some (hdapp,args) else None @@ -235,11 +235,11 @@ let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) let match_with_conjunction t = let (hdapp,args) = decomp_app t in match kind_of_term hdapp with - | IsMutInd _ -> - let nconstr = Global.mind_nconstr hdapp in + | IsMutInd ind -> + let nconstr = Global.mind_nconstr ind in if (nconstr = 1) && - (not (Global.mind_is_recursive hdapp)) && - (nb_prod (Global.mind_arity hdapp)) = (Global.mind_nparams hdapp) + (not (Global.mind_is_recursive ind)) && + (nb_prod (Global.mind_arity ind)) = (Global.mind_nparams ind) then Some (hdapp,args) else @@ -254,13 +254,13 @@ let is_conjunction t = op2bool (match_with_conjunction t) let match_with_disjunction t = let (hdapp,args) = decomp_app t in match kind_of_term hdapp with - | IsMutInd _ -> + | IsMutInd ind -> let constr_types = - Global.mind_lc_without_abstractions hdapp in + Global.mind_lc_without_abstractions ind in let only_one_arg c = - ((nb_prod c) - (Global.mind_nparams hdapp)) = 1 in + ((nb_prod c) - (Global.mind_nparams ind)) = 1 in if (array_for_all only_one_arg constr_types) && - (not (Global.mind_is_recursive hdapp)) + (not (Global.mind_is_recursive ind)) then Some (hdapp,args) else @@ -272,8 +272,8 @@ let is_disjunction t = op2bool (match_with_disjunction t) let match_with_empty_type t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with - | IsMutInd _ -> - let nconstr = Global.mind_nconstr hdapp in + | IsMutInd ind -> + let nconstr = Global.mind_nconstr ind in if nconstr = 0 then Some hdapp else None | _ -> None @@ -282,11 +282,11 @@ let is_empty_type t = op2bool (match_with_empty_type t) let match_with_unit_type t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with - | IsMutInd _ -> + | IsMutInd ind -> let constr_types = - Global.mind_lc_without_abstractions hdapp in - let nconstr = Global.mind_nconstr hdapp in - let zero_args c = ((nb_prod c) - (Global.mind_nparams hdapp)) = 0 in + Global.mind_lc_without_abstractions ind in + let nconstr = Global.mind_nconstr ind in + let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in if nconstr = 1 && (array_for_all zero_args constr_types) then Some hdapp else @@ -303,12 +303,12 @@ let is_unit_type t = op2bool (match_with_unit_type t) let match_with_equation t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with - | IsMutInd _ -> + | IsMutInd ind -> let constr_types = - Global.mind_lc_without_abstractions hdapp in + Global.mind_lc_without_abstractions ind in let refl_rel_term1 = put_pat mmk "(A:?)(x:A)(? A x x)" in let refl_rel_term2 = put_pat mmk "(x:?)(? x x)" in - let nconstr = Global.mind_nconstr hdapp in + let nconstr = Global.mind_nconstr ind in if nconstr = 1 && (somatches constr_types.(0) refl_rel_term1 || somatches constr_types.(0) refl_rel_term2) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 4755cc50e..891f411a1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -229,7 +229,7 @@ let ifOnClause pred tac1 tac2 cls gl = the elimination. *) type branch_args = { - ity : constr; (* the type we were eliminating on *) + ity : inductive; (* the type we were eliminating on *) largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) @@ -245,16 +245,15 @@ type branch_assumptions = { recargs : identifier list; (* the RECURSIVE constructor arguments *) indargs : identifier list} (* the inductive arguments *) - (* Hum ... the following function looks quite similar to the one - * defined with the same name in Tactics.ml. + * (previously) defined with the same name in Tactics.ml. * --Eduardo (11/8/97) *) -let reduce_to_ind gl t = +let reduce_to_ind_goal gl t = let rec elimrec t l = match decomp_app(t) with - | (DOPN(MutInd (sp,_),_) as mind,_) -> - (mind,mind_path mind,t,prod_it t l) + | (DOPN(MutInd ind_sp,args) as mind,_) -> + ((ind_sp,args),path_of_inductive_path ind_sp,t,prod_it t l) | (DOPN(Const _,_),_) -> elimrec (pf_nf_betaiota gl (pf_one_step_reduce gl t)) l | (DOP2(Cast,c,_),[]) -> elimrec c l @@ -272,7 +271,7 @@ let case_sign ity i = analrec [] recarg.(i-1) let elim_sign ity i = - let (_,j,_) = destMutInd ity in + let (_,j),_ = ity in let rec analrec acc = function | (Param(_)::rest) -> analrec (false::acc) rest | (Norec::rest) -> analrec (false::acc) rest @@ -313,7 +312,7 @@ let last_arg = function let general_elim_then_using elim elim_sign_fun tac predicate (indbindings,elimbindings) c gl = - let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in + let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in let name_elim = (match elim with | DOPN(Const sp,_) -> id_of_string(string_of_path sp) @@ -361,7 +360,7 @@ let general_elim_then_using let elimination_then_using tac predicate (indbindings,elimbindings) c gl = - let (ity,path_name,_,t) = reduce_to_ind gl (pf_type_of gl c) in + let (ity,path_name,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in let elim = lookup_eliminator (pf_hyps gl) path_name (suff gl (pf_concl gl)) in @@ -374,7 +373,7 @@ let simple_elimination_then tac = elimination_then tac ([],[]) let case_then_using tac predicate (indbindings,elimbindings) c gl = (* finding the case combinator *) - let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in + let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in let sigma = project gl in let sort = sort_of_goal gl in let elim = Indrec.make_case_gen (pf_env gl) sigma ity sort in @@ -383,7 +382,7 @@ let case_then_using tac predicate (indbindings,elimbindings) c gl = let case_nodep_then_using tac predicate (indbindings,elimbindings) c gl = (* finding the case combinator *) - let (ity,_,_,t) = reduce_to_ind gl (pf_type_of gl c) in + let (ity,_,_,t) = reduce_to_ind_goal gl (pf_type_of gl c) in let sigma = project gl in let sort = sort_of_goal gl in let elim = Indrec.make_case_nodep (pf_env gl) sigma ity sort in @@ -448,3 +447,4 @@ let make_case_branch_assumptions ba gl = with Failure _ -> anomaly "make_case_branch_assumptions") let case_on_ba tac ba gl = tac (make_case_branch_assumptions ba gl) gl + diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4ac1fb41d..7884ba02e 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -83,7 +83,7 @@ val conclPattern : constr -> constr -> Coqast.t -> tactic (*s Elimination tacticals. *) type branch_args = { - ity : constr; (* the type we were eliminating on *) + ity : inductive; (* the type we were eliminating on *) largs : constr list; (* its arguments *) branchnum : int; (* the branch number *) pred : constr; (* the predicate we used *) @@ -105,7 +105,7 @@ val lookup_eliminator : typed_type signature -> section_path -> string -> constr val general_elim_then_using : - constr -> (constr -> int -> bool list) -> + constr -> (inductive -> int -> bool list) -> (branch_args -> tactic) -> constr option -> (arg_bindings * arg_bindings) -> constr -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 8759e54a9..479120929 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -48,8 +48,8 @@ let get_commands = let rec string_head_bound = function | DOPN(Const _,_) as x -> string_of_id (basename (path_of_const x)) - | DOPN(MutInd _,_) as x -> - let mispec = Global.lookup_mind_specif x in + | DOPN(MutInd ind_sp,args) as x -> + let mispec = Global.lookup_mind_specif (ind_sp,args) in string_of_id (mis_typename mispec) | DOPN(MutConstruct ((sp,tyi),i),_) -> let mib = Global.lookup_mind sp in @@ -833,7 +833,6 @@ let dyn_move_dep = function let constructor_checking_bound boundopt i lbind gl = let cl = pf_concl gl in let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in - let (x_0,x_1,args) = destMutInd mind in let nconstr = mis_nconstr (Global.lookup_mind_specif mind) and sigma = project gl in if i=0 then error "The constructors are numbered starting from 1"; @@ -844,7 +843,7 @@ let constructor_checking_bound boundopt i lbind gl = error "Not the expected number of constructors" | None -> () end; - let cons = DOPN(MutConstruct((x_0,x_1),i),args) in + let cons = mkMutConstruct (ith_constructor_of_inductive mind i) in let apply_tac = apply_with_bindings (cons,lbind) in (tclTHENLIST [convert_concl redcl; intros; apply_tac]) gl @@ -853,7 +852,6 @@ let one_constructor i = (constructor_checking_bound None i) let any_constructor gl = let cl = pf_concl gl in let (mind,_,redcl) = reduce_to_mind (pf_env gl) (project gl) cl in - let (x_0,x_1,args) = destMutInd mind in let nconstr = mis_nconstr (Global.lookup_mind_specif mind) and sigma = project gl in if nconstr = 0 then error "The type has no constructors"; @@ -1003,9 +1001,9 @@ let simplest_elim c = default_elim (c,[]) let rec is_rec_arg indpath t = - try - Declare.mind_path (fst (find_mrectype (Global.env()) Evd.empty t)) - = indpath + try + let ((ind_sp,_),_) = find_mrectype (Global.env()) Evd.empty t in + Declare.path_of_inductive_path ind_sp = indpath with Induc -> false @@ -1265,9 +1263,9 @@ let induction_from_context hyp0 gl = let sign = pf_untyped_hyps gl in let tsign = pf_hyps gl in let tmptyp0 = pf_get_hyp gl hyp0 in - let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in + let ((ind_sp,_) as mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in let indvars = find_atomic_param_of_ind mind indtyp in - let mindpath = Declare.mind_path mind in + let mindpath = Declare.path_of_inductive_path ind_sp in let elimc = lookup_eliminator tsign mindpath (suff gl (pf_concl gl)) in let elimt = pf_type_of gl elimc in let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars sign in diff --git a/toplevel/class.ml b/toplevel/class.ml index 7912b2fdf..f8b84b7b6 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -117,10 +117,10 @@ let coe_constructor_at_head t = let rec aux t' = match kind_of_term t' with | IsConst (sp,l) -> (Array.to_list l),NAM_SP sp - | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp + | IsMutInd ((sp,_),l) -> (Array.to_list l),NAM_SP sp | IsVar id -> [],NAM_Var id | IsCast (c,_) -> aux c - | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j) + | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Construct cstr_sp | IsAppL(f,args) -> aux f | _ -> raise Not_found in @@ -130,7 +130,7 @@ let constructor_at_head1 t = let rec aux t' = match kind_of_term t' with | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0 - | IsMutInd (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),0 + | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0 | IsVar id -> t',[],[],CL_Var id,0 | IsCast (c,_) -> aux c | IsAppL(f,args) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index c1860012b..ce804aa7f 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -337,15 +337,16 @@ let build_corecursive lnameardef = in () -exception NotInductive let inductive_of_ident id = - try match kind_of_term (global_reference CCI id) with + let c = + try global_reference CCI id + with Not_found -> + errorlabstrm "inductive_of_ident" ((string_of_id id) ^ " not found") + in + match kind_of_term (global_reference CCI id) with | IsMutInd ind -> ind - | _ -> raise NotInductive - with Not_found | NotInductive -> - errorlabstrm "inductive_of_ident" - [< 'sTR (string_of_id id); 'sPC; - 'sTR "is not an inductive type" >] + | _ -> errorlabstrm "inductive_of_ident" + [< 'sTR (string_of_id id); 'sPC; 'sTR "is not an inductive type" >] let build_scheme lnamedepindsort = let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 15f52e412..f13890228 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -151,7 +151,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = let lmodif_one_mind i = let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in (MutInd(osecsp,i),DO_ABSTRACT(MutInd(nsecsp,i),modl)):: - (MutCase(Some (osecsp,i)),DO_ABSTRACT(MutCase(Some (nsecsp,i)),[])):: + (MutCase(osecsp,i),DO_ABSTRACT(MutCase(nsecsp,i),[])):: (list_tabulate (function j -> let j' = j + 1 in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index a7cc960ab..78709719a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -217,7 +217,7 @@ let explain_bad_constructor k ctx cstr ind = 'sTR " in inductive type "; pt >] let explain_wrong_numarg_of_constructor k ctx cstr n = - let pc = pr_constructor cstr in + let pc = pr_constructor (cstr,[||]) in [<'sTR "The constructor "; pc; 'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">] |