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

2 files changed, 61 insertions, 136 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index f134614cbc..e7dbc1af65 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -8,6 +8,10 @@
 
 (* $Id$ *)
 
+(* File initially created by Christine Paulin, 1996 *)
+
+(* This file builds various inductive schemes *)
+
 open Pp
 open Util
 open Names
@@ -27,6 +31,8 @@ open Safe_typing
 open Nametab
 open Sign
 
+type dep_flag = bool
+
 (* Errors related to recursors building *)
 type recursion_scheme_error =
   | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive
@@ -43,16 +49,10 @@ let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c)
 
 (**********************************************************************)
 (* Building case analysis schemes *)
-(* Nouvelle version, plus concise mais plus coûteuse à cause de
-   lift_constructor et lift_inductive_family qui ne se contentent pas de
-   lifter les paramètres globaux *)
+(* Christine Paulin, 1996 *)
 
-let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
+let mis_make_case_com dep env sigma ind (mib,mip as specif) kind =
   let lnamespar = mib.mind_params_ctxt in
-  let dep = match depopt with
-    | None -> inductive_sort_family mip <> InProp
-    | Some d -> d
-  in
   if not (List.mem kind (elim_sorts specif)) then
     raise
       (RecursionSchemeError
@@ -108,6 +108,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind =
 
 (**********************************************************************)
 (* Building the recursive elimination *)
+(* Christine Paulin, 1996 *)
 
 (*
  * t is the type of the constructor co and recargs is the information on
@@ -428,7 +429,7 @@ let mis_make_indrec env sigma listdepkind mib =
 	  it_mkLambda_or_LetIn_name env (put_arity env' 0 listdepkind)
 	    lnamesparrec
       else
-	mis_make_case_com (Some dep) env sigma indi (mibi,mipi) kind
+	mis_make_case_com dep env sigma indi (mibi,mipi) kind
   in
     (* Body of mis_make_indrec *)
     list_tabulate make_one_rec nrec
@@ -436,17 +437,18 @@ let mis_make_indrec env sigma listdepkind mib =
 (**********************************************************************)
 (* This builds elimination predicate for Case tactic *)
 
-let make_case_com depopt env sigma ity kind =
+let build_case_analysis_scheme env sigma ity dep kind =
   let (mib,mip) = lookup_mind_specif env ity in
-    mis_make_case_com depopt env sigma ity (mib,mip) kind
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
-let make_case_dep env   = make_case_com (Some true) env
-let make_case_nodep env = make_case_com (Some false) env
-let make_case_gen env   = make_case_com None env
+let build_case_analysis_scheme_default env sigma ity kind =
+  let (mib,mip) = lookup_mind_specif env ity in
+  let dep = inductive_sort_family mip <> InProp in
+  mis_make_case_com dep env sigma ity (mib,mip) kind
 
 
 (**********************************************************************)
-(* [instantiate_indrec_scheme s rec] replace the sort of the scheme
+(* [modify_sort_scheme s rec] replaces the sort of the scheme
    [rec] by [s] *)
 
 let change_sort_arity sort =
@@ -460,7 +462,7 @@ let change_sort_arity sort =
     drec
 
 (* [npar] is the number of expected arguments (then excluding letin's) *)
-let instantiate_indrec_scheme sort =
+let modify_sort_scheme sort =
   let rec drec npar elim =
     match kind_of_term elim with
       | Lambda (n,t,c) ->
@@ -469,13 +471,13 @@ let instantiate_indrec_scheme sort =
 	  else
 	    mkLambda (n, t, drec (npar-1) c)
       | LetIn (n,b,t,c) -> mkLetIn (n,b,t,drec npar c)
-      | _ -> anomaly "instantiate_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "modify_sort_scheme: wrong elimination type"
   in
   drec
 
 (* Change the sort in the type of an inductive definition, builds the
    corresponding eta-expanded term *)
-let instantiate_type_indrec_scheme sort npars term =
+let weaken_sort_scheme sort npars term =
   let rec drec np elim =
     match kind_of_term elim with
       | Prod (n,t,c) ->
@@ -488,7 +490,7 @@ let instantiate_type_indrec_scheme sort npars term =
 	    mkProd (n, t, c'), mkLambda (n, t, term')
       | LetIn (n,b,t,c) -> let c',term' = drec np c in
            mkLetIn (n,b,t,c'), mkLetIn (n,b,t,term')
-      | _ -> anomaly "instantiate_type_indrec_scheme: wrong elimination type"
+      | _ -> anomaly "weaken_sort_scheme: wrong elimination type"
   in
   drec npars
 
@@ -510,56 +512,29 @@ let check_arities listdepkind =
 	    [] listdepkind
   in true
 
-let build_mutual_indrec env sigma = function
-  | (mind,mib,mip,dep,s)::lrecspec ->
+let build_mutual_induction_scheme env sigma = function
+  | (mind,dep,s)::lrecspec ->
+      let (mib,mip) = Global.lookup_inductive mind in
       let (sp,tyi) = mind in
       let listdepkind =
-    	(mind,mib,mip, dep,s)::
+	(mind,mib,mip,dep,s)::
     	(List.map
-	   (function (mind',mibi',mipi',dep',s') ->
+	   (function (mind',dep',s') ->
 	      let (sp',_) = mind' in
 	      if sp=sp' then
                 let (mibi',mipi') = lookup_mind_specif env mind' in
 		(mind',mibi',mipi',dep',s')
 	      else
-		  raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
+		raise (RecursionSchemeError (NotMutualInScheme (mind,mind'))))
 	   lrecspec)
       in
       let _ = check_arities listdepkind in
       mis_make_indrec env sigma listdepkind mib
-  | _ -> anomaly "build_indrec expects a non empty list of inductive types"
+  | _ -> anomaly "build_induction_scheme expects a non empty list of inductive types"
 
-let build_indrec env sigma ind =
+let build_induction_scheme env sigma ind dep kind =
   let (mib,mip) = lookup_mind_specif env ind in
-  let kind = inductive_sort_family mip in
-  let dep = kind <> InProp in
-    List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
-
-(**********************************************************************)
-(* To handle old Case/Match syntax in Pretyping                       *)
-
-(*****************************************)
-(* To interpret Case and Match operators *)
-(* Expects a dependent predicate *)
-
-let type_rec_branches recursive env sigma indt p c =
-  let IndType (indf,realargs) = indt in
-  let (ind,params) = dest_ind_family indf in
-  let (mib,mip) = lookup_mind_specif env ind in
-  let recargs = mip.mind_recargs in
-  let tyi = snd ind in
-  let init_depPvec i = if i = tyi then Some(true,p) else None in
-  let depPvec = Array.init mib.mind_ntypes init_depPvec in
-  let constructors = get_constructors env indf in
-  let lft =
-    array_map2
-      (type_rec_branch recursive true env sigma (params,depPvec,0) tyi)
-      constructors (dest_subterms recargs) in
-  (lft,Reduction.beta_appvect p (Array.of_list (realargs@[c])))
-(* Non recursive case. Pb: does not deal with unification
-    let (p,ra,_) = type_case_branches env (ind,params@realargs) pj c in
-    (p,ra)
-*)
+  List.hd (mis_make_indrec env sigma [(ind,mib,mip,dep,kind)] mib)
 
 (*s Eliminations. *)
 
@@ -568,6 +543,8 @@ let elimination_suffix = function
   | InSet  -> "_rec"
   | InType -> "_rect"
 
+let case_suffix = "_case"
+
 let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 (* Look up function for the default elimination constant *)
@@ -595,59 +572,3 @@ let lookup_eliminator ind_sp s =
        pr_global_env Idset.empty (IndRef ind_sp) ++
        strbrk " on sort " ++ pr_sort_family s ++
        strbrk " is probably not allowed.")
-
-(* Build the congruence lemma associated to an inductive type
-   I p1..pn a1..am with one constructor C : I q1..qn b1..bm *)
-
-(* TODO: extend it to types with more than one index *)
-
-let build_congr env (eq,refl) ind (mib,mip) =
-  if Array.length mib.mind_packets <> 1 or Array.length mip.mind_nf_lc <> 1 then
-    error "Not an inductive type with a single constructor.";
-  if mip.mind_nrealargs <> 1 then
-    error "Expect an inductive type with one predicate parameter.";
-  let i = 1 in
-  let realsign,_ = list_chop mip.mind_nrealargs_ctxt mip.mind_arity_ctxt in
-  if List.exists (fun (_,b,_) -> b <> None) realsign then
-    error "Inductive equalities with local definitions in arity not supported";
-  let env_with_arity = push_rel_context mip.mind_arity_ctxt env in
-  let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
-  let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
-  let _,constrargs = decompose_app ccl in
-  if rel_context_length constrsign<>rel_context_length mib.mind_params_ctxt then
-    error "Constructor must have no arguments";
-  let c = List.nth constrargs (i + mib.mind_nparams - 1) in
-  let varB = id_of_string "B" in
-  let varH = id_of_string "H" in
-  let varf = id_of_string "f" in
-  let ci = make_case_info (Global.env()) ind RegularStyle in
-  let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn ~init:c s in
-  let my_it_mkLambda_or_LetIn_name s c = it_mkLambda_or_LetIn_name env c s in
-  my_it_mkLambda_or_LetIn mib.mind_params_ctxt
-     (mkNamedLambda varB (new_Type ())
-     (mkNamedLambda varf (mkArrow (lift 1 ty) (mkVar varB))
-     (my_it_mkLambda_or_LetIn_name (lift_rel_context 2 realsign)
-     (mkNamedLambda varH
-        (applist
-           (mkInd ind,
-	    extended_rel_list (mip.mind_nrealargs+2) mib.mind_params_ctxt @
-	    extended_rel_list 0 realsign))
-     (mkCase (ci,
-       my_it_mkLambda_or_LetIn_name
-	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
-         (mkLambda
-           (Anonymous,
-            applist
-             (mkInd ind,
-	        extended_rel_list (2*mip.mind_nrealargs_ctxt+3)
-		  mib.mind_params_ctxt
-	        @ extended_rel_list 0 realsign),
-            mkApp (eq,
-	      [|mkVar varB;
-                mkApp (mkVar varf, [|lift (2*mip.mind_nrealargs_ctxt+4) c|]);
-		mkApp (mkVar varf, [|mkRel (mip.mind_nrealargs - i + 2)|])|]))),
-       mkVar varH,
-       [|mkApp (refl,
-          [|mkVar varB;
-	    mkApp (mkVar varf, [|lift (mip.mind_nrealargs+3) c|])|])|]))))))
-
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index ac6a61c3c4..91d559e17e 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -27,36 +27,41 @@ exception RecursionSchemeError of recursion_scheme_error
 
 (** Eliminations *)
 
-(* These functions build elimination predicate for Case tactic *)
+type dep_flag = bool
 
-val make_case_dep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_nodep : env -> evar_map -> inductive -> sorts_family -> constr
-val make_case_gen : env -> evar_map -> inductive -> sorts_family -> constr
+(* Build a case analysis elimination scheme in some sort family *)
 
-(* This builds an elimination scheme associated (using the own arity
-   of the inductive) *)
+val build_case_analysis_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val build_indrec : env -> evar_map -> inductive -> constr
-val instantiate_indrec_scheme : sorts -> int -> constr -> constr
-val instantiate_type_indrec_scheme : sorts -> int -> constr -> types ->
-  constr * types
+(* Build a dependent case elimination predicate unless type is in Prop *)
 
-(** Complex recursion schemes [Scheme] *)
+val build_case_analysis_scheme_default : env -> evar_map -> inductive ->
+      sorts_family -> constr
 
-val build_mutual_indrec :
-  env -> evar_map ->
-    (inductive * mutual_inductive_body * one_inductive_body
-    * bool * sorts_family) list
-    -> constr list
+(* Builds a recursive induction scheme (Peano-induction style) in the same
+   sort family as the inductive family; it is dependent if not in Prop *)
 
-(** Old Case/Match typing *)
+val build_induction_scheme : env -> evar_map -> inductive ->
+      dep_flag -> sorts_family -> constr
 
-val type_rec_branches : bool -> env -> evar_map -> inductive_type
-  -> constr -> constr -> constr array * constr
-val make_rec_branch_arg :
-  env -> evar_map ->
-    int * ('b * constr) option array * int ->
-    constr -> constructor_summary -> wf_paths list -> constr
+(* Builds mutual (recursive) induction schemes *)
+
+val build_mutual_induction_scheme :
+  env -> evar_map -> (inductive * dep_flag * sorts_family) list -> constr list
+
+(** Scheme combinators *)
+
+(* [modify_sort_scheme s n c] modifies the quantification sort of
+   scheme c whose predicate is abstracted at position [n] of [c] *)
+
+val modify_sort_scheme : sorts -> int -> constr -> constr
+
+(* [weaken_sort_scheme s n c t] derives by subtyping from [c:t]
+   whose conclusion is quantified on [Type] at position [n] of [t] a
+   scheme quantified on sort [s] *)
+
+val weaken_sort_scheme : sorts -> int -> constr -> types -> constr * types
 
 (** Recursor names utilities *)
 
@@ -64,5 +69,4 @@ val lookup_eliminator : inductive -> sorts_family -> constr
 val elimination_suffix : sorts_family -> string
 val make_elimination_ident : identifier -> sorts_family -> identifier
 
-
-
+val case_suffix : string