Interpretation MetaId + Progress + Inst

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

6 files changed, 34 insertions, 6 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 45b6b6ae9..30ec93b79 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -716,8 +716,12 @@ let type_judgment_of_rawconstr sigma env c =
   understand_type_judgment sigma env (interp_rawconstr sigma env c)
 
 (*To retype a list of key*constr with undefined key*)
-let retype_list sigma env lst=
-  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst
+let retype_list sigma env lst =
+  List.fold_right (fun (x,csr) a ->
+    try (x,Retyping.get_judgment_of env sigma csr)::a with
+    | Anomaly _ -> a) lst []
+
+(*  List.map (fun (x,csr) -> (x,Retyping.get_judgment_of env sigma csr)) lst*)
 
 (* Interprets a constr according to two lists *)
 (* of instantiations (variables and metas)    *)
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 56779d71f..4bb01a6a4 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -43,8 +43,10 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = constr8 -> c 
-(*      | IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
+      (*| IDENT "Context"; id = ident; IDENT "With"; c = constr8 ->
         <:ast< (CONTEXT $id $c) >>*)
+      | IDENT "Inst"; id = ident; "["; c = constr8; "]" ->
+        <:ast< (CONTEXT $id $c) >>
       | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr8 ->
         <:ast< (EVAL $c (REDEXP $rtc)) >> ] ]
   ;
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index fc455cd21..142dac320 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -50,6 +50,10 @@ GEXTEND Gram
   identarg:
     [ [ id = Constr.ident -> id ] ]
   ;
+  idmeta_arg:
+    [ [ id = Constr.ident -> id
+      | "?"; n = Prim.number -> <:ast< (METAID $n) >> ] ]
+  ;
   qualidarg:
     [ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
       | "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ]
@@ -90,6 +94,9 @@ GEXTEND Gram
   ne_identarg_list:
     [ [ l = LIST1 identarg -> l ] ]
   ;
+  ne_idmeta_arg_list:
+    [ [ l = LIST1 idmeta_arg -> l ] ]
+  ;
   ne_qualidarg_list:
     [ [ l = LIST1 qualidarg -> l ] ]
   ;
@@ -249,7 +256,8 @@ GEXTEND Gram
   match_pattern:
     [ [ id = constrarg; "["; pc = constrarg; "]" ->
         (match id with
-        | Coqast.Node(_,"COMMAND",[Coqast.Nvar(_,s)]) ->
+        | Coqast.Node(_,"COMMAND",
+            [Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)])]) ->
           <:ast< (SUBTERM ($VAR $s) $pc) >>
         | _ ->
           errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
@@ -343,6 +351,7 @@ GEXTEND Gram
       |	IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>>
       |	ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
           <:ast< (ORELSE $ta0 $ta1) >>
+      | IDENT "Progress"; ta = tactic_atom -> <:ast< (PROGRESS $ta) >>
       |	st = simple_tactic -> st
       |	tca = tactic_arg -> tca ] ]
   ;
@@ -354,6 +363,8 @@ GEXTEND Gram
       | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
       |	IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
         <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
+      | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
+        <:ast< (CONTEXT $id $c) >>
       |	"'"; c = constrarg -> c ] ]
   ;
   simple_tactic:
@@ -447,7 +458,7 @@ GEXTEND Gram
       | IDENT "LetTac"; s = identarg; ":="; c = constrarg; p = clause_pattern->
 	  <:ast< (LetTac $s $c $p) >>
       | IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
-      | IDENT "Clear"; l = ne_identarg_list -> 
+      | IDENT "Clear"; l = ne_idmeta_arg_list -> 
                 <:ast< (Clear (CLAUSE ($LIST $l))) >>
       | IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg -> 
                 <:ast< (MoveDep $id1 $id2) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 7cbc4d5d7..ff103ae2c 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -292,6 +292,7 @@ module Tactic =
     let constrarg_list = gec_list "constrarg_list"
     let ident_or_constrarg = gec "ident_or_constrarg"
     let identarg = gec "identarg"
+    let idmeta_arg = gec "idmeta_arg"
     let qualidarg = gec "qualidarg"
     let qualidconstarg = gec "qualidconstarg"
     let input_fun = gec "input_fun"
@@ -306,6 +307,7 @@ module Tactic =
     let match_rule = gec "match_rule"
     let match_list = gec_list "match_list"
     let ne_identarg_list = gec_list "ne_identarg_list"
+    let ne_idmeta_arg_list = gec_list "ne_idmeta_arg_list"
     let ne_qualidarg_list = gec_list "ne_qualidarg_list"
     let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
     let ne_pattern_list = gec_list "ne_pattern_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fda1c94cb..30773eaa6 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -116,6 +116,7 @@ module Tactic :
     val fixdecl : Coqast.t list Gram.Entry.e
     val ident_or_constrarg : Coqast.t Gram.Entry.e
     val identarg : Coqast.t Gram.Entry.e
+    val idmeta_arg : Coqast.t Gram.Entry.e
     val qualidarg : Coqast.t Gram.Entry.e
     val qualidconstarg : Coqast.t Gram.Entry.e
     val input_fun : Coqast.t Gram.Entry.e
@@ -131,6 +132,7 @@ module Tactic :
     val match_rule : Coqast.t Gram.Entry.e
     val match_list : Coqast.t list Gram.Entry.e
     val ne_identarg_list : Coqast.t list Gram.Entry.e
+    val ne_idmeta_arg_list : Coqast.t list Gram.Entry.e
     val ne_qualidarg_list : Coqast.t list Gram.Entry.e
     val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
     val ne_intropattern : Coqast.t Gram.Entry.e
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 6730419a9..6b0078b4c 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -443,7 +443,7 @@ let rec make_subs_list = function
   | [] -> []
 
 (* Debug reference *)
-let debug =ref DebugOff
+let debug = ref DebugOff
 
 (* Sets the debugger mode *)
 let set_debug pos = debug := pos
@@ -479,6 +479,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
     | Node(_,"IDTAC",[]) -> VTactic tclIDTAC
     | Node(_,"FAIL",[]) -> VTactic (tclFAIL 0)
     | Node(_,"FAIL",[n]) -> VTactic (tclFAIL (num_of_ast n))
+    | Node(_,"PROGRESS",[tac]) ->
+      VTactic (tclPROGRESS (tac_interp lfun lmatch debug tac))
     | Node(_,"TACTICLIST",l) ->
       VTactic (interp_semi_list tclIDTAC lfun lmatch debug l)
     | Node(_,"DO",[n;tac]) ->
@@ -512,6 +514,11 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
        with | Not_found ->
          (try (vcontext_interp (evc,env,lfun,lmatch,goalopt,debug) (lookup s))
           with | Not_found -> VArg (Identifier (id_of_string s))))
+    | Node(loc,"METAID",[Num(_,n)]) ->
+      (try VArg (Identifier (destVar (List.assoc n lmatch))) with
+       | Invalid_argument "destVar" ->
+         user_err_loc (loc, "Tacinterp.val_interp",[<'sTR
+          "Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))
     | Str(_,s) -> VArg (Quoted_string s)
     | Num(_,n) -> VArg (Integer n)
     | Node(_,"COMMAND",[c]) ->