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

7 files changed, 40 insertions, 42 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 949150ba5..3d789b92e 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -968,7 +968,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
 	)
       ]
   in
-  Command.start_proof
+  Lemmas.start_proof
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
@@ -977,7 +977,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
     lemma_type
     (fun _ _ -> ());
   Pfedit.by (prove_replacement);
-  Command.save_named false
+  Lemmas.save_named false
 
 
 
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index f6959d77e..ff4d1e972 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -303,7 +303,7 @@ let pp_dur time time' =
 (* let qed () = save_named true  *)
 let defined () =
   try
-    Command.save_named false
+    Lemmas.save_named false
   with
     | UserError("extract_proof",msg) ->
 	Util.errorlabstrm
@@ -333,7 +333,7 @@ let build_functional_principle interactive_proof old_princ_type sorts funs i pro
     next_global_ident_away true (id_of_string "___________princ_________") []
   in
   begin
-    Command.start_proof
+    Lemmas.start_proof
       new_princ_name
       (Decl_kinds.Global,(Decl_kinds.Proof Decl_kinds.Theorem))
       new_principle_type
@@ -529,15 +529,14 @@ let make_scheme (fas : (constant*Rawterm.rawsort) list) : Entries.definition_ent
     List.map
       (fun (idx) ->
 	 let ind = first_fun_kn,idx in
-	 let (mib,mip) = Global.lookup_inductive ind in
-	 ind,mib,mip,true,prop_sort
+	 ind,true,prop_sort
       )
       funs_indexes
   in
   let l_schemes =
     List.map
       (Typing.type_of env sigma)
-      (Indrec.build_mutual_indrec env sigma ind_list)
+      (Indrec.build_mutual_induction_scheme env sigma ind_list)
   in
   let i = ref (-1) in
   let sorts =
@@ -712,7 +711,7 @@ let build_case_scheme fa =
 	 let ind = first_fun_kn,funs_indexes in
 	 ind,prop_sort
   in
-  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.make_case_gen env sigma ind sf)  ind_fun) in
+  let scheme_type =  (Typing.type_of env sigma ) ((fun (ind,sf) -> Indrec.build_case_analysis_scheme_default env sigma ind sf)  ind_fun) in
   let sorts =
     (fun (_,_,x) ->
        Termops.new_sort_in_family (Pretyping.interp_elimination_sort x)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 68850603b..77389681b 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -150,7 +150,7 @@ let rec abstract_rawconstr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
 (*   Constrintern.interp_rawconstr_with_implicits sigma env [] impls c *)
-  Constrintern.intern_gen false sigma env ~impls:([],impls)
+  Constrintern.intern_gen false sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 
@@ -166,15 +166,12 @@ let build_newrecursive
   let (rec_sign,rec_impls) =
     List.fold_left
       (fun (env,impls) ((_,recname),_,bl,arityc,_) ->
-        let arityc = Command.generalize_constr_expr arityc bl in
+        let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
-	let impl =
-	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits  env0 arity
-	  else [] in
-	let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in
-        (Environ.push_named (recname,None,arity) env, impls'))
+	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
+        (Environ.push_named (recname,None,arity) env, (recname,impl) :: impls))
       (env0,[]) lnameargsardef in
+  let rec_impls = Constrintern.set_internalization_env_params rec_impls [] in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
@@ -367,16 +364,15 @@ let generate_principle  on_error
 let register_struct is_rec fixpoint_exprl =
   match fixpoint_exprl with
     | [((_,fname),_,bl,ret_type,body),_] when not is_rec ->
+	let ce,imps =
+	  Command.interp_definition
+	    (Flags.boxed_definitions ()) bl None body (Some ret_type)
+	in
 	Command.declare_definition
-	  fname
-	  (Decl_kinds.Global,Flags.boxed_definitions (),Decl_kinds.Definition)
-	  bl
-	  None
-  	  body
-	  (Some ret_type)
-	  (fun _ _ -> ())
+	  fname (Decl_kinds.Global,Decl_kinds.Definition)
+	  ce imps (fun _ _ -> ())
     | _ ->
-	Command.build_recursive fixpoint_exprl (Flags.boxed_definitions())
+	Command.do_fixpoint fixpoint_exprl (Flags.boxed_definitions())
 
 let generate_correction_proof_wf f_ref tcc_lemma_ref
     is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
@@ -389,7 +385,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref
 let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body
     pre_hook
     =
-  let type_of_f = Command.generalize_constr_expr ret_type args in
+  let type_of_f = Topconstr.prod_constr_expr ret_type args in
   let rec_arg_num =
     let names =
       List.map
@@ -420,7 +416,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
     Topconstr.CApp (dummy_loc,(None,Topconstr.mkRefC (Qualid (dummy_loc,(qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
-  let eq = Command.generalize_constr_expr unbounded_eq args in
+  let eq = Topconstr.prod_constr_expr unbounded_eq args in
   let hook f_ref tcc_lemma_ref functional_ref eq_ref rec_arg_num rec_arg_type
       nb_args relation =
     try
@@ -531,7 +527,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 			 raise (UserError("",str "Cannot find argument " ++
 					    Ppconstr.pr_id id))
 		     in
- 		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation)
+		     (name,annot,args,types,body),(None:Vernacexpr.decl_notation option)
 		 | (name,None,args,types,body),recdef ->
 		     let names =  (Topconstr.names_of_local_assums args) in
 		     if  is_one_rec recdef  && List.length names > 1 then
@@ -541,7 +537,7 @@ let do_generate_principle on_error register_built interactive_proof fixpoint_exp
 		     else
 		       let loc, na = List.hd names in
 			 (name,(Some (loc, Nameops.out_name na), Topconstr.CStructRec),args,types,body),
-		     (None:Vernacexpr.decl_notation)
+		     (None:Vernacexpr.decl_notation option)
 		 | (_,Some (Wf _),_,_,_),_ | (_,Some (Mes _),_,_,_),_->
 		     error
 		       ("Cannot use mutual definition with well-founded recursion or measure")
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 116a3c991..ca93056ad 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -734,7 +734,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 
 
 
-let do_save () = Command.save_named false
+let do_save () = Lemmas.save_named false
 
 
 (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness
@@ -786,7 +786,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_correct_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
@@ -823,10 +823,10 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     let  mib,mip = Global.lookup_inductive graph_ind in
     let schemes =
       Array.of_list
-	(Indrec.build_mutual_indrec (Global.env ()) Evd.empty
+	(Indrec.build_mutual_induction_scheme (Global.env ()) Evd.empty
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i mip -> (kn,i),mib,mip,true,InType)
+		 (fun i _ -> (kn,i),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
@@ -838,7 +838,7 @@ let derive_correctness make_scheme functional_induction (funs: constant list) (g
     Array.iteri
       (fun i f_as_constant ->
 	 let f_id = id_of_label (con_label f_as_constant) in
-	 Command.start_proof
+	 Lemmas.start_proof
 	   (*i The next call to mk_complete_id is valid since we are constructing the lemma
 	     Ensures by: obvious
 	     i*)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 8aeff61e6..6dc36decf 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -904,7 +904,10 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
     } in *)
   let indexpr = rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  Command.build_mutual [(indexpr,None)] true (* means: not coinductive *)
+  let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,None)] in
+  let mie,impls = Command.interp_mutual_inductive indl [] true (* means: not coinductive *) in
+  (* Declare the mutual inductive block with its associated schemes *)
+  ignore (Command.declare_mutual_inductive_with_eliminations false mie impls)
 
 
 (* Find infos on identifier id. *)
diff --git a/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 4bd0385ca..607734f22 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -1364,7 +1364,7 @@ let do_build_inductive
 (*   in *)
   let _time2 = System.get_time () in
   try
-    with_full_print (Flags.silently (Command.build_mutual rel_inds)) true
+    with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds)) true
   with
     | UserError(s,msg) as e ->
 	let _time3 = System.get_time () in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5499425df..d64b9728b 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -52,8 +52,8 @@ open Genarg
 let compute_renamed_type gls c =
   rename_bound_var (pf_env gls) [] (pf_type_of gls c)
 
-let qed () = Command.save_named true
-let defined () = Command.save_named false
+let qed () = Lemmas.save_named true
+let defined () = Lemmas.save_named false
 
 let pf_get_new_ids idl g =
   let ids = pf_ids_of_hyps g in
@@ -993,7 +993,7 @@ let open_new_goal (build_proof:tactic -> tactic -> unit) using_lemmas ref_ goal_
 	       )
       		 g)
 ;
-    Command.save_named opacity;
+    Lemmas.save_named opacity;
   in
   start_proof
     na
@@ -1042,7 +1042,7 @@ let com_terminate
     nb_args
     hook =
   let start_proof (tac_start:tactic) (tac_end:tactic) =
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     start_proof thm_name
       (Global, Proof Lemma) (Environ.named_context_val env)
       (hyp_terminates nb_args fonctional_ref) hook;
@@ -1322,7 +1322,7 @@ let (com_eqn : identifier ->
 	    else begin match cb.const_body with None -> true | _ -> false end
 	| _ -> anomaly "terminate_lemma: not a constant"
     in
-    let (evmap, env) = Command.get_current_context() in
+    let (evmap, env) = Lemmas.get_current_context() in
     let f_constr = (constr_of_global f_ref) in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
     (start_proof eq_name (Global, Proof Lemma)
@@ -1343,7 +1343,7 @@ let (com_eqn : identifier ->
        );
 (*      (try Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowProof) with _ -> ()); *)
 (*      Vernacentries.interp (Vernacexpr.VernacShow Vernacexpr.ShowScript); *)
-     Flags.silently (fun () ->Command.save_named opacity) () ;
+     Flags.silently (fun () -> Lemmas.save_named opacity) () ;
 (*      Pp.msgnl (str "eqn finished"); *)
 
     );;
@@ -1358,7 +1358,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let function_type = interp_constr Evd.empty (Global.env()) type_of_f in
   let env = push_named (function_name,None,function_type) (Global.env()) in
 (*   Pp.msgnl (str "function type := " ++ Printer.pr_lconstr function_type); *)
-  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:([],rec_impls) eq in
+  let equation_lemma_type = interp_gen (OfType None) Evd.empty env ~impls:rec_impls eq in
 (*   Pp.msgnl (Printer.pr_lconstr equation_lemma_type); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> (x,None,y)) res_vars) env in