aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-21 00:02:58 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2000-03-21 00:02:58 +0000
commit1c1b6f2da919c1303b87b97119b621a06952fadc (patch)
treeeda5f0c909d2c78b31f5bf0b49d22c081ac2b17e /kernel
parent815485820cd1aab70b5a70a10261fa6969ea14d9 (diff)
Ajout des fonctions de formation du 'case_info'; Suppression de make_arity et make_constructor de inductive_summary
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@333 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
-rw-r--r--kernel/inductive.ml15
-rw-r--r--kernel/inductive.mli18
2 files changed, 19 insertions, 14 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index d235245e6..fda1190d1 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -19,6 +19,7 @@ type mutual_inductive_packet = {
mind_typename : identifier;
mind_lc : constr;
mind_arity : typed_type;
+ mind_nrealargs : int;
mind_kelim : sorts list;
mind_listrec : (recarg list) array;
mind_finite : bool }
@@ -44,6 +45,7 @@ type mind_specif = {
let mis_ntypes mis = mis.mis_mib.mind_ntypes
let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
let mis_nparams mis = mis.mis_mib.mind_nparams
+let mis_nrealargs mis = mis.mis_mip.mind_nrealargs
let mis_kelim mis = mis.mis_mip.mind_kelim
let mis_recargs mis =
Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
@@ -69,8 +71,6 @@ type inductive_summary = {
nparams : int;
nrealargs : int;
nconstr : int;
- make_arity : inductive -> constr list -> (name * constr) list * sorts;
- make_constrs : inductive -> constr list -> constructor_summary array
}
let is_recursive listind =
@@ -88,6 +88,17 @@ let mis_is_recursive mis =
let mind_nth_type_packet mib n = mib.mind_packets.(n)
+(* Annotation for cases *)
+let make_case_info mis style pats_source =
+ let constr_lengths = Array.map List.length (mis_recarg mis) in
+ let indsp = (mis.mis_sp,mis.mis_tyi) in
+ let print_info =
+ (indsp,mis_consnames mis,mis.mis_mip.mind_nrealargs,style,pats_source) in
+ (constr_lengths,print_info)
+
+let make_default_case_info mis =
+ make_case_info mis None (Array.init (mis_nconstr mis) (fun _ -> RegularPat))
+
(*s Declaration. *)
type mutual_inductive_entry = {
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 6e568e912..c9857daaf 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -21,6 +21,7 @@ type mutual_inductive_packet = {
mind_typename : identifier;
mind_lc : constr;
mind_arity : typed_type;
+ mind_nrealargs : int;
mind_kelim : sorts list;
mind_listrec : (recarg list) array;
mind_finite : bool }
@@ -52,6 +53,7 @@ type mind_specif = {
val mis_ntypes : mind_specif -> int
val mis_nconstr : mind_specif -> int
val mis_nparams : mind_specif -> int
+val mis_nrealargs : mind_specif -> int
val mis_kelim : mind_specif -> sorts list
val mis_recargs : mind_specif -> (recarg list) array array
val mis_recarg : mind_specif -> (recarg list) array
@@ -63,6 +65,10 @@ val mis_consnames : mind_specif -> identifier array
val mind_nth_type_packet :
mutual_inductive_body -> int -> mutual_inductive_packet
+val make_case_info : mind_specif -> case_style option -> pattern_source array
+ -> case_info
+val make_default_case_info : mind_specif -> case_info
+
(*s This type gathers useful informations about some instance of a constructor
relatively to some implicit context (the current one)
@@ -87,16 +93,6 @@ type constructor_summary = {
[Hnf (fullmind)] = [DOPN(AppL,[|MutInd mind;..params..;..realargs..|])] \par
with [mind] = [((sp,i),localvars)] for some [sp, i, localvars].
- [make_constrs] is a receipt to build constructor instantiated by
- local vars and params; it is a closure which does not need to be
- lifted; it must be applied to [mind] and [params] to get the constructors
- correctly lifted and instantiated
-
- [make_arity] is a receipt to build the arity instantiated by local
- vars and by params; it is a closure which does not need to be
- lifted. Arity is pre-decomposed into its real parameters and its
- sort; it must be applied to [mind] and [params] to get the arity
- correctly lifted and instantiated
*)
type inductive_summary = {
@@ -107,8 +103,6 @@ type inductive_summary = {
nparams : int;
nrealargs : int;
nconstr : int;
- make_arity : inductive -> constr list -> (name * constr) list * sorts;
- make_constrs : inductive -> constr list -> constructor_summary array
}
(*s Declaration of inductive types. *)