Elpi Accumulate Plugin

gares · gares · commit 6666c316fab0 · 2026-03-04T15:46:07.000+01:00
diff --git a/README.md b/README.md
@@ -148,6 +148,8 @@ and `ocaml-lsp-server` (version 1.15).
 - [open terms](examples/example_open_terms.v) implements
   a tactic like `replace` that receives terms containing free variables, i.e.
   variables bound in the goal but not in the proof context.
+- [builtins](examples/example_plugin/) adds builtin predicates
+  (hence implemented in OCaml) to Elpi via a Rocq plugin
 
 ### Applications written in Coq-Elpi
 
diff --git a/examples/example_plugin/doc/dune b/examples/example_plugin/doc/dune
@@ -0,0 +1,16 @@
+(executable
+ (name gen_doc)
+ (libraries elpi_example_plugin))
+
+(rule
+ (targets
+  elpi_example_plugin.elpi)
+ (deps gen_doc.exe)
+ (mode promote)
+ (action (run ./gen_doc.exe)))
+
+(install
+ (files
+  elpi_example_plugin.elpi)
+ (section doc)
+ (package rocq-elpi))
diff --git a/examples/example_plugin/doc/elpi_example_plugin.elpi b/examples/example_plugin/doc/elpi_example_plugin.elpi
@@ -0,0 +1,12 @@
+
+
+% doc
+kind stuff type.
+external symbol stuff : int -> stuff = "1". 
+
+% [q xxx] bla
+external func q stuff.
+
+
+
+
diff --git a/examples/example_plugin/doc/gen_doc.ml b/examples/example_plugin/doc/gen_doc.ml
@@ -0,0 +1,3 @@
+
+let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated"
+  Elpi_example_plugin.Rocq_elpi_example_plugin.builtins
diff --git a/examples/example_plugin/src/dune b/examples/example_plugin/src/dune
@@ -0,0 +1,6 @@
+(library
+ (name elpi_example_plugin)
+ (public_name rocq-elpi.elpi_example_plugin)
+ (flags :standard -w -27)
+ (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")"))
+ (libraries rocq-runtime.plugins.ltac rocq-runtime.vernac rocq-elpi.elpi elpi))
diff --git a/examples/example_plugin/src/elpi_example_plugin.mlpack b/examples/example_plugin/src/elpi_example_plugin.mlpack
@@ -0,0 +1 @@
+Rocq_elpi_example_plugin
diff --git a/examples/example_plugin/src/rocq_elpi_example_plugin.ml b/examples/example_plugin/src/rocq_elpi_example_plugin.ml
@@ -0,0 +1,17 @@
+open Elpi.API
+let c = AlgebraicData.(declare {
+  ty = Conversion.TyName "stuff";
+  doc = "doc";
+  pp = (fun fmt (x : int) -> ());
+  constructors = [
+    K("stuff","",A(BuiltInData.int,N),B (fun x -> x),M (fun ~ok ~ko:_ x -> ok x));
+  ];
+}
+) |> ContextualConversion.(!<)
+
+let builtins =
+  let open BuiltIn in
+  let open BuiltInPredicate in
+  let cx = MLData c in
+  let q = MLCode(Pred("q",In(c,"xxx",Easy "bla"),(fun i ~depth -> Printf.eprintf "ok %d\n%!" i)),DocAbove) in
+  declare ~file_name:"elpi_example_plugin.elpi" [ cx; q ]
diff --git a/examples/example_plugin/theories/dune b/examples/example_plugin/theories/dune
@@ -0,0 +1,6 @@
+(coq.theory
+ (name example_plugin)
+ (theories elpi)
+ (plugins rocq-elpi.elpi_example_plugin))
+
+(include_subdirs qualified)
diff --git a/examples/example_plugin/theories/example_plugin.v b/examples/example_plugin/theories/example_plugin.v
@@ -0,0 +1,15 @@
+Declare ML Module "rocq-elpi.elpi_example_plugin".
+
+From elpi Require Import elpi.
+
+Elpi Command test.
+
+Fail Elpi Query lp:{{
+  q (stuff 46)
+}}.
+
+Elpi Accumulate Plugin "elpi_example_plugin.elpi".
+
+Elpi Query lp:{{
+  q (stuff 46)
+}}.
diff --git a/examples/example_plugin/theories/example_plugin2.v b/examples/example_plugin/theories/example_plugin2.v
@@ -0,0 +1,9 @@
+
+From elpi Require Import elpi.
+From example_plugin Require Import example_plugin.
+
+Elpi Command test2.
+Elpi Accumulate Plugin "elpi_example_plugin.elpi".
+Elpi Query lp:{{
+  q (stuff 46)
+}}.
diff --git a/rocq-elpi.opam b/rocq-elpi.opam
@@ -17,7 +17,7 @@ bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
 depends: [
   "dune" {>= "3.13"}
   "ocaml" {>= "4.10.0"}
-  "elpi" {>= "3.6.0" & < "3.7.0~"}
+  "elpi" {>= "3.6.1" & < "3.7.0~"}
   "rocq-core" {>= "9.0+rc1" & < "9.2~" | = "dev"}
   "ppx_optcomp"
   "ocaml-lsp-server" {with-dev-setup}
diff --git a/src/rocq_elpi_programs.ml b/src/rocq_elpi_programs.ml
@@ -207,6 +207,7 @@ module type Programs = sig
   val ast_from_string : elpi:API.Setup.elpi -> loc:Loc.t -> API.Ast.Loc.t -> string -> Digest.t * API.Compile.scoped_program
   val unit_from_ast    : ?error_header:string -> elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string option -> API.Compile.scoped_program -> cunit
   val unit_signature_from_ast    : elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string option -> API.Compile.scoped_program -> cunit
+  val unit_from_plugin : ?error_header:string -> elpi:API.Setup.elpi -> base:API.Compile.program -> loc:Loc.t -> string -> API.Setup.builtins -> cunit
   val extend_w_units : base:API.Compile.program -> loc:Loc.t -> cunit list -> API.Compile.program
   val parse_goal : elpi:API.Setup.elpi -> loc:Loc.t -> API.Ast.Loc.t -> string -> API.Ast.query
 
@@ -391,16 +392,25 @@ let intern_unit_signature u =
   
 (* Source files can be large, and loaded multiple times since many entry point
    can be implemented in the same file. We share (in memory) the parsed file. *)
-let unit_from_ast ?error_header ~elpi ~flags h ~base ~loc ast =
+let unit_from_ast ?error_header ~elpi ~flags h ~base ~loc ?builtins ast =
   handle_elpi_compiler_errors ~loc ?error_header (fun () ->
-    let u = EC.unit ~elpi ~flags ~base ast in
+    let u = EC.unit ~elpi ~flags ~base ?builtins ast in
     intern_unit (h,u,flags))
 
 let unit_signature_from_ast ~elpi ~flags h ~base ~loc ast =
   handle_elpi_compiler_errors ~loc (fun () ->
     let u = EC.unit ~elpi ~flags ~base ast in
     intern_unit_signature (h,u,flags))
         
+let unit_from_plugin ?error_header ~elpi ~base ~loc name builtins ~flags : cunit =
+  handle_elpi_compiler_errors ~loc (fun () ->
+    let ast = EP.program ~elpi ~files:[] in
+    let ast = EC.scope ~elpi ~builtins ast in
+    let loc = Loc.initial Loc.ToplevelInput in
+    let hash = Digest.(to_hex @@ string name) in
+    unit_from_ast ~elpi ~flags (Some hash) ~base ~loc ~builtins ast)
+
+
 let unit_from_file ~elpi ~base ~loc x : cunit =
   let flags = cc_flags () in
   let hash = Digest.(to_hex @@ file (EP.resolve_file ~elpi ~unit:x ())) in
@@ -703,6 +713,8 @@ let get ?(fail_if_not_exists=false) p =
 let unit_signature_from_ast ~elpi ~base ~loc h ast =
   unit_signature_from_ast ~elpi ~base h ~loc ast ~flags:(cc_flags ())
   
+let unit_from_plugin ?error_header ~elpi ~base ~loc name builtins =
+  unit_from_plugin ?error_header ~elpi ~base ~loc name builtins ~flags:(cc_flags ())
 
 (* Units are marshalable, but programs are not *)
 
diff --git a/src/rocq_elpi_programs.mli b/src/rocq_elpi_programs.mli
@@ -85,6 +85,7 @@ module type Programs = sig
   val ast_from_string  : elpi:Setup.elpi -> loc:Loc.t -> Ast.Loc.t -> string -> Digest.t * Compile.scoped_program
   val unit_from_ast    : ?error_header:string -> elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string option -> Compile.scoped_program -> cunit
   val unit_signature_from_ast    : elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string option -> Compile.scoped_program -> cunit
+  val unit_from_plugin : ?error_header:string -> elpi:Setup.elpi -> base:Compile.program -> loc:Loc.t -> string -> Setup.builtins -> cunit
   val extend_w_units   : base:Compile.program -> loc:Loc.t -> cunit list -> Compile.program
   val parse_goal       : elpi:Setup.elpi -> loc:Loc.t -> Ast.Loc.t -> string -> Ast.query
 
diff --git a/src/rocq_elpi_vernacular.ml b/src/rocq_elpi_vernacular.ml
@@ -291,6 +291,24 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x)
     
   let accumulate_extra_deps ~atts:((scope,only),ph) ~loc ?program ~what ids = skip ~only ~ph (accumulate_extra_deps ~loc ?program ~scope ~what) ids
 
+
+  let accumulate_plugin ~loc ?(program=current_program()) ~scope id =
+    let elpi = P.ensure_initialized () in
+    warn_scope_not_regular ~loc scope;
+    match get_base ~loc ~elpi program with
+    | `Db _ -> err ~loc:(of_coq_loc loc) Pp.(str "TODO")
+    | `Program base ->
+        let b =
+          try Elpi.API.BuiltIn.of_file id
+          with Not_found -> err ~loc:(of_coq_loc loc) Pp.(str "Elpi plugin " ++ str id ++
+            str " not found." ++ spc () ++ str "Did you have a Declare ML Module for the plugin?"++ spc () ++
+            str "Does the plugin run Elpi.API.BuiltIn.declare ~file_name:\"" ++ str id ++ str "\"?") in
+        let u = P.unit_from_plugin ~elpi ~base ~loc id b in
+        let new_src_ast = File { fname = id; fast = u; } in
+        P.accumulate ~loc program [new_src_ast]
+
+  let accumulate_plugin ~atts:((scope,only),ph) ~loc ?program id = skip ~only ~ph (accumulate_plugin ~loc ?program ~scope) id
+
   let accumulate_files ~loc ?(program=current_program()) ~scope s =
     let elpi = P.ensure_initialized () in
     try
@@ -460,6 +478,7 @@ module type Common = sig
 
   val accumulate_files       : atts:atts -> loc:Loc.t -> ?program:qualified_name -> string list -> unit
   val accumulate_extra_deps  : atts:atts -> loc:Loc.t -> ?program:qualified_name -> what:what -> qualified_name list -> unit
+  val accumulate_plugin      : atts:atts -> loc:Loc.t -> ?program:qualified_name -> string -> unit
   val accumulate_string      : atts:atts -> loc:Loc.t -> ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> unit
   val accumulate_db          : atts:atts -> loc:Loc.t -> ?program:qualified_name -> qualified_name -> unit
   val accumulate_db_header   : atts:atts -> loc:Loc.t -> ?program:qualified_name -> qualified_name -> unit
diff --git a/src/rocq_elpi_vernacular.mli b/src/rocq_elpi_vernacular.mli
@@ -28,6 +28,7 @@ module type Common = sig
 
   val accumulate_files       : atts:atts -> loc:Loc.t -> ?program:qualified_name -> string list -> unit
   val accumulate_extra_deps  : atts:atts -> loc:Loc.t -> ?program:qualified_name -> what:what -> qualified_name list -> unit
+  val accumulate_plugin      : atts:atts -> loc:Loc.t -> ?program:qualified_name -> string -> unit
   val accumulate_string      : atts:atts -> loc:Loc.t -> ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> unit
   val accumulate_db          : atts:atts -> loc:Loc.t -> ?program:qualified_name -> qualified_name -> unit
   val accumulate_db_header   : atts:atts -> loc:Loc.t -> ?program:qualified_name -> qualified_name -> unit
diff --git a/src/rocq_elpi_vernacular_syntax.mlg b/src/rocq_elpi_vernacular_syntax.mlg
@@ -257,6 +257,18 @@ VERNAC COMMAND EXTEND ElpiAccumulate CLASSIFIED AS SIDEFF
      atts
    } -> {
      EV.Interp.accumulate_extra_deps ~atts ~loc:gloc ~program:(snd p) ~what:Signature (List.map snd ids) }
+| #[ atts = any_attribute ] [ "Elpi" "Accumulate" ghost(gloc) "Plugin" string(s) ] SYNTERP AS atts {
+     let atts = validate_attributes scope_and_skip_and_synterp_attributes atts in
+     EV.Synterp.accumulate_plugin ~atts ~loc:gloc s;
+     atts
+   } -> {
+     EV.Interp.accumulate_plugin ~atts ~loc:gloc s }
+| #[ atts = any_attribute ] [ "Elpi" "Accumulate" ghost(gloc) qualified_name(p) "Plugin" string(s) ] SYNTERP AS atts {
+     let atts = validate_attributes scope_and_skip_and_synterp_attributes atts in
+     EV.Synterp.accumulate_plugin ~atts ~loc:gloc ~program:(snd p) s;
+     atts
+   } -> {
+     EV.Interp.accumulate_plugin ~atts ~loc:gloc ~program:(snd p) s }
 
 (************************************** legacy accumulation *************************************************)
 

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,3 @@`
	`1`	`+`
	`2`	`+let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated"`
	`3`	`+ Elpi_example_plugin.Rocq_elpi_example_plugin.builtins`