change add path commands to get the extra argument and the Hint commands

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

3 files changed, 130 insertions, 77 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 0a579b274..e99392ccb 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -51,7 +51,7 @@ and ct_COMMAND =
   | CT_abort of ct_ID_OPT_OR_ALL
   | CT_abstraction of ct_ID * ct_FORMULA * ct_INT_LIST
   | CT_add_natural_feature of ct_NATURAL_FEATURE * ct_ID
-  | CT_addpath of ct_STRING
+  | CT_addpath of ct_STRING * ct_ID_OPT
   | CT_cd of ct_STRING_OPT
   | CT_check of ct_FORMULA
   | CT_class of ct_ID
@@ -69,7 +69,8 @@ and ct_COMMAND =
   | CT_focus of ct_INT_OPT
   | CT_go of ct_INT_OR_LOCN
   | CT_guarded
-  | CT_hint of ct_ID * ct_ID_LIST * ct_HINT_EXPRESSION
+  | CT_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
+  | CT_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
   | CT_hintrewrite of ct_ORIENTATION * ct_FORMULA_NE_LIST * ct_ID * ct_TACTIC_COM
   | CT_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
   | CT_implicits of ct_ID * ct_INT_LIST
@@ -78,6 +79,9 @@ and ct_COMMAND =
   | CT_inspect of ct_INT
   | CT_kill_node of ct_INT
   | CT_load of ct_VERBOSE_OPT * ct_ID_OR_STRING
+  | CT_local_hint_destruct of ct_ID * ct_INT * ct_DESTRUCT_LOCATION * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
+  | CT_local_hint_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM * ct_ID_LIST
+  | CT_local_hints of ct_ID * ct_ID_NE_LIST * ct_ID_LIST
   | CT_locate of ct_ID
   | CT_locate_file of ct_STRING
   | CT_locate_lib of ct_ID
@@ -114,7 +118,7 @@ and ct_COMMAND =
   | 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_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
   | CT_require of ct_IMPEXP * ct_SPEC_OPT * ct_ID * ct_STRING_OPT
@@ -210,6 +214,10 @@ and ct_DEP =
 and ct_DESTRUCTING =
     CT_coerce_NONE_to_DESTRUCTING of ct_NONE
   | CT_destructing
+and ct_DESTRUCT_LOCATION =
+    CT_conclusion_location
+  | CT_discardable_hypothesis
+  | CT_hypothesis_location
 and ct_EQN =
     CT_eqn of ct_MATCH_PATTERN_NE_LIST * ct_FORMULA
 and ct_EQN_LIST =
@@ -265,12 +273,6 @@ and ct_FORMULA_OR_INT =
   | CT_coerce_ID_OR_INT_to_FORMULA_OR_INT of ct_ID_OR_INT
 and ct_GRAMMAR =
     CT_grammar_none
-and ct_HINT_EXPRESSION =
-    CT_constructors of ct_ID_LIST
-  | CT_extern of ct_INT * ct_FORMULA * ct_TACTIC_COM
-  | CT_immediate of ct_FORMULA
-  | CT_resolve of ct_FORMULA
-  | CT_unfold_hint of ct_ID
 and ct_HYP_LOCATION =
     CT_coerce_UNFOLD_to_HYP_LOCATION of ct_UNFOLD
   | CT_intype of ct_ID * ct_INT_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 344d28bed..81df96b67 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -116,9 +116,10 @@ and fCOMMAND = function
    fNATURAL_FEATURE x1;
    fID x2;
    fNODE "add_natural_feature" 2
-| CT_addpath(x1) ->
+| CT_addpath(x1, x2) ->
    fSTRING x1;
-   fNODE "addpath" 1
+   fID_OPT x2;
+   fNODE "addpath" 2
 | CT_cd(x1) ->
    fSTRING_OPT x1;
    fNODE "cd" 1
@@ -187,11 +188,20 @@ and fCOMMAND = function
    fINT_OR_LOCN x1;
    fNODE "go" 1
 | CT_guarded -> fNODE "guarded" 0
-| CT_hint(x1, x2, x3) ->
+| CT_hint_destruct(x1, x2, x3, x4, x5, x6) ->
    fID x1;
-   fID_LIST x2;
-   fHINT_EXPRESSION x3;
-   fNODE "hint" 3
+   fINT x2;
+   fDESTRUCT_LOCATION x3;
+   fFORMULA x4;
+   fTACTIC_COM x5;
+   fID_LIST x6;
+   fNODE "hint_destruct" 6
+| CT_hint_extern(x1, x2, x3, x4) ->
+   fINT x1;
+   fFORMULA x2;
+   fTACTIC_COM x3;
+   fID_LIST x4;
+   fNODE "hint_extern" 4
 | CT_hintrewrite(x1, x2, x3, x4) ->
    fORIENTATION x1;
    fFORMULA_NE_LIST x2;
@@ -226,6 +236,25 @@ and fCOMMAND = function
    fVERBOSE_OPT x1;
    fID_OR_STRING x2;
    fNODE "load" 2
+| CT_local_hint_destruct(x1, x2, x3, x4, x5, x6) ->
+   fID x1;
+   fINT x2;
+   fDESTRUCT_LOCATION x3;
+   fFORMULA x4;
+   fTACTIC_COM x5;
+   fID_LIST x6;
+   fNODE "local_hint_destruct" 6
+| CT_local_hint_extern(x1, x2, x3, x4) ->
+   fINT x1;
+   fFORMULA x2;
+   fTACTIC_COM x3;
+   fID_LIST x4;
+   fNODE "local_hint_extern" 4
+| CT_local_hints(x1, x2, x3) ->
+   fID x1;
+   fID_NE_LIST x2;
+   fID_LIST x3;
+   fNODE "local_hints" 3
 | CT_locate(x1) ->
    fID x1;
    fNODE "locate" 1
@@ -313,9 +342,10 @@ and fCOMMAND = function
 | CT_rec_tactic_definition(x1) ->
    fREC_TACTIC_FUN_LIST x1;
    fNODE "rec_tactic_definition" 1
-| CT_recaddpath(x1) ->
+| CT_recaddpath(x1, x2) ->
    fSTRING x1;
-   fNODE "recaddpath" 1
+   fID_OPT x2;
+   fNODE "recaddpath" 2
 | CT_record(x1, x2, x3, x4, x5, x6) ->
    fCOERCION_OPT x1;
    fID x2;
@@ -537,6 +567,10 @@ and fDEP = function
    print_string "\n"and fDESTRUCTING = function
 | CT_coerce_NONE_to_DESTRUCTING x -> fNONE x
 | CT_destructing -> fNODE "destructing" 0
+and fDESTRUCT_LOCATION = function
+| CT_conclusion_location -> fNODE "conclusion_location" 0
+| CT_discardable_hypothesis -> fNODE "discardable_hypothesis" 0
+| CT_hypothesis_location -> fNODE "hypothesis_location" 0
 and fEQN = function
 | CT_eqn(x1, x2) ->
    fMATCH_PATTERN_NE_LIST x1;
@@ -690,24 +724,6 @@ and fFORMULA_OR_INT = function
 | CT_coerce_ID_OR_INT_to_FORMULA_OR_INT x -> fID_OR_INT x
 and fGRAMMAR = function
 | CT_grammar_none -> fNODE "grammar_none" 0
-and fHINT_EXPRESSION = function
-| CT_constructors(x1) ->
-   fID_LIST x1;
-   fNODE "constructors" 1
-| CT_extern(x1, x2, x3) ->
-   fINT x1;
-   fFORMULA x2;
-   fTACTIC_COM x3;
-   fNODE "extern" 3
-| CT_immediate(x1) ->
-   fFORMULA x1;
-   fNODE "immediate" 1
-| CT_resolve(x1) ->
-   fFORMULA x1;
-   fNODE "resolve" 1
-| CT_unfold_hint(x1) ->
-   fID x1;
-   fNODE "unfold_hint" 1
 and fHYP_LOCATION = function
 | CT_coerce_UNFOLD_to_HYP_LOCATION x -> fUNFOLD x
 | CT_intype(x1, x2) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index be3d27d2d..0ca53aa17 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -237,6 +237,7 @@ let xlate_sort =
     | RType None -> CT_sortc "Type"
     | RType (Some u) -> xlate_error "xlate_sort";;
 
+
 let xlate_qualid a =
   let d,i = Libnames.repr_qualid a in
   let l = Names.repr_dirpath d in
@@ -1186,9 +1187,9 @@ and coerce_genarg_to_TARG x =
       	(CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula
 						 (out_gen
 						    rawwit_casted_open_constr x)))
-  | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
-  | BindingsArgType -> xlate_error "TODO: with bindings"
-  | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
+  | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
+  | BindingsArgType -> xlate_error "TODO: generic with bindings"
+  | RedExprArgType -> xlate_error "TODO: generic red expr"
   | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
   | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
   | OptArgType x -> xlate_error "TODO: optional generic arguments"
@@ -1271,9 +1272,9 @@ let coerce_genarg_to_VARG x =
   | TacticArgType ->
       let t = xlate_tactic (out_gen rawwit_tactic x) in
       CT_coerce_TACTIC_OPT_to_VARG (CT_coerce_TACTIC_COM_to_TACTIC_OPT t)
-  | CastedOpenConstrArgType -> xlate_error "TODO: open constr"
-  | ConstrWithBindingsArgType -> xlate_error "TODO: constr with bindings"
-  | BindingsArgType -> xlate_error "TODO: with bindings"
+  | CastedOpenConstrArgType -> xlate_error "TODO: generic open constr"
+  | ConstrWithBindingsArgType -> xlate_error "TODO: generic constr with bindings"
+  | BindingsArgType -> xlate_error "TODO: generic with bindings"
   | RedExprArgType -> xlate_error "TODO: red expr as generic argument"
   | List0ArgType l -> xlate_error "TODO: lists of generic arguments"
   | List1ArgType l -> xlate_error "TODO: non empty lists of generic arguments"
@@ -1433,13 +1434,19 @@ let xlate_vernac =
        (CT_eval (xlate_int_opt numopt, red, xlate_formula f))
     | VernacChdir (Some str) -> CT_cd (ctf_STRING_OPT_SOME (CT_string str))
     | VernacChdir None -> CT_cd ctf_STRING_OPT_NONE
-    | VernacAddLoadPath (false,str,None) -> CT_addpath (CT_string str)
-    | VernacAddLoadPath (true,str,None) -> CT_recaddpath (CT_string str)
-    | VernacAddLoadPath (_,str,Some x) ->
-	xlate_error"TODO: Add (Rec) LoadPath as"
+    | VernacAddLoadPath (false,str,None) ->
+ 	CT_addpath (CT_string str, ctv_ID_OPT_NONE)
+    | VernacAddLoadPath (false,str,Some x) ->
+ 	CT_addpath (CT_string str,
+		    CT_coerce_ID_to_ID_OPT (CT_ident (string_of_dirpath x)))
+    | VernacAddLoadPath (true,str,None) ->
+ 	CT_recaddpath (CT_string str, ctv_ID_OPT_NONE)
+    | VernacAddLoadPath (_,str, Some x) ->
+	CT_recaddpath (CT_string str,
+		       CT_coerce_ID_to_ID_OPT (CT_ident (string_of_dirpath x)))
     | VernacRemoveLoadPath str -> CT_delpath (CT_string str)
     | VernacToplevelControl Quit -> CT_quit
-    | VernacToplevelControl _ -> xlate_error "TODO?: Drop/ProtectedToplevel"
+    | VernacToplevelControl _ -> xlate_error "Drop/ProtectedToplevel not supported"
       (*ML commands *)
     | VernacAddMLPath (false,str) -> CT_ml_add_path (CT_string str)
     | VernacAddMLPath (true,str) -> CT_rec_ml_add_path (CT_string str)
@@ -1476,47 +1483,75 @@ let xlate_vernac =
       (* TODO: locality flag *)
       let dblist = CT_id_list(List.map (fun x -> CT_ident x) dbnames) in
       (match h with
-	| HintsResolve [Some id_name, c] -> (* = Old HintResolve *)
-	    CT_hint(xlate_ident id_name, dblist, CT_resolve (xlate_formula c))
-	| HintsImmediate [Some id_name, c] -> (* = Old HintImmediate *)
-	    CT_hint(xlate_ident id_name, dblist, CT_immediate(xlate_formula c))
-	| HintsUnfold [Some id_name, q] -> (* = Old HintUnfold *)
-	    CT_hint(xlate_ident id_name, dblist,
-              CT_unfold_hint (loc_qualid_to_ct_ID q))
-	| HintsConstructors (Some id_name, ql) ->
-	    CT_hint(xlate_ident id_name, dblist,
-              CT_constructors (CT_id_list(List.map loc_qualid_to_ct_ID ql)))
-	| HintsExtern (Some id_name, n, c, t) ->
-	    CT_hint(xlate_ident id_name, dblist,
-              CT_extern(CT_int n, xlate_formula c, xlate_tactic t))
-        | HintsResolve l -> (* = Old HintsResolve *)
-	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
+	| HintsConstructors (None, l) ->
+	 let n1, names = match List.map tac_qualid_to_ct_ID l with
+	     n1 :: names -> n1, names
+	   | _  -> failwith "" in
+	   if local then
+	     CT_local_hints(CT_ident "Constructors",
+			    CT_id_ne_list(n1, names), dblist)
+	   else
+	     CT_hints(CT_ident "Constructors",
+		      CT_id_ne_list(n1, names), dblist)
+	| HintsExtern (None, n, c, t) ->
+	    CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist)
+        | HintsResolve l -> 
+	 let l = 
+	   List.map 
+	     (function (None,CRef r) -> r 
+		| _ -> xlate_error "obsolete Hint Resolve not supported") l in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
-         CT_hints(CT_ident "Resolve",
-                  CT_id_ne_list(n1, names),
-		  dblist)
-        | HintsImmediate l -> (* = Old HintsImmediate *)
-	 let l = List.map (function (None,CRef r) -> r | _ -> failwith "") l in
+	   if local then
+             CT_local_hints(CT_ident "Resolve",
+			    CT_id_ne_list(n1, names), dblist)
+	   else
+             CT_hints(CT_ident "Resolve", CT_id_ne_list(n1, names), dblist)
+        | HintsImmediate l -> 
+	    let l =
+	      List.map 
+		(function (None,CRef r) -> r 
+		   | _ ->
+		       xlate_error "obsolete Hint Immediate not supported") l
+	    in
 	 let n1, names = match List.map tac_qualid_to_ct_ID l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
-        CT_hints(CT_ident "Immediate", 
-                 CT_id_ne_list(n1, names),
-                 dblist)
-        | HintsUnfold l ->  (* = Old HintsUnfold *)
+	   if local then
+             CT_local_hints(CT_ident "Immediate",
+			    CT_id_ne_list(n1, names), dblist)
+	   else
+             CT_hints(CT_ident "Immediate", CT_id_ne_list(n1, names), dblist)
+        | HintsUnfold l -> 
 	 let l = List.map
-	   (function
-	       (None,ref) -> loc_qualid_to_ct_ID ref
-	     | _ -> failwith "") l in
+	   (function (None,ref) -> loc_qualid_to_ct_ID ref |
+	      _ -> xlate_error "obsolete Hint Unfold not supported") l in
 	 let n1, names = match l with
 	     n1 :: names -> n1, names
 	   | _  -> failwith "" in
-        CT_hints(CT_ident "Unfold", 
-                 CT_id_ne_list(n1, names),
-                 dblist)
-        | _ -> xlate_error"TODO: Hint")
+	   if local then
+             CT_local_hints(CT_ident "Unfold",
+			    CT_id_ne_list(n1, names), dblist)
+	   else	     
+             CT_hints(CT_ident "Unfold", CT_id_ne_list(n1, names), dblist)
+       	| HintsDestruct(id, n, loc, f, t) ->
+	    let dl = match loc with
+		ConclLocation() -> CT_conclusion_location
+	      | HypLocation true -> CT_discardable_hypothesis
+	      | HypLocation false -> CT_hypothesis_location in
+	     if local then
+               CT_local_hint_destruct
+		 (xlate_ident id, CT_int n,
+		  dl, xlate_formula f, xlate_tactic t, dblist)
+	     else
+	       CT_hint_destruct
+		 (xlate_ident id, CT_int n, dl, xlate_formula f,
+		  xlate_tactic t, dblist)
+	| HintsExtern(Some _, _, _, _)
+	| HintsConstructors(Some _, _) -> 
+            xlate_error "obsolete Hint Constructors not supported"
+)
   | VernacEndProof (Proved (true,None)) ->
       CT_save (CT_coerce_THM_to_THM_OPT (CT_thm "Theorem"), ctv_ID_OPT_NONE)
   | VernacEndProof (Proved (false,None)) ->