adds the notations in inductive definitions, improves the consistency between

induction et destruct, takes the extra argument for fail and idtac into
account


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

3 files changed, 46 insertions, 26 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 829972ecf..7106b5d65 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -187,6 +187,9 @@ and ct_CONV_SET =
   | CT_unfbut of ct_ID list
 and ct_CO_IND =
     CT_co_ind of string
+and ct_DECL_NOTATION_OPT =
+    CT_coerce_NONE_to_DECL_NOTATION_OPT of ct_NONE
+  | CT_decl_notation of ct_STRING * ct_FORMULA * ct_ID_OPT
 and ct_DEF =
     CT_def of ct_ID_OPT * ct_FORMULA
 and ct_DEFN =
@@ -317,7 +320,7 @@ and ct_IMPEXP =
     CT_export
   | CT_import
 and ct_IND_SPEC =
-    CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST
+    CT_ind_spec of ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_CONSTR_LIST * ct_DECL_NOTATION_OPT
 and ct_IND_SPEC_LIST =
     CT_ind_spec_list of ct_IND_SPEC list
 and ct_INT =
@@ -532,12 +535,12 @@ and ct_TACTIC_COM =
   | CT_elim_type of ct_FORMULA
   | CT_exact of ct_FORMULA
   | CT_exists of ct_SPEC_LIST
-  | CT_fail of ct_INT
+  | CT_fail of ct_INT * ct_STRING_OPT
   | CT_first of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_fixtactic of ct_ID_OPT * ct_INT * ct_FIX_TAC_LIST
   | CT_generalize of ct_FORMULA_NE_LIST
   | CT_generalize_dependent of ct_FORMULA
-  | CT_idtac
+  | CT_idtac of ct_STRING_OPT
   | CT_induction of ct_ID_OR_INT
   | CT_info of ct_TACTIC_COM
   | CT_injection_eq of ct_ID_OR_INT_OPT
@@ -554,7 +557,7 @@ and ct_TACTIC_COM =
   | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
-  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
+  | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
   | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index eeb09b2a9..f3610f4d3 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -500,7 +500,14 @@ and fCONV_SET = function
 and fCO_IND = function
 | CT_co_ind x -> fATOM "co_ind";
    (f_atom_string x);
-   print_string "\n"and fDEF = function
+   print_string "\n"and fDECL_NOTATION_OPT = function
+| CT_coerce_NONE_to_DECL_NOTATION_OPT x -> fNONE x
+| CT_decl_notation(x1, x2, x3) ->
+   fSTRING x1;
+   fFORMULA x2;
+   fID_OPT x3;
+   fNODE "decl_notation" 3
+and fDEF = function
 | CT_def(x1, x2) ->
    fID_OPT x1;
    fFORMULA x2;
@@ -772,12 +779,13 @@ and fIMPEXP = function
 | CT_export -> fNODE "export" 0
 | CT_import -> fNODE "import" 0
 and fIND_SPEC = function
-| CT_ind_spec(x1, x2, x3, x4) ->
+| CT_ind_spec(x1, x2, x3, x4, x5) ->
    fID x1;
    fBINDER_LIST x2;
    fFORMULA x3;
    fCONSTR_LIST x4;
-   fNODE "ind_spec" 4
+   fDECL_NOTATION_OPT x5;
+   fNODE "ind_spec" 5
 and fIND_SPEC_LIST = function
 | CT_ind_spec_list l ->
    (List.iter fIND_SPEC l);
@@ -1248,9 +1256,10 @@ and fTACTIC_COM = function
 | CT_exists(x1) ->
    fSPEC_LIST x1;
    fNODE "exists" 1
-| CT_fail(x1) ->
+| CT_fail(x1, x2) ->
    fINT x1;
-   fNODE "fail" 1
+   fSTRING_OPT x2;
+   fNODE "fail" 2
 | CT_first(x,l) ->
    fTACTIC_COM x;
    (List.iter fTACTIC_COM l);
@@ -1266,7 +1275,9 @@ and fTACTIC_COM = function
 | CT_generalize_dependent(x1) ->
    fFORMULA x1;
    fNODE "generalize_dependent" 1
-| CT_idtac -> fNODE "idtac" 0
+| CT_idtac(x1) ->
+   fSTRING_OPT x1;
+   fNODE "idtac" 1
 | CT_induction(x1) ->
    fID_OR_INT x1;
    fNODE "induction" 1
@@ -1330,7 +1341,7 @@ and fTACTIC_COM = function
 | CT_new_destruct(x1, x2, x3) ->
    fFORMULA_OR_INT x1;
    fUSING x2;
-   fID_LIST_LIST x3;
+   fINTRO_PATT_LIST x3;
    fNODE "new_destruct" 3
 | CT_new_induction(x1, x2, x3) ->
    fFORMULA_OR_INT x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 2d6cca540..aae7d714f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -606,11 +606,6 @@ let rec xlate_intro_pattern =
   | IntroWildcard -> CT_coerce_ID_to_INTRO_PATT(CT_ident "_" )
   | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c)
 
-let xlate_newind_names = 
-  function
-    | IntroIdentifier id -> xlate_ident id
-    | _ -> xlate_error "TODO: intro_patterns for NewDestruct/NewInduction"
-
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
  | SimpleInversion -> CT_inv_simple
@@ -853,10 +848,10 @@ and xlate_tactic =
 		   (xlate_local_rec_tac f1, List.map xlate_local_rec_tac l) in
        CT_rec_tactic_in(tl, xlate_tactic t)
    | TacAtom (_, t) -> xlate_tac t 
-   | TacFail (n,"") -> CT_fail (CT_int n)
-   | TacFail (n,s) -> xlate_error "TODO: Fail n message"
-   | TacId "" -> CT_idtac
-   | TacId _ -> xlate_error "TODO: Idtac with argument"
+   | TacFail (n,"") -> CT_fail(CT_int n, ctf_STRING_OPT_NONE)
+   | TacFail (n,s) -> CT_fail(CT_int n, ctf_STRING_OPT_SOME (CT_string s))
+   | TacId "" -> CT_idtac ctf_STRING_OPT_NONE
+   | TacId s -> CT_idtac(ctf_STRING_OPT_SOME (CT_string s))
    | TacInfo t -> CT_info(xlate_tactic t)
    | TacArg a -> xlate_call_or_tacarg a
 
@@ -1095,8 +1090,11 @@ and xlate_tac =
     | TacNewDestruct(a,b,(c,_)) ->
 	CT_new_destruct
 	  (xlate_int_or_constr a, xlate_using b, 
-	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
+	   (CT_intro_patt_list
+	      (List.map (fun l -> 
+			   CT_conj_pattern
+			     (CT_intro_patt_list
+				(List.map xlate_intro_pattern l))) c)))
     | TacNewInduction(a,b,(c,_)) ->
 	CT_new_induction
 	  (xlate_int_or_constr a, xlate_using b,
@@ -1391,6 +1389,15 @@ let xlate_comment = function
       CT_coerce_FORMULA_to_SCOMMENT_CONTENT
 	(CT_coerce_NUM_to_FORMULA(CT_int_encapsulator (string_of_int n)));;
 
+let translate_opt_notation_decl = function
+    None -> CT_coerce_NONE_to_DECL_NOTATION_OPT(CT_none)
+  |  Some(s, f, sc) ->
+       let tr_sc = 
+	 match sc with 
+	     None -> ctv_ID_OPT_NONE
+	   | Some id -> CT_coerce_ID_to_ID_OPT (CT_ident id) in
+       CT_decl_notation(CT_string s, xlate_formula f, tr_sc);;
+
 let xlate_vernac =
  function
    | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) ->
@@ -1650,11 +1657,10 @@ let xlate_vernac =
    | VernacInductive (isind, lmi) ->
       let co_or_ind = if isind then "Inductive" else "CoInductive" in
       let strip_mutind ((_,s), notopt, parameters, c, constructors) =
-        if notopt = None then
-           CT_ind_spec
+          CT_ind_spec
             (xlate_ident s, xlate_binder_list parameters, xlate_formula c,
-             build_constructors constructors)
-        else xlate_error "TODO: Notation in Inductive" in
+             build_constructors constructors,
+	     translate_opt_notation_decl notopt) in
         CT_mind_decl
 	  (CT_co_ind co_or_ind, CT_ind_spec_list (List.map strip_mutind lmi))
    | VernacFixpoint [] -> xlate_error "mutual recursive"