Skip to content

Instantly share code, notes, and snippets.

@eupp
Created December 25, 2019 00:13
Show Gist options
  • Save eupp/a78e9fc086834106e98d50e1e7bdea24 to your computer and use it in GitHub Desktop.
Save eupp/a78e9fc086834106e98d50e1e7bdea24 to your computer and use it in GitHub Desktop.
Demo of OCanren's reifiers without modules
; 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))
)
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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment