Demo of OCanren's reifiers without modules

dune

; to build the demo type
; 1) `opam install dune`
; 2) `dune exec ./main.exe`

(executable
  (name main)
  (flags (:standard -rectypes -warn-error -A -w -K-9-27))
)

main.ml

open Printf

(* The `Core` is an interface to logic programming facilities.
 * It is unsafe to expose the content of this module to an end user.
 *)
module Core : sig

  module Var : sig
    type t

    val idx : t -> int
  end

  (* Type `logic` --- either value or variable.
   * Exposing this type is okay.
   *)
  type 'a logic = Value of 'a | Var of Var.t

  (* Type `ilogic` --- (implicit) logic type.
   * (a.k.a `injected` in the current implementation)
   * At runtime `'a ilogic` has the same representation as `'a`.
   * It is unsafe to expose this type to an end user.
   *)
  type 'a ilogic

  val inj : 'a -> 'a ilogic

  (* This exception is raised when the (implicit) logic variable is used outside of its scope
   * (i.g. in the different `run` statement).
   *)
  exception Var_scope_violation of Var.t

  module Env: sig
    (* `'a Env.t` --- essentially a reader monad *)
    type 'a t

    (* Usual boring monadic stuff *)

    val return : 'a -> 'a t

    val fmap : ('a -> 'b) -> 'a t -> 'b t

    val bind : 'a t -> ('a -> 'b t) -> 'b t

  end

  module State : sig
    (* `'a State.t` --- essentially a coreader comonad, dual to '`a Env.t` *)
    type 'a t

    (* Usual comonadic stuff *)

    val extract : 'a t -> 'a

    val extend : 'a t -> ('a t -> 'b) -> 'b t

    (* Interesting part --- we can `observe` implicit logic variable, dipped into our comonad *)
    val observe : 'a ilogic t -> 'a logic

  end

  exception Not_a_value

  module Reifier : sig
    (* Reifier from type `'a` into type `'b` is an `'a -> 'b` function
     * dipped into the `Env.t` monad, will see how it plays later.
     * Perhaps, it is possible to not expose the reifier type and make it itself
     * a monad or something else that composes nicely, but I haven't figured out yet.
     *)
    type ('a, 'b) t = ('a -> 'b) Env.t

    (* Some predefined reifiers from which other reifiers will be composed *)

    (* this one transforms implicit logic value into regular logic value *)
    val reify : ('a ilogic, 'a logic) t

    (* this one projects implicit logic into the underlying type,
     * handling variables with the help of the user provided function
     *)
    val prj : (Var.t -> 'a) -> ('a ilogic, 'a) t

    (* this one projects implicit logic into the underlying type,
     * raising an exception if it finds a variable
     *)
    val prj_exn : ('a ilogic, 'a) t

    (* Interesting part --- we can apply a reifier to a value dipped into `State.t` comonad *)
    val apply : ('a, 'b) t -> 'a State.t -> 'b

    (* composition of two reifiers *)
    val compose : ('a, 'b) t -> ('b, 'c) t -> ('a, 'c) t

    (* Reifier is a profunctor, so we get combinators
     * to compose reifiers with regular functions
     *)

    val fmap : ('b -> 'c) -> ('a, 'b) t -> ('a, 'c) t

    val fcomap : ('a -> 'b) -> ('b, 'c) t -> ('a, 'c) t
  end

  (* Here the usual MiniKanrenish goal-related stuff should be given.
   * For simplicity everything except the `fresh` is omitted.
   *)

  (* The 'real' type of the `fresh` is commented.
   * For testing purposes we use different type.
   *)

  (* val fresh : ('a ilogic -> goal) -> goal *)
  val fresh : ('a ilogic -> 'b Env.t) -> 'b Env.t

  (* The 'real' type of the `run` is commented.
   * For testing purposes we use very simplified run.
   *)

  (* val run : ('a ilogic -> goal) -> 'a ilogic State.t Stream.t *)
  val run : ('a ilogic -> 'b ilogic Env.t) -> 'b ilogic State.t

end = struct

  (* copy-pasted some code from the OCanren *)

  module Anchor : sig
    type t

    val anchor : t

    val is_valid : t -> bool
  end = struct
    type t = int list

    let anchor = [1]

    let is_valid x = (x == anchor)
  end

  type env = int

  module Var = struct
    type t =
      { anchor        : Anchor.t;
        env           : env;
        index         : int;
      }

    let idx { index } = index

    let make ~env index = { env; index; anchor = Anchor.anchor }

    let dummy = make ~env:0 0

  end

  exception Var_scope_violation of Var.t

  module Term : sig
    type 'a t

    val var : env -> 'a t -> Var.t option

    val fresh : env -> 'a t

  end = struct
    type 'a t = Obj.t

    let var_tag, var_size =
      let dummy = Obj.repr Var.dummy in
      Obj.tag dummy, Obj.size dummy

    let is_var env tx sx x =
      if (tx = var_tag) && (sx = var_size) then
        let v = (Obj.obj x : Var.t) in
        let a = v.Var.anchor in
        if (Obj.(is_block @@ repr a)) && (Anchor.is_valid a) then
          (if env = v.Var.env then true else raise (Var_scope_violation v))
        else false
      else false

    let is_box t =
      if (t <= Obj.last_non_constant_constructor_tag) &&
         (t >= Obj.first_non_constant_constructor_tag)
      then true
      else false

    let is_int = (=) Obj.int_tag
    let is_str = (=) Obj.string_tag

    let var env x =
      let x = Obj.repr x in
      let tx = Obj.tag x in
      if is_box tx then
        let sx = Obj.size x in
        if is_var env tx sx x then Some (Obj.magic x) else None
      else None

    let var_cnt = ref 0

    let fresh env =
      let idx = !var_cnt in
      var_cnt := 1 + !var_cnt;
      Obj.magic (Var.make ~env idx)

  end

  type 'a ilogic = 'a Term.t

  external inj : 'a -> 'a ilogic = "%identity"

  type 'a logic = Value of 'a | Var of Var.t

  let observe : env -> 'a ilogic -> 'a logic = fun env t ->
     match Term.var env t with
     | None   -> Value (Obj.magic t)
     | Some v -> Var v

  module Env = struct

    type 'a t = env -> 'a

    let return a = fun _ -> a

    let fmap f r env = f (r env)

    let bind r k env = k (r env) env

  end

  module State = struct

    type 'a t = env * 'a

    let extract (_, a) = a

    let extend (env, a) k = (env, k (env, a))

    let observe (env, a) = observe env a

  end

  exception Not_a_value

  module Reifier = struct

    type ('a, 'b) t = ('a -> 'b) Env.t

    let reify = observe

    let prj k env t =
      match reify env t with
      | Value x -> x
      | Var v   -> k v

    (* can be implemented more efficiently, without allocation of `'a logic`,
     * but for demonstration purposes this implementation is okay
     *)
    let prj_exn env t =
      match reify env t with
      | Value x -> x
      | Var v   -> raise Not_a_value

    let apply r (env, a) = r env a

    let compose r r' env a = r' env (r env a)

    let fmap f r env a = f (r env a)

    let fcomap f r env a = r env (f a)

  end

  let fresh g env = g (Term.fresh env) env

  let env_cnt = ref 0

  let run rel =
    let env = !env_cnt in
    env_cnt := 1 + !env_cnt;
    (env, rel (Term.fresh env) env)

end

open Core

let ret = Env.return

(* test that reifiyng a variable yeilds variable *)
let () =
  match Reifier.(apply reify @@ run (fun v -> ret v)) with
  | Var _   -> printf "Passed\n"
  | Value _ -> failwith "Failed"

(* test that reifiyng a fresh variable yeilds variable *)
let () =
  match Reifier.(apply reify @@ run (fun v -> fresh (fun x -> ret x))) with
  | Var _   -> printf "Passed\n"
  | Value _ -> failwith "Failed"

(* test that reifiyng a value yeilds value *)
let () =
  match Reifier.(apply reify @@ run (fun v -> ret @@ inj 42)) with
  | Value i ->
    if (i = 42) then
      printf "Passed\n"
    else
      failwith "Failed"
  | Var _   -> failwith "Failed"

(* test that runaway variables are handled *)
let () =
  let runaway : int ilogic ref = ref (Obj.magic ()) in
  let _ = run (fun v -> runaway := v; ret v) in
  try
    let _ = Reifier.(apply reify @@ run (fun v -> ret !runaway)) in
    failwith "Failed"
  with
  | Var_scope_violation v -> printf "Passed\n"

(* example of reifiers for custom types *)

module Option = struct

  type 'a t = 'a option

  type 'a ground = 'a t

  type 'a logic = 'a t Core.logic

  type 'a ilogic = 'a t Core.ilogic

  let fmap : ('a -> 'b) -> 'a t -> 'b t = fun f a ->
    match a with
    | Some a -> Some (f a)
    | None   -> None

  let reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t = fun ra ->
    let (>>=) = Env.bind in
    (Reifier.reify >>= (fun r -> (ra >>= (fun fa ->
      Env.return (fun x ->
        match r x with
        | Var v   -> Var v
        | Value t -> Value (fmap fa t)
      )
    ))))

end

(* test reification of the option *)

let () =
  match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret @@ v)) with
  | Var _ -> printf "Passed\n"
  | _ -> failwith "Failed"

let () =
  match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some v)) with
  | Value (Some (Var _)) -> printf "Passed\n"
  | _ -> failwith "Failed"

let () =
  match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some (inj 42))) with
  | Value (Some (Value 42)) -> printf "Passed\n"
  | _ -> failwith "Failed"

(* example of the reifier for the custom recursive type *)

module List = struct

  type ('a, 't) t = Nil | Cons of 'a * 't

  type 'a ground = ('a, 'a ground) t

  type 'a logic = ('a, 'a logic) t Core.logic

  type 'a ilogic = ('a, 'a ilogic) t Core.ilogic

  let fmap : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) t -> ('c, 'd) t = fun f g l ->
    match l with
    | Cons (a, b) -> Cons (f a, g b)
    | Nil         -> Nil

  let rec reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t = fun ra ->
    let (>>=) = Env.bind in
    (* Here the usage of `compose` is essential,
     * the 'monadic' implementation shown below fails with stack overflow due to an infinite recursion
     *)
    Reifier.compose Reifier.reify @@
      (ra >>= (fun fa -> (reify ra >>= (fun fr ->
        Env.return (fun lx ->
          match lx with
          | Var v   -> Var v
          | Value t -> Value (fmap fa fr t)
        )
      ))))

     (*    (Reifier.reify >>= (fun r -> (ra >>= (fun fa -> (reify ra >>= (fun fr ->*)
     (*      Env.return (fun x ->*)
     (*        match r x with*)
     (*        | Var v   -> Var v*)
     (*        | Value t -> Value (fmap fa fr t)*)
     (*      )*)
     (*    ))))))*)

  (* we can build reifier directly into `string`, that is nice *)
  let stringify : ('a, string) Reifier.t -> ('a ilogic, string) Reifier.t = fun sa ->
    let rec show f ll =
      match ll with
      | Var v   -> sprintf "_.%d" @@ Var.idx v
      | Value l ->
        begin match l with
        | Nil         -> "Nil"
        | Cons (a, t) -> sprintf "Cons (%s, %s)" (f a) (show f t)
        end
    in
    Reifier.compose (reify sa) (Env.return @@ show (fun s -> s))

end

(* test reification of the list *)

let () =
  let open List in
  match Reifier.(apply (List.reify reify) @@ run (fun v -> ret @@ v)) with
  | Var _ -> printf "Passed\n"
  | _ -> failwith "Failed"

let () =
  let open List in
  match Reifier.(apply (List.reify reify) @@ run (fun v -> ret @@ inj @@ (Cons (v, inj Nil)))) with
  | Value (Cons (Var _, Value Nil)) -> printf "Passed\n"
  | _ -> failwith "Failed"

let () =
  let open List in
  match Reifier.(apply (List.reify reify) @@ run (fun v -> ret @@ inj @@ (Cons (inj 42, inj Nil)))) with
  | Value (Cons (Value 42, Value Nil)) -> printf "Passed\n"
  | _ -> failwith "Failed"

(* perhaps, we can build `stringifiers` from the smaller pieces,
 * (i.g. by reusing function of type `('a -> string) -> 'a logic -> string`),
 * haven't thought about it a lot
 *)
let stringify : ('a -> string) -> ('a ilogic, string) Reifier.t = fun fs ->
  Reifier.(compose reify @@ Env.return (fun lx ->
    match lx with
    | Var v   -> sprintf "_.%d" @@ Var.idx v
    | Value x -> fs x
  ))

let () =
  let goal =
    let open List in
    run (fun tl -> fresh (fun x -> fresh (fun y ->
      ret @@ inj @@ (Cons (x, inj @@ Cons (inj 42, inj @@ Cons (y, tl))))
    )))
  in
  let s = Reifier.(apply (List.stringify @@ stringify string_of_int)) goal in
  printf "%s\n" s