updates the definition of tactics using Ltac and adds the subst tactic

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

3 files changed, 133 insertions, 73 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 5ecbc6b53..7531d80b3 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -57,6 +57,7 @@ and ct_COMMAND =
   | CT_coercion of ct_LOCAL_OPT * ct_IDENTITY_OPT * ct_ID * ct_ID * ct_ID
   | CT_cofix_decl of ct_COFIX_REC_LIST
   | CT_compile_module of ct_VERBOSE_OPT * ct_ID * ct_STRING_OPT
+  | CT_declare_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
   | CT_define_notation of ct_STRING * ct_FORMULA * ct_MODIFIER_LIST * ct_ID_OPT
   | CT_definition of ct_DEFN * ct_ID * ct_BINDER_LIST * ct_DEF_BODY * ct_FORMULA_OPT
   | CT_delim_scope of ct_ID * ct_ID
@@ -67,6 +68,8 @@ and ct_COMMAND =
   | CT_explain_proof of ct_INT_LIST
   | CT_explain_prooftree of ct_INT_LIST
   | CT_export_id of ct_ID_NE_LIST
+  | CT_extract_to_file of ct_STRING * ct_ID_NE_LIST
+  | CT_extraction of ct_ID_OPT
   | CT_fix_decl of ct_FIX_REC_LIST
   | CT_focus of ct_INT_OPT
   | CT_go of ct_INT_OR_LOCN
@@ -98,7 +101,8 @@ and ct_COMMAND =
   | CT_ml_declare_modules of ct_STRING_NE_LIST
   | CT_ml_print_modules
   | CT_ml_print_path
-  | CT_module of ct_ID
+  | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR
+  | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT
   | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE
   | CT_opaque of ct_ID_NE_LIST
   | CT_open_scope of ct_ID
@@ -135,7 +139,6 @@ and ct_COMMAND =
   | CT_quit
   | CT_read_module of ct_ID
   | CT_rec_ml_add_path of ct_STRING
-  | CT_rec_tactic_definition of ct_REC_TACTIC_FUN_LIST
   | CT_recaddpath of ct_STRING * ct_ID_OPT
   | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_ID_OPT * ct_RECCONSTR_LIST
   | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID
@@ -174,7 +177,7 @@ and ct_COMMAND =
   | CT_solve of ct_INT * ct_TACTIC_COM
   | CT_suspend
   | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
-  | CT_tactic_definition of ct_ID * ct_ID_UNIT_LIST * ct_TACTIC_COM
+  | CT_tactic_definition of ct_TAC_DEF_NE_LIST
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
   | CT_time of ct_COMMAND
@@ -351,13 +354,6 @@ and ct_ID_OR_STRING =
   | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING
 and ct_ID_OR_STRING_NE_LIST =
     CT_id_or_string_ne_list of ct_ID_OR_STRING * ct_ID_OR_STRING list
-and ct_ID_UNIT =
-    CT_coerce_ID_to_ID_UNIT of ct_ID
-  | CT_unit
-and ct_ID_UNIT_LIST =
-    CT_id_unit_list of ct_ID_UNIT list
-and ct_ID_UNIT_NE_LIST =
-    CT_id_unit_ne_list of ct_ID_UNIT * ct_ID_UNIT list
 and ct_IMPEXP =
     CT_coerce_NONE_to_IMPEXP of ct_NONE
   | CT_export
@@ -442,6 +438,23 @@ and ct_MODIFIER =
   | CT_set_level of ct_INT
 and ct_MODIFIER_LIST =
     CT_modifier_list of ct_MODIFIER list
+and ct_MODULE_BINDER =
+    CT_module_binder of ct_ID_NE_LIST * ct_MODULE_TYPE
+and ct_MODULE_BINDER_LIST =
+    CT_module_binder_list of ct_MODULE_BINDER list
+and ct_MODULE_EXPR =
+    CT_coerce_ID_OPT_to_MODULE_EXPR of ct_ID_OPT
+  | CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
+and ct_MODULE_TYPE =
+    CT_coerce_ID_to_MODULE_TYPE of ct_ID
+  | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA
+  | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID
+and ct_MODULE_TYPE_CHECK =
+    CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
+  | CT_only_check of ct_MODULE_TYPE
+and ct_MODULE_TYPE_OPT =
+    CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT
+  | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE
 and ct_NATURAL_FEATURE =
     CT_contractible
   | CT_implicit
@@ -489,7 +502,7 @@ and ct_RECCONSTR =
 and ct_RECCONSTR_LIST =
     CT_recconstr_list of ct_RECCONSTR list
 and ct_REC_TACTIC_FUN =
-    CT_rec_tactic_fun of ct_ID * ct_ID_UNIT_NE_LIST * ct_TACTIC_COM
+    CT_rec_tactic_fun of ct_ID * ct_ID_OPT_NE_LIST * ct_TACTIC_COM
 and ct_REC_TACTIC_FUN_LIST =
     CT_rec_tactic_fun_list of ct_REC_TACTIC_FUN * ct_REC_TACTIC_FUN list
 and ct_RED_COM =
@@ -648,11 +661,12 @@ and ct_TACTIC_COM =
   | CT_simplify_eq of ct_ID_OPT
   | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST
   | CT_split of ct_SPEC_LIST
+  | CT_subst of ct_ID_LIST
   | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB
   | CT_symmetry of ct_CLAUSE
   | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
   | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_tactic_fun of ct_ID_UNIT_NE_LIST * ct_TACTIC_COM
+  | CT_tactic_fun of ct_ID_OPT_NE_LIST * ct_TACTIC_COM
   | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_transitivity of ct_FORMULA
   | CT_trivial
@@ -665,6 +679,10 @@ and ct_TACTIC_COM =
 and ct_TACTIC_OPT =
     CT_coerce_NONE_to_TACTIC_OPT of ct_NONE
   | CT_coerce_TACTIC_COM_to_TACTIC_OPT of ct_TACTIC_COM
+and ct_TAC_DEF =
+    CT_tac_def of ct_ID * ct_TACTIC_COM
+and ct_TAC_DEF_NE_LIST =
+    CT_tac_def_ne_list of ct_TAC_DEF * ct_TAC_DEF list
 and ct_TARG =
     CT_coerce_BINDING_to_TARG of ct_BINDING
   | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 5c9ab48c3..a6fad0769 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -154,6 +154,12 @@ and fCOMMAND = function
    fID x2;
    fSTRING_OPT x3;
    fNODE "compile_module" 3
+| CT_declare_module(x1, x2, x3, x4) ->
+   fID x1;
+   fMODULE_BINDER_LIST x2;
+   fMODULE_TYPE_CHECK x3;
+   fMODULE_EXPR x4;
+   fNODE "declare_module" 4
 | CT_define_notation(x1, x2, x3, x4) ->
    fSTRING x1;
    fFORMULA x2;
@@ -201,6 +207,13 @@ and fCOMMAND = function
 | CT_export_id(x1) ->
    fID_NE_LIST x1;
    fNODE "export_id" 1
+| CT_extract_to_file(x1, x2) ->
+   fSTRING x1;
+   fID_NE_LIST x2;
+   fNODE "extract_to_file" 2
+| CT_extraction(x1) ->
+   fID_OPT x1;
+   fNODE "extraction" 1
 | CT_fix_decl(x1) ->
    fFIX_REC_LIST x1;
    fNODE "fix_decl" 1
@@ -323,9 +336,17 @@ and fCOMMAND = function
    fNODE "ml_declare_modules" 1
 | CT_ml_print_modules -> fNODE "ml_print_modules" 0
 | CT_ml_print_path -> fNODE "ml_print_path" 0
-| CT_module(x1) ->
+| CT_module(x1, x2, x3, x4) ->
+   fID x1;
+   fMODULE_BINDER_LIST x2;
+   fMODULE_TYPE_CHECK x3;
+   fMODULE_EXPR x4;
+   fNODE "module" 4
+| CT_module_type_decl(x1, x2, x3) ->
    fID x1;
-   fNODE "module" 1
+   fMODULE_BINDER_LIST x2;
+   fMODULE_TYPE_OPT x3;
+   fNODE "module_type_decl" 3
 | CT_omega_flag(x1, x2) ->
    fOMEGA_MODE x1;
    fOMEGA_FEATURE x2;
@@ -410,9 +431,6 @@ and fCOMMAND = function
 | CT_rec_ml_add_path(x1) ->
    fSTRING x1;
    fNODE "rec_ml_add_path" 1
-| CT_rec_tactic_definition(x1) ->
-   fREC_TACTIC_FUN_LIST x1;
-   fNODE "rec_tactic_definition" 1
 | CT_recaddpath(x1, x2) ->
    fSTRING x1;
    fID_OPT x2;
@@ -527,11 +545,9 @@ and fCOMMAND = function
    fFORMULA x2;
    fINT_OPT x3;
    fNODE "syntax_macro" 3
-| CT_tactic_definition(x1, x2, x3) ->
-   fID x1;
-   fID_UNIT_LIST x2;
-   fTACTIC_COM x3;
-   fNODE "tactic_definition" 3
+| CT_tactic_definition(x1) ->
+   fTAC_DEF_NE_LIST x1;
+   fNODE "tactic_definition" 1
 | CT_test_natural_feature(x1, x2) ->
    fNATURAL_FEATURE x1;
    fID x2;
@@ -899,18 +915,6 @@ and fID_OR_STRING_NE_LIST = function
    fID_OR_STRING x;
    (List.iter fID_OR_STRING l);
    fNODE "id_or_string_ne_list" (1 + (List.length l))
-and fID_UNIT = function
-| CT_coerce_ID_to_ID_UNIT x -> fID x
-| CT_unit -> fNODE "unit" 0
-and fID_UNIT_LIST = function
-| CT_id_unit_list l ->
-   (List.iter fID_UNIT l);
-   fNODE "id_unit_list" (List.length l)
-and fID_UNIT_NE_LIST = function
-| CT_id_unit_ne_list(x,l) ->
-   fID_UNIT x;
-   (List.iter fID_UNIT l);
-   fNODE "id_unit_ne_list" (1 + (List.length l))
 and fIMPEXP = function
 | CT_coerce_NONE_to_IMPEXP x -> fNONE x
 | CT_export -> fNODE "export" 0
@@ -1074,6 +1078,41 @@ and fMODIFIER_LIST = function
 | CT_modifier_list l ->
    (List.iter fMODIFIER l);
    fNODE "modifier_list" (List.length l)
+and fMODULE_BINDER = function
+| CT_module_binder(x1, x2) ->
+   fID_NE_LIST x1;
+   fMODULE_TYPE x2;
+   fNODE "module_binder" 2
+and fMODULE_BINDER_LIST = function
+| CT_module_binder_list l ->
+   (List.iter fMODULE_BINDER l);
+   fNODE "module_binder_list" (List.length l)
+and fMODULE_EXPR = function
+| CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x
+| CT_module_app(x1, x2) ->
+   fMODULE_EXPR x1;
+   fMODULE_EXPR x2;
+   fNODE "module_app" 2
+and fMODULE_TYPE = function
+| CT_coerce_ID_to_MODULE_TYPE x -> fID x
+| CT_module_type_with_def(x1, x2, x3) ->
+   fMODULE_TYPE x1;
+   fID x2;
+   fFORMULA x3;
+   fNODE "module_type_with_def" 3
+| CT_module_type_with_mod(x1, x2, x3) ->
+   fMODULE_TYPE x1;
+   fID x2;
+   fID x3;
+   fNODE "module_type_with_mod" 3
+and fMODULE_TYPE_CHECK = function
+| CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x
+| CT_only_check(x1) ->
+   fMODULE_TYPE x1;
+   fNODE "only_check" 1
+and fMODULE_TYPE_OPT = function
+| CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x
+| CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x
 and fNATURAL_FEATURE = function
 | CT_contractible -> fNODE "contractible" 0
 | CT_implicit -> fNODE "implicit" 0
@@ -1161,7 +1200,7 @@ and fRECCONSTR_LIST = function
 and fREC_TACTIC_FUN = function
 | CT_rec_tactic_fun(x1, x2, x3) ->
    fID x1;
-   fID_UNIT_NE_LIST x2;
+   fID_OPT_NE_LIST x2;
    fTACTIC_COM x3;
    fNODE "rec_tactic_fun" 3
 and fREC_TACTIC_FUN_LIST = function
@@ -1611,6 +1650,9 @@ and fTACTIC_COM = function
 | CT_split(x1) ->
    fSPEC_LIST x1;
    fNODE "split" 1
+| CT_subst(x1) ->
+   fID_LIST x1;
+   fNODE "subst" 1
 | CT_superauto(x1, x2, x3, x4) ->
    fINT_OPT x1;
    fID_LIST x2;
@@ -1629,7 +1671,7 @@ and fTACTIC_COM = function
    (List.iter fTACTIC_COM l);
    fNODE "tacsolve" (1 + (List.length l))
 | CT_tactic_fun(x1, x2) ->
-   fID_UNIT_NE_LIST x1;
+   fID_OPT_NE_LIST x1;
    fTACTIC_COM x2;
    fNODE "tactic_fun" 2
 | CT_then(x,l) ->
@@ -1665,6 +1707,16 @@ and fTACTIC_COM = function
 and fTACTIC_OPT = function
 | CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x
 | CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x
+and fTAC_DEF = function
+| CT_tac_def(x1, x2) ->
+   fID x1;
+   fTACTIC_COM x2;
+   fNODE "tac_def" 2
+and fTAC_DEF_NE_LIST = function
+| CT_tac_def_ne_list(x,l) ->
+   fTAC_DEF x;
+   (List.iter fTAC_DEF l);
+   fNODE "tac_def_ne_list" (1 + (List.length l))
 and fTARG = function
 | CT_coerce_BINDING_to_TARG x -> fBINDING x
 | CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 97410ceb5..a6fd97833 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -174,10 +174,6 @@ let coerce_VARG_to_ID =
      x
     | _ -> xlate_error "coerce_VARG_to_ID";;
 
-let xlate_id_unit = function
-    None -> CT_unit
-  | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);;
-
 let xlate_ident_opt =
   function
     | None -> ctv_ID_OPT_NONE
@@ -639,8 +635,12 @@ let xlate_context_pattern = function
 let xlate_match_context_hyps = function
   | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b);;
 
-let xlate_largs_to_id_unit largs =
-  match List.map xlate_id_unit largs with
+let xlate_arg_to_id_opt = function
+    Some id -> CT_coerce_ID_to_ID_OPT(CT_ident (string_of_id id))
+  | None -> ctv_ID_OPT_NONE;;
+
+let xlate_largs_to_id_opt largs =
+  match List.map xlate_arg_to_id_opt largs with
       fst::rest -> fst, rest
     | _ -> assert false;;
 
@@ -765,31 +765,20 @@ and xlate_red_tactic =
       | [] -> error "Expecting at least one pattern in a Pattern command")
   | ExtraRedExpr _ -> xlate_error "TODO LATER: ExtraRedExpr (probably dead code)"
 
-and xlate_rec_tac = function
-  | ((_,x),TacFun (argl,tac)) ->
-      let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
-	CT_rec_tactic_fun(xlate_ident x,
-			  CT_id_unit_ne_list(fst, rest),
-			  xlate_tactic tac)
-  | ((_,x),tac) ->
-      CT_rec_tactic_fun(xlate_ident x,
-			CT_id_unit_ne_list (xlate_id_unit (Some x), []),
-			xlate_tactic tac)
-
 and xlate_local_rec_tac = function 
  (* TODO LATER: local recursive tactics and global ones should be handled in
     the same manner *)
   | ((_,x),(argl,tac)) ->
-      let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
+      let fst, rest = xlate_largs_to_id_opt argl in
 	CT_rec_tactic_fun(xlate_ident x,
-			  CT_id_unit_ne_list(fst, rest),
+			  CT_id_opt_ne_list(fst, rest),
 			  xlate_tactic tac)
 
 and xlate_tactic =
  function
    | TacFun (largs, t) ->
-       let fst, rest =  xlate_largs_to_id_unit largs in
-       CT_tactic_fun (CT_id_unit_ne_list(fst, rest), xlate_tactic t)
+       let fst, rest =  xlate_largs_to_id_opt largs in
+       CT_tactic_fun (CT_id_opt_ne_list(fst, rest), xlate_tactic t)
    | TacThen (t1,t2) -> 
        (match xlate_tactic t1 with
             CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
@@ -999,6 +988,11 @@ and xlate_tac =
       let id = xlate_ident (out_gen rawwit_ident id) in
       if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
       else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id)
+    | TacExtend(_, "subst", [l]) ->
+	CT_subst
+	  (CT_id_list
+	     (List.map (fun x -> CT_ident (string_of_id x))
+		(out_gen (wit_list1 rawwit_ident) l)))
     | TacReflexivity -> CT_reflexivity
     | TacSymmetry cls -> CT_symmetry(xlate_clause cls)
     | TacTransitivity c -> CT_transitivity (xlate_formula c)
@@ -1515,22 +1509,18 @@ let rec xlate_module_expr = function
 
 let rec xlate_vernac =
  function
-   | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) ->
-       let fst, rest = xlate_largs_to_id_unit largs in
-       CT_tactic_definition(xlate_ident id,
-			    CT_id_unit_list (fst::rest),
-			    xlate_tactic tac)
-   | VernacDeclareTacticDefinition 
-       (true,((id,TacFun (largs,tac))::_ as the_list)) ->
-       let x_rec_tacs =
-	 List.map xlate_rec_tac the_list in
-       let fst, others = match x_rec_tacs with
-	   fst::others -> fst, others
-	 | _ -> assert false in
-       CT_rec_tactic_definition(CT_rec_tactic_fun_list(fst, others))
-    | VernacDeclareTacticDefinition (false,[(_,id),tac]) ->
-       CT_tactic_definition(xlate_ident id, CT_id_unit_list[], xlate_tactic tac)
-    | VernacDeclareTacticDefinition (loc,_) -> xlate_error "Shouldn't occur"
+   | VernacDeclareTacticDefinition (true, tacs) ->
+       (match List.map 
+	 (function
+	      ((_, id), body) ->
+		CT_tac_def(CT_ident (string_of_id id), xlate_tactic body))
+	 tacs with
+	     [] -> assert false
+	   | fst::tacs1 ->
+	       CT_tactic_definition
+		 (CT_tac_def_ne_list(fst, tacs1)))
+   | VernacDeclareTacticDefinition(false, _) -> 
+       xlate_error "obsolete tactic definition not handled"
     | VernacLoad (verbose,s) ->
       CT_load (
        (match verbose with