handles explicit function calls, names meta variables in patterns

(in V8 the name is not a number), explicitation of arguments with names
(but not with rank anymore), the refine tactic now has its own operator
the structure information for hypotheses in induction is now handled
as in intro, the tactic instantiate has been modified to use clauses,
the wildcard rule for Ltac pattern matching on goals has been added
and the possibility to refer to types of values and instantiated contexts
in values in Ltac have been added.


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

3 files changed, 60 insertions, 31 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 3b45f86a5..829972ecf 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -173,6 +173,7 @@ and ct_CONTEXT_PATTERN =
   | CT_context of ct_ID_OPT * ct_FORMULA
 and ct_CONTEXT_RULE =
     CT_context_rule of ct_CONTEXT_HYP_LIST * ct_CONTEXT_PATTERN * ct_TACTIC_COM
+  | CT_def_context_rule of ct_TACTIC_COM
 and ct_CONVERSION_FLAG =
     CT_beta
   | CT_delta
@@ -196,6 +197,7 @@ and ct_DEFN_OR_THM =
 and ct_DEF_BODY =
     CT_coerce_CONTEXT_PATTERN_to_DEF_BODY of ct_CONTEXT_PATTERN
   | CT_coerce_EVAL_CMD_to_DEF_BODY of ct_EVAL_CMD
+  | CT_type_of of ct_FORMULA
 and ct_DEF_BODY_OPT =
     CT_coerce_DEF_BODY_to_DEF_BODY_OPT of ct_DEF_BODY
   | CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT of ct_FORMULA_OPT
@@ -231,7 +233,7 @@ and ct_FORMULA =
   | CT_coerce_TYPED_FORMULA_to_FORMULA of ct_TYPED_FORMULA
   | CT_appc of ct_FORMULA * ct_FORMULA_NE_LIST
   | CT_arrowc of ct_FORMULA * ct_FORMULA
-  | CT_bang of ct_INT_OPT * ct_FORMULA
+  | CT_bang of ct_FORMULA
   | CT_cases of ct_MATCHED_FORMULA_NE_LIST * ct_FORMULA_OPT * ct_EQN_LIST
   | CT_cofixc of ct_ID * ct_COFIX_REC_LIST
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
@@ -239,6 +241,7 @@ and ct_FORMULA =
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
   | CT_if of ct_FORMULA * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
+  | CT_labelled_arg of ct_ID * ct_FORMULA
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
   | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
@@ -538,7 +541,7 @@ and ct_TACTIC_COM =
   | CT_induction of ct_ID_OR_INT
   | CT_info of ct_TACTIC_COM
   | CT_injection_eq of ct_ID_OR_INT_OPT
-  | CT_instantiate of ct_INT * ct_FORMULA
+  | CT_instantiate of ct_INT * ct_FORMULA * ct_CLAUSE
   | CT_intro of ct_ID_OPT
   | CT_intro_after of ct_ID_OPT * ct_ID
   | CT_intros of ct_INTRO_PATT_LIST
@@ -552,7 +555,7 @@ and ct_TACTIC_COM =
   | CT_match_tac of ct_TACTIC_COM * ct_MATCH_TAC_RULES
   | CT_move_after of ct_ID * ct_ID
   | CT_new_destruct of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
-  | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_ID_LIST_LIST
+  | CT_new_induction of ct_FORMULA_OR_INT * ct_USING * ct_INTRO_PATT_LIST
   | CT_omega
   | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM
   | CT_parallel of ct_TACTIC_COM * ct_TACTIC_COM list
@@ -561,6 +564,7 @@ and ct_TACTIC_COM =
   | CT_prolog of ct_FORMULA_LIST * ct_INT
   | CT_rec_tactic_in of ct_REC_TACTIC_FUN_LIST * ct_TACTIC_COM
   | CT_reduce of ct_RED_COM * ct_CLAUSE
+  | CT_refine of ct_FORMULA
   | CT_reflexivity
   | CT_rename of ct_ID * ct_ID
   | CT_repeat of ct_TACTIC_COM
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index f04c4beaf..eeb09b2a9 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -477,6 +477,9 @@ and fCONTEXT_RULE = function
    fCONTEXT_PATTERN x2;
    fTACTIC_COM x3;
    fNODE "context_rule" 3
+| CT_def_context_rule(x1) ->
+   fTACTIC_COM x1;
+   fNODE "def_context_rule" 1
 and fCONVERSION_FLAG = function
 | CT_beta -> fNODE "beta" 0
 | CT_delta -> fNODE "delta" 0
@@ -511,6 +514,9 @@ and fDEFN = function
 and fDEF_BODY = function
 | CT_coerce_CONTEXT_PATTERN_to_DEF_BODY x -> fCONTEXT_PATTERN x
 | CT_coerce_EVAL_CMD_to_DEF_BODY x -> fEVAL_CMD x
+| CT_type_of(x1) ->
+   fFORMULA x1;
+   fNODE "type_of" 1
 and fDEF_BODY_OPT = function
 | CT_coerce_DEF_BODY_to_DEF_BODY_OPT x -> fDEF_BODY x
 | CT_coerce_FORMULA_OPT_to_DEF_BODY_OPT x -> fFORMULA_OPT x
@@ -585,10 +591,9 @@ and fFORMULA = function
    fFORMULA x1;
    fFORMULA x2;
    fNODE "arrowc" 2
-| CT_bang(x1, x2) ->
-   fINT_OPT x1;
-   fFORMULA x2;
-   fNODE "bang" 2
+| CT_bang(x1) ->
+   fFORMULA x1;
+   fNODE "bang" 1
 | CT_cases(x1, x2, x3) ->
    fMATCHED_FORMULA_NE_LIST x1;
    fFORMULA_OPT x2;
@@ -622,6 +627,10 @@ and fFORMULA = function
    fFORMULA x3;
    fFORMULA x4;
    fNODE "inductive_let" 4
+| CT_labelled_arg(x1, x2) ->
+   fID x1;
+   fFORMULA x2;
+   fNODE "labelled_arg" 2
 | CT_lambdac(x1, x2) ->
    fBINDER_NE_LIST x1;
    fFORMULA x2;
@@ -1267,10 +1276,11 @@ and fTACTIC_COM = function
 | CT_injection_eq(x1) ->
    fID_OR_INT_OPT x1;
    fNODE "injection_eq" 1
-| CT_instantiate(x1, x2) ->
+| CT_instantiate(x1, x2, x3) ->
    fINT x1;
    fFORMULA x2;
-   fNODE "instantiate" 2
+   fCLAUSE x3;
+   fNODE "instantiate" 3
 | CT_intro(x1) ->
    fID_OPT x1;
    fNODE "intro" 1
@@ -1325,7 +1335,7 @@ and fTACTIC_COM = function
 | CT_new_induction(x1, x2, x3) ->
    fFORMULA_OR_INT x1;
    fUSING x2;
-   fID_LIST_LIST x3;
+   fINTRO_PATT_LIST x3;
    fNODE "new_induction" 3
 | CT_omega -> fNODE "omega" 0
 | CT_orelse(x1, x2) ->
@@ -1355,6 +1365,9 @@ and fTACTIC_COM = function
    fRED_COM x1;
    fCLAUSE x2;
    fNODE "reduce" 2
+| CT_refine(x1) ->
+   fFORMULA x1;
+   fNODE "refine" 1
 | CT_reflexivity -> fNODE "reflexivity" 0
 | CT_rename(x1, x2) ->
    fID x1;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index a11d75d4d..2d6cca540 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -348,10 +348,10 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
        let l', last = decompose_last l in
 	 CT_proj(xlate_formula last,
 		 CT_formula_ne_list
-		   (CT_bang(xlate_int_opt None, varc (xlate_reference r)),
+		   (CT_bang(varc (xlate_reference r)),
 		    List.map xlate_formula l'))
    | CAppExpl(_, (None, r), l) -> 
-       CT_appc(CT_bang(xlate_int_opt None, varc (xlate_reference r)),
+       CT_appc(CT_bang(varc (xlate_reference r)),
 	       xlate_formula_ne_list l)
    | CApp(_, (Some n,f), l) -> 
        let l', last = decompose_last l in
@@ -407,8 +407,11 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
 	 (CT_typed_formula(xlate_formula e, xlate_formula t))
    | CPatVar (_, (_,i)) when is_int_meta i ->
        CT_coerce_ID_to_FORMULA(CT_metac (CT_int (int_of_meta i)))
-   | CPatVar (_, _) -> xlate_error "TODO: meta as ident"
-   | CEvar (_, _) -> xlate_error "TODO: evars"
+   | CPatVar (_, (false, s)) ->
+       CT_coerce_ID_to_FORMULA(CT_metaid (string_of_id s))
+   | CPatVar (_, (true, s)) ->
+       xlate_error "Second order variable not supported"
+   | CEvar (_, _) -> xlate_error "CEvar not supported"
    | CCoFix (_, (_, id), lm::lmi) -> 
      let strip_mutcorec (fid, arf, ardef) =
 	CT_cofix_rec (xlate_ident fid, xlate_formula arf, xlate_formula ardef) in
@@ -445,9 +448,9 @@ and xlate_matched_formula = function
 and xlate_formula_expl = function
     (a, None) -> xlate_formula a
   | (a, Some (_,ExplByPos i)) -> 
-      CT_bang(xlate_int_opt (Some i), xlate_formula a)
+      xlate_error "explicitation of implicit by rank not supported"
   | (a, Some (_,ExplByName i)) ->
-      xlate_error "TODO: explicitation of implicit by name"
+      CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a)
 and xlate_formula_expl_ne_list = function
     [] -> assert false
   | a::l -> CT_formula_ne_list(xlate_formula_expl a, List.map xlate_formula_expl l)
@@ -859,6 +862,9 @@ and xlate_tactic =
 
 and xlate_tac =
   function
+    | TacExtend (_, "refine", [c]) ->
+       CT_refine
+	 (xlate_formula (out_gen rawwit_casted_open_constr c))
     | TacExtend (_,"Absurd",[c]) ->
        CT_absurd (xlate_formula (out_gen rawwit_constr c))
     | TacChange (None, f, b) -> CT_change (xlate_formula f, xlate_clause b)
@@ -908,7 +914,6 @@ and xlate_tac =
     | TacMove (true, id1, id2) ->
 	CT_move_after(xlate_hyp id1, xlate_hyp id2)
     | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
-    | TacIntroPattern [] -> CT_intros (CT_intro_patt_list [])
     | TacIntroPattern patt_list ->
 	CT_intros (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
     | TacIntroMove (Some id, None) ->
@@ -1094,12 +1099,15 @@ and xlate_tac =
 	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
     | TacNewInduction(a,b,(c,_)) ->
 	CT_new_induction
-	  (xlate_int_or_constr a, xlate_using b, 
-	   CT_id_list_list
-	     (List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
-    | TacInstantiate (a, b, _) -> 
-	xlate_error "TODO: Instantiate ... <clause>"
-
+	  (xlate_int_or_constr a, xlate_using b,
+	   (CT_intro_patt_list
+	      (List.map (fun l -> 
+			   CT_conj_pattern
+			     (CT_intro_patt_list
+				(List.map xlate_intro_pattern l))) c)))
+    | TacInstantiate (a, b, cl) -> 
+        CT_instantiate(CT_int a, xlate_formula b,
+		       xlate_clause cl)
     | TacLetTac (na, c, cl) ->
         CT_lettac(xlate_id_opt ((0,0),na), xlate_formula c, 
 		  (* TODO LATER: This should be shared with Unfold,
@@ -1124,7 +1132,7 @@ and xlate_tac =
 		(out_gen (wit_list0 rawwit_constr) arg)))
     | TacExtend (_,id, l) ->
      CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l))
-    | TacAlias _ -> xlate_error "TODO LATER: aliases"
+    | TacAlias _ -> xlate_error "Alias not supported"
 
 and coerce_genarg_to_TARG x =
  match Genarg.genarg_tag x with
@@ -1190,19 +1198,23 @@ and coerce_genarg_to_TARG x =
 and xlate_context_rule =
   function
     | Pat (hyps, concl_pat, tactic) ->
-	CT_context_rule(
-          CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
-	  xlate_context_pattern concl_pat, xlate_tactic tactic)
-    | All te ->
-	xlate_error "TODO: wildcard match_context_rule"
+	CT_context_rule
+	  (CT_context_hyp_list (List.map xlate_match_context_hyps hyps),
+	   xlate_context_pattern concl_pat, xlate_tactic tactic)
+    | All tactic ->
+        CT_def_context_rule (xlate_tactic tactic)
 and formula_to_def_body =
   function
     | ConstrEval (red, f) ->
         CT_coerce_EVAL_CMD_to_DEF_BODY(
 	CT_eval(CT_coerce_NONE_to_INT_OPT CT_none,
                 xlate_red_tactic red, xlate_formula f))
-    | ConstrContext _ -> xlate_error "TODO: Inst"
-    | ConstrTypeOf _ -> xlate_error "TODO: Check"
+    | ConstrContext((_, id), f) ->
+       	CT_coerce_CONTEXT_PATTERN_to_DEF_BODY
+	  (CT_context
+	     (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id id)),
+	      xlate_formula f))
+    | ConstrTypeOf f -> CT_type_of (xlate_formula f)
     | ConstrTerm c -> ct_coerce_FORMULA_to_DEF_BODY(xlate_formula c)
 
 and mk_let_value = function