feat: Add support for user-defined builtins with Dune plugins

This patch adds support for model extensions in `Dolmen_loop` using a
similar mechanism to typing extensions.

Model extensions and typing extensions are now loaded by the binary
through Dune's plugin mechanism, and the existing `bvconv` extension is
moved to use the plugin mechanism.

Fixes #203

doc/extensions.md

@@ -0,0 +1,25 @@
+# User-defined builtins
+
+Dolmen supports extensions through the form of user-defined builtins; see the
+`abs_real` and `abs_real_split` plugins.
+
+User-defined builtins can be added to the extensible `Builtin` type in
+`Dolmen.Std.Builtin.t`.
+
+Builtins need to be registered with the typer using `Dolmen_loop.Typer.Ext`,
+and they optionally need to be registered with the model evaluation mechanism
+(if they are to be used with model verification) using `Dolmen_model.Env.Ext`.
+
+The `dolmen` command-line tool looks up user-defined extensions using the Dune
+plugin mechanism. A plugin named `plugin.typing` will be picked up when
+`--ext plugin` or `--ext plugin.typing` is provided on the command-line, and
+the plugin must register a typing extension named `"plugin"` using
+`Dolmen_loop.Typer.Ext.create`. A plugin named `plugin.model` will be picked up
+when `--ext plugin` or `--ext plugin.model` is provided on the command-line and
+the plugin must register a model extension named `"plugin"` using
+`Dolmen_model.Env.Ext.create`. A plugin named `plugin` (without dots) will be
+picked up when either of the above command line flags is provided, and must
+provide both a typing and model extension.
+
+*Note*: Model extensions are only used (and their existence checked) if the
+user provides the `--check-model` flag.

dolmen_bin.opam

@@ -15,6 +15,7 @@ depends: [
   "dolmen_loop" {= version }
   "dolmen_model" {= version }
   "dune" { >= "3.0" }
+  "dune-site" { >= "3.0" }
   "fmt"
   "cmdliner" { >= "1.1.0" }
   "odoc" { with-doc }

dune-project

@@ -2,4 +2,24 @@
 (name dolmen)
 (using mdx 0.2)
 (using menhir 2.0)
+(using dune_site 0.1)
 (implicit_transitive_deps true)
+
+(package
+  (name dolmen)
+  (sites (lib plugins)))
+
+(package
+  (name dolmen_type))
+
+(package
+  (name dolmen_loop))
+
+(package
+  (name dolmen_model))
+
+(package
+  (name dolmen_bin))
+
+(package
+  (name dolmen_lsp))

examples/extensions/abs_real/README.md

@@ -0,0 +1,5 @@
+# `abs_real` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements both the typing and model extensions for the `abs_real`
+function in the same Dune plugin.

examples/extensions/abs_real/abs_real.ml

@@ -0,0 +1,49 @@
+type _ Dolmen.Std.Builtin.t += Abs_real
+
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real" ~builtins
+
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Env.Ext.create ~name:"abs_real" ~builtins

examples/extensions/abs_real/dune

@@ -0,0 +1,10 @@
+(library
+  (public_name dolmen-extensions-abs-real.plugin)
+  (name abs_real)
+  (modules abs_real)
+  (libraries dolmen_model))
+
+(plugin
+  (name abs_real)
+  (libraries dolmen-extensions-abs-real.plugin)
+  (site (dolmen plugins)))

examples/extensions/abs_real/dune-project

@@ -0,0 +1,8 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-extensions-abs-real)
+  (depopts dolmen_type dolmen_loop dolmen_model))

examples/extensions/abs_real_split/README.md

@@ -0,0 +1,8 @@
+# `abs_real_split` plugin
+
+This is an example plugin adding support for an `abs_real` function. This
+plugin implements the typing and model extensions for the `abs_real` function
+in separate Dune plugins.
+
+This is more complex than implementing `abs_real` as a single plugin, but
+allows using the typing extension without a dependency on `dolmen_model`.

examples/extensions/abs_real_split/builtin.ml

@@ -0,0 +1 @@
+type _ Dolmen.Std.Builtin.t += Abs_real

examples/extensions/abs_real_split/dune

@@ -0,0 +1,27 @@
+(library
+  (name abs_real_split)
+  (modules builtin)
+  (libraries dolmen)
+  (package dolmen-extensions-abs-real-split))
+
+(library
+  (public_name dolmen-extensions-abs-real-split.typing)
+  (name typing)
+  (modules typing)
+  (libraries dolmen_loop abs_real_split))
+
+(library
+  (public_name dolmen-extensions-abs-real-split.model)
+  (name model)
+  (modules model)
+  (libraries dolmen_model abs_real_split))
+
+(plugin
+  (name abs_real_split.typing)
+  (libraries dolmen-extensions-abs-real-split.typing)
+  (site (dolmen plugins)))
+
+(plugin
+  (name abs_real_split.model)
+  (libraries dolmen-extensions-abs-real-split.model)
+  (site (dolmen plugins)))

examples/extensions/abs_real_split/dune-project

@@ -0,0 +1,8 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-extensions-abs-real-split)
+  (depopts dolmen_type dolmen_loop dolmen_model))

examples/extensions/abs_real_split/model.ml

@@ -0,0 +1,16 @@
+module B = Dolmen.Std.Builtin
+module Fun = Dolmen_model.Fun
+
+let real = Dolmen_model.Real.mk
+let of_real = Dolmen_model.Real.get
+
+let abs_real ~cst =
+  Some (Fun.mk_clos @@ Fun.fun_1 ~cst (fun x -> real (Q.abs (of_real x))))
+
+let builtins ~eval:_ _ (cst : Dolmen.Std.Expr.Term.Const.t) =
+  match cst.builtin with
+  | Abs_real_split.Builtin.Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Env.Ext.create ~name:"abs_real_split" ~builtins

examples/extensions/abs_real_split/typing.ml

@@ -0,0 +1,30 @@
+module Type = Dolmen_loop.Typer.T
+module Ty = Dolmen.Std.Expr.Ty
+module Term = Dolmen.Std.Expr.Term
+module Builtin = Dolmen.Std.Builtin
+module Base = Dolmen_type.Base
+
+module Const = struct
+  let mk' ?pos ?name ?builtin ?tags cname vars args ret =
+    let ty = Ty.pi vars (Ty.arrow args ret) in
+    Dolmen.Std.Expr.Id.mk ?pos ?name ?builtin ?tags
+      (Dolmen.Std.Path.global cname) ty
+
+  module Real = struct
+    (* NB: Use [Dolmen.Std.Expr.with_cache] for parameterized builtins. *)
+    let abs =
+      mk' ~builtin:Abs_real_split.Builtin.Abs_real "abs_real"
+        [] [Ty.real] Ty.real
+  end
+end
+
+let abs_real x = Term.apply_cst Const.Real.abs [] [x]
+
+let builtins _lang env s =
+  match s with
+  | Type.Id { ns = Term ; name = Simple "abs_real" } ->
+    Type.builtin_term (Base.term_app1 (module Type) env s abs_real)
+  | _ -> `Not_found
+
+let typing_ext =
+  Dolmen_loop.Typer.Ext.create ~name:"abs_real_split" ~builtins

src/bin/dune

@@ -1,14 +1,16 @@
-
 (executable
   (name           main)
   (public_name    dolmen)
   (package        dolmen_bin)
   (libraries
     ; external deps
     cmdliner fmt gen
+    ; extension support
+    dune-site dune-site.plugins
     ; dolmen deps
     dolmen dolmen.intf dolmen.std
     dolmen_type dolmen_loop dolmen_model
+    dolmen_loop.bvconv dolmen_model.bvconv
     ; Memtrace dependency
     (select memory_profiler.ml from
             (memtrace -> memory_profiler.memtrace.ml)
@@ -28,3 +30,7 @@
  (files    dolmen.1)
  (package  dolmen_bin)
 )
+
+(generate_sites_module
+  (module Sites)
+  (plugins (dolmen plugins)))

src/bin/main.ml

@@ -118,6 +118,13 @@ let doc conf t =
     pp_status t
     (Report.T.doc t)
 
+(* Extensions list *)
+(* *************** *)
+
+let list_extensions () =
+  let all = Options.list_extensions () in
+  Format.printf "%a@." Fmt.(vbox @@ list (box Options.pp_plugin)) all
+
 
 (* Main code *)
 (* ********* *)
@@ -146,3 +153,5 @@ let () =
     doc conf report
   | Ok (`Ok List_reports { conf; }) ->
     list conf
+  | Ok (`Ok List_extensions) ->
+    list_extensions ()