Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7

12 files changed, 101 insertions, 193 deletions

diff --git a/library/decl_kinds.mli b/intf/decl_kinds.mli
index 5b81d54ee..6ee6f707d 100644
--- a/library/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -6,10 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
-open Util
-open Libnames
-
 (** Informal mathematical status of declarations *)
 
 type locality =
@@ -68,24 +64,9 @@ type logical_kind =
   | IsDefinition of definition_object_kind
   | IsProof of theorem_kind
 
-(** Utils *)
-
-val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
-val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_kind :
-  locality * definition_object_kind -> string
-
-(** About locality *)
-
-val strength_of_global : global_reference -> locality
-val string_of_strength : locality -> string
-
-(** About recursive power of type declarations *)
+(** Recursive power of type declarations *)
 
 type recursivity_kind =
   | Finite (** = inductive *)
   | CoFinite (** = coinductive *)
   | BiFinite (** = non-recursive, like in "Record" definitions *)
-
-(** helper, converts to "finiteness flag" booleans *)
-val recursivity_flag_of_kind : recursivity_kind -> bool
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
deleted file mode 100644
index e8734cbaa..000000000
--- a/library/decl_kinds.ml
+++ /dev/null
@@ -1,126 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Errors
-open Util
-open Libnames
-
-(* Informal mathematical status of declarations *)
-
-type locality =
-  | Local
-  | Global
-
-type theorem_kind =
-  | Theorem
-  | Lemma
-  | Fact
-  | Remark
-  | Property
-  | Proposition
-  | Corollary
-
-type definition_object_kind =
-  | Definition
-  | Coercion
-  | SubClass
-  | CanonicalStructure
-  | Example
-  | Fixpoint
-  | CoFixpoint
-  | Scheme
-  | StructureComponent
-  | IdentityCoercion
-  | Instance
-  | Method
-
-type assumption_object_kind = Definitional | Logical | Conjectural
-
-(* [assumption_kind]
-
-                |  Local      | Global
-   ------------------------------------
-   Definitional |  Variable   | Parameter
-   Logical      |  Hypothesis | Axiom
-
-*)
-type assumption_kind = locality * assumption_object_kind
-
-type definition_kind = locality * definition_object_kind
-
-(* Kinds used in proofs *)
-
-type goal_object_kind =
-  | DefinitionBody of definition_object_kind
-  | Proof of theorem_kind
-
-type goal_kind = locality * goal_object_kind
-
-(* Kinds used in library *)
-
-type logical_kind =
-  | IsAssumption of assumption_object_kind
-  | IsDefinition of definition_object_kind
-  | IsProof of theorem_kind
-
-(* Utils *)
-
-let logical_kind_of_goal_kind = function
-  | DefinitionBody d -> IsDefinition d
-  | Proof s -> IsProof s
-
-let string_of_theorem_kind = function
-  | Theorem -> "Theorem"
-  | Lemma -> "Lemma"
-  | Fact -> "Fact"
-  | Remark -> "Remark"
-  | Property -> "Property"
-  | Proposition -> "Proposition"
-  | Corollary -> "Corollary"
-
-let string_of_definition_kind def =
-  match def with
-  | Local, Coercion -> "Coercion Local"
-  | Global, Coercion -> "Coercion"
-  | Local, Definition -> "Let"
-  | Global, Definition -> "Definition"
-  | Local, SubClass -> "Local SubClass"
-  | Global, SubClass -> "SubClass"
-  | Global, CanonicalStructure -> "Canonical Structure"
-  | Global, Example -> "Example"
-  | Local, (CanonicalStructure|Example) ->
-      anomaly "Unsupported local definition kind"
-  | Local, Instance -> "Instance"
-  | Global, Instance -> "Global Instance"
-  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
-      -> anomaly "Internal definition kind"
-
-(* Strength *)
-
-let strength_of_global = function
-  | VarRef _ -> Local
-  | IndRef _ | ConstructRef _ | ConstRef _ -> Global
-
-let string_of_strength = function
-  | Local -> "Local"
-  | Global -> "Global"
-
-
-(* Recursive power *)
-
-(* spiwack: this definition might be of use in the kernel, for now I do not
-                   push them deeper than needed, though. *)
-type recursivity_kind =
-  | Finite (* = inductive *)
-  | CoFinite (* = coinductive *)
-  | BiFinite (* = non-recursive, like in "Record" definitions *)
-
-(* helper, converts to "finiteness flag" booleans *)
-let recursivity_flag_of_kind = function
-  | Finite | BiFinite -> true
-  | CoFinite -> false
diff --git a/library/kindops.ml b/library/kindops.ml
new file mode 100644
index 000000000..012e599e2
--- /dev/null
+++ b/library/kindops.ml
@@ -0,0 +1,41 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Decl_kinds
+
+(** Operations about types defined in [Decl_kinds] *)
+
+let logical_kind_of_goal_kind = function
+  | DefinitionBody d -> IsDefinition d
+  | Proof s -> IsProof s
+
+let string_of_theorem_kind = function
+  | Theorem -> "Theorem"
+  | Lemma -> "Lemma"
+  | Fact -> "Fact"
+  | Remark -> "Remark"
+  | Property -> "Property"
+  | Proposition -> "Proposition"
+  | Corollary -> "Corollary"
+
+let string_of_definition_kind def =
+  match def with
+  | Local, Coercion -> "Coercion Local"
+  | Global, Coercion -> "Coercion"
+  | Local, Definition -> "Let"
+  | Global, Definition -> "Definition"
+  | Local, SubClass -> "Local SubClass"
+  | Global, SubClass -> "SubClass"
+  | Global, CanonicalStructure -> "Canonical Structure"
+  | Global, Example -> "Example"
+  | Local, (CanonicalStructure|Example) ->
+      Errors.anomaly "Unsupported local definition kind"
+  | Local, Instance -> "Instance"
+  | Global, Instance -> "Global Instance"
+  | _, (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method)
+      -> Errors.anomaly "Internal definition kind"
diff --git a/library/kindops.mli b/library/kindops.mli
new file mode 100644
index 000000000..c7f2a2e7f
--- /dev/null
+++ b/library/kindops.mli
@@ -0,0 +1,16 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Decl_kinds
+
+(** Operations about types defined in [Decl_kinds] *)
+
+val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
+val string_of_theorem_kind : theorem_kind -> string
+val string_of_definition_kind :
+  locality * definition_object_kind -> string
diff --git a/library/library.mllib b/library/library.mllib
index e8b5a7a4c..edd5bfc07 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -8,7 +8,7 @@ Lib
 Declaremods
 Library
 States
-Decl_kinds
+Kindops
 Dischargedhypsmap
 Goptions
 Decls
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 0852f846a..9f0cc4c03 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -360,7 +360,7 @@ let pr_ne_params_list pr_c l =
   prlist_with_sep pr_semicolon (pr_params pr_c)
 *)
 
-let pr_thm_token k = str (string_of_theorem_kind k)
+let pr_thm_token k = str (Kindops.string_of_theorem_kind k)
 
 let pr_syntax_modifier = function
   | SetItemLevel (l,NextLevel) ->
@@ -532,7 +532,7 @@ let rec pr_vernac = function
 
   (* Gallina *)
   | VernacDefinition (d,id,b,f) -> (* A verifier... *)
-      let pr_def_token dk = str (string_of_definition_kind dk) in
+      let pr_def_token dk = str (Kindops.string_of_definition_kind dk) in
       let pr_reduce = function
         | None -> mt()
         | Some r ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 60aa99b12..de7e17957 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,16 +163,16 @@ let save with_clean id const (locality,kind) hook =
        const_entry_opaque = opacity } = const in
   let l,r = match locality with
     | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Local ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn)
     | Global ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   if with_clean then  Pfedit.delete_current_proof ();
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 13821488a..93ff00dff 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -64,12 +64,12 @@ let extract_nparams pack =
 
 *)
 
+open Decl_kinds
+
 (* could_have_namesakes sp = true iff o is an object that could be cooked and *)
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
- let module DK = Decl_kinds in
- let module D = Declare in
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
@@ -106,11 +106,6 @@ let filter_params pvars hyps =
    aux (Names.repr_dirpath modulepath) (List.rev pvars)
 ;;
 
-type variables_type =
-   Definition of string * Term.constr * Term.types
- | Assumption of string * Term.constr
-;;
-
 (* The computation is very inefficient, but we can't do anything *)
 (* better unless this function is reimplemented in the Declare   *)
 (* module.                                                       *)
@@ -401,9 +396,9 @@ let theory_output_string ?(do_not_quote = false) s =
 ;;
 
 let kind_of_global_goal = function
-  | Decl_kinds.Global, Decl_kinds.DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
-  | Decl_kinds.Global, (Decl_kinds.Proof k) -> "THEOREM",Decl_kinds.string_of_theorem_kind k
-  | Decl_kinds.Local, _ -> assert false
+  | Global, DefinitionBody _ -> "DEFINITION","InteractiveDefinition"
+  | Global, (Proof k) -> "THEOREM",Kindops.string_of_theorem_kind k
+  | Local, _ -> assert false
 
 let kind_of_inductive isrecord kn =
  "DEFINITION",
@@ -417,68 +412,65 @@ let kind_of_inductive isrecord kn =
 ;;
 
 let kind_of_variable id =
-  let module DK = Decl_kinds in
   match Decls.variable_kind id with
-    | DK.IsAssumption DK.Definitional -> "VARIABLE","Assumption"
-    | DK.IsAssumption DK.Logical -> "VARIABLE","Hypothesis"
-    | DK.IsAssumption DK.Conjectural -> "VARIABLE","Conjecture"
-    | DK.IsDefinition DK.Definition -> "VARIABLE","LocalDefinition"
-    | DK.IsProof _ -> "VARIABLE","LocalFact"
+    | IsAssumption Definitional -> "VARIABLE","Assumption"
+    | IsAssumption Logical -> "VARIABLE","Hypothesis"
+    | IsAssumption Conjectural -> "VARIABLE","Conjecture"
+    | IsDefinition Definition -> "VARIABLE","LocalDefinition"
+    | IsProof _ -> "VARIABLE","LocalFact"
     | _ -> Errors.anomaly "Unsupported variable kind"
 ;;
 
 let kind_of_constant kn =
-  let module DK = Decl_kinds in
   match Decls.constant_kind kn with
-    | DK.IsAssumption DK.Definitional -> "AXIOM","Declaration"
-    | DK.IsAssumption DK.Logical -> "AXIOM","Axiom"
-    | DK.IsAssumption DK.Conjectural ->
+    | IsAssumption Definitional -> "AXIOM","Declaration"
+    | IsAssumption Logical -> "AXIOM","Axiom"
+    | IsAssumption Conjectural ->
         Pp.warning "Conjecture not supported in dtd (used Declaration instead)";
         "AXIOM","Declaration"
-    | DK.IsDefinition DK.Definition -> "DEFINITION","Definition"
-    | DK.IsDefinition DK.Example ->
+    | IsDefinition Definition -> "DEFINITION","Definition"
+    | IsDefinition Example ->
         Pp.warning "Example not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Coercion ->
+    | IsDefinition Coercion ->
         Pp.warning "Coercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.SubClass ->
+    | IsDefinition SubClass ->
         Pp.warning "SubClass not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.CanonicalStructure ->
+    | IsDefinition CanonicalStructure ->
         Pp.warning "CanonicalStructure not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Fixpoint ->
+    | IsDefinition Fixpoint ->
         Pp.warning "Fixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.CoFixpoint ->
+    | IsDefinition CoFixpoint ->
         Pp.warning "CoFixpoint not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Scheme ->
+    | IsDefinition Scheme ->
         Pp.warning "Scheme not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.StructureComponent ->
+    | IsDefinition StructureComponent ->
         Pp.warning "StructureComponent not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.IdentityCoercion ->
+    | IsDefinition IdentityCoercion ->
         Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Instance ->
+    | IsDefinition Instance ->
         Pp.warning "Instance not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsDefinition DK.Method ->
+    | IsDefinition Method ->
         Pp.warning "Method not supported in dtd (used Definition instead)";
         "DEFINITION","Definition"
-    | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) ->
-        "THEOREM",DK.string_of_theorem_kind thm
-    | DK.IsProof _ ->
+    | IsProof (Theorem|Lemma|Corollary|Fact|Remark as thm) ->
+        "THEOREM",Kindops.string_of_theorem_kind thm
+    | IsProof _ ->
         Pp.warning "Unsupported theorem kind (used Theorem instead)";
-        "THEOREM",DK.string_of_theorem_kind DK.Theorem
+        "THEOREM",Kindops.string_of_theorem_kind Theorem
 ;;
 
 let kind_of_global r =
   let module Ln = Libnames in
-  let module DK = Decl_kinds in
   match r with
   | Ln.IndRef kn | Ln.ConstructRef (kn,_) ->
       let isrecord =
diff --git a/toplevel/class.ml b/toplevel/class.ml
index be2482a2b..9adf68031 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -160,6 +160,10 @@ let strength_of_cl = function
   | CL_SECVAR id -> Local
   | _ -> Global
 
+let strength_of_global = function
+  | VarRef _ -> Local
+  | _ -> Global
+
 let get_strength stre ref cls clt =
   let stres = strength_of_cl cls in
   let stret = strength_of_cl clt in
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 2d4633427..00592848f 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -161,7 +161,7 @@ let save id const do_guard (locality,kind) hook =
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
-  let k = logical_kind_of_goal_kind kind in
+  let k = Kindops.logical_kind_of_goal_kind kind in
   let l,r = match locality with
     | Local when Lib.sections_are_opened () ->
 	let c = SectionLocalDef (pft, tpo, opacity) in
@@ -203,7 +203,7 @@ let save_remaining_recthms (local,kind) body opaq i (id,(t_i,(_,imps))) =
           let kn = declare_constant id (ParameterEntry (None,t_i,None), k) in
           (Global,ConstRef kn,imps))
   | Some body ->
-      let k = logical_kind_of_goal_kind kind in
+      let k = Kindops.logical_kind_of_goal_kind kind in
       let body_i = match kind_of_term body with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index ed57bfc49..c6f620ae5 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -270,7 +270,7 @@ let declare_structure finite infer id idbuild paramimpls params arity fieldimpls
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
       mind_entry_record = true;
-      mind_entry_finite = recursivity_flag_of_kind finite;
+      mind_entry_finite = finite<>CoFinite;
       mind_entry_inds = [mie_ind] } in
   let kn = Command.declare_mutual_inductive_with_eliminations KernelVerbose mie [(paramimpls,[])] in
   let rsp = (kn,0) in (* This is ind path of idstruc *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b6e625136..fc51e1348 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -449,7 +449,7 @@ let vernac_inductive finite infer indl =
       | _ -> Errors.error "Cannot handle mutually (co)inductive records."
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl (recursivity_flag_of_kind finite)
+    do_mutual_inductive indl (finite<>CoFinite)
 
 let vernac_fixpoint l =
   if Dumpglob.dump () then