Ajoute le bon traitement pour Ring, Locate, Comments

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

3 files changed, 92 insertions, 20 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index fb9d6476b..a5f620afd 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -14,7 +14,8 @@ and ct_AST_LIST =
 and ct_BINARY =
     CT_binary of int
 and ct_BINDER =
-    CT_binder of ct_ID_OPT_NE_LIST * ct_FORMULA
+    CT_coerce_DEF_to_BINDER of ct_DEF
+  | CT_binder of ct_ID_OPT_NE_LIST * ct_FORMULA
 and ct_BINDER_LIST =
     CT_binder_list of ct_BINDER list
 and ct_BINDER_NE_LIST =
@@ -69,11 +70,15 @@ and ct_COMMAND =
   | CT_hint of ct_ID * ct_ID_LIST * ct_HINT_EXPRESSION
   | 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
   | CT_ind_scheme of ct_SCHEME_SPEC_LIST
   | CT_infix of ct_ASSOC * ct_INT * ct_STRING * ct_ID
   | CT_inspect of ct_INT
   | CT_kill_node of ct_INT
   | CT_load of ct_VERBOSE_OPT * ct_ID_OR_STRING
+  | CT_locate of ct_ID
+  | CT_locate_file of ct_STRING
+  | CT_locate_lib of ct_ID
   | CT_mind_decl of ct_CO_IND * ct_IND_SPEC_LIST
   | CT_ml_add_path of ct_STRING
   | CT_ml_declare_modules of ct_STRING_NE_LIST
@@ -117,6 +122,7 @@ and ct_COMMAND =
   | CT_restore_state of ct_ID
   | CT_resume of ct_ID_OPT
   | CT_save of ct_THM_OPT * ct_ID_OPT
+  | CT_scomments of ct_SCOMMENT_CONTENT_LIST
   | CT_search of ct_ID * ct_IN_OR_OUT_MODULES
   | CT_search_pattern of ct_FORMULA * ct_IN_OR_OUT_MODULES
   | CT_search_rewrite of ct_FORMULA * ct_IN_OR_OUT_MODULES
@@ -178,6 +184,8 @@ and ct_CONV_SET =
   | CT_unfbut of ct_ID list
 and ct_CO_IND =
     CT_co_ind of string
+and ct_DEF =
+    CT_def of ct_ID_OPT * ct_FORMULA
 and ct_DEFN =
     CT_defn of string
 and ct_DEFN_OR_THM =
@@ -225,7 +233,7 @@ and ct_FORMULA =
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
   | CT_int_encapsulator of string
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_letin of ct_ID_OPT * ct_FORMULA * ct_FORMULA
+  | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
   | CT_prodc of ct_BINDER_NE_LIST * ct_FORMULA
 and ct_FORMULA_LIST =
@@ -392,6 +400,11 @@ and ct_SCHEME_SPEC =
     CT_scheme_spec of ct_ID * ct_DEP * ct_FORMULA * ct_SORT_TYPE
 and ct_SCHEME_SPEC_LIST =
     CT_scheme_spec_list of ct_SCHEME_SPEC * ct_SCHEME_SPEC list
+and ct_SCOMMENT_CONTENT =
+    CT_coerce_FORMULA_to_SCOMMENT_CONTENT of ct_FORMULA
+  | CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT of ct_ID_OR_STRING
+and ct_SCOMMENT_CONTENT_LIST =
+    CT_scomment_content_list of ct_SCOMMENT_CONTENT list
 and ct_SECTION_BEGIN =
     CT_section of ct_ID
 and ct_SECTION_BODY =
@@ -493,6 +506,7 @@ and ct_TACTIC_COM =
   | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
   | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT
   | CT_right of ct_SPEC_LIST
+  | CT_ring of ct_FORMULA_LIST
   | CT_simple_user_tac of ct_ID * ct_TACTIC_ARG_LIST
   | CT_simplify_eq of ct_ID_OPT
   | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST
@@ -517,10 +531,9 @@ and ct_TARG =
     CT_coerce_BINDING_to_TARG of ct_BINDING
   | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC
   | CT_coerce_FIXTAC_to_TARG of ct_FIXTAC
-  | CT_coerce_FORMULA_to_TARG of ct_FORMULA
   | CT_coerce_ID_OR_INT_to_TARG of ct_ID_OR_INT
-  | CT_coerce_ID_OR_STRING_to_TARG of ct_ID_OR_STRING
   | 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_SPEC_LIST_to_TARG of ct_SPEC_LIST
   | CT_coerce_TACTIC_COM_to_TARG of ct_TACTIC_COM
@@ -569,6 +582,7 @@ and ct_VARG =
   | CT_coerce_ID_OPT_OR_ALL_to_VARG of ct_ID_OPT_OR_ALL
   | CT_coerce_ID_OR_INT_OPT_to_VARG of ct_ID_OR_INT_OPT
   | CT_coerce_INT_LIST_to_VARG of ct_INT_LIST
+  | CT_coerce_SCOMMENT_CONTENT_to_VARG of ct_SCOMMENT_CONTENT
   | CT_coerce_STRING_OPT_to_VARG of ct_STRING_OPT
   | CT_coerce_TACTIC_OPT_to_VARG of ct_TACTIC_OPT
   | CT_coerce_VARG_LIST_to_VARG of ct_VARG_LIST
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index effa9aca0..24df307c3 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -41,6 +41,7 @@ and fBINARY = function
 | CT_binary x -> fATOM "binary";
    (f_atom_int x);
    print_string "\n"and fBINDER = function
+| CT_coerce_DEF_to_BINDER x -> fDEF x
 | CT_binder(x1, x2) ->
    fID_OPT_NE_LIST x1;
    fFORMULA x2;
@@ -197,6 +198,10 @@ and fCOMMAND = function
    fID_NE_LIST x2;
    fID_LIST x3;
    fNODE "hints" 3
+| CT_implicits(x1, x2) ->
+   fID x1;
+   fINT_LIST x2;
+   fNODE "implicits" 2
 | CT_ind_scheme(x1) ->
    fSCHEME_SPEC_LIST x1;
    fNODE "ind_scheme" 1
@@ -216,6 +221,15 @@ and fCOMMAND = function
    fVERBOSE_OPT x1;
    fID_OR_STRING x2;
    fNODE "load" 2
+| CT_locate(x1) ->
+   fID x1;
+   fNODE "locate" 1
+| CT_locate_file(x1) ->
+   fSTRING x1;
+   fNODE "locate_file" 1
+| CT_locate_lib(x1) ->
+   fID x1;
+   fNODE "locate_lib" 1
 | CT_mind_decl(x1, x2) ->
    fCO_IND x1;
    fIND_SPEC_LIST x2;
@@ -332,6 +346,9 @@ and fCOMMAND = function
    fTHM_OPT x1;
    fID_OPT x2;
    fNODE "save" 2
+| CT_scomments(x1) ->
+   fSCOMMENT_CONTENT_LIST x1;
+   fNODE "scomments" 1
 | CT_search(x1, x2) ->
    fID x1;
    fIN_OR_OUT_MODULES x2;
@@ -475,7 +492,12 @@ and fCONV_SET = function
 and fCO_IND = function
 | CT_co_ind x -> fATOM "co_ind";
    (f_atom_string x);
-   print_string "\n"and fDEFN = function
+   print_string "\n"and fDEF = function
+| CT_def(x1, x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "def" 2
+and fDEFN = function
 | CT_defn x -> fATOM "defn";
    (f_atom_string x);
    print_string "\n"and fDEFN_OR_THM = function
@@ -583,11 +605,10 @@ and fFORMULA = function
    fBINDER_NE_LIST x1;
    fFORMULA x2;
    fNODE "lambdac" 2
-| CT_letin(x1, x2, x3) ->
-   fID_OPT x1;
+| CT_letin(x1, x2) ->
+   fDEF x1;
    fFORMULA x2;
-   fFORMULA x3;
-   fNODE "letin" 3
+   fNODE "letin" 2
 | CT_notation(x1, x2) ->
    fSTRING x1;
    fFORMULA_LIST x2;
@@ -893,6 +914,13 @@ and fSCHEME_SPEC_LIST = function
    fSCHEME_SPEC x;
    (List.iter fSCHEME_SPEC l);
    fNODE "scheme_spec_list" (1 + (List.length l))
+and fSCOMMENT_CONTENT = function
+| CT_coerce_FORMULA_to_SCOMMENT_CONTENT x -> fFORMULA x
+| CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT x -> fID_OR_STRING x
+and fSCOMMENT_CONTENT_LIST = function
+| CT_scomment_content_list l ->
+   (List.iter fSCOMMENT_CONTENT l);
+   fNODE "scomment_content_list" (List.length l)
 and fSECTION_BEGIN = function
 | CT_section(x1) ->
    fID x1;
@@ -1182,6 +1210,9 @@ and fTACTIC_COM = function
 | CT_right(x1) ->
    fSPEC_LIST x1;
    fNODE "right" 1
+| CT_ring(x1) ->
+   fFORMULA_LIST x1;
+   fNODE "ring" 1
 | CT_simple_user_tac(x1, x2) ->
    fID x1;
    fTACTIC_ARG_LIST x2;
@@ -1249,10 +1280,9 @@ and fTARG = function
 | CT_coerce_BINDING_to_TARG x -> fBINDING x
 | CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x
 | CT_coerce_FIXTAC_to_TARG x -> fFIXTAC x
-| CT_coerce_FORMULA_to_TARG x -> fFORMULA x
 | CT_coerce_ID_OR_INT_to_TARG x -> fID_OR_INT x
-| CT_coerce_ID_OR_STRING_to_TARG x -> fID_OR_STRING x
 | 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_SPEC_LIST_to_TARG x -> fSPEC_LIST x
 | CT_coerce_TACTIC_COM_to_TARG x -> fTACTIC_COM x
@@ -1335,6 +1365,7 @@ and fVAR = function
 | CT_coerce_ID_OPT_OR_ALL_to_VARG x -> fID_OPT_OR_ALL x
 | CT_coerce_ID_OR_INT_OPT_to_VARG x -> fID_OR_INT_OPT x
 | CT_coerce_INT_LIST_to_VARG x -> fINT_LIST x
+| CT_coerce_SCOMMENT_CONTENT_to_VARG x -> fSCOMMENT_CONTENT x
 | CT_coerce_STRING_OPT_to_VARG x -> fSTRING_OPT x
 | CT_coerce_TACTIC_OPT_to_VARG x -> fTACTIC_OPT x
 | CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 1ba580c45..91bd1a13b 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -314,7 +314,7 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CProdN(_,ll,b)-> CT_prodc(xlate_binder_ne_list ll, xlate_formula b)
    | CLambdaN(_,ll,b)-> CT_lambdac(xlate_binder_ne_list ll, xlate_formula b)
    | CLetIn(_, v, a, b) -> 
-       CT_letin(xlate_id_opt v, xlate_formula a, xlate_formula b)
+       CT_letin(CT_def(xlate_id_opt v, xlate_formula a), xlate_formula b)
    | CAppExpl(_, r, l) ->
        CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)),
 	       xlate_formula_ne_list l)
@@ -892,6 +892,11 @@ and xlate_tac =
     | TacForward (_, _, _) -> xlate_error "TODO: Assert/Pose id:=c"
     | TacTrueCut (_, _) -> xlate_error "TODO: Assert id:t"
     | TacAnyConstructor tacopt -> xlate_error "TODO: Constructor tac"
+    | TacExtend(_, "Ring", [arg]) -> 
+	CT_ring
+	  (CT_formula_list
+	     (List.map xlate_formula
+		(out_gen (wit_list0 rawwit_constr) arg)))
     | TacExtend (_,id, l) ->
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
     | TacAlias (_, _, _) -> xlate_error "TODO: aliases"
@@ -910,7 +915,9 @@ and coerce_genarg_to_TARG x =
       CT_coerce_ID_OR_INT_to_TARG x
   | StringArgType ->
      let s = CT_string (out_gen rawwit_string x) in
-     CT_coerce_ID_OR_STRING_to_TARG (CT_coerce_STRING_to_ID_OR_STRING s)
+       CT_coerce_SCOMMENT_CONTENT_to_TARG
+	 (CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT
+	    (CT_coerce_STRING_to_ID_OR_STRING s))
   | PreIdentArgType ->
       let id = CT_ident (out_gen rawwit_pre_ident x) in
       CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
@@ -922,10 +929,12 @@ and coerce_genarg_to_TARG x =
       CT_coerce_ID_OR_INT_to_TARG (CT_coerce_ID_to_ID_OR_INT id)
   (* Specific types *)
   | SortArgType ->
-      CT_coerce_FORMULA_to_TARG
-        (CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x)))
+      CT_coerce_SCOMMENT_CONTENT_to_TARG
+      (CT_coerce_FORMULA_to_SCOMMENT_CONTENT
+        (CT_coerce_SORT_TYPE_to_FORMULA (xlate_sort (out_gen rawwit_sort x))))
   | ConstrArgType ->
-      CT_coerce_FORMULA_to_TARG (xlate_formula (out_gen rawwit_constr x))
+      CT_coerce_SCOMMENT_CONTENT_to_TARG
+      (CT_coerce_FORMULA_to_SCOMMENT_CONTENT (xlate_formula (out_gen rawwit_constr x)))
   | ConstrMayEvalArgType -> xlate_error"TODO: generic constr-may-eval argument"
   | QuantHypArgType ->xlate_error"TODO: generic quantified hypothesis argument"
   | TacticArgType ->
@@ -1141,6 +1150,13 @@ let cvt_vernac_binders args =
 let cvt_fixpoint_binders bl =
   CT_binder_list(List.map xlate_binder bl)
 
+let xlate_comment = function
+    CommentConstr c -> CT_coerce_FORMULA_to_SCOMMENT_CONTENT(xlate_formula c)
+  | CommentString s -> CT_coerce_ID_OR_STRING_to_SCOMMENT_CONTENT
+      (CT_coerce_STRING_to_ID_OR_STRING(CT_string s))
+  | CommentInt n ->
+      CT_coerce_FORMULA_to_SCOMMENT_CONTENT(CT_int_encapsulator (string_of_int n));;
+
 let xlate_vernac =
  function
    | VernacDeclareTacticDefinition (loc,[(_,id),TacFun (largs,tac)]) ->
@@ -1506,14 +1522,25 @@ let xlate_vernac =
   | VernacDebug b -> xlate_error "TODO: Debug On/Off"
 
   | VernacList l -> xlate_error "Not treated here"
-  |VernacNop -> CT_proof_no_op
-  | (VernacLocate _|VernacGlobalCheck _|VernacPrintOption _|
+  | VernacNop -> CT_proof_no_op
+  | VernacComments l -> 
+      CT_scomments(CT_scomment_content_list (List.map xlate_comment l))
+  | VernacDeclareImplicits(id, opt_positions) ->
+      CT_implicits
+	(reference_to_ct_ID id,
+	 match opt_positions with
+	     None -> CT_int_list[]
+	   | Some l -> CT_int_list(List.map (fun x -> CT_int x) l))
+  | VernacLocate(LocateTerm id) -> CT_locate(reference_to_ct_ID id)
+  | VernacLocate(LocateLibrary id) -> CT_locate_lib(reference_to_ct_ID id)
+  | VernacLocate(LocateFile s) -> CT_locate_file(CT_string s)
+  | (VernacGlobalCheck _|VernacPrintOption _|
      VernacMemOption (_, _)|VernacRemoveOption (_, _)|VernacAddOption (_, _)|
-     VernacSetOption (_, _)|VernacUnsetOption _|VernacDeclareImplicits (_, _)|
+     VernacSetOption (_, _)|VernacUnsetOption _|
      VernacHintDestruct (_, _, _, _, _)|VernacBack _|VernacRestoreState _|
      VernacWriteState _|VernacSolveExistential (_, _)|VernacCanonical _|
      VernacImport (_, _)|VernacExactProof _|VernacDistfix (_, _, _, _, _)|
-     VernacTacticGrammar _|VernacVar _|VernacTime _|VernacComments _)
+     VernacTacticGrammar _|VernacVar _|VernacTime _)
     -> xlate_error "TODO: vernac"
 
   (* Modules and Module Types *)