Demo of OCanren's reifiers without modules

.ocamlformat

dune

; to build the demo type
; 1) `opam install dune`
; 2) `dune runtest -w`

(library
 (name main)
 (modules logic main)
 (inline_tests)
 (flags
  (:standard -rectypes -warn-error -A -w -K-9-27))
 (preprocess
  (pps ppx_inline_test)))

(library
 (name test_reader)
 (modules test_reader)
 (preprocess
  (pps ppx_inline_test))
 (inline_tests))

dune-project

(lang dune 2.8)

logic.ml

include (
  struct
    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

    let make_env =
      let last = ref 0 in
      fun () ->
        incr last;
        !last

    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 fmap_logic f = function Value x -> Value (f x) | Var n -> Var n
  end :
    sig
      module Var : sig
        type t

        val idx : t -> int
      end

      (* 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

      type env

      val make_env : unit -> env

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

      val fmap_logic : ('a -> 'b) -> 'a logic -> 'b logic

      (* 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

      module Term : sig
        type 'a t

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

        val fresh : env -> 'a ilogic
      end
    end)

main.ml

open Printf
open Logic

(* 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 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 *)

  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 _ = 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 : ('a ilogic -> 'b Env.t) -> 'b Env.t =
   fun g env -> g (Obj.magic (Term.fresh env)) env

  let env_cnt = ref 0

  let run : ('a ilogic -> 'b ilogic Env.t) -> 'b ilogic State.t =
   fun rel ->
    let env = Logic.make_env () in
    (env, rel (Term.fresh env) env)
end

open Core

let ret = Env.return

(* test that reifiyng a variable yeilds variable *)
let%test _ =
  match Reifier.(apply reify @@ run (fun v -> ret v)) with
  | Var _ -> true
  | Value _ -> false

(* test that reifiyng a fresh variable yeilds variable *)
let%test _ =
  match Reifier.(apply reify @@ run (fun v -> fresh (fun x -> ret x))) with
  | Var _ -> true
  | Value _ -> false

(* test that reifiyng a value yeilds value *)
let%test _ =
  match Reifier.(apply reify @@ run (fun v -> ret @@ inj 42)) with
  | Value i -> i = 42
  | Var _ -> false

(* test that runaway variables are handled *)
let%test _ =
  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
    false
  with Var_scope_violation v -> true

(* example of reifiers for custom types *)
module TestOption = struct
  module Option = struct
    type 'a t = 'a option

    type 'a ground = 'a t

    type nonrec 'a logic = 'a t logic

    type nonrec 'a ilogic = 'a t 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))

    let prj_exn : 'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t
        =
     fun ra ->
      let ( >>= ) = Env.bind in
      Reifier.prj_exn >>= fun r ->
      ra >>= fun fa -> Env.return (fun x -> fmap fa (r x))
  end

  (* test prjc *)
  let%test _ =
    match
      Reifier.(apply (Option.prj_exn prj_exn) @@ run (fun v -> ret @@ v))
    with
    | exception Not_a_value -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.prj_exn prj_exn)
        @@ run (fun v -> ret @@ inj @@ Some (inj 42)))
    with
    | Some 42 -> true
    | _ -> false

  (* test reification of the option *)

  let%test _ =
    match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret @@ v)) with
    | Var _ -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some v))
    with
    | Value (Some (Var _)) -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.reify reify) @@ run (fun v -> ret @@ inj @@ Some (inj 42)))
    with
    | Value (Some (Value 42)) -> true
    | _ -> false
end

module TestOptionLogicsInside = struct
  module Option = struct
    type 'a t = 'a logic option

    type 'a ground = 'a t

    type nonrec 'a logic = 'a t logic

    type nonrec 'a ilogic = 'a t ilogic

    let fmap : ('a -> 'b) -> 'a t -> 'b t =
     fun f a ->
      match a with Some a -> Some (Logic.fmap_logic 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))

    let prj_exn : 'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t
        =
     fun ra ->
      let ( >>= ) = Env.bind in
      Reifier.prj_exn >>= fun r ->
      ra >>= fun fa -> Env.return (fun x -> fmap fa (r x))
  end

  (* test prjc *)

  let%test _ =
    match
      Reifier.(apply (Option.prj_exn prj_exn) @@ run (fun v -> ret @@ v))
    with
    | exception Not_a_value -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.prj_exn prj_exn)
        @@ run (fun v -> ret @@ inj @@ Some (Value (inj 42))))
    with
    | Some (Value 42) -> true
    | _ -> false

  (* test reification of the option *)

  let%test _ =
    match Reifier.(apply (Option.reify reify) @@ run (fun v -> ret v)) with
    | Var _ -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.reify reify)
        @@ run (fun v -> ret @@ inj @@ Some (Value v)))
    with
    | Value (Some (Value (Var _))) -> true
    | _ -> false

  let%test _ =
    match
      Reifier.(
        apply (Option.reify reify)
        @@ run (fun v -> ret @@ inj @@ Some (Value (inj 42))))
    with
    | Value (Some (Value (Value 42))) -> true
    | _ -> false
end

module TestList = struct
  (* 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 Logic.logic

    type 'a ilogic = ('a, 'a ilogic) t Logic.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 prj_exn :
              'a 'b. ('a, 'b) Reifier.t -> ('a ilogic, 'b ground) Reifier.t =
     fun ra ->
      let ( >>= ) = Env.bind in
      Reifier.compose Reifier.prj_exn
        ( ra >>= fun fa ->
          prj_exn ra >>= fun fr -> Env.return (fun x -> fmap fa fr x) )

    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))
         )

    (*
    let reify : ('a, 'b) Reifier.t -> ('a ilogic, 'b logic) Reifier.t =
     fun ra ->
      let rec helper ra =
        lazy
          (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 ->
                   helper 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 ->
           Lazy.force (helper ra) >>= fun fr ->
           Env.return (fun x ->
               match r x with Var v -> Var v | Value t -> Value (fmap fa fr t))) *)
      in
      Lazy.force helper ra
*)
    (* 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 -> (
            match l with
            | Nil -> "Nil"
            | Cons (a, t) -> sprintf "Cons (%s, %s)" (f a) (show f t))
      in
      Reifier.compose (reify sa) (Env.return @@ show (fun s -> s))
  end

  (* test reification of the list *)

  let%test _ =
    let open List in
    match Reifier.(apply (List.reify reify) @@ run (fun v -> ret @@ v)) with
    | Var _ -> true
    | _ -> false

  let%test _ =
    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)) -> true
    | _ -> false

  let%test _ =
    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)) -> true
    | _ -> false

  (* 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
    print_endline s
end

module TestResult = struct
  module Result = struct
    type ('a, 'b) t = ('a, 'b) Result.t

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

    type ('a, 'b) logic = ('a, 'b) t Logic.logic

    type ('a, 'b) ilogic = ('a, 'b) t Logic.ilogic

    let fmap : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) t -> ('c, 'd) t =
     fun f g l ->
      match l with
      | Result.Ok x -> Result.Ok (f x)
      | Result.Error e -> Result.Error (g e)

    let reify :
          'a 'b 'c 'd.
          ('a, 'c) Reifier.t ->
          ('b, 'd) Reifier.t ->
          (('a, 'b) ilogic, ('c, 'd) logic) Reifier.t =
     fun ra rb ->
      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
       *)
      ra >>= fun fa ->
      rb >>= fun fb ->
      Reifier.reify >>= fun r ->
      Env.return (fun lx ->
          match r lx with Var v -> Var v | Value t -> Value (fmap fa fb t))

    (* we can build reifier directly into `string`, that is nice *)
    let stringify :
        ('a, string) Reifier.t ->
        ('b, string) Reifier.t ->
        (('a, 'b) ilogic, string) Reifier.t =
     fun sa sb ->
      let show f g = function
        | Var v -> sprintf "_.%d" @@ Var.idx v
        | Value l -> (
            match l with
            | Ok e -> sprintf "Ok (%s)" (f e)
            | Error e -> sprintf "Error (%s)" (g e))
      in

      Reifier.compose (reify sa sb)
      @@ Env.return
      @@ show (fun s -> s) (fun s -> s)
  end

  (* test reification of the list *)

  let%test _ =
    let open List in
    match
      Reifier.(apply (Result.reify reify reify) @@ run (fun v -> ret @@ v))
    with
    | Var _ -> true
    | _ -> false

  let%test _ =
    let open List in
    match
      Reifier.(
        apply (Result.reify reify reify) @@ run (fun v -> ret @@ inj @@ Ok v))
    with
    | Value (Ok (Var _)) -> true
    | _ -> false

  let%test _ =
    let open List in
    match
      Reifier.(
        apply (Result.reify reify reify)
        @@ run (fun v -> ret @@ inj @@ Ok (inj 42)))
    with
    | Value (Ok (Value 42)) -> true
    | _ -> false

  (* 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%test _ =
    let goal =
      let open List in
      ret @@ inj @@ Ok (inj 42)
    in
    let s =
      Reifier.(
        apply
          (Result.stringify (stringify string_of_int) (stringify string_of_int)))
        (run (fun v -> goal))
    in
    s = "Ok (42)"
end

module TestHack = struct
  (* example of the reifier for the custom recursive type *)

  module L = struct
    type ('a, 'b, 't) t = Nil | Cons of 'a * 'b * 't

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

    type ('a, 'b) logic = ('a, 'b, ('a, 'b) logic) t Logic.logic

    type ('a, 'b) ilogic = ('a, 'b, ('a, 'b) ilogic) t Logic.ilogic

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

    let rec reify :
              'a 'b 'c 'd.
              ('a, 'b) Reifier.t ->
              ('c, 'd) Reifier.t ->
              (('a, 'c) ilogic, ('b, 'd) logic) Reifier.t =
     fun ra rb ->
      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 ->
           rb >>= fun fb ->
           reify ra rb >>= fun fr ->
           Env.return (fun lx ->
               match lx with
               | Var v -> Var v
               | Value t -> Value (fmap fa fb 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 'b.
          ('a, string) Reifier.t ->
          ('b, string) Reifier.t ->
          (('a, 'b) ilogic, string) Reifier.t =
     fun sa sb ->
      let rec show f g = function
        | Var v -> sprintf "_.%d" @@ Var.idx v
        | Value l -> (
            match l with
            | Nil -> "Nil"
            | Cons (a, b, t) ->
                sprintf "Cons (%s, %s, %s)" (f a) (g b) (show f g t))
      in

      Reifier.compose (reify sa sb)
        (Env.return @@ show (fun s -> s) (fun s -> s))
  end

  (* test reification of the list *)

  let%test _ =
    let open L in
    match Reifier.(apply (L.reify reify reify) @@ run (fun v -> ret @@ v)) with
    | Var _ -> true
    | _ -> false

  let%test _ =
    let open L in
    match
      Reifier.(
        apply (L.reify reify reify)
        @@ run (fun v -> ret @@ inj @@ Cons (v, v, inj Nil)))
    with
    | Value (Cons (Var _, Var _, Value Nil)) -> true
    | _ -> false

  let%test _ =
    let open L in
    match
      Reifier.(
        apply (L.reify reify reify)
        @@ run (fun v -> ret @@ inj @@ Cons (inj 42, inj 42, inj Nil)))
    with
    | Value (Cons (Value 42, Value 42, Value Nil)) -> true
    | _ -> false

  (* 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 L in
      run (fun tl ->
          fresh (fun x ->
              fresh (fun y ->
                  ret @@ inj
                  @@ Cons
                       ( x,
                         x,
                         inj @@ Cons (inj 42, inj 42, inj @@ Cons (y, y, tl)) ))))
    in
    let s =
      Reifier.(
        apply (L.stringify (stringify string_of_int) (stringify string_of_int)))
        goal
    in
    printf "%s\n" s
end

test_reader.ml

open Format

type env = float

[@@@warnerror "-27-32-33"]

[@@@warning "+27+33-32"]

module type READER = sig
  type 'a rez = 'a

  type 'a t = env -> 'a rez

  val ( <*> ) : ('a -> 'b) t -> 'a t -> 'b t

  val pure : 'a -> 'a t

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

  val run : 'a t -> env -> 'a
end

module R1 : READER = struct
  type 'a rez = 'a

  type 'a t = env -> 'a rez

  let pure a _ = a

  let run m e = m e

  let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
   fun r f env ->
    printf "Applying (r env)\n%!";
    let u = r env in
    f u

  let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t = fun r k env -> k (r env) env

  let ( >>= ) = bind

  let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
   fun foo arg env -> foo env (arg env)

  module Syntax = struct
    let ( let* ) = bind

    let ( let+ ) = fmap
  end
end

(*
module R2 : READER = struct
  type 'a rez = unit -> 'a

  type 'a t = env -> 'a rez

  let return : 'a. 'a -> 'a t = fun a _ () -> a

  let pure = return

  let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
   fun r f env ->
    printf "Applying (r env)\n%!";
    let u = r env in
    fun () -> f (u ())

  let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
   fun r k env ->
    let u = r env in
    fun () -> k (u ()) env ()

  let ( >>= ) = bind

  let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
   fun foo arg env ->
    let x = arg env in
    fun () -> foo env () (x ())

  let run m env = m env ()
end
 *)
module Test (Reader : READER) : sig
  type ('a, 'b) t

  val fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t

  val ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t

  val pure : ('a -> 'b) -> ('a, 'b) t

  val apply : ('a, 'b) t -> env -> 'a -> 'b
end = struct
  type ('a, 'b) t = ('a -> 'b) Reader.t

  let rec fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t =
   fun f env v -> f (fix f) env v

  (* let fix f =
     let rec p = lazy (f r) and r buf = (Lazy.force p) buf in
     r *)

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

  let ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t =
   fun f arg -> Reader.(pure (fun f x -> f x) <*> f <*> arg)

  let pure f = Reader.pure f

  let simple : (int, string) t = Reader.pure string_of_int

  let apply : 'a 'b. ('a, 'b) t -> env -> 'a -> 'b =
   fun r env -> Reader.run r env
end

module _ = struct
  module R = Test (R1)

  (* Stack overflow *)
  let%test _ =
    let foo =
      R.fix (fun self ->
          let open R in
          pure (fun _rself -> string_of_int) <*> self)
    in
    R.apply foo 42. 112 = "112"
end
(*
module _ = struct
  module R = Test (R2)

  (* Stack overflow AGAIN  *)
  let%test _ =
    let foo =
      R.fix (fun self ->
          let open R in
          pure (fun _rself -> string_of_int) <*> self)
    in
    R.apply foo 42. 112 = "112"

  let%test _ =
    let rec foo =
      lazy
        (let open R in
        pure (fun _rself -> string_of_int) <*> Lazy.force foo)
    in
    R.apply (Lazy.force foo) 42. 112 = "112"
end *)
(*
let%test _ =
  let foo =
    R.fix (fun self ->
        let open Reader.Syntax in
        let+ rself = self in
        string_of_int)
  in
  R.apply foo 42.0 112 = "112" *)

(*
module Test2 (Reader : READER) : sig
  type ('a, 'b) t

  val fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t

  val ( <*> ) : ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t

  val pure : ('a -> 'b) -> ('a, 'b) t

  val apply : ('a, 'b) t -> env -> 'a -> 'b
end = struct
  type ('a, 'b) t = 'a -> 'b Reader.t

  let rec fix : (('a, 'b) t -> ('a, 'b) t) -> ('a, 'b) t =
   fun f eta -> f (fix f) eta

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

  let ( <*> ) : 'a 'b 'c 'd. ('a -> 'b, 'c -> 'd) t -> ('a, 'b) t -> ('c, 'd) t
      =
   (* (('a -> 'b) -> env -> 'c -> 'd) -> ('a -> env  -> 'b) -> ('c -> env -> 'd) *)
   fun f arg : ('c, 'd) t ->
    fun (a : 'a) ->
     let (_ : ('a, 'b) t) = arg in
     let open Reader in
     arg a >>= fun b ->
     f a b >>= fun c -> return c

  (* f (fun x -> Reader.run (arg x) env) env *)
  (* Reader.(pure (fun f x -> f x) <*> f x <*> arg ) *)

  let pure f = Reader.pure f

  let simple : (int, string) t = Reader.pure string_of_int

  let apply : 'a 'b. ('a, 'b) t -> env -> 'a -> 'b =
   fun r env -> Reader.run r env
end
*)

(*
let%test _ =
  let foo =
    R.fix (fun self ->
        let open Reader.Syntax in
        let* rself = self in
        (* This line casuses stack overflow *)
        R.simple)
  in
  R.apply foo 42. 112 = "112"
   *)
(*
module R3 : READER = struct
  type 'a rez = unit -> 'a

  type 'a t = env -> 'a rez

  let return : 'a. 'a -> 'a t = fun a _ () -> a

  let pure = return

  let fmap : 'a 'b. 'a t -> ('a -> 'b) -> 'b t =
   fun r f env ->
    printf "Applying (r env)\n%!";
    let u = r env in
    fun () -> f (u ())

  let bind : 'a 'b. 'a t -> ('a -> 'b t) -> 'b t =
   fun r k env ->
    let u = r env in
    fun () -> k (u ()) env ()

  let ( >>= ) = bind

  let ( <*> ) : 'a 'b. ('a -> 'b) t -> 'a t -> 'b t =
   fun foo arg env ->
    let x = arg env in
    fun () -> foo env () (x ())

  let run m env = m env ()
end
 *)