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 /kernel/inductive.ml | |
| 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
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 21 |
1 files changed, 18 insertions, 3 deletions
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) |