diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 367 |
1 files changed, 367 insertions, 0 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 new file mode 100644 index 00000000..2e067215 --- /dev/null +++ b/parsing/g_tactic.ml4 @@ -0,0 +1,367 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: g_tactic.ml4,v 1.83.2.2 2004/07/16 19:30:39 herbelin Exp $ *) + +open Pp +open Ast +open Pcoq +open Util +open Tacexpr +open Rawterm +open Genarg +open Constr +open Prim +open Tactic + +let tactic_kw = + [ "using"; "Orelse"; "Proof"; "Qed"; "And"; "()"; "|-" ] +let _ = + if !Options.v7 then + List.iter (fun s -> Lexer.add_token ("",s)) tactic_kw + +(* Functions overloaded by quotifier *) + +let induction_arg_of_constr c = + try ElimOnIdent (Topconstr.constr_loc c,snd (coerce_to_id c)) + with _ -> ElimOnConstr c + +let local_compute = [FBeta;FIota;FDeltaBut [];FZeta] + +let error_oldelim _ = error "OldElim no longer supported" + +let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2) + +(* Auxiliary grammar rules *) + +if !Options.v7 then +GEXTEND Gram + GLOBAL: simple_tactic constrarg bindings constr_with_bindings + quantified_hypothesis red_expr int_or_var castedopenconstr + simple_intropattern; + + int_or_var: + [ [ n = integer -> Genarg.ArgArg n + | id = identref -> Genarg.ArgVar id ] ] + ; + autoarg_depth: + [ [ n = OPT natural -> n ] ] + ; + autoarg_adding: + [ [ IDENT "Adding" ; "["; l = LIST1 global; "]" -> l | -> [] ] ] + ; + autoarg_destructing: + [ [ IDENT "Destructing" -> true | -> false ] ] + ; + autoarg_usingTDB: + [ [ "Using"; "TDB" -> true | -> false ] ] + ; + autoargs: + [ [ a0 = autoarg_depth; l = autoarg_adding; + a2 = autoarg_destructing; a3 = autoarg_usingTDB -> (a0,l,a2,a3) ] ] + ; + (* Either an hypothesis or a ltac ref (variable or pattern patvar) *) + id_or_ltac_ref: + [ [ id = base_ident -> AI (loc,id) + | "?"; n = natural -> AI (loc,Pattern.patvar_of_int n) ] ] + ; + (* Either a global ref or a ltac ref (variable or pattern patvar) *) + global_or_ltac_ref: + [ [ qid = global -> qid + | "?"; n = natural -> Libnames.Ident (loc,Pattern.patvar_of_int n) ] ] + ; + (* An identifier or a quotation meta-variable *) + id_or_meta: + [ [ id = identref -> AI id + + (* This is used in quotations *) + | id = METAIDENT -> MetaId (loc,id) ] ] + ; + (* A number or a quotation meta-variable *) + num_or_meta: + [ [ n = integer -> AI n + | id = METAIDENT -> MetaId (loc,id) + ] ] + ; + constrarg: + [ [ IDENT "Inst"; id = identref; "["; c = constr; "]" -> + ConstrContext (id, c) + | IDENT "Eval"; rtc = Tactic.red_expr; "in"; c = constr -> + ConstrEval (rtc,c) + | IDENT "Check"; c = constr -> ConstrTypeOf c + | c = constr -> ConstrTerm c ] ] + ; + castedopenconstr: + [ [ c = constr -> c ] ] + ; + induction_arg: + [ [ n = natural -> ElimOnAnonHyp n + | c = constr -> induction_arg_of_constr c + ] ] + ; + quantified_hypothesis: + [ [ id = base_ident -> NamedHyp id + | n = natural -> AnonHyp n ] ] + ; + conversion: + [ [ nl = LIST1 integer; c1 = constr; "with"; c2 = constr -> + (Some (nl,c1), c2) + | c1 = constr; "with"; c2 = constr -> (Some ([],c1), c2) + | c = constr -> (None, c) ] ] + ; + pattern_occ: + [ [ nl = LIST0 integer; c = constr -> (nl,c) ] ] + ; + intropatterns: + [ [ l = LIST0 simple_intropattern -> l ]] + ; + simple_intropattern: + [ [ "["; tc = LIST1 intropatterns SEP "|" ; "]" -> IntroOrAndPattern tc + | "("; tc = LIST1 simple_intropattern SEP "," ; ")" -> IntroOrAndPattern [tc] + | IDENT "_" -> IntroWildcard + | id = base_ident -> IntroIdentifier id + ] ] + ; + simple_binding: + [ [ id = base_ident; ":="; c = constr -> (loc, NamedHyp id, c) + | n = natural; ":="; c = constr -> (loc, AnonHyp n, c) ] ] + ; + bindings: + [ [ c1 = constr; ":="; c2 = constr; bl = LIST0 simple_binding -> + ExplicitBindings + ((join_to_constr loc c2,NamedHyp (snd(coerce_to_id c1)), c2) :: bl) + | n = natural; ":="; c = constr; bl = LIST0 simple_binding -> + ExplicitBindings ((join_to_constr loc c,AnonHyp n, c) :: bl) + | c1 = constr; bl = LIST0 constr -> + ImplicitBindings (c1 :: bl) ] ] + ; + constr_with_bindings: + [ [ c = constr; l = with_bindings -> (c, l) ] ] + ; + with_bindings: + [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] + ; + unfold_occ: + [ [ nl = LIST0 integer; c = global_or_ltac_ref -> (nl,c) ] ] + ; + red_flag: + [ [ IDENT "Beta" -> FBeta + | IDENT "Delta" -> FDeltaBut [] + | IDENT "Iota" -> FIota + | IDENT "Zeta" -> FZeta + | IDENT "Delta"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FConst idl + | IDENT "Delta"; "-"; "["; idl = LIST1 global_or_ltac_ref; "]" -> FDeltaBut idl + ] ] + ; + red_tactic: + [ [ IDENT "Red" -> Red false + | IDENT "Hnf" -> Hnf + | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po + | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s) + | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s) + | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta]) + | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul + | IDENT "Fold"; cl = LIST1 constr -> Fold cl + | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ] + ; + (* This is [red_tactic] including possible extensions *) + red_expr: + [ [ IDENT "Red" -> Red false + | IDENT "Hnf" -> Hnf + | IDENT "Simpl"; po = OPT pattern_occ -> Simpl po + | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s) + | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s) + | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta]) + | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul + | IDENT "Fold"; cl = LIST1 constr -> Fold cl + | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl + | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ] + ; + hypident: + [ [ id = id_or_meta -> id,[],(InHyp,ref None) + | "("; "Type"; "of"; id = id_or_meta; ")" -> + id,[],(InHypTypeOnly,ref None) + ] ] + ; + clause: + [ [ "in"; idl = LIST1 hypident -> + {onhyps=Some idl;onconcl=false; concl_occs=[]} + | -> {onhyps=Some[];onconcl=true;concl_occs=[]} ] ] + ; + simple_clause: + [ [ "in"; idl = LIST1 id_or_meta -> idl + | -> [] ] ] + ; + pattern_occ_hyp_tail_list: + [ [ pl = pattern_occ_hyp_list -> pl + | -> {onhyps=Some[];onconcl=false; concl_occs=[]} ] ] + ; + pattern_occ_hyp_list: + [ [ nl = LIST1 natural; IDENT "Goal" -> + {onhyps=Some[];onconcl=true;concl_occs=nl} + | nl = LIST1 natural; id = id_or_meta; cls = pattern_occ_hyp_tail_list + -> {cls with + onhyps=option_app(fun l -> (id,nl,(InHyp,ref None))::l) + cls.onhyps} + | IDENT "Goal" -> {onhyps=Some[];onconcl=true;concl_occs=[]} + | id = id_or_meta; cls = pattern_occ_hyp_tail_list -> + {cls with + onhyps=option_app(fun l -> (id,[],(InHyp,ref None))::l) + cls.onhyps} ] ] + ; + clause_pattern: + [ [ "in"; p = pattern_occ_hyp_list -> p + | -> {onhyps=None; onconcl=true; concl_occs=[] } ] ] + ; + fixdecl: + [ [ id = base_ident; "/"; n = natural; ":"; c = constr -> (id,n,c) ] ] + ; + cofixdecl: + [ [ id = base_ident; ":"; c = constr -> (id,c) ] ] + ; + hintbases: + [ [ "with"; "*" -> None + | "with"; l = LIST1 IDENT -> Some l + | -> Some [] ] ] + ; + eliminator: + [ [ "using"; el = constr_with_bindings -> el ] ] + ; + with_names: + [ [ "as"; ipat = simple_intropattern -> Some ipat | -> None ] ] + ; + simple_tactic: + [ [ + (* Basic tactics *) + IDENT "Intros"; IDENT "until"; id = quantified_hypothesis -> + TacIntrosUntil id + | IDENT "Intros"; pl = intropatterns -> TacIntroPattern pl + | IDENT "Intro"; id = base_ident; IDENT "after"; id2 = identref -> + TacIntroMove (Some id, Some id2) + | IDENT "Intro"; IDENT "after"; id2 = identref -> + TacIntroMove (None, Some id2) + | IDENT "Intro"; id = base_ident -> TacIntroMove (Some id,None) + | IDENT "Intro" -> TacIntroMove (None, None) + + | IDENT "Assumption" -> TacAssumption + | IDENT "Exact"; c = constr -> TacExact c + + | IDENT "Apply"; cl = constr_with_bindings -> TacApply cl + | IDENT "Elim"; cl = constr_with_bindings; el = OPT eliminator -> + TacElim (cl,el) + | IDENT "OldElim"; c = constr -> + (* TacOldElim c *) error_oldelim () + | IDENT "ElimType"; c = constr -> TacElimType c + | IDENT "Case"; cl = constr_with_bindings -> TacCase cl + | IDENT "CaseType"; c = constr -> TacCaseType c + | IDENT "Fix"; n = natural -> TacFix (None,n) + | IDENT "Fix"; id = base_ident; n = natural -> TacFix (Some id,n) + | IDENT "Fix"; id = base_ident; n = natural; "with"; fd = LIST0 fixdecl -> + TacMutualFix (id,n,fd) + | IDENT "Cofix" -> TacCofix None + | IDENT "Cofix"; id = base_ident -> TacCofix (Some id) + | IDENT "Cofix"; id = base_ident; "with"; fd = LIST0 cofixdecl -> + TacMutualCofix (id,fd) + + | IDENT "Cut"; c = constr -> TacCut c + | IDENT "Assert"; c = constr -> TacTrueCut (Names.Anonymous,c) + | IDENT "Assert"; c = constr; ":"; t = constr -> + TacTrueCut (Names.Name (snd(coerce_to_id c)),t) + | IDENT "Assert"; c = constr; ":="; b = constr -> + TacForward (false,Names.Name (snd (coerce_to_id c)),b) + | IDENT "Pose"; c = constr; ":="; b = constr -> + TacForward (true,Names.Name (snd(coerce_to_id c)),b) + | IDENT "Pose"; b = constr -> TacForward (true,Names.Anonymous,b) + | IDENT "Generalize"; lc = LIST1 constr -> TacGeneralize lc + | IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c + | IDENT "LetTac"; (_,na) = name; ":="; c = constr; p = clause_pattern + -> TacLetTac (na,c,p) + | IDENT "Instantiate"; n = natural; c = constr; cls = clause -> + TacInstantiate (n,c,cls) + | IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings -> + TacSpecialize (n,lcb) + | IDENT "LApply"; c = constr -> TacLApply c + + (* Derived basic tactics *) + | IDENT "Induction"; h = quantified_hypothesis -> TacSimpleInduction (h,ref []) + | IDENT "NewInduction"; c = induction_arg; el = OPT eliminator; + ids = with_names -> TacNewInduction (c,el,(ids,ref [])) + | IDENT "Double"; IDENT "Induction"; h1 = quantified_hypothesis; + h2 = quantified_hypothesis -> TacDoubleInduction (h1,h2) + | IDENT "Destruct"; h = quantified_hypothesis -> TacSimpleDestruct h + | IDENT "NewDestruct"; c = induction_arg; el = OPT eliminator; + ids = with_names -> TacNewDestruct (c,el,(ids,ref [])) + | IDENT "Decompose"; IDENT "Record" ; c = constr -> TacDecomposeAnd c + | IDENT "Decompose"; IDENT "Sum"; c = constr -> TacDecomposeOr c + | IDENT "Decompose"; "["; l = LIST1 global_or_ltac_ref; "]"; c = constr + -> TacDecompose (l,c) + + (* Automation tactic *) + | IDENT "Trivial"; db = hintbases -> TacTrivial db + | IDENT "Auto"; n = OPT natural; db = hintbases -> TacAuto (n, db) + + | IDENT "AutoTDB"; n = OPT natural -> TacAutoTDB n + | IDENT "CDHyp"; id = identref -> TacDestructHyp (true,id) + | IDENT "DHyp"; id = identref -> TacDestructHyp (false,id) + | IDENT "DConcl" -> TacDestructConcl + | IDENT "SuperAuto"; l = autoargs -> TacSuperAuto l + | IDENT "Auto"; n = OPT natural; IDENT "Decomp"; p = OPT natural -> + TacDAuto (n, p) + + (* Context management *) + | IDENT "Clear"; l = LIST1 id_or_ltac_ref -> TacClear l + | IDENT "ClearBody"; l = LIST1 id_or_ltac_ref -> TacClearBody l + | IDENT "Move"; id1 = id_or_ltac_ref; IDENT "after"; + id2 = id_or_ltac_ref -> TacMove (true,id1,id2) + | IDENT "Rename"; id1 = id_or_ltac_ref; IDENT "into"; + id2 = id_or_ltac_ref -> TacRename (id1,id2) + + (* Constructors *) + | IDENT "Left"; bl = with_bindings -> TacLeft bl + | IDENT "Right"; bl = with_bindings -> TacRight bl + | IDENT "Split"; bl = with_bindings -> TacSplit (false,bl) + | IDENT "Exists"; bl = bindings -> TacSplit (true,bl) + | IDENT "Exists" -> TacSplit (true,NoBindings) + | IDENT "Constructor"; n = num_or_meta; l = with_bindings -> + TacConstructor (n,l) + | IDENT "Constructor"; t = OPT tactic -> TacAnyConstructor t + + (* Equivalence relations *) + | IDENT "Reflexivity" -> TacReflexivity + | IDENT "Symmetry"; cls = clause -> TacSymmetry cls + | IDENT "Transitivity"; c = constr -> TacTransitivity c + + (* Equality and inversion *) + | IDENT "Dependent"; k = + [ IDENT "Simple"; IDENT "Inversion" -> SimpleInversion + | IDENT "Inversion" -> FullInversion + | IDENT "Inversion_clear" -> FullInversionClear ]; + hyp = quantified_hypothesis; + ids = with_names; co = OPT ["with"; c = constr -> c] -> + TacInversion (DepInversion (k,co,ids),hyp) + | IDENT "Simple"; IDENT "Inversion"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp) + | IDENT "Inversion"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (FullInversion, cl, ids), hyp) + | IDENT "Inversion_clear"; + hyp = quantified_hypothesis; ids = with_names; cl = simple_clause -> + TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp) + | IDENT "Inversion"; hyp = quantified_hypothesis; + "using"; c = constr; cl = simple_clause -> + TacInversion (InversionUsing (c,cl), hyp) + + (* Conversion *) + | r = red_tactic; cl = clause -> TacReduce (r, cl) + (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) + | IDENT "Change"; (oc,c) = conversion; cl = clause -> TacChange (oc,c,cl) + + ] ] + ; +END;; |