updates the tactics contradiction and autorewrite, the commands

set implicit arguments, hint rewrite, and proof


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

3 files changed, 127 insertions, 12 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 65708a191..5ecbc6b53 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -1,6 +1,7 @@
 type ct_AST =
     CT_coerce_ID_OR_INT_to_AST of ct_ID_OR_INT
   | CT_coerce_ID_OR_STRING_to_AST of ct_ID_OR_STRING
+  | CT_coerce_SINGLE_OPTION_VALUE_to_AST of ct_SINGLE_OPTION_VALUE
   | CT_astnode of ct_ID * ct_AST_LIST
   | CT_astpath of ct_ID_LIST
   | CT_astslam of ct_ID_OPT * ct_AST
@@ -155,6 +156,9 @@ and ct_COMMAND =
   | CT_section_struct of ct_SECTION_BEGIN * ct_SECTION_BODY * ct_COMMAND
   | CT_set_natural of ct_ID
   | CT_set_natural_default
+  | CT_set_option of ct_TABLE
+  | CT_set_option_value of ct_TABLE * ct_SINGLE_OPTION_VALUE
+  | CT_set_option_value2 of ct_TABLE * ct_ID_OR_STRING_NE_LIST
   | CT_sethyp of ct_INT
   | CT_setundo of ct_INT
   | CT_show_existentials
@@ -177,6 +181,7 @@ and ct_COMMAND =
   | CT_transparent of ct_ID_NE_LIST
   | CT_undo of ct_INT_OPT
   | CT_unfocus
+  | CT_unset_option of ct_TABLE
   | CT_unsethyp
   | CT_unsetundo
   | CT_user_vernac of ct_ID * ct_VARG_LIST
@@ -518,6 +523,9 @@ and ct_SIGNED_INT =
   | CT_minus of ct_INT
 and ct_SIGNED_INT_LIST =
     CT_signed_int_list of ct_SIGNED_INT list
+and ct_SINGLE_OPTION_VALUE =
+    CT_coerce_INT_to_SINGLE_OPTION_VALUE of ct_INT
+  | CT_coerce_STRING_to_SINGLE_OPTION_VALUE of ct_STRING
 and ct_SORT_TYPE =
     CT_sortc of string
 and ct_SPEC_LIST =
@@ -538,6 +546,9 @@ and ct_STRING_NE_LIST =
 and ct_STRING_OPT =
     CT_coerce_NONE_to_STRING_OPT of ct_NONE
   | CT_coerce_STRING_to_STRING_OPT of ct_STRING
+and ct_TABLE =
+    CT_coerce_ID_to_TABLE of ct_ID
+  | CT_table of ct_ID * ct_ID
 and ct_TACTIC_ARG =
     CT_coerce_EVAL_CMD_to_TACTIC_ARG of ct_EVAL_CMD
   | CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG of ct_FORMULA_OR_INT
@@ -569,6 +580,7 @@ and ct_TACTIC_COM =
   | CT_condrewrite_rl of ct_TACTIC_COM * ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
   | CT_constructor of ct_INT * ct_SPEC_LIST
   | CT_contradiction
+  | CT_contradiction_thm of ct_FORMULA * ct_SPEC_LIST
   | CT_cut of ct_FORMULA
   | CT_cutrewrite_lr of ct_FORMULA * ct_ID_OPT
   | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT
@@ -661,8 +673,10 @@ and ct_TARG =
   | CT_coerce_PATTERN_to_TARG of ct_PATTERN
   | CT_coerce_SCOMMENT_CONTENT_to_TARG of ct_SCOMMENT_CONTENT
   | CT_coerce_SIGNED_INT_LIST_to_TARG of ct_SIGNED_INT_LIST
+  | CT_coerce_SINGLE_OPTION_VALUE_to_TARG of ct_SINGLE_OPTION_VALUE
   | CT_coerce_SPEC_LIST_to_TARG of ct_SPEC_LIST
   | CT_coerce_TACTIC_COM_to_TARG of ct_TACTIC_COM
+  | CT_coerce_TARG_LIST_to_TARG of ct_TARG_LIST
   | CT_coerce_UNFOLD_to_TARG of ct_UNFOLD
   | CT_coerce_UNFOLD_NE_LIST_to_TARG of ct_UNFOLD_NE_LIST
 and ct_TARG_LIST =
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 037e48fe2..5c9ab48c3 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -17,6 +17,7 @@ let f_atom_int = print_int;;
 let rec fAST = function
 | CT_coerce_ID_OR_INT_to_AST x -> fID_OR_INT x
 | CT_coerce_ID_OR_STRING_to_AST x -> fID_OR_STRING x
+| CT_coerce_SINGLE_OPTION_VALUE_to_AST x -> fSINGLE_OPTION_VALUE x
 | CT_astnode(x1, x2) ->
    fID x1;
    fAST_LIST x2;
@@ -485,6 +486,17 @@ and fCOMMAND = function
    fID x1;
    fNODE "set_natural" 1
 | CT_set_natural_default -> fNODE "set_natural_default" 0
+| CT_set_option(x1) ->
+   fTABLE x1;
+   fNODE "set_option" 1
+| CT_set_option_value(x1, x2) ->
+   fTABLE x1;
+   fSINGLE_OPTION_VALUE x2;
+   fNODE "set_option_value" 2
+| CT_set_option_value2(x1, x2) ->
+   fTABLE x1;
+   fID_OR_STRING_NE_LIST x2;
+   fNODE "set_option_value2" 2
 | CT_sethyp(x1) ->
    fINT x1;
    fNODE "sethyp" 1
@@ -538,6 +550,9 @@ and fCOMMAND = function
    fINT_OPT x1;
    fNODE "undo" 1
 | CT_unfocus -> fNODE "unfocus" 0
+| CT_unset_option(x1) ->
+   fTABLE x1;
+   fNODE "unset_option" 1
 | CT_unsethyp -> fNODE "unsethyp" 0
 | CT_unsetundo -> fNODE "unsetundo" 0
 | CT_user_vernac(x1, x2) ->
@@ -1222,6 +1237,9 @@ and fSIGNED_INT_LIST = function
 | CT_signed_int_list l ->
    (List.iter fSIGNED_INT l);
    fNODE "signed_int_list" (List.length l)
+and fSINGLE_OPTION_VALUE = function
+| CT_coerce_INT_to_SINGLE_OPTION_VALUE x -> fINT x
+| CT_coerce_STRING_to_SINGLE_OPTION_VALUE x -> fSTRING x
 and fSORT_TYPE = function
 | CT_sortc x -> fATOM "sortc";
    (f_atom_string x);
@@ -1247,6 +1265,12 @@ and fSTRING = function
 and fSTRING_OPT = function
 | CT_coerce_NONE_to_STRING_OPT x -> fNONE x
 | CT_coerce_STRING_to_STRING_OPT x -> fSTRING x
+and fTABLE = function
+| CT_coerce_ID_to_TABLE x -> fID x
+| CT_table(x1, x2) ->
+   fID x1;
+   fID x2;
+   fNODE "table" 2
 and fTACTIC_ARG = function
 | CT_coerce_EVAL_CMD_to_TACTIC_ARG x -> fEVAL_CMD x
 | CT_coerce_FORMULA_OR_INT_to_TACTIC_ARG x -> fFORMULA_OR_INT x
@@ -1338,6 +1362,10 @@ and fTACTIC_COM = function
    fSPEC_LIST x2;
    fNODE "constructor" 2
 | CT_contradiction -> fNODE "contradiction" 0
+| CT_contradiction_thm(x1, x2) ->
+   fFORMULA x1;
+   fSPEC_LIST x2;
+   fNODE "contradiction_thm" 2
 | CT_cut(x1) ->
    fFORMULA x1;
    fNODE "cut" 1
@@ -1645,8 +1673,10 @@ and fTARG = function
 | CT_coerce_PATTERN_to_TARG x -> fPATTERN x
 | CT_coerce_SCOMMENT_CONTENT_to_TARG x -> fSCOMMENT_CONTENT x
 | CT_coerce_SIGNED_INT_LIST_to_TARG x -> fSIGNED_INT_LIST x
+| CT_coerce_SINGLE_OPTION_VALUE_to_TARG x -> fSINGLE_OPTION_VALUE x
 | CT_coerce_SPEC_LIST_to_TARG x -> fSPEC_LIST x
 | CT_coerce_TACTIC_COM_to_TARG x -> fTACTIC_COM x
+| CT_coerce_TARG_LIST_to_TARG x -> fTARG_LIST x
 | CT_coerce_UNFOLD_to_TARG x -> fUNFOLD x
 | CT_coerce_UNFOLD_NE_LIST_to_TARG x -> fUNFOLD_NE_LIST x
 and fTARG_LIST = function
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7837e8299..0e6fc2998 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -13,6 +13,7 @@ open Vernacexpr;;
 open Decl_kinds;;
 open Topconstr;;
 open Libnames;;
+open Goptions;;
 
 
 let in_coq_ref = ref false;;
@@ -287,6 +288,11 @@ let xlate_id_opt_ne_list = function
   | a::l -> CT_id_opt_ne_list(xlate_id_opt a, List.map xlate_id_opt l);;
 
 
+let rec last = function
+    [] -> assert false
+  | [a] -> a
+  | a::tl -> last tl;;
+
 let rec decompose_last = function
     [] -> assert false
   | [a] -> [], a
@@ -878,8 +884,15 @@ and xlate_tac =
     | TacExtend (_, "refine", [c]) ->
        CT_refine
 	 (xlate_formula (out_gen rawwit_casted_open_constr c))
-    | TacExtend (_,"Absurd",[c]) ->
+    | TacExtend (_,"absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
+    | TacExtend (_,"contradiction",[opt_c]) ->
+	(match out_gen (wit_opt rawwit_constr_with_bindings) opt_c with
+	     None -> CT_contradiction
+	   | Some(c, b) ->
+	       let c1 = xlate_formula c in
+	       let bindings = xlate_bindings b in
+		 CT_contradiction_thm(c1, bindings))
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
     | TacChange (Some(l,c), f, b) -> 
 	(* TODO LATER: combine with other constructions of pattern_occ *)
@@ -1009,6 +1022,19 @@ and xlate_tac =
 	CT_auto_with(xlate_int_opt nopt,
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
+    |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) ->
+       let (id_list:ct_ID list) =
+	 List.map (fun x -> CT_ident x) (out_gen (wit_list1 rawwit_pre_ident) l) in
+       let fst, (id_list1: ct_ID list) =
+	 match id_list with [] -> assert false | a::tl -> a,tl in
+       let t1 =
+	 match t with
+	     [t0] -> 
+	       CT_coerce_TACTIC_COM_to_TACTIC_OPT
+		 (xlate_tactic(out_gen rawwit_tactic t0))
+	   | [] -> CT_coerce_NONE_to_TACTIC_OPT CT_none
+	   | _ -> assert false in
+	 CT_autorewrite (CT_id_ne_list(fst, id_list1), t1)
     | TacExtend (_,"eauto", [nopt; popt; idl]) ->
 	let first_n =
 	  match out_gen (wit_opt rawwit_int_or_var) nopt with
@@ -1507,14 +1533,18 @@ let rec xlate_vernac =
     | VernacSolve (n, tac, b) -> CT_solve (CT_int n, xlate_tactic tac)
     | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
     | VernacUnfocus -> CT_unfocus
-  | VernacExtend ("HintRewrite", orient :: formula_list :: base :: t) ->
-      let orient = out_gen Extraargs.rawwit_orient orient in
-      let formula_list = out_gen (wit_list1 (rawwit_constr)) formula_list in
-      let base = out_gen rawwit_pre_ident base in
-      let t = match t with
-	| [] -> TacId ""
-	| [t] -> out_gen rawwit_tactic t
-	| _ -> failwith "" in
+  | VernacExtend (("HintRewriteV7"|"HintRewriteV8") as key, largs) ->
+      let in_v8 = (key = "HintRewriteV8") in
+      let orient = out_gen Extraargs.rawwit_orient (List.nth largs 0) in
+      let formula_list = out_gen (wit_list1 rawwit_constr) (List.nth largs 1) in
+      let t =
+	if List.length largs = 4 then
+	   out_gen rawwit_tactic (List.nth largs (if in_v8 then 2 else 3))
+	 else
+	   TacId "" in
+      let base = 
+	out_gen rawwit_pre_ident
+	  (if in_v8 then last largs else List.nth largs 2) in
       let ct_orient = match orient with
 	| true  -> CT_lr
 	| false -> CT_rl in
@@ -1893,12 +1923,53 @@ let rec xlate_vernac =
   | VernacLocate(LocateNotation s) -> CT_locate_notation(CT_string s)
   | VernacTime(v) -> CT_time(xlate_vernac v)
   | VernacSetOption (Goptions.SecondaryTable ("Implicit", "Arguments"), BoolValue true)->CT_user_vernac (CT_ident "IMPLICIT_ARGS_ON", CT_varg_list[])
+  |VernacExactProof f -> CT_proof(xlate_formula f)
+  | VernacSetOption (table, BoolValue true) -> 
+      let table1 = 
+	match table with
+	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	CT_set_option(table1)
+  | VernacSetOption (table, v) -> 
+      let table1 = 
+	match table with
+	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+      let value =
+	match v with
+	  | BoolValue _ -> assert false
+	  | StringValue s ->
+	      CT_coerce_STRING_to_SINGLE_OPTION_VALUE(CT_string s)
+	  | IntValue n ->
+	      CT_coerce_INT_to_SINGLE_OPTION_VALUE(CT_int n) in
+	CT_set_option_value(table1, value)
+  | VernacUnsetOption(table) ->
+      let table1 = 
+	match table with
+	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	CT_unset_option(table1)
+  | VernacAddOption (table, l) ->
+      let values =
+	List.map
+	  (function
+	     | QualidRefValue x -> 
+		 CT_coerce_ID_to_ID_OR_STRING(loc_qualid_to_ct_ID x)
+	     | StringRefValue x -> 
+		 CT_coerce_STRING_to_ID_OR_STRING(CT_string x)) l in
+      let fst, values1 = 
+	match values with [] -> assert false | a::b -> (a,b) in
+      let table1 = 
+	match table with
+	    PrimaryTable(s) -> CT_coerce_ID_to_TABLE(CT_ident s)
+	  | SecondaryTable(s1,s2) -> CT_table(CT_ident s1, CT_ident s2) in
+	CT_set_option_value2(table1, CT_id_or_string_ne_list(fst, values1))
   | (VernacGlobalCheck _|VernacPrintOption _|
-     VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
-     VernacSetOption (_, _)|VernacUnsetOption _|
+     VernacMemOption (_, _)|VernacRemoveOption (_, _)
+  |
      VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
-     VernacImport (_, _)|VernacExactProof _|VernacDistfix _|
+     VernacImport (_, _)|VernacDistfix _|
      VernacTacticGrammar _|VernacVar _|VernacProof _)
     -> xlate_error "TODO: vernac"