Typeclass-based Ltac2 dispatch.

rocq-ltac2-tc-dispatch/README.md

@@ -0,0 +1,7 @@
+Extensible Ltac2 Dispatch with Typeclasses
+===========================================
+
+To use the library, require via the following command:
+```coq
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+```

rocq-ltac2-tc-dispatch/dune

@@ -0,0 +1,16 @@
+(env
+ (sl_timing
+  (binaries
+   (../rocq-tools/bin/rocq_perf.exe as rocq))
+  (flags :standard %{read-lines:flags/ocamlc})
+  (ocamlopt_flags :standard -O3 -unbox-closures)
+  (rocq
+   (rocqdep_flags :standard -w +all)
+   (flags (:standard %{read-lines:flags/coqc}))))
+ ; Same, but without coqc_perf
+ (_
+  (flags :standard %{read-lines:flags/ocamlc})
+  (ocamlopt_flags :standard -O3 -unbox-closures)
+  (rocq
+   (rocqdep_flags :standard -w +all)
+   (flags (:standard %{read-lines:flags/coqc})))))

rocq-ltac2-tc-dispatch/dune-project

@@ -0,0 +1,22 @@
+(lang dune 3.21)
+(using rocq 0.11)
+(name ltac2-tc-dispatch)
+
+(generate_opam_files)
+
+(maintainers
+ "Gregory Malecha <gregory@skylabs-ai.com>")
+
+(authors
+ "Gregory Malecha <gregory@skylabs-ai.com>")
+
+(license MIT)
+
+(source (github SkyLabsAI/BRiCk))
+
+(package
+ (name ltac2-tc-dispatch)
+ (synopsis "Typeclass-based lookup for Ltac2 functions")
+ (depends coq-core coq-stdlib stdlib-extra rocq-extra))
+
+(subst disabled)

rocq-ltac2-tc-dispatch/flags

@@ -0,0 +1 @@
+../flags

rocq-ltac2-tc-dispatch/ltac2-tc-dispatch.opam

@@ -0,0 +1,31 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Typeclass-based lookup for Ltac2 functions"
+maintainer: ["Gregory Malecha <gregory@skylabs-ai.com>"]
+authors: ["Gregory Malecha <gregory@skylabs-ai.com>"]
+license: "MIT"
+homepage: "https://github.com/SkyLabsAI/BRiCk"
+bug-reports: "https://github.com/SkyLabsAI/BRiCk/issues"
+depends: [
+  "dune" {>= "3.21"}
+  "coq-core"
+  "coq-stdlib"
+  "stdlib-extra"
+  "rocq-extra"
+  "odoc" {with-doc}
+]
+build: [
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]
+dev-repo: "git+https://github.com/SkyLabsAI/BRiCk.git"
+x-maintenance-intent: ["(latest)"]

rocq-ltac2-tc-dispatch/plugin/dune

@@ -0,0 +1,4 @@
+(library
+ (name ltac2_tc_dispatch)
+ (public_name ltac2-tc-dispatch.plugin)
+ (libraries coq-core.plugins.ltac2 rocq-extra stdlib-extra ltac2-extra.plugin))

rocq-ltac2-tc-dispatch/plugin/lookup.ml

@@ -0,0 +1,47 @@
+
+open Ltac2_plugin
+open Tac2ffi
+(* open Tac2val *)
+open Tac2externals
+
+let resolve_ltac2_safe (mp : string list) (id : string) : (unit -> unit Proofview.tactic) option =
+  let qualid = Libnames.make_qualid
+    (Names.DirPath.make (List.map Names.Id.of_string mp))
+    (Names.Id.of_string id)
+  in
+  let is_unit_typ (t : int Tac2expr.glb_typexpr) : bool =
+    (* TODO: why does Init.unit have two different representations? *)
+    match t with
+    | Tac2expr.GTypRef (Tac2expr.Other ty, []) ->
+      ty = Tac2core.Core.t_unit
+    | Tac2expr.GTypRef (Tac2expr.Tuple 0, []) ->
+      true
+    | _ -> false
+  in
+  let is_unit_to_unit ((n, t) : Tac2expr.type_scheme) : bool =
+    Int.equal n 0 &&
+    match t with
+    | Tac2expr.GTypArrow (t1, t2) -> is_unit_typ t1 && is_unit_typ t2
+    | _ -> false
+  in
+  match Tac2env.locate_ltac qualid with
+  | Tac2expr.TacConstant kn ->
+    let data = Tac2env.interp_global kn in
+    if is_unit_to_unit data.Tac2env.gdata_type
+    then
+      let v = Tac2interp.eval_global kn in
+      Some (repr_to (fun1 unit unit) v)
+    else
+      None
+  | Tac2expr.TacAlias _ ->
+    None
+  | exception Not_found -> None
+
+
+let define s =
+  define Tac2expr.{ mltac_plugin = "ltac2_tc_dispatch"; mltac_tactic = s }
+
+let () =
+  define "resolve_ltac2"
+    (list string @-> string @-> ret (option (fun1 unit unit))) @@ fun modpath name ->
+    resolve_ltac2_safe modpath name

rocq-ltac2-tc-dispatch/tests/dune

@@ -0,0 +1,4 @@
+(include_subdirs qualified)
+(rocq.theory
+ (name skylabs_tests.ltac2.tc_dispatch)
+ (theories Stdlib skylabs.ltac2.extra skylabs.ltac2.tc_dispatch))

rocq-ltac2-tc-dispatch/tests/external.v

@@ -0,0 +1,13 @@
+Require Import Stdlib.Strings.PrimString.
+Require Import Ltac2.Ltac2.
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+
+Ltac2 ext_tactic () := ltac1:(reflexivity).
+
+#[local] Open Scope pstring_scope.
+
+#[export]
+Instance nested_inst : Ltac2Lookup (0 = 0) := {
+  ltac2_path := "external" :: "tc_dispatch" :: "ltac2" :: "skylabs_tests" :: nil;
+  ltac2_name := "ext_tactic";
+}.

rocq-ltac2-tc-dispatch/tests/nested.v

@@ -0,0 +1,17 @@
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+Require Import Stdlib.Strings.PrimString.
+
+#[local] Open Scope pstring_scope.
+
+Module Import Nested.
+  Ltac2 inside_module () := ltac1:(reflexivity).
+  Instance nested_inst : Ltac2Lookup (0 = 0) := {
+    ltac2_path := "Nested" :: "nested" :: "tc_dispatch" :: "ltac2" :: "skylabs_tests" :: nil;
+    ltac2_name := "inside_module";
+  }.
+End Nested.
+
+Example test_success_nested : 0 = 0.
+Proof.
+  goal_dispatch. (* Should resolve Nested.inside_module *)
+Qed.

rocq-ltac2-tc-dispatch/tests/simple.v

@@ -0,0 +1,47 @@
+Require Import Stdlib.Lists.List.
+Require Import Stdlib.Strings.PrimString.
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+
+#[local] Open Scope pstring_scope.
+
+(* A simple success tactic *)
+Ltac2 solve_true () := ltac1:(exact I).
+
+(* A tactic that prints a message *)
+Ltac2 say_hello () := Message.print (Message.of_string "Hello from dynamic lookup!").
+
+(* Success Instance for True *)
+Instance test_true_inst : Ltac2Lookup True := {
+  ltac2_path := "simple" :: "tc_dispatch" :: "ltac2" :: "skylabs_tests" :: nil;
+  ltac2_name := "solve_true";
+}.
+
+(* Success Instance for False (pointing to a printing tactic) *)
+Instance test_hello_inst : Ltac2Lookup False := {
+  ltac2_path := nil;
+  ltac2_name := "say_hello";
+}.
+
+(* A "Broken" Instance: String name does not exist *)
+Instance broken_inst : Ltac2Lookup (True -> True) := {
+  ltac2_path := nil;
+  ltac2_name := "non_existent_tactic_12345";
+}.
+
+Example test_succeed : True.
+Proof.
+  goal_dispatch.
+Abort.
+
+
+(* Testing the "No Instance" failure *)
+Example test_fail_no_instance : unit.
+Proof.
+  Fail goal_dispatch.
+Abort.
+
+(* Testing the "Invalid Name" failure *)
+Example test_fail_bad_string : nat.
+Proof.
+  Fail goal_dispatch. (* Triggers the None branch of our match *)
+Abort.

rocq-ltac2-tc-dispatch/tests/test_external.v

@@ -0,0 +1,7 @@
+Require Import skylabs_tests.ltac2.tc_dispatch.external.
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+
+Goal 0 = 0.
+Proof.
+  goal_dispatch.
+Qed.

rocq-ltac2-tc-dispatch/theories/crush_ext.v

@@ -0,0 +1,22 @@
+Require Ltac2.Ltac2.
+Require Import skylabs.ltac2.tc_dispatch.lookup.
+
+(**
+[crush_ext] is An extensible version of [crush].
+
+Users can add new tactics / strategies by adding [Ltac2Lookup] hints
+to the [crush_ext] database.
+ *)
+
+Create HintDb crush_ext discriminated.
+
+Module ltac2.
+    Import Ltac2.Init.
+    Import Ltac2.Notations.
+    Ltac2 crush2 () :=
+      let dbs := Some [ident:(crush_ext)] in
+      repeat (ltac2.goal_dispatch_with dbs).
+End ltac2.
+
+Ltac crush_ext :=
+    ltac2:(ltac2.crush2 ()).

rocq-ltac2-tc-dispatch/theories/dune

@@ -0,0 +1,10 @@
+(include_subdirs qualified)
+(rocq.theory
+ (name skylabs.ltac2.tc_dispatch)
+ (package ltac2-tc-dispatch)
+ (theories
+  Ltac2
+  Stdlib ; for ltac2-extra/theories/internal/char.v
+  skylabs.ltac2.extra
+  )
+ (plugins ltac2-tc-dispatch.plugin))

rocq-ltac2-tc-dispatch/theories/lookup.v

@@ -0,0 +1,76 @@
+(*
+ * Copyright (C) 2026 SkyLabs AI, Inc.
+ *)
+Require Import Ltac2.Ltac2.
+Require Import Ltac2.Control.
+Require Import Ltac2.Printf.
+
+
+Require Import Ltac2.Std.
+Require Import Stdlib.Strings.PrimString.
+Require Import skylabs.ltac2.extra.extra.
+
+Declare ML Module "ltac2-tc-dispatch.plugin".
+
+(* The typeclass: P is the goal/type, path is the module hierarchy, name is the tactic *)
+Class Ltac2Lookup (P : Prop) := {
+    ltac2_path : list string;
+    ltac2_name : string;
+  }.
+
+Module ltac2.
+
+  Ltac2 @ external resolve_ltac2 : string list -> string -> (unit -> unit) option :=
+    "ltac2_tc_dispatch" "resolve_ltac2".
+
+  Ltac2 Type exn ::= [ UnexpectedConstr (string * constr) ].
+
+  Ltac2 string_of_pstring_constr (c : constr) : string :=
+    match Constr.Unsafe.kind c with
+    | Constr.Unsafe.String s => Pstring.to_string s
+    | _ => throw (UnexpectedConstr("Expected a pstring", c))
+    end.
+
+  Ltac2 rec list_of_list_constr (f : constr -> 'a) (c : constr) : 'a list :=
+    lazy_match! c with
+    | List.nil => []
+    | List.cons ?c ?cs => f c :: list_of_list_constr f cs
+    end.
+
+  Ltac2 goal_dispatch_with (dbs : ident list option) :=
+    let g := Control.goal () in
+    let query := constr:(Ltac2Lookup $g) in
+    (* let _ := printf "query=%t" query in *)
+    let inst := Constr.Unsafe.make (TC.resolve dbs query) in
+    (* let _ := printf "inst=%t" inst in *)
+    let flags := RedFlags.all in
+    let reduced_inst := Std.eval_cbv flags inst in
+    (* let _ := printf "reduced_inst=%t" reduced_inst in *)
+
+    lazy_match! reduced_inst with
+    | {| ltac2_path := ?p; ltac2_name := ?n |} =>
+        let p_ltac2 := list_of_list_constr (fun c => string_of_pstring_constr c) p in
+        let n_ltac2 := string_of_pstring_constr n in
+        (* printf "n_ltac2=%s" n_ltac2 ; *)
+
+        match resolve_ltac2 p_ltac2 n_ltac2 with
+        | Some f =>
+            (* let _ := printf "resolve_ltac2 success!" in *)
+            f ()
+        | None =>
+            (* let _ := printf "resolve_ltac2 failed!" in *)
+
+            let err :=
+              Message.concat [Message.of_string "Could not find: ";
+                              Message.of_string n_ltac2] in
+            Control.zero (Tactic_failure (Some err))
+        end
+    | _ =>
+        Control.zero (Tactic_failure (Some (Message.of_string "Could not reduce instance to record.")))
+    end.
+
+End ltac2.
+
+Ltac goal_dispatch :=
+  idtac;
+  ltac2:(ltac2.goal_dispatch_with None).