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

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

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

Try this!
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.t = `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:

Try this!
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.

Try this!
In [5]:
#h;;
Out[5]:





















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:











  
    
Try this!

  





In [6]:



    


Imandra.add_plugin_rand ();;




















Out[6]:








- : unit = ()



















  
    
Try this!

  





In [7]:



    


rand_t;;




















Out[7]:








- : Gen_rand_Random.t -> t = <fun>



















  
    
Try this!

  





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 : Gen_rand_Random.t = <abstr>
val l : t list = [{x = -16; y = ""};{x = -38; y = "[JhDMejnbX"}]