Restructuration of command.ml + generic infrastructure for inductive schemes

- Cleaning and uniformisation in command.ml:
  - For better modularity and better visibility, two files got isolated
    out of command.ml:
    - lemmas.ml is about starting and saving a proof
    - indschemes.ml is about declaring inductive schemes
  - Decomposition of the functions of command.ml into a functional part
    and the imperative part
- Inductive schemes:
  - New architecture in ind_tables.ml for registering scheme builders,
    and for sharing and generating on demand inductive schemes
  - Adding new automatically generated equality schemes (file eqschemes.ml)
    - "_congr" for equality types (completing here commit 12273)
    - "_rew_forward" (similar to vernac-level eq_rect_r), "_rew_forward_dep",
      "_rew_backward" (similar to eq_rect), "_rew_backward_dep" for
      rewriting schemes (warning, rew_forward_dep cannot be stated following
      the standard Coq pattern for inductive types: "t=u" cannot be the
      last argument of the scheme)
    - "_case", "_case_nodep", "_case_dep" for case analysis schemes
  - Preliminary step towards discriminate and injection working on any
    equality-like type (e.g. eq_true)
  - Restating JMeq_congr under the canonical form of congruence schemes
  - Renamed "Set Equality Scheme" into "Set Equality Schemes"
  - Added "Set Rewriting Schemes", "Set Case Analysis Schemes"
  - Activation of the automatic generation of boolean equality lemmas
  - Partial debug and error messages improvements for the generation of
    boolean equality and decidable equality
  - Added schemes for making dependent rewrite working (unfortunately with
    not a fully satisfactory design - see file eqschemes.ml)
- Some names of ML function made more regular (see dev/doc/changes.txt)
- Incidentally, added a flush to obsolete Local/Global syntax warning

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

1 files changed, 28 insertions, 12 deletions

diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index e13eedbdc..57ebbcda1 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -11,25 +11,41 @@ open Names
 open Libnames
 open Mod_subst
 open Sign
+open Declarations
 
+(* This module provides support for registering inductive scheme builders,
+   declaring schemes and generating schemes on demand *)
 
-val cache_scheme :(object_name*(Indmap.key*constr)) -> unit
+(* A scheme is either a "mutual scheme_kind" or an "individual scheme_kind" *)
 
-val find_eq_scheme : Indmap.key -> constr
-val check_eq_scheme : Indmap.key -> bool
+type mutual
+type individual
+type 'a scheme_kind
 
-val cache_bl: (object_name*(Indmap.key*constr)) -> unit
-val cache_lb: (object_name*(Indmap.key*constr)) -> unit
-val cache_dec : (object_name*(Indmap.key*constr)) -> unit
+type mutual_scheme_object_function = mutual_inductive -> constr array
+type individual_scheme_object_function = inductive -> constr
 
-val find_bl_proof : Indmap.key -> constr
-val find_lb_proof : Indmap.key -> constr
-val find_eq_dec_proof : Indmap.key -> constr
+(* Main functions to register a scheme builder *)
 
-val check_bl_proof: Indmap.key -> bool
-val check_lb_proof: Indmap.key -> bool
-val check_dec_proof: Indmap.key -> bool
+val declare_mutual_scheme_object : string -> ?aux:string ->
+  mutual_scheme_object_function -> mutual scheme_kind
 
+val declare_individual_scheme_object : string -> ?aux:string ->
+  individual_scheme_object_function -> individual scheme_kind
 
+(*
+val declare_scheme : 'a scheme_kind -> (inductive * constant) array -> unit
+*)
 
+(* Force generation of a (mutually) scheme with possibly user-level names *)
 
+val define_individual_scheme : individual scheme_kind -> bool (* internal *) ->
+  identifier option -> inductive -> constant
+
+val define_mutual_scheme : mutual scheme_kind -> bool (* internal *) ->
+  (int * identifier) list -> mutual_inductive -> constant array
+
+(* Main function to retrieve a scheme in the cache or to generate it *)
+val find_scheme : 'a scheme_kind -> inductive -> constant
+
+val check_scheme : 'a scheme_kind -> inductive -> bool