Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR

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

10 files changed, 136 insertions, 93 deletions

diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index fc09cfa69c..70596779d0 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -578,14 +578,11 @@ GEXTEND Gram
       tac = Tactic.tactic; "." ->
 	let d = Ast.dynamic (in_prog p) in
 	let str = Ast.str s in
-	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >>
-
-    | IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
+	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ];
+  Pcoq.Vernac_.command:
+  [ [ IDENT "Debug"; IDENT "on"; "." -> <:ast< (PROGDEBUGON) >>
 	
-    | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >>
-	    
-  ] ]
-  ;
+    | IDENT "Debug"; IDENT "off"; "." -> <:ast< (PROGDEBUGOFF) >> ] ];
  END
 ;;
 
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 61bd3353f7..90e87c9df5 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -71,8 +71,8 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
   ainv_l =
   begin
     (try
-       Ring.add_theory true true false a None None None aplus amult aone azero (Some aopp) aeq rth
-         Quote.ConstrSet.empty
+      Ring.add_theory true true false a None None None aplus amult aone azero
+        (Some aopp) aeq rth Quote.ConstrSet.empty
      with | UserError("Add Semi Ring",_) -> ());
     let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"),
       [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in
@@ -112,12 +112,20 @@ let field g =
   let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
               goalopt=Some g; debug=get_debug () } in
   let typ = constr_of_Constr (interp_tacarg ist
-  <:tactic<
+    <:tactic<
       Match Context With
-      | [|-(eq ?1 ? ?)] -> ?1
-      |	[|-(eqT ?1 ? ?)] -> ?1>>) in
+      | [|- (eq ?1 ? ?)] -> ?1
+      | [|- (eqT ?1 ? ?)] -> ?1>>) in
   let th = VArg (Constr (lookup typ)) in
-  (tac_interp [(id_of_string "FT",th)] [] (get_debug ()) <:tactic<Field_Gen FT>>) g
+  (tac_interp [(id_of_string "FT",th)] [] (get_debug ())
+    <:tactic<
+      Match Context With
+      | [|- (eq ?1 ?2 ?3)] ->
+        Let t = (eqT ?1 ?2 ?3) In
+        Cut t;[Intro;
+          (Match Context With
+          | [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT]
+      | [|- (eqT ? ? ?)] -> Field_Gen FT>>) g
 
 (* Declaration of Field *)
 let _ = hide_tactic "Field" (function _ -> field)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index af4df3b6f4..66c8e0170b 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -455,7 +455,7 @@ GEXTEND Gram
           <:ast< (ResetSection $id) >>
       
 (* Tactic Debugger *)
-      |	IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >>
+      | IDENT "Debug"; IDENT "On" -> <:ast< (DebugOn) >>
       |	IDENT "Debug"; IDENT "Off" -> <:ast< (DebugOff) >>
 
  ] ];
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 8d44d146ee..339a53d82d 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -476,12 +476,12 @@ let rec val_interp ist ast =
 (* mSGNL [<print_ast ast>]; *)
 (* mSGNL [<print_ast (Termast.ast_of_constr false (Pretty.assumptions_for_print []) c)>] *)
 
-  let value_interp debug =
+  let value_interp ist =
   match ast with
     | Node(_,"APP",l) ->
         let fv = val_interp ist (List.hd l)
         and largs = List.map (val_interp ist) (List.tl l) in
-      app_interp ist fv largs ast
+        app_interp ist fv largs ast
     | Node(_,"FUN",l) -> VFun (ist.lfun,read_fun (List.hd l),List.nth l 1)
     | Node(_,"REC",l) -> rec_interp ist ast l
     | Node(_,"LET",[Node(_,"LETDECL",l);u]) ->
@@ -508,10 +508,10 @@ let rec val_interp ist ast =
     | Node(_,"FIRST",l) -> VTactic (tclFIRST (List.map (tactic_interp ist) l))
     | Node(_,"TCLSOLVE",l) ->
         VTactic (tclSOLVE (List.map (tactic_interp ist) l))
-    | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
+(*    | Node(loc0,"APPTACTIC",[Node(loc1,s,l)]) ->
         val_interp ist
-          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))
-    | Node(_,"PRIM-TACTIC",[Node(loc,opn,[])]) ->
+          (Node(loc0,"APP",[Node(loc1,"PRIM-TACTIC",[Node(loc1,s,[])])]@l))*)
+    | Node(_,"PRIMTACTIC",[Node(loc,opn,[])]) ->
         VFTactic ([],(interp_atomic opn))
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
@@ -553,7 +553,18 @@ let rec val_interp ist ast =
           ((look_for_interp s) ist ast)
         with
            Not_found ->
-             val_interp ist (Node(dummy_loc,"APPTACTIC",[ast])))
+             if l = [] then
+               VFTactic ([],(interp_atomic s))
+             else
+               let fv = val_interp ist
+                          (Node(loc,"PRIMTACTIC",[Node(loc,s,[])]))
+               and largs = List.map (val_interp ist) l in
+               app_interp ist fv largs ast)
+
+       (*     val_interp ist (Node(dummy_loc,"APP",[Node(loc,"PRIMTACTIC",
+                            [Node(loc,s,[])])]@l)))*)
+ 
+(*             val_interp ist (Node(dummy_loc,"APPTACTIC",[ast])))*)
     | Dynamic(_,t) ->
       let tg = (tag t) in
       if tg = "tactic" then
@@ -571,9 +582,9 @@ let rec val_interp ist ast =
   if ist.debug = DebugOn then
     match debug_prompt ist.goalopt ast with
     | Exit -> VTactic tclIDTAC
-    | v -> value_interp v
+    | v -> value_interp {ist with debug=v}
   else
-    value_interp debug
+    value_interp ist
 
 (* Interprets an application node *)
 and app_interp ist fv largs ast =
@@ -979,47 +990,58 @@ and bind_interp ist = function
       print_ast x>]
 
 (* Interprets a COMMAND expression (in case of failure, returns Command) *)
-and com_interp ist = function
-  | Node(_,"EVAL",[c;rtc]) ->
-    let redexp = unredexp (unvarg (val_interp ist rtc)) in
-    VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc
-		    (interp_constr ist c None)))
-  | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
-    (try
-      let ic = interp_constr ist c None
-      and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
-      VArg (Constr (subst_meta [-1,ic] ctxt))
-     with
-    | Not_found ->
-      errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
-        print_ast ast>])
-  | c -> VArg (Constr (interp_constr ist c None))
-
-(* Interprets a CASTEDCOMMAND expression *)
-and cast_com_interp ist com =
-  match ist.goalopt with
-  | Some gl ->
-    (match com with
+and com_interp ist com = 
+  let csr =
+    match com with
     | Node(_,"EVAL",[c;rtc]) ->
-      let redexp = unredexp (unvarg (val_interp
-        ist rtc)) in
-      VArg (Constr ((reduction_of_redexp redexp) ist.env ist.evc
-        (interp_constr ist c (Some (pf_concl gl)))))
+      let redexp = unredexp (unvarg (val_interp ist rtc)) in
+      (reduction_of_redexp redexp) ist.env ist.evc (interp_constr ist c None)
     | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
       (try
         let ic = interp_constr ist c None
         and ctxt = constr_of_Constr_context (unvarg (List.assoc s ist.lfun)) in
-        begin
-          wARNING [<'sTR
-            "Cannot pre-constrain the context expression with goal">];
-          VArg (Constr (subst_meta [-1,ic] ctxt))
-        end
+        subst_meta [-1,ic] ctxt
        with
-      |	Not_found ->
-        errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier";
+      | Not_found ->
+        errorlabstrm "com_interp" [<'sTR "Unbound context identifier";
           print_ast ast>])
-    | c ->
-        VArg (Constr (interp_constr ist c (Some (pf_concl gl)))))
+    | c -> interp_constr ist c None in
+  begin
+    db_constr ist.debug ist.env csr;
+    VArg (Constr csr)
+  end
+
+(* Interprets a CASTEDCOMMAND expression *)
+and cast_com_interp ist com =
+  match ist.goalopt with
+  | Some gl ->
+    let csr =
+      match com with
+      | Node(_,"EVAL",[c;rtc]) ->
+        let redexp = unredexp (unvarg (val_interp
+          ist rtc)) in
+        (reduction_of_redexp redexp) ist.env ist.evc
+          (interp_constr ist c (Some (pf_concl gl)))
+      | Node(_,"CONTEXT",[Nvar (_,s);c]) as ast ->
+        (try
+          let ic = interp_constr ist c None
+          and ctxt = constr_of_Constr_context
+            (unvarg (List.assoc s ist.lfun)) in
+          begin
+           wARNING [<'sTR
+              "Cannot pre-constrain the context expression with goal">];
+            subst_meta [-1,ic] ctxt
+          end
+         with
+         | Not_found ->
+           errorlabstrm "cast_com_interp" [<'sTR "Unbound context identifier";
+             print_ast ast>])
+      | c ->
+        interp_constr ist c (Some (pf_concl gl)) in
+    begin
+      db_constr ist.debug ist.env csr;
+      VArg (Constr csr)
+    end
   | None ->
     errorlabstrm "val_interp" [<'sTR "Cannot cast a constr without goal">]
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 0cdf49c70c..08446d0112 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -25,23 +25,39 @@ let db_pr_goal = function
   | Some g ->
     mSGNL [<'sTR ("Goal:"); 'fNL; Proof_trees.pr_goal (Tacmach.sig_it g) >]
 
+(* Prints the commands *)
+let help () =
+  mSGNL [< 'sTR "Commands: <Enter>=Continue, h=Help, s=Skip, x=Exit" >]
+
 (* Prints the state and waits for an instruction *)
 let debug_prompt goalopt tac_ast =
   db_pr_goal goalopt;
-  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
-         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];
+  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL >];
+(*         'sTR "Commands: <Enter>=Continue, s=Skip, x=Exit" >];*)
+(*  mSG [< 'sTR "Going to execute:"; 'fNL; (gentacpr tac_ast); 'fNL; 'fNL;
+         'sTR "----<Enter>=Continue----s=Skip----x=Exit----" >];*)
   let rec prompt () =
-    mSG [<'fNL; 'sTR "TcDebug> " >];
+    mSG [<'fNL; 'sTR "TcDebug > " >];
     flush stdout;
     let inst = read_line () in
-    mSGNL [<>];
+(*    mSGNL [<>];*)
     match inst with
     | ""  -> DebugOn
     | "s" -> DebugOff
     | "x" -> Exit
+    | "h" ->
+      begin
+        help ();
+        prompt ()
+      end
     | _   -> prompt () in
   prompt ()
 
+(* Prints a constr *)
+let db_constr debug env c =
+  if debug = DebugOn then
+    mSGNL [< 'sTR "Evaluated term --> ";  prterm_env env c >]
+
 (* Prints a matched hypothesis *)
 let db_matched_hyp debug env (id,c) =
   if debug = DebugOn then
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index aa386762b9..4a6aecfde9 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -24,6 +24,9 @@ type debug_info =
 (* Prints the state and waits *)
 val debug_prompt : goal sigma option -> Coqast.t -> debug_info
 
+(* Prints a constr *)
+val db_constr : debug_info -> Environ.env -> constr -> unit
+
 (* Prints a matched hypothesis *)
 val db_matched_hyp : debug_info -> Environ.env -> string * constr -> unit
 
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index f4718f2f2b..a72a70ee57 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -418,6 +418,9 @@ Syntax tactic
                   [ $x ","[1 0] (LISTCOMA ($LIST $l)) ]
   | listcoma_one  [<<(LISTCOMA $x)>>] -> [ $x ]
   | listcoma_nil  [<<(LISTCOMA )>>] -> [ ]
+
+  (* Only when debugging *)
+  | prim_tactic [<<(PRIMTACTIC $tac)>>] -> [ $tac ]
   ;
 
   level 8:
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ab96c8759b..7ccca8c758 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -60,9 +60,9 @@ let axioms ist =
   and t_is_empty = tacticIn is_empty in
   <:tactic<
     Match Context With
-    |[ |- ?1] -> $t_is_unit;Constructor
-    |[ _:?1 |- ?] -> $t_is_empty
-    |[ _:?1 |- ?1] -> Assumption>>
+    |[|- ?1] -> $t_is_unit;Constructor
+    |[_:?1 |- ?] -> $t_is_empty
+    |[_:?1 |- ?1] -> Assumption>>
 
 let simplif ist =
   let t_is_unit = tacticIn is_unit
diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 9005b60896..c955c57eff 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -12,38 +12,28 @@ Require Rbase.
 
 Recursive Tactic Definition Isrealint trm:=
   Match trm With
-  | [R0] -> Idtac
-  | [R1] -> Idtac
-  | [(Rplus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Rminus ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Rmult ?1 ?2)] -> (Isrealint ?1);(Isrealint ?2)
-  | [(Ropp ?1)] -> (Isrealint ?1)
+  | [``0``] -> Idtac
+  | [``1``] -> Idtac
+  | [``?1+?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``?1-?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``?1*?2``] -> (Isrealint ?1);(Isrealint ?2)
+  | [``-?1``] -> (Isrealint ?1)
   | _ -> Fail.
 
-
-Tactic Definition Sup0 :=
+Recursive Tactic Definition Sup0 :=
   Match Context With
-  | [ |- (Rgt R1 R0) ] -> Unfold Rgt;Apply Rlt_R0_R1
-  | [ |- (Rgt (Rplus R1 ?1) R0) ] ->
-    Apply (Rgt_trans (Rplus R1 ?1) ?1 R0);
-    [Pattern 1 (Rplus R1 ?1);Rewrite Rplus_sym;Unfold Rgt;
-     Apply Rlt_r_r_plus_R1
-    |Sup0].
+  | [ |- ``1>0`` ] -> Unfold Rgt;Apply Rlt_R0_R1
+  | [ |- ``1+?1>0`` ] ->
+    Apply (Rgt_trans ``1+?1`` ?1 ``0``);
+    [Pattern 1 ``1+?1``;Rewrite Rplus_sym;Unfold Rgt;
+     Apply Rlt_r_r_plus_R1|Sup0].
 
 Tactic Definition DiscrR :=
-  Match Context With
-  | [ |- ~R1==R0 ] -> Red;Intro;Apply R1_neq_R0;Assumption
-  | [ |- ~((Rplus R1 ?1)==R0) ] -> (Isrealint ?1);Apply Rgt_not_eq;Sup0
-  | [ |- ~(Ropp ?1)==R0 ] -> (Isrealint ?1);Apply Ropp_neq; DiscrR
-  | [ |- ~(?1==?1) ] -> ElimType False
-  | [ |- ~(Rminus R0 ?1)==R0 ] -> (Isrealint ?1);Rewrite Rminus_Ropp; DiscrR
-  | [ |- ~(?1==?2) ] -> ((Isrealint ?1);(Isrealint ?2);
-    Apply Rminus_not_eq; Ring (Rminus ?1 ?2); 
+  Try Match Context With
+  | [ |- ~(?1==?2) ] ->
+    Isrealint ?1;Isrealint ?2;
+    Apply Rminus_not_eq; Ring ``?1-?2``; 
       (Match Context With
-      | [ |- ~(Rplus (Ropp R1) ?)==R0 ] -> 
-        Repeat Rewrite <-Ropp_distr1; DiscrR
-      | [ |- ? ] -> DiscrR)
-     Orelse (Apply Rminus_not_eq_right; DiscrR)).
-  
-
-
+      | [ |- ``-1+?<>0`` ] -> 
+        Repeat Rewrite <- Ropp_distr1;Apply Ropp_neq
+      | _ -> Idtac);Apply Rgt_not_eq;Sup0.
diff --git a/theories/Reals/Rsyntax.v b/theories/Reals/Rsyntax.v
index 9600cdce34..21a33391c2 100644
--- a/theories/Reals/Rsyntax.v
+++ b/theories/Reals/Rsyntax.v
@@ -50,7 +50,6 @@ with rexpr2 : constr :=
 
 with rexpr0 : constr :=
   expr_id [ constr:global($c) ] -> [ $c ]
-| expr_hole [ "?" ] -> [ ? ]
 | expr_com [ "[" constr:constr($c) "]" ] -> [ $c ]
 | expr_appl [ "(" rapplication($a) ")" ] -> [ $a ]
 | expr_num [ rnumber($s) ] -> [ $s ]
@@ -58,6 +57,11 @@ with rexpr0 : constr :=
 | expr_div [ rexpr0($p) "/" rexpr0($c) ] -> [ (Rdiv $p $c) ]
 | expr_opp [ "-" rexpr0($c) ] -> [ (Ropp $c) ] 
 | expr_inv [ "/" rexpr0($c) ] -> [ (Rinv $c) ]
+| expr_meta [ meta($m) ] -> [ $m ]
+
+with meta : ast :=
+| rimpl [ "?" ] -> [ (ISEVAR) ]
+| rmeta [ "?" prim:number($n) ] -> [ (META $n) ]
 
 with rapplication : constr :=
   apply [ rapplication($p) rexpr($c1) ] -> [ ($p $c1) ]