Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v

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

4 files changed, 52 insertions, 69 deletions

diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index 69687c1009..df2a44f3e7 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -12,31 +12,4 @@ Require Export Field_Compl.
 Require Export Field_Theory.
 Require Export Field_Tactic.
 
-Declare ML Module "field".
-
-Grammar vernac opt_arg_list : ast list :=
-| noal [] -> []
-| minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] ->
-  [ "minus" $aminus ($LIST $l) ]
-| div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] ->
-  [ "div" $adiv ($LIST $l) ]
-
-with extra_args : ast list :=
-| nea [] -> []
-| with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ]
-
-with vernac : ast := 
-  addfield [ "Add" "Field" 
-      	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
-      	     constrarg($azero) constrarg($aopp) constrarg($aeq)
-             constrarg($ainv) constrarg($rth) constrarg($ainv_l) extra_args($l)
-             "." ]
-    -> [(AddField $a $aplus $amult $aone $azero $aopp $aeq $ainv $rth
-                  $ainv_l ($LIST $l))].
-
-Grammar tactic simple_tactic: ast :=
-  | field [ "Field" constrarg_list($arg) ] -> [(Field ($LIST $arg))].
-
-Syntax tactic level 0:
-  | field [ <<(Field ($LIST $lc))>> ] -> ["Field" [1 1] (LISTSPC ($LIST $lc))]
-  | field_e [(Field)] -> ["Field"].
+(* Command declarations are moved to the ML side *)
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 7be170ebb7..e893c9f36c 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -271,7 +271,7 @@ Tactic Definition Field_Gen_Aux FT :=
     Let mul = (GiveMult '(EAplus trm1 trm2)) In
     Cut [ft:=FT][vm:=lvar](interp_ExprA ft vm trm1)==(interp_ExprA ft vm trm2);
     [Compute;Auto
-    |Intros;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
+    |Intros ft vm;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
      (Multiply mul);[(ApplySimplif ApplyMultiply);
        (ApplySimplif (ApplyInverse mul));
        (Let id = GrepMult In Clear id);WeakReduce;Clear ft vm;
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 54cc9609e9..fcd864f366 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -41,7 +41,7 @@ Inductive ExprA : Set :=
 
 Lemma eqExprA_O:(e1,e2:ExprA){e1=e2}+{~e1=e2}.
 Proof.
-  Double Induction 1 2;Try Intros;
+  Double Induction e1 e2;Try Intros;
    Try (Left;Reflexivity) Orelse Try (Right;Discriminate).
   Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
     Try (Left; Rewrite y; Rewrite y0;Auto)
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 1edf302e07..137d125287 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -19,6 +19,8 @@ open Term
 open Typing
 open Util
 open Vernacinterp
+open Vernacexpr
+open Tacexpr
 
 (* Interpretation of constr's *)
 let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
@@ -86,30 +88,43 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
   end
 
 (* Vernac command declaration *)
-let _ =
-  let rec opt_arg (aminus_o,adiv_o) = function
-    | (VARG_STRING "minus")::(VARG_CONSTR aminus)::l ->
-      (match aminus_o with
-      |	None -> opt_arg ((Some aminus),adiv_o) l
-      |	_ -> anomaly "AddField")
-    | (VARG_STRING "div")::(VARG_CONSTR adiv)::l ->
-      (match adiv_o with
-      |	None -> opt_arg (aminus_o,(Some adiv)) l
-      |	_ -> anomaly "AddField")
-    | _ -> (aminus_o,adiv_o) in
-  vinterp_add "AddField"
-    (function 
-       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
-	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
-	 ::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth)
-         ::(VARG_CONSTR ainv_l)::l ->
-         (fun () ->
-           let (aminus_o,adiv_o) = opt_arg (None,None) l in
-           add_field (constr_of a) (constr_of aplus) (constr_of amult)
-             (constr_of aone) (constr_of azero) (constr_of aopp)
-             (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
-             (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l))
-       | _ -> anomaly "AddField")
+open Extend
+open Pcoq
+open Genarg
+
+let wit_minus_div_arg, rawwit_minus_div_arg = Genarg.create_arg "minus_div_arg"
+let minus_div_arg = create_generic_entry "minus_div_arg" rawwit_minus_div_arg
+let _ = Tacinterp.add_genarg_interp "minus_div_arg"
+  (fun ist x ->
+    (in_gen wit_minus_div_arg
+      (out_gen (wit_pair (wit_opt wit_constr) (wit_opt wit_constr))
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr))
+	    (out_gen rawwit_minus_div_arg x))))))
+
+open Pcoq.Constr
+GEXTEND Gram
+  GLOBAL: minus_div_arg;
+  minus_arg: [ [ IDENT "minus"; ":="; aminus = constr -> aminus ] ];
+  div_arg: [ [ IDENT "div"; ":="; adiv = constr -> adiv ] ];
+  minus_div_arg:
+    [ [ "with"; m = minus_arg; d = OPT div_arg -> Some m, d
+      | "with"; d = div_arg; m = OPT minus_arg -> m, Some d
+      | -> None, None ] ];
+END
+
+VERNAC COMMAND EXTEND Field
+  [ "Add" "Field" 
+      constr(a) constr(aplus) constr(amult) constr(aone)
+      constr(azero) constr(aopp) constr(aeq)
+      constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
+    -> [ let (aminus_o, adiv_o) = md in
+         add_field
+           (constr_of a) (constr_of aplus) (constr_of amult)
+           (constr_of aone) (constr_of azero) (constr_of aopp)
+           (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
+           (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
+END
 
 (* Guesses the type and calls Field_Gen with the right theory *)
 let field g =
@@ -117,12 +132,12 @@ let field g =
   and env = pf_env g in
   let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
               goalopt=Some g; debug=get_debug () } in
-  let typ = constr_of_Constr (interp_tacarg ist
+  let typ = constr_of_VConstr (val_interp ist
     <:tactic<
       Match Context With
       | [|- (eq ?1 ? ?)] -> ?1
       | [|- (eqT ?1 ? ?)] -> ?1>>) in
-  let th = VArg (Constr (lookup typ)) in
+  let th = VConstr (lookup typ) in
   (tac_interp [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic<
       Match Context With
@@ -148,21 +163,16 @@ let guess_theory env evc = function
 let field_term l g =
   let env = (pf_env g)
   and evc = (project g) in
-  let th = constrIn (guess_theory env evc l)
-  and nl = List.map constrIn (Quote.sort_subterm g l) in
+  let th = valueIn (VConstr (guess_theory env evc l))
+  and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
   (List.fold_right
     (fun c a ->
      let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
-     tclTHENSI tac [a]) nl tclIDTAC) g
-
-(* Gives the constr list from the tactic_arg list *)
-let targ_constr =
-   List.map
-     (fun e ->
-        match e with
-        | Constr c -> c
-        | _ -> anomaly "Field: must be a constr")
+     Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
 
 (* Declaration of Field *)
-let _ = hide_tactic "Field"
-        (fun l -> if l = [] then field else field_term (targ_constr l))
+
+TACTIC EXTEND Field
+| [ "Field" ] -> [ field ]
+| [ "Field" ne_constr_list(l) ] -> [ field_term l ]
+END