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

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.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

@@ -4,4 +4,3 @@
   ; Use -03 in release mode when the compiler has flambda enabled
   (release (ocamlopt_flags :standard -O3))
 )
-

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 @@
+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
+
+type _ Builtin.t += Abs_real
+
+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.Ext.create ~name:"abs_real" ~builtins

examples/extensions/abs_real/dune

@@ -0,0 +1,10 @@
+(library
+  (public_name dolmen-extension-abs-real)
+  (name abs_real)
+  (modules abs_real)
+  (libraries dolmen_model))
+
+(plugin
+  (name abs_real)
+  (libraries dolmen-extension-abs-real)
+  (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-extension-abs-real)
+  (depends 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/abs_real_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_typing.Abs_real -> abs_real ~cst
+  | _ -> None
+
+let model_ext =
+  Dolmen_model.Ext.create ~name:"abs_real_split" ~builtins

examples/extensions/abs_real_split/abs_real_typing.ml

@@ -0,0 +1,32 @@
+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
+
+type _ Builtin.t += Abs_real
+
+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_split" ~builtins

examples/extensions/abs_real_split/dune

@@ -0,0 +1,23 @@
+(library
+  (public_name dolmen-typing-extension-abs-real-split)
+  (name abs_real_typing)
+  (modules abs_real_typing)
+  (libraries dolmen_loop))
+
+(library
+  (public_name dolmen-model-extension-abs-real-split)
+  (name abs_real_model)
+  (modules abs_real_model)
+  (libraries dolmen_model dolmen-typing-extension-abs-real-split))
+
+(plugin
+  (package dolmen-typing-extension-abs-real-split)
+  (name abs_real_split.typing)
+  (libraries dolmen-typing-extension-abs-real-split)
+  (site (dolmen plugins)))
+
+(plugin
+  (package dolmen-model-extension-abs-real-split)
+  (name abs_real_split.model)
+  (libraries dolmen-model-extension-abs-real-split)
+  (site (dolmen plugins)))

examples/extensions/abs_real_split/dune-project

@@ -0,0 +1,12 @@
+(lang dune 3.0)
+(using dune_site 0.1)
+
+(generate_opam_files false)
+
+(package
+  (name dolmen-typing-extension-abs-real-split)
+  (depends dolmen_type dolmen_loop))
+
+(package
+  (name dolmen-model-extension-abs-real-split)
+  (depends dolmen-typing-extension-abs-real-split dolmen_model))

src/bin/dune

@@ -1,4 +1,3 @@
-
 (executable
   (name           main)
   (public_name    dolmen)