Module Rel

module Rel: sig .. end
Relational programming for OCaml.

Rel is a typed, relational, programming language embedded in OCaml.

See the basics.

References.

cd37faa — homepage



Domains


type 'a dom 
The type for domains of values of type 'a.
module Dom: sig .. end
Domains.

Terms


type 'a term 
The type for terms denoting values of type 'a.
val pp_term : Format.formatter -> 'a term -> unit
pp_term ppf t prints an unspecified representation of t on ppf.

Constants


val const : 'a dom -> 'a -> 'a term
const dom v is a term for the constant v in domain dom. Two constants of the same type with different domains never unify.
val unit : unit term
unit is const Dom.unit ().
val bool : bool -> bool term
bool b is const Dom.bool b.
val int : int -> int term
int i is const Dom.int i
val float : float -> float term
float f is const Dom.float f.
val string : string -> string term
string s is const Dom.string s.

Function applications (constructors)

Two terms that represent function applications unify if the functions are physically equal, if each of their argument unifies and if the application's return values are in the same domain.

type 'a ret 
The type for function applications returning values of type 'a.
val pure : 'a -> 'a ret
pure f is the application that yields f itself.
val app : 'a dom -> 'a term -> ('a -> 'b) ret -> 'b ret
app d t ret is the application of term t interpreted in domain d to the function returned by ret.
val ret : 'b dom -> 'b ret -> 'b term
ret d app is a term that interprets the application app in domain d and returns a term representing the function application.

Polymorphic types


val pair : 'a dom ->
'b dom ->
('a * 'b) dom -> 'a term -> 'b term -> ('a * 'b) term
pair dom fst snd is a pair for fst and snd in dom.

Goals


type goal 
The type for goals. In a given state a goal either succeeds or fails.
val fail : goal
fail is a goal that always fails.
val succeed : goal
succeed is a goal that always succeeds.
val (=) : 'a term -> 'a term -> goal
t0 = t1 is a goal that succeeds iff there is a unifier for t0 and t1. The unifier becomes part of the state.
val (||) : goal -> goal -> goal
g0 || g1 is a goal that succeeds if either g0 or g1 succeeds.
val (&&) : goal -> goal -> goal
g0 && g1 is a goal succeeds if both g0 and g1 succeed.
val delay : goal Lazy.t -> goal
delay gazy sees the lazy goal gazy as a goal.
val fresh : ('a term -> goal) -> goal
fresh f is the goal f v with v a fresh logical variable.
module Fresh: sig .. end
Multiple freshness introduction.

Reification


type 'a seq 
The type for (possibly infinite) sequences of values of type 'a.
module Seq: sig .. end
Sequences of values.
type 'a value 
The type for representing the value of a variable of type 'a in a given state.
module Value: sig .. end
Variable values.
type ('q, 'r) reifier 
The type for reifiers. The type 'q is the query to reify, the type 'r is the state reifying function applied on each state.
val reifier : 'q -> 'r -> ('q, 'r) reifier
reifier q f reifies the query q with reifying function f.
val query : ?name:string ->
('a term -> 'q, 'a value -> 'r) reifier -> ('q, 'r) reifier
query ~name r introduces a logical query variable in r's query and binds its value in the state reyifing function. name can be used to name the value.
module Query: sig .. end
Multiple query introduction.
val run : (goal, 'r) reifier -> 'r Seq.t
run r is the sequence of states reified by r's reifying function and obtained by running r's query on the empty state.
val success : goal -> bool
success g is true iff g succeeds on the empty state.

Basics

Fixme explain terms, goals, unification, recursion through delay and reification.

let q x = Rel.(x = int 5)
let xs = Rel.(Seq.to_list @@ run @@ Query.v1 @@ reifier q Value.get1)
let () = assert (xs = [5])

let q x y = Rel.(y = int 6 && (x = y || x = int 5))
let xys = Rel.(Seq.to_list @@ run @@ Query.v2 @@ reifier q Value.get2)
let () = assert (xys = [(6, 6); (5, 6)])

Unifying function applications (constructors)

Represent lists in the term language:

let intl = Rel.Dom.(list int)

let empty = Rel.const intl []
let cons x xs = Rel.(pure List.cons |> app Dom.int x |> app intl xs |> ret intl)

let rec ilist = function [] -> empty | i :: is -> cons (Rel.int i) (ilist is)

Unify lists:

let l x xs = Rel.(cons x xs = ilist [1;2;3]) in
let ls = Rel.(Seq.to_list @@ run @@ Query.v2 @@ reifier q Value.get2)
let () = assert (ls = [(1;[2;3])]

Relational append. Express a predicate appendo l0 l1 l that asserts l is the concatenation of l1 to l0.

let rec appendo l0 l1 l =
  let open Rel in
  (l0 = empty && l1 = l) ||
  (Fresh.v3 @@ fun x xs tl ->
   cons x xs = l0 &&
   cons x tl = l  &&
   delay @@ lazy (appendo xs l1 tl))

Find all lists that appended together give the list [1;2;3]:

let q l0 l1 = appendo l0 l1 (ilist [1;2;3])
let l01s = Rel.(Seq.to_list @@ run @@ Query.v2 @@ reifier q Value.get2)
let () = assert (l01s =
    [([], [1;2;3]);
     ([1],  [2;3]);
     ([1;2],  [3]);
     ([1;2;3], [])])