PBE demo using OCanren

Makefile

.PHONY: all pbe clean

all: pbe

clean:
	rm pbe *.cmi *.cmx *.o

pbe:
	ocamlfind opt -g -rectypes -syntax camlp5o -package ocanren,ocanren.syntax -linkpkg -o pbe pbe.ml

pbe.ml

open Printf

open MiniKanren
open MiniKanren.Std

module T =
  struct
    type 't t =
      | N
      | Add     of 't
      | Mul     of 't

    let fmap ft = function
    | N     -> N
    | Add t -> Add (ft t)
    | Mul t -> Mul (ft t)

    let show st = function
    | N      -> "n"
    | Add t  -> sprintf "n + %s" (st t)
    | Mul t  -> sprintf "n * (%s)" (st t)

  end

module F = Fmap(T)

let n ()  = inj @@ F.distrib @@ T.N
let add t = inj @@ F.distrib @@ T.Add t
let mul t = inj @@ F.distrib @@ T.Mul t

let rec show t = T.show show t

let rec evalo t i o = conde
  [ (t === n ()) &&& (i === o)
  ; fresh (x t')
      (t === add t')
      (Nat.addo i x o)
      (evalo t' i x)
  ; fresh (x t')
      (t === mul t')
      (Nat.mulo i x o)
      (evalo t' i x)
  ]

let pbe exs =
  let goal t = ?& (List.map (fun (i, o) -> evalo t (nat i) (nat o)) exs) in
  run q (fun q -> goal q) (fun q -> q#prj)

(* After running this i got answer: n + n * (n + n) *)
let () =
  let printer t = printf "%s\n" @@ show t in
  let stream = pbe [(0, 0); (1, 3); (2, 10); (3, 21)] in
  List.iter printer @@ Stream.take ~n:1 stream