From cfc8b6a66bf4b9d23ea72ca8dfe5a5b03f74a46c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 22 Jun 2018 16:18:28 +0200 Subject: Port g_tactic to the homebrew GEXTEND parser. --- plugins/ltac/g_tactic.ml4 | 700 --------------------------------------------- plugins/ltac/g_tactic.mlg | 704 ++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 704 insertions(+), 700 deletions(-) delete mode 100644 plugins/ltac/g_tactic.ml4 create mode 100644 plugins/ltac/g_tactic.mlg (limited to 'plugins') diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 deleted file mode 100644 index 31bc34a32..000000000 --- a/plugins/ltac/g_tactic.ml4 +++ /dev/null @@ -1,700 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* "; "<-" ; "by" ] -let _ = List.iter CLexer.add_keyword tactic_kw - -let err () = raise Stream.Failure - -(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) -(* admissible notation "(x t)" *) -let test_lpar_id_coloneq = - Gram.Entry.of_parser "lpar_id_coloneq" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -(* Hack to recognize "(x)" *) -let test_lpar_id_rpar = - Gram.Entry.of_parser "lpar_id_coloneq" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ -> - (match stream_nth 2 strm with - | KEYWORD ")" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -(* idem for (x:=t) and (1:=t) *) -let test_lpar_idnum_coloneq = - Gram.Entry.of_parser "test_lpar_idnum_coloneq" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "(" -> - (match stream_nth 1 strm with - | IDENT _ | INT _ -> - (match stream_nth 2 strm with - | KEYWORD ":=" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -(* idem for (x:t) *) -open Extraargs - -(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) -let check_for_coloneq = - Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - let rec skip_to_rpar p n = - match List.last (Stream.npeek n strm) with - | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) - | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1) - | KEYWORD "." -> err () - | _ -> skip_to_rpar p (n+1) in - let rec skip_names n = - match List.last (Stream.npeek n strm) with - | IDENT _ | KEYWORD "_" -> skip_names (n+1) - | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) - | _ -> err () in - let rec skip_binders n = - match List.last (Stream.npeek n strm) with - | KEYWORD "(" -> skip_binders (skip_names (n+1)) - | IDENT _ | KEYWORD "_" -> skip_binders (n+1) - | KEYWORD ":=" -> () - | _ -> err () in - match stream_nth 0 strm with - | KEYWORD "(" -> skip_binders 2 - | _ -> err ()) - -let lookup_at_as_comma = - Gram.Entry.of_parser "lookup_at_as_comma" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD (","|"at"|"as") -> () - | _ -> err ()) - -open Constr -open Prim -open Pltac - -let mk_fix_tac (loc,id,bl,ann,ty) = - let n = - match bl,ann with - [([_],_,_)], None -> 1 - | _, Some x -> - let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in - (try List.index Names.Name.equal x.CAst.v ids - with Not_found -> user_err Pp.(str "No such fix variable.")) - | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in - let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in - (id,n, CAst.make ~loc @@ CProdN(bl,ty)) - -let mk_cofix_tac (loc,id,bl,ann,ty) = - let _ = Option.map (fun { CAst.loc = aloc } -> - user_err ?loc:aloc - ~hdr:"Constr:mk_cofix_tac" - (Pp.str"Annotation forbidden in cofix expression.")) ann in - let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in - (id,CAst.make ~loc @@ CProdN(bl,ty)) - -(* Functions overloaded by quotifier *) -let destruction_arg_of_constr (c,lbind as clbind) = match lbind with - | NoBindings -> - begin - try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v) - with e when CErrors.noncritical e -> ElimOnConstr clbind - end - | _ -> ElimOnConstr clbind - -let mkNumeral n = Numeral (string_of_int (abs n), 0<=n) - -let mkTacCase with_evar = function - | [(clear,ElimOnConstr cl),(None,None),None],None -> - TacCase (with_evar,(clear,cl)) - (* Reinterpret numbers as a notation for terms *) - | [(clear,ElimOnAnonHyp n),(None,None),None],None -> - TacCase (with_evar, - (clear,(CAst.make @@ CPrim (mkNumeral n), - NoBindings))) - (* Reinterpret ident as notations for variables in the context *) - (* because we don't know if they are quantified or not *) - | [(clear,ElimOnIdent id),(None,None),None],None -> - TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) - | ic -> - if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) - then - user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported."); - TacInductionDestruct (false,with_evar,ic) - -let rec mkCLambdaN_simple_loc ?loc bll c = - match bll with - | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll -> - CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) - | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c - | [] -> c - -let mkCLambdaN_simple bl c = match bl with - | [] -> c - | h :: _ -> - let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in - mkCLambdaN_simple_loc ?loc bl c - -let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc - -let map_int_or_var f = function - | ArgArg x -> ArgArg (f x) - | ArgVar _ as y -> y - -let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } - -let merge_occurrences loc cl = function - | None -> - if Locusops.clause_with_generic_occurrences cl then (None, cl) - else - user_err ~loc (str "Found an \"at\" clause without \"with\" clause.") - | Some (occs, p) -> - let ans = match occs with - | AllOccurrences -> cl - | _ -> - begin match cl with - | { onhyps = Some []; concl_occs = AllOccurrences } -> - { onhyps = Some []; concl_occs = occs } - | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } -> - { cl with onhyps = Some [(occs, id), l] } - | _ -> - if Locusops.clause_with_generic_occurrences cl then - user_err ~loc (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") - else - user_err ~loc (str "Cannot use clause \"at\" twice.") - end - in - (Some p, ans) - -let warn_deprecated_eqn_syntax = - CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" - (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) - -(* Auxiliary grammar rules *) - -open Pvernac.Vernac_ - -GEXTEND Gram - GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis - bindings red_expr int_or_var open_constr uconstr - simple_intropattern in_clause clause_dft_concl hypident destruction_arg; - - int_or_var: - [ [ n = integer -> ArgArg n - | id = identref -> ArgVar id ] ] - ; - nat_or_var: - [ [ n = natural -> ArgArg n - | id = identref -> ArgVar id ] ] - ; - (* An identifier or a quotation meta-variable *) - id_or_meta: - [ [ id = identref -> id ] ] - ; - open_constr: - [ [ c = constr -> c ] ] - ; - uconstr: - [ [ c = constr -> c ] ] - ; - destruction_arg: - [ [ n = natural -> (None,ElimOnAnonHyp n) - | test_lpar_id_rpar; c = constr_with_bindings -> - (Some false,destruction_arg_of_constr c) - | c = constr_with_bindings_arg -> on_snd destruction_arg_of_constr c - ] ] - ; - constr_with_bindings_arg: - [ [ ">"; c = constr_with_bindings -> (Some true,c) - | c = constr_with_bindings -> (None,c) ] ] - ; - quantified_hypothesis: - [ [ id = ident -> NamedHyp id - | n = natural -> AnonHyp n ] ] - ; - conversion: - [ [ c = constr -> (None, c) - | c1 = constr; "with"; c2 = constr -> (Some (AllOccurrences,c1),c2) - | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> - (Some (occs,c1), c2) ] ] - ; - occs_nums: - [ [ nl = LIST1 nat_or_var -> OnlyOccurrences nl - | "-"; n = nat_or_var; nl = LIST0 int_or_var -> - (* have used int_or_var instead of nat_or_var for compatibility *) - AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) ] ] - ; - occs: - [ [ "at"; occs = occs_nums -> occs | -> AllOccurrences ] ] - ; - pattern_occ: - [ [ c = constr; nl = occs -> (nl,c) ] ] - ; - ref_or_pattern_occ: - (* If a string, it is interpreted as a ref - (anyway a Coq string does not reduce) *) - [ [ c = smart_global; nl = occs -> nl,Inl c - | c = constr; nl = occs -> nl,Inr c ] ] - ; - unfold_occ: - [ [ c = smart_global; nl = occs -> (nl,c) ] ] - ; - intropatterns: - [ [ l = LIST0 nonsimple_intropattern -> l ]] - ; - ne_intropatterns: - [ [ l = LIST1 nonsimple_intropattern -> l ]] - ; - or_and_intropattern: - [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> IntroOrPattern tc - | "()" -> IntroAndPattern [] - | "("; si = simple_intropattern; ")" -> IntroAndPattern [si] - | "("; si = simple_intropattern; ","; - tc = LIST1 simple_intropattern SEP "," ; ")" -> - IntroAndPattern (si::tc) - | "("; si = simple_intropattern; "&"; - tc = LIST1 simple_intropattern SEP "&" ; ")" -> - (* (A & B & C) is translated into (A,(B,C)) *) - let rec pairify = function - | ([]|[_]|[_;_]) as l -> l - | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] - in IntroAndPattern (pairify (si::tc)) ] ] - ; - equality_intropattern: - [ [ "->" -> IntroRewrite true - | "<-" -> IntroRewrite false - | "[="; tc = intropatterns; "]" -> IntroInjection tc ] ] - ; - naming_intropattern: - [ [ prefix = pattern_ident -> IntroFresh prefix - | "?" -> IntroAnonymous - | id = ident -> IntroIdentifier id ] ] - ; - nonsimple_intropattern: - [ [ l = simple_intropattern -> l - | "*" -> CAst.make ~loc:!@loc @@ IntroForthcoming true - | "**" -> CAst.make ~loc:!@loc @@ IntroForthcoming false ]] - ; - simple_intropattern: - [ [ pat = simple_intropattern_closed; - l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> - let {CAst.loc=loc0;v=pat} = pat in - let f c pat = - let loc1 = Constrexpr_ops.constr_loc c in - let loc = Loc.merge_opt loc0 loc1 in - IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in - CAst.make ~loc:!@loc @@ List.fold_right f l pat ] ] - ; - simple_intropattern_closed: - [ [ pat = or_and_intropattern -> CAst.make ~loc:!@loc @@ IntroAction (IntroOrAndPattern pat) - | pat = equality_intropattern -> CAst.make ~loc:!@loc @@ IntroAction pat - | "_" -> CAst.make ~loc:!@loc @@ IntroAction IntroWildcard - | pat = naming_intropattern -> CAst.make ~loc:!@loc @@ IntroNaming pat ] ] - ; - simple_binding: - [ [ "("; id = ident; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (NamedHyp id, c) - | "("; n = natural; ":="; c = lconstr; ")" -> CAst.make ~loc:!@loc (AnonHyp n, c) ] ] - ; - bindings: - [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> - ExplicitBindings bl - | bl = LIST1 constr -> ImplicitBindings bl ] ] - ; - constr_with_bindings: - [ [ c = constr; l = with_bindings -> (c, l) ] ] - ; - with_bindings: - [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] - ; - red_flags: - [ [ IDENT "beta" -> [FBeta] - | IDENT "iota" -> [FMatch;FFix;FCofix] - | IDENT "match" -> [FMatch] - | IDENT "fix" -> [FFix] - | IDENT "cofix" -> [FCofix] - | IDENT "zeta" -> [FZeta] - | IDENT "delta"; d = delta_flag -> [d] - ] ] - ; - delta_flag: - [ [ "-"; "["; idl = LIST1 smart_global; "]" -> FDeltaBut idl - | "["; idl = LIST1 smart_global; "]" -> FConst idl - | -> FDeltaBut [] - ] ] - ; - strategy_flag: - [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s) - | d = delta_flag -> all_with d - ] ] - ; - red_expr: - [ [ IDENT "red" -> Red false - | IDENT "hnf" -> Hnf - | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po) - | IDENT "cbv"; s = strategy_flag -> Cbv s - | IDENT "cbn"; s = strategy_flag -> Cbn s - | IDENT "lazy"; s = strategy_flag -> Lazy s - | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta) - | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> CbvVm po - | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> CbvNative po - | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul - | IDENT "fold"; cl = LIST1 constr -> Fold cl - | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl - | s = IDENT -> ExtraRedExpr s ] ] - ; - hypident: - [ [ id = id_or_meta -> - let id : lident = id in - id,InHyp - | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> - let id : lident = id in - id,InHypTypeOnly - | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> - let id : lident = id in - id,InHypValueOnly - ] ] - ; - hypident_occ: - [ [ (id,l)=hypident; occs=occs -> - let id : lident = id in - ((occs,id),l) ] ] - ; - in_clause: - [ [ "*"; occs=occs -> - {onhyps=None; concl_occs=occs} - | "*"; "|-"; occs=concl_occ -> - {onhyps=None; concl_occs=occs} - | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> - {onhyps=Some hl; concl_occs=occs} - | hl=LIST0 hypident_occ SEP"," -> - {onhyps=Some hl; concl_occs=NoOccurrences} ] ] - ; - clause_dft_concl: - [ [ "in"; cl = in_clause -> cl - | occs=occs -> {onhyps=Some[]; concl_occs=occs} - | -> all_concl_occs_clause ] ] - ; - clause_dft_all: - [ [ "in"; cl = in_clause -> cl - | -> {onhyps=None; concl_occs=AllOccurrences} ] ] - ; - opt_clause: - [ [ "in"; cl = in_clause -> Some cl - | "at"; occs = occs_nums -> Some {onhyps=Some[]; concl_occs=occs} - | -> None ] ] - ; - concl_occ: - [ [ "*"; occs = occs -> occs - | -> NoOccurrences ] ] - ; - in_hyp_list: - [ [ "in"; idl = LIST1 id_or_meta -> idl - | -> [] ] ] - ; - in_hyp_as: - [ [ "in"; id = id_or_meta; ipat = as_ipat -> Some (id,ipat) - | -> None ] ] - ; - orient: - [ [ "->" -> true - | "<-" -> false - | -> true ]] - ; - simple_binder: - [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ - CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c) - ] ] - ; - fixdecl: - [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; - ":"; ty=lconstr; ")" -> (!@loc, id, bl, ann, ty) ] ] - ; - fixannot: - [ [ "{"; IDENT "struct"; id=name; "}" -> Some id - | -> None ] ] - ; - cofixdecl: - [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" -> - (!@loc, id, bl, None, ty) ] ] - ; - bindings_with_parameters: - [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; - ":="; c = lconstr; ")" -> (id, mkCLambdaN_simple bl c) ] ] - ; - eliminator: - [ [ "using"; el = constr_with_bindings -> el ] ] - ; - as_ipat: - [ [ "as"; ipat = simple_intropattern -> Some ipat - | -> None ] ] - ; - or_and_intropattern_loc: - [ [ ipat = or_and_intropattern -> ArgArg (CAst.make ~loc:!@loc ipat) - | locid = identref -> ArgVar locid ] ] - ; - as_or_and_ipat: - [ [ "as"; ipat = or_and_intropattern_loc -> Some ipat - | -> None ] ] - ; - eqn_ipat: - [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> Some (CAst.make ~loc:!@loc pat) - | IDENT "_eqn"; ":"; pat = naming_intropattern -> - let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) - | IDENT "_eqn" -> - let loc = !@loc in - warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) - | -> None ] ] - ; - as_name: - [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ] - ; - by_tactic: - [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac - | -> None ] ] - ; - rewriter : - [ [ "!"; c = constr_with_bindings_arg -> (Equality.RepeatPlus,c) - | ["?"| LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.RepeatStar,c) - | n = natural; "!"; c = constr_with_bindings_arg -> (Equality.Precisely n,c) - | n = natural; ["?" | LEFTQMARK]; c = constr_with_bindings_arg -> (Equality.UpTo n,c) - | n = natural; c = constr_with_bindings_arg -> (Equality.Precisely n,c) - | c = constr_with_bindings_arg -> (Equality.Precisely 1, c) - ] ] - ; - oriented_rewriter : - [ [ b = orient; p = rewriter -> let (m,c) = p in (b,m,c) ] ] - ; - induction_clause: - [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; - cl = opt_clause -> (c,(eq,pat),cl) ] ] - ; - induction_clause_list: - [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; - cl_tolerance = opt_clause -> - (* Condition for accepting "in" at the end by compatibility *) - match ic,el,cl_tolerance with - | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el) - | _,_,Some _ -> err () - | _,_,None -> (ic,el) ]] - ; - simple_tactic: - [ [ - (* Basic tactics *) - IDENT "intros"; pl = ne_intropatterns -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,pl)) - | IDENT "intros" -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (false,[CAst.make ~loc:!@loc @@IntroForthcoming false])) - | IDENT "eintros"; pl = ne_intropatterns -> - TacAtom (Loc.tag ~loc:!@loc @@ TacIntroPattern (true,pl)) - - | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,false,cl,inhyp)) - | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (true,true,cl,inhyp)) - | IDENT "simple"; IDENT "apply"; - cl = LIST1 constr_with_bindings_arg SEP ","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,false,cl,inhyp)) - | IDENT "simple"; IDENT "eapply"; - cl = LIST1 constr_with_bindings_arg SEP","; - inhyp = in_hyp_as -> TacAtom (Loc.tag ~loc:!@loc @@ TacApply (false,true,cl,inhyp)) - | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (Loc.tag ~loc:!@loc @@ TacElim (false,cl,el)) - | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator -> - TacAtom (Loc.tag ~loc:!@loc @@ TacElim (true,cl,el)) - | IDENT "case"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase false icl) - | IDENT "ecase"; icl = induction_clause_list -> TacAtom (Loc.tag ~loc:!@loc @@ mkTacCase true icl) - | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) - | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) - - | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) - | IDENT "pose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) - | IDENT "epose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) - | IDENT "epose"; b = constr; na = as_name -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) - | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) - | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None)) - | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) - | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None)) - | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; - p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e)) - | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; - p = clause_dft_all -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e)) - - (* Alternative syntax for "pose proof c as id" *) - | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; - c = lconstr; ")" -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; - c = lconstr; ")" -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - - (* Alternative syntax for "assert c as id by tac" *) - | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; - c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; - c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - - (* Alternative syntax for "enough c as id by tac" *) - | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; - c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; - c = lconstr; ")"; tac=by_tactic -> - let { CAst.loc = loc; v = id } = lid in - TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) - - | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c)) - | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c)) - | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c)) - | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c)) - | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c)) - | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> - TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c)) - - | IDENT "generalize"; c = constr -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) - | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l))) - | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; - na = as_name; - l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (((nl,c),na)::l)) - - (* Derived basic tactics *) - | IDENT "induction"; ic = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct (true,false,ic)) - | IDENT "einduction"; ic = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(true,true,ic)) - | IDENT "destruct"; icl = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,false,icl)) - | IDENT "edestruct"; icl = induction_clause_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInductionDestruct(false,true,icl)) - - (* Equality and inversion *) - | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (false,l,cl,t)) - | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; - cl = clause_dft_concl; t=by_tactic -> TacAtom (Loc.tag ~loc:!@loc @@ TacRewrite (true,l,cl,t)) - | IDENT "dependent"; k = - [ IDENT "simple"; IDENT "inversion" -> SimpleInversion - | IDENT "inversion" -> FullInversion - | IDENT "inversion_clear" -> FullInversionClear ]; - hyp = quantified_hypothesis; - ids = as_or_and_ipat; co = OPT ["with"; c = constr -> c] -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (DepInversion (k,co,ids),hyp)) - | IDENT "simple"; IDENT "inversion"; - hyp = quantified_hypothesis; ids = as_or_and_ipat; - cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) - | IDENT "inversion"; - hyp = quantified_hypothesis; ids = as_or_and_ipat; - cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) - | IDENT "inversion_clear"; - hyp = quantified_hypothesis; ids = as_or_and_ipat; - cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) - | IDENT "inversion"; hyp = quantified_hypothesis; - "using"; c = constr; cl = in_hyp_list -> - TacAtom (Loc.tag ~loc:!@loc @@ TacInversion (InversionUsing (c,cl), hyp)) - - (* Conversion *) - | IDENT "red"; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Red false, cl)) - | IDENT "hnf"; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Hnf, cl)) - | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Simpl (all_with d, po), cl)) - | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv s, cl)) - | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbn s, cl)) - | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Lazy s, cl)) - | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Cbv (all_with delta), cl)) - | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvVm po, cl)) - | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (CbvNative po, cl)) - | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Unfold ul, cl)) - | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Fold l, cl)) - | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacReduce (Pattern pl, cl)) - - (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) - | IDENT "change"; (oc,c) = conversion; cl = clause_dft_concl -> - let p,cl = merge_occurrences (!@loc) cl oc in - TacAtom (Loc.tag ~loc:!@loc @@ TacChange (p,c,cl)) - ] ] - ; -END;; diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg new file mode 100644 index 000000000..2e1ce814a --- /dev/null +++ b/plugins/ltac/g_tactic.mlg @@ -0,0 +1,704 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* "; "<-" ; "by" ] +let _ = List.iter CLexer.add_keyword tactic_kw + +let err () = raise Stream.Failure + +(* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *) +(* admissible notation "(x t)" *) +let test_lpar_id_coloneq = + Gram.Entry.of_parser "lpar_id_coloneq" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "(" -> + (match stream_nth 1 strm with + | IDENT _ -> + (match stream_nth 2 strm with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +(* Hack to recognize "(x)" *) +let test_lpar_id_rpar = + Gram.Entry.of_parser "lpar_id_coloneq" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "(" -> + (match stream_nth 1 strm with + | IDENT _ -> + (match stream_nth 2 strm with + | KEYWORD ")" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +(* idem for (x:=t) and (1:=t) *) +let test_lpar_idnum_coloneq = + Gram.Entry.of_parser "test_lpar_idnum_coloneq" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "(" -> + (match stream_nth 1 strm with + | IDENT _ | INT _ -> + (match stream_nth 2 strm with + | KEYWORD ":=" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +(* idem for (x:t) *) +open Extraargs + +(* idem for (x1..xn:t) [n^2 complexity but exceptional use] *) +let check_for_coloneq = + Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + let rec skip_to_rpar p n = + match List.last (Stream.npeek n strm) with + | KEYWORD "(" -> skip_to_rpar (p+1) (n+1) + | KEYWORD ")" -> if Int.equal p 0 then n+1 else skip_to_rpar (p-1) (n+1) + | KEYWORD "." -> err () + | _ -> skip_to_rpar p (n+1) in + let rec skip_names n = + match List.last (Stream.npeek n strm) with + | IDENT _ | KEYWORD "_" -> skip_names (n+1) + | KEYWORD ":" -> skip_to_rpar 0 (n+1) (* skip a constr *) + | _ -> err () in + let rec skip_binders n = + match List.last (Stream.npeek n strm) with + | KEYWORD "(" -> skip_binders (skip_names (n+1)) + | IDENT _ | KEYWORD "_" -> skip_binders (n+1) + | KEYWORD ":=" -> () + | _ -> err () in + match stream_nth 0 strm with + | KEYWORD "(" -> skip_binders 2 + | _ -> err ()) + +let lookup_at_as_comma = + Gram.Entry.of_parser "lookup_at_as_comma" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD (","|"at"|"as") -> () + | _ -> err ()) + +open Constr +open Prim +open Pltac + +let mk_fix_tac (loc,id,bl,ann,ty) = + let n = + match bl,ann with + [([_],_,_)], None -> 1 + | _, Some x -> + let ids = List.map (fun x -> x.CAst.v) (List.flatten (List.map (fun (nal,_,_) -> nal) bl)) in + (try List.index Names.Name.equal x.CAst.v ids + with Not_found -> user_err Pp.(str "No such fix variable.")) + | _ -> user_err Pp.(str "Cannot guess decreasing argument of fix.") in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in + (id,n, CAst.make ~loc @@ CProdN(bl,ty)) + +let mk_cofix_tac (loc,id,bl,ann,ty) = + let _ = Option.map (fun { CAst.loc = aloc } -> + user_err ?loc:aloc + ~hdr:"Constr:mk_cofix_tac" + (Pp.str"Annotation forbidden in cofix expression.")) ann in + let bl = List.map (fun (nal,bk,t) -> CLocalAssum (nal,bk,t)) bl in + (id,CAst.make ~loc @@ CProdN(bl,ty)) + +(* Functions overloaded by quotifier *) +let destruction_arg_of_constr (c,lbind as clbind) = match lbind with + | NoBindings -> + begin + try ElimOnIdent (CAst.make ?loc:(Constrexpr_ops.constr_loc c) (Constrexpr_ops.coerce_to_id c).CAst.v) + with e when CErrors.noncritical e -> ElimOnConstr clbind + end + | _ -> ElimOnConstr clbind + +let mkNumeral n = Numeral (string_of_int (abs n), 0<=n) + +let mkTacCase with_evar = function + | [(clear,ElimOnConstr cl),(None,None),None],None -> + TacCase (with_evar,(clear,cl)) + (* Reinterpret numbers as a notation for terms *) + | [(clear,ElimOnAnonHyp n),(None,None),None],None -> + TacCase (with_evar, + (clear,(CAst.make @@ CPrim (mkNumeral n), + NoBindings))) + (* Reinterpret ident as notations for variables in the context *) + (* because we don't know if they are quantified or not *) + | [(clear,ElimOnIdent id),(None,None),None],None -> + TacCase (with_evar,(clear,(CAst.make @@ CRef (qualid_of_ident ?loc:id.CAst.loc id.CAst.v,None),NoBindings))) + | ic -> + if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic) + then + user_err Pp.(str "Use of numbers as direct arguments of 'case' is not supported."); + TacInductionDestruct (false,with_evar,ic) + +let rec mkCLambdaN_simple_loc ?loc bll c = + match bll with + | ({CAst.loc = loc1}::_ as idl,bk,t) :: bll -> + CAst.make ?loc @@ CLambdaN ([CLocalAssum (idl,bk,t)],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c) + | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c + | [] -> c + +let mkCLambdaN_simple bl c = match bl with + | [] -> c + | h :: _ -> + let loc = Loc.merge_opt (List.hd (pi1 h)).CAst.loc (Constrexpr_ops.constr_loc c) in + mkCLambdaN_simple_loc ?loc bl c + +let loc_of_ne_list l = Loc.merge_opt (List.hd l).CAst.loc (List.last l).CAst.loc + +let map_int_or_var f = function + | ArgArg x -> ArgArg (f x) + | ArgVar _ as y -> y + +let all_concl_occs_clause = { onhyps=Some[]; concl_occs=AllOccurrences } + +let merge_occurrences loc cl = function + | None -> + if Locusops.clause_with_generic_occurrences cl then (None, cl) + else + user_err ~loc (str "Found an \"at\" clause without \"with\" clause.") + | Some (occs, p) -> + let ans = match occs with + | AllOccurrences -> cl + | _ -> + begin match cl with + | { onhyps = Some []; concl_occs = AllOccurrences } -> + { onhyps = Some []; concl_occs = occs } + | { onhyps = Some [(AllOccurrences, id), l]; concl_occs = NoOccurrences } -> + { cl with onhyps = Some [(occs, id), l] } + | _ -> + if Locusops.clause_with_generic_occurrences cl then + user_err ~loc (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") + else + user_err ~loc (str "Cannot use clause \"at\" twice.") + end + in + (Some p, ans) + +let warn_deprecated_eqn_syntax = + CWarnings.create ~name:"deprecated-eqn-syntax" ~category:"deprecated" + (fun arg -> strbrk (Printf.sprintf "Syntax \"_eqn:%s\" is deprecated. Please use \"eqn:%s\" instead." arg arg)) + +(* Auxiliary grammar rules *) + +open Pvernac.Vernac_ + +} + +GRAMMAR EXTEND Gram + GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis + bindings red_expr int_or_var open_constr uconstr + simple_intropattern in_clause clause_dft_concl hypident destruction_arg; + + int_or_var: + [ [ n = integer -> { ArgArg n } + | id = identref -> { ArgVar id } ] ] + ; + nat_or_var: + [ [ n = natural -> { ArgArg n } + | id = identref -> { ArgVar id } ] ] + ; + (* An identifier or a quotation meta-variable *) + id_or_meta: + [ [ id = identref -> { id } ] ] + ; + open_constr: + [ [ c = constr -> { c } ] ] + ; + uconstr: + [ [ c = constr -> { c } ] ] + ; + destruction_arg: + [ [ n = natural -> { (None,ElimOnAnonHyp n) } + | test_lpar_id_rpar; c = constr_with_bindings -> + { (Some false,destruction_arg_of_constr c) } + | c = constr_with_bindings_arg -> { on_snd destruction_arg_of_constr c } + ] ] + ; + constr_with_bindings_arg: + [ [ ">"; c = constr_with_bindings -> { (Some true,c) } + | c = constr_with_bindings -> { (None,c) } ] ] + ; + quantified_hypothesis: + [ [ id = ident -> { NamedHyp id } + | n = natural -> { AnonHyp n } ] ] + ; + conversion: + [ [ c = constr -> { (None, c) } + | c1 = constr; "with"; c2 = constr -> { (Some (AllOccurrences,c1),c2) } + | c1 = constr; "at"; occs = occs_nums; "with"; c2 = constr -> + { (Some (occs,c1), c2) } ] ] + ; + occs_nums: + [ [ nl = LIST1 nat_or_var -> { OnlyOccurrences nl } + | "-"; n = nat_or_var; nl = LIST0 int_or_var -> + (* have used int_or_var instead of nat_or_var for compatibility *) + { AllOccurrencesBut (List.map (map_int_or_var abs) (n::nl)) } ] ] + ; + occs: + [ [ "at"; occs = occs_nums -> { occs } | -> { AllOccurrences } ] ] + ; + pattern_occ: + [ [ c = constr; nl = occs -> { (nl,c) } ] ] + ; + ref_or_pattern_occ: + (* If a string, it is interpreted as a ref + (anyway a Coq string does not reduce) *) + [ [ c = smart_global; nl = occs -> { nl,Inl c } + | c = constr; nl = occs -> { nl,Inr c } ] ] + ; + unfold_occ: + [ [ c = smart_global; nl = occs -> { (nl,c) } ] ] + ; + intropatterns: + [ [ l = LIST0 nonsimple_intropattern -> { l } ] ] + ; + ne_intropatterns: + [ [ l = LIST1 nonsimple_intropattern -> { l } ] ] + ; + or_and_intropattern: + [ [ "["; tc = LIST1 intropatterns SEP "|"; "]" -> { IntroOrPattern tc } + | "()" -> { IntroAndPattern [] } + | "("; si = simple_intropattern; ")" -> { IntroAndPattern [si] } + | "("; si = simple_intropattern; ","; + tc = LIST1 simple_intropattern SEP "," ; ")" -> + { IntroAndPattern (si::tc) } + | "("; si = simple_intropattern; "&"; + tc = LIST1 simple_intropattern SEP "&" ; ")" -> + (* (A & B & C) is translated into (A,(B,C)) *) + { let rec pairify = function + | ([]|[_]|[_;_]) as l -> l + | t::q -> [t; CAst.make ?loc:(loc_of_ne_list q) (IntroAction (IntroOrAndPattern (IntroAndPattern (pairify q))))] + in IntroAndPattern (pairify (si::tc)) } ] ] + ; + equality_intropattern: + [ [ "->" -> { IntroRewrite true } + | "<-" -> { IntroRewrite false } + | "[="; tc = intropatterns; "]" -> { IntroInjection tc } ] ] + ; + naming_intropattern: + [ [ prefix = pattern_ident -> { IntroFresh prefix } + | "?" -> { IntroAnonymous } + | id = ident -> { IntroIdentifier id } ] ] + ; + nonsimple_intropattern: + [ [ l = simple_intropattern -> { l } + | "*" -> { CAst.make ~loc @@ IntroForthcoming true } + | "**" -> { CAst.make ~loc @@ IntroForthcoming false } ] ] + ; + simple_intropattern: + [ [ pat = simple_intropattern_closed; + l = LIST0 ["%"; c = operconstr LEVEL "0" -> { c } ] -> + { let {CAst.loc=loc0;v=pat} = pat in + let f c pat = + let loc1 = Constrexpr_ops.constr_loc c in + let loc = Loc.merge_opt loc0 loc1 in + IntroAction (IntroApplyOn (CAst.(make ?loc:loc1 c),CAst.(make ?loc pat))) in + CAst.make ~loc @@ List.fold_right f l pat } ] ] + ; + simple_intropattern_closed: + [ [ pat = or_and_intropattern -> { CAst.make ~loc @@ IntroAction (IntroOrAndPattern pat) } + | pat = equality_intropattern -> { CAst.make ~loc @@ IntroAction pat } + | "_" -> { CAst.make ~loc @@ IntroAction IntroWildcard } + | pat = naming_intropattern -> { CAst.make ~loc @@ IntroNaming pat } ] ] + ; + simple_binding: + [ [ "("; id = ident; ":="; c = lconstr; ")" -> { CAst.make ~loc (NamedHyp id, c) } + | "("; n = natural; ":="; c = lconstr; ")" -> { CAst.make ~loc (AnonHyp n, c) } ] ] + ; + bindings: + [ [ test_lpar_idnum_coloneq; bl = LIST1 simple_binding -> + { ExplicitBindings bl } + | bl = LIST1 constr -> { ImplicitBindings bl } ] ] + ; + constr_with_bindings: + [ [ c = constr; l = with_bindings -> { (c, l) } ] ] + ; + with_bindings: + [ [ "with"; bl = bindings -> { bl } | -> { NoBindings } ] ] + ; + red_flags: + [ [ IDENT "beta" -> { [FBeta] } + | IDENT "iota" -> { [FMatch;FFix;FCofix] } + | IDENT "match" -> { [FMatch] } + | IDENT "fix" -> { [FFix] } + | IDENT "cofix" -> { [FCofix] } + | IDENT "zeta" -> { [FZeta] } + | IDENT "delta"; d = delta_flag -> { [d] } + ] ] + ; + delta_flag: + [ [ "-"; "["; idl = LIST1 smart_global; "]" -> { FDeltaBut idl } + | "["; idl = LIST1 smart_global; "]" -> { FConst idl } + | -> { FDeltaBut [] } + ] ] + ; + strategy_flag: + [ [ s = LIST1 red_flags -> { Redops.make_red_flag (List.flatten s) } + | d = delta_flag -> { all_with d } + ] ] + ; + red_expr: + [ [ IDENT "red" -> { Red false } + | IDENT "hnf" -> { Hnf } + | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> { Simpl (all_with d,po) } + | IDENT "cbv"; s = strategy_flag -> { Cbv s } + | IDENT "cbn"; s = strategy_flag -> { Cbn s } + | IDENT "lazy"; s = strategy_flag -> { Lazy s } + | IDENT "compute"; delta = delta_flag -> { Cbv (all_with delta) } + | IDENT "vm_compute"; po = OPT ref_or_pattern_occ -> { CbvVm po } + | IDENT "native_compute"; po = OPT ref_or_pattern_occ -> { CbvNative po } + | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> { Unfold ul } + | IDENT "fold"; cl = LIST1 constr -> { Fold cl } + | IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> { Pattern pl } + | s = IDENT -> { ExtraRedExpr s } ] ] + ; + hypident: + [ [ id = id_or_meta -> + { let id : lident = id in + id,InHyp } + | "("; IDENT "type"; IDENT "of"; id = id_or_meta; ")" -> + { let id : lident = id in + id,InHypTypeOnly } + | "("; IDENT "value"; IDENT "of"; id = id_or_meta; ")" -> + { let id : lident = id in + id,InHypValueOnly } + ] ] + ; + hypident_occ: + [ [ h=hypident; occs=occs -> + { let (id,l) = h in + let id : lident = id in + ((occs,id),l) } ] ] + ; + in_clause: + [ [ "*"; occs=occs -> + { {onhyps=None; concl_occs=occs} } + | "*"; "|-"; occs=concl_occ -> + { {onhyps=None; concl_occs=occs} } + | hl=LIST0 hypident_occ SEP","; "|-"; occs=concl_occ -> + { {onhyps=Some hl; concl_occs=occs} } + | hl=LIST0 hypident_occ SEP"," -> + { {onhyps=Some hl; concl_occs=NoOccurrences} } ] ] + ; + clause_dft_concl: + [ [ "in"; cl = in_clause -> { cl } + | occs=occs -> { {onhyps=Some[]; concl_occs=occs} } + | -> { all_concl_occs_clause } ] ] + ; + clause_dft_all: + [ [ "in"; cl = in_clause -> { cl } + | -> { {onhyps=None; concl_occs=AllOccurrences} } ] ] + ; + opt_clause: + [ [ "in"; cl = in_clause -> { Some cl } + | "at"; occs = occs_nums -> { Some {onhyps=Some[]; concl_occs=occs} } + | -> { None } ] ] + ; + concl_occ: + [ [ "*"; occs = occs -> { occs } + | -> { NoOccurrences } ] ] + ; + in_hyp_list: + [ [ "in"; idl = LIST1 id_or_meta -> { idl } + | -> { [] } ] ] + ; + in_hyp_as: + [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) } + | -> { None } ] ] + ; + orient: + [ [ "->" -> { true } + | "<-" -> { false } + | -> { true } ] ] + ; + simple_binder: + [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } + ] ] + ; + fixdecl: + [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot; + ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ] + ; + fixannot: + [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id } + | -> { None } ] ] + ; + cofixdecl: + [ [ "("; id = ident; bl=LIST0 simple_binder; ":"; ty=lconstr; ")" -> + { (loc, id, bl, None, ty) } ] ] + ; + bindings_with_parameters: + [ [ check_for_coloneq; "("; id = ident; bl = LIST0 simple_binder; + ":="; c = lconstr; ")" -> { (id, mkCLambdaN_simple bl c) } ] ] + ; + eliminator: + [ [ "using"; el = constr_with_bindings -> { el } ] ] + ; + as_ipat: + [ [ "as"; ipat = simple_intropattern -> { Some ipat } + | -> { None } ] ] + ; + or_and_intropattern_loc: + [ [ ipat = or_and_intropattern -> { ArgArg (CAst.make ~loc ipat) } + | locid = identref -> { ArgVar locid } ] ] + ; + as_or_and_ipat: + [ [ "as"; ipat = or_and_intropattern_loc -> { Some ipat } + | -> { None } ] ] + ; + eqn_ipat: + [ [ IDENT "eqn"; ":"; pat = naming_intropattern -> { Some (CAst.make ~loc pat) } + | IDENT "_eqn"; ":"; pat = naming_intropattern -> + { warn_deprecated_eqn_syntax ~loc "H"; Some (CAst.make ~loc pat) } + | IDENT "_eqn" -> + { warn_deprecated_eqn_syntax ~loc "?"; Some (CAst.make ~loc IntroAnonymous) } + | -> { None } ] ] + ; + as_name: + [ [ "as"; id = ident -> { Names.Name.Name id } | -> { Names.Name.Anonymous } ] ] + ; + by_tactic: + [ [ "by"; tac = tactic_expr LEVEL "3" -> { Some tac } + | -> { None } ] ] + ; + rewriter : + [ [ "!"; c = constr_with_bindings_arg -> { (Equality.RepeatPlus,c) } + | ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.RepeatStar,c) } + | n = natural; "!"; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) } + | n = natural; ["?" -> { () } | LEFTQMARK -> { () } ]; c = constr_with_bindings_arg -> { (Equality.UpTo n,c) } + | n = natural; c = constr_with_bindings_arg -> { (Equality.Precisely n,c) } + | c = constr_with_bindings_arg -> { (Equality.Precisely 1, c) } + ] ] + ; + oriented_rewriter : + [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ] + ; + induction_clause: + [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat; + cl = opt_clause -> { (c,(eq,pat),cl) } ] ] + ; + induction_clause_list: + [ [ ic = LIST1 induction_clause SEP ","; el = OPT eliminator; + cl_tolerance = opt_clause -> + (* Condition for accepting "in" at the end by compatibility *) + { match ic,el,cl_tolerance with + | [c,pat,None],Some _,Some _ -> ([c,pat,cl_tolerance],el) + | _,_,Some _ -> err () + | _,_,None -> (ic,el) } ] ] + ; + simple_tactic: + [ [ + (* Basic tactics *) + IDENT "intros"; pl = ne_intropatterns -> + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,pl)) } + | IDENT "intros" -> + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (false,[CAst.make ~loc @@IntroForthcoming false])) } + | IDENT "eintros"; pl = ne_intropatterns -> + { TacAtom (Loc.tag ~loc @@ TacIntroPattern (true,pl)) } + + | IDENT "apply"; cl = LIST1 constr_with_bindings_arg SEP ","; + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,false,cl,inhyp)) } + | IDENT "eapply"; cl = LIST1 constr_with_bindings_arg SEP ","; + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (true,true,cl,inhyp)) } + | IDENT "simple"; IDENT "apply"; + cl = LIST1 constr_with_bindings_arg SEP ","; + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,false,cl,inhyp)) } + | IDENT "simple"; IDENT "eapply"; + cl = LIST1 constr_with_bindings_arg SEP","; + inhyp = in_hyp_as -> { TacAtom (Loc.tag ~loc @@ TacApply (false,true,cl,inhyp)) } + | IDENT "elim"; cl = constr_with_bindings_arg; el = OPT eliminator -> + { TacAtom (Loc.tag ~loc @@ TacElim (false,cl,el)) } + | IDENT "eelim"; cl = constr_with_bindings_arg; el = OPT eliminator -> + { TacAtom (Loc.tag ~loc @@ TacElim (true,cl,el)) } + | IDENT "case"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase false icl) } + | IDENT "ecase"; icl = induction_clause_list -> { TacAtom (Loc.tag ~loc @@ mkTacCase true icl) } + | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> + { TacAtom (Loc.tag ~loc @@ TacMutualFix (id,n,List.map mk_fix_tac fd)) } + | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> + { TacAtom (Loc.tag ~loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) } + + | IDENT "pose"; bl = bindings_with_parameters -> + { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) } + | IDENT "pose"; b = constr; na = as_name -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) } + | IDENT "epose"; bl = bindings_with_parameters -> + { let (id,b) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None)) } + | IDENT "epose"; b = constr; na = as_name -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) } + | IDENT "set"; bl = bindings_with_parameters; p = clause_dft_concl -> + { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) } + | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,true,None)) } + | IDENT "eset"; bl = bindings_with_parameters; p = clause_dft_concl -> + { let (id,c) = bl in TacAtom (Loc.tag ~loc @@ TacLetTac (true,Names.Name id,c,p,true,None)) } + | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,true,None)) } + | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (false,na,c,p,false,e)) } + | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat; + p = clause_dft_all -> + { TacAtom (Loc.tag ~loc @@ TacLetTac (true,na,c,p,false,e)) } + + (* Alternative syntax for "pose proof c as id" *) + | IDENT "assert"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "eassert"; test_lpar_id_coloneq; "("; lid = identref; ":="; + c = lconstr; ")" -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,None,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + + (* Alternative syntax for "assert c as id by tac" *) + | IDENT "assert"; test_lpar_id_colon; "("; lid = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "eassert"; test_lpar_id_colon; "("; lid = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,true,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + + (* Alternative syntax for "enough c as id by tac" *) + | IDENT "enough"; test_lpar_id_colon; "("; lid = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (false,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + | IDENT "eenough"; test_lpar_id_colon; "("; lid = identref; ":"; + c = lconstr; ")"; tac=by_tactic -> + { let { CAst.loc = loc; v = id } = lid in + TacAtom (Loc.tag ?loc @@ TacAssert (true,false,Some tac,Some (CAst.make ?loc @@ IntroNaming (IntroIdentifier id)),c)) } + + | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic -> + { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,Some tac,ipat,c)) } + | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic -> + { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,Some tac,ipat,c)) } + | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> + { TacAtom (Loc.tag ~loc @@ TacAssert (false,true,None,ipat,c)) } + | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat -> + { TacAtom (Loc.tag ~loc @@ TacAssert (true,true,None,ipat,c)) } + | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic -> + { TacAtom (Loc.tag ~loc @@ TacAssert (false,false,Some tac,ipat,c)) } + | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic -> + { TacAtom (Loc.tag ~loc @@ TacAssert (true,false,Some tac,ipat,c)) } + + | IDENT "generalize"; c = constr -> + { TacAtom (Loc.tag ~loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) } + | IDENT "generalize"; c = constr; l = LIST1 constr -> + { let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in + TacAtom (Loc.tag ~loc @@ TacGeneralize (List.map gen_everywhere (c::l))) } + | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; + na = as_name; + l = LIST0 [","; c = pattern_occ; na = as_name -> { (c,na) } ] -> + { TacAtom (Loc.tag ~loc @@ TacGeneralize (((nl,c),na)::l)) } + + (* Derived basic tactics *) + | IDENT "induction"; ic = induction_clause_list -> + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct (true,false,ic)) } + | IDENT "einduction"; ic = induction_clause_list -> + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(true,true,ic)) } + | IDENT "destruct"; icl = induction_clause_list -> + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,false,icl)) } + | IDENT "edestruct"; icl = induction_clause_list -> + { TacAtom (Loc.tag ~loc @@ TacInductionDestruct(false,true,icl)) } + + (* Equality and inversion *) + | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; + cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (false,l,cl,t)) } + | IDENT "erewrite"; l = LIST1 oriented_rewriter SEP ","; + cl = clause_dft_concl; t=by_tactic -> { TacAtom (Loc.tag ~loc @@ TacRewrite (true,l,cl,t)) } + | IDENT "dependent"; k = + [ IDENT "simple"; IDENT "inversion" -> { SimpleInversion } + | IDENT "inversion" -> { FullInversion } + | IDENT "inversion_clear" -> { FullInversionClear } ]; + hyp = quantified_hypothesis; + ids = as_or_and_ipat; co = OPT ["with"; c = constr -> { c } ] -> + { TacAtom (Loc.tag ~loc @@ TacInversion (DepInversion (k,co,ids),hyp)) } + | IDENT "simple"; IDENT "inversion"; + hyp = quantified_hypothesis; ids = as_or_and_ipat; + cl = in_hyp_list -> + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (SimpleInversion, cl, ids), hyp)) } + | IDENT "inversion"; + hyp = quantified_hypothesis; ids = as_or_and_ipat; + cl = in_hyp_list -> + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversion, cl, ids), hyp)) } + | IDENT "inversion_clear"; + hyp = quantified_hypothesis; ids = as_or_and_ipat; + cl = in_hyp_list -> + { TacAtom (Loc.tag ~loc @@ TacInversion (NonDepInversion (FullInversionClear, cl, ids), hyp)) } + | IDENT "inversion"; hyp = quantified_hypothesis; + "using"; c = constr; cl = in_hyp_list -> + { TacAtom (Loc.tag ~loc @@ TacInversion (InversionUsing (c,cl), hyp)) } + + (* Conversion *) + | IDENT "red"; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Red false, cl)) } + | IDENT "hnf"; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Hnf, cl)) } + | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Simpl (all_with d, po), cl)) } + | IDENT "cbv"; s = strategy_flag; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv s, cl)) } + | IDENT "cbn"; s = strategy_flag; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbn s, cl)) } + | IDENT "lazy"; s = strategy_flag; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Lazy s, cl)) } + | IDENT "compute"; delta = delta_flag; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Cbv (all_with delta), cl)) } + | IDENT "vm_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (CbvVm po, cl)) } + | IDENT "native_compute"; po = OPT ref_or_pattern_occ; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (CbvNative po, cl)) } + | IDENT "unfold"; ul = LIST1 unfold_occ SEP ","; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Unfold ul, cl)) } + | IDENT "fold"; l = LIST1 constr; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Fold l, cl)) } + | IDENT "pattern"; pl = LIST1 pattern_occ SEP","; cl = clause_dft_concl -> + { TacAtom (Loc.tag ~loc @@ TacReduce (Pattern pl, cl)) } + + (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *) + | IDENT "change"; c = conversion; cl = clause_dft_concl -> + { let (oc, c) = c in + let p,cl = merge_occurrences loc cl oc in + TacAtom (Loc.tag ~loc @@ TacChange (p,c,cl)) } + ] ] + ; +END -- cgit v1.2.3