Ajout de Eval, Inst et Check

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

4 files changed, 45 insertions, 18 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index ca5f582d9f..c93acba58b 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -56,9 +56,10 @@ GEXTEND Gram
   constr:
     [ [ c = constr8 -> c
       | IDENT "Inst"; id = ident; "["; c = constr8; "]" ->
-        <:ast< (CONTEXT $id $c) >>
+        <:ast<(CONTEXT $id $c)>>
       | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
-        <:ast< (EVAL $c (REDEXP $rtc)) >> ] ]
+        <:ast<(EVAL $c (REDEXP $rtc))>>
+      | IDENT "Check"; c = constr8 -> <:ast<(CHECK $c)>> ] ]
   ;
   lconstr:
     [ [ c = constr10 -> c ] ]
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 2beb62f243..ec482d43d0 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -145,6 +145,7 @@ GEXTEND Gram
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
         <:ast< (COMMAND (CONTEXT $id $c)) >>
+      | IDENT "Check"; c = Constr.constr  -> <:ast<(COMMAND (CHECK $c))>>
       |	st = simple_tactic -> st
       | id = lqualid; la = LIST1 tactic_atom0 ->
         <:ast< (APP $id ($LIST $la)) >>
@@ -164,6 +165,7 @@ GEXTEND Gram
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
       | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
         <:ast< (COMMAND (CONTEXT $id $c)) >>
+      | IDENT "Check"; c = Constr.constr  -> <:ast<(COMMAND (CHECK $c))>>
       |	"'"; c = constrarg -> c ] ]
   ;
   lqualid:
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index b9a1f23a78..c8c541228f 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -33,6 +33,7 @@ open Term
 open Termops
 open Declare
 open Safe_typing
+open Typing
 
 let err_msg_tactic_not_found macro_loc macro =
   user_err_loc
@@ -345,13 +346,18 @@ let read_pattern evc env lfun = function
       "Not a pattern ast node: " ++ print_ast ast))
 
 (* Reads the hypotheses of a Match Context rule *)
-let rec read_match_context_hyps evc env lfun = function
+let rec read_match_context_hyps evc env lfun lidh = function
   | Node(_,"MATCHCONTEXTHYPS",[mp])::tl ->
-    (NoHypId (read_pattern evc env lfun mp))::(read_match_context_hyps evc env
-      lfun tl)
-  | Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);mp])::tl ->
-    (Hyp (s,read_pattern evc env lfun mp))::(read_match_context_hyps evc env
-      lfun tl)
+    (NoHypId (read_pattern evc env lfun mp))::
+      (read_match_context_hyps evc env lfun lidh tl)
+  | (Node(_,"MATCHCONTEXTHYPS",[Nvar(_,s);mp]) as ast)::tl ->
+    if List.mem s lidh then
+      user_err_loc (Ast.loc ast,"Tacinterp.read_match_context_hyps",
+      str ("Hypothesis pattern-matching variable "^(string_of_id s)^
+           " used twice in the same pattern"))
+    else
+      (Hyp (s,read_pattern evc env lfun mp))::
+        (read_match_context_hyps evc env lfun (s::lidh) tl)
   | ast::tl ->
     anomaly_loc (Ast.loc ast, "Tacinterp.read_match_context_hyp",(str
       "Not a MATCHCONTEXTHYP ast node: " ++ print_ast ast))
@@ -363,7 +369,7 @@ let rec read_match_context_rule evc env lfun = function
     (All tc)::(read_match_context_rule evc env lfun tl)
   | Node(_,"MATCHCONTEXTRULE",l)::tl ->
     let rl=List.rev l in
-      (Pat (read_match_context_hyps evc env lfun (List.rev (List.tl (List.tl
+      (Pat (read_match_context_hyps evc env lfun [] (List.rev (List.tl (List.tl
         rl))),read_pattern evc env lfun (List.nth rl 1),List.hd
         rl))::(read_match_context_rule evc env lfun tl)
   | ast::tl ->
@@ -490,7 +496,9 @@ let rec val_interp ist ast =
           | Some g -> match_context_interp ist ast lmr g)
     | Node(_,"MATCH",lmr) -> match_interp ist ast lmr
     (* Delayed evaluation *)
-    | Node(loc,("LETCUT"|"IDTAC"|"FAIL"|"PROGRESS"|"TACTICLIST"|"DO"|"TRY"|"INFO"|"REPEAT"|"ORELSE"|"FIRST"|"TCLSOLVE"),_) -> VTacticClos (ist,ast)
+    | Node(loc,("LETCUT"|"IDTAC"|"FAIL"|"PROGRESS"|"TACTICLIST"|"DO"|"TRY"
+               |"INFO"|"REPEAT"|"ORELSE"|"FIRST"|"TCLSOLVE"),_) ->
+      VTacticClos (ist,ast)
     (* Arguments and primitive tactics *)
     | Node(_,"VOID",[]) -> VVoid
     | Nvar(_,s) ->
@@ -863,8 +871,7 @@ and apply_hyps_context ist mt lgmatch mhyps hyps =
             eval_with_fail
               (val_interp {ist with lfun=lfun@lid@lc@ist.lfun;
                                     lmatch=lmatch@lm@ist.lmatch;
-                                    goalopt=Some goal})
-              mt goal
+                                    goalopt=Some goal}) mt goal
         else
           let nextlhyps =
             List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) []
@@ -1032,6 +1039,8 @@ and com_interp ist com =
       | Not_found ->
         errorlabstrm "com_interp" (str "Unbound context identifier" ++
           print_ast ast))
+    | Node(_,"CHECK",[c]) ->
+      let csr = interp_constr ist c None in type_of ist.env ist.evc csr
     | c -> interp_constr ist c None in
   begin
     db_constr ist.debug ist.env csr;
@@ -1063,6 +1072,9 @@ and cast_com_interp ist com =
          | Not_found ->
            errorlabstrm "cast_com_interp" (str "Unbound context identifier" ++
              print_ast ast))
+      | Node(_,"CHECK",[c]) ->
+        let csr = interp_constr ist c (Some (pf_concl gl)) in
+        type_of ist.env ist.evc csr
       | c ->
         interp_constr ist c (Some (pf_concl gl)) in
     begin
@@ -1096,6 +1108,9 @@ and cast_opencom_interp ist com =
       |	Not_found ->
         errorlabstrm "cast_opencom_interp" (str "Unbound context identifier" ++
           print_ast ast))
+    | Node(_,"CHECK",[c]) ->
+      let csr = interp_constr ist c (Some (pf_concl gl)) in
+      VArg (Constr (type_of ist.env ist.evc csr))
     | c ->
         VArg
 	  (OpenConstr (interp_openconstr ist c (Some (pf_concl gl)))))
@@ -1123,7 +1138,7 @@ and cvt_pattern ist = function
       let occs = List.map num_of_ast nums
       and csr = constr_of_Constr (unvarg (val_interp
         ist (Node(loc,"COMMAND",[com])))) in
-      let jdt = Typing.unsafe_machine ist.env ist.evc csr in
+      let jdt = unsafe_machine ist.env ist.evc csr in
       (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type)
   | arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
 
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 05effb2430..434590cb8f 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -42,7 +42,7 @@ Syntax tactic
 
   level 2:
   | orelse [ $st Orelse $tc ] -> [ [<hov 0> $st:L " Orelse" [1 1] $tc:E] ]
-  | match_context [<<(MATCHCONTEXT ($LIST $lrul))>>] ->
+  | match_context [<<(MATCHCONTEXT "RL" ($LIST $lrul))>>] ->
     [ [ <hov 0> "Match Context With" (MATCHCONTEXTLIST ($LIST $lrul)) ] ]
   | match [<<(MATCH $t ($LIST $lrul))>>] ->
     [ [ <hov 0> "Match" [1 0] $t [1 0] "With" (MATCHLIST ($LIST $lrul)) ] ]
@@ -138,10 +138,13 @@ Syntax tactic
     ["First" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
   | solve  [<<(TCLSOLVE ($LIST $l))>>] ->
     ["Solve" [1 0] "[" [1 0] (TACTICSEQBODY ($LIST $l)) [1 0] "]"]
-  | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] 
-         -> ["Abstract " $t:E]
-  | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] 
-         -> ["Abstract " $t:E " using "  $id]
+  | abstract_anon [<<(ABSTRACT (TACTIC $t))>>] -> ["Abstract " $t:E]
+  | abstract_name [<<(ABSTRACT ($VAR $id) (TACTIC $t))>>] ->
+    ["Abstract " $t:E " using "  $id]
+  | eval  [<<(EVAL $c (REDEXP $rtc))>>] ->
+    ["Eval" [1 0] (REDEXP $rtc) [1 0] "in" [1 0] (COMMAND $c)]
+  | inst  [<<(CONTEXT $id $c)>>] -> ["Inst" [1 0] $id "[" (COMMAND $c) "]"]
+  | check [<<(CHECK $c)>>] -> ["Check" [1 0] (COMMAND $c)]
 
 (* =================================== *)
 (*     PP rules for simple tactics     *)
@@ -434,6 +437,12 @@ Syntax tactic
   | tactic_to_castedconstr [<<(CASTEDCOMMAND $c)>>] -> [ $c:"constr":9 ]
   | tactic_to_openconstr [<<(CASTEDOPENCOMMAND $c)>>] -> [ $c:"constr":9 ]
 
+  (* Some operations over constr to be pretty-printed here *)
+  | eval_command  [<<(COMMAND (EVAL $c (REDEXP $rtc)))>>] ->
+    [(EVAL $c (REDEXP $rtc))]
+  | inst_command  [<<(COMMAND (CONTEXT $id $c))>>] -> [(CONTEXT $id $c)]
+  | check_command [<<(COMMAND (CHECK $c))>>] -> [(CHECK $c)]
+
   (* This is produced bu UNFOLDLIST *)
   | tactic_qualidarg_constr [<<(COMMAND (QUALIDARG $p))>>] -> [(QUALIDARG $p)]
   | tactic_qualidarg_nil [<<(QUALIDARG $id)>>] -> [ $id ]