From dfa81d7860309029d100cd5348d2dd6bd8fa33c9 Mon Sep 17 00:00:00 2001 From: jforest Date: Tue, 21 Mar 2006 21:54:43 +0000 Subject: + destruct now works as induction on multiple arguments : destruct x y z using scheme + replace c1 with c2 has now a new optional argument replace c1 with c2 by tac tries to prove c2 = c1 with tac + I've also factorize the code correspoing to replace in extractactics git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8651 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/ascent.mli | 4 ++-- contrib/interface/vtp.ml | 8 +++++--- contrib/interface/xlate.ml | 27 ++++++++++++++++++++------- 3 files changed, 27 insertions(+), 12 deletions(-) (limited to 'contrib/interface') diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 335afddd2..fb71288a9 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -670,7 +670,7 @@ and ct_TACTIC_COM = | CT_match_context_reverse of ct_CONTEXT_RULE * ct_CONTEXT_RULE list | 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_INTRO_PATT_OPT + | CT_new_destruct of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT | CT_new_induction of ct_FORMULA_OR_INT list * ct_USING * ct_INTRO_PATT_OPT | CT_omega | CT_orelse of ct_TACTIC_COM * ct_TACTIC_COM @@ -684,7 +684,7 @@ and ct_TACTIC_COM = | CT_reflexivity | CT_rename of ct_ID * ct_ID | CT_repeat of ct_TACTIC_COM - | CT_replace_with of ct_FORMULA * ct_FORMULA + | CT_replace_with of ct_FORMULA * ct_FORMULA * ct_ID_OPT * ct_TACTIC_OPT | CT_rewrite_lr of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT | CT_rewrite_rl of ct_FORMULA * ct_SPEC_LIST * ct_ID_OPT | CT_right of ct_SPEC_LIST diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 88852aa59..5a7ccc26b 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -1660,7 +1660,7 @@ and fTACTIC_COM = function fID x2; fNODE "move_after" 2 | CT_new_destruct(x1, x2, x3) -> - fFORMULA_OR_INT x1; + (List.iter fFORMULA_OR_INT x1); (* Julien F. Est-ce correct? *) fUSING x2; fINTRO_PATT_OPT x3; fNODE "new_destruct" 3 @@ -1708,10 +1708,12 @@ and fTACTIC_COM = function | CT_repeat(x1) -> fTACTIC_COM x1; fNODE "repeat" 1 -| CT_replace_with(x1, x2) -> +| CT_replace_with(x1, x2,x3,x4) -> fFORMULA x1; fFORMULA x2; - fNODE "replace_with" 2 + fID_OPT x3; + fTACTIC_OPT x4; + fNODE "replace_with" 4 | CT_rewrite_lr(x1, x2, x3) -> fFORMULA x1; fSPEC_LIST x2; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 4556d818e..da87086e2 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -63,7 +63,7 @@ let coercion_description t = !coercion_description_holder t;; let set_coercion_description f = coercion_description_holder:=f; ();; -let xlate_error s = failwith ("Translation error: " ^ s);; +let xlate_error s = print_endline ("xlate_error : "^s);failwith ("Translation error: " ^ s);; let ctf_STRING_OPT_NONE = CT_coerce_NONE_to_STRING_OPT CT_none;; @@ -957,10 +957,22 @@ and xlate_tac = | TacRight bindl -> CT_right (xlate_bindings bindl) | TacSplit (false,bindl) -> CT_split (xlate_bindings bindl) | TacSplit (true,bindl) -> CT_exists (xlate_bindings bindl) - | TacExtend (_,"replace", [c1; c2]) -> - let c1 = xlate_formula (out_gen rawwit_constr c1) in - let c2 = xlate_formula (out_gen rawwit_constr c2) in - CT_replace_with (c1, c2) + | TacExtend (_,"replace", [c1; c2;id_opt;tac_opt]) -> + let c1 = xlate_formula (out_gen rawwit_constr c1) in + let c2 = xlate_formula (out_gen rawwit_constr c2) in + let id_opt = + match out_gen Extratactics.rawwit_in_arg_hyp id_opt with + | None -> ctv_ID_OPT_NONE + | Some id -> ctf_ID_OPT_SOME (xlate_ident id) + in + let tac_opt = + match out_gen (Extratactics.rawwit_by_arg_tac) tac_opt with + | None -> CT_coerce_NONE_to_TACTIC_OPT CT_none + | Some tac -> + let tac = xlate_tactic tac in + CT_coerce_TACTIC_COM_to_TACTIC_OPT tac + in + CT_replace_with (c1, c2,id_opt,tac_opt) | TacExtend (_,"rewrite", [b; cbindl]) -> let b = out_gen Extraargs.rawwit_orient b in let (c,bindl) = out_gen rawwit_constr_with_bindings cbindl in @@ -1157,8 +1169,8 @@ and xlate_tac = | TacDAuto (a, b) -> CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacNewDestruct(a,b,c) -> - CT_new_destruct - (xlate_int_or_constr a, xlate_using b, + CT_new_destruct (* Julien F. : est-ce correct *) + (List.map xlate_int_or_constr a, xlate_using b, xlate_with_names c) | TacNewInduction(a,b,c) -> CT_new_induction (* Pierre C. : est-ce correct *) @@ -1195,6 +1207,7 @@ and xlate_tac = (List.map xlate_formula (out_gen (wit_list0 rawwit_constr) args))) | TacExtend (_,id, l) -> + print_endline ("Extratactics : "^ id); CT_user_tac (CT_ident id, CT_targ_list (List.map coerce_genarg_to_TARG l)) | TacAlias _ -> xlate_error "Alias not supported" -- cgit v1.2.3