diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 13:14:38 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-22 13:14:38 +0000 |
commit | 2bb331f734ed58eb90eb9535fe883aa5d2f5a278 (patch) | |
tree | b3606667a186baf9b674ca70476fb039be5d79b1 /kernel/declarations.ml | |
parent | f9031792f714bb468c2dc8bfb49f34cfef44b27a (diff) |
Changement nom module Constant en Declarations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@459 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/declarations.ml')
-rw-r--r-- | kernel/declarations.ml | 76 |
1 files changed, 76 insertions, 0 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml new file mode 100644 index 000000000..7f45aae57 --- /dev/null +++ b/kernel/declarations.ml @@ -0,0 +1,76 @@ + +(* $Id$ *) + +open Names +open Univ +open Generic +open Term +open Sign + +(* Constant entries *) + +type lazy_constant_value = + | Cooked of constr + | Recipe of (unit -> constr) + +type constant_value = lazy_constant_value ref + +type constant_body = { + const_kind : path_kind; + const_body : constant_value option; + const_type : typed_type; + const_hyps : typed_type signature; + const_constraints : constraints; + mutable const_opaque : bool } + +let is_defined cb = + match cb.const_body with Some _ -> true | _ -> false + +let is_opaque cb = cb.const_opaque + +let cook_constant = function + | { contents = Cooked c } -> c + | { contents = Recipe f } as v -> let c = f () in v := Cooked c; c + +type constant_entry = { + const_entry_body : lazy_constant_value; + const_entry_type : constr option } + +(* Inductive entries *) + +type recarg = + | Param of int + | Norec + | Mrec of int + | Imbr of inductive_path * recarg list + +type mutual_inductive_packet = { + mind_consnames : identifier array; + mind_typename : identifier; + mind_lc : constr; + mind_arity : typed_type; + mind_sort : sorts; + mind_nrealargs : int; + mind_kelim : sorts list; + mind_listrec : (recarg list) array; + mind_finite : bool } + +type mutual_inductive_body = { + mind_kind : path_kind; + mind_ntypes : int; + mind_hyps : typed_type signature; + mind_packets : mutual_inductive_packet array; + mind_constraints : constraints; + mind_singl : constr option; + mind_nparams : int } + +let mind_type_finite mib i = mib.mind_packets.(i).mind_finite + +(*s Declaration. *) + +type mutual_inductive_entry = { + mind_entry_nparams : int; + mind_entry_finite : bool; + mind_entry_inds : (identifier * constr * identifier list * constr) list } + +let mind_nth_type_packet mib n = mib.mind_packets.(n) |