PPX Syntax extensions

Writing OCanren without syntax extensions

OCanren and original miniKanren consist of many syntax extension. Here we describe how to write relations in OCanren without extension.

This is how we write relation without syntax extensions. The top of the input is techinal stuff for loading right packages into OCaml toplevel. The commands assumes that OCanren is already installed (meaning via opam install OCanren --yes or after git clone and make install). When you will copy-paste the following examples to terminal, omit leading $.

$ ocaml -stdin  -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#rectypes;;

let rec appendo x y xy =
  let open OCanren in
  let open OCanren.Std in
  conde
    [ (x === Std.nil ()) &&& (y === xy)
    ; Fresh.three (fun h tl tmp ->
        (x === h % tl) &&& (appendo tl y tmp) &&& (xy === h % tmp)
      )
    ]

let answers =
  let open OCanren in
  run q (fun xs -> appendo (Std.list inj [1; 2]) (Std.list inj [3; 4]) xs)
    (fun xs -> xs#reify (Std.List.prj_exn OCanren.prj_exn))
  |> Stream.take

let () =
  List.iter (fun xs -> print_endline (GT.show GT.list (GT.show GT.int) xs)) answers
EOF

Now we will use PPX extension to simplify the code. It allows us

• not to think about count of fresh varaibles;

• automatically insert &&& when creating fresh variables.

$ ocaml -stdin  -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#rectypes;;
#require "OCanren-ppx.ppx_fresh";;

let rec appendo x y xy =
  let open OCanren in
  let open OCanren.Std in
  conde
    [ fresh () (x === Std.nil()) (y === xy)
    ; fresh (h tl tmp)
        (x === h % tl)
        (appendo tl y tmp)
        (xy === h % tmp)
    ]

let answers =
  let open OCanren in
  run q (fun xs -> appendo (Std.list inj [1; 2]) (Std.list inj [3; 4]) xs)
    (fun xs -> xs#reify (Std.List.prj_exn OCanren.prj_exn))
  |> Stream.take

let () =
  List.iter (fun xs -> print_endline (GT.show GT.list (GT.show GT.int) xs)) answers
EOF

There is also a camlp5 extension for simplifing relations described here.

PPX syntax extensions

PPX syntax extensions could be used without camlp5. They are able to provide miniKanren-specific syntax for relations, generate types for logic and ground representation for user-defined types, and provide more convenience for testing relations. Camlp5 extension relies on PPX extension for genereation of types. PPX extensions are compilable by make ppx

ppx_repr

An analogue for logger library is called ppx_repr (located at OCanren-ppx.ppx_repr package):

$ ocaml -stdin -impl - <<EOF
#use "topfind";;
#require "OCanren-ppx.ppx_repr";;

let (repr,x) = REPR(1+2);;
let () = Printf.printf "The text expression %S compiles to %d\n" repr x;;
EOF

ppx_fresh

An OCanren-specific syntax extension extension for creating fresh variables. It provides canonical miniKanren syntax similar to the one from Scheme-based miniKanren.

$ ocaml -stdin -dsource -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#require "OCanren-ppx.ppx_repr";;
#require "OCanren-ppx.ppx_fresh";;
#rectypes;;
open OCanren;;
let one_el xs = fresh (x) (xs === Std.(x % nil()));;
let answers =
  run q one_el
    (fun xs -> xs#reify (Std.List.reify OCanren.reify))
  |> Stream.take

let () =
  List.iter
    (fun xs -> print_endline (GT.show Std.List.logic (GT.show OCanren.logic (GT.show GT.int)) xs))
    answers
EOF

It should print a representation of singleton list of a free variable. For example:

[_.11]

ppx_tester

There is OCanren.tester library which simplifies running and printing results of the query. The main function is run_r which takes reifier, pretty-printer, number of expected results, a query and two numerals to support polyvariadic query. Adding these numerals may be cumbersome, so there is a syntax extension which calculates right numeral from the number of lambda-abstration in the passed relation.

You can use the tester library via

$ ocaml -stdin -dsource -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#require "OCanren.tester";;
#require "OCanren-ppx.ppx_repr";;
#require "OCanren-ppx.ppx_tester";;
#require "OCanren-ppx.ppx_fresh";;
#rectypes;;
open OCanren;;
open Tester;;
let _ =
  (* without ppx_tester *)
  run_r OCanren.reify (GT.show OCanren.logic (GT.show GT.int)) 1
    q Tester.qh
    ("<string repr of goal>", (fun q -> q === (inj 1)));;

let _ =
  (* with ppx_tester *)
  [%tester
    run_r OCanren.reify (GT.show OCanren.logic (GT.show GT.int)) 1
      (fun q -> q === (inj 1))];;

EOF

It will print something like

<string repr of goal>, 1 answer {
q=1;
}
fun q -> q === (inj 1), 1 answer {
q=1;
}

ppx_distrib

This extension is used to generate smart constructors and reifier from definition of our type. It optionally allows to decorate type definitions with deriving attributes which could be expanded later.

Below we use extension point with two type definitions. First one is nonrecursive fully abstract type. The extension with generate monadic fmap called fmapt for it. The second one is a specialization of previous type definition for our needs. it is uses to generate types for ground, logic, and injected values; reifier reify and exceptionful projection prj_exn from injected to logic/ground values; and smart constructor for creating values of injected type.

✗ ocaml -stdin -dsource -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#require "OCanren-ppx.ppx_distrib";;
#require "GT.ppx_all";;
#rectypes;;
[%%distrib
  type nonrec 'a t =
    | Z
    | S of 'a
  [@@deriving gt ~options:{ gmap; show }]

  type ground = ground t];;

#show_type t;;
#show_type ground;;
#show_type logic;;
#show reify;;
#show prj_exn;;

EOF

It will output expanded type and value definitions.

type 'a t = Z | S of 'a
type ground = ground t
type logic = logic t OCanren.logic
val reify : (injected, logic) OCanren.Reifier.t
val prj_exn : (injected, ground) OCanren.Reifier.t

ppx_deriving_reify

Simplifies inline generation of reifiers for already known types. With it we can specify a type, and syntax extension will try to build reifier for it. There is a syntax exension in GT, which work similarly.

✗ ocaml -stdin -dsource -impl - <<EOF
#use "topfind";;
#require "OCanren";;
#require "OCanren.tester";;
#require "OCanren-ppx.ppx_deriving_reify";;
#require "GT.ppx_all";;
#rectypes;;
open OCanren;;
open Tester;;
let _ =
  run_r
    [%prj_exn: GT.int OCanren.Std.List.injected]
    ([%show:    GT.int OCanren.Std.List.ground] ())
    1
    q Tester.qh
    ("", (fun q -> q === Std.list inj [1;2;3]));;
EOF

will output

, 1 answer {
q=[1; 2; 3];
}