From 4da233a9685cd193a84def037ec18a27c9225dce Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 12 Oct 2018 09:22:56 +0200 Subject: Port remaining EXTEND ml4 files to coqpp. Almost all of ml4 were removed in the process. The only remaining files are in the test-suite and probably need a bit of fiddling with coq_makefile, and there only two really remaning ml4 files containing code. --- plugins/ltac/extraargs.ml4 | 310 --------- plugins/ltac/extraargs.mlg | 353 ++++++++++ plugins/ltac/extratactics.ml4 | 1065 ------------------------------ plugins/ltac/extratactics.mlg | 1160 +++++++++++++++++++++++++++++++++ plugins/ltac/g_auto.ml4 | 226 ------- plugins/ltac/g_auto.mlg | 249 +++++++ plugins/ltac/g_class.ml4 | 117 ---- plugins/ltac/g_class.mlg | 137 ++++ plugins/ltac/g_ltac.ml4 | 528 --------------- plugins/ltac/g_ltac.mlg | 560 ++++++++++++++++ plugins/ltac/g_obligations.ml4 | 161 ----- plugins/ltac/g_obligations.mlg | 173 +++++ plugins/ltac/g_rewrite.ml4 | 297 --------- plugins/ltac/g_rewrite.mlg | 318 +++++++++ plugins/ltac/profile_ltac_tactics.ml4 | 74 --- plugins/ltac/profile_ltac_tactics.mlg | 82 +++ 16 files changed, 3032 insertions(+), 2778 deletions(-) delete mode 100644 plugins/ltac/extraargs.ml4 create mode 100644 plugins/ltac/extraargs.mlg delete mode 100644 plugins/ltac/extratactics.ml4 create mode 100644 plugins/ltac/extratactics.mlg delete mode 100644 plugins/ltac/g_auto.ml4 create mode 100644 plugins/ltac/g_auto.mlg delete mode 100644 plugins/ltac/g_class.ml4 create mode 100644 plugins/ltac/g_class.mlg delete mode 100644 plugins/ltac/g_ltac.ml4 create mode 100644 plugins/ltac/g_ltac.mlg delete mode 100644 plugins/ltac/g_obligations.ml4 create mode 100644 plugins/ltac/g_obligations.mlg delete mode 100644 plugins/ltac/g_rewrite.ml4 create mode 100644 plugins/ltac/g_rewrite.mlg delete mode 100644 plugins/ltac/profile_ltac_tactics.ml4 create mode 100644 plugins/ltac/profile_ltac_tactics.mlg (limited to 'plugins/ltac') diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 deleted file mode 100644 index 4de27e8138..0000000000 --- a/plugins/ltac/extraargs.ml4 +++ /dev/null @@ -1,310 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Metasyntax.add_token_obj "<-"; - Metasyntax.add_token_obj "->") - "ltac_plugin" - -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient -| [ "->" ] -> [ true ] -| [ "<-" ] -> [ false ] -| [ ] -> [ true ] -END - -let pr_int _ _ _ i = Pp.int i - -let _natural = Pcoq.Prim.natural - -ARGUMENT EXTEND natural TYPED AS int PRINTED BY pr_int -| [ _natural(i) ] -> [ i ] -END - -let pr_orient = pr_orient () () () - - -let pr_int_list = Pp.pr_sequence Pp.int -let pr_int_list_full _prc _prlc _prt l = pr_int_list l - -let pr_occurrences _prc _prlc _prt l = - match l with - | ArgArg x -> pr_int_list x - | ArgVar { CAst.loc = loc; v=id } -> Id.print id - -let occurrences_of = function - | [] -> NoOccurrences - | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) - | nl -> - if List.exists (fun n -> n < 0) nl then - CErrors.user_err Pp.(str "Illegal negative occurrence number."); - OnlyOccurrences nl - -let coerce_to_int v = match Value.to_int v with - | None -> raise (CannotCoerceTo "an integer") - | Some n -> n - -let int_list_of_VList v = match Value.to_list v with -| Some l -> List.map (fun n -> coerce_to_int n) l -| _ -> raise (CannotCoerceTo "an integer") - -let interp_occs ist gl l = - match l with - | ArgArg x -> x - | ArgVar ({ CAst.v = id } as locid) -> - (try int_list_of_VList (Id.Map.find id ist.lfun) - with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) -let interp_occs ist gl l = - Tacmach.project gl , interp_occs ist gl l - -let glob_occs ist l = l - -let subst_occs evm l = l - -ARGUMENT EXTEND occurrences - TYPED AS int list - PRINTED BY pr_int_list_full - - INTERPRETED BY interp_occs - GLOBALIZED BY glob_occs - SUBSTITUTED BY subst_occs - - RAW_PRINTED BY pr_occurrences - GLOB_PRINTED BY pr_occurrences - -| [ ne_integer_list(l) ] -> [ ArgArg l ] -| [ var(id) ] -> [ ArgVar id ] -END - -let pr_occurrences = pr_occurrences () () () - -let pr_gen prc _prlc _prtac c = prc c - -let pr_globc _prc _prlc _prtac (_,glob) = - let _, env = Pfedit.get_current_context () in - Printer.pr_glob_constr_env env glob - -let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) - -let glob_glob = Tacintern.intern_constr - -let pr_lconstr _ prc _ c = prc c - -let subst_glob = Tacsubst.subst_glob_constr_and_expr - -ARGUMENT EXTEND glob - PRINTED BY pr_globc - - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob - - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ constr(c) ] -> [ c ] -END - -let l_constr = Pcoq.Constr.lconstr - -ARGUMENT EXTEND lconstr - TYPED AS constr - PRINTED BY pr_lconstr - [ l_constr(c) ] -> [ c ] -END - -ARGUMENT EXTEND lglob - TYPED AS glob - PRINTED BY pr_globc - - INTERPRETED BY interp_glob - GLOBALIZED BY glob_glob - SUBSTITUTED BY subst_glob - - RAW_PRINTED BY pr_gen - GLOB_PRINTED BY pr_gen - [ lconstr(c) ] -> [ c ] -END - -let interp_casted_constr ist gl c = - interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c - -ARGUMENT EXTEND casted_constr - TYPED AS constr - PRINTED BY pr_gen - INTERPRETED BY interp_casted_constr - [ constr(c) ] -> [ c ] -END - -type 'id gen_place= ('id * hyp_location_flag,unit) location - -type loc_place = lident gen_place -type place = Id.t gen_place - -let pr_gen_place pr_id = function - ConclLocation () -> Pp.mt () - | HypLocation (id,InHyp) -> str "in " ++ pr_id id - | HypLocation (id,InHypTypeOnly) -> - str "in (type of " ++ pr_id id ++ str ")" - | HypLocation (id,InHypValueOnly) -> - str "in (value of " ++ pr_id id ++ str ")" - -let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) -let pr_place _ _ _ = pr_gen_place Id.print -let pr_hloc = pr_loc_place () () () - -let intern_place ist = function - ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) - -let interp_place ist env sigma = function - ConclLocation () -> ConclLocation () - | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) - -let interp_place ist gl p = - Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p - -let subst_place subst pl = pl - -let warn_deprecated_instantiate_syntax = - CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" - (fun (v,v',id) -> - let s = Id.to_string id in - Pp.strbrk - ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") - ) - -ARGUMENT EXTEND hloc - PRINTED BY pr_place - INTERPRETED BY interp_place - GLOBALIZED BY intern_place - SUBSTITUTED BY subst_place - RAW_PRINTED BY pr_loc_place - GLOB_PRINTED BY pr_loc_place - [ ] -> - [ ConclLocation () ] - | [ "in" "|-" "*" ] -> - [ ConclLocation () ] -| [ "in" ident(id) ] -> - [ HypLocation ((CAst.make id),InHyp) ] -| [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Type","type",id); - HypLocation ((CAst.make id),InHypTypeOnly) ] -| [ "in" "(" "Value" "of" ident(id) ")" ] -> - [ warn_deprecated_instantiate_syntax ("Value","value",id); - HypLocation ((CAst.make id),InHypValueOnly) ] -| [ "in" "(" "type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] -| [ "in" "(" "value" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypValueOnly) ] - - END - -let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m - -ARGUMENT EXTEND rename - TYPED AS ident * ident - PRINTED BY pr_rename -| [ ident(n) "into" ident(m) ] -> [ (n, m) ] -END - -(* Julien: Mise en commun des differentes version de replace with in by *) - -let pr_by_arg_tac _prc _prlc prtac opt_c = - match opt_c with - | None -> mt () - | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) - -ARGUMENT EXTEND by_arg_tac - TYPED AS tactic_opt - PRINTED BY pr_by_arg_tac -| [ "by" tactic3(c) ] -> [ Some c ] -| [ ] -> [ None ] -END - -let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c - -let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl -let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl -let in_clause' = Pltac.in_clause - -ARGUMENT EXTEND in_clause - TYPED AS clause_dft_concl - PRINTED BY pr_in_top_clause - RAW_PRINTED BY pr_in_clause - GLOB_PRINTED BY pr_in_clause -| [ in_clause'(cl) ] -> [ cl ] -END - -let local_test_lpar_id_colon = - let err () = raise Stream.Failure in - Pcoq.Gram.Entry.of_parser "lpar_id_colon" - (fun strm -> - match Util.stream_nth 0 strm with - | Tok.KEYWORD "(" -> - (match Util.stream_nth 1 strm with - | Tok.IDENT _ -> - (match Util.stream_nth 2 strm with - | Tok.KEYWORD ":" -> () - | _ -> err ()) - | _ -> err ()) - | _ -> err ()) - -let pr_lpar_id_colon _ _ _ _ = mt () - -ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY pr_lpar_id_colon -| [ local_test_lpar_id_colon(x) ] -> [ () ] -END diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg new file mode 100644 index 0000000000..c4c4e51ecc --- /dev/null +++ b/plugins/ltac/extraargs.mlg @@ -0,0 +1,353 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Metasyntax.add_token_obj "<-"; + Metasyntax.add_token_obj "->") + "ltac_plugin" + +let pr_orient _prc _prlc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +} + +ARGUMENT EXTEND orient TYPED AS bool PRINTED BY { pr_orient } +| [ "->" ] -> { true } +| [ "<-" ] -> { false } +| [ ] -> { true } +END + +{ + +let pr_int _ _ _ i = Pp.int i + +let _natural = Pcoq.Prim.natural + +} + +ARGUMENT EXTEND natural TYPED AS int PRINTED BY { pr_int } +| [ _natural(i) ] -> { i } +END + +{ + +let pr_orient = pr_orient () () () + +let pr_int_list = Pp.pr_sequence Pp.int +let pr_int_list_full _prc _prlc _prt l = pr_int_list l + +let pr_occurrences _prc _prlc _prt l = + match l with + | ArgArg x -> pr_int_list x + | ArgVar { CAst.loc = loc; v=id } -> Id.print id + +let occurrences_of = function + | [] -> NoOccurrences + | n::_ as nl when n < 0 -> AllOccurrencesBut (List.map abs nl) + | nl -> + if List.exists (fun n -> n < 0) nl then + CErrors.user_err Pp.(str "Illegal negative occurrence number."); + OnlyOccurrences nl + +let coerce_to_int v = match Value.to_int v with + | None -> raise (CannotCoerceTo "an integer") + | Some n -> n + +let int_list_of_VList v = match Value.to_list v with +| Some l -> List.map (fun n -> coerce_to_int n) l +| _ -> raise (CannotCoerceTo "an integer") + +let interp_occs ist gl l = + match l with + | ArgArg x -> x + | ArgVar ({ CAst.v = id } as locid) -> + (try int_list_of_VList (Id.Map.find id ist.lfun) + with Not_found | CannotCoerceTo _ -> [interp_int ist locid]) +let interp_occs ist gl l = + Tacmach.project gl , interp_occs ist gl l + +let glob_occs ist l = l + +let subst_occs evm l = l + +} + +ARGUMENT EXTEND occurrences + TYPED AS int list + PRINTED BY { pr_int_list_full } + + INTERPRETED BY { interp_occs } + GLOBALIZED BY { glob_occs } + SUBSTITUTED BY { subst_occs } + + RAW_PRINTED BY { pr_occurrences } + GLOB_PRINTED BY { pr_occurrences } + +| [ ne_integer_list(l) ] -> { ArgArg l } +| [ var(id) ] -> { ArgVar id } +END + +{ + +let pr_occurrences = pr_occurrences () () () + +let pr_gen prc _prlc _prtac c = prc c + +let pr_globc _prc _prlc _prtac (_,glob) = + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env glob + +let interp_glob ist gl (t,_) = Tacmach.project gl , (ist,t) + +let glob_glob = Tacintern.intern_constr + +let pr_lconstr _ prc _ c = prc c + +let subst_glob = Tacsubst.subst_glob_constr_and_expr + +} + +ARGUMENT EXTEND glob + PRINTED BY { pr_globc } + + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } + + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ constr(c) ] -> { c } +END + +{ + +let l_constr = Pcoq.Constr.lconstr + +} + +ARGUMENT EXTEND lconstr + TYPED AS constr + PRINTED BY { pr_lconstr } +| [ l_constr(c) ] -> { c } +END + +ARGUMENT EXTEND lglob + TYPED AS glob + PRINTED BY { pr_globc } + + INTERPRETED BY { interp_glob } + GLOBALIZED BY { glob_glob } + SUBSTITUTED BY { subst_glob } + + RAW_PRINTED BY { pr_gen } + GLOB_PRINTED BY { pr_gen } +| [ lconstr(c) ] -> { c } +END + +{ + +let interp_casted_constr ist gl c = + interp_constr_gen (Pretyping.OfType (pf_concl gl)) ist (pf_env gl) (project gl) c + +} + +ARGUMENT EXTEND casted_constr + TYPED AS constr + PRINTED BY { pr_gen } + INTERPRETED BY { interp_casted_constr } +| [ constr(c) ] -> { c } +END + +{ + +type 'id gen_place= ('id * hyp_location_flag,unit) location + +type loc_place = lident gen_place +type place = Id.t gen_place + +let pr_gen_place pr_id = function + ConclLocation () -> Pp.mt () + | HypLocation (id,InHyp) -> str "in " ++ pr_id id + | HypLocation (id,InHypTypeOnly) -> + str "in (type of " ++ pr_id id ++ str ")" + | HypLocation (id,InHypValueOnly) -> + str "in (value of " ++ pr_id id ++ str ")" + +let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) +let pr_place _ _ _ = pr_gen_place Id.print +let pr_hloc = pr_loc_place () () () + +let intern_place ist = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (Tacintern.intern_hyp ist id,hl) + +let interp_place ist env sigma = function + ConclLocation () -> ConclLocation () + | HypLocation (id,hl) -> HypLocation (Tacinterp.interp_hyp ist env sigma id,hl) + +let interp_place ist gl p = + Tacmach.project gl , interp_place ist (Tacmach.pf_env gl) (Tacmach.project gl) p + +let subst_place subst pl = pl + +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + +} + +ARGUMENT EXTEND hloc + PRINTED BY { pr_place } + INTERPRETED BY { interp_place } + GLOBALIZED BY { intern_place } + SUBSTITUTED BY { subst_place } + RAW_PRINTED BY { pr_loc_place } + GLOB_PRINTED BY { pr_loc_place } +| [ ] -> + { ConclLocation () } + | [ "in" "|-" "*" ] -> + { ConclLocation () } +| [ "in" ident(id) ] -> + { HypLocation ((CAst.make id),InHyp) } +| [ "in" "(" "Type" "of" ident(id) ")" ] -> + { warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) } +| [ "in" "(" "Value" "of" ident(id) ")" ] -> + { warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) } +| [ "in" "(" "type" "of" ident(id) ")" ] -> + { HypLocation ((CAst.make id),InHypTypeOnly) } +| [ "in" "(" "value" "of" ident(id) ")" ] -> + { HypLocation ((CAst.make id),InHypValueOnly) } + + END + +{ + +let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m + +} + +ARGUMENT EXTEND rename + TYPED AS (ident * ident) + PRINTED BY { pr_rename } +| [ ident(n) "into" ident(m) ] -> { (n, m) } +END + +(* Julien: Mise en commun des differentes version de replace with in by *) + +{ + +let pr_by_arg_tac _prc _prlc prtac opt_c = + match opt_c with + | None -> mt () + | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t) + +} + +ARGUMENT EXTEND by_arg_tac + TYPED AS tactic option + PRINTED BY { pr_by_arg_tac } +| [ "by" tactic3(c) ] -> { Some c } +| [ ] -> { None } +END + +{ + +let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c + +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl +let in_clause' = Pltac.in_clause + +} + +ARGUMENT EXTEND in_clause + TYPED AS clause_dft_concl + PRINTED BY { pr_in_top_clause } + RAW_PRINTED BY { pr_in_clause } + GLOB_PRINTED BY { pr_in_clause } +| [ in_clause'(cl) ] -> { cl } +END + +{ + +let local_test_lpar_id_colon = + let err () = raise Stream.Failure in + Pcoq.Gram.Entry.of_parser "lpar_id_colon" + (fun strm -> + match Util.stream_nth 0 strm with + | Tok.KEYWORD "(" -> + (match Util.stream_nth 1 strm with + | Tok.IDENT _ -> + (match Util.stream_nth 2 strm with + | Tok.KEYWORD ":" -> () + | _ -> err ()) + | _ -> err ()) + | _ -> err ()) + +let pr_lpar_id_colon _ _ _ _ = mt () + +} + +ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon } +| [ local_test_lpar_id_colon(x) ] -> { () } +END diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 deleted file mode 100644 index e5b032e638..0000000000 --- a/plugins/ltac/extratactics.ml4 +++ /dev/null @@ -1,1065 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) - -let replace_term ist dir_opt c cl = - with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) - -TACTIC EXTEND replace - ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] --> [ replace_in_clause_maybe_by ist c1 c2 cl tac ] -END - -TACTIC EXTEND replace_term_left - [ "replace" "->" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some true) c cl ] -END - -TACTIC EXTEND replace_term_right - [ "replace" "<-" uconstr(c) clause(cl) ] - -> [ replace_term ist (Some false) c cl ] -END - -TACTIC EXTEND replace_term - [ "replace" uconstr(c) clause(cl) ] - -> [ replace_term ist None c cl ] -END - -let induction_arg_of_quantified_hyp = function - | AnonHyp n -> None,ElimOnAnonHyp n - | NamedHyp id -> None,ElimOnIdent (CAst.make id) - -(* Versions *_main must come first!! so that "1" is interpreted as a - ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a - ElimOnIdent and not as "constr" *) - -let mytclWithHoles tac with_evars c = - Proofview.Goal.enter begin fun gl -> - let env = Tacmach.New.pf_env gl in - let sigma = Tacmach.New.project gl in - let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in - Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' - end - -let elimOnConstrWithHoles tac with_evars c = - Tacticals.New.tclDELAYEDWITHHOLES with_evars c - (fun c -> tac with_evars (Some (None,ElimOnConstr c))) - -TACTIC EXTEND simplify_eq - [ "simplify_eq" ] -> [ dEq ~keep_proofs:None false None ] -| [ "simplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) false c ] -END -TACTIC EXTEND esimplify_eq -| [ "esimplify_eq" ] -> [ dEq ~keep_proofs:None true None ] -| [ "esimplify_eq" destruction_arg(c) ] -> [ mytclWithHoles (dEq ~keep_proofs:None) true c ] -END - -let discr_main c = elimOnConstrWithHoles discr_tac false c - -TACTIC EXTEND discriminate -| [ "discriminate" ] -> [ discr_tac false None ] -| [ "discriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac false c ] -END -TACTIC EXTEND ediscriminate -| [ "ediscriminate" ] -> [ discr_tac true None ] -| [ "ediscriminate" destruction_arg(c) ] -> - [ mytclWithHoles discr_tac true c ] -END - -let discrHyp id = - Proofview.tclEVARMAP >>= fun sigma -> - discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) - -let injection_main with_evars c = - elimOnConstrWithHoles (injClause None None) with_evars c - -TACTIC EXTEND injection -| [ "injection" ] -> [ injClause None None false None ] -| [ "injection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) false c ] -END -TACTIC EXTEND einjection -| [ "einjection" ] -> [ injClause None None true None ] -| [ "einjection" destruction_arg(c) ] -> [ mytclWithHoles (injClause None None) true c ] -END -TACTIC EXTEND injection_as -| [ "injection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) false None ] -| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) false c ] -END -TACTIC EXTEND einjection_as -| [ "einjection" "as" intropattern_list(ipat)] -> - [ injClause None (Some ipat) true None ] -| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - [ mytclWithHoles (injClause None (Some ipat)) true c ] -END -TACTIC EXTEND simple_injection -| [ "simple" "injection" ] -> [ simpleInjClause None false None ] -| [ "simple" "injection" destruction_arg(c) ] -> [ mytclWithHoles (simpleInjClause None) false c ] -END - -let injHyp id = - Proofview.tclEVARMAP >>= fun sigma -> - injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) - -TACTIC EXTEND dependent_rewrite -| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] -| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] - -> [ rewriteInHyp b c id ] -END - -(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to - "replace u with t" or "enough (t=u) as <-" and - "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) - -TACTIC EXTEND cut_rewrite -| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ] -| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] - -> [ cutRewriteInHyp b eqn id ] -END - -(**********************************************************************) -(* Decompose *) - -TACTIC EXTEND decompose_sum -| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ] -END - -TACTIC EXTEND decompose_record -| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ] -END - -(**********************************************************************) -(* Contradiction *) - -open Contradiction - -TACTIC EXTEND absurd - [ "absurd" constr(c) ] -> [ absurd c ] -END - -let onSomeWithHoles tac = function - | None -> tac None - | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) - -TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> - [ onSomeWithHoles contradiction c ] -END - -(**********************************************************************) -(* AutoRewrite *) - -open Autorewrite - -let pr_orient _prc _prlc _prt = function - | true -> Pp.mt () - | false -> Pp.str " <-" - -let pr_orient_string _prc _prlc _prt (orient, s) = - pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s - -ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY pr_orient_string -| [ orient(r) preident(i) ] -> [ r, i ] -END - -TACTIC EXTEND autorewrite -| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite l ( cl) ] -| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ - auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl - ] -END - -TACTIC EXTEND autorewrite_star -| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> - [ auto_multi_rewrite ~conds:AllMatches l cl ] -| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> - [ auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl ] -END - -(**********************************************************************) -(* Rewrite star *) - -let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = - let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in - with_delayed_uconstr ist c - (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) - -TACTIC EXTEND rewrite_star -| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] -> - [ rewrite_star ist (Some id) o Locus.AllOccurrences c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> - [ rewrite_star ist None o (occurrences_of occ) c tac ] -| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] -> - [ rewrite_star ist None o Locus.AllOccurrences c tac ] - END - -(**********************************************************************) -(* Hint Rewrite *) - -let add_rewrite_hint ~poly bases ort t lcsr = - let env = Global.env() in - let sigma = Evd.from_env env in - let f ce = - let c, ctx = Constrintern.interp_constr env sigma ce in - let c = EConstr.to_constr sigma c in - let ctx = - let ctx = UState.context_set ctx in - if poly then ctx - else (** This is a global universe context that shouldn't be - refreshed at every use of the hint, declare it globally. *) - (Declare.declare_universe_context false ctx; - Univ.ContextSet.empty) - in - CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in - let eqs = List.map f lcsr in - let add_hints base = add_rew_rules base eqs in - List.iter add_hints bases - -let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater - -VERNAC COMMAND FUNCTIONAL EXTEND HintRewrite CLASSIFIED BY classify_hint - [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o None l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) - ":" preident_list(bl) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l; st ] -| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> - [ fun ~atts ~st -> add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l; st ] -END - -(**********************************************************************) -(* Refine *) - -open EConstr -open Vars - -let constr_flags () = { - Pretyping.use_typeclasses = true; - Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); - Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); - Pretyping.fail_evar = false; - Pretyping.expand_evars = true } - -let refine_tac ist simple with_classes c = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - let flags = - { constr_flags () with Pretyping.use_typeclasses = with_classes } in - let expected_type = Pretyping.OfType concl in - let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in - let update = begin fun sigma -> - c env sigma - end in - let refine = Refine.refine ~typecheck:false update in - if simple then refine - else refine <*> - Tactics.New.reduce_after_refine <*> - Proofview.shelve_unifiable - end - -TACTIC EXTEND refine -| [ "refine" uconstr(c) ] -> - [ refine_tac ist false true c ] -END - -TACTIC EXTEND simple_refine -| [ "simple" "refine" uconstr(c) ] -> - [ refine_tac ist true true c ] -END - -TACTIC EXTEND notcs_refine -| [ "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist false false c ] -END - -TACTIC EXTEND notcs_simple_refine -| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> - [ refine_tac ist true false c ] -END - -(* Solve unification constraints using heuristics or fail if any remain *) -TACTIC EXTEND solve_constraints -[ "solve_constraints" ] -> [ Refine.solve_constraints ] -END - -(**********************************************************************) -(* Inversion lemmas (Leminv) *) - -open Inv -open Leminv - -let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater - -(*VERNAC ARGUMENT EXTEND sort_family -| [ "Set" ] -> [ InSet ] -| [ "Prop" ] -> [ InProp ] -| [ "Type" ] -> [ InType ] -END*) - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversionClear -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac; st ] - -| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveInversion -| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac; st ] - -| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversion -| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac; st ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND DeriveDependentInversionClear -| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] - => [ seff na ] - -> [ fun ~atts ~st -> - let open Vernacinterp in - add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac; st ] -END - -(**********************************************************************) -(* Subst *) - -TACTIC EXTEND subst -| [ "subst" ne_var_list(l) ] -> [ subst l ] -| [ "subst" ] -> [ subst_all () ] -END - -let simple_subst_tactic_flags = - { only_leibniz = true; rewrite_dependent_proof = false } - -TACTIC EXTEND simple_subst -| [ "simple" "subst" ] -> [ subst_all ~flags:simple_subst_tactic_flags () ] -END - -open Evar_tactics - -(**********************************************************************) -(* Evar creation *) - -(* TODO: add support for some test similar to g_constr.name_colon so that - expressions like "evar (list A)" do not raise a syntax error *) -TACTIC EXTEND evar - [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ] -| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ] -END - -TACTIC EXTEND instantiate - [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> - [ Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals ] -| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> - [ Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals ] -| [ "instantiate" ] -> [ Proofview.V82.nf_evar_goals ] -END - -(**********************************************************************) -(** Nijmegen "step" tactic for setoid rewriting *) - -open Tactics -open Glob_term -open Libobject -open Lib - -(* Registered lemmas are expected to be of the form - x R y -> y == z -> x R z (in the right table) - x R y -> x == z -> z R y (in the left table) -*) - -let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" -let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" - -(* [step] tries to apply a rewriting lemma; then apply [tac] intended to - complete to proof of the last hypothesis (assumed to state an equality) *) - -let step left x tac = - let l = - List.map (fun lem -> - let lem = EConstr.of_constr lem in - Tacticals.New.tclTHENLAST - (apply_with_bindings (lem, ImplicitBindings [x])) - tac) - !(if left then transitivity_left_table else transitivity_right_table) - in - Tacticals.New.tclFIRST l - -(* Main function to push lemmas in persistent environment *) - -let cache_transitivity_lemma (_,(left,lem)) = - if left then - transitivity_left_table := lem :: !transitivity_left_table - else - transitivity_right_table := lem :: !transitivity_right_table - -let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) - -let inTransitivity : bool * Constr.t -> obj = - declare_object {(default_object "TRANSITIVITY-STEPS") with - cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); - subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o) } - -(* Main entry points *) - -let add_transitivity_lemma left lem = - let env = Global.env () in - let sigma = Evd.from_env env in - let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in - let lem' = EConstr.to_constr sigma lem' in - add_anonymous_leaf (inTransitivity (left,lem')) - -(* Vernacular syntax *) - -TACTIC EXTEND stepl -| ["stepl" constr(c) "by" tactic(tac) ] -> [ step true c (Tacinterp.tactic_of_value ist tac) ] -| ["stepl" constr(c) ] -> [ step true c (Proofview.tclUNIT ()) ] -END - -TACTIC EXTEND stepr -| ["stepr" constr(c) "by" tactic(tac) ] -> [ step false c (Tacinterp.tactic_of_value ist tac) ] -| ["stepr" constr(c) ] -> [ step false c (Proofview.tclUNIT ()) ] -END - -VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF -| [ "Declare" "Left" "Step" constr(t) ] -> - [ add_transitivity_lemma true t ] -END - -VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF -| [ "Declare" "Right" "Step" constr(t) ] -> - [ add_transitivity_lemma false t ] -END - -let cache_implicit_tactic (_,tac) = match tac with - | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) - | None -> Pfedit.clear_implicit_tactic () - -let subst_implicit_tactic (subst,tac) = - Option.map (Tacsubst.subst_tactic subst) tac - -let inImplicitTactic : glob_tactic_expr option -> obj = - declare_object {(default_object "IMPLICIT-TACTIC") with - open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); - cache_function = cache_implicit_tactic; - subst_function = subst_implicit_tactic; - classify_function = (fun o -> Dispose)} - -let warn_deprecated_implicit_tactic = - CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" - (fun () -> strbrk "Implicit tactics are deprecated") - -let declare_implicit_tactic tac = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) - -let clear_implicit_tactic () = - let () = warn_deprecated_implicit_tactic () in - Lib.add_anonymous_leaf (inImplicitTactic None) - -VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] -| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] -END - - - - -(**********************************************************************) -(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as - defined by Conor McBride *) -TACTIC EXTEND generalize_eqs -| ["generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false id ] -END -TACTIC EXTEND dep_generalize_eqs -| ["dependent" "generalize_eqs" hyp(id) ] -> [ abstract_generalize ~generalize_vars:false ~force_dep:true id ] -END -TACTIC EXTEND generalize_eqs_vars -| ["generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~generalize_vars:true id ] -END -TACTIC EXTEND dep_generalize_eqs_vars -| ["dependent" "generalize_eqs_vars" hyp(id) ] -> [ abstract_generalize ~force_dep:true ~generalize_vars:true id ] -END - -(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] - where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated - during dependent induction. For internal use. *) - -TACTIC EXTEND specialize_eqs -[ "specialize_eqs" hyp(id) ] -> [ specialize_eqs id ] -END - -(**********************************************************************) -(* A tactic that considers a given occurrence of [c] in [t] and *) -(* abstract the minimal set of all the occurrences of [c] so that the *) -(* abstraction [fun x -> t[x/c]] is well-typed *) -(* *) -(* Contributed by Chung-Kil Hur (Winter 2009) *) -(**********************************************************************) - -let subst_var_with_hole occ tid t = - let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in - let locref = ref 0 in - let rec substrec x = match DAst.get x with - | GVar id -> - if Id.equal id tid - then - (decr occref; - if Int.equal !occref 0 then x - else - (incr locref; - DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }, IntroAnonymous, None))) - else x - | _ -> map_glob_constr_left_to_right substrec x in - let t' = substrec t - in - if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' - -let subst_hole_with_term occ tc t = - let locref = ref 0 in - let occref = ref occ in - let rec substrec c = match DAst.get c with - | GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - }, IntroAnonymous, s) -> - decr occref; - if Int.equal !occref 0 then tc - else - (incr locref; - DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ - GHole (Evar_kinds.QuestionMark { - Evar_kinds.qm_obligation=Evar_kinds.Define true; - Evar_kinds.qm_name=Anonymous; - Evar_kinds.qm_record_field=None; - },IntroAnonymous,s)) - | _ -> map_glob_constr_left_to_right substrec c - in - substrec t - -open Tacmach - -let hResolve id c occ t = - Proofview.Goal.enter begin fun gl -> - let sigma = Proofview.Goal.sigma gl in - let env = Termops.clear_named_body id (Proofview.Goal.env gl) in - let concl = Proofview.Goal.concl gl in - let env_ids = Termops.vars_of_env env in - let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in - let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in - let rec resolve_hole t_hole = - try - Pretyping.understand env sigma t_hole - with - | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> - let (e, info) = CErrors.push e in - let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in - resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) - in - let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in - let sigma = Evd.merge_universe_context sigma ctx in - let t_constr_type = Retyping.get_type_of env sigma t_constr in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) - end - -let hResolve_auto id c t = - let rec resolve_auto n = - try - hResolve id c n t - with - | UserError _ as e -> raise e - | e when CErrors.noncritical e -> resolve_auto (n+1) - in - resolve_auto 1 - -TACTIC EXTEND hresolve_core -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> [ hResolve id c occ t ] -| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> [ hResolve_auto id c t ] -END - -(** - hget_evar -*) - -TACTIC EXTEND hget_evar -| [ "hget_evar" int_or_var(n) ] -> [ Evar_tactics.hget_evar n ] -END - -(**********************************************************************) - -(**********************************************************************) -(* A tactic that reduces one match t with ... by doing destruct t. *) -(* if t is not a variable, the tactic does *) -(* case_eq t;intros ... heq;rewrite heq in *|-. (but heq itself is *) -(* preserved). *) -(* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) -(**********************************************************************) - -exception Found of unit Proofview.tactic - -let rewrite_except h = - Proofview.Goal.enter begin fun gl -> - let hyps = Tacmach.New.pf_ids_of_hyps gl in - Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else - Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) - hyps - end - - -let refl_equal () = Coqlib.lib_ref "core.eq.type" - -(* This is simply an implementation of the case_eq tactic. this code - should be replaced by a call to the tactic but I don't know how to - call it before it is defined. *) -let mkCaseEq a : unit Proofview.tactic = - Proofview.Goal.enter begin fun gl -> - let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in - Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> - Tacticals.New.tclTHENLIST - [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let env = Proofview.Goal.env gl in - (** FIXME: this looks really wrong. Does anybody really use this tactic? *) - let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in - change_concl c - end; - simplest_case a] - end - - -let case_eq_intros_rewrite x = - Proofview.Goal.enter begin fun gl -> - let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in - (* Pp.msgnl (Printer.pr_lconstr x); *) - Tacticals.New.tclTHENLIST [ - mkCaseEq x; - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let hyps = Tacmach.New.pf_ids_set_of_hyps gl in - let n' = nb_prod (Tacmach.New.project gl) concl in - let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in - Tacticals.New.tclTHENLIST [ - Tacticals.New.tclDO (n'-n-1) intro; - introduction h; - rewrite_except h] - end - ] - end - -let rec find_a_destructable_match sigma t = - let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in - let cl = [cl, (None, None), None], None in - let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in - match EConstr.kind sigma t with - | Case (_,_,x,_) when closed0 sigma x -> - if isVar sigma x then - (* TODO check there is no rel n. *) - raise (Found (Tacinterp.eval_tactic dest)) - else - (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) - raise (Found (case_eq_intros_rewrite x)) - | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t - - -let destauto t = - Proofview.tclEVARMAP >>= fun sigma -> - try find_a_destructable_match sigma t; - Tacticals.New.tclZEROMSG (str "No destructable match found") - with Found tac -> tac - -let destauto_in id = - Proofview.Goal.enter begin fun gl -> - let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in -(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) -(* Pp.msgnl (Printer.pr_lconstr (ctype)); *) - destauto ctype - end - -TACTIC EXTEND destauto -| [ "destauto" ] -> [ Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end ] -| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ] -END - -(**********************************************************************) - -(**********************************************************************) -(* A version of abstract constructing transparent terms *) -(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) -(**********************************************************************) - -TACTIC EXTEND transparent_abstract -| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ] -| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl -> - Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ] -END - -(* ********************************************************************* *) - -TACTIC EXTEND constr_eq -| [ "constr_eq" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:false x y ] -END - -TACTIC EXTEND constr_eq_strict -| [ "constr_eq_strict" constr(x) constr(y) ] -> [ Tactics.constr_eq ~strict:true x y ] -END - -TACTIC EXTEND constr_eq_nounivs -| [ "constr_eq_nounivs" constr(x) constr(y) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") ] -END - -TACTIC EXTEND is_evar -| [ "is_evar" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Evar _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") - ] -END - -TACTIC EXTEND has_evar -| [ "has_evar" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - if Evarutil.has_undefined_evars sigma x - then Proofview.tclUNIT () - else Tacticals.New.tclFAIL 0 (str "No evars") -] -END - -TACTIC EXTEND is_hyp -| [ "is_var" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Var _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") ] -END - -TACTIC EXTEND is_fix -| [ "is_fix" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Fix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") ] -END;; - -TACTIC EXTEND is_cofix -| [ "is_cofix" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | CoFix _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") ] -END;; - -TACTIC EXTEND is_ind -| [ "is_ind" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Ind _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") ] -END;; - -TACTIC EXTEND is_constructor -| [ "is_constructor" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Construct _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") ] -END;; - -TACTIC EXTEND is_proj -| [ "is_proj" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Proj _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") ] -END;; - -TACTIC EXTEND is_const -| [ "is_const" constr(x) ] -> [ - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma x with - | Const _ -> Proofview.tclUNIT () - | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") ] -END;; - -(* Command to grab the evars left unresolved at the end of a proof. *) -(* spiwack: I put it in extratactics because it is somewhat tied with - the semantics of the LCF-style tactics, hence with the classic tactic - mode. *) -VERNAC COMMAND EXTEND GrabEvars -[ "Grab" "Existential" "Variables" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) ] -END - -(* Shelves all the goals under focus. *) -TACTIC EXTEND shelve -| [ "shelve" ] -> - [ Proofview.shelve ] -END - -(* Shelves the unifiable goals under focus, i.e. the goals which - appear in other goals under focus (the unfocused goals are not - considered). *) -TACTIC EXTEND shelve_unifiable -| [ "shelve_unifiable" ] -> - [ Proofview.shelve_unifiable ] -END - -(* Unshelves the goal shelved by the tactic. *) -TACTIC EXTEND unshelve -| [ "unshelve" tactic1(t) ] -> - [ - Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> - let gls = List.map Proofview.with_empty_state gls in - Proofview.Unsafe.tclGETGOALS >>= fun ogls -> - Proofview.Unsafe.tclSETGOALS (gls @ ogls) - ] -END - -(* Command to add every unshelved variables to the focus *) -VERNAC COMMAND EXTEND Unshelve -[ "Unshelve" ] - => [ Vernac_classifier.classify_as_proofstep ] - -> [ Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) ] -END - -(* Gives up on the goals under focus: the goals are considered solved, - but the proof cannot be closed until the user goes back and solve - these goals. *) -TACTIC EXTEND give_up -| [ "give_up" ] -> - [ Proofview.give_up ] -END - -(* cycles [n] goals *) -TACTIC EXTEND cycle -| [ "cycle" int_or_var(n) ] -> [ Proofview.cycle n ] -END - -(* swaps goals number [i] and [j] *) -TACTIC EXTEND swap -| [ "swap" int_or_var(i) int_or_var(j) ] -> [ Proofview.swap i j ] -END - -(* reverses the list of focused goals *) -TACTIC EXTEND revgoals -| [ "revgoals" ] -> [ Proofview.revgoals ] -END - -type cmp = - | Eq - | Lt | Le - | Gt | Ge - -type 'i test = - | Test of cmp * 'i * 'i - -let pr_cmp = function - | Eq -> Pp.str"=" - | Lt -> Pp.str"<" - | Le -> Pp.str"<=" - | Gt -> Pp.str">" - | Ge -> Pp.str">=" - -let pr_cmp' _prc _prlc _prt = pr_cmp - -let pr_test_gen f (Test(c,x,y)) = - Pp.(f x ++ pr_cmp c ++ f y) - -let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) - -let pr_test' _prc _prlc _prt = pr_test - -let pr_itest = pr_test_gen Pp.int - -let pr_itest' _prc _prlc _prt = pr_itest - - - -ARGUMENT EXTEND comparison PRINTED BY pr_cmp' -| [ "=" ] -> [ Eq ] -| [ "<" ] -> [ Lt ] -| [ "<=" ] -> [ Le ] -| [ ">" ] -> [ Gt ] -| [ ">=" ] -> [ Ge ] - END - -let interp_test ist gls = function - | Test (c,x,y) -> - project gls , - Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) - -ARGUMENT EXTEND test - PRINTED BY pr_itest' - INTERPRETED BY interp_test - RAW_PRINTED BY pr_test' - GLOB_PRINTED BY pr_test' -| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ] -END - -let interp_cmp = function - | Eq -> Int.equal - | Lt -> ((<):int->int->bool) - | Le -> ((<=):int->int->bool) - | Gt -> ((>):int->int->bool) - | Ge -> ((>=):int->int->bool) - -let run_test = function - | Test(c,x,y) -> interp_cmp c x y - -let guard tst = - if run_test tst then - Proofview.tclUNIT () - else - let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in - Tacticals.New.tclZEROMSG msg - - -TACTIC EXTEND guard -| [ "guard" test(tst) ] -> [ guard tst ] -END - -let decompose l c = - Proofview.Goal.enter begin fun gl -> - let sigma = Tacmach.New.project gl in - let to_ind c = - if isInd sigma c then fst (destInd sigma c) - else user_err Pp.(str "not an inductive type") - in - let l = List.map to_ind l in - Elim.h_decompose l c - end - -TACTIC EXTEND decompose -| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ] -END - -(** library/keys *) - -VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF -| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [ - let get_key c = - let env = Global.env () in - let evd = Evd.from_env env in - let (evd, c) = Constrintern.interp_open_constr env evd c in - let kind c = EConstr.kind evd c in - Keys.constr_key kind c - in - let k1 = get_key c in - let k2 = get_key c' in - match k1, k2 with - | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 - | _ -> () ] -END - -VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY -| [ "Print" "Equivalent" "Keys" ] -> [ Feedback.msg_info (Keys.pr_keys Printer.pr_global) ] -END - - -VERNAC COMMAND EXTEND OptimizeProof -| [ "Optimize" "Proof" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Proof_global.compact_the_proof () ] -| [ "Optimize" "Heap" ] => [ Vernac_classifier.classify_as_proofstep ] -> - [ Gc.compact () ] -END - -(** tactic analogous to "OPTIMIZE HEAP" *) - -let tclOPTIMIZE_HEAP = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) - -TACTIC EXTEND optimize_heap -| [ "optimize_heap" ] -> [ tclOPTIMIZE_HEAP ] -END diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg new file mode 100644 index 0000000000..b660865e8b --- /dev/null +++ b/plugins/ltac/extratactics.mlg @@ -0,0 +1,1160 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* replace_in_clause_maybe_by c1 c2 cl (Option.map (Tacinterp.tactic_of_value ist) tac)) + +let replace_term ist dir_opt c cl = + with_delayed_uconstr ist c (fun c -> replace_term dir_opt c cl) + +} + +TACTIC EXTEND replace +| ["replace" uconstr(c1) "with" constr(c2) clause(cl) by_arg_tac(tac) ] +-> { replace_in_clause_maybe_by ist c1 c2 cl tac } +END + +TACTIC EXTEND replace_term_left +| [ "replace" "->" uconstr(c) clause(cl) ] + -> { replace_term ist (Some true) c cl } +END + +TACTIC EXTEND replace_term_right +| [ "replace" "<-" uconstr(c) clause(cl) ] + -> { replace_term ist (Some false) c cl } +END + +TACTIC EXTEND replace_term +| [ "replace" uconstr(c) clause(cl) ] + -> { replace_term ist None c cl } +END + +{ + +let induction_arg_of_quantified_hyp = function + | AnonHyp n -> None,ElimOnAnonHyp n + | NamedHyp id -> None,ElimOnIdent (CAst.make id) + +(* Versions *_main must come first!! so that "1" is interpreted as a + ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a + ElimOnIdent and not as "constr" *) + +let mytclWithHoles tac with_evars c = + Proofview.Goal.enter begin fun gl -> + let env = Tacmach.New.pf_env gl in + let sigma = Tacmach.New.project gl in + let sigma',c = Tactics.force_destruction_arg with_evars env sigma c in + Tacticals.New.tclWITHHOLES with_evars (tac with_evars (Some c)) sigma' + end + +let elimOnConstrWithHoles tac with_evars c = + Tacticals.New.tclDELAYEDWITHHOLES with_evars c + (fun c -> tac with_evars (Some (None,ElimOnConstr c))) + +} + +TACTIC EXTEND simplify_eq +| [ "simplify_eq" ] -> { dEq ~keep_proofs:None false None } +| [ "simplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) false c } +END +TACTIC EXTEND esimplify_eq +| [ "esimplify_eq" ] -> { dEq ~keep_proofs:None true None } +| [ "esimplify_eq" destruction_arg(c) ] -> { mytclWithHoles (dEq ~keep_proofs:None) true c } +END + +{ + +let discr_main c = elimOnConstrWithHoles discr_tac false c + +} + +TACTIC EXTEND discriminate +| [ "discriminate" ] -> { discr_tac false None } +| [ "discriminate" destruction_arg(c) ] -> + { mytclWithHoles discr_tac false c } +END +TACTIC EXTEND ediscriminate +| [ "ediscriminate" ] -> { discr_tac true None } +| [ "ediscriminate" destruction_arg(c) ] -> + { mytclWithHoles discr_tac true c } +END + +{ + +let discrHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + discr_main (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) + +let injection_main with_evars c = + elimOnConstrWithHoles (injClause None None) with_evars c + +} + +TACTIC EXTEND injection +| [ "injection" ] -> { injClause None None false None } +| [ "injection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) false c } +END +TACTIC EXTEND einjection +| [ "einjection" ] -> { injClause None None true None } +| [ "einjection" destruction_arg(c) ] -> { mytclWithHoles (injClause None None) true c } +END +TACTIC EXTEND injection_as +| [ "injection" "as" intropattern_list(ipat)] -> + { injClause None (Some ipat) false None } +| [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> + { mytclWithHoles (injClause None (Some ipat)) false c } +END +TACTIC EXTEND einjection_as +| [ "einjection" "as" intropattern_list(ipat)] -> + { injClause None (Some ipat) true None } +| [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> + { mytclWithHoles (injClause None (Some ipat)) true c } +END +TACTIC EXTEND simple_injection +| [ "simple" "injection" ] -> { simpleInjClause None false None } +| [ "simple" "injection" destruction_arg(c) ] -> { mytclWithHoles (simpleInjClause None) false c } +END + +{ + +let injHyp id = + Proofview.tclEVARMAP >>= fun sigma -> + injection_main false (fun env sigma -> (sigma, (EConstr.mkVar id, NoBindings))) + +} + +TACTIC EXTEND dependent_rewrite +| [ "dependent" "rewrite" orient(b) constr(c) ] -> { rewriteInConcl b c } +| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ] + -> { rewriteInHyp b c id } +END + +(** To be deprecated?, "cutrewrite (t=u) as <-" is equivalent to + "replace u with t" or "enough (t=u) as <-" and + "cutrewrite (t=u) as ->" is equivalent to "enough (t=u) as ->". *) + +TACTIC EXTEND cut_rewrite +| [ "cutrewrite" orient(b) constr(eqn) ] -> { cutRewriteInConcl b eqn } +| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ] + -> { cutRewriteInHyp b eqn id } +END + +(**********************************************************************) +(* Decompose *) + +TACTIC EXTEND decompose_sum +| [ "decompose" "sum" constr(c) ] -> { Elim.h_decompose_or c } +END + +TACTIC EXTEND decompose_record +| [ "decompose" "record" constr(c) ] -> { Elim.h_decompose_and c } +END + +(**********************************************************************) +(* Contradiction *) + +{ + +open Contradiction + +} + +TACTIC EXTEND absurd +| [ "absurd" constr(c) ] -> { absurd c } +END + +{ + +let onSomeWithHoles tac = function + | None -> tac None + | Some c -> Tacticals.New.tclDELAYEDWITHHOLES false c (fun c -> tac (Some c)) + +} + +TACTIC EXTEND contradiction +| [ "contradiction" constr_with_bindings_opt(c) ] -> + { onSomeWithHoles contradiction c } +END + +(**********************************************************************) +(* AutoRewrite *) + +{ + +open Autorewrite + +let pr_orient _prc _prlc _prt = function + | true -> Pp.mt () + | false -> Pp.str " <-" + +let pr_orient_string _prc _prlc _prt (orient, s) = + pr_orient _prc _prlc _prt orient ++ Pp.spc () ++ Pp.str s + +} + +ARGUMENT EXTEND orient_string TYPED AS (bool * string) PRINTED BY { pr_orient_string } +| [ orient(r) preident(i) ] -> { r, i } +END + +TACTIC EXTEND autorewrite +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) ] -> + { auto_multi_rewrite l ( cl) } +| [ "autorewrite" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> + { + auto_multi_rewrite_with (Tacinterp.tactic_of_value ist t) l cl + } +END + +TACTIC EXTEND autorewrite_star +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) ] -> + { auto_multi_rewrite ~conds:AllMatches l cl } +| [ "autorewrite" "*" "with" ne_preident_list(l) clause(cl) "using" tactic(t) ] -> + { auto_multi_rewrite_with ~conds:AllMatches (Tacinterp.tactic_of_value ist t) l cl } +END + +(**********************************************************************) +(* Rewrite star *) + +{ + +let rewrite_star ist clause orient occs c (tac : Geninterp.Val.t option) = + let tac' = Option.map (fun t -> Tacinterp.tactic_of_value ist t, FirstSolved) tac in + with_delayed_uconstr ist c + (fun c -> general_rewrite_ebindings_clause clause orient occs ?tac:tac' true true (c,NoBindings) true) + +} + +TACTIC EXTEND rewrite_star +| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) "at" occurrences(occ) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) "in" hyp(id) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "in" hyp(id) by_arg_tac(tac) ] -> + { rewrite_star ist (Some id) o Locus.AllOccurrences c tac } +| [ "rewrite" "*" orient(o) uconstr(c) "at" occurrences(occ) by_arg_tac(tac) ] -> + { rewrite_star ist None o (occurrences_of occ) c tac } +| [ "rewrite" "*" orient(o) uconstr(c) by_arg_tac(tac) ] -> + { rewrite_star ist None o Locus.AllOccurrences c tac } + END + +(**********************************************************************) +(* Hint Rewrite *) + +{ + +let add_rewrite_hint ~poly bases ort t lcsr = + let env = Global.env() in + let sigma = Evd.from_env env in + let f ce = + let c, ctx = Constrintern.interp_constr env sigma ce in + let c = EConstr.to_constr sigma c in + let ctx = + let ctx = UState.context_set ctx in + if poly then ctx + else (** This is a global universe context that shouldn't be + refreshed at every use of the hint, declare it globally. *) + (Declare.declare_universe_context false ctx; + Univ.ContextSet.empty) + in + CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in + let eqs = List.map f lcsr in + let add_hints base = add_rew_rules base eqs in + List.iter add_hints bases + +let classify_hint _ = Vernacexpr.VtSideff [], Vernacexpr.VtLater + +} + +VERNAC COMMAND EXTEND HintRewrite CLASSIFIED BY { classify_hint } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:atts.polymorphic bl o None l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) + ":" preident_list(bl) ] -> + { add_rewrite_hint ~poly:atts.polymorphic bl o (Some t) l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) ] -> + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o None l } +| [ "Hint" "Rewrite" orient(o) ne_constr_list(l) "using" tactic(t) ] -> + { add_rewrite_hint ~poly:atts.polymorphic ["core"] o (Some t) l } +END + +(**********************************************************************) +(* Refine *) + +{ + +open EConstr +open Vars + +let constr_flags () = { + Pretyping.use_typeclasses = true; + Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics (); + Pretyping.use_hook = Pfedit.solve_by_implicit_tactic (); + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } + +let refine_tac ist simple with_classes c = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + let flags = + { (constr_flags ()) with Pretyping.use_typeclasses = with_classes } in + let expected_type = Pretyping.OfType concl in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in + let update = begin fun sigma -> + c env sigma + end in + let refine = Refine.refine ~typecheck:false update in + if simple then refine + else refine <*> + Tactics.New.reduce_after_refine <*> + Proofview.shelve_unifiable + end + +} + +TACTIC EXTEND refine +| [ "refine" uconstr(c) ] -> + { refine_tac ist false true c } +END + +TACTIC EXTEND simple_refine +| [ "simple" "refine" uconstr(c) ] -> + { refine_tac ist true true c } +END + +TACTIC EXTEND notcs_refine +| [ "notypeclasses" "refine" uconstr(c) ] -> + { refine_tac ist false false c } +END + +TACTIC EXTEND notcs_simple_refine +| [ "simple" "notypeclasses" "refine" uconstr(c) ] -> + { refine_tac ist true false c } +END + +(* Solve unification constraints using heuristics or fail if any remain *) +TACTIC EXTEND solve_constraints +| [ "solve_constraints" ] -> { Refine.solve_constraints } +END + +(**********************************************************************) +(* Inversion lemmas (Leminv) *) + +{ + +open Inv +open Leminv + +let seff id = Vernacexpr.VtSideff [id], Vernacexpr.VtLater + +} + +(*VERNAC ARGUMENT EXTEND sort_family +| [ "Set" ] -> { InSet } +| [ "Prop" ] -> { InProp } +| [ "Type" ] -> { InType } +END*) + +VERNAC COMMAND EXTEND DeriveInversionClear +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_clear_tac } + +| [ "Derive" "Inversion_clear" ident(na) "with" constr(c) ] => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_clear_tac } +END + +VERNAC COMMAND EXTEND DeriveInversion +| [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s false inv_tac } + +| [ "Derive" "Inversion" ident(na) "with" constr(c) ] => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c Sorts.InProp false inv_tac } +END + +VERNAC COMMAND EXTEND DeriveDependentInversion +| [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_tac } +END + +VERNAC COMMAND EXTEND DeriveDependentInversionClear +| [ "Derive" "Dependent" "Inversion_clear" ident(na) "with" constr(c) "Sort" sort_family(s) ] + => { seff na } + -> { + let open Vernacinterp in + add_inversion_lemma_exn ~poly:atts.polymorphic na c s true dinv_clear_tac } +END + +(**********************************************************************) +(* Subst *) + +TACTIC EXTEND subst +| [ "subst" ne_var_list(l) ] -> { subst l } +| [ "subst" ] -> { subst_all () } +END + +{ + +let simple_subst_tactic_flags = + { only_leibniz = true; rewrite_dependent_proof = false } + +} + +TACTIC EXTEND simple_subst +| [ "simple" "subst" ] -> { subst_all ~flags:simple_subst_tactic_flags () } +END + +{ + +open Evar_tactics + +} + +(**********************************************************************) +(* Evar creation *) + +(* TODO: add support for some test similar to g_constr.name_colon so that + expressions like "evar (list A)" do not raise a syntax error *) +TACTIC EXTEND evar +| [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> { let_evar (Name.Name id) typ } +| [ "evar" constr(typ) ] -> { let_evar Name.Anonymous typ } +END + +TACTIC EXTEND instantiate +| [ "instantiate" "(" ident(id) ":=" lglob(c) ")" ] -> + { Tacticals.New.tclTHEN (instantiate_tac_by_name id c) Proofview.V82.nf_evar_goals } +| [ "instantiate" "(" integer(i) ":=" lglob(c) ")" hloc(hl) ] -> + { Tacticals.New.tclTHEN (instantiate_tac i c hl) Proofview.V82.nf_evar_goals } +| [ "instantiate" ] -> { Proofview.V82.nf_evar_goals } +END + +(**********************************************************************) +(** Nijmegen "step" tactic for setoid rewriting *) + +{ + +open Tactics +open Glob_term +open Libobject +open Lib + +(* Registered lemmas are expected to be of the form + x R y -> y == z -> x R z (in the right table) + x R y -> x == z -> z R y (in the left table) +*) + +let transitivity_right_table = Summary.ref [] ~name:"transitivity-steps-r" +let transitivity_left_table = Summary.ref [] ~name:"transitivity-steps-l" + +(* [step] tries to apply a rewriting lemma; then apply [tac] intended to + complete to proof of the last hypothesis (assumed to state an equality) *) + +let step left x tac = + let l = + List.map (fun lem -> + let lem = EConstr.of_constr lem in + Tacticals.New.tclTHENLAST + (apply_with_bindings (lem, ImplicitBindings [x])) + tac) + !(if left then transitivity_left_table else transitivity_right_table) + in + Tacticals.New.tclFIRST l + +(* Main function to push lemmas in persistent environment *) + +let cache_transitivity_lemma (_,(left,lem)) = + if left then + transitivity_left_table := lem :: !transitivity_left_table + else + transitivity_right_table := lem :: !transitivity_right_table + +let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) + +let inTransitivity : bool * Constr.t -> obj = + declare_object {(default_object "TRANSITIVITY-STEPS") with + cache_function = cache_transitivity_lemma; + open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); + subst_function = subst_transitivity_lemma; + classify_function = (fun o -> Substitute o) } + +(* Main entry points *) + +let add_transitivity_lemma left lem = + let env = Global.env () in + let sigma = Evd.from_env env in + let lem',ctx (*FIXME*) = Constrintern.interp_constr env sigma lem in + let lem' = EConstr.to_constr sigma lem' in + add_anonymous_leaf (inTransitivity (left,lem')) + +} + +(* Vernacular syntax *) + +TACTIC EXTEND stepl +| ["stepl" constr(c) "by" tactic(tac) ] -> { step true c (Tacinterp.tactic_of_value ist tac) } +| ["stepl" constr(c) ] -> { step true c (Proofview.tclUNIT ()) } +END + +TACTIC EXTEND stepr +| ["stepr" constr(c) "by" tactic(tac) ] -> { step false c (Tacinterp.tactic_of_value ist tac) } +| ["stepr" constr(c) ] -> { step false c (Proofview.tclUNIT ()) } +END + +VERNAC COMMAND EXTEND AddStepl CLASSIFIED AS SIDEFF +| [ "Declare" "Left" "Step" constr(t) ] -> + { add_transitivity_lemma true t } +END + +VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF +| [ "Declare" "Right" "Step" constr(t) ] -> + { add_transitivity_lemma false t } +END + +{ + +let cache_implicit_tactic (_,tac) = match tac with + | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) + | None -> Pfedit.clear_implicit_tactic () + +let subst_implicit_tactic (subst,tac) = + Option.map (Tacsubst.subst_tactic subst) tac + +let inImplicitTactic : glob_tactic_expr option -> obj = + declare_object {(default_object "IMPLICIT-TACTIC") with + open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); + cache_function = cache_implicit_tactic; + subst_function = subst_implicit_tactic; + classify_function = (fun o -> Dispose)} + +let warn_deprecated_implicit_tactic = + CWarnings.create ~name:"deprecated-implicit-tactic" ~category:"deprecated" + (fun () -> strbrk "Implicit tactics are deprecated") + +let declare_implicit_tactic tac = + let () = warn_deprecated_implicit_tactic () in + Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) + +let clear_implicit_tactic () = + let () = warn_deprecated_implicit_tactic () in + Lib.add_anonymous_leaf (inImplicitTactic None) + +} + +VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> { declare_implicit_tactic tac } +| [ "Clear" "Implicit" "Tactic" ] -> { clear_implicit_tactic () } +END + + + + +(**********************************************************************) +(* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as + defined by Conor McBride *) +TACTIC EXTEND generalize_eqs +| ["generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false id } +END +TACTIC EXTEND dep_generalize_eqs +| ["dependent" "generalize_eqs" hyp(id) ] -> { abstract_generalize ~generalize_vars:false ~force_dep:true id } +END +TACTIC EXTEND generalize_eqs_vars +| ["generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~generalize_vars:true id } +END +TACTIC EXTEND dep_generalize_eqs_vars +| ["dependent" "generalize_eqs_vars" hyp(id) ] -> { abstract_generalize ~force_dep:true ~generalize_vars:true id } +END + +(** Tactic to automatically simplify hypotheses of the form [Π Δ, x_i = t_i -> T] + where [t_i] is closed w.r.t. Δ. Such hypotheses are automatically generated + during dependent induction. For internal use. *) + +TACTIC EXTEND specialize_eqs +| [ "specialize_eqs" hyp(id) ] -> { specialize_eqs id } +END + +(**********************************************************************) +(* A tactic that considers a given occurrence of [c] in [t] and *) +(* abstract the minimal set of all the occurrences of [c] so that the *) +(* abstraction [fun x -> t[x/c]] is well-typed *) +(* *) +(* Contributed by Chung-Kil Hur (Winter 2009) *) +(**********************************************************************) + +{ + +let subst_var_with_hole occ tid t = + let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in + let locref = ref 0 in + let rec substrec x = match DAst.get x with + | GVar id -> + if Id.equal id tid + then + (decr occref; + if Int.equal !occref 0 then x + else + (incr locref; + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, None))) + else x + | _ -> map_glob_constr_left_to_right substrec x in + let t' = substrec t + in + if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t' + +let subst_hole_with_term occ tc t = + let locref = ref 0 in + let occref = ref occ in + let rec substrec c = match DAst.get c with + | GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + }, IntroAnonymous, s) -> + decr occref; + if Int.equal !occref 0 then tc + else + (incr locref; + DAst.make ~loc:(Loc.make_loc (!locref,0)) @@ + GHole (Evar_kinds.QuestionMark { + Evar_kinds.qm_obligation=Evar_kinds.Define true; + Evar_kinds.qm_name=Anonymous; + Evar_kinds.qm_record_field=None; + },IntroAnonymous,s)) + | _ -> map_glob_constr_left_to_right substrec c + in + substrec t + +open Tacmach + +let hResolve id c occ t = + Proofview.Goal.enter begin fun gl -> + let sigma = Proofview.Goal.sigma gl in + let env = Termops.clear_named_body id (Proofview.Goal.env gl) in + let concl = Proofview.Goal.concl gl in + let env_ids = Termops.vars_of_env env in + let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in + let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in + let rec resolve_hole t_hole = + try + Pretyping.understand env sigma t_hole + with + | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e -> + let (e, info) = CErrors.push e in + let loc_begin = Option.cata (fun l -> fst (Loc.unloc l)) 0 (Loc.get_loc info) in + resolve_hole (subst_hole_with_term loc_begin c_raw t_hole) + in + let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in + let sigma = Evd.merge_universe_context sigma ctx in + let t_constr_type = Retyping.get_type_of env sigma t_constr in + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) + (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) + end + +let hResolve_auto id c t = + let rec resolve_auto n = + try + hResolve id c n t + with + | UserError _ as e -> raise e + | e when CErrors.noncritical e -> resolve_auto (n+1) + in + resolve_auto 1 + +} + +TACTIC EXTEND hresolve_core +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "at" int_or_var(occ) "in" constr(t) ] -> { hResolve id c occ t } +| [ "hresolve_core" "(" ident(id) ":=" constr(c) ")" "in" constr(t) ] -> { hResolve_auto id c t } +END + +(** + hget_evar +*) + +TACTIC EXTEND hget_evar +| [ "hget_evar" int_or_var(n) ] -> { Evar_tactics.hget_evar n } +END + +(**********************************************************************) + +(**********************************************************************) +(* A tactic that reduces one match t with ... by doing destruct t. *) +(* if t is not a variable, the tactic does *) +(* case_eq t;intros ... heq;rewrite heq in *|-. (but heq itself is *) +(* preserved). *) +(* Contributed by Julien Forest and Pierre Courtieu (july 2010) *) +(**********************************************************************) + +{ + +exception Found of unit Proofview.tactic + +let rewrite_except h = + Proofview.Goal.enter begin fun gl -> + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else + Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false)) + hyps + end + + +let refl_equal () = Coqlib.lib_ref "core.eq.type" + +(* This is simply an implementation of the case_eq tactic. this code + should be replaced by a call to the tactic but I don't know how to + call it before it is defined. *) +let mkCaseEq a : unit Proofview.tactic = + Proofview.Goal.enter begin fun gl -> + let type_of_a = Tacmach.New.pf_unsafe_type_of gl a in + Tacticals.New.pf_constr_of_global (delayed_force refl_equal) >>= fun req -> + Tacticals.New.tclTHENLIST + [Tactics.generalize [(mkApp(req, [| type_of_a; a|]))]; + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let env = Proofview.Goal.env gl in + (** FIXME: this looks really wrong. Does anybody really use this tactic? *) + let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in + change_concl c + end; + simplest_case a] + end + + +let case_eq_intros_rewrite x = + Proofview.Goal.enter begin fun gl -> + let n = nb_prod (Tacmach.New.project gl) (Proofview.Goal.concl gl) in + (* Pp.msgnl (Printer.pr_lconstr x); *) + Tacticals.New.tclTHENLIST [ + mkCaseEq x; + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let hyps = Tacmach.New.pf_ids_set_of_hyps gl in + let n' = nb_prod (Tacmach.New.project gl) concl in + let h = fresh_id_in_env hyps (Id.of_string "heq") (Proofview.Goal.env gl) in + Tacticals.New.tclTHENLIST [ + Tacticals.New.tclDO (n'-n-1) intro; + introduction h; + rewrite_except h] + end + ] + end + +let rec find_a_destructable_match sigma t = + let cl = induction_arg_of_quantified_hyp (NamedHyp (Id.of_string "x")) in + let cl = [cl, (None, None), None], None in + let dest = TacAtom (Loc.tag @@ TacInductionDestruct(false, false, cl)) in + match EConstr.kind sigma t with + | Case (_,_,x,_) when closed0 sigma x -> + if isVar sigma x then + (* TODO check there is no rel n. *) + raise (Found (Tacinterp.eval_tactic dest)) + else + (* let _ = Pp.msgnl (Printer.pr_lconstr x) in *) + raise (Found (case_eq_intros_rewrite x)) + | _ -> EConstr.iter sigma (fun c -> find_a_destructable_match sigma c) t + + +let destauto t = + Proofview.tclEVARMAP >>= fun sigma -> + try find_a_destructable_match sigma t; + Tacticals.New.tclZEROMSG (str "No destructable match found") + with Found tac -> tac + +let destauto_in id = + Proofview.Goal.enter begin fun gl -> + let ctype = Tacmach.New.pf_unsafe_type_of gl (mkVar id) in +(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *) +(* Pp.msgnl (Printer.pr_lconstr (ctype)); *) + destauto ctype + end + +} + +TACTIC EXTEND destauto +| [ "destauto" ] -> { Proofview.Goal.enter begin fun gl -> destauto (Proofview.Goal.concl gl) end } +| [ "destauto" "in" hyp(id) ] -> { destauto_in id } +END + +(**********************************************************************) + +(**********************************************************************) +(* A version of abstract constructing transparent terms *) +(* Introduced by Jason Gross and Benjamin Delaware in June 2016 *) +(**********************************************************************) + +TACTIC EXTEND transparent_abstract +| [ "transparent_abstract" tactic3(t) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end } +| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> { Proofview.Goal.enter begin fun gl -> + Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end } +END + +(* ********************************************************************* *) + +TACTIC EXTEND constr_eq +| [ "constr_eq" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:false x y } +END + +TACTIC EXTEND constr_eq_strict +| [ "constr_eq_strict" constr(x) constr(y) ] -> { Tactics.constr_eq ~strict:true x y } +END + +TACTIC EXTEND constr_eq_nounivs +| [ "constr_eq_nounivs" constr(x) constr(y) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + if eq_constr_nounivs sigma x y then Proofview.tclUNIT () else Tacticals.New.tclFAIL 0 (str "Not equal") } +END + +TACTIC EXTEND is_evar +| [ "is_evar" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Evar _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not an evar") + } +END + +TACTIC EXTEND has_evar +| [ "has_evar" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + if Evarutil.has_undefined_evars sigma x + then Proofview.tclUNIT () + else Tacticals.New.tclFAIL 0 (str "No evars") +} +END + +TACTIC EXTEND is_hyp +| [ "is_var" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Var _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (str "Not a variable or hypothesis") } +END + +TACTIC EXTEND is_fix +| [ "is_fix" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Fix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a fix definition") } +END + +TACTIC EXTEND is_cofix +| [ "is_cofix" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | CoFix _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a cofix definition") } +END + +TACTIC EXTEND is_ind +| [ "is_ind" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Ind _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not an (co)inductive datatype") } +END + +TACTIC EXTEND is_constructor +| [ "is_constructor" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Construct _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constructor") } +END + +TACTIC EXTEND is_proj +| [ "is_proj" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Proj _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a primitive projection") } +END + +TACTIC EXTEND is_const +| [ "is_const" constr(x) ] -> { + Proofview.tclEVARMAP >>= fun sigma -> + match EConstr.kind sigma x with + | Const _ -> Proofview.tclUNIT () + | _ -> Tacticals.New.tclFAIL 0 (Pp.str "not a constant") } +END + +(* Command to grab the evars left unresolved at the end of a proof. *) +(* spiwack: I put it in extratactics because it is somewhat tied with + the semantics of the LCF-style tactics, hence with the classic tactic + mode. *) +VERNAC COMMAND EXTEND GrabEvars +| [ "Grab" "Existential" "Variables" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.V82.grab_evars p) } +END + +(* Shelves all the goals under focus. *) +TACTIC EXTEND shelve +| [ "shelve" ] -> + { Proofview.shelve } +END + +(* Shelves the unifiable goals under focus, i.e. the goals which + appear in other goals under focus (the unfocused goals are not + considered). *) +TACTIC EXTEND shelve_unifiable +| [ "shelve_unifiable" ] -> + { Proofview.shelve_unifiable } +END + +(* Unshelves the goal shelved by the tactic. *) +TACTIC EXTEND unshelve +| [ "unshelve" tactic1(t) ] -> + { + Proofview.with_shelf (Tacinterp.tactic_of_value ist t) >>= fun (gls, ()) -> + let gls = List.map Proofview.with_empty_state gls in + Proofview.Unsafe.tclGETGOALS >>= fun ogls -> + Proofview.Unsafe.tclSETGOALS (gls @ ogls) + } +END + +(* Command to add every unshelved variables to the focus *) +VERNAC COMMAND EXTEND Unshelve +| [ "Unshelve" ] + => { Vernac_classifier.classify_as_proofstep } + -> { Proof_global.simple_with_current_proof (fun _ p -> Proof.unshelve p) } +END + +(* Gives up on the goals under focus: the goals are considered solved, + but the proof cannot be closed until the user goes back and solve + these goals. *) +TACTIC EXTEND give_up +| [ "give_up" ] -> + { Proofview.give_up } +END + +(* cycles [n] goals *) +TACTIC EXTEND cycle +| [ "cycle" int_or_var(n) ] -> { Proofview.cycle n } +END + +(* swaps goals number [i] and [j] *) +TACTIC EXTEND swap +| [ "swap" int_or_var(i) int_or_var(j) ] -> { Proofview.swap i j } +END + +(* reverses the list of focused goals *) +TACTIC EXTEND revgoals +| [ "revgoals" ] -> { Proofview.revgoals } +END + +{ + +type cmp = + | Eq + | Lt | Le + | Gt | Ge + +type 'i test = + | Test of cmp * 'i * 'i + +let pr_cmp = function + | Eq -> Pp.str"=" + | Lt -> Pp.str"<" + | Le -> Pp.str"<=" + | Gt -> Pp.str">" + | Ge -> Pp.str">=" + +let pr_cmp' _prc _prlc _prt = pr_cmp + +let pr_test_gen f (Test(c,x,y)) = + Pp.(f x ++ pr_cmp c ++ f y) + +let pr_test = pr_test_gen (Pputils.pr_or_var Pp.int) + +let pr_test' _prc _prlc _prt = pr_test + +let pr_itest = pr_test_gen Pp.int + +let pr_itest' _prc _prlc _prt = pr_itest + +} + +ARGUMENT EXTEND comparison PRINTED BY { pr_cmp' } +| [ "=" ] -> { Eq } +| [ "<" ] -> { Lt } +| [ "<=" ] -> { Le } +| [ ">" ] -> { Gt } +| [ ">=" ] -> { Ge } + END + +{ + +let interp_test ist gls = function + | Test (c,x,y) -> + project gls , + Test(c,Tacinterp.interp_int_or_var ist x,Tacinterp.interp_int_or_var ist y) + +} + +ARGUMENT EXTEND test + PRINTED BY { pr_itest' } + INTERPRETED BY { interp_test } + RAW_PRINTED BY { pr_test' } + GLOB_PRINTED BY { pr_test' } +| [ int_or_var(x) comparison(c) int_or_var(y) ] -> { Test(c,x,y) } +END + +{ + +let interp_cmp = function + | Eq -> Int.equal + | Lt -> ((<):int->int->bool) + | Le -> ((<=):int->int->bool) + | Gt -> ((>):int->int->bool) + | Ge -> ((>=):int->int->bool) + +let run_test = function + | Test(c,x,y) -> interp_cmp c x y + +let guard tst = + if run_test tst then + Proofview.tclUNIT () + else + let msg = Pp.(str"Condition not satisfied:"++ws 1++(pr_itest tst)) in + Tacticals.New.tclZEROMSG msg + +} + +TACTIC EXTEND guard +| [ "guard" test(tst) ] -> { guard tst } +END + +{ + +let decompose l c = + Proofview.Goal.enter begin fun gl -> + let sigma = Tacmach.New.project gl in + let to_ind c = + if isInd sigma c then fst (destInd sigma c) + else user_err Pp.(str "not an inductive type") + in + let l = List.map to_ind l in + Elim.h_decompose l c + end + +} + +TACTIC EXTEND decompose +| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> { decompose l c } +END + +(** library/keys *) + +VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF +| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> { + let get_key c = + let env = Global.env () in + let evd = Evd.from_env env in + let (evd, c) = Constrintern.interp_open_constr env evd c in + let kind c = EConstr.kind evd c in + Keys.constr_key kind c + in + let k1 = get_key c in + let k2 = get_key c' in + match k1, k2 with + | Some k1, Some k2 -> Keys.declare_equiv_keys k1 k2 + | _ -> () } +END + +VERNAC COMMAND EXTEND Print_keys CLASSIFIED AS QUERY +| [ "Print" "Equivalent" "Keys" ] -> { Feedback.msg_info (Keys.pr_keys Printer.pr_global) } +END + + +VERNAC COMMAND EXTEND OptimizeProof +| [ "Optimize" "Proof" ] => { Vernac_classifier.classify_as_proofstep } -> + { Proof_global.compact_the_proof () } +| [ "Optimize" "Heap" ] => { Vernac_classifier.classify_as_proofstep } -> + { Gc.compact () } +END + +(** tactic analogous to "OPTIMIZE HEAP" *) + +{ + +let tclOPTIMIZE_HEAP = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> Gc.compact ())) + +} + +TACTIC EXTEND optimize_heap +| [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP } +END diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 deleted file mode 100644 index 6913543c9a..0000000000 --- a/plugins/ltac/g_auto.ml4 +++ /dev/null @@ -1,226 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ Eauto.e_assumption ] -END - -TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] -END - -let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases - -ARGUMENT EXTEND hintbases - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ "with" "*" ] -> [ None ] -| [ "with" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ Some [] ] -END - -let eval_uconstrs ist cs = - let flags = { - Pretyping.use_typeclasses = false; - solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); - fail_evar = false; - expand_evars = true - } in - let map c env sigma = c env sigma in - List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs - -let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr -let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> - let _, env = Pfedit.get_current_context () in - Printer.pr_glob_constr_env env c) -let pr_auto_using _ _ _ = Pptactic.pr_auto_using - (let sigma, env = Pfedit.get_current_context () in - Printer.pr_closed_glob_env env sigma) - -ARGUMENT EXTEND auto_using - TYPED AS uconstr_list - PRINTED BY pr_auto_using - RAW_PRINTED BY pr_auto_using_raw - GLOB_PRINTED BY pr_auto_using_glob -| [ "using" ne_uconstr_list_sep(l, ",") ] -> [ l ] -| [ ] -> [ [] ] -END - -(** Auto *) - -TACTIC EXTEND trivial -| [ "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_trivial -| [ "info_trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND debug_trivial -| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> - [ Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND auto -| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto n (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_auto -| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND debug_auto -| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> - [ Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db ] -END - -(** Eauto *) - -TACTIC EXTEND prolog -| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> - [ Eauto.prolog_tac (eval_uconstrs ist l) n ] -END - -let make_depth n = snd (Eauto.make_dimension n None) - -TACTIC EXTEND eauto -| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND new_eauto -| [ "new" "auto" int_or_var_opt(n) auto_using(lems) - hintbases(db) ] -> - [ match db with - | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) - | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l ] -END - -TACTIC EXTEND debug_eauto -| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND info_eauto -| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND dfs_eauto -| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) - hintbases(db) ] -> - [ Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db ] -END - -TACTIC EXTEND autounfold -| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> [ Eauto.autounfold_tac db cl ] -END - -TACTIC EXTEND autounfold_one -| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) ] -| [ "autounfold_one" hintbases(db) ] -> - [ Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None ] - END - -TACTIC EXTEND unify -| ["unify" constr(x) constr(y) ] -> [ Tactics.unify x y ] -| ["unify" constr(x) constr(y) "with" preident(base) ] -> [ - let table = try Some (Hints.searchtable_map base) with Not_found -> None in - match table with - | None -> - let msg = str "Hint table " ++ str base ++ str " not found" in - Tacticals.New.tclZEROMSG msg - | Some t -> - let state = Hints.Hint_db.transparent_state t in - Tactics.unify ~state x y - ] -END - - -TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ] -END - -let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid -let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global -let glob_hints_path_atom ist = Hints.glob_hints_path_atom - -ARGUMENT EXTEND hints_path_atom - PRINTED BY pr_hints_path_atom - - GLOBALIZED BY glob_hints_path_atom - - RAW_PRINTED BY pr_pre_hints_path_atom - GLOB_PRINTED BY pr_hints_path_atom -| [ ne_global_list(g) ] -> [ Hints.PathHints g ] -| [ "_" ] -> [ Hints.PathAny ] -END - -let pr_hints_path prc prx pry c = Hints.pp_hints_path c -let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c -let glob_hints_path ist = Hints.glob_hints_path - -ARGUMENT EXTEND hints_path -PRINTED BY pr_hints_path - -GLOBALIZED BY glob_hints_path -RAW_PRINTED BY pr_pre_hints_path -GLOB_PRINTED BY pr_hints_path - -| [ "(" hints_path(p) ")" ] -> [ p ] -| [ hints_path(p) "*" ] -> [ Hints.PathStar p ] -| [ "emp" ] -> [ Hints.PathEmpty ] -| [ "eps" ] -> [ Hints.PathEpsilon ] -| [ hints_path(p) "|" hints_path(q) ] -> [ Hints.PathOr (p, q) ] -| [ hints_path_atom(a) ] -> [ Hints.PathAtom a ] -| [ hints_path(p) hints_path(q) ] -> [ Hints.PathSeq (p, q) ] -END - -ARGUMENT EXTEND opthints - TYPED AS preident_list_opt - PRINTED BY pr_hintbases -| [ ":" ne_preident_list(l) ] -> [ Some l ] -| [ ] -> [ None ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF -| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> [ - fun ~atts ~st -> begin - let open Vernacinterp in - let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in - Hints.add_hints ~local:(Locality.make_section_locality atts.locality) - (match dbnames with None -> ["core"] | Some l -> l) entry; - st - end - ] -END - diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg new file mode 100644 index 0000000000..c07b653f3a --- /dev/null +++ b/plugins/ltac/g_auto.mlg @@ -0,0 +1,249 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { Eauto.e_assumption } +END + +TACTIC EXTEND eexact +| [ "eexact" constr(c) ] -> { Eauto.e_give_exact c } +END + +{ + +let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases + +} + +ARGUMENT EXTEND hintbases + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ "with" "*" ] -> { None } +| [ "with" ne_preident_list(l) ] -> { Some l } +| [ ] -> { Some [] } +END + +{ + +let eval_uconstrs ist cs = + let flags = { + Pretyping.use_typeclasses = false; + solve_unification_constraints = true; + use_hook = Pfedit.solve_by_implicit_tactic (); + fail_evar = false; + expand_evars = true + } in + let map c env sigma = c env sigma in + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs + +let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr +let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> + let _, env = Pfedit.get_current_context () in + Printer.pr_glob_constr_env env c) +let pr_auto_using _ _ _ = Pptactic.pr_auto_using + (let sigma, env = Pfedit.get_current_context () in + Printer.pr_closed_glob_env env sigma) + +} + +ARGUMENT EXTEND auto_using + TYPED AS uconstr list + PRINTED BY { pr_auto_using } + RAW_PRINTED BY { pr_auto_using_raw } + GLOB_PRINTED BY { pr_auto_using_glob } +| [ "using" ne_uconstr_list_sep(l, ",") ] -> { l } +| [ ] -> { [] } +END + +(** Auto *) + +TACTIC EXTEND trivial +| [ "trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_trivial +| [ "info_trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial ~debug:Info (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND debug_trivial +| [ "debug" "trivial" auto_using(lems) hintbases(db) ] -> + { Auto.h_trivial ~debug:Debug (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND auto +| [ "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto n (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_auto +| [ "info_auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto ~debug:Info n (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND debug_auto +| [ "debug" "auto" int_or_var_opt(n) auto_using(lems) hintbases(db) ] -> + { Auto.h_auto ~debug:Debug n (eval_uconstrs ist lems) db } +END + +(** Eauto *) + +TACTIC EXTEND prolog +| [ "prolog" "[" uconstr_list(l) "]" int_or_var(n) ] -> + { Eauto.prolog_tac (eval_uconstrs ist l) n } +END + +{ + +let make_depth n = snd (Eauto.make_dimension n None) + +} + +TACTIC EXTEND eauto +| [ "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND new_eauto +| [ "new" "auto" int_or_var_opt(n) auto_using(lems) + hintbases(db) ] -> + { match db with + | None -> Auto.new_full_auto (make_depth n) (eval_uconstrs ist lems) + | Some l -> Auto.new_auto (make_depth n) (eval_uconstrs ist lems) l } +END + +TACTIC EXTEND debug_eauto +| [ "debug" "eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto ~debug:Debug (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND info_eauto +| [ "info_eauto" int_or_var_opt(n) int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto ~debug:Info (Eauto.make_dimension n p) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND dfs_eauto +| [ "dfs" "eauto" int_or_var_opt(p) auto_using(lems) + hintbases(db) ] -> + { Eauto.gen_eauto (Eauto.make_dimension p None) (eval_uconstrs ist lems) db } +END + +TACTIC EXTEND autounfold +| [ "autounfold" hintbases(db) clause_dft_concl(cl) ] -> { Eauto.autounfold_tac db cl } +END + +TACTIC EXTEND autounfold_one +| [ "autounfold_one" hintbases(db) "in" hyp(id) ] -> + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) (Some (id, Locus.InHyp)) } +| [ "autounfold_one" hintbases(db) ] -> + { Eauto.autounfold_one (match db with None -> ["core"] | Some x -> "core"::x) None } + END + +TACTIC EXTEND unify +| ["unify" constr(x) constr(y) ] -> { Tactics.unify x y } +| ["unify" constr(x) constr(y) "with" preident(base) ] -> { + let table = try Some (Hints.searchtable_map base) with Not_found -> None in + match table with + | None -> + let msg = str "Hint table " ++ str base ++ str " not found" in + Tacticals.New.tclZEROMSG msg + | Some t -> + let state = Hints.Hint_db.transparent_state t in + Tactics.unify ~state x y + } +END + + +TACTIC EXTEND convert_concl_no_check +| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } +END + +{ + +let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_qualid +let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Printer.pr_global +let glob_hints_path_atom ist = Hints.glob_hints_path_atom + +} + +ARGUMENT EXTEND hints_path_atom + PRINTED BY { pr_hints_path_atom } + + GLOBALIZED BY { glob_hints_path_atom } + + RAW_PRINTED BY { pr_pre_hints_path_atom } + GLOB_PRINTED BY { pr_hints_path_atom } +| [ ne_global_list(g) ] -> { Hints.PathHints g } +| [ "_" ] -> { Hints.PathAny } +END + +{ + +let pr_hints_path prc prx pry c = Hints.pp_hints_path c +let pr_pre_hints_path prc prx pry c = Hints.pp_hints_path_gen Libnames.pr_qualid c +let glob_hints_path ist = Hints.glob_hints_path + +} + +ARGUMENT EXTEND hints_path +PRINTED BY { pr_hints_path } + +GLOBALIZED BY { glob_hints_path } +RAW_PRINTED BY { pr_pre_hints_path } +GLOB_PRINTED BY { pr_hints_path } + +| [ "(" hints_path(p) ")" ] -> { p } +| [ hints_path(p) "*" ] -> { Hints.PathStar p } +| [ "emp" ] -> { Hints.PathEmpty } +| [ "eps" ] -> { Hints.PathEpsilon } +| [ hints_path(p) "|" hints_path(q) ] -> { Hints.PathOr (p, q) } +| [ hints_path_atom(a) ] -> { Hints.PathAtom a } +| [ hints_path(p) hints_path(q) ] -> { Hints.PathSeq (p, q) } +END + +ARGUMENT EXTEND opthints + TYPED AS preident list option + PRINTED BY { pr_hintbases } +| [ ":" ne_preident_list(l) ] -> { Some l } +| [ ] -> { None } +END + +VERNAC COMMAND EXTEND HintCut CLASSIFIED AS SIDEFF +| [ "Hint" "Cut" "[" hints_path(p) "]" opthints(dbnames) ] -> { + let open Vernacinterp in + let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in + Hints.add_hints ~local:(Locality.make_section_locality atts.locality) + (match dbnames with None -> ["core"] | Some l -> l) entry; + } +END + diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 deleted file mode 100644 index 265368833b..0000000000 --- a/plugins/ltac/g_class.ml4 +++ /dev/null @@ -1,117 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - let gr = Smartlocate.global_with_alias r in - let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in - Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl - -VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Transparent" reference_list(cl) ] -> [ - set_transparency cl true ] -END - -VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF -| [ "Typeclasses" "Opaque" reference_list(cl) ] -> [ - set_transparency cl false ] -END - -let pr_debug _prc _prlc _prt b = - if b then Pp.str "debug" else Pp.mt() - -ARGUMENT EXTEND debug TYPED AS bool PRINTED BY pr_debug -| [ "debug" ] -> [ true ] -| [ ] -> [ false ] -END - -let pr_search_strategy _prc _prlc _prt = function - | Some Dfs -> Pp.str "dfs" - | Some Bfs -> Pp.str "bfs" - | None -> Pp.mt () - -ARGUMENT EXTEND eauto_search_strategy PRINTED BY pr_search_strategy -| [ "(bfs)" ] -> [ Some Bfs ] -| [ "(dfs)" ] -> [ Some Dfs ] -| [ ] -> [ None ] -END - -(* true = All transparent, false = Opaque if possible *) - -VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF - | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> [ - set_typeclasses_debug d; - Option.iter set_typeclasses_strategy s; - set_typeclasses_depth depth - ] -END - -(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) -TACTIC EXTEND typeclasses_eauto - | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~strategy:Bfs ~depth:d l ] - | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> - [ typeclasses_eauto ~depth:d l ] - | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> [ - typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] ] -END - -TACTIC EXTEND head_of_constr - [ "head_of_constr" ident(h) constr(c) ] -> [ head_of_constr h c ] -END - -TACTIC EXTEND not_evar - [ "not_evar" constr(ty) ] -> [ not_evar ty ] -END - -TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ is_ground ty ] -END - -TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ autoapply c i ] -END - -(** TODO: DEPRECATE *) -(* A progress test that allows to see if the evars have changed *) -open Constr -open Proofview.Notations - -let rec eq_constr_mod_evars sigma x y = - let open EConstr in - match EConstr.kind sigma x, EConstr.kind sigma y with - | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true - | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y - -let progress_evars t = - Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl gl in - let check = - Proofview.Goal.enter begin fun gl' -> - let sigma = Tacmach.New.project gl' in - let newconcl = Proofview.Goal.concl gl' in - if eq_constr_mod_evars sigma concl newconcl - then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") - else Proofview.tclUNIT () - end - in t <*> check - end - -TACTIC EXTEND progress_evars - [ "progress_evars" tactic(t) ] -> [ progress_evars (Tacinterp.tactic_of_value ist t) ] -END diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg new file mode 100644 index 0000000000..9ecc36bdf3 --- /dev/null +++ b/plugins/ltac/g_class.mlg @@ -0,0 +1,137 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + let gr = Smartlocate.global_with_alias r in + let ev = Tacred.evaluable_of_global_reference (Global.env ()) gr in + Classes.set_typeclass_transparency ev (Locality.make_section_locality None) b) cl + +} + +VERNAC COMMAND EXTEND Typeclasses_Unfold_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Transparent" reference_list(cl) ] -> { + set_transparency cl true } +END + +VERNAC COMMAND EXTEND Typeclasses_Rigid_Settings CLASSIFIED AS SIDEFF +| [ "Typeclasses" "Opaque" reference_list(cl) ] -> { + set_transparency cl false } +END + +{ + +let pr_debug _prc _prlc _prt b = + if b then Pp.str "debug" else Pp.mt() + +} + +ARGUMENT EXTEND debug TYPED AS bool PRINTED BY { pr_debug } +| [ "debug" ] -> { true } +| [ ] -> { false } +END + +{ + +let pr_search_strategy _prc _prlc _prt = function + | Some Dfs -> Pp.str "dfs" + | Some Bfs -> Pp.str "bfs" + | None -> Pp.mt () + +} + +ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy } +| [ "(bfs)" ] -> { Some Bfs } +| [ "(dfs)" ] -> { Some Dfs } +| [ ] -> { None } +END + +(* true = All transparent, false = Opaque if possible *) + +VERNAC COMMAND EXTEND Typeclasses_Settings CLASSIFIED AS SIDEFF + | [ "Typeclasses" "eauto" ":=" debug(d) eauto_search_strategy(s) int_opt(depth) ] -> { + set_typeclasses_debug d; + Option.iter set_typeclasses_strategy s; + set_typeclasses_depth depth + } +END + +(** Compatibility: typeclasses eauto has 8.5 and 8.6 modes *) +TACTIC EXTEND typeclasses_eauto + | [ "typeclasses" "eauto" "bfs" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + { typeclasses_eauto ~strategy:Bfs ~depth:d l } + | [ "typeclasses" "eauto" int_or_var_opt(d) "with" ne_preident_list(l) ] -> + { typeclasses_eauto ~depth:d l } + | [ "typeclasses" "eauto" int_or_var_opt(d) ] -> { + typeclasses_eauto ~only_classes:true ~depth:d [Hints.typeclasses_db] } +END + +TACTIC EXTEND head_of_constr +| [ "head_of_constr" ident(h) constr(c) ] -> { head_of_constr h c } +END + +TACTIC EXTEND not_evar +| [ "not_evar" constr(ty) ] -> { not_evar ty } +END + +TACTIC EXTEND is_ground +| [ "is_ground" constr(ty) ] -> { is_ground ty } +END + +TACTIC EXTEND autoapply +| [ "autoapply" constr(c) "using" preident(i) ] -> { autoapply c i } +END + +{ + +(** TODO: DEPRECATE *) +(* A progress test that allows to see if the evars have changed *) +open Constr +open Proofview.Notations + +let rec eq_constr_mod_evars sigma x y = + let open EConstr in + match EConstr.kind sigma x, EConstr.kind sigma y with + | Evar (e1, l1), Evar (e2, l2) when not (Evar.equal e1 e2) -> true + | _, _ -> compare_constr sigma (fun x y -> eq_constr_mod_evars sigma x y) x y + +let progress_evars t = + Proofview.Goal.enter begin fun gl -> + let concl = Proofview.Goal.concl gl in + let check = + Proofview.Goal.enter begin fun gl' -> + let sigma = Tacmach.New.project gl' in + let newconcl = Proofview.Goal.concl gl' in + if eq_constr_mod_evars sigma concl newconcl + then Tacticals.New.tclFAIL 0 (Pp.str"No progress made (modulo evars)") + else Proofview.tclUNIT () + end + in t <*> check + end + +} + +TACTIC EXTEND progress_evars +| [ "progress_evars" tactic(t) ] -> { progress_evars (Tacinterp.tactic_of_value ist t) } +END diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 deleted file mode 100644 index 929390b1c4..0000000000 --- a/plugins/ltac/g_ltac.ml4 +++ /dev/null @@ -1,528 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* a - | e -> Tacexp (e:raw_tactic_expr) - -let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () -let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat -let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c -let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac - -let reference_to_id qid = - if Libnames.qualid_is_ident qid then - CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid - else - CErrors.user_err ?loc:qid.CAst.loc - (str "This expression should be a simple identifier.") - -let tactic_mode = Entry.create "vernac:tactic_command" - -let new_entry name = - let e = Entry.create name in - e - -let toplevel_selector = new_entry "vernac:toplevel_selector" -let tacdef_body = new_entry "tactic:tacdef_body" - -(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for - proof editing and changes nothing else). Then sets it as the default proof mode. *) -let _ = - let mode = { - Proof_global.name = "Classic"; - set = (fun () -> Pvernac.set_command_entry tactic_mode); - reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); - } in - Proof_global.register_proof_mode mode - -(* Hack to parse "[ id" without dropping [ *) -let test_bracket_ident = - Gram.Entry.of_parser "test_bracket_ident" - (fun strm -> - match stream_nth 0 strm with - | KEYWORD "[" -> - (match stream_nth 1 strm with - | IDENT _ -> () - | _ -> raise Stream.Failure) - | _ -> raise Stream.Failure) - -(* Tactics grammar rules *) - -let hint = G_proofs.hint - -GEXTEND Gram - GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint - tactic_mode constr_may_eval constr_eval toplevel_selector - operconstr; - - tactic_then_last: - [ [ "|"; lta = LIST0 OPT tactic_expr SEP "|" -> - Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) - | -> [||] - ] ] - ; - tactic_then_gen: - [ [ ta = tactic_expr; "|"; (first,last) = tactic_then_gen -> (ta::first, last) - | ta = tactic_expr; ".."; l = tactic_then_last -> ([], Some (ta, l)) - | ".."; l = tactic_then_last -> ([], Some (TacId [], l)) - | ta = tactic_expr -> ([ta], None) - | "|"; (first,last) = tactic_then_gen -> (TacId [] :: first, last) - | -> ([TacId []], None) - ] ] - ; - tactic_then_locality: (* [true] for the local variant [TacThens] and [false] - for [TacExtend] *) - [ [ "[" ; l = OPT">" -> if Option.is_empty l then true else false ] ] - ; - tactic_expr: - [ "5" RIGHTA - [ te = binder_tactic -> te ] - | "4" LEFTA - [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1) - | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0,ta1) - | ta0 = tactic_expr; ";"; l = tactic_then_locality; (first,tail) = tactic_then_gen; "]" -> - match l , tail with - | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) - | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) - | false , None -> TacThen (ta0,TacDispatch first) - | true , None -> TacThens (ta0,first) ] - | "3" RIGHTA - [ IDENT "try"; ta = tactic_expr -> TacTry ta - | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta) - | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) - | IDENT "time"; s = OPT string; ta = tactic_expr -> TacTime (s,ta) - | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta - | IDENT "progress"; ta = tactic_expr -> TacProgress ta - | IDENT "once"; ta = tactic_expr -> TacOnce ta - | IDENT "exactly_once"; ta = tactic_expr -> TacExactlyOnce ta - | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta -(*To do: put Abstract in Refiner*) - | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) - | IDENT "abstract"; tc = NEXT; "using"; s = ident -> - TacAbstract (tc,Some s) - | sel = selector; ta = tactic_expr -> TacSelect (sel, ta) ] -(*End of To do*) - | "2" RIGHTA - [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> TacOr (ta0,ta1) - | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> TacOr (ta0,ta1) - | IDENT "tryif" ; ta = tactic_expr ; - "then" ; tat = tactic_expr ; - "else" ; tae = tactic_expr -> TacIfThenCatch(ta,tat,tae) - | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1) - | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ] - | "1" RIGHTA - [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> - TacMatchGoal (b,false,mrl) - | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; - mrl = match_context_list; "end" -> - TacMatchGoal (b,true,mrl) - | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> - TacMatch (b,c,mrl) - | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacFirst l - | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> - TacSolve l - | IDENT "idtac"; l = LIST0 message_token -> TacId l - | g=failkw; n = [ n = int_or_var -> n | -> fail_default_value ]; - l = LIST0 message_token -> TacFail (g,n,l) - | st = simple_tactic -> st - | a = tactic_arg -> TacArg(Loc.tag ~loc:!@loc a) - | r = reference; la = LIST0 tactic_arg_compat -> - TacArg(Loc.tag ~loc:!@loc @@ TacCall (Loc.tag ~loc:!@loc (r,la))) ] - | "0" - [ "("; a = tactic_expr; ")" -> a - | "["; ">"; (tf,tail) = tactic_then_gen; "]" -> - begin match tail with - | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) - | None -> TacDispatch tf - end - | a = tactic_atom -> TacArg (Loc.tag ~loc:!@loc a) ] ] - ; - failkw: - [ [ IDENT "fail" -> TacLocal | IDENT "gfail" -> TacGlobal ] ] - ; - (* binder_tactic: level 5 of tactic_expr *) - binder_tactic: - [ RIGHTA - [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> - TacFun (it,body) - | "let"; isrec = [IDENT "rec" -> true | -> false]; - llc = LIST1 let_clause SEP "with"; "in"; - body = tactic_expr LEVEL "5" -> TacLetIn (isrec,llc,body) - | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ] - ; - (* Tactic arguments to the right of an application *) - tactic_arg_compat: - [ [ a = tactic_arg -> a - | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) - (* Unambiguous entries: tolerated w/o "ltac:" modifier *) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - (* Can be used as argument and at toplevel in tactic expressions. *) - tactic_arg: - [ [ c = constr_eval -> ConstrMayEval c - | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l - | IDENT "type_term"; c=uconstr -> TacPretype c - | IDENT "numgoals" -> TacNumgoals ] ] - ; - (* If a qualid is given, use its short name. TODO: have the shortest - non ambiguous name where dots are replaced by "_"? Probably too - verbose most of the time. *) - fresh_id: - [ [ s = STRING -> Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) - | qid = qualid -> Locus.ArgVar (CAst.make ~loc:!@loc @@ Libnames.qualid_basename qid) ] ] - ; - constr_eval: - [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> - ConstrEval (rtc,c) - | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> - ConstrContext (id,c) - | IDENT "type"; IDENT "of"; c = Constr.constr -> - ConstrTypeOf c ] ] - ; - constr_may_eval: (* For extensions *) - [ [ c = constr_eval -> c - | c = Constr.constr -> ConstrTerm c ] ] - ; - tactic_atom: - [ [ n = integer -> TacGeneric (genarg_of_int n) - | r = reference -> TacCall (Loc.tag ~loc:!@loc (r,[])) - | "()" -> TacGeneric (genarg_of_unit ()) ] ] - ; - match_key: - [ [ "match" -> Once - | "lazymatch" -> Select - | "multimatch" -> General ] ] - ; - input_fun: - [ [ "_" -> Name.Anonymous - | l = ident -> Name.Name l ] ] - ; - let_clause: - [ [ idr = identref; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr te) - | na = ["_" -> CAst.make ~loc:!@loc Anonymous]; ":="; te = tactic_expr -> - (na, arg_of_expr te) - | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) ] ] - ; - match_pattern: - [ [ IDENT "context"; oid = OPT Constr.ident; - "["; pc = Constr.lconstr_pattern; "]" -> - Subterm (oid, pc) - | pc = Constr.lconstr_pattern -> Term pc ] ] - ; - match_hyps: - [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) - | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) - | na = name; ":="; mpv = match_pattern -> - let t, ty = - match mpv with - | Term t -> (match t with - | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) - | _ -> mpv, None) - | _ -> mpv, None - in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) - ] ] - ; - match_context_rule: - [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; - "]"; "=>"; te = tactic_expr -> Pat (largs, mp, te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_context_list: - [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ] - ; - match_rule: - [ [ mp = match_pattern; "=>"; te = tactic_expr -> Pat ([],mp,te) - | "_"; "=>"; te = tactic_expr -> All te ] ] - ; - match_list: - [ [ mrl = LIST1 match_rule SEP "|" -> mrl - | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ] - ; - message_token: - [ [ id = identref -> MsgIdent id - | s = STRING -> MsgString s - | n = integer -> MsgInt n ] ] - ; - - ltac_def_kind: - [ [ ":=" -> false - | "::=" -> true ] ] - ; - - (* Definitions for tactics *) - tacdef_body: - [ [ name = Constr.global; it=LIST1 input_fun; - redef = ltac_def_kind; body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) - else - let id = reference_to_id name in - Tacexpr.TacticDefinition (id, TacFun (it, body)) - | name = Constr.global; redef = ltac_def_kind; - body = tactic_expr -> - if redef then Tacexpr.TacticRedefinition (name, body) - else - let id = reference_to_id name in - Tacexpr.TacticDefinition (id, body) - ] ] - ; - tactic: - [ [ tac = tactic_expr -> tac ] ] - ; - - range_selector: - [ [ n = natural ; "-" ; m = natural -> (n, m) - | n = natural -> (n, n) ] ] - ; - (* We unfold a range selectors list once so that we can make a special case - * for a unique SelectNth selector. *) - range_selector_or_nth: - [ [ n = natural ; "-" ; m = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - Goal_select.SelectList ((n, m) :: Option.default [] l) - | n = natural; - l = OPT [","; l = LIST1 range_selector SEP "," -> l] -> - let open Goal_select in - Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ] - ; - selector_body: - [ [ l = range_selector_or_nth -> l - | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ] - ; - selector: - [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ] - ; - toplevel_selector: - [ [ sel = selector_body; ":" -> sel - | "!"; ":" -> Goal_select.SelectAlreadyFocused - | IDENT "all"; ":" -> Goal_select.SelectAll ] ] - ; - tactic_mode: - [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g - | g = OPT toplevel_selector; "{" -> Vernacexpr.VernacSubproof g ] ] - ; - command: - [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; - l = OPT [ "using"; l = G_vernac.section_subset_expr -> l ] -> - Vernacexpr.VernacProof (Some (in_tac ta), l) - | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; - ta = OPT [ "with"; ta = Pltac.tactic -> in_tac ta ] -> - Vernacexpr.VernacProof (ta,Some l) ] ] - ; - hint: - [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; - tac = Pltac.tactic -> - Hints.HintsExtern (n,c, in_tac tac) ] ] - ; - operconstr: LEVEL "0" - [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> - let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in - CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ] - ; - END - -open Stdarg -open Tacarg -open Vernacexpr -open Vernac_classifier -open Goptions -open Libnames - -let print_info_trace = ref None - -let _ = declare_int_option { - optdepr = false; - optname = "print info trace"; - optkey = ["Info" ; "Level"]; - optread = (fun () -> !print_info_trace); - optwrite = fun n -> print_info_trace := n; -} - -let vernac_solve n info tcom b = - let open Goal_select in - let status = Proof_global.with_current_proof (fun etac p -> - let with_end_tac = if b then Some etac else None in - let global = match n with SelectAll | SelectList _ -> true | _ -> false in - let info = Option.append info !print_info_trace in - let (p,status) = - Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p - in - (* in case a strict subtree was completed, - go back to the top of the prooftree *) - let p = Proof.maximal_unfocus Vernacentries.command_focus p in - p,status) in - if not status then Feedback.feedback Feedback.AddedAxiom - -let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s - -VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector -| [ toplevel_selector(s) ] -> [ s ] -END - -let pr_ltac_info n = str "Info" ++ spc () ++ int n - -VERNAC ARGUMENT EXTEND ltac_info PRINTED BY pr_ltac_info -| [ "Info" natural(n) ] -> [ n ] -END - -let pr_ltac_use_default b = - if b then (* Bug: a space is inserted before "..." *) str ".." else mt () - -VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY pr_ltac_use_default -| [ "." ] -> [ false ] -| [ "..." ] -> [ true ] -END - -let is_anonymous_abstract = function - | TacAbstract (_,None) -> true - | TacSolve [TacAbstract (_,None)] -> true - | _ -> false -let rm_abstract = function - | TacAbstract (t,_) -> t - | TacSolve [TacAbstract (t,_)] -> TacSolve [t] - | x -> x -let is_explicit_terminator = function TacSolve _ -> true | _ -> false - -VERNAC tactic_mode EXTEND VernacSolve -| [ - ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ classify_as_proofstep ] -> [ - let g = Option.default (Goal_select.get_default_goal_selector ()) g in - vernac_solve g n t def - ] -| [ - "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => - [ - let anon_abstracting_tac = is_anonymous_abstract t in - let solving_tac = is_explicit_terminator t in - let parallel = `Yes (solving_tac,anon_abstracting_tac) in - let pbr = if solving_tac then Some "par" else None in - VtProofStep{ parallel = parallel; proof_block_detection = pbr }, - VtLater - ] -> [ - let t = rm_abstract t in - vernac_solve Goal_select.SelectAll n t def - ] -END - -let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" - -VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY pr_ltac_tactic_level -| [ "(" "at" "level" natural(n) ")" ] -> [ n ] -END - -VERNAC ARGUMENT EXTEND ltac_production_sep -| [ "," string(sep) ] -> [ sep ] -END - -let pr_ltac_production_item = function -| Tacentries.TacTerm s -> quote (str s) -| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg -| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false -| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> - let sep = match sep with - | None -> mt () - | Some sep -> str "," ++ spc () ++ quote (str sep) - in - str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" - -VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item -| [ string(s) ] -> [ Tacentries.TacTerm s ] -| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ] -| [ ident(nt) ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND VernacTacticNotation -| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => - [ VtSideff [], VtNow ] -> - [ fun ~atts ~st -> let open Vernacinterp in - let n = Option.default 0 n in - let deprecation = atts.deprecated in - Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; - st - ] -END - -VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY -| [ "Print" "Ltac" reference(r) ] -> - [ Feedback.msg_notice (Tacintern.print_ltac r) ] -END - -VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY -| [ "Locate" "Ltac" reference(r) ] -> - [ Tacentries.print_located_tactic r ] -END - -let pr_ltac_ref = Libnames.pr_qualid - -let pr_tacdef_body tacdef_body = - let id, redef, body = - match tacdef_body with - | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body - | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body - in - let idl, body = - match body with - | Tacexpr.TacFun (idl,b) -> idl,b - | _ -> [], body in - id ++ - prlist (function Name.Anonymous -> str " _" - | Name.Name id -> spc () ++ Id.print id) idl - ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) - ++ Pptactic.pr_raw_tactic body - -VERNAC ARGUMENT EXTEND ltac_tacdef_body -PRINTED BY pr_tacdef_body -| [ tacdef_body(t) ] -> [ t ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND VernacDeclareTacticDefinition -| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => [ - VtSideff (List.map (function - | TacticDefinition ({CAst.v=r},_) -> r - | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater - ] -> [ fun ~atts ~st -> let open Vernacinterp in - let deprecation = atts.deprecated in - Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; - st - ] -END - -VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY -| [ "Print" "Ltac" "Signatures" ] -> [ Tacentries.print_ltacs () ] -END diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg new file mode 100644 index 0000000000..d62f985350 --- /dev/null +++ b/plugins/ltac/g_ltac.mlg @@ -0,0 +1,560 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* a + | e -> Tacexp (e:raw_tactic_expr) + +let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () +let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat +let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c +let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac + +let reference_to_id qid = + if Libnames.qualid_is_ident qid then + CAst.make ?loc:qid.CAst.loc @@ Libnames.qualid_basename qid + else + CErrors.user_err ?loc:qid.CAst.loc + (str "This expression should be a simple identifier.") + +let tactic_mode = Entry.create "vernac:tactic_command" + +let new_entry name = + let e = Entry.create name in + e + +let toplevel_selector = new_entry "vernac:toplevel_selector" +let tacdef_body = new_entry "tactic:tacdef_body" + +(* Registers the Classic Proof Mode (which uses [tactic_mode] as a parser for + proof editing and changes nothing else). Then sets it as the default proof mode. *) +let _ = + let mode = { + Proof_global.name = "Classic"; + set = (fun () -> Pvernac.set_command_entry tactic_mode); + reset = (fun () -> Pvernac.(set_command_entry noedit_mode)); + } in + Proof_global.register_proof_mode mode + +(* Hack to parse "[ id" without dropping [ *) +let test_bracket_ident = + Gram.Entry.of_parser "test_bracket_ident" + (fun strm -> + match stream_nth 0 strm with + | KEYWORD "[" -> + (match stream_nth 1 strm with + | IDENT _ -> () + | _ -> raise Stream.Failure) + | _ -> raise Stream.Failure) + +(* Tactics grammar rules *) + +let hint = G_proofs.hint + +} + +GRAMMAR EXTEND Gram + GLOBAL: tactic tacdef_body tactic_expr binder_tactic tactic_arg command hint + tactic_mode constr_may_eval constr_eval toplevel_selector + operconstr; + + tactic_then_last: + [ [ "|"; lta = LIST0 (OPT tactic_expr) SEP "|" -> + { Array.map (function None -> TacId [] | Some t -> t) (Array.of_list lta) } + | -> { [||] } + ] ] + ; + tactic_then_gen: + [ [ ta = tactic_expr; "|"; tg = tactic_then_gen -> { let (first,last) = tg in (ta::first, last) } + | ta = tactic_expr; ".."; l = tactic_then_last -> { ([], Some (ta, l)) } + | ".."; l = tactic_then_last -> { ([], Some (TacId [], l)) } + | ta = tactic_expr -> { ([ta], None) } + | "|"; tg = tactic_then_gen -> { let (first,last) = tg in (TacId [] :: first, last) } + | -> { ([TacId []], None) } + ] ] + ; + tactic_then_locality: (* [true] for the local variant [TacThens] and [false] + for [TacExtend] *) + [ [ "[" ; l = OPT">" -> { if Option.is_empty l then true else false } ] ] + ; + tactic_expr: + [ "5" RIGHTA + [ te = binder_tactic -> { te } ] + | "4" LEFTA + [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> { TacThen (ta0, ta1) } + | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> { TacThen (ta0,ta1) } + | ta0 = tactic_expr; ";"; l = tactic_then_locality; tg = tactic_then_gen; "]" -> { + let (first,tail) = tg in + match l , tail with + | false , Some (t,last) -> TacThen (ta0,TacExtendTac (Array.of_list first, t, last)) + | true , Some (t,last) -> TacThens3parts (ta0, Array.of_list first, t, last) + | false , None -> TacThen (ta0,TacDispatch first) + | true , None -> TacThens (ta0,first) } ] + | "3" RIGHTA + [ IDENT "try"; ta = tactic_expr -> { TacTry ta } + | IDENT "do"; n = int_or_var; ta = tactic_expr -> { TacDo (n,ta) } + | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> { TacTimeout (n,ta) } + | IDENT "time"; s = OPT string; ta = tactic_expr -> { TacTime (s,ta) } + | IDENT "repeat"; ta = tactic_expr -> { TacRepeat ta } + | IDENT "progress"; ta = tactic_expr -> { TacProgress ta } + | IDENT "once"; ta = tactic_expr -> { TacOnce ta } + | IDENT "exactly_once"; ta = tactic_expr -> { TacExactlyOnce ta } + | IDENT "infoH"; ta = tactic_expr -> { TacShowHyps ta } +(*To do: put Abstract in Refiner*) + | IDENT "abstract"; tc = NEXT -> { TacAbstract (tc,None) } + | IDENT "abstract"; tc = NEXT; "using"; s = ident -> + { TacAbstract (tc,Some s) } + | sel = selector; ta = tactic_expr -> { TacSelect (sel, ta) } ] +(*End of To do*) + | "2" RIGHTA + [ ta0 = tactic_expr; "+"; ta1 = binder_tactic -> { TacOr (ta0,ta1) } + | ta0 = tactic_expr; "+"; ta1 = tactic_expr -> { TacOr (ta0,ta1) } + | IDENT "tryif" ; ta = tactic_expr ; + "then" ; tat = tactic_expr ; + "else" ; tae = tactic_expr -> { TacIfThenCatch(ta,tat,tae) } + | ta0 = tactic_expr; "||"; ta1 = binder_tactic -> { TacOrelse (ta0,ta1) } + | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> { TacOrelse (ta0,ta1) } ] + | "1" RIGHTA + [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" -> + { TacMatchGoal (b,false,mrl) } + | b = match_key; IDENT "reverse"; IDENT "goal"; "with"; + mrl = match_context_list; "end" -> + { TacMatchGoal (b,true,mrl) } + | b = match_key; c = tactic_expr; "with"; mrl = match_list; "end" -> + { TacMatch (b,c,mrl) } + | IDENT "first" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + { TacFirst l } + | IDENT "solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" -> + { TacSolve l } + | IDENT "idtac"; l = LIST0 message_token -> { TacId l } + | g=failkw; n = [ n = int_or_var -> { n } | -> { fail_default_value } ]; + l = LIST0 message_token -> { TacFail (g,n,l) } + | st = simple_tactic -> { st } + | a = tactic_arg -> { TacArg(Loc.tag ~loc a) } + | r = reference; la = LIST0 tactic_arg_compat -> + { TacArg(Loc.tag ~loc @@ TacCall (Loc.tag ~loc (r,la))) } ] + | "0" + [ "("; a = tactic_expr; ")" -> { a } + | "["; ">"; tg = tactic_then_gen; "]" -> { + let (tf,tail) = tg in + begin match tail with + | Some (t,tl) -> TacExtendTac(Array.of_list tf,t,tl) + | None -> TacDispatch tf + end } + | a = tactic_atom -> { TacArg (Loc.tag ~loc a) } ] ] + ; + failkw: + [ [ IDENT "fail" -> { TacLocal } | IDENT "gfail" -> { TacGlobal } ] ] + ; + (* binder_tactic: level 5 of tactic_expr *) + binder_tactic: + [ RIGHTA + [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" -> + { TacFun (it,body) } + | "let"; isrec = [IDENT "rec" -> { true } | -> { false } ]; + llc = LIST1 let_clause SEP "with"; "in"; + body = tactic_expr LEVEL "5" -> { TacLetIn (isrec,llc,body) } + | IDENT "info"; tc = tactic_expr LEVEL "5" -> { TacInfo tc } ] ] + ; + (* Tactic arguments to the right of an application *) + tactic_arg_compat: + [ [ a = tactic_arg -> { a } + | c = Constr.constr -> { (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c)) } + (* Unambiguous entries: tolerated w/o "ltac:" modifier *) + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + ; + (* Can be used as argument and at toplevel in tactic expressions. *) + tactic_arg: + [ [ c = constr_eval -> { ConstrMayEval c } + | IDENT "fresh"; l = LIST0 fresh_id -> { TacFreshId l } + | IDENT "type_term"; c=uconstr -> { TacPretype c } + | IDENT "numgoals" -> { TacNumgoals } ] ] + ; + (* If a qualid is given, use its short name. TODO: have the shortest + non ambiguous name where dots are replaced by "_"? Probably too + verbose most of the time. *) + fresh_id: + [ [ s = STRING -> { Locus.ArgArg s (*| id = ident -> Locus.ArgVar (!@loc,id)*) } + | qid = qualid -> { Locus.ArgVar (CAst.make ~loc @@ Libnames.qualid_basename qid) } ] ] + ; + constr_eval: + [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr -> + { ConstrEval (rtc,c) } + | IDENT "context"; id = identref; "["; c = Constr.lconstr; "]" -> + { ConstrContext (id,c) } + | IDENT "type"; IDENT "of"; c = Constr.constr -> + { ConstrTypeOf c } ] ] + ; + constr_may_eval: (* For extensions *) + [ [ c = constr_eval -> { c } + | c = Constr.constr -> { ConstrTerm c } ] ] + ; + tactic_atom: + [ [ n = integer -> { TacGeneric (genarg_of_int n) } + | r = reference -> { TacCall (Loc.tag ~loc (r,[])) } + | "()" -> { TacGeneric (genarg_of_unit ()) } ] ] + ; + match_key: + [ [ "match" -> { Once } + | "lazymatch" -> { Select } + | "multimatch" -> { General } ] ] + ; + input_fun: + [ [ "_" -> { Name.Anonymous } + | l = ident -> { Name.Name l } ] ] + ; + let_clause: + [ [ idr = identref; ":="; te = tactic_expr -> + { (CAst.map (fun id -> Name id) idr, arg_of_expr te) } + | na = ["_" -> { CAst.make ~loc Anonymous } ]; ":="; te = tactic_expr -> + { (na, arg_of_expr te) } + | idr = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + { (CAst.map (fun id -> Name id) idr, arg_of_expr (TacFun(args,te))) } ] ] + ; + match_pattern: + [ [ IDENT "context"; oid = OPT Constr.ident; + "["; pc = Constr.lconstr_pattern; "]" -> + { Subterm (oid, pc) } + | pc = Constr.lconstr_pattern -> { Term pc } ] ] + ; + match_hyps: + [ [ na = name; ":"; mp = match_pattern -> { Hyp (na, mp) } + | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> { Def (na, mpv, mpt) } + | na = name; ":="; mpv = match_pattern -> + { let t, ty = + match mpv with + | Term t -> (match t with + | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty) + | _ -> mpv, None) + | _ -> mpv, None + in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty) } + ] ] + ; + match_context_rule: + [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "=>"; te = tactic_expr -> { Pat (largs, mp, te) } + | "["; largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern; + "]"; "=>"; te = tactic_expr -> { Pat (largs, mp, te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] + ; + match_context_list: + [ [ mrl = LIST1 match_context_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_context_rule SEP "|" -> { mrl } ] ] + ; + match_rule: + [ [ mp = match_pattern; "=>"; te = tactic_expr -> { Pat ([],mp,te) } + | "_"; "=>"; te = tactic_expr -> { All te } ] ] + ; + match_list: + [ [ mrl = LIST1 match_rule SEP "|" -> { mrl } + | "|"; mrl = LIST1 match_rule SEP "|" -> { mrl } ] ] + ; + message_token: + [ [ id = identref -> { MsgIdent id } + | s = STRING -> { MsgString s } + | n = integer -> { MsgInt n } ] ] + ; + + ltac_def_kind: + [ [ ":=" -> { false } + | "::=" -> { true } ] ] + ; + + (* Definitions for tactics *) + tacdef_body: + [ [ name = Constr.global; it=LIST1 input_fun; + redef = ltac_def_kind; body = tactic_expr -> + { if redef then Tacexpr.TacticRedefinition (name, TacFun (it, body)) + else + let id = reference_to_id name in + Tacexpr.TacticDefinition (id, TacFun (it, body)) } + | name = Constr.global; redef = ltac_def_kind; + body = tactic_expr -> + { if redef then Tacexpr.TacticRedefinition (name, body) + else + let id = reference_to_id name in + Tacexpr.TacticDefinition (id, body) } + ] ] + ; + tactic: + [ [ tac = tactic_expr -> { tac } ] ] + ; + + range_selector: + [ [ n = natural ; "-" ; m = natural -> { (n, m) } + | n = natural -> { (n, n) } ] ] + ; + (* We unfold a range selectors list once so that we can make a special case + * for a unique SelectNth selector. *) + range_selector_or_nth: + [ [ n = natural ; "-" ; m = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { Goal_select.SelectList ((n, m) :: Option.default [] l) } + | n = natural; + l = OPT [","; l = LIST1 range_selector SEP "," -> { l } ] -> + { let open Goal_select in + Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l } ] ] + ; + selector_body: + [ [ l = range_selector_or_nth -> { l } + | test_bracket_ident; "["; id = ident; "]" -> { Goal_select.SelectId id } ] ] + ; + selector: + [ [ IDENT "only"; sel = selector_body; ":" -> { sel } ] ] + ; + toplevel_selector: + [ [ sel = selector_body; ":" -> { sel } + | "!"; ":" -> { Goal_select.SelectAlreadyFocused } + | IDENT "all"; ":" -> { Goal_select.SelectAll } ] ] + ; + tactic_mode: + [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> { tac g } + | g = OPT toplevel_selector; "{" -> { Vernacexpr.VernacSubproof g } ] ] + ; + command: + [ [ IDENT "Proof"; "with"; ta = Pltac.tactic; + l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] -> + { Vernacexpr.VernacProof (Some (in_tac ta), l) } + | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr; + ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] -> + { Vernacexpr.VernacProof (ta,Some l) } ] ] + ; + hint: + [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; + tac = Pltac.tactic -> + { Hints.HintsExtern (n,c, in_tac tac) } ] ] + ; + operconstr: LEVEL "0" + [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> + { let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in + CAst.make ~loc @@ CHole (None, IntroAnonymous, Some arg) } ] ] + ; + END + +{ + +open Stdarg +open Tacarg +open Vernacexpr +open Vernac_classifier +open Goptions +open Libnames + +let print_info_trace = ref None + +let _ = declare_int_option { + optdepr = false; + optname = "print info trace"; + optkey = ["Info" ; "Level"]; + optread = (fun () -> !print_info_trace); + optwrite = fun n -> print_info_trace := n; +} + +let vernac_solve n info tcom b = + let open Goal_select in + let status = Proof_global.with_current_proof (fun etac p -> + let with_end_tac = if b then Some etac else None in + let global = match n with SelectAll | SelectList _ -> true | _ -> false in + let info = Option.append info !print_info_trace in + let (p,status) = + Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p + in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p,status) in + if not status then Feedback.feedback Feedback.AddedAxiom + +let pr_ltac_selector s = Pptactic.pr_goal_selector ~toplevel:true s + +} + +VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY { pr_ltac_selector } +| [ toplevel_selector(s) ] -> { s } +END + +{ + +let pr_ltac_info n = str "Info" ++ spc () ++ int n + +} + +VERNAC ARGUMENT EXTEND ltac_info PRINTED BY { pr_ltac_info } +| [ "Info" natural(n) ] -> { n } +END + +{ + +let pr_ltac_use_default b = + if b then (* Bug: a space is inserted before "..." *) str ".." else mt () + +} + +VERNAC ARGUMENT EXTEND ltac_use_default PRINTED BY { pr_ltac_use_default } +| [ "." ] -> { false } +| [ "..." ] -> { true } +END + +{ + +let is_anonymous_abstract = function + | TacAbstract (_,None) -> true + | TacSolve [TacAbstract (_,None)] -> true + | _ -> false +let rm_abstract = function + | TacAbstract (t,_) -> t + | TacSolve [TacAbstract (t,_)] -> TacSolve [t] + | x -> x +let is_explicit_terminator = function TacSolve _ -> true | _ -> false + +} + +VERNAC { tactic_mode } EXTEND VernacSolve +| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + { classify_as_proofstep } -> { + let g = Option.default (Goal_select.get_default_goal_selector ()) g in + vernac_solve g n t def + } +| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] => + { + let anon_abstracting_tac = is_anonymous_abstract t in + let solving_tac = is_explicit_terminator t in + let parallel = `Yes (solving_tac,anon_abstracting_tac) in + let pbr = if solving_tac then Some "par" else None in + VtProofStep{ parallel = parallel; proof_block_detection = pbr }, + VtLater + } -> { + let t = rm_abstract t in + vernac_solve Goal_select.SelectAll n t def + } +END + +{ + +let pr_ltac_tactic_level n = str "(at level " ++ int n ++ str ")" + +} + +VERNAC ARGUMENT EXTEND ltac_tactic_level PRINTED BY { pr_ltac_tactic_level } +| [ "(" "at" "level" natural(n) ")" ] -> { n } +END + +VERNAC ARGUMENT EXTEND ltac_production_sep +| [ "," string(sep) ] -> { sep } +END + +{ + +let pr_ltac_production_item = function +| Tacentries.TacTerm s -> quote (str s) +| Tacentries.TacNonTerm (_, ((arg, None), None)) -> str arg +| Tacentries.TacNonTerm (_, ((arg, Some _), None)) -> assert false +| Tacentries.TacNonTerm (_, ((arg, sep), Some id)) -> + let sep = match sep with + | None -> mt () + | Some sep -> str "," ++ spc () ++ quote (str sep) + in + str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" + +} + +VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY { pr_ltac_production_item } +| [ string(s) ] -> { Tacentries.TacTerm s } +| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) } +| [ ident(nt) ] -> + { Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) } +END + +VERNAC COMMAND EXTEND VernacTacticNotation +| [ "Tactic" "Notation" ltac_tactic_level_opt(n) ne_ltac_production_item_list(r) ":=" tactic(e) ] => + { VtSideff [], VtNow } -> + { let open Vernacinterp in + let n = Option.default 0 n in + let deprecation = atts.deprecated in + Tacentries.add_tactic_notation (Locality.make_module_locality atts.locality) n ?deprecation r e; + } +END + +VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY +| [ "Print" "Ltac" reference(r) ] -> + { Feedback.msg_notice (Tacintern.print_ltac r) } +END + +VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY +| [ "Locate" "Ltac" reference(r) ] -> + { Tacentries.print_located_tactic r } +END + +{ + +let pr_ltac_ref = Libnames.pr_qualid + +let pr_tacdef_body tacdef_body = + let id, redef, body = + match tacdef_body with + | TacticDefinition ({CAst.v=id}, body) -> Id.print id, false, body + | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body + in + let idl, body = + match body with + | Tacexpr.TacFun (idl,b) -> idl,b + | _ -> [], body in + id ++ + prlist (function Name.Anonymous -> str " _" + | Name.Name id -> spc () ++ Id.print id) idl + ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) + ++ Pptactic.pr_raw_tactic body + +} + +VERNAC ARGUMENT EXTEND ltac_tacdef_body +PRINTED BY { pr_tacdef_body } +| [ tacdef_body(t) ] -> { t } +END + +VERNAC COMMAND EXTEND VernacDeclareTacticDefinition +| [ "Ltac" ne_ltac_tacdef_body_list_sep(l, "with") ] => { + VtSideff (List.map (function + | TacticDefinition ({CAst.v=r},_) -> r + | TacticRedefinition (qid,_) -> qualid_basename qid) l), VtLater + } -> { let open Vernacinterp in + let deprecation = atts.deprecated in + Tacentries.register_ltac (Locality.make_module_locality atts.locality) ?deprecation l; + } +END + +VERNAC COMMAND EXTEND VernacPrintLtacs CLASSIFIED AS QUERY +| [ "Print" "Ltac" "Signatures" ] -> { Tacentries.print_ltacs () } +END diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 deleted file mode 100644 index 1f56244c75..0000000000 --- a/plugins/ltac/g_obligations.ml4 +++ /dev/null @@ -1,161 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* - snd (get_default_tactic ()) - end in - Obligations.default_tactic := tac - -let with_tac f tac = - let env = Genintern.empty_glob_sign (Global.env ()) in - let tac = match tac with - | None -> None - | Some tac -> - let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in - let _, tac = Genintern.generic_intern env tac in - Some tac - in - f tac - -(* We define new entries for programs, with the use of this module - * Subtac. These entries are named Subtac. - *) - -module Gram = Pcoq.Gram -module Tactic = Pltac - -open Pcoq - -let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") - -type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type - -let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = - Genarg.create_arg "withtac" - -let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) - -GEXTEND Gram - GLOBAL: withtac; - - withtac: - [ [ "with"; t = Tactic.tactic -> Some t - | -> None ] ] - ; - - Constr.closed_binder: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref !@loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [CLocalAssum ([id], default_binder_kind, typ)] - ] ]; - - END - -open Obligations - -let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac -let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac - -let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) - -VERNAC COMMAND EXTEND Obligations CLASSIFIED BY classify_obbl -| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, Some name, Some t) tac ] -| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> - [ obligation (num, Some name, None) tac ] -| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> - [ obligation (num, None, Some t) tac ] -| [ "Obligation" integer(num) withtac(tac) ] -> - [ obligation (num, None, None) tac ] -| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> - [ next_obligation (Some name) tac ] -| [ "Next" "Obligation" withtac(tac) ] -> [ next_obligation None tac ] -END - -VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF -| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> - [ try_solve_obligation num None (Some (Tacinterp.interp t)) ] -END - -VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> - [ try_solve_obligations (Some name) (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" "with" tactic(t) ] -> - [ try_solve_obligations None (Some (Tacinterp.interp t)) ] -| [ "Solve" "Obligations" ] -> - [ try_solve_obligations None None ] -END - -VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF -| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> - [ solve_all_obligations (Some (Tacinterp.interp t)) ] -| [ "Solve" "All" "Obligations" ] -> - [ solve_all_obligations None ] -END - -VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF -| [ "Admit" "Obligations" "of" ident(name) ] -> [ admit_obligations (Some name) ] -| [ "Admit" "Obligations" ] -> [ admit_obligations None ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND Set_Solver CLASSIFIED AS SIDEFF -| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ - fun ~atts ~st -> begin - let open Vernacinterp in - set_default_tactic - (Locality.make_section_locality atts.locality) - (Tacintern.glob_tactic t); - st - end] -END - -open Pp - -VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY -| [ "Show" "Obligation" "Tactic" ] -> [ - Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) ] -END - -VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY -| [ "Obligations" "of" ident(name) ] -> [ show_obligations (Some name) ] -| [ "Obligations" ] -> [ show_obligations None ] -END - -VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY -| [ "Preterm" "of" ident(name) ] -> [ Feedback.msg_info (show_term (Some name)) ] -| [ "Preterm" ] -> [ Feedback.msg_info (show_term None) ] -END - -open Pp - -(* Declare a printer for the content of Program tactics *) -let () = - let printer _ _ _ = function - | None -> mt () - | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac - in - Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg new file mode 100644 index 0000000000..26f2b08d3a --- /dev/null +++ b/plugins/ltac/g_obligations.mlg @@ -0,0 +1,173 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* + snd (get_default_tactic ()) + end in + Obligations.default_tactic := tac + +let with_tac f tac = + let env = Genintern.empty_glob_sign (Global.env ()) in + let tac = match tac with + | None -> None + | Some tac -> + let tac = Genarg.in_gen (Genarg.rawwit wit_ltac) tac in + let _, tac = Genintern.generic_intern env tac in + Some tac + in + f tac + +(* We define new entries for programs, with the use of this module + * Subtac. These entries are named Subtac. + *) + +module Gram = Pcoq.Gram +module Tactic = Pltac + +open Pcoq + +let sigref loc = mkRefC (Libnames.qualid_of_string ~loc "Coq.Init.Specif.sig") + +type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_argument_type + +let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type = + Genarg.create_arg "withtac" + +let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac) + +} + +GRAMMAR EXTEND Gram + GLOBAL: withtac; + + withtac: + [ [ "with"; t = Tactic.tactic -> { Some t } + | -> { None } ] ] + ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> { + let typ = mkAppC (sigref loc, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [CLocalAssum ([id], default_binder_kind, typ)] } + ] ]; + + END + +{ + +open Obligations + +let obligation obl tac = with_tac (fun t -> Obligations.obligation obl t) tac +let next_obligation obl tac = with_tac (fun t -> Obligations.next_obligation obl t) tac + +let classify_obbl _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]), VtLater) + +} + +VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } +| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] -> + { obligation (num, Some name, Some t) tac } +| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] -> + { obligation (num, Some name, None) tac } +| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] -> + { obligation (num, None, Some t) tac } +| [ "Obligation" integer(num) withtac(tac) ] -> + { obligation (num, None, None) tac } +| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] -> + { next_obligation (Some name) tac } +| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac } +END + +VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF +| [ "Solve" "Obligation" integer(num) "of" ident(name) "with" tactic(t) ] -> + { try_solve_obligation num (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligation" integer(num) "with" tactic(t) ] -> + { try_solve_obligation num None (Some (Tacinterp.interp t)) } +END + +VERNAC COMMAND EXTEND Solve_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "Obligations" "of" ident(name) "with" tactic(t) ] -> + { try_solve_obligations (Some name) (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" "with" tactic(t) ] -> + { try_solve_obligations None (Some (Tacinterp.interp t)) } +| [ "Solve" "Obligations" ] -> + { try_solve_obligations None None } +END + +VERNAC COMMAND EXTEND Solve_All_Obligations CLASSIFIED AS SIDEFF +| [ "Solve" "All" "Obligations" "with" tactic(t) ] -> + { solve_all_obligations (Some (Tacinterp.interp t)) } +| [ "Solve" "All" "Obligations" ] -> + { solve_all_obligations None } +END + +VERNAC COMMAND EXTEND Admit_Obligations CLASSIFIED AS SIDEFF +| [ "Admit" "Obligations" "of" ident(name) ] -> { admit_obligations (Some name) } +| [ "Admit" "Obligations" ] -> { admit_obligations None } +END + +VERNAC COMMAND EXTEND Set_Solver CLASSIFIED AS SIDEFF +| [ "Obligation" "Tactic" ":=" tactic(t) ] -> { + let open Vernacinterp in + set_default_tactic + (Locality.make_section_locality atts.locality) + (Tacintern.glob_tactic t); + } +END + +{ + +open Pp + +} + +VERNAC COMMAND EXTEND Show_Solver CLASSIFIED AS QUERY +| [ "Show" "Obligation" "Tactic" ] -> { + Feedback.msg_info (str"Program obligation tactic is " ++ print_default_tactic ()) } +END + +VERNAC COMMAND EXTEND Show_Obligations CLASSIFIED AS QUERY +| [ "Obligations" "of" ident(name) ] -> { show_obligations (Some name) } +| [ "Obligations" ] -> { show_obligations None } +END + +VERNAC COMMAND EXTEND Show_Preterm CLASSIFIED AS QUERY +| [ "Preterm" "of" ident(name) ] -> { Feedback.msg_info (show_term (Some name)) } +| [ "Preterm" ] -> { Feedback.msg_info (show_term None) } +END + +{ + +(* Declare a printer for the content of Program tactics *) +let () = + let printer _ _ _ = function + | None -> mt () + | Some tac -> str "with" ++ spc () ++ Pptactic.pr_raw_tactic tac + in + Pptactic.declare_extra_vernac_genarg_pprule wit_withtac printer + +} diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 deleted file mode 100644 index f1634f1561..0000000000 --- a/plugins/ltac/g_rewrite.ml4 +++ /dev/null @@ -1,297 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* [ bl ] -END - -type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast -type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast - -let interp_strategy ist gl s = - let sigma = project gl in - sigma, strategy_of_ast s -let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s -let subst_strategy s str = str - -let pr_strategy _ _ _ (s : strategy) = Pp.str "" -let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in - Rewrite.pr_strategy prc prr s -let pr_glob_strategy prc prlc _ (s : glob_strategy) = - let prr = Pptactic.pr_red_expr - (Ppconstr.pr_constr_expr, - Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_qualid, - Ppconstr.pr_constr_expr) - in - Rewrite.pr_strategy prc prr s - -ARGUMENT EXTEND rewstrategy - PRINTED BY pr_strategy - - INTERPRETED BY interp_strategy - GLOBALIZED BY glob_strategy - SUBSTITUTED BY subst_strategy - - RAW_PRINTED BY pr_raw_strategy - GLOB_PRINTED BY pr_glob_strategy - - [ glob(c) ] -> [ StratConstr (c, true) ] - | [ "<-" constr(c) ] -> [ StratConstr (c, false) ] - | [ "subterms" rewstrategy(h) ] -> [ StratUnary (Subterms, h) ] - | [ "subterm" rewstrategy(h) ] -> [ StratUnary (Subterm, h) ] - | [ "innermost" rewstrategy(h) ] -> [ StratUnary(Innermost, h) ] - | [ "outermost" rewstrategy(h) ] -> [ StratUnary(Outermost, h) ] - | [ "bottomup" rewstrategy(h) ] -> [ StratUnary(Bottomup, h) ] - | [ "topdown" rewstrategy(h) ] -> [ StratUnary(Topdown, h) ] - | [ "id" ] -> [ StratId ] - | [ "fail" ] -> [ StratFail ] - | [ "refl" ] -> [ StratRefl ] - | [ "progress" rewstrategy(h) ] -> [ StratUnary (Progress, h) ] - | [ "try" rewstrategy(h) ] -> [ StratUnary (Try, h) ] - | [ "any" rewstrategy(h) ] -> [ StratUnary (Any, h) ] - | [ "repeat" rewstrategy(h) ] -> [ StratUnary (Repeat, h) ] - | [ rewstrategy(h) ";" rewstrategy(h') ] -> [ StratBinary (Compose, h, h') ] - | [ "(" rewstrategy(h) ")" ] -> [ h ] - | [ "choice" rewstrategy(h) rewstrategy(h') ] -> [ StratBinary (Choice, h, h') ] - | [ "old_hints" preident(h) ] -> [ StratHints (true, h) ] - | [ "hints" preident(h) ] -> [ StratHints (false, h) ] - | [ "terms" constr_list(h) ] -> [ StratTerms h ] - | [ "eval" red_expr(r) ] -> [ StratEval r ] - | [ "fold" constr(c) ] -> [ StratFold c ] -END - -(* By default the strategy for "rewrite_db" is top-down *) - -let db_strat db = StratUnary (Topdown, StratHints (false, db)) -let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) - -TACTIC EXTEND rewrite_strat -| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> [ cl_rewrite_clause_strat s (Some id) ] -| [ "rewrite_strat" rewstrategy(s) ] -> [ cl_rewrite_clause_strat s None ] -| [ "rewrite_db" preident(db) "in" hyp(id) ] -> [ cl_rewrite_clause_db db (Some id) ] -| [ "rewrite_db" preident(db) ] -> [ cl_rewrite_clause_db db None ] -END - -let clsubstitute o c = - Proofview.Goal.enter begin fun gl -> - let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in - let hyps = Tacmach.New.pf_ids_of_hyps gl in - Tacticals.New.tclMAP - (fun cl -> - match cl with - | Some id when is_tac id -> Tacticals.New.tclIDTAC - | _ -> cl_rewrite_clause c o AllOccurrences cl) - (None :: List.map (fun id -> Some id) hyps) - end - -TACTIC EXTEND substitute -| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ] -END - - -(* Compatibility with old Setoids *) - -TACTIC EXTEND setoid_rewrite - [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] - -> [ cl_rewrite_clause c o AllOccurrences None ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> - [ cl_rewrite_clause c o AllOccurrences (Some id) ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> - [ cl_rewrite_clause c o (occurrences_of occ) None ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] - | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> - [ cl_rewrite_clause c o (occurrences_of occ) (Some id) ] -END - -VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) (Some lemma2) None ] - - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None None ] - | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation a aeq n None None None ] -END - -VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) - "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) None ] - | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n None (Some lemma2) (Some lemma3) ] -END - -VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) None (Some lemma3) ] - | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] - | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation a aeq n None None (Some lemma3) ] -END - -type binders_argtype = local_binder_expr list - -let wit_binders = - (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) - -let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) - -let () = - let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in - Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer - -open Pcoq - -GEXTEND Gram - GLOBAL: binders; - binders: - [ [ b = Pcoq.Constr.binders -> b ] ]; -END - -VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) - "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) - "reflexivity" "proved" "by" constr(lemma1) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None None ] -END - -VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) None ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) ] -END - -VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF - [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) - "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) ] - | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) - "as" ident(n) ] -> - [ declare_relation ~binders:b a aeq n None None (Some lemma3) ] -END - -VERNAC COMMAND FUNCTIONAL EXTEND AddSetoid1 CLASSIFIED AS SIDEFF - [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; - st - ] - | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> - [ fun ~atts ~st -> let open Vernacinterp in - add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; - st - ] - | [ "Add" "Morphism" constr(m) ":" ident(n) ] - (* This command may or may not open a goal *) - => [ Vernacexpr.VtUnknown, Vernacexpr.VtNow ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; - st - ] - | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; - st - ] - | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) - "with" "signature" lconstr(s) "as" ident(n) ] - => [ Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) ] - -> [ fun ~atts ~st -> let open Vernacinterp in - add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; - st - ] -END - -TACTIC EXTEND setoid_symmetry - [ "setoid_symmetry" ] -> [ setoid_symmetry ] - | [ "setoid_symmetry" "in" hyp(n) ] -> [ setoid_symmetry_in n ] -END - -TACTIC EXTEND setoid_reflexivity -[ "setoid_reflexivity" ] -> [ setoid_reflexivity ] -END - -TACTIC EXTEND setoid_transitivity - [ "setoid_transitivity" constr(t) ] -> [ setoid_transitivity (Some t) ] -| [ "setoid_etransitivity" ] -> [ setoid_transitivity None ] -END - -VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY - [ "Print" "Rewrite" "HintDb" preident(s) ] -> - [ let sigma, env = Pfedit.get_current_context () in - Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) ] -END diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg new file mode 100644 index 0000000000..3e47724c4c --- /dev/null +++ b/plugins/ltac/g_rewrite.mlg @@ -0,0 +1,318 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* { bl } +END + +{ + +type raw_strategy = (constr_expr, Tacexpr.raw_red_expr) strategy_ast +type glob_strategy = (Tacexpr.glob_constr_and_expr, Tacexpr.raw_red_expr) strategy_ast + +let interp_strategy ist gl s = + let sigma = project gl in + sigma, strategy_of_ast s +let glob_strategy ist s = map_strategy (Tacintern.intern_constr ist) (fun c -> c) s +let subst_strategy s str = str + +let pr_strategy _ _ _ (s : strategy) = Pp.str "" +let pr_raw_strategy prc prlc _ (s : raw_strategy) = + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in + Rewrite.pr_strategy prc prr s +let pr_glob_strategy prc prlc _ (s : glob_strategy) = + let prr = Pptactic.pr_red_expr + (Ppconstr.pr_constr_expr, + Ppconstr.pr_lconstr_expr, + Pputils.pr_or_by_notation Libnames.pr_qualid, + Ppconstr.pr_constr_expr) + in + Rewrite.pr_strategy prc prr s + +} + +ARGUMENT EXTEND rewstrategy + PRINTED BY { pr_strategy } + + INTERPRETED BY { interp_strategy } + GLOBALIZED BY { glob_strategy } + SUBSTITUTED BY { subst_strategy } + + RAW_PRINTED BY { pr_raw_strategy } + GLOB_PRINTED BY { pr_glob_strategy } + + | [ glob(c) ] -> { StratConstr (c, true) } + | [ "<-" constr(c) ] -> { StratConstr (c, false) } + | [ "subterms" rewstrategy(h) ] -> { StratUnary (Subterms, h) } + | [ "subterm" rewstrategy(h) ] -> { StratUnary (Subterm, h) } + | [ "innermost" rewstrategy(h) ] -> { StratUnary(Innermost, h) } + | [ "outermost" rewstrategy(h) ] -> { StratUnary(Outermost, h) } + | [ "bottomup" rewstrategy(h) ] -> { StratUnary(Bottomup, h) } + | [ "topdown" rewstrategy(h) ] -> { StratUnary(Topdown, h) } + | [ "id" ] -> { StratId } + | [ "fail" ] -> { StratFail } + | [ "refl" ] -> { StratRefl } + | [ "progress" rewstrategy(h) ] -> { StratUnary (Progress, h) } + | [ "try" rewstrategy(h) ] -> { StratUnary (Try, h) } + | [ "any" rewstrategy(h) ] -> { StratUnary (Any, h) } + | [ "repeat" rewstrategy(h) ] -> { StratUnary (Repeat, h) } + | [ rewstrategy(h) ";" rewstrategy(h') ] -> { StratBinary (Compose, h, h') } + | [ "(" rewstrategy(h) ")" ] -> { h } + | [ "choice" rewstrategy(h) rewstrategy(h') ] -> { StratBinary (Choice, h, h') } + | [ "old_hints" preident(h) ] -> { StratHints (true, h) } + | [ "hints" preident(h) ] -> { StratHints (false, h) } + | [ "terms" constr_list(h) ] -> { StratTerms h } + | [ "eval" red_expr(r) ] -> { StratEval r } + | [ "fold" constr(c) ] -> { StratFold c } +END + +(* By default the strategy for "rewrite_db" is top-down *) + +{ + +let db_strat db = StratUnary (Topdown, StratHints (false, db)) +let cl_rewrite_clause_db db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db)) + +} + +TACTIC EXTEND rewrite_strat +| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) } +| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None } +| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db db (Some id) } +| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db db None } +END + +{ + +let clsubstitute o c = + Proofview.Goal.enter begin fun gl -> + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in + let hyps = Tacmach.New.pf_ids_of_hyps gl in + Tacticals.New.tclMAP + (fun cl -> + match cl with + | Some id when is_tac id -> Tacticals.New.tclIDTAC + | _ -> cl_rewrite_clause c o AllOccurrences cl) + (None :: List.map (fun id -> Some id) hyps) + end + +} + +TACTIC EXTEND substitute +| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c } +END + + +(* Compatibility with old Setoids *) + +TACTIC EXTEND setoid_rewrite + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ] + -> { cl_rewrite_clause c o AllOccurrences None } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] -> + { cl_rewrite_clause c o AllOccurrences (Some id) } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] -> + { cl_rewrite_clause c o (occurrences_of occ) None } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] -> + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } + | [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] -> + { cl_rewrite_clause c o (occurrences_of occ) (Some id) } +END + +VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) (Some lemma2) None } + + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) None None } + | [ "Add" "Relation" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation a aeq n None None None } +END + +VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + { declare_relation a aeq n None (Some lemma2) None } + | [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation a aeq n None (Some lemma2) (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) None (Some lemma3) } + | [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation a aeq n None None (Some lemma3) } +END + +{ + +type binders_argtype = local_binder_expr list + +let wit_binders = + (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) + +let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders) + +let () = + let raw_printer _ _ _ l = Pp.pr_non_empty_arg Ppconstr.pr_binders l in + Pptactic.declare_extra_vernac_genarg_pprule wit_binders raw_printer + +open Pcoq + +} + +GRAMMAR EXTEND Gram + GLOBAL: binders; + binders: + [ [ b = Pcoq.Constr.binders -> { b } ] ]; +END + +VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) + "reflexivity" "proved" "by" constr(lemma1) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) None None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None None None } +END + +VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None (Some lemma2) None } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None (Some lemma2) (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "transitivity" "proved" "by" constr(lemma3) "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) None (Some lemma3) } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1) + "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) } + | [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3) + "as" ident(n) ] -> + { declare_relation ~binders:b a aeq n None None (Some lemma3) } +END + +VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF + | [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) [] a aeq t n; + } + | [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" ident(n) ] -> + { let open Vernacinterp in + add_setoid (not (Locality.make_section_locality atts.locality)) binders a aeq t n; + } + | [ "Add" "Morphism" constr(m) ":" ident(n) ] + (* This command may or may not open a goal *) + => { Vernacexpr.VtUnknown, Vernacexpr.VtNow } + -> { let open Vernacinterp in + add_morphism_infer (not (Locality.make_section_locality atts.locality)) m n; + } + | [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" ident(n) ] + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) [] m s n; + } + | [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m) + "with" "signature" lconstr(s) "as" ident(n) ] + => { Vernacexpr.(VtStartProof("Classic",GuaranteesOpacity,[n]), VtLater) } + -> { let open Vernacinterp in + add_morphism (not (Locality.make_section_locality atts.locality)) binders m s n; + } +END + +TACTIC EXTEND setoid_symmetry + | [ "setoid_symmetry" ] -> { setoid_symmetry } + | [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n } +END + +TACTIC EXTEND setoid_reflexivity +| [ "setoid_reflexivity" ] -> { setoid_reflexivity } +END + +TACTIC EXTEND setoid_transitivity +| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) } +| [ "setoid_etransitivity" ] -> { setoid_transitivity None } +END + +VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY +| [ "Print" "Rewrite" "HintDb" preident(s) ] -> + { let sigma, env = Pfedit.get_current_context () in + Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s) } +END diff --git a/plugins/ltac/profile_ltac_tactics.ml4 b/plugins/ltac/profile_ltac_tactics.ml4 deleted file mode 100644 index 983e1578be..0000000000 --- a/plugins/ltac/profile_ltac_tactics.ml4 +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* set_profiling b)) - -let tclRESET_PROFILE = - Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) - -let tclSHOW_PROFILE ~cutoff = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) - -let tclSHOW_PROFILE_TACTIC s = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) - -let tclRESTART_TIMER s = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) - -let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = - Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) - -TACTIC EXTEND start_ltac_profiling -| [ "start" "ltac" "profiling" ] -> [ tclSET_PROFILING true ] -END - -TACTIC EXTEND stop_ltac_profiling -| [ "stop" "ltac" "profiling" ] -> [ tclSET_PROFILING false ] -END - -TACTIC EXTEND reset_ltac_profile -| [ "reset" "ltac" "profile" ] -> [ tclRESET_PROFILE ] -END - -TACTIC EXTEND show_ltac_profile -| [ "show" "ltac" "profile" ] -> [ tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "show" "ltac" "profile" "cutoff" int(n) ] -> [ tclSHOW_PROFILE ~cutoff:(float_of_int n) ] -| [ "show" "ltac" "profile" string(s) ] -> [ tclSHOW_PROFILE_TACTIC s ] -END - -TACTIC EXTEND restart_timer -| [ "restart_timer" string_opt(s) ] -> [ tclRESTART_TIMER s ] -END - -TACTIC EXTEND finish_timing -| [ "finish_timing" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix:"Timer" s ] -| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> [ tclFINISH_TIMING ~prefix s ] -END - -VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF - [ "Reset" "Ltac" "Profile" ] -> [ reset_profile () ] -END - -VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] -| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] -END - -VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY - [ "Show" "Ltac" "Profile" string(s) ] -> [ print_results_tactic s ] -END diff --git a/plugins/ltac/profile_ltac_tactics.mlg b/plugins/ltac/profile_ltac_tactics.mlg new file mode 100644 index 0000000000..2713819c7b --- /dev/null +++ b/plugins/ltac/profile_ltac_tactics.mlg @@ -0,0 +1,82 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* set_profiling b)) + +let tclRESET_PROFILE = + Proofview.tclLIFT (Proofview.NonLogical.make reset_profile) + +let tclSHOW_PROFILE ~cutoff = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results ~cutoff)) + +let tclSHOW_PROFILE_TACTIC s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> print_results_tactic s)) + +let tclRESTART_TIMER s = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> restart_timer s)) + +let tclFINISH_TIMING ?(prefix="Timer") (s : string option) = + Proofview.tclLIFT (Proofview.NonLogical.make (fun () -> finish_timing ~prefix s)) + +} + +TACTIC EXTEND start_ltac_profiling +| [ "start" "ltac" "profiling" ] -> { tclSET_PROFILING true } +END + +TACTIC EXTEND stop_ltac_profiling +| [ "stop" "ltac" "profiling" ] -> { tclSET_PROFILING false } +END + +TACTIC EXTEND reset_ltac_profile +| [ "reset" "ltac" "profile" ] -> { tclRESET_PROFILE } +END + +TACTIC EXTEND show_ltac_profile +| [ "show" "ltac" "profile" ] -> { tclSHOW_PROFILE ~cutoff:!Flags.profile_ltac_cutoff } +| [ "show" "ltac" "profile" "cutoff" int(n) ] -> { tclSHOW_PROFILE ~cutoff:(float_of_int n) } +| [ "show" "ltac" "profile" string(s) ] -> { tclSHOW_PROFILE_TACTIC s } +END + +TACTIC EXTEND restart_timer +| [ "restart_timer" string_opt(s) ] -> { tclRESTART_TIMER s } +END + +TACTIC EXTEND finish_timing +| [ "finish_timing" string_opt(s) ] -> { tclFINISH_TIMING ~prefix:"Timer" s } +| [ "finish_timing" "(" string(prefix) ")" string_opt(s) ] -> { tclFINISH_TIMING ~prefix s } +END + +VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF +| [ "Reset" "Ltac" "Profile" ] -> { reset_profile () } +END + +VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY +| [ "Show" "Ltac" "Profile" ] -> { print_results ~cutoff:!Flags.profile_ltac_cutoff } +| [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> { print_results ~cutoff:(float_of_int n) } +END + +VERNAC COMMAND EXTEND ShowLtacProfileTactic CLASSIFIED AS QUERY +| [ "Show" "Ltac" "Profile" string(s) ] -> { print_results_tactic s } +END -- cgit v1.2.3