Skip to content

Commit

Permalink
clarify API for side effects
Browse files Browse the repository at this point in the history
  • Loading branch information
@gares
gares committed Mar 9, 2023
1 parent d035549 commit 09bc41a
Showing 1 changed file with 46 additions and 36 deletions.
82 changes: 46 additions & 36 deletions src/coq_elpi_builtins.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -109,16 +109,26 @@ let invocation_site_loc = State.declare ~name:"coq-elpi:invocation-site-loc"
~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)")
~start:(fun x -> x)

let on_global_state ?(abstract_exception=false) ?options api thunk = (); (fun state ->
if not abstract_exception && State.get tactic_mode state then
let abstract__grab_global_env_keep_sigma api thunk = (); (fun state ->
let state, result, gls = thunk state in
Coq_elpi_HOAS.grab_global_env state, result, gls)

let grab_global_env__drop_sigma_univs_if_option_is_set options api thunk = (); (fun state ->
if State.get tactic_mode state then
Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
let state, result, gls = thunk state in
match options with
| Some { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
| { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls
| _ -> Coq_elpi_HOAS.grab_global_env state, result, gls)

let grab_global_env api thunk = (); (fun state ->
if State.get tactic_mode state then
Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
let state, result, gls = thunk state in
Coq_elpi_HOAS.grab_global_env state, result, gls)

(* This is for stuff that is not monotonic in the env, eg section closing *)
let on_global_state_does_rewind_env api thunk = (); (fun state ->
let grab_global_env_drop_sigma api thunk = (); (fun state ->
if State.get tactic_mode state then
Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics"));
let state, result, gls = thunk state in
Expand Down Expand Up @@ -1774,7 +1784,7 @@ Supported attributes:
- @udecl! (default unset)
- @dropunivs! (default: false, drops all universe constraints from the store after the definition)
|})))))),
(fun id body types opaque _ ~depth {options} _ -> on_global_state ~options "coq.env.add-const" (fun state ->
(fun id body types opaque _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-const" (fun state ->
let local = options.local = Some true in
let state = minimize_universes state in
(* Maybe: UState.nf_universes on body and type *)
Expand Down Expand Up @@ -1849,7 +1859,7 @@ Supported attributes:
- @using! (default: section variables actually used)
- @inline! (default: no inlining)
- @inline-at! N (default: no inlining)|})))),
(fun id ty _ ~depth {options} _ -> on_global_state "coq.env.add-axiom" (fun state ->
(fun id ty _ ~depth {options} _ -> grab_global_env "coq.env.add-axiom" (fun state ->
let gr = add_axiom_or_variable "coq.env.add-axiom" id ty false options state in
state, !: (global_constant_of_globref gr), []))),
DocAbove);
Expand All @@ -1860,7 +1870,7 @@ Supported attributes:
Out(constant, "C",
Full (global, {|Declare a new section variable: C gets a constant derived from Name
and the current module|})))),
(fun id ty _ ~depth {options} _ -> on_global_state "coq.env.add-section-variable" (fun state ->
(fun id ty _ ~depth {options} _ -> grab_global_env_drop_sigma "coq.env.add-section-variable" (fun state ->
let gr = add_axiom_or_variable "coq.env.add-section-variable" id ty true options state in
state, !: (global_constant_of_globref gr), []))),
DocAbove);
Expand All @@ -1872,7 +1882,7 @@ and the current module|})))),
Supported attributes:
- @dropunivs! (default: false, drops all universe constraints from the store after the definition)
- @primitive! (default: false, makes records primitive)|}))),
(fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth {options} _ -> on_global_state ~options "coq.env.add-indt" (fun state ->
(fun (me, uctx, univ_binders, record_info, ind_impls) _ ~depth {options} _ -> grab_global_env__drop_sigma_univs_if_option_is_set options "coq.env.add-indt" (fun state ->
let sigma = get_sigma state in
if not (is_mutual_inductive_entry_ground me sigma) then
err Pp.(str"coq.env.add-indt: the inductive type declaration must be ground. Did you forge to call coq.typecheck-indt-decl?");
Expand Down Expand Up @@ -1959,7 +1969,7 @@ with a number, starting from 1.
In(option modtypath, "Its module type",
In(list (pair id modtypath), "Parameters of the functor",
Full(unit_ctx, "Starts a functor *E*")))),
(fun name mp binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module-functor" (fun state ->
(fun name mp binders_ast ~depth _ _ -> grab_global_env "coq.env.begin-module-functor" (fun state ->
if Global.sections_are_opened () then
err Pp.(str"This elpi code cannot be run within a section since it opens a module");
let ty =
Expand Down Expand Up @@ -1988,7 +1998,7 @@ coq.env.begin-module Name MP :-
MLCode(Pred("coq.env.end-module",
Out(modpath, "ModPath",
Full(unit_ctx, "end the current module that becomes known as ModPath *E*")),
(fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module" (fun state ->
(fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module" (fun state ->
let mp = Declaremods.end_module () in
state, !: mp, []))),
DocAbove);
Expand All @@ -1998,7 +2008,7 @@ coq.env.begin-module Name MP :-
In(id, "The name of the functor",
In(list (pair id modtypath), "The parameters of the functor",
Full(unit_ctx,"Starts a module type functor *E*"))),
(fun id binders_ast ~depth _ _ -> on_global_state "coq.env.begin-module-type-functor" (fun state ->
(fun id binders_ast ~depth _ _ -> grab_global_env "coq.env.begin-module-type-functor" (fun state ->
if Global.sections_are_opened () then
err Pp.(str"This elpi code cannot be run within a section since it opens a module");
let id = Id.of_string id in
Expand All @@ -2023,7 +2033,7 @@ coq.env.begin-module-type Name :-
MLCode(Pred("coq.env.end-module-type",
Out(modtypath, "ModTyPath",
Full(unit_ctx, "end the current module type that becomes known as ModPath *E*")),
(fun _ ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-module-type" (fun state ->
(fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module-type" (fun state ->
let mp = Declaremods.end_modtype () in
state, !: mp, []))),
DocAbove);
Expand All @@ -2036,7 +2046,7 @@ coq.env.begin-module-type Name :-
In(module_inline_default, "Arguments inlining",
Out(modpath, "The modpath of the new module",
Full(unit_ctx, "Applies a functor *E*"))))))),
(fun name mp f arguments inline _ ~depth _ _ -> on_global_state "coq.env.apply-module-functor" (fun state ->
(fun name mp f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-functor" (fun state ->
if Global.sections_are_opened () then
err Pp.(str"This elpi code cannot be run within a section since it defines a module");
let ty =
Expand All @@ -2061,7 +2071,7 @@ coq.env.begin-module-type Name :-
In(module_inline_default, "Arguments inlining",
Out(modtypath, "The modtypath of the new module type",
Full(unit_ctx, "Applies a type functor *E*")))))),
(fun name f arguments inline _ ~depth _ _ -> on_global_state "coq.env.apply-module-type-functor" (fun state ->
(fun name f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-type-functor" (fun state ->
if Global.sections_are_opened () then
err Pp.(str"This elpi code cannot be run within a section since it defines a module");
let id = Id.of_string name in
Expand All @@ -2080,7 +2090,7 @@ coq.env.begin-module-type Name :-
In(modpath, "ModPath",
In(module_inline_default, "Inline",
Full(unit_ctx, "is like the vernacular Include, Inline can be omitted *E*"))),
(fun mp inline ~depth _ _ -> on_global_state "coq.env.include-module" (fun state ->
(fun mp inline ~depth _ _ -> grab_global_env "coq.env.include-module" (fun state ->
let fpath = match mp with
| ModPath.MPdot(mp,l) ->
Libnames.make_path (ModPath.dp mp) (Label.to_id l)
Expand All @@ -2096,7 +2106,7 @@ coq.env.begin-module-type Name :-
In(modtypath, "ModTyPath",
In(module_inline_default, "Inline",
Full(unit_ctx, "is like the vernacular Include Type, Inline can be omitted *E*"))),
(fun mp inline ~depth _ _ -> on_global_state "coq.env.include-module-type" (fun state ->
(fun mp inline ~depth _ _ -> grab_global_env "coq.env.include-module-type" (fun state ->
let fpath = Nametab.path_of_modtype mp in
let tname = Constrexpr.CMident (Libnames.qualid_of_path fpath) in
let i = CAst.make tname, inline in
Expand All @@ -2107,15 +2117,15 @@ coq.env.begin-module-type Name :-
MLCode(Pred("coq.env.import-module",
In(modpath, "ModPath",
Full(unit_ctx, "is like the vernacular Import *E*")),
(fun mp ~depth _ _ -> on_global_state "coq.env.import-module" (fun state ->
(fun mp ~depth _ _ -> grab_global_env "coq.env.import-module" (fun state ->
Declaremods.import_module ~export:Lib.Import Libobject.unfiltered mp;
state, (), []))),
DocAbove);

MLCode(Pred("coq.env.export-module",
In(modpath, "ModPath",
Full(unit_ctx, "is like the vernacular Export *E*")),
(fun mp ~depth _ _ -> on_global_state "coq.env.export-module" (fun state ->
(fun mp ~depth _ _ -> grab_global_env "coq.env.export-module" (fun state ->
Declaremods.import_module ~export:Lib.Export Libobject.unfiltered mp;
state, (), []))),
DocAbove);
Expand All @@ -2139,7 +2149,7 @@ denote the same x as before.|};
MLCode(Pred("coq.env.begin-section",
In(id, "Name",
Full(unit_ctx, "starts a section named Name *E*")),
(fun id ~depth _ _ -> on_global_state "coq.env.begin-section" (fun state ->
(fun id ~depth _ _ -> grab_global_env "coq.env.begin-section" (fun state ->
let id = Id.of_string id in
let lid = CAst.make ~loc:(to_coq_loc @@ State.get invocation_site_loc state) id in
Dumpglob.dump_definition lid true "sec";
Expand All @@ -2149,7 +2159,7 @@ denote the same x as before.|};

MLCode(Pred("coq.env.end-section",
Full(unit_ctx, "end the current section *E*"),
(fun ~depth _ _ -> on_global_state_does_rewind_env "coq.env.end-section" (fun state ->
(fun ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-section" (fun state ->
let loc = to_coq_loc @@ State.get invocation_site_loc state in
Dumpglob.dump_reference ~loc
(DirPath.to_string (Lib.current_dirpath true)) "<>" "sec";
Expand Down Expand Up @@ -2500,7 +2510,7 @@ declared as cumulative.|};
Full(global, {|Declares GR as a canonical structure instance.
Supported attributes:
- @local! (default: false)|})),
(fun gr ~depth { options } _ -> on_global_state "coq.CS.declare-instance" (fun state ->
(fun gr ~depth { options } _ -> grab_global_env "coq.CS.declare-instance" (fun state ->
Canonical.declare_canonical_structure ?local:options.local gr;
state, (), []))),
DocAbove);
Expand Down Expand Up @@ -2538,7 +2548,7 @@ Supported attributes:
MLCode(Pred("coq.TC.declare-class",
In(gref, "GR",
Full(global, {|Declare GR as a type class|})),
(fun gr ~depth { options } _ -> on_global_state "coq.TC.declare-class" (fun state ->
(fun gr ~depth { options } _ -> grab_global_env "coq.TC.declare-class" (fun state ->
Record.declare_existing_class gr;
state, (), []))),
DocAbove);
Expand All @@ -2551,7 +2561,7 @@ Supported attributes:
Full(global, {|Declare GR as a Global type class instance with Priority.
Supported attributes:
- @global! (default: true)|}))),
(fun gr priority ~depth { options } _ -> on_global_state "coq.TC.declare-instance" (fun state ->
(fun gr priority ~depth { options } _ -> grab_global_env "coq.TC.declare-instance" (fun state ->
let global = if options.local = Some false then Hints.SuperGlobal else Hints.Local in
let hint_priority = Some priority in
let qualid =
Expand Down Expand Up @@ -2596,7 +2606,7 @@ NParams can always be omitted, since it is inferred.
- @global! (default: false)
- @nonuniform! (default: false)
- @reversible! (default: false)|})),
(fun (gr, _, source, target) ~depth { options } _ -> on_global_state "coq.coercion.declare" (fun state ->
(fun (gr, _, source, target) ~depth { options } _ -> grab_global_env "coq.coercion.declare" (fun state ->
let local = options.local <> Some false in
let poly = false in
let nonuniform = options.nonuniform = Some true in
Expand Down Expand Up @@ -2668,7 +2678,7 @@ This old behavior is available via the @global! flag, but is discouraged.
In(B.list mode, "Mode",
Full(global, {|Adds a mode declaration to DB about GR.
Supported attributes:|} ^ hint_locality_doc)))),
(fun gr (db,_) mode ~depth:_ {options} _ -> on_global_state "coq.hints.add-mode" (fun state ->
(fun gr (db,_) mode ~depth:_ {options} _ -> grab_global_env "coq.hints.add-mode" (fun state ->
let locality = hint_locality options in
Hints.add_hints ~locality [db] (Hints.HintsModeEntry(gr,mode));
state, (), []
Expand All @@ -2695,7 +2705,7 @@ Supported attributes:|} ^ hint_locality_doc)))),
In(B.bool, "Opaque",
Full(global,{|Like Hint Opaque C : DB (or Hint Transparent, if the boolean is ff).
Supported attributes:|} ^ hint_locality_doc)))),
(fun c (db,_) opaque ~depth:_ {options} _ -> on_global_state "coq.hints.set-opaque" (fun state ->
(fun c (db,_) opaque ~depth:_ {options} _ -> grab_global_env "coq.hints.set-opaque" (fun state ->
let locality = hint_locality options in
let transparent = not opaque in
let r = match c with
Expand Down Expand Up @@ -2725,7 +2735,7 @@ Supported attributes:|} ^ hint_locality_doc)))),
CIn(B.unspecC closed_term, "Pattern",
Full(global,{|Like Hint Resolve GR | Priority Pattern : DB.
Supported attributes:|} ^ hint_locality_doc))))),
(fun gr (db,_) priority pattern ~depth:_ {env;options} _ -> on_global_state "coq.hints.add-resolve" (fun state ->
(fun gr (db,_) priority pattern ~depth:_ {env;options} _ -> grab_global_env "coq.hints.add-resolve" (fun state ->
let locality = hint_locality options in
let hint_priority = unspec2opt priority in
let sigma = get_sigma state in
Expand Down Expand Up @@ -2761,7 +2771,7 @@ Unspecified means explicit.
See also the [] and {} flags for the Arguments command.
Supported attributes:
- @global! (default: false)|}))),
(fun gref imps ~depth {options} _ -> on_global_state "coq.arguments.set-implicit" (fun state ->
(fun gref imps ~depth {options} _ -> grab_global_env "coq.arguments.set-implicit" (fun state ->
let local = options.local <> Some false in
let imps = imps |> List.(map (map (function
| B.Unspec -> Anonymous, Glob_term.Explicit
Expand All @@ -2777,7 +2787,7 @@ Supported attributes:
See also the "default implicits" flag to the Arguments command.
Supported attributes:
- @global! (default: false)|})),
(fun gref ~depth { options } _ -> on_global_state "coq.arguments.set-default-implicit" (fun state ->
(fun gref ~depth { options } _ -> grab_global_env "coq.arguments.set-default-implicit" (fun state ->
let local = options.local <> Some false in
Impargs.declare_implicits local gref;
state, (), []))),
Expand All @@ -2802,7 +2812,7 @@ Supported attributes:
See also the :rename flag to the Arguments command.
Supported attributes:
- @global! (default: false)|}))),
(fun gref names ~depth { options } _ -> on_global_state "coq.arguments.set-name" (fun state ->
(fun gref names ~depth { options } _ -> grab_global_env "coq.arguments.set-name" (fun state ->
let local = options.local <> Some false in
let names = names |> List.map (function
| None -> Names.Name.Anonymous
Expand All @@ -2827,7 +2837,7 @@ Scope can be a scope name or its delimiter.
See also the %scope modifier for the Arguments command.
Supported attributes:
- @global! (default: false)|}))),
(fun gref scopes ~depth { options } _ -> on_global_state "coq.arguments.set-scope" (fun state ->
(fun gref scopes ~depth { options } _ -> grab_global_env "coq.arguments.set-scope" (fun state ->
let local = options.local <> Some false in
let scopes = scopes |> List.map (List.map (fun k ->
try ignore (CNotation.find_scope k); k
Expand Down Expand Up @@ -2855,7 +2865,7 @@ Positions are 0 based.
See also the ! and / modifiers for the Arguments command.
Supported attributes:
- @global! (default: false)|}))),
(fun gref strategy ~depth { options } _ -> on_global_state "coq.arguments.set-simplification" (fun state ->
(fun gref strategy ~depth { options } _ -> grab_global_env "coq.arguments.set-simplification" (fun state ->
let local = options.local <> Some false in
Reductionops.ReductionBehaviour.set ~local gref strategy;
state, (), []))),
Expand Down Expand Up @@ -2886,7 +2896,7 @@ The term must begin with at least Nargs "fun" nodes whose domain is ignored, eg
Supported attributes:
- @deprecated! (default: not deprecated)
- @global! (default: false)|})))))),
(fun name nargs term onlyparsing _ ~depth { env; options } _ -> on_global_state "coq.notation.add-abbreviation" (fun state ->
(fun name nargs term onlyparsing _ ~depth { env; options } _ -> grab_global_env "coq.notation.add-abbreviation" (fun state ->
let sigma = get_sigma state in
let strip_n_lambas nargs env term =
let rec aux vars nenv env n t =
Expand Down Expand Up @@ -3006,7 +3016,7 @@ at which the term is written (unlike if a regular abbreviation was
declared by hand).
A call to coq.notation.add-abbreviation-for-tactic TacName TacName []
is equivalent to Elpi Export TacName.|})))),
(fun name tacname more_args ~depth { options} _ -> on_global_state "coq.notation.add-abbreviation-for-tactic" (fun state ->
(fun name tacname more_args ~depth { options} _ -> grab_global_env "coq.notation.add-abbreviation-for-tactic" (fun state ->
let sigma = get_sigma state in
let env = get_global_env state in
let tac_fixed_args = more_args |> List.map (function
Expand Down Expand Up @@ -3361,7 +3371,7 @@ coq.reduction.lazy.whd_all X Y :-
In(B.list constant, "CL",
In(conversion_strategy, "Level",
Full(global,"Sets the unfolding priority for all the constants in the list CL. See the command Strategy."))),
(fun csts level ~depth:_ ctx _ -> on_global_state "coq.strategy.set" (fun state ->
(fun csts level ~depth:_ ctx _ -> grab_global_env "coq.strategy.set" (fun state ->
let local = ctx.options.local = Some true in
let csts = csts |> List.map (function
| Constant c -> Tacred.EvalConstRef c
Expand Down Expand Up @@ -3451,7 +3461,7 @@ fold_left over the terms, letin body comes before the type).
CIn(goal, "G",
Out(list sealed_goal,"GL",
Full(raw_ctx, "Calls Ltac1 tactic named Tac on goal G (passing the arguments of G, see coq.ltac.call for a handy wrapper)")))),
(fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> on_global_state ~abstract_exception:true "coq.ltac.call-ltac1" (fun state ->
(fun tac_name (proof_context,goal,tac_args) _ ~depth _ _ -> abstract__grab_global_env_keep_sigma "coq.ltac.call-ltac1" (fun state ->
let open Ltac_plugin in
let sigma = get_sigma state in
let tac_args = tac_args |> List.map (function
Expand Down

0 comments on commit 09bc41a

Please sign in to comment.