From 2a52a7bab29b0c926382c29e560f7df48a097ecb Mon Sep 17 00:00:00 2001 From: bertot Date: Thu, 22 Jan 2004 14:47:18 +0000 Subject: 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 --- contrib/interface/ascent.mli | 19 ++++++++------ contrib/interface/vtp.ml | 46 +++++++++++++++++++++++---------- contrib/interface/xlate.ml | 60 +++++++++++++++++++++----------------------- 3 files changed, 73 insertions(+), 52 deletions(-) (limited to 'contrib/interface') 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 ( -- cgit v1.2.3