package ppx_mica

Mica: Automated Differential Testing for OCaml Modules

README Contents:

• Overview

• Compilation notes

• Case studies

• An overview of the codebase

• Differences between the OCaml Workshop '24 & ICFP '23 SRC artifacts

• Notes for implementors

  • Testing changes locally

  • Dependencies

Overview

Mica is a PPX extension that automates differential testing for a pair of OCaml modules implementing the same signature. Users annotate module signatures with the directive [@@deriving mica], and at compile-time, Mica derives specialized property-based testing (PBT) code that checks if two modules implementing the signature are observationally equivalent. (Under the hood, Mica uses Jane Street's Core.Quickcheck PBT library.)

An online demo of Mica is available here.

Mica was presented at the OCaml Workshop '24 and the ICFP '23 SRC. The OCaml Workshop paper contains a lot more details about Mica's design -- this README focuses on describing how to interact with our OCaml artifact.

Here is how we envisage users interacting with Mica:
Suppose modules M1 & M2 both implement the module signature S. Users insert the directive [@@deriving_inline mica] beneath the definition of S, like so:

module type S = sig
  type 'a t 
  val empty : 'a t
  val add : 'a -> 'a t -> 'a t
  ...
end
[@@deriving_inline mica] 
...
[@@@end]

Then, after users run dune build --auto-promote, the derived PBT code is automatically inserted in-line in the source file in-between [@@deriving_inline mica] and [@@@end]. (Note: this doesn't work fully out of the box at the moment -- see compilation notes for details.)

Then, after running dune build, Mica derives the following PBT code:

module Mica = struct 
  (** [expr] is an inductively-defined algebraic data type 
      representing {i symbolic expressions}. 
      
      Each [val] declaration in the module signature [S] corresponds to a 
      cosntructor for [expr] that shares the same name, arity & argument types. 
      - Type variables ['a] are instantiated with [int]
      - Function arguments of type ['a t] correpond to
        constructor arguments of type [expr] *)
  type expr =
    | Empty
    | Is_empty of expr
    ...
  [@@deriving show, ...]

  (** Types of symbolic expressions *)
  type ty = Int | IntT | ... [@@deriving show, ...]

  (** QuickCheck generator for symbolic expressions. 
      [gen_expr ty] generates random [expr]s of type [ty]. *)
  let rec gen_expr : ty -> Core.Quickcheck.Generator.t = ...

  (** Functor that interprets symbolic expressions *)
  module Interpret (M : S) = struct   
    (** Values of symbolic expressions *)
    type value = ValInt of int | ValIntT of int M.t | ...

    (** Big-step interpreter for symbolic expressions: 
        [interp] takes an [expr] and interprets it over the module 
        [M], evaluating the [expr] to a [value] *)
    let rec interp : expr -> value = ...
  end 

  (** Functor that tests [M1] and [M2] for observational equivalence *)
  module TestHarness (M1 : S) (M2 : S) = struct 
    (* Runs all observational equivalence tests *)
    let run_tests : unit -> unit = ... 
  end
end

• Now suppose modules M1 and M2 both implement S. To run Mica's testing code and check whether M1 & M2 are observationally equivalent with respect to S, one can invoke the run_tests : unit -> unit function in Mica's TestHarness functor, like so:

module T = Mica.TestHarness(M1)(M2)
let () = T.run_tests ()

• Note: Mica only tests for observational equivalence at concrete types (e.g. int, string option), and not abstract types defined in a module (e.g. 'a M.t), since abstract types have a more abstract notion of equality different from OCaml's standard notion of polymorphic equality.

A minimum working example of how to use Mica can be found in the bin subdirectory. Also, the case studies section of this README contains many more examples!

Compilation notes

There is a known issue with Ppxlib (#338, #342) which causes Ppxlib to error when Dune is promoting changes (i.e. after one runs dune build --auto-promote, during which Dune inserts the code derived by Mica into the source file).

To fix this issue, remove [@@deriving_inline mica] and [@@@end] from the source file while keeping the code inserted by Dune/Mica. Then, recompile by running dune build again. This second compilation run should complete successfully!

Case Studies

Code for the following case studies (along with the code automatically derived by Mica) is located in the ancillary mica_case_studies repo.

An overview of the codebase

The lib subdirectory contains the code for the Mica PPX deriver.
The PPX code is organized as follows:

• ppx_mica.ml: Declares the main Mica PPX deriver

• type_deriver.ml: Derives the definitions of auxiliary data types & the gen_expr Quickcheck generator

• interp_deriver.ml: Derives the Interpret functor

• test_harness_deriver.ml: Derives the TestHarness functor

• overall_deriver.ml: Produces a module called Mica containing all the automatically derived code

• utils.ml: Includes all the following helper modules for convenience:

  • builders.ml: Functions for creating AST nodes

  • getters.ml: Functions for inspecting AST nodes

  • equality.ml: Location-agnostic equality functions for Parsetree types

  • lident.ml: Utilities for working with the Longident type

  • names.ml: Functions for generating fresh variable names & quoting expressions

  • printers.ml: Pretty-printers for AST types + functions for monomorphizing types

  • errors.ml: Functions for error handling (embedding errors as extension nodes in the derived code)

  • inv_ctx.ml: The "inverse typing context", mapping types ty to expressions of type ty

  • let_open.ml: Helpers for producing let open expressions

  • include.ml: Helpers for producing include statements

  • miscellany.ml: Miscellaneous helpers for working with lists & strings

The ancillary mica_tyche_utils repo contains a small library for creating JSON files that are ingested by Tyche.

• Note: the Tyche-Mica integration is still work in progress (contact Ernest Ng for more details).

• For more details about Tyche, we refer the reader to the UIST '24 paper by Goldstein et al.

Differences between the OCaml Workshop & ICFP SRC artifacts

• The OCaml Workshop artifact (2024) includes a version of Mica that has been
  re-implemented from scratch as a PPX deriver (using Ppxlib). This artifact derives code at compile-time and is more feature rich (e.g. is compatible with Tyche).

  • The main branch of this repo currently contains the OCaml Workshop artifact.

• The ICFP SRC artifact (2023) contained a Mica prototype that was implemented as a command-line script. This prototype contained a parser for ML module signatures (written using Angstrom) and pretty-printed the derived PBT code to a new .ml file (using PPrint). This artifact derived code at runtime and is less robust compared to the newer OCaml Workshop artifact.

  • Contact Ernest (ernest@cs.cornell.edu) for access to the (now-deprecated) ICFP '23 SRC artifact.

Notes for Implementors

Testing changes locally

1. test/utils_test contains Alcotest unit tests for various helper functions.

• See the README in utils_test for instructions on how to add new tests to the Alcotest test suite.

1. test/ppx_test contains .ml test files used to test the PPX functionality

• To add a new test file to the corpus of test files, in either ppx_test/passing or ppx_test/errors, run:

$ touch test_file.{ml,expected}; dune runtest --auto-promote

(This automatically generates new Dune stanzas that are needed for the new test files to compile.)

• Then fill in the newly-created .ml and .expected files with the module signature under test (plus relevant PPX annotations), and execute dune runtest. If the test output from Dune looks good, run dune promote to update the .expected file with the contents of the .actual file (which contains what the PPX actually generated from that test run).

Dependencies

• This repo has been tested with OCaml 5.0.0 on an M1 Mac.

• To install all dependencies required for local development, run make install

• We recommend having the following libraries installed:

  • ppxlib

  • ppx_jane

  • ppx_deriving.show

  • base

  • base_quickcheck

  • core

  • core_unix

  • alcotest

• You can also run dune utop to see the output of functions in the codebase in a REPL.