attribute @using! (fix #210)

Author: gares

Changelog.md

@@ -4,7 +4,9 @@
 
 Requires Elpi 1.13 and Coq 8.13.
 
-- Fix `elpi.loc` computation when run in interactive mode
+### API
+- Fix `elpi.loc` computation when run in interactive mode.
+- New `@using! S` attribute for `coq.env.add-const` akin to Coq's `#[using=S]`.
 
 ## [1.9.1] - 11-02-2021
 

coq-builtin.elpi

@@ -302,6 +302,8 @@ macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
 
+macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
+
 % both arguments are strings eg "8.12.0" "use foo instead"
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).
@@ -568,6 +570,7 @@ external pred coq.env.current-path o:list string.
 % instead.
 % Supported attributes:
 % - @local! (default: false)
+% - @using! (default: section variables actually used)
 external pred coq.env.add-const i:id, i:term, i:term, i:opaque?, 
                                 o:constant.
 

elpi/coq-HOAS.elpi

@@ -287,6 +287,8 @@ macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
 
+macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
+
 % both arguments are strings eg "8.12.0" "use foo instead"
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).

src/coq_elpi_HOAS.ml

@@ -82,6 +82,7 @@ type options = {
   failsafe : bool; (* don't fail, e.g. we are trying to print a term *)
   ppwidth : int;
   pp : ppoption;
+  using : string option;
 }
 
 let default_options = {
@@ -92,6 +93,7 @@ let default_options = {
   failsafe = false;
   ppwidth = 80;
   pp = Normal;
+  using = None;
 }
 
 type 'a coq_context = {
@@ -645,6 +647,7 @@ let get_options ~depth hyps state =
     failsafe = false;
     ppwidth = ppwidth @@ get_int_option "coq:ppwidth";
     pp = pp @@ get_string_option "coq:pp";
+    using = get_string_option "coq:using";
   }
 
 let mk_coq_context ~options state =

src/coq_elpi_HOAS.mli

@@ -24,6 +24,7 @@ type options = {
   failsafe : bool; (* readback is resilient to illformed terms *)
   ppwidth : int;
   pp : ppoption;
+  using : string option;
 }
 
 type 'a coq_context = {

src/coq_elpi_builtins.ml

@@ -1178,7 +1178,8 @@ if a section is open and @local! is used). Omitting the body and the type is
 an error. Note: using this API for declaring an axiom or a section variable is
 deprecated, use coq.env.add-axiom or coq.env.add-section-variable instead.
 Supported attributes:
-- @local! (default: false)|})))))),
+- @local! (default: false)
+- @using! (default: section variables actually used)|})))))),
   (fun id body types opaque _ ~depth {options} _ -> on_global_state "coq.env.add-const" (fun state ->
     let local = options.local = Some true in
     let sigma = get_sigma state in
@@ -1207,7 +1208,12 @@ Supported attributes:
        let scope = if local
          then Locality.Discharge
          else Locality.(Global ImportDefaultBehavior) in
-       let cinfo = Declare.CInfo.make ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
+       let using = Option.map  Proof_using.(fun s ->
+         let types = Option.List.cons types [] in
+         let expr = using_from_string s in
+         let names = process_expr (get_global_env state) sigma expr types in
+         List.fold_right Names.Id.Set.add names Names.Id.Set.empty) options.using in
+       let cinfo = Declare.CInfo.make ?using ~name:(Id.of_string id) ~typ:types ~impargs:[] () in
        let info = Declare.Info.make ~scope ~kind ~poly:false ~udecl () in
        let gr = Declare.declare_definition ~cinfo ~info ~opaque:(opaque = Given true) ~body sigma in
        state, !: (global_constant_of_globref gr), []))),

src/coq_elpi_builtins_HOAS.ml

@@ -289,6 +289,8 @@ macro @ppwidth! N :- get-option "coq:ppwidth" N. % printing width
 macro @ppall! :- get-option "coq:pp" "all". % printing all
 macro @ppmost! :- get-option "coq:pp" "most". % printing most of contents
 
+macro @using! S :- get-option "coq:using" S. % like the #[using=S] attribute
+
 % both arguments are strings eg "8.12.0" "use foo instead"
 macro @deprecated! Since Msg :-
   get-option "coq:deprecated" (pr Since Msg).

tests/test_API.v

@@ -774,3 +774,12 @@ main _ :- std.do! [
 }}.
 Elpi Typecheck.
 Elpi test.pp.
+
+(************* using ********************)
+Section Using.
+Variable A : bool.
+Elpi Query lp:{{ coq.env.add-const "foo" {{ 3 }} {{ nat }} @transparent! _ }}.
+Elpi Query lp:{{ @using! "All" => coq.env.add-const "bar" {{ 3 }} {{ nat }} @transparent! _ }}.
+End Using.
+Check foo : nat.
+Check bar : bool -> nat.