Merge pull request #226 from LPCIC/db-clause-survive-section

accumulated clauses can survive section if they don't mention variables

Changelog.md

@@ -2,6 +2,14 @@
 
 ## UNRELEASED
 
+
+### Vernacular
+- Commands, Tactics and Db cannot be declared inside sections or modules
+  (it never really worked, but now you get an error message).
+- Clauses which are accumulated via `coq.elpi.accumulate` and are not `@local!`
+  survive section closing if they don't mention the section variables being
+  discharged.
+
 ### Typechecker
 - Warnings can be turned into errors by passing Coq `-w +elpi.typecheck`.
 

coq-builtin.elpi

@@ -418,8 +418,8 @@ external type coq.say variadic any prop.
 external type coq.warn variadic any prop.
 
 % [coq.warning Category Name ...] 
-% Prints a warning message with a Name an Category which can be used
-% to silence this warning or turn it into an error. See coqc -w connad
+% Prints a warning message with a Name and Category which can be used
+% to silence this warning or turn it into an error. See coqc -w commad
 % line option
 external type coq.warning string -> string -> variadic any prop.
 
@@ -1032,9 +1032,13 @@ type current scope. % The module being defined (see begin/end-module)
 % to
 % the given db (see Elpi Db). Clauses belong to Coq modules: the Scope
 % argument
-% lets one select which module (default is execution-site). 
+% lets one select which module (default is execution-site).
+% A clause that mentions a section variable is automatically discarded at
+% the
+% end of the section.
+% Clauses cannot be accumulated inside functors.
 % Supported attributes:
-% - @local! (default: false)
+% - @local! (default: false, discard at the end of section or module)
 external pred coq.elpi.accumulate i:scope, i:id, i:clause.
 
 % -- Utils ------------------------------------------------------------

src/coq_elpi_HOAS.ml

@@ -206,8 +206,8 @@ let global_constant_of_globref = function
   | GlobRef.ConstRef x -> Constant x
   | x -> CErrors.anomaly Pp.(str"not a global constant: " ++ (Printer.pr_global x))
 
-let constant, inductive, constructor =
-  let open API.OpaqueData in
+let ({ CD.isc = isconstant; cout = constantout },constant), (_,inductive), (_,constructor) =
+  let open API.RawOpaqueData in
   declare {
     name = "constant";
     doc = "Global constant name";
@@ -241,6 +241,19 @@ let constant, inductive, constructor =
   }
 ;;
 
+let collect_term_variables ~depth t =
+  let rec aux ~depth acc t =
+    match E.look ~depth t with
+    | E.CData c when isconstant c ->
+        begin match constantout c with
+        | Variable id -> id :: acc
+        | _ -> acc
+        end
+    | x -> fold_elpi_term aux acc ~depth x
+  in
+  aux ~depth [] t
+
+
 let gref =
   let open GlobRef in
   let open API.AlgebraicData in declare {

src/coq_elpi_HOAS.mli

@@ -146,6 +146,7 @@ val universe : Sorts.t Conversion.t
 val global_constant_of_globref : Names.GlobRef.t -> global_constant
 val abbreviation : Globnames.syndef_name Conversion.t
 val implicit_kind : Glob_term.binding_kind Conversion.t
+val collect_term_variables : depth:int -> term -> Names.Id.t list
 
 module GRMap : Elpi.API.Utils.Map.S with type key = Names.GlobRef.t
 module GRSet : Elpi.API.Utils.Set.S with type elt = Names.GlobRef.t

src/coq_elpi_builtins.ml

@@ -111,15 +111,6 @@ let on_global_state_does_rewind_env api thunk = (); (fun state ->
   Coq_elpi_HOAS.grab_global_env_drop_univs state, result, gls)
 
 let warn_if_contains_univ_levels ~depth t =
-  let fold f acc ~depth t =
-    match t with
-    | E.Const _ | E.Nil | E.CData _ -> acc
-    | E.App(_,x,xs) -> List.fold_left (f ~depth) (f ~depth acc x) xs
-    | E.Cons(x,xs) -> f ~depth (f ~depth acc x) xs
-    | E.Builtin(_,xs) -> List.fold_left (f ~depth) acc xs
-    | E.Lam x -> f ~depth:(depth+1) acc x
-    | E.UnifVar(_,xs) -> List.fold_left (f ~depth) acc xs
-  in
   let global_univs = UGraph.domain (Environ.universes (Global.env ())) in
   let is_global u =
     match Univ.Universe.level u with
@@ -128,7 +119,7 @@ let warn_if_contains_univ_levels ~depth t =
   let rec aux ~depth acc t =
     match E.look ~depth t with
     | E.CData c when isuniv c -> let u = univout c in if is_global u then acc else u :: acc
-    | x -> fold aux acc ~depth x
+    | x -> Coq_elpi_utils.fold_elpi_term aux acc ~depth x
   in
   let univs = aux ~depth [] t in
   if univs <> [] then
@@ -224,7 +215,7 @@ let clauses_for_later =
     ~init:(fun () -> [])
     ~start:(fun x -> x)
     ~pp:(fun fmt l ->
-       List.iter (fun (dbname, code,local) ->
+       List.iter (fun (dbname, code,vars,local) ->
          Format.fprintf fmt "db:%s code:%a local:%b\n"
               (String.concat "." dbname)
             Elpi.API.Pp.Ast.program code local) l)
@@ -503,7 +494,7 @@ The name and the grafting specification can be left unspecified.|};
 } |> CConv.(!<)
 
 let set_accumulate_to_db, get_accumulate_to_db =
-  let f = ref (fun _ _ ~local:_ -> assert false) in
+  let f = ref (fun _ _ _ ~local:_ -> assert false) in
   (fun x -> f := x),
   (fun () -> !f)
 
@@ -2345,22 +2336,26 @@ Supported attributes:
     Full (global, {|
 Declare that, once the program is over, the given clause has to be added to
 the given db (see Elpi Db). Clauses belong to Coq modules: the Scope argument
-lets one select which module (default is execution-site). 
+lets one select which module (default is execution-site).
+A clause that mentions a section variable is automatically discarded at the
+end of the section.
+Clauses cannot be accumulated inside functors.
 Supported attributes:
-- @local! (default: false)|} )))),
+- @local! (default: false, discard at the end of section or module)|} )))),
   (fun scope dbname (name,graft,clause) ~depth ctx _ state ->
      let loc = API.Ast.Loc.initial "(elpi.add_clause)" in
      let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in
      warn_if_contains_univ_levels ~depth clause;
+     let vars = collect_term_variables ~depth clause in
      let clause = API.Utils.clause_of_term ?name ?graft ~depth loc clause in
      let local = ctx.options.local = Some true in
      match scope with
      | Unspec | Given ExecutionSite ->
          State.update clauses_for_later state (fun l ->
-           (dbname,clause,local) :: l), (), []
+           (dbname,clause,vars,local) :: l), (), []
      | Given CurrentModule ->
           let f = get_accumulate_to_db () in
-          f dbname clause ~local;
+          f dbname clause vars ~local;
           state, (), []
      )),
   DocAbove);

src/coq_elpi_builtins.mli

@@ -9,8 +9,8 @@ val coq_builtins : BuiltIn.declaration list
 (* Clauses to be added to elpi programs when the execution is over *)
 
 val clauses_for_later :
-  (string list * Ast.program * bool) list State.component
-val set_accumulate_to_db : ((string list -> Ast.program -> local:bool -> unit)) -> unit
+  (string list * Ast.program * Names.Id.t list * bool) list State.component
+val set_accumulate_to_db : ((string list -> Ast.program -> Names.Id.t list -> local:bool -> unit)) -> unit
 
 val attribute : (string * Attributes.vernac_flag_value) Conversion.t
 

src/coq_elpi_utils.ml

@@ -130,4 +130,15 @@ let float64 : Float64.t Elpi.API.Conversion.t =
     hash = Float64.hash;
     hconsed = false;
     constants = [];
-  }
+  }
+
+let fold_elpi_term f acc ~depth t =
+  let module E = Elpi.API.RawData in
+  match t with
+  | E.Const _ | E.Nil | E.CData _ -> acc
+  | E.App(_,x,xs) -> List.fold_left (f ~depth) (f ~depth acc x) xs
+  | E.Cons(x,xs) -> f ~depth (f ~depth acc x) xs
+  | E.Builtin(_,xs) -> List.fold_left (f ~depth) acc xs
+  | E.Lam x -> f ~depth:(depth+1) acc x
+  | E.UnifVar(_,xs) -> List.fold_left (f ~depth) acc xs
+

src/coq_elpi_utils.mli

@@ -21,5 +21,9 @@ val manual_implicit_of_binding_kind : Names.Name.t -> Glob_term.binding_kind ->
 val manual_implicit_of_gdecl : Glob_term.glob_decl -> (Names.Name.t * bool) option CAst.t
 val lookup_inductive : Environ.env -> Names.inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body
 
+val fold_elpi_term :
+  (depth:int -> 'a -> Elpi.API.Data.term -> 'a) ->
+    'a -> depth:int -> Elpi.API.RawData.view -> 'a
+
 val uint63 : Uint63.t Elpi.API.Conversion.t
-val float64 : Float64.t Elpi.API.Conversion.t
+val float64 : Float64.t Elpi.API.Conversion.t

src/coq_elpi_vernacular.ml

@@ -326,7 +326,7 @@ and src_string = {
   val set_current_program : qualified_name -> unit
   val current_program : unit -> qualified_name
   val accumulate : qualified_name -> src list -> unit
-  val accumulate_to_db : qualified_name -> Compile.compilation_unit -> local:bool -> unit
+  val accumulate_to_db : qualified_name -> Compile.compilation_unit -> Names.Id.t list -> local:bool -> unit
 
   val load_checker : string -> unit
   val load_printer : string -> unit
@@ -481,23 +481,31 @@ type snippet = {
   program : qualified_name;
   code : EC.compilation_unit;
   local : bool;
+  vars : Names.Id.t list;
 }
 
 let in_db : snippet -> Libobject.obj =
   let cache ((_,kname), { program = name; code = p; _ }) =
     db_name_src := SLMap.add name (append_to_db name (kname,p)) !db_name_src in
   let import i o = if Int.equal i 1 then cache o in
   Libobject.declare_object @@ { (Libobject.default_object "ELPI-DB") with
-    Libobject.classify_function = (fun ({ local; _ } as o) ->
-       if local then Libobject.Dispose else Libobject.Keep o);
+    Libobject.classify_function = (fun ({ local; program; _ } as o) ->
+      if local then Libobject.Dispose else Libobject.Keep o);
     Libobject.cache_function  = cache;
-    Libobject.subst_function = (fun _ -> CErrors.user_err Pp.(str"elpi: No functors yet"));
+    Libobject.subst_function = (fun _ ->
+      CErrors.user_err Pp.(str"elpi: Accumulating clauses in a functor is not supported yet"));
     Libobject.open_function = Libobject.simple_open import;
+    Libobject.discharge_function = (fun (_,({ local; program; vars; } as o)) ->
+      if local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None
+      else Some o);
+
 }
 
 let accum = ref 0
-let add_to_db program code local =
-  ignore @@ Lib.add_leaf (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum)) (in_db { program; code; local })
+let add_to_db program code vars local =
+  ignore @@ Lib.add_leaf 
+    (Names.Id.of_string (incr accum; Printf.sprintf "_ELPI_%d" !accum))
+    (in_db { program; code; local; vars })
 
 let lp_command_ast = Summary.ref ~name:"elpi-lp-command" None
 let in_lp_command_src : src -> Libobject.obj =
@@ -538,15 +546,21 @@ let tactic_init () =
 let create_program (loc,qualid) init =
   if program_exists qualid || db_exists qualid then
     CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists")
+  else if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections")
   else
     add_to_program qualid [init]
 
 let create_db (loc,qualid) init =
   if program_exists qualid || db_exists qualid then
     CErrors.user_err Pp.(str "Program/Tactic/Db " ++ pr_qualified_name qualid ++ str " already exists")
+  else if Global.sections_are_opened () then
+    CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside sections")
+  else if match Global.current_modpath () with Names.ModPath.MPdot (Names.ModPath.MPfile _,_) -> true | _ -> false then
+    CErrors.user_err Pp.(str "Program/Tactic/Db cannot be declared inside modules")
   else
     match ast_of_src init with
-    | [`Static,base] -> add_to_db qualid base false
+    | [`Static,base] -> add_to_db qualid base [] false
     | _ -> assert false
 ;;
 
@@ -605,10 +619,10 @@ let accumulate p v =
     CErrors.user_err Pp.(str "No Elpi Program named " ++ pr_qualified_name p);
   add_to_program p v
 
-let accumulate_to_db p v ~local =
+let accumulate_to_db p v vs ~local =
   if not (db_exists p) then
     CErrors.user_err Pp.(str "No Elpi Db " ++ pr_qualified_name p);
-  add_to_db p v local
+  add_to_db p v vs local
 
 end
 
@@ -670,14 +684,14 @@ let compile name baseul extra =
     (Summary.Local.(:=) compiler_cache (SLMap.add name (baseul,program) (Summary.Local.(!) compiler_cache)));
     extend_w_units ~base:program extra
 
-let () = Coq_elpi_builtins.set_accumulate_to_db (fun n x ~local ->
+let () = Coq_elpi_builtins.set_accumulate_to_db (fun n x vs ~local ->
   let elpi = ensure_initialized () in
   let u =
     try EC.unit ~elpi ~flags:(cc_flags ()) x
     with EC.CompileError(oloc, msg) ->
       let loc = Option.map Coq_elpi_utils.to_coq_loc oloc in
       CErrors.user_err ?loc ~hdr:"elpi" (Pp.str msg) in
-  Programs.accumulate_to_db n u ~local)
+  Programs.accumulate_to_db n u vs ~local)
 
 let get_and_compile name =
   let core_units, extra_units = get name in
@@ -745,9 +759,9 @@ let run_and_print ~tactic_mode ~print ~static_check program_ast query_ast =
       API.State.get Coq_elpi_builtins.clauses_for_later
         state in
     let elpi = ensure_initialized () in
-    List.iter (fun (dbname,ast,local) ->
+    List.iter (fun (dbname,ast,vs,local) ->
       let unit = EC.unit ~elpi ~flags:(cc_flags()) ast in
-      accumulate_to_db dbname unit ~local) clauses_to_add
+      accumulate_to_db dbname unit vs ~local) clauses_to_add
 ;;
 
 let run_in_program ?(program = current_program ()) (loc, query) =
@@ -902,7 +916,7 @@ let accumulate_string ?(program=current_program()) (loc,s) =
   let elpi = ensure_initialized () in
   let new_ast = unit_from_string ~elpi loc s in
   if db_exists program then
-    accumulate_to_db program new_ast ~local:false
+    accumulate_to_db program new_ast [] ~local:false
   else
     accumulate program [EmbeddedString { sloc = loc; sdata = s; sast = new_ast}]
 ;;

src/coq_elpi_vernacular.mli

@@ -18,7 +18,7 @@ val accumulate_files  : ?program:qualified_name -> string list -> unit
 val accumulate_string : ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> unit
 val accumulate_db     : ?program:qualified_name -> qualified_name -> unit
 
-val accumulate_to_db  : qualified_name -> Elpi.API.Ast.Loc.t * string -> local:bool -> unit
+val accumulate_to_db  : qualified_name -> Elpi.API.Ast.Loc.t * string -> Names.Id.t list -> local:bool -> unit
 
 
 (* Setup *)

tests/test_API.v

@@ -329,9 +329,6 @@ End II.
 
 (* inductive *)
 
-Section Dummy.
-Variable dummy : nat.
-
 Elpi Command indtest.
 Elpi Accumulate lp:{{
 main _ :-
@@ -359,8 +356,6 @@ Check K2 true : myind true true.
 Check myind1 true false : Prop.
 Check K21 true : myind1 true true.
 
-End Dummy.
-
 Elpi Query lp:{{
   coq.env.add-indt (parameter "X" _ {{Type}} x\
                       inductive "nuind" _ (parameter "n" _ {{ nat }} _\ arity {{ bool -> Type }}) i\
@@ -757,6 +752,39 @@ Fail Elpi Query lp:{{foo "there"}}.
 Import test_db_accumulate.
 Elpi Query lp:{{foo "there"}}.
 
+(********* accumulate *************** *)
+
+Elpi Db test2.db lp:{{
+    type foo gref -> prop.
+}}.
+Elpi Command test2.use.db.
+Elpi Accumulate Db test2.db.
+Elpi Accumulate lp:{{
+  main [str S] :- coq.locate S GR, coq.elpi.accumulate _ "test2.db" (clause _ _ (foo GR)).
+  main [str "local", str S] :- coq.locate S GR, @local! => coq.elpi.accumulate _ "test2.db" (clause _ _ (foo GR)).
+  main [int N] :- std.findall (foo X_) L, coq.say L, std.length L N.
+}}.
+
+Module T2.
+Section T2.
+Variable X : nat.
+Elpi test2.use.db X.
+Elpi test2.use.db nat.
+Elpi test2.use.db "local" bool.
+Elpi test2.use.db 3.
+End T2.
+Elpi test2.use.db "local" bool.
+Elpi test2.use.db 2.
+End T2.
+Elpi test2.use.db 0.
+Import T2.
+Elpi test2.use.db 1.
+
+
+Section T3. Fail Elpi Db test3.db lp:{{ }}. End T3.
+Module T3. Fail Elpi Db test3.db lp:{{ }}. End T3.
+
+(********* export *************** *)
 
 Elpi Command export.me.
 Elpi Accumulate lp:{{ main _ :- coq.say "hello". }}.