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

5 files changed, 174 insertions, 38 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 0057edad6..36a219a61 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -24,15 +24,32 @@ open Nametab
 open Notation
 open Inductiveops
 
-(* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions *)
-type var_internalisation_type = Inductive | Recursive | Method
-
-type var_internalisation_data =
-  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
-
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+(* To interpret implicits and arg scopes of variables in inductive
+   types and recursive definitions and of projection names in records *)
+
+type var_internalization_type = Inductive | Recursive | Method
+
+type var_internalization_data =
+    (* type of the "free" variable, for coqdoc, e.g. while typing the
+       constructor of JMeq, "JMeq" behaves as a variable of type Inductive *)
+    var_internalization_type *
+    (* impargs to automatically add to the variable, e.g. for "JMeq A a B b"
+       in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
+    identifier list *
+    (* signature of impargs of the variable *)
+    Impargs.implicits_list *
+    (* subscopes of the args of the variable *)
+    scope_name option list
+
+type internalization_env =
+    (identifier * var_internalization_data) list
+
+type full_internalization_env =
+    (* a superset of the list of variables that may be automatically
+       inserted and that must not occur as binders *)
+    identifier list *
+    (* mapping of the variables to their internalization data *)
+    internalization_env
 
 type raw_binder = (name * binding_kind * rawconstr option * rawconstr)
 
@@ -155,6 +172,35 @@ let error_inductive_parameter_not_implicit loc =
     "the 'return' clauses; they must be replaced by '_' in the 'in' clauses."))
 
 (**********************************************************************)
+(* Pre-computing the implicit arguments and arguments scopes needed   *)
+(* for interpretation *)
+
+let empty_internalization_env = ([],[])
+
+let set_internalization_env_params ienv params =
+  let nparams = List.length params in
+  if nparams = 0 then
+    ([],ienv)
+  else
+    let ienv_with_implicit_params =
+      List.map (fun (id,(ty,_,impl,scopes)) ->
+	let sub_impl,_ = list_chop nparams impl in
+	let sub_impl' = List.filter is_status_implicit sub_impl in
+	(id,(ty,List.map name_of_implicit sub_impl',impl,scopes))) ienv in
+    (params, ienv_with_implicit_params)
+
+let compute_internalization_data env ty typ impls =
+  let impl = compute_implicits_with_manual env typ (is_implicit_args()) impls in
+  (ty, [], impl, compute_arguments_scope typ)
+
+let compute_full_internalization_env env ty params idl typl impll =
+  set_internalization_env_params
+    (list_map3
+      (fun id typ impl -> (id,compute_internalization_data env ty typ impl))
+      idl typl impll)
+    params
+
+(**********************************************************************)
 (* Contracting "{ _ }" in notations *)
 
 let rec wildcards ntn n =
@@ -368,7 +414,7 @@ let intern_var (env,unbound_vars,_,_ as genv) (ltacvars,vars2,vars3,(_,impls)) l
 	(* [id] a goal variable *)
 	RVar (loc,id), [], [], []
 
-let find_appl_head_data (_,_,_,(_,impls)) = function
+let find_appl_head_data _ = function
   | RRef (_,ref) as x -> x,implicits_of_global ref,find_arguments_scope ref,[]
   | x -> x,[],[],[]
 
@@ -1405,12 +1451,12 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_rawconstr c
 
-let interp_aconstr impls (vars,varslist) a =
+let interp_aconstr ?(impls=([],[])) (vars,varslist) a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) (vars@varslist) in
   let c = internalise Evd.empty (Global.env()) (extract_ids env, false, None, [])
-    false (([],[]),Environ.named_context env,vl,([],impls)) a in
+    false (([],[]),Environ.named_context env,vl,impls) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index b39f6e18b..b08b8dd1f 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,19 +33,42 @@ open Pretyping
    - insert existential variables for implicit arguments
 *)
 
-(* To interpret implicits and arg scopes of recursive variables in
-   inductive types and recursive definitions; mention of a list of
-   implicits arguments in the ``rel'' part of [env]; the second
-   argument associates a list of implicit positions and scopes to
-   identifiers declared in the [rel_context] of [env] *)
+(* To interpret implicits and arg scopes of recursive variables while
+   internalizing inductive types and recursive definitions, and also
+   projection while typing records.
 
-type var_internalisation_type = Inductive | Recursive | Method
+   the third and fourth arguments associate a list of implicit
+   positions and scopes to identifiers declared in the [rel_context]
+   of [env] *)
 
-type var_internalisation_data =
-  var_internalisation_type * identifier list * Impargs.implicits_list * scope_name option list
+type var_internalization_type = Inductive | Recursive | Method
 
-type implicits_env = (identifier * var_internalisation_data) list
-type full_implicits_env = identifier list * implicits_env
+type var_internalization_data =
+    var_internalization_type *
+    identifier list *
+    Impargs.implicits_list *
+    scope_name option list
+
+(* A map of free variables to their implicit arguments and scopes *)
+type internalization_env =
+    (identifier * var_internalization_data) list
+
+(* Contains also a list of identifiers to automatically apply to the variables*)
+type full_internalization_env =
+    identifier list * internalization_env
+
+val empty_internalization_env : full_internalization_env
+
+val compute_internalization_data : env -> var_internalization_type ->
+  types -> Impargs.manual_explicitation list -> var_internalization_data
+
+val set_internalization_env_params :
+  internalization_env -> identifier list -> full_internalization_env
+
+val compute_full_internalization_env : env ->
+  var_internalization_type ->
+  identifier list -> identifier list -> types list ->
+  Impargs.manual_explicitation list list -> full_internalization_env
 
 type manual_implicits = (explicitation * (bool * bool * bool)) list
 
@@ -60,7 +83,7 @@ val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 val intern_type : evar_map -> env -> constr_expr -> rawconstr
 
 val intern_gen : bool -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
 
 val intern_pattern : env -> cases_pattern_expr ->
@@ -69,12 +92,12 @@ val intern_pattern : env -> cases_pattern_expr ->
 
 val intern_context : bool -> evar_map -> env -> local_binder list -> raw_binder list
 
-(*s Composing internalisation with pretyping *)
+(*s Composing internalization with pretyping *)
 
 (* Main interpretation function *)
 
 val interp_gen : typing_constraint -> evar_map -> env ->
-  ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> constr
 
 (* Particular instances *)
@@ -82,33 +105,33 @@ val interp_gen : typing_constraint -> evar_map -> env ->
 val interp_constr : evar_map -> env ->
   constr_expr -> constr
 
-val interp_type : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_type : evar_map -> env -> ?impls:full_internalization_env ->
   constr_expr -> types
 
 val interp_open_constr   : evar_map -> env -> constr_expr -> evar_map * constr
 
 val interp_open_constr_patvar   : evar_map -> env -> constr_expr -> evar_map * constr
 
-val interp_casted_constr : evar_map -> env -> ?impls:full_implicits_env ->
+val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env ->
   constr_expr -> types -> constr
 
 (* Accepting evars and giving back the manual implicits in addition. *)
 
 val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env ->
-  ?impls:full_implicits_env -> constr_expr -> types -> constr * manual_implicits
+  ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits
 
 val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_implicits_env ->
+  env -> ?impls:full_internalization_env ->
   constr_expr -> types * manual_implicits
 
 val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool ->
-  env -> ?impls:full_implicits_env ->
+  env -> ?impls:full_internalization_env ->
   constr_expr -> constr * manual_implicits
 
 val interp_casted_constr_evars : evar_defs ref -> env ->
-  ?impls:full_implicits_env -> constr_expr -> types -> constr
+  ?impls:full_internalization_env -> constr_expr -> types -> constr
 
-val interp_type_evars : evar_defs ref -> env -> ?impls:full_implicits_env ->
+val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env ->
   constr_expr -> types
 
 (*s Build a judgment  *)
@@ -147,8 +170,8 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
 
 (* Interprets into a abbreviatable constr *)
 
-val interp_aconstr : implicits_env -> identifier list * identifier list
-  -> constr_expr -> interpretation
+val interp_aconstr : ?impls:full_internalization_env ->
+  identifier list * identifier list -> constr_expr -> interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 90432a4a4..1ca82e35c 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -215,9 +215,11 @@ type coq_eq_data = {
   trans: constr;
   congr: constr }
 
-type coq_rewrite_data = {
-  rrec : constr option;
-  rect : constr option
+(* Data needed for discriminate and injection *)
+type coq_inversion_data = {
+  inv_eq   : constr; (* : forall params, t -> Prop *)
+  inv_ind  : constr; (* : forall params P y, eq params y -> P y *)
+  inv_congr: constr  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
 }
 
 let lazy_init_constant dir id = lazy (init_constant dir id)
@@ -234,6 +236,8 @@ let coq_eq_congr = lazy_init_constant ["Logic"] "f_equal"
 let coq_eq_sym  = lazy_init_constant ["Logic"] "eq_sym"
 let coq_eq_trans  = lazy_init_constant ["Logic"] "eq_trans"
 let coq_f_equal2 = lazy_init_constant ["Logic"] "f_equal2"
+let coq_eq_congr_canonical =
+  lazy_init_constant ["Logic"] "f_equal_canonical_form"
 
 let build_coq_eq_data () =
   let _ = check_required_library logic_module_name in {
@@ -245,11 +249,18 @@ let build_coq_eq_data () =
   congr = Lazy.force coq_eq_congr }
 
 let build_coq_eq () = Lazy.force coq_eq_eq
+let build_coq_eq_refl () = Lazy.force coq_eq_refl
 let build_coq_eq_sym () = Lazy.force coq_eq_sym
 let build_coq_f_equal2 () = Lazy.force coq_f_equal2
 
 let build_coq_sym_eq = build_coq_eq_sym (* compatibility *)
 
+let build_coq_inversion_eq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_eq;
+  inv_ind = Lazy.force coq_eq_ind;
+  inv_congr = Lazy.force coq_eq_congr_canonical }
+
 (* Heterogenous equality on Type *)
 
 let coq_jmeq_eq = lazy_logic_constant ["JMeq"] "JMeq"
@@ -260,6 +271,8 @@ let coq_jmeq_rect = lazy_logic_constant ["JMeq"] "JMeq_rect"
 let coq_jmeq_sym  = lazy_logic_constant ["JMeq"] "JMeq_sym"
 let coq_jmeq_congr  = lazy_logic_constant ["JMeq"] "JMeq_congr"
 let coq_jmeq_trans  = lazy_logic_constant ["JMeq"] "JMeq_trans"
+let coq_jmeq_congr_canonical =
+  lazy_logic_constant ["JMeq"] "JMeq_congr_canonical_form"
 
 let build_coq_jmeq_data () =
   let _ = check_required_library jmeq_module_name in {
@@ -270,6 +283,17 @@ let build_coq_jmeq_data () =
   trans = Lazy.force coq_jmeq_trans;
   congr = Lazy.force coq_jmeq_congr }
 
+let join_jmeq_types eq =
+  mkLambda(Name (id_of_string "A"),Termops.new_Type(),
+  mkLambda(Name (id_of_string "x"),mkRel 1,
+  mkApp (eq,[|mkRel 2;mkRel 1;mkRel 2|])))
+
+let build_coq_inversion_jmeq_data () =
+  let _ = check_required_library logic_module_name in {
+  inv_eq = join_jmeq_types (Lazy.force coq_jmeq_eq);
+  inv_ind = Lazy.force coq_jmeq_ind;
+  inv_congr = Lazy.force coq_jmeq_congr_canonical }
+
 (* Specif *)
 let coq_sumbool  = lazy_init_constant ["Specif"] "sumbool"
 
@@ -284,6 +308,7 @@ let coq_identity_rect = lazy_init_constant ["Datatypes"] "identity_rect"
 let coq_identity_congr = lazy_init_constant ["Logic_Type"] "identity_congr"
 let coq_identity_sym = lazy_init_constant ["Logic_Type"] "identity_sym"
 let coq_identity_trans = lazy_init_constant ["Logic_Type"] "identity_trans"
+let coq_identity_congr_canonical = lazy_init_constant ["Logic_Type"] "identity_congr_canonical_form"
 
 let build_coq_identity_data () =
   let _ = check_required_library datatypes_module_name in {
@@ -294,6 +319,25 @@ let build_coq_identity_data () =
   trans = Lazy.force coq_identity_trans;
   congr = Lazy.force coq_identity_congr }
 
+let build_coq_inversion_identity_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_type_module_name in {
+  inv_eq = Lazy.force coq_identity_eq;
+  inv_ind = Lazy.force coq_identity_ind;
+  inv_congr = Lazy.force coq_identity_congr_canonical }
+
+(* Equality to true *)
+let coq_eq_true_eq = lazy_init_constant ["Datatypes"] "eq_true"
+let coq_eq_true_ind = lazy_init_constant ["Datatypes"] "eq_true_ind"
+let coq_eq_true_congr = lazy_init_constant ["Logic"] "eq_true_congr"
+
+let build_coq_inversion_eq_true_data () =
+  let _ = check_required_library datatypes_module_name in
+  let _ = check_required_library logic_module_name in {
+  inv_eq = Lazy.force coq_eq_true_eq;
+  inv_ind = Lazy.force coq_eq_true_ind;
+  inv_congr = Lazy.force coq_eq_true_congr }
+
 (* The False proposition *)
 let coq_False  = lazy_init_constant ["Logic"] "False"
 
@@ -332,6 +376,7 @@ let build_coq_iff_right_proj () = Lazy.force coq_iff_right_proj
 let coq_eq_ref      = lazy (init_reference ["Logic"] "eq")
 let coq_identity_ref = lazy (init_reference ["Datatypes"] "identity")
 let coq_jmeq_ref     = lazy (gen_reference "Coqlib" ["Logic";"JMeq"] "JMeq")
+let coq_eq_true_ref = lazy (gen_reference "Coqlib" ["Init";"Datatypes"] "eq_true")
 let coq_existS_ref  = lazy (anomaly "use coq_existT_ref")
 let coq_existT_ref  = lazy (init_reference ["Specif"] "existT")
 let coq_not_ref     = lazy (init_reference ["Logic"] "not")
diff --git a/interp/coqlib.mli b/interp/coqlib.mli
index 8b0384960..6bb79c8b6 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.mli
@@ -58,6 +58,9 @@ val check_required_library : string list -> unit
 val logic_module : dir_path
 val logic_type_module : dir_path
 
+val datatypes_module_name : string list
+val logic_module_name : string list
+
 (* Natural numbers *)
 val nat_path : full_path
 val glob_nat : global_reference
@@ -119,9 +122,22 @@ val build_coq_identity_data : coq_eq_data delayed
 val build_coq_jmeq_data : coq_eq_data delayed
 
 val build_coq_eq       : constr delayed (* = [(build_coq_eq_data()).eq] *)
+val build_coq_eq_refl  : constr delayed (* = [(build_coq_eq_data()).refl] *)
 val build_coq_eq_sym   : constr delayed (* = [(build_coq_eq_data()).sym] *)
 val build_coq_f_equal2 : constr delayed
 
+(* Data needed for discriminate and injection *)
+
+type coq_inversion_data = {
+  inv_eq   : constr; (* : forall params, t -> Prop *)
+  inv_ind  : constr; (* : forall params P y, eq params y -> P y *)
+  inv_congr: constr  (* : forall params B (f:t->B) y, eq params y -> f c=f y *)
+}
+
+val build_coq_inversion_eq_data : coq_inversion_data delayed
+val build_coq_inversion_identity_data : coq_inversion_data delayed
+val build_coq_inversion_jmeq_data : coq_inversion_data delayed
+val build_coq_inversion_eq_true_data : coq_inversion_data delayed
 
 (* Specif *)
 val build_coq_sumbool : constr delayed
@@ -154,6 +170,7 @@ val build_coq_ex : constr delayed
 val coq_eq_ref : global_reference lazy_t
 val coq_identity_ref : global_reference lazy_t
 val coq_jmeq_ref : global_reference lazy_t
+val coq_eq_true_ref : global_reference lazy_t
 val coq_existS_ref : global_reference lazy_t
 val coq_existT_ref : global_reference lazy_t
 val coq_not_ref : global_reference lazy_t
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 04715d51b..df48458e6 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -856,12 +856,17 @@ let occur_var_constr_expr id c = Idset.mem id (free_vars_of_constr_expr c)
 
 let mkIdentC id  = CRef (Ident (dummy_loc, id))
 let mkRefC r     = CRef r
-let mkAppC (f,l) = CApp (dummy_loc, (None,f), List.map (fun x -> (x,None)) l)
 let mkCastC (a,k)  = CCast (dummy_loc,a,k)
 let mkLambdaC (idl,bk,a,b) = CLambdaN (dummy_loc,[idl,bk,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,bk,a,b)   = CProdN (dummy_loc,[idl,bk,a],b)
 
+let mkAppC (f,l) =
+  let l = List.map (fun x -> (x,None)) l in
+  match f with
+  | CApp (_,g,l') -> CApp (dummy_loc, g, l' @ l)
+  | _ -> CApp (dummy_loc, (None, f), l)
+
 let rec mkCProdN loc bll c =
   match bll with
   | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll ->