correcting the treatment of many tactics that use quant_hyp in file xlate.ml

and associated file.  Also adding a systematic check approach


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

4 files changed, 88 insertions, 45 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index a1f6e2489..790ffb4b3 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -267,6 +267,10 @@ and ct_ID_OPT_OR_ALL =
 and ct_ID_OR_INT =
     CT_coerce_ID_to_ID_OR_INT of ct_ID
   | CT_coerce_INT_to_ID_OR_INT of ct_INT
+and ct_ID_OR_INT_OPT =
+    CT_coerce_ID_OPT_to_ID_OR_INT_OPT of ct_ID_OPT
+  | CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT of ct_ID_OR_INT
+  | CT_coerce_INT_OPT_to_ID_OR_INT_OPT of ct_INT_OPT
 and ct_ID_OR_STRING =
     CT_coerce_ID_to_ID_OR_STRING of ct_ID
   | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING
@@ -443,16 +447,16 @@ and ct_TACTIC_COM =
   | CT_cutrewrite_rl of ct_FORMULA * ct_ID_OPT
   | CT_dconcl
   | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA
-  | CT_depinversion of ct_INV_TYPE * ct_ID * ct_FORMULA_OPT
+  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_FORMULA_OPT
   | CT_deprewrite_lr of ct_ID
   | CT_deprewrite_rl of ct_ID
   | CT_destruct of ct_ID_OR_INT
   | CT_dhyp of ct_ID
-  | CT_discriminate_eq of ct_ID_OPT
+  | CT_discriminate_eq of ct_ID_OR_INT_OPT
   | CT_do of ct_INT * ct_TACTIC_COM
   | CT_eapply of ct_FORMULA * ct_SPEC_LIST
-  | CT_eauto of ct_INT_OPT
-  | CT_eauto_with of ct_INT_OPT * ct_ID_NE_LIST_OR_STAR
+  | CT_eauto of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT
+  | CT_eauto_with of ct_ID_OR_INT_OPT * ct_ID_OR_INT_OPT * ct_ID_NE_LIST_OR_STAR
   | CT_elim of ct_FORMULA * ct_SPEC_LIST * ct_USING
   | CT_elim_type of ct_FORMULA
   | CT_exact of ct_FORMULA
@@ -465,12 +469,12 @@ and ct_TACTIC_COM =
   | CT_idtac
   | CT_induction of ct_ID_OR_INT
   | CT_info of ct_TACTIC_COM
-  | CT_injection_eq of ct_ID_OPT
+  | CT_injection_eq of ct_ID_OR_INT_OPT
   | CT_intro of ct_ID_OPT
   | CT_intro_after of ct_ID_OPT * ct_ID
   | CT_intros of ct_INTRO_PATT_LIST
   | CT_intros_until of ct_ID
-  | CT_inversion of ct_INV_TYPE * ct_ID * ct_ID_LIST
+  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_lettac of ct_LET_CLAUSES * ct_LET_VALUE
   | CT_match_context of ct_CONTEXT_RULE * ct_CONTEXT_RULE list
@@ -504,7 +508,7 @@ and ct_TACTIC_COM =
   | CT_trivial_with of ct_ID_NE_LIST_OR_STAR
   | CT_try of ct_TACTIC_COM
   | CT_use of ct_FORMULA
-  | CT_use_inversion of ct_ID * ct_FORMULA * ct_ID_LIST
+  | CT_use_inversion of ct_ID_OR_INT * ct_FORMULA * ct_ID_LIST
   | CT_user_tac of ct_ID * ct_TARG_LIST
 and ct_TACTIC_OPT =
     CT_coerce_NONE_to_TACTIC_OPT of ct_NONE
@@ -563,8 +567,8 @@ and ct_VARG =
   | CT_coerce_FORMULA_LIST_to_VARG of ct_FORMULA_LIST
   | CT_coerce_FORMULA_OPT_to_VARG of ct_FORMULA_OPT
   | CT_coerce_ID_OPT_OR_ALL_to_VARG of ct_ID_OPT_OR_ALL
+  | CT_coerce_ID_OR_INT_OPT_to_VARG of ct_ID_OR_INT_OPT
   | CT_coerce_INT_LIST_to_VARG of ct_INT_LIST
-  | CT_coerce_INT_OPT_to_VARG of ct_INT_OPT
   | CT_coerce_STRING_OPT_to_VARG of ct_STRING_OPT
   | CT_coerce_TACTIC_OPT_to_VARG of ct_TACTIC_OPT
   | CT_coerce_VARG_LIST_to_VARG of ct_VARG_LIST
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 79375cf2b..b35a5f56f 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -177,7 +177,7 @@ let constant_to_ast_list kn =
       None -> 
 	make_variable_ast (id_of_label (label kn)) typ l
     | Some c1 ->
-	make_definition_ast (id_of_label (label kn)) c1 typ l)
+	make_definition_ast (id_of_label (label kn)) (Lazy.force_val c1) typ l)
 
 let variable_to_ast_list sp =
   let ((id, c, v), _) = get_variable sp in
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index e2f519504..219584113 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -663,6 +663,10 @@ and fID_OPT_OR_ALL = function
 and fID_OR_INT = function
 | CT_coerce_ID_to_ID_OR_INT x -> fID x
 | CT_coerce_INT_to_ID_OR_INT x -> fINT x
+and fID_OR_INT_OPT = function
+| CT_coerce_ID_OPT_to_ID_OR_INT_OPT x -> fID_OPT x
+| CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT x -> fID_OR_INT x
+| CT_coerce_INT_OPT_to_ID_OR_INT_OPT x -> fINT_OPT x
 and fID_OR_STRING = function
 | CT_coerce_ID_to_ID_OR_STRING x -> fID x
 | CT_coerce_STRING_to_ID_OR_STRING x -> fSTRING x
@@ -1019,7 +1023,7 @@ and fTACTIC_COM = function
    fNODE "decompose_list" 2
 | CT_depinversion(x1, x2, x3) ->
    fINV_TYPE x1;
-   fID x2;
+   fID_OR_INT x2;
    fFORMULA_OPT x3;
    fNODE "depinversion" 3
 | CT_deprewrite_lr(x1) ->
@@ -1035,7 +1039,7 @@ and fTACTIC_COM = function
    fID x1;
    fNODE "dhyp" 1
 | CT_discriminate_eq(x1) ->
-   fID_OPT x1;
+   fID_OR_INT_OPT x1;
    fNODE "discriminate_eq" 1
 | CT_do(x1, x2) ->
    fINT x1;
@@ -1045,13 +1049,15 @@ and fTACTIC_COM = function
    fFORMULA x1;
    fSPEC_LIST x2;
    fNODE "eapply" 2
-| CT_eauto(x1) ->
-   fINT_OPT x1;
-   fNODE "eauto" 1
-| CT_eauto_with(x1, x2) ->
-   fINT_OPT x1;
-   fID_NE_LIST_OR_STAR x2;
-   fNODE "eauto_with" 2
+| CT_eauto(x1, x2) ->
+   fID_OR_INT_OPT x1;
+   fID_OR_INT_OPT x2;
+   fNODE "eauto" 2
+| CT_eauto_with(x1, x2, x3) ->
+   fID_OR_INT_OPT x1;
+   fID_OR_INT_OPT x2;
+   fID_NE_LIST_OR_STAR x3;
+   fNODE "eauto_with" 3
 | CT_elim(x1, x2, x3) ->
    fFORMULA x1;
    fSPEC_LIST x2;
@@ -1092,7 +1098,7 @@ and fTACTIC_COM = function
    fTACTIC_COM x1;
    fNODE "info" 1
 | CT_injection_eq(x1) ->
-   fID_OPT x1;
+   fID_OR_INT_OPT x1;
    fNODE "injection_eq" 1
 | CT_intro(x1) ->
    fID_OPT x1;
@@ -1109,7 +1115,7 @@ and fTACTIC_COM = function
    fNODE "intros_until" 1
 | CT_inversion(x1, x2, x3) ->
    fINV_TYPE x1;
-   fID x2;
+   fID_OR_INT x2;
    fID_LIST x3;
    fNODE "inversion" 3
 | CT_left(x1) ->
@@ -1228,7 +1234,7 @@ and fTACTIC_COM = function
    fFORMULA x1;
    fNODE "use" 1
 | CT_use_inversion(x1, x2, x3) ->
-   fID x1;
+   fID_OR_INT x1;
    fFORMULA x2;
    fID_LIST x3;
    fNODE "use_inversion" 3
@@ -1327,8 +1333,8 @@ and fVAR = function
 | CT_coerce_FORMULA_LIST_to_VARG x -> fFORMULA_LIST x
 | CT_coerce_FORMULA_OPT_to_VARG x -> fFORMULA_OPT x
 | CT_coerce_ID_OPT_OR_ALL_to_VARG x -> fID_OPT_OR_ALL x
+| CT_coerce_ID_OR_INT_OPT_to_VARG x -> fID_OR_INT_OPT x
 | CT_coerce_INT_LIST_to_VARG x -> fINT_LIST x
-| CT_coerce_INT_OPT_to_VARG x -> fINT_OPT x
 | CT_coerce_STRING_OPT_to_VARG x -> fSTRING_OPT x
 | CT_coerce_TACTIC_OPT_to_VARG x -> fTACTIC_OPT x
 | CT_coerce_VARG_LIST_to_VARG x -> fVARG_LIST x
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 700fa0f7c..4e4b51833 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -203,6 +203,18 @@ let xlate_int =
     | Num (_, n) -> CT_int n
     | _ -> xlate_error "xlate_int: not an int";;
 
+let xlate_id_to_id_or_int_opt s =
+   CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+     (CT_coerce_ID_to_ID_OPT (CT_ident (string_of_id s)));;
+
+let xlate_int_to_id_or_int_opt n =
+   CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+     (CT_coerce_INT_to_ID_OR_INT (CT_int n));;
+
+let none_in_id_or_int_opt =
+  CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+    (CT_coerce_NONE_to_ID_OPT(CT_none));;
+
 let xlate_int_opt = function
   | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n)
   | None ->  CT_coerce_NONE_to_INT_OPT CT_none
@@ -846,6 +858,12 @@ let xlate_quantified_hypothesis = function
   | AnonHyp n -> CT_coerce_INT_to_ID_OR_INT (CT_int n)
   | NamedHyp id -> CT_coerce_ID_to_ID_OR_INT (xlate_ident id)
 
+let xlate_quantified_hypothesis_opt = function
+  | None -> 
+      CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE
+  | Some (AnonHyp n) -> xlate_int_to_id_or_int_opt n
+  | Some (NamedHyp id) -> xlate_id_to_id_or_int_opt id;;
+
 let xlate_explicit_binding (h,c) = 
   CT_binding (xlate_quantified_hypothesis h, xlate_constr c)
 
@@ -1094,13 +1112,15 @@ and xlate_tac =
     | TacDoubleInduction _ -> xlate_error "TODO: Double Induction id1 id2"
     | TacExtend ("Discriminate", [idopt]) ->
      CT_discriminate_eq
-         (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+         (xlate_quantified_hypothesis_opt
+	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
     | TacExtend ("DEq", [idopt]) ->
      CT_simplify_eq
          (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
     | TacExtend ("Injection", [idopt]) ->
      CT_injection_eq
-         (xlate_ident_opt (out_gen (wit_opt rawwit_ident) idopt))
+         (xlate_quantified_hypothesis_opt
+	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
     | TacFix (idopt, n) ->
      CT_fixtactic (xlate_ident_opt idopt, CT_int n, CT_fix_tac_list [])
     | TacMutualFix (id, n, fixtac_list) ->
@@ -1205,15 +1225,26 @@ and xlate_tac =
              CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR(
              CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl)))
     | TacExtend ("EAuto", [nopt; popt; idl]) ->
-	let control =
-	match out_gen (wit_opt rawwit_int_or_var) nopt with
-	  | Some breadth -> Some (true, breadth)
-	  | None ->
-	match out_gen (wit_opt rawwit_int_or_var) popt with
-	  | Some depth -> Some (false, depth)
-	  | None -> None in
-	let idl = out_gen (wit_opt (wit_list0 rawwit_string)) idl in
-	xlate_error "TODO: EAuto n p"
+	let first_n =
+	  match out_gen (wit_opt rawwit_int_or_var) nopt with
+	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
+	    | Some ArgArg n -> xlate_int_to_id_or_int_opt n
+	    | None -> none_in_id_or_int_opt in
+	let second_n =
+	  match out_gen (wit_opt rawwit_int_or_var) popt with
+	    | Some (ArgVar(_, s)) -> xlate_id_to_id_or_int_opt s
+	    | Some ArgArg n -> xlate_int_to_id_or_int_opt n
+	    | None -> none_in_id_or_int_opt in
+	let idl = out_gen Eauto.rawwit_hintbases idl in
+          (match idl with
+	    None -> CT_eauto_with(first_n, second_n, CT_star)
+	  | Some [] -> CT_eauto(first_n, second_n)
+	  | Some (a::l) -> 
+	      CT_eauto_with(first_n, second_n,
+			    CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR
+			      (CT_id_ne_list
+				 (CT_ident a,
+				  List.map (fun x -> CT_ident x) l))))
     | TacExtend ("Prolog", [cl; n]) ->
       let cl = List.map xlate_constr (out_gen (wit_list0 rawwit_constr) cl) in
       (match out_gen wit_int_or_var n with
@@ -1272,15 +1303,13 @@ and xlate_tac =
        CT_clear (CT_id_ne_list (ident_or_meta_to_ct_ID id, idl'))
     | (*For translating tactics/Inv.v *)
       TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s, [id]) ->
-	let quant_hyp =  (out_gen rawwit_quant_hyp id) in
-	  (match quant_hyp with
-	       NamedHyp id1 -> 	let id = xlate_ident id1  in
-		 CT_inversion (compute_INV_TYPE_from_string s, id, CT_id_list [])
-	     | AnonHyp _ -> assert false)
+	let quant_hyp =  out_gen rawwit_quant_hyp id in
+	  CT_inversion(compute_INV_TYPE_from_string s,
+		       xlate_quantified_hypothesis quant_hyp, CT_id_list [])
     | TacExtend ("SimpleInversion"|"Inversion"|"InversionClear" as s,
         [id;copt_or_idl]) ->
-(* TODO: rawwit_ident should be rawwit_quant_hyp *)
-	let id = xlate_ident (out_gen rawwit_ident id) in
+	let quant_hyp = (out_gen rawwit_quant_hyp id) in
+	let id = xlate_quantified_hypothesis quant_hyp in
 	(match genarg_tag copt_or_idl with
 	  | List1ArgType IdentArgType -> (* InvIn *)
 	      let idl = out_gen (wit_list1 rawwit_ident) copt_or_idl in
@@ -1292,11 +1321,11 @@ and xlate_tac =
 		(compute_INV_TYPE_from_string s, id, xlate_constr_opt copt)
 	  | _ -> xlate_error "")
     | TacExtend ("InversionUsing", [id; c]) ->
-     let id = xlate_ident (out_gen rawwit_ident id) in
+     let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in
      let c = out_gen rawwit_constr c in
      CT_use_inversion (id, xlate_constr c, CT_id_list [])
     | TacExtend ("InversionUsing", [id; c; idlist]) ->
-     let id = xlate_ident (out_gen rawwit_ident id) in
+     let id = xlate_quantified_hypothesis (out_gen rawwit_quant_hyp id) in
      let c = out_gen rawwit_constr c in
      let idlist = out_gen (wit_list1 rawwit_ident) idlist in
      CT_use_inversion (id, xlate_constr c,
@@ -1385,11 +1414,15 @@ let coerce_genarg_to_VARG x =
   | BoolArgType -> xlate_error "TODO: generic boolean argument"
   | IntArgType ->
       let n = out_gen rawwit_int x in
-      CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n))
+      CT_coerce_ID_OR_INT_OPT_to_VARG
+	(CT_coerce_INT_OPT_to_ID_OR_INT_OPT
+	   (CT_coerce_INT_to_INT_OPT (CT_int n)))
   | IntOrVarArgType ->
       (match out_gen rawwit_int_or_var x with
 	| ArgArg n -> 
-	    CT_coerce_INT_OPT_to_VARG (CT_coerce_INT_to_INT_OPT (CT_int n))
+      CT_coerce_ID_OR_INT_OPT_to_VARG
+	(CT_coerce_INT_OPT_to_ID_OR_INT_OPT
+	   (CT_coerce_INT_to_INT_OPT (CT_int n)))
 	| ArgVar (_,id) ->
 	    CT_coerce_ID_OPT_OR_ALL_to_VARG
 	      (CT_coerce_ID_OPT_to_ID_OPT_OR_ALL
@@ -1626,7 +1659,7 @@ let xlate_vernac =
     | VernacFocus nopt -> CT_focus (xlate_int_opt nopt)
     | VernacUnfocus -> CT_unfocus
   | VernacExtend ("HintRewrite", orient :: formula_list :: base :: t) ->
-      let orient = out_gen rawwit_bool orient in
+      let orient = out_gen Extraargs.rawwit_orient orient in
       let formula_list = out_gen (wit_list1 (rawwit_constr)) formula_list in
       let base = out_gen rawwit_pre_ident base in
       let t = match t with