Plugins

Some programming tasks are tedious and distracting, such as writing pretty-printers or (de)serializers for one's types. Imandra provides a plugin mechanism to make your life easier using automatic code generation

In [1]:
[@@@ocaml.warning "-3"];;
Imandra.add_plugin_pp ();;
Imandra.add_plugin_yojson ();;
Out[1]:
- : unit = ()
- : unit = ()
In [2]:
type t = {
    x: int;
    y: string;
}
Out[2]:
type t = { x : int; y : string; }
val to_yojson_t : t -> YJ.json = <fun>
val of_yojson_t : YJ.json -> (t, string) result = <fun>
val pp_t : t Fmt.printer = <fun>

Note that when we define t, some functions were automatically defined along. Let's try them.

In [3]:
let some_t = {x=42; y="howdy"};;

let some_json = to_yojson_t some_t [@@program];;

Format.printf "some_t = %a@." pp_t some_t;;
Out[3]:
val some_t : t = {x = 42; y = "howdy"}
val some_json : YJ.json =
  `Assoc [("x", `Intlit "42"); ("y", `String "howdy")]
some_t = {x=42; y="howdy"}
- : unit = ()

We can also deserialize the json object we just got, and recover Ok x where x is the same object as some_t:

In [4]:
of_yojson_t some_json;;
Out[4]:
- : (t, string) result = Ok {x = 42; y = "howdy"}

These functions are program-mode only, though. Plugins can define logic-mode functions, but for most use cases it's not necessary, and program-mode code generation is easier.

In [5]:
#h;;
Out[5]:

All events in session

  • 0. Type: t
  • 1. Fun: some_t

dependency graph

We can also load plugins in the middle of a development, and it will automatically apply to pre-existing definitions.

It is cleaner to load plugins first, but nevertheless, this is a possibility.

For example, we can ask Imandra to produce random generators for all types, automatically:

In [6]:
Imandra.add_plugin_rand ();;
Out[6]:
- : unit = ()
In [7]:
rand_t;;
Out[7]:
- : Gen_rand_Random.t -> t = <fun>
In [8]:
(* a random state with fixed seed, so that this notebook is deterministic *)
let rand_st = Random.State.make [| 4i |] [@@program];;

(* generate a list of at most 5 instances of [t] *)
let l = gen_rand_l ~st:rand_st ~n:5i rand_t [@@program];;
Out[8]:
val rand_st : Random.State.t = <abstr>
val l : t CCList.t = [{x = -16; y = ""}; {x = -38; y = "[JhDMejnbX"}]