fixes argument lists for tactic definitions, updates inversion tactics

so that they use intro-pattern-lists like induction and destruct


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

3 files changed, 73 insertions, 52 deletions

diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index bf138b394..0a579b274 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -144,7 +144,7 @@ and ct_COMMAND =
   | CT_solve of ct_INT * ct_TACTIC_COM
   | CT_suspend
   | CT_syntax_macro of ct_ID * ct_FORMULA * ct_INT_OPT
-  | CT_tactic_definition of ct_ID * ct_ID_LIST * ct_TACTIC_COM
+  | CT_tactic_definition of ct_ID * ct_ID_UNIT_LIST * ct_TACTIC_COM
   | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID
   | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT
   | CT_token of ct_STRING
@@ -164,6 +164,7 @@ and ct_COMMENT_S =
     CT_comment_s of ct_COMMENT list
 and ct_CONSTR =
     CT_constr of ct_ID * ct_FORMULA
+  | CT_constr_coercion of ct_ID * ct_FORMULA
 and ct_CONSTR_LIST =
     CT_constr_list of ct_CONSTR list
 and ct_CONTEXT_HYP_LIST =
@@ -315,7 +316,9 @@ and ct_ID_UNIT =
     CT_coerce_ID_to_ID_UNIT of ct_ID
   | CT_unit
 and ct_ID_UNIT_LIST =
-    CT_id_unit_list of ct_ID_UNIT * ct_ID_UNIT list
+    CT_id_unit_list of ct_ID_UNIT list
+and ct_ID_UNIT_NE_LIST =
+    CT_id_unit_ne_list of ct_ID_UNIT * ct_ID_UNIT list
 and ct_IMPEXP =
     CT_export
   | CT_import
@@ -423,12 +426,14 @@ and ct_PREMISE_PATTERN =
 and ct_PROOF_SCRIPT =
     CT_proof_script of ct_COMMAND list
 and ct_RECCONSTR =
-    CT_constr_coercion of ct_ID_OPT * ct_FORMULA
+    CT_defrecconstr of ct_ID_OPT * ct_FORMULA * ct_FORMULA_OPT
+  | CT_defrecconstr_coercion of ct_ID_OPT * ct_FORMULA * ct_FORMULA_OPT
   | CT_recconstr of ct_ID_OPT * ct_FORMULA
+  | CT_recconstr_coercion of ct_ID_OPT * ct_FORMULA
 and ct_RECCONSTR_LIST =
     CT_recconstr_list of ct_RECCONSTR list
 and ct_REC_TACTIC_FUN =
-    CT_rec_tactic_fun of ct_ID * ct_ID_UNIT_LIST * ct_TACTIC_COM
+    CT_rec_tactic_fun of ct_ID * ct_ID_UNIT_NE_LIST * ct_TACTIC_COM
 and ct_REC_TACTIC_FUN_LIST =
     CT_rec_tactic_fun_list of ct_REC_TACTIC_FUN * ct_REC_TACTIC_FUN list
 and ct_RED_COM =
@@ -521,7 +526,7 @@ and ct_TACTIC_COM =
   | CT_decompose_list of ct_ID_NE_LIST * ct_FORMULA
   | CT_decompose_record of ct_FORMULA
   | CT_decompose_sum of ct_FORMULA
-  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_FORMULA_OPT
+  | CT_depinversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_LIST * ct_FORMULA_OPT
   | CT_deprewrite_lr of ct_ID
   | CT_deprewrite_rl of ct_ID
   | CT_destruct of ct_ID_OR_INT
@@ -549,7 +554,7 @@ and ct_TACTIC_COM =
   | CT_intro_after of ct_ID_OPT * ct_ID
   | CT_intros of ct_INTRO_PATT_LIST
   | CT_intros_until of ct_ID_OR_INT
-  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_ID_LIST
+  | CT_inversion of ct_INV_TYPE * ct_ID_OR_INT * ct_INTRO_PATT_LIST * ct_ID_LIST
   | CT_left of ct_SPEC_LIST
   | CT_let_ltac of ct_LET_CLAUSES * ct_LET_VALUE
   | CT_lettac of ct_ID_OPT * ct_FORMULA * ct_CLAUSE
@@ -584,7 +589,7 @@ and ct_TACTIC_COM =
   | CT_symmetry of ct_CLAUSE
   | CT_tac_double of ct_ID_OR_INT * ct_ID_OR_INT
   | CT_tacsolve of ct_TACTIC_COM * ct_TACTIC_COM list
-  | CT_tactic_fun of ct_ID_UNIT_LIST * ct_TACTIC_COM
+  | CT_tactic_fun of ct_ID_UNIT_NE_LIST * ct_TACTIC_COM
   | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list
   | CT_transitivity of ct_FORMULA
   | CT_trivial
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 689ae2216..344d28bed 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -405,7 +405,7 @@ and fCOMMAND = function
    fNODE "syntax_macro" 3
 | CT_tactic_definition(x1, x2, x3) ->
    fID x1;
-   fID_LIST x2;
+   fID_UNIT_LIST x2;
    fTACTIC_COM x3;
    fNODE "tactic_definition" 3
 | CT_test_natural_feature(x1, x2) ->
@@ -457,6 +457,10 @@ and fCONSTR = function
    fID x1;
    fFORMULA x2;
    fNODE "constr" 2
+| CT_constr_coercion(x1, x2) ->
+   fID x1;
+   fFORMULA x2;
+   fNODE "constr_coercion" 2
 and fCONSTR_LIST = function
 | CT_constr_list l ->
    (List.iter fCONSTR l);
@@ -771,10 +775,14 @@ and fID_UNIT = function
 | CT_coerce_ID_to_ID_UNIT x -> fID x
 | CT_unit -> fNODE "unit" 0
 and fID_UNIT_LIST = function
-| CT_id_unit_list(x,l) ->
+| CT_id_unit_list l ->
+   (List.iter fID_UNIT l);
+   fNODE "id_unit_list" (List.length l)
+and fID_UNIT_NE_LIST = function
+| CT_id_unit_ne_list(x,l) ->
    fID_UNIT x;
    (List.iter fID_UNIT l);
-   fNODE "id_unit_list" (1 + (List.length l))
+   fNODE "id_unit_ne_list" (1 + (List.length l))
 and fIMPEXP = function
 | CT_export -> fNODE "export" 0
 | CT_import -> fNODE "import" 0
@@ -972,14 +980,24 @@ and fPROOF_SCRIPT = function
    (List.iter fCOMMAND l);
    fNODE "proof_script" (List.length l)
 and fRECCONSTR = function
-| CT_constr_coercion(x1, x2) ->
+| CT_defrecconstr(x1, x2, x3) ->
    fID_OPT x1;
    fFORMULA x2;
-   fNODE "constr_coercion" 2
+   fFORMULA_OPT x3;
+   fNODE "defrecconstr" 3
+| CT_defrecconstr_coercion(x1, x2, x3) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fFORMULA_OPT x3;
+   fNODE "defrecconstr_coercion" 3
 | CT_recconstr(x1, x2) ->
    fID_OPT x1;
    fFORMULA x2;
    fNODE "recconstr" 2
+| CT_recconstr_coercion(x1, x2) ->
+   fID_OPT x1;
+   fFORMULA x2;
+   fNODE "recconstr_coercion" 2
 and fRECCONSTR_LIST = function
 | CT_recconstr_list l ->
    (List.iter fRECCONSTR l);
@@ -987,7 +1005,7 @@ and fRECCONSTR_LIST = function
 and fREC_TACTIC_FUN = function
 | CT_rec_tactic_fun(x1, x2, x3) ->
    fID x1;
-   fID_UNIT_LIST x2;
+   fID_UNIT_NE_LIST x2;
    fTACTIC_COM x3;
    fNODE "rec_tactic_fun" 3
 and fREC_TACTIC_FUN_LIST = function
@@ -1205,11 +1223,12 @@ and fTACTIC_COM = function
 | CT_decompose_sum(x1) ->
    fFORMULA x1;
    fNODE "decompose_sum" 1
-| CT_depinversion(x1, x2, x3) ->
+| CT_depinversion(x1, x2, x3, x4) ->
    fINV_TYPE x1;
    fID_OR_INT x2;
-   fFORMULA_OPT x3;
-   fNODE "depinversion" 3
+   fINTRO_PATT_LIST x3;
+   fFORMULA_OPT x4;
+   fNODE "depinversion" 4
 | CT_deprewrite_lr(x1) ->
    fID x1;
    fNODE "deprewrite_lr" 1
@@ -1305,11 +1324,12 @@ and fTACTIC_COM = function
 | CT_intros_until(x1) ->
    fID_OR_INT x1;
    fNODE "intros_until" 1
-| CT_inversion(x1, x2, x3) ->
+| CT_inversion(x1, x2, x3, x4) ->
    fINV_TYPE x1;
    fID_OR_INT x2;
-   fID_LIST x3;
-   fNODE "inversion" 3
+   fINTRO_PATT_LIST x3;
+   fID_LIST x4;
+   fNODE "inversion" 4
 | CT_left(x1) ->
    fSPEC_LIST x1;
    fNODE "left" 1
@@ -1440,7 +1460,7 @@ and fTACTIC_COM = function
    (List.iter fTACTIC_COM l);
    fNODE "tacsolve" (1 + (List.length l))
 | CT_tactic_fun(x1, x2) ->
-   fID_UNIT_LIST x1;
+   fID_UNIT_NE_LIST x1;
    fTACTIC_COM x2;
    fNODE "tactic_fun" 2
 | CT_then(x,l) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index b2cb66d66..be3d27d2d 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -628,8 +628,7 @@ let xlate_context_pattern = function
 
 
 let xlate_match_context_hyps = function
-  | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b)
-
+  | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b);;
 
 let xlate_largs_to_id_unit largs =
   match List.map xlate_id_unit largs with
@@ -672,6 +671,13 @@ let xlate_lettac_clauses = function
 	      CT_unfold_list((CT_coerce_ID_to_UNFOLD(CT_ident "Goal"))::res)
 	  | None -> CT_unfold_list res;;
 
+let xlate_intro_patt_list c =
+ CT_intro_patt_list
+   (List.map
+      (fun l -> 
+	 CT_conj_pattern (CT_intro_patt_list (List.map xlate_intro_pattern l)))
+      c);;
+
 let rec (xlate_tacarg:raw_tactic_arg -> ct_TACTIC_ARG) =
   function
     | TacVoid ->
@@ -750,11 +756,11 @@ and xlate_rec_tac = function
   | ((_,x),TacFun (argl,tac)) ->
       let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
 	CT_rec_tactic_fun(xlate_ident x,
-			  CT_id_unit_list(fst, rest),
+			  CT_id_unit_ne_list(fst, rest),
 			  xlate_tactic tac)
   | ((_,x),tac) ->
       CT_rec_tactic_fun(xlate_ident x,
-			CT_id_unit_list (xlate_id_unit (Some x), []),
+			CT_id_unit_ne_list (xlate_id_unit (Some x), []),
 			xlate_tactic tac)
 
 and xlate_local_rec_tac = function 
@@ -763,14 +769,14 @@ and xlate_local_rec_tac = function
   | ((_,x),(argl,tac)) ->
       let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in
 	CT_rec_tactic_fun(xlate_ident x,
-			  CT_id_unit_list(fst, rest),
+			  CT_id_unit_ne_list(fst, rest),
 			  xlate_tactic tac)
 
 and xlate_tactic =
  function
    | TacFun (largs, t) ->
        let fst, rest =  xlate_largs_to_id_unit largs in
-       CT_tactic_fun (CT_id_unit_list(fst, rest), xlate_tactic t)
+       CT_tactic_fun (CT_id_unit_ne_list(fst, rest), xlate_tactic t)
    | TacThen (t1,t2) -> 
        (match xlate_tactic t1 with
             CT_then(a,l) -> CT_then(a,l@[xlate_tactic t2])
@@ -1072,20 +1078,18 @@ and xlate_tac =
        let idl' = List.map xlate_hyp idl in
        CT_clear (CT_id_ne_list (xlate_hyp id, idl'))
     | (*For translating tactics/Inv.v *)
-      TacInversion (NonDepInversion (k,idl,[]),quant_hyp) ->
+      TacInversion (NonDepInversion (k,idl,l),quant_hyp) ->
 	CT_inversion(compute_INV_TYPE k, xlate_quantified_hypothesis quant_hyp,
+		     xlate_intro_patt_list l,
 	             CT_id_list (List.map xlate_hyp idl))
-    | TacInversion (DepInversion (k,copt,[]),quant_hyp) ->
+    | TacInversion (DepInversion (k,copt,l),quant_hyp) ->
 	let id = xlate_quantified_hypothesis quant_hyp in
-	CT_depinversion (compute_INV_TYPE k, id, xlate_formula_opt copt)
+	CT_depinversion (compute_INV_TYPE k, id, 
+			 xlate_intro_patt_list l, xlate_formula_opt copt)
     | TacInversion (InversionUsing (c,idlist), id) ->
 	let id = xlate_quantified_hypothesis id in
 	  CT_use_inversion (id, xlate_formula c,
 	    CT_id_list (List.map xlate_hyp idlist))
-    | TacInversion (NonDepInversion (k,idl,names),quant_hyp) ->
-	xlate_error "TODO: Inversion with names"
-    | TacInversion (DepInversion (k,copt,names),quant_hyp) ->
-	xlate_error "TODO: Inversion with names"
     | TacExtend (_,"Omega", []) -> CT_omega
     | TacRename (id1, id2) -> CT_rename(xlate_hyp id1, xlate_hyp id2)
     | TacClearBody([]) -> assert false
@@ -1095,19 +1099,11 @@ and xlate_tac =
     | TacNewDestruct(a,b,(c,_)) ->
 	CT_new_destruct
 	  (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)))
+	   xlate_intro_patt_list c)
     | TacNewInduction(a,b,(c,_)) ->
 	CT_new_induction
 	  (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)))
+	   xlate_intro_patt_list c)
     | TacInstantiate (a, b, cl) -> 
         CT_instantiate(CT_int a, xlate_formula b,
 		       xlate_clause cl)
@@ -1337,18 +1333,22 @@ let xlate_check =
 
 let build_constructors l =
  let f (coe,((_,id),c)) =
-   if coe then xlate_error "TODO: coercions in constructors"
+   if coe then CT_constr_coercion (xlate_ident id, xlate_formula c)
    else CT_constr (xlate_ident id, xlate_formula c) in
  CT_constr_list (List.map f l)
 
 let build_record_field_list l =
  let build_record_field (coe,d) = match d with
   | AssumExpr (id,c) ->
-      if coe then CT_constr_coercion (xlate_id_opt id, xlate_formula c)
+      if coe then CT_recconstr_coercion (xlate_id_opt id, xlate_formula c)
       else
 	CT_recconstr(xlate_id_opt id, xlate_formula c)
   | DefExpr (id,c,topt) ->
-      xlate_error "TODO: manifest fields in Record" in
+      if coe then
+ 	CT_defrecconstr_coercion(xlate_id_opt id, xlate_formula c,
+			      xlate_formula_opt topt)
+      else
+ 	CT_defrecconstr(xlate_id_opt id, xlate_formula c, xlate_formula_opt topt) in
  CT_recconstr_list (List.map build_record_field l);;
 
 let get_require_flags impexp spec =
@@ -1407,12 +1407,8 @@ let xlate_vernac =
  function
    | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) ->
        let fst, rest = xlate_largs_to_id_unit largs in
-       let extract = function CT_unit -> xlate_error "TODO: void parameter"
-	 | CT_coerce_ID_to_ID_UNIT x -> x in
-       let largs = List.map extract (fst::rest) in
        CT_tactic_definition(xlate_ident id,
-                           (* TODO, replace CT_id_list by CT_id_unit_list *)
-			    CT_id_list largs,
+			    CT_id_unit_list (fst::rest),
 			    xlate_tactic tac)
    | VernacDeclareTacticDefinition 
        (true,((id,TacFun (largs,tac))::_ as the_list)) ->
@@ -1423,7 +1419,7 @@ let xlate_vernac =
 	 | _ -> assert false in
        CT_rec_tactic_definition(CT_rec_tactic_fun_list(fst, others))
     | VernacDeclareTacticDefinition (false,[(_,id),tac]) ->
-       CT_tactic_definition(xlate_ident id, CT_id_list[], xlate_tactic tac)
+       CT_tactic_definition(xlate_ident id, CT_id_unit_list[], xlate_tactic tac)
     | VernacDeclareTacticDefinition (loc,_) -> xlate_error "Shouldn't occur"
     | VernacLoad (verbose,s) ->
       CT_load (