Add builtin to the tc app

.github/workflows/release.yml

@@ -98,6 +98,6 @@ jobs:
           GITHUB_DEBUG=1 opam-publish --no-confirmation --tag=$TAG \
             --packages-directory=${OPAM_SUITE:-released}/packages \
             --repo=rocq-prover/opam --no-browser -v ${TAG##v}	\
-            rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam \
+            rocq-elpi.opam rocq-elpi-json.opam rocq-elpi-xml.opam rocq-elpi-typeclasses.opam\
             coq-elpi.opam \
             https://github.com/LPCIC/coq-elpi/releases/download/$TAG/rocq-elpi-${TAG##v}.tar.gz

Changelog.md

@@ -21,6 +21,12 @@ Requires Elpi 3.7.1 and Rocq 9.0, 9.1 or 9.2.
 ### Plugins
 - New `xml` plugin containing minimal bindings to `xml-light`, see
   [apps/xml](apps/xml/) for the doc.
+- New `typeclasses` plugin containing rocq-elpi's typeclass solver, see
+  [apps/tc](apps/tc/) for the doc.
+
+### API
+- New `coq.TC.override-solver` builtin calling the
+  `Elpi TC Solver Override _ Add _` directive.
 
 ### API
 - Change `main-interp-proof` and `main-interp-qed` changed type to better chain

apps/tc/doc/dune

@@ -0,0 +1,16 @@
+(executable
+ (name gen_doc)
+ (libraries elpi_tc_plugin))
+
+(rule
+ (targets
+  tc-builtin.elpi)
+ (deps gen_doc.exe)
+ (mode promote)
+ (action (run ./gen_doc.exe)))
+
+(install
+ (files
+  tc-builtin.elpi)
+ (section doc)
+ (package rocq-elpi-typeclasses))

apps/tc/doc/gen_doc.ml

@@ -0,0 +1,3 @@
+
+let _ = Elpi.API.BuiltIn.document_file ~header:"% Generated"
+  Elpi_tc_plugin.Rocq_elpi_class_tactics_takeover.tc_builtins

apps/tc/src/dune

@@ -1,6 +1,6 @@
 (library
  (name elpi_tc_plugin)
- (public_name rocq-elpi.tc)
+ (public_name rocq-elpi-typeclasses.elpi_tc_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))

apps/tc/src/rocq_elpi_class_tactics_takeover.ml

@@ -180,6 +180,17 @@ let set_solver_mode kind qname (l: Libnames.qualid list) =
   | ANone-> Lib.add_leaf (cache_solver_mode (qname, Set (Only OSet.empty), false))
   | ASet -> Lib.add_leaf (cache_solver_mode (qname, Set (Only l), false))
 
+let tc_builtins = [
+  Elpi.API.BuiltIn.MLCode(Pred("coq.TC.override-solver",
+    In(Elpi.API.BuiltInData.string, "GR",
+    In(Elpi.API.BuiltInData.list Elpi.API.BuiltInData.string, "GR",
+    Easy("Declares that goals on GR should be solved using elpi's typeclass solver."))),
+  (fun s gr ~depth ->
+    set_solver_mode AAdd [s] (List.map Libnames.qualid_of_string gr))), 
+  DocAbove)]
+
+let tc_builtins = API.BuiltIn.declare ~file_name:"tc-builtin.elpi" tc_builtins
+
 let solver_register l =
   Lib.add_leaf (Solver.cache_solver (l, Create));
   Lib.add_leaf (Modes.cache_solver_mode (l, Add OSet.empty, true))

apps/tc/src/rocq_elpi_class_tactics_takeover.mli

@@ -8,3 +8,4 @@ val set_solver_mode : aaction -> string list -> Libnames.qualid list -> unit
 val solver_register : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
 val solver_activate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
 val solver_deactivate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit
+val tc_builtins : Elpi.API.Setup.builtins

apps/tc/src/rocq_elpi_tc_hook.mlg

@@ -1,7 +1,7 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-DECLARE PLUGIN "rocq-elpi.tc"
+DECLARE PLUGIN "rocq-elpi-typeclasses.elpi_tc_plugin"
 
 {
 open Stdarg
@@ -51,4 +51,4 @@ VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF
      let () = ignore_unknown_attributes atts in
      set_solver_mode ARm (snd p) cs }
 
-END
+END

apps/tc/theories/dune

@@ -1,8 +1,8 @@
 (coq.theory
  (name elpi.apps.tc)
- (package rocq-elpi)
- (theories elpi elpi.apps.tc.elpi)
+ (package rocq-elpi-typeclasses)
+ (theories elpi_elpi elpi elpi.apps.tc.elpi)
  (flags -w -all -w -elpi)
- (plugins rocq-elpi.tc))
+ (plugins rocq-elpi.elpi rocq-elpi-typeclasses.elpi_tc_plugin))
 
 (include_subdirs qualified)

apps/tc/theories/tc.v

@@ -1,7 +1,8 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* ------------------------------------------------------------------------- *)
 
-Declare ML Module "rocq-elpi.tc".
+From elpi Require Import elpi.
+Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin".
 
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *)

apps/tc/theories/wip.v

@@ -1,8 +1,9 @@
 (* license: GNU Lesser General Public License Version 2.1 or later           *)
 (* --------------------------------------------------------------------------*)
 
-Declare ML Module "rocq-elpi.tc".
+(*
 From elpi Require Import elpi.
+Declare ML Module "rocq-elpi-typeclasses.elpi_tc_plugin".
 
 From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes.
 From elpi.apps.tc.elpi Extra Dependency "ho_precompile.elpi" as ho_precompile.
@@ -16,7 +17,7 @@ From elpi.apps.tc.elpi Extra Dependency "rewrite_forward.elpi" as rforward.
 From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux.
 From elpi.apps.tc.elpi Extra Dependency "create_tc_predicate.elpi" as create_tc_predicate.
 
-(* From elpi.apps Require Import tc.
+From elpi.apps Require Import tc.
 Set Warnings "+elpi".
 
 Elpi Command AddForwardRewriting.

dune-project

@@ -35,6 +35,12 @@
   ppx_optcomp
   (ocaml-lsp-server :with-dev-setup)))
 
+(package
+ (name rocq-elpi-typeclasses)
+ (synopsis "TC bindings for rocq-elpi")
+ (description "This package provides a typeclass solver written in Elpi for Rocq")
+ (depends rocq-elpi))
+
 (package
  (name rocq-elpi-json)
  (synopsis "Yojson bindings for rocq-elpi")

rocq-elpi-typeclasses.opam

@@ -0,0 +1,29 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "TC bindings for rocq-elpi"
+description: "This package provides a typeclass solver written in Elpi for Rocq"
+maintainer: ["Enrico Tassi <enrico.tassi@inria.fr>"]
+authors: ["Enrico Tassi <enrico.tassi@inria.fr>"]
+license: "LGPL-2.1-or-later"
+homepage: "https://github.com/LPCIC/coq-elpi/apps/tc/"
+bug-reports: "https://github.com/LPCIC/coq-elpi/issues"
+depends: [
+  "dune" {>= "3.13"}
+  "rocq-elpi"
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "etc/with-rocq-wrap.sh" {!coq-core:installed}
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/LPCIC/coq-elpi.git"