From 43d720413387ae7670951920de07478b2e76efe4 Mon Sep 17 00:00:00 2001 From: bertot Date: Fri, 30 Jan 2004 09:34:40 +0000 Subject: updates the definition of tactics using Ltac and adds the subst tactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5274 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/interface/ascent.mli | 42 ++++++++++++------ contrib/interface/vtp.ml | 100 ++++++++++++++++++++++++++++++++----------- contrib/interface/xlate.ml | 64 ++++++++++++--------------- 3 files changed, 133 insertions(+), 73 deletions(-) diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli index 5ecbc6b53..7531d80b3 100644 --- a/contrib/interface/ascent.mli +++ b/contrib/interface/ascent.mli @@ -57,6 +57,7 @@ and ct_COMMAND = | CT_coercion of ct_LOCAL_OPT * ct_IDENTITY_OPT * ct_ID * ct_ID * ct_ID | CT_cofix_decl of ct_COFIX_REC_LIST | CT_compile_module of ct_VERBOSE_OPT * ct_ID * ct_STRING_OPT + | CT_declare_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR | CT_define_notation of ct_STRING * ct_FORMULA * ct_MODIFIER_LIST * ct_ID_OPT | CT_definition of ct_DEFN * ct_ID * ct_BINDER_LIST * ct_DEF_BODY * ct_FORMULA_OPT | CT_delim_scope of ct_ID * ct_ID @@ -67,6 +68,8 @@ and ct_COMMAND = | CT_explain_proof of ct_INT_LIST | CT_explain_prooftree of ct_INT_LIST | CT_export_id of ct_ID_NE_LIST + | CT_extract_to_file of ct_STRING * ct_ID_NE_LIST + | CT_extraction of ct_ID_OPT | CT_fix_decl of ct_FIX_REC_LIST | CT_focus of ct_INT_OPT | CT_go of ct_INT_OR_LOCN @@ -98,7 +101,8 @@ and ct_COMMAND = | CT_ml_declare_modules of ct_STRING_NE_LIST | CT_ml_print_modules | CT_ml_print_path - | CT_module of ct_ID + | CT_module of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_CHECK * ct_MODULE_EXPR + | CT_module_type_decl of ct_ID * ct_MODULE_BINDER_LIST * ct_MODULE_TYPE_OPT | CT_omega_flag of ct_OMEGA_MODE * ct_OMEGA_FEATURE | CT_opaque of ct_ID_NE_LIST | CT_open_scope of ct_ID @@ -135,7 +139,6 @@ and ct_COMMAND = | CT_quit | CT_read_module of ct_ID | CT_rec_ml_add_path of ct_STRING - | CT_rec_tactic_definition of ct_REC_TACTIC_FUN_LIST | CT_recaddpath of ct_STRING * ct_ID_OPT | CT_record of ct_COERCION_OPT * ct_ID * ct_BINDER_LIST * ct_FORMULA * ct_ID_OPT * ct_RECCONSTR_LIST | CT_remove_natural_feature of ct_NATURAL_FEATURE * ct_ID @@ -174,7 +177,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_UNIT_LIST * ct_TACTIC_COM + | CT_tactic_definition of ct_TAC_DEF_NE_LIST | CT_test_natural_feature of ct_NATURAL_FEATURE * ct_ID | CT_theorem_struct of ct_THEOREM_GOAL * ct_PROOF_SCRIPT | CT_time of ct_COMMAND @@ -351,13 +354,6 @@ and ct_ID_OR_STRING = | CT_coerce_STRING_to_ID_OR_STRING of ct_STRING and ct_ID_OR_STRING_NE_LIST = CT_id_or_string_ne_list of ct_ID_OR_STRING * ct_ID_OR_STRING list -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 list -and ct_ID_UNIT_NE_LIST = - CT_id_unit_ne_list of ct_ID_UNIT * ct_ID_UNIT list and ct_IMPEXP = CT_coerce_NONE_to_IMPEXP of ct_NONE | CT_export @@ -442,6 +438,23 @@ and ct_MODIFIER = | CT_set_level of ct_INT and ct_MODIFIER_LIST = CT_modifier_list of ct_MODIFIER list +and ct_MODULE_BINDER = + CT_module_binder of ct_ID_NE_LIST * ct_MODULE_TYPE +and ct_MODULE_BINDER_LIST = + CT_module_binder_list of ct_MODULE_BINDER list +and ct_MODULE_EXPR = + CT_coerce_ID_OPT_to_MODULE_EXPR of ct_ID_OPT + | CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR +and ct_MODULE_TYPE = + CT_coerce_ID_to_MODULE_TYPE of ct_ID + | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA + | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID +and ct_MODULE_TYPE_CHECK = + CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT + | CT_only_check of ct_MODULE_TYPE +and ct_MODULE_TYPE_OPT = + CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT + | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE and ct_NATURAL_FEATURE = CT_contractible | CT_implicit @@ -489,7 +502,7 @@ and ct_RECCONSTR = 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_NE_LIST * ct_TACTIC_COM + CT_rec_tactic_fun of ct_ID * ct_ID_OPT_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 = @@ -648,11 +661,12 @@ and ct_TACTIC_COM = | CT_simplify_eq of ct_ID_OPT | CT_specialize of ct_INT_OPT * ct_FORMULA * ct_SPEC_LIST | CT_split of ct_SPEC_LIST + | CT_subst of ct_ID_LIST | CT_superauto of ct_INT_OPT * ct_ID_LIST * ct_DESTRUCTING * ct_USINGTDB | 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_NE_LIST * ct_TACTIC_COM + | CT_tactic_fun of ct_ID_OPT_NE_LIST * ct_TACTIC_COM | CT_then of ct_TACTIC_COM * ct_TACTIC_COM list | CT_transitivity of ct_FORMULA | CT_trivial @@ -665,6 +679,10 @@ and ct_TACTIC_COM = and ct_TACTIC_OPT = CT_coerce_NONE_to_TACTIC_OPT of ct_NONE | CT_coerce_TACTIC_COM_to_TACTIC_OPT of ct_TACTIC_COM +and ct_TAC_DEF = + CT_tac_def of ct_ID * ct_TACTIC_COM +and ct_TAC_DEF_NE_LIST = + CT_tac_def_ne_list of ct_TAC_DEF * ct_TAC_DEF list and ct_TARG = CT_coerce_BINDING_to_TARG of ct_BINDING | CT_coerce_COFIXTAC_to_TARG of ct_COFIXTAC diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml index 5c9ab48c3..a6fad0769 100644 --- a/contrib/interface/vtp.ml +++ b/contrib/interface/vtp.ml @@ -154,6 +154,12 @@ and fCOMMAND = function fID x2; fSTRING_OPT x3; fNODE "compile_module" 3 +| CT_declare_module(x1, x2, x3, x4) -> + fID x1; + fMODULE_BINDER_LIST x2; + fMODULE_TYPE_CHECK x3; + fMODULE_EXPR x4; + fNODE "declare_module" 4 | CT_define_notation(x1, x2, x3, x4) -> fSTRING x1; fFORMULA x2; @@ -201,6 +207,13 @@ and fCOMMAND = function | CT_export_id(x1) -> fID_NE_LIST x1; fNODE "export_id" 1 +| CT_extract_to_file(x1, x2) -> + fSTRING x1; + fID_NE_LIST x2; + fNODE "extract_to_file" 2 +| CT_extraction(x1) -> + fID_OPT x1; + fNODE "extraction" 1 | CT_fix_decl(x1) -> fFIX_REC_LIST x1; fNODE "fix_decl" 1 @@ -323,9 +336,17 @@ and fCOMMAND = function fNODE "ml_declare_modules" 1 | CT_ml_print_modules -> fNODE "ml_print_modules" 0 | CT_ml_print_path -> fNODE "ml_print_path" 0 -| CT_module(x1) -> +| CT_module(x1, x2, x3, x4) -> + fID x1; + fMODULE_BINDER_LIST x2; + fMODULE_TYPE_CHECK x3; + fMODULE_EXPR x4; + fNODE "module" 4 +| CT_module_type_decl(x1, x2, x3) -> fID x1; - fNODE "module" 1 + fMODULE_BINDER_LIST x2; + fMODULE_TYPE_OPT x3; + fNODE "module_type_decl" 3 | CT_omega_flag(x1, x2) -> fOMEGA_MODE x1; fOMEGA_FEATURE x2; @@ -410,9 +431,6 @@ and fCOMMAND = function | CT_rec_ml_add_path(x1) -> fSTRING x1; fNODE "rec_ml_add_path" 1 -| CT_rec_tactic_definition(x1) -> - fREC_TACTIC_FUN_LIST x1; - fNODE "rec_tactic_definition" 1 | CT_recaddpath(x1, x2) -> fSTRING x1; fID_OPT x2; @@ -527,11 +545,9 @@ and fCOMMAND = function fFORMULA x2; fINT_OPT x3; fNODE "syntax_macro" 3 -| CT_tactic_definition(x1, x2, x3) -> - fID x1; - fID_UNIT_LIST x2; - fTACTIC_COM x3; - fNODE "tactic_definition" 3 +| CT_tactic_definition(x1) -> + fTAC_DEF_NE_LIST x1; + fNODE "tactic_definition" 1 | CT_test_natural_feature(x1, x2) -> fNATURAL_FEATURE x1; fID x2; @@ -899,18 +915,6 @@ and fID_OR_STRING_NE_LIST = function fID_OR_STRING x; (List.iter fID_OR_STRING l); fNODE "id_or_string_ne_list" (1 + (List.length l)) -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 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_ne_list" (1 + (List.length l)) and fIMPEXP = function | CT_coerce_NONE_to_IMPEXP x -> fNONE x | CT_export -> fNODE "export" 0 @@ -1074,6 +1078,41 @@ and fMODIFIER_LIST = function | CT_modifier_list l -> (List.iter fMODIFIER l); fNODE "modifier_list" (List.length l) +and fMODULE_BINDER = function +| CT_module_binder(x1, x2) -> + fID_NE_LIST x1; + fMODULE_TYPE x2; + fNODE "module_binder" 2 +and fMODULE_BINDER_LIST = function +| CT_module_binder_list l -> + (List.iter fMODULE_BINDER l); + fNODE "module_binder_list" (List.length l) +and fMODULE_EXPR = function +| CT_coerce_ID_OPT_to_MODULE_EXPR x -> fID_OPT x +| CT_module_app(x1, x2) -> + fMODULE_EXPR x1; + fMODULE_EXPR x2; + fNODE "module_app" 2 +and fMODULE_TYPE = function +| CT_coerce_ID_to_MODULE_TYPE x -> fID x +| CT_module_type_with_def(x1, x2, x3) -> + fMODULE_TYPE x1; + fID x2; + fFORMULA x3; + fNODE "module_type_with_def" 3 +| CT_module_type_with_mod(x1, x2, x3) -> + fMODULE_TYPE x1; + fID x2; + fID x3; + fNODE "module_type_with_mod" 3 +and fMODULE_TYPE_CHECK = function +| CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK x -> fMODULE_TYPE_OPT x +| CT_only_check(x1) -> + fMODULE_TYPE x1; + fNODE "only_check" 1 +and fMODULE_TYPE_OPT = function +| CT_coerce_ID_OPT_to_MODULE_TYPE_OPT x -> fID_OPT x +| CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT x -> fMODULE_TYPE x and fNATURAL_FEATURE = function | CT_contractible -> fNODE "contractible" 0 | CT_implicit -> fNODE "implicit" 0 @@ -1161,7 +1200,7 @@ and fRECCONSTR_LIST = function and fREC_TACTIC_FUN = function | CT_rec_tactic_fun(x1, x2, x3) -> fID x1; - fID_UNIT_NE_LIST x2; + fID_OPT_NE_LIST x2; fTACTIC_COM x3; fNODE "rec_tactic_fun" 3 and fREC_TACTIC_FUN_LIST = function @@ -1611,6 +1650,9 @@ and fTACTIC_COM = function | CT_split(x1) -> fSPEC_LIST x1; fNODE "split" 1 +| CT_subst(x1) -> + fID_LIST x1; + fNODE "subst" 1 | CT_superauto(x1, x2, x3, x4) -> fINT_OPT x1; fID_LIST x2; @@ -1629,7 +1671,7 @@ and fTACTIC_COM = function (List.iter fTACTIC_COM l); fNODE "tacsolve" (1 + (List.length l)) | CT_tactic_fun(x1, x2) -> - fID_UNIT_NE_LIST x1; + fID_OPT_NE_LIST x1; fTACTIC_COM x2; fNODE "tactic_fun" 2 | CT_then(x,l) -> @@ -1665,6 +1707,16 @@ and fTACTIC_COM = function and fTACTIC_OPT = function | CT_coerce_NONE_to_TACTIC_OPT x -> fNONE x | CT_coerce_TACTIC_COM_to_TACTIC_OPT x -> fTACTIC_COM x +and fTAC_DEF = function +| CT_tac_def(x1, x2) -> + fID x1; + fTACTIC_COM x2; + fNODE "tac_def" 2 +and fTAC_DEF_NE_LIST = function +| CT_tac_def_ne_list(x,l) -> + fTAC_DEF x; + (List.iter fTAC_DEF l); + fNODE "tac_def_ne_list" (1 + (List.length l)) and fTARG = function | CT_coerce_BINDING_to_TARG x -> fBINDING x | CT_coerce_COFIXTAC_to_TARG x -> fCOFIXTAC x diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 97410ceb5..a6fd97833 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -174,10 +174,6 @@ let coerce_VARG_to_ID = x | _ -> xlate_error "coerce_VARG_to_ID";; -let xlate_id_unit = function - None -> CT_unit - | Some x -> CT_coerce_ID_to_ID_UNIT (xlate_ident x);; - let xlate_ident_opt = function | None -> ctv_ID_OPT_NONE @@ -639,8 +635,12 @@ 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);; -let xlate_largs_to_id_unit largs = - match List.map xlate_id_unit largs with +let xlate_arg_to_id_opt = function + Some id -> CT_coerce_ID_to_ID_OPT(CT_ident (string_of_id id)) + | None -> ctv_ID_OPT_NONE;; + +let xlate_largs_to_id_opt largs = + match List.map xlate_arg_to_id_opt largs with fst::rest -> fst, rest | _ -> assert false;; @@ -765,31 +765,20 @@ and xlate_red_tactic = | [] -> error "Expecting at least one pattern in a Pattern command") | ExtraRedExpr _ -> xlate_error "TODO LATER: ExtraRedExpr (probably dead code)" -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_ne_list(fst, rest), - xlate_tactic tac) - | ((_,x),tac) -> - CT_rec_tactic_fun(xlate_ident x, - CT_id_unit_ne_list (xlate_id_unit (Some x), []), - xlate_tactic tac) - and xlate_local_rec_tac = function (* TODO LATER: local recursive tactics and global ones should be handled in the same manner *) | ((_,x),(argl,tac)) -> - let fst, rest = xlate_largs_to_id_unit ((Some x)::argl) in + let fst, rest = xlate_largs_to_id_opt argl in CT_rec_tactic_fun(xlate_ident x, - CT_id_unit_ne_list(fst, rest), + CT_id_opt_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_ne_list(fst, rest), xlate_tactic t) + let fst, rest = xlate_largs_to_id_opt largs in + CT_tactic_fun (CT_id_opt_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]) @@ -999,6 +988,11 @@ and xlate_tac = let id = xlate_ident (out_gen rawwit_ident id) in if b then CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id) else CT_cutrewrite_lr (c, ctf_ID_OPT_SOME id) + | TacExtend(_, "subst", [l]) -> + CT_subst + (CT_id_list + (List.map (fun x -> CT_ident (string_of_id x)) + (out_gen (wit_list1 rawwit_ident) l))) | TacReflexivity -> CT_reflexivity | TacSymmetry cls -> CT_symmetry(xlate_clause cls) | TacTransitivity c -> CT_transitivity (xlate_formula c) @@ -1515,22 +1509,18 @@ let rec xlate_module_expr = function let rec xlate_vernac = function - | VernacDeclareTacticDefinition (false,[(_,id),TacFun (largs,tac)]) -> - let fst, rest = xlate_largs_to_id_unit largs in - CT_tactic_definition(xlate_ident id, - CT_id_unit_list (fst::rest), - xlate_tactic tac) - | VernacDeclareTacticDefinition - (true,((id,TacFun (largs,tac))::_ as the_list)) -> - let x_rec_tacs = - List.map xlate_rec_tac the_list in - let fst, others = match x_rec_tacs with - fst::others -> fst, others - | _ -> 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_unit_list[], xlate_tactic tac) - | VernacDeclareTacticDefinition (loc,_) -> xlate_error "Shouldn't occur" + | VernacDeclareTacticDefinition (true, tacs) -> + (match List.map + (function + ((_, id), body) -> + CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) + tacs with + [] -> assert false + | fst::tacs1 -> + CT_tactic_definition + (CT_tac_def_ne_list(fst, tacs1))) + | VernacDeclareTacticDefinition(false, _) -> + xlate_error "obsolete tactic definition not handled" | VernacLoad (verbose,s) -> CT_load ( (match verbose with -- cgit v1.2.3