Ajout d'une entrée hyp de type HypArgType pour parser et interpréter les noms d'hypothèses; Changement de natural en int_or_var pour 'do' et 'fail'

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

2 files changed, 26 insertions, 12 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 3f3f8c4d28..9f1bf17f5a 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -806,7 +806,8 @@ and xlate_tactic =
    | TacFirst(t1::l)-> CT_first(xlate_tactic t1, List.map xlate_tactic l)
    | TacSolve([]) -> assert false
    | TacSolve(t1::l)-> CT_tacsolve(xlate_tactic t1, List.map xlate_tactic l)
-   | TacDo(n, t) -> CT_do(CT_int n, xlate_tactic t)
+   | TacDo(ArgArg n, t) -> CT_do(CT_int n, xlate_tactic t)
+   | TacDo(ArgVar _, t) -> xlate_error "Parametric tacticals 'do'"
    | TacTry t -> CT_try (xlate_tactic t)
    | TacRepeat t -> CT_repeat(xlate_tactic t)
    | TacAbstract(t,id_opt) -> 
@@ -873,8 +874,9 @@ 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, ctf_STRING_OPT_NONE)
-   | TacFail (n,s) -> CT_fail(CT_int n, ctf_STRING_OPT_SOME (CT_string s))
+   | TacFail (ArgArg n,"") -> CT_fail(CT_int n, ctf_STRING_OPT_NONE)
+   | TacFail (ArgArg n,s) -> CT_fail(CT_int n, ctf_STRING_OPT_SOME (CT_string s))
+   | TacFail (ArgVar _, _) -> xlate_error "Parametric tacticals 'fail'"
    | 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)
@@ -1232,6 +1234,8 @@ and coerce_genarg_to_TARG x =
 	CT_coerce_FORMULA_OR_INT_to_TARG
 	  (CT_coerce_ID_OR_INT_to_FORMULA_OR_INT
 	     (CT_coerce_ID_to_ID_OR_INT id))
+  | HypArgType ->
+      xlate_error "TODO (similar to IdentArgType)"
   | RefArgType ->
       let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
 	CT_coerce_FORMULA_OR_INT_to_TARG
@@ -1324,6 +1328,8 @@ let coerce_genarg_to_VARG x =
       CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
 	        (CT_coerce_ID_to_ID_OPT id))
+  | HypArgType ->
+      xlate_error "TODO (similar to IdentArgType)"
   | RefArgType ->
       let id = tac_qualid_to_ct_ID (out_gen rawwit_ref x) in
       CT_coerce_ID_OPT_OR_ALL_to_VARG
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4a08804c5a..14482cb7a1 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -764,7 +764,8 @@ and intern_tactic_seq ist = function
       ist.ltacvars, TacMatchContext(lr, intern_match_rule ist lmr)
   | TacMatch (c,lmr) ->
       ist.ltacvars, TacMatch (intern_tactic ist c,intern_match_rule ist lmr)
-  | TacId _ | TacFail _ as x -> ist.ltacvars, x
+  | TacId _ as x -> ist.ltacvars, x
+  | TacFail (n,x) -> ist.ltacvars, TacFail (intern_int_or_var ist n,x)
   | TacProgress tac -> ist.ltacvars, TacProgress (intern_tactic ist tac)
   | TacAbstract (tac,s) -> ist.ltacvars, TacAbstract (intern_tactic ist tac,s)
   | TacThen (t1,t2) ->
@@ -776,7 +777,8 @@ and intern_tactic_seq ist = function
       (* Que faire en cas de (tac complexe avec Match et Thens; tac2) ?? *)
       lfun',
       TacThens (t, List.map (intern_tactic { ist with ltacvars = lfun' }) tl)
-  | TacDo (n,tac) -> ist.ltacvars, TacDo (n,intern_tactic ist tac)
+  | TacDo (n,tac) -> 
+      ist.ltacvars, TacDo (intern_int_or_var ist n,intern_tactic ist tac)
   | TacTry tac -> ist.ltacvars, TacTry (intern_tactic ist tac)
   | TacInfo tac -> ist.ltacvars, TacInfo (intern_tactic ist tac)
   | TacRepeat tac -> ist.ltacvars, TacRepeat (intern_tactic ist tac)
@@ -847,7 +849,10 @@ and intern_genarg ist x =
       in_gen globwit_intro_pattern
         (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
   | IdentArgType ->
-      in_gen globwit_ident (snd (intern_hyp ist (dummy_loc,out_gen rawwit_ident x)))
+      let lf = ref ([],[]) in
+      in_gen globwit_ident(intern_ident lf ist (out_gen rawwit_ident x))
+  | HypArgType ->
+      in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
   | RefArgType ->
       in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
   | SortArgType ->
@@ -1324,13 +1329,13 @@ and eval_tactic ist = function
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
   | TacId s -> tclIDTAC_MESSAGE s
-  | TacFail (n,s) -> tclFAIL n s
+  | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
   | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
   | TacThens (t,tl) ->
       tclTHENS (interp_tactic ist t) (List.map (interp_tactic ist) tl)
-  | TacDo (n,tac) -> tclDO n (interp_tactic ist tac)
+  | TacDo (n,tac) -> tclDO (interp_int_or_var ist n) (interp_tactic ist tac)
   | TacTry tac -> tclTRY (interp_tactic ist tac)
   | TacInfo tac -> tclINFO (interp_tactic ist tac)
   | TacRepeat tac -> tclREPEAT (interp_tactic ist tac)
@@ -1572,6 +1577,8 @@ and interp_genarg ist goal x =
         (interp_intro_pattern ist (out_gen globwit_intro_pattern x))
   | IdentArgType ->
       in_gen wit_ident (interp_ident ist (out_gen globwit_ident x))
+  | HypArgType ->
+      in_gen wit_var (mkVar (interp_hyp ist goal (out_gen globwit_var x)))
   | RefArgType ->
       in_gen wit_ref (pf_interp_reference ist goal (out_gen globwit_ref x))
   | SortArgType ->
@@ -1778,13 +1785,13 @@ and interp_atomic ist gl = function
     | IntOrVarArgType -> 
 	VInteger (interp_int_or_var ist (out_gen globwit_int_or_var x))
     | PreIdentArgType ->
-        VIntroPattern
-	  (IntroIdentifier (id_of_string (out_gen globwit_pre_ident x)))
+	failwith "pre-identifiers cannot be bound"
     | IntroPatternArgType ->
 	VIntroPattern (out_gen globwit_intro_pattern x)
     | IdentArgType -> 
-	VConstr 
-	  (mkVar (interp_hyp ist gl (dummy_loc,out_gen globwit_ident x)))
+        VIntroPattern (IntroIdentifier (out_gen globwit_ident x))
+    | HypArgType ->
+	VConstr (mkVar (interp_var ist gl (out_gen globwit_var x)))
     | RefArgType -> 
         VConstr (constr_of_reference 
           (pf_interp_reference ist gl (out_gen globwit_ref x)))
@@ -2069,6 +2076,7 @@ and subst_genarg subst (x:glob_generic_argument) =
   | IntroPatternArgType ->
       in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
   | IdentArgType -> in_gen globwit_ident (out_gen globwit_ident x)
+  | HypArgType -> in_gen globwit_var (out_gen globwit_var x)
   | RefArgType ->
       in_gen globwit_ref (subst_global_reference subst 
 	(out_gen globwit_ref x))