Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion OCanren-ppx.opam
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,7 @@ homepage: "https://github.com/PLTools/OCanren"
bug-reports: "https://github.com/PLTools/OCanren/issues"
depends: [
"dune" {>= "2.9"}
"ocaml" {>= "4.10"}
"ocaml" {>= "4.14.2"}
"dune-configurator"
"ppxlib" {>= "0.26.0" & <= "0.28.0"}
"ppx_inline_test_nobase"
Expand Down
2 changes: 1 addition & 1 deletion OCanren.opam
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@ homepage: "https://github.com/PLTools/OCanren"
bug-reports: "https://github.com/PLTools/OCanren/issues"
depends: [
"dune" {>= "2.9"}
"ocaml" {>= "4.10"}
"ocaml" {>= "4.14.2"}
"dune-configurator"
"ocamlfind"
"camlp5"
Expand Down
4 changes: 2 additions & 2 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@
"The family of miniKanren derivatives has many implementations. This\none is typed embedding to OCaml. The original implementation for\nthis is in scheme and can be found at https://github.com/michaelballantyne/faster-miniKanren .\n\nFeatures:\n1) disequality constraints\n2) relational standard library: lists, nats\n")
(depends
(ocaml
(>= 4.10))
(>= 4.14.2))
dune-configurator
ocamlfind
camlp5
Expand Down Expand Up @@ -53,7 +53,7 @@
"PPX rewriters for writing relational programs more conveniently.\n\n1) `ppx_fresh` -- a clone of original miniKanren syntax\n\n fresh (x...) goal\n\nexpands into\n\n Fresh.numeral (fun x ... -> goal)\n\n2) `ppx_distrib` for easier generation of type-safe wrappers: distrib functor, etc...\n\n [%%distrib\n type t = fully_abstract_typee\n type ground = ...\n ]\n\n3) `ppx_repr` for test. Expands `REPR(expr)` to `(string_of_expr expr, expr)`\n")
(depends
(ocaml
(>= 4.10))
(>= 4.14.2))
dune-configurator
(ppxlib
(and
Expand Down
1 change: 0 additions & 1 deletion src/core/Core.ml
Original file line number Diff line number Diff line change
Expand Up @@ -154,7 +154,6 @@ module Prunes : sig
type t

val empty : t
(* Returns false when constraints are violated *)
val recheck : t -> Env.t -> Subst.t -> rez
val check_last : t -> Env.t -> Subst.t -> rez
val extend : t -> Term.VarTbl.key -> ('a, 'b) reifier -> 'b cond -> t
Expand Down
4 changes: 2 additions & 2 deletions src/core/Disequality.ml
Original file line number Diff line number Diff line change
Expand Up @@ -178,8 +178,8 @@ module Disjunct :
raise Disequality_fulfilled
| Refined delta -> (
(* When leading terms are reified into something new, we still need to
do whole unification, beacuse other pairs may need walking ---
(we postponed walking, so som einformation may be lost.)
do whole unification, because other pairs may need walking ---
(we postponed walking, so some information may be lost.)
See issue #173
*)
(* log "Refined into: %a" (Format.pp_print_list Subst.Binding.pp) delta; *)
Expand Down
4 changes: 0 additions & 4 deletions src/core/Logic.ml
Original file line number Diff line number Diff line change
Expand Up @@ -87,10 +87,6 @@ module Reifier = struct
let i, cs = Term.Var.reify (reify env) v in
Var (i, cs)

(* can be implemented more efficiently,
* without allocation of `'a logic`,
* but for demonstration purposes this implementation is okay
*)
let prj_exn : ('a ilogic, 'a) t =
fun env t ->
match Term.var t with
Expand Down
6 changes: 4 additions & 2 deletions src/core/Logic.mli
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,9 @@ module Reifier : sig
*)
val prj_exn : ('a ilogic, 'a) t

(* TODO(Kakadu): document this *)
(** [prj onvar] Projects implicit logic into the underlying type,
* handling logic variables with [onvar]
*)
val prj : (int -> 'a) -> ('a ilogic, 'a) t

(* Interesting part --- we can apply a reifier to a value dipped into `State.t` comonad *)
Expand All @@ -82,7 +84,7 @@ module Reifier : sig
(** Fixpoint for reifier. *)
val fix: ( ('a, 'b) t as 'c -> 'c) -> 'c

(** And uxiliary function to make reifiers generated by generic programming point-free. *)
(** An auxiliary function to make reifiers generated by generic programming point-free. *)
val rework : fv:('a Env.m -> 'b Env.m)
-> ('a logic Env.m -> 'b logic Env.m)
-> 'a logic Env.m
Expand Down
1 change: 1 addition & 0 deletions src/core/Subst.mli
Original file line number Diff line number Diff line change
Expand Up @@ -89,6 +89,7 @@ module Answer :
val subsumed : Env.t -> t -> t -> bool
end

(* see [apply] *)
val reify : Env.t -> t -> 'a -> Answer.t

IFDEF STATS THEN
Expand Down
4 changes: 2 additions & 2 deletions tester/tester.mli
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
(** {1 Main} *)

(** In this module you can find convenience functions to speedup your introduction to OCanre.
In realy projects, more likely you will need more low-level interface like {!OCanren.run}. *)
(** In this module you can find convenience functions to speedup your introduction to OCanren.
In real projects, more likely you will need more low-level interface like {!OCanren.run}. *)

(**
The call [run_r reifier to_string count num num_handler ("description", goal)] should be used
Expand Down