Designing a Theorem Prover, Part 8

As our codebase grows, maintaining clarity and organization becomes more important. It’s time to move beyond inline tests and switch to Alcotest.

Alcotest Link to heading

To use Alcotest, you need to provide a pp function for pretty-printing and an equals function for equality checks. The testable function in Alcotest handles wrapping your type for testing, requiring only these two functions.

(* unification.mli *)

module Env : sig
  (* ... *)
  val pp : Format.formatter -> t -> unit
  (** Prints the env [t] using the format output function [fmt].

      @param fmt The formatter to which the formatted env is output.
      @param t The env to be formatted. *)

  val equal : t -> t -> bool
  (** Returns [true] if two environments are equal. *)
end

To implement pretty-printing we’ll use the Format module. Equality is just an alias for Map.equal Term.equal.

(* unification.ml *)

module Env = struct
  (* ... *)
  let pp fmt env =
    let pp_binding fmt (key, term) =
      Format.fprintf fmt "%s -> %s" key (Term.to_string term)
    in
    let bindings = Map.to_alist env in
    Format.fprintf fmt "{%a}"
      (Format.pp_print_list
         ~pp_sep:(fun fmt () -> Format.fprintf fmt ", ")
         pp_binding)
      bindings

  let equal = Map.equal Term.equal
end

Testsuite Link to heading

We need a a couple of helper functions and testables as well:

(* helpers *)

let pp_error ppf err = Format.pp_print_string ppf err
let error = Alcotest.testable pp_error ( = )

(* testables *)

let term_testable = Alcotest.testable Term.pp Term.equal
let env_testable = Alcotest.testable Env.pp Env.equal

Here is the new testsuite and a few example tests for unification module:

(* unification_test.ml *)

let test_unify_occurs_check_failure () =
  (* equation: P(x) = P(f(x))
     expected: Error "Occurs check failed for variable x" *)
  let env = Env.empty in
  let f1 = Formula.Pred ("P", [ Term.Var "x" ]) in
  let f2 = Formula.Pred ("P", [ Term.Function ("f", [ Term.Var "x" ]) ]) in
  let result_env = unify env (f1, f2) in
  let expected_error = "Occurs check failed for variable x" in
  Alcotest.(check (result env_testable error))
    "unify: occurs check failure" (Error expected_error) result_env

Notice how we test the negative case above ^

(* unification_test.ml *)

let test_unify_unifies_nested_functions () =
  (* equation: P(f(x)) = P(f(g()))
     expected: x -> g() *)
  let env = Env.empty in
  let f1 = Formula.Pred ("P", [ Term.Function ("f", [ Term.Var "x" ]) ]) in
  let f2 =
    Formula.Pred ("P", [ Term.Function ("f", [ Term.Function ("g", []) ]) ])
  in
  let result_env = unify env (f1, f2) in
  let expected_env = Env.add Env.empty ("x", Term.Function ("g", [])) in
  Alcotest.(check (result env_testable error))
    "unify: unifies nested functions" (Ok expected_env) result_env

(* unification_test.ml *)

let test_unify_unifies_nested_functions_with_variables () =
  (* equation: P(f(x, g(y)), z) = P(f(a, g(b)), h(c))
     expected: x -> a, y -> b, z -> h(c) *)
  let env = Env.empty in
  let f1 =
    Formula.Pred
      ( "P",
        [
          Term.Function
            ("f", [ Term.Var "x"; Term.Function ("g", [ Term.Var "y" ]) ]);
          Term.Var "z";
        ] )
  in
  let f2 =
    Formula.Pred
      ( "P",
        [
          Term.Function
            ( "f",
              [
                Term.Param ("a", []);
                Term.Function ("g", [ Term.Param ("b", []) ]);
              ] );
          Term.Function ("h", [ Term.Param ("c", []) ]);
        ] )
  in
  let result_env = unify env (f1, f2) in
  let expected_env =
    let e = Env.empty in
    let e = Env.add e ("x", Term.Param ("a", [])) in
    let e = Env.add e ("y", Term.Param ("b", [])) in
    let e = Env.add e ("z", Term.Function ("h", [ Term.Param ("c", []) ])) in
    e
  in
  Alcotest.(check (result env_testable error))
    "unify: nested function unification with variables" (Ok expected_env)
    result_env

You can find the remaining tests in the repository.
Next time, as we continue through Paulson’s paper, I want to focus on term instantiation and inference.