Sketch of an extensible implementation of crush.

Author: gmalecha-at-skylabs

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/lookup.v

@@ -37,11 +37,11 @@ Module ltac2.
     | List.cons ?c ?cs => f c :: list_of_list_constr f cs
     end.
 
-  Ltac2 goal_dispatch () :=
+  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 None 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
@@ -68,8 +68,9 @@ Module ltac2.
     | _ =>
         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 ()).
+  ltac2:(ltac2.goal_dispatch_with None).