datalog 0.3.1 · OCaml Package

type symbol = string

type literal

type clause

type soft_lit = symbol * [ `Symbol of symbol | `Var of int ] list

type soft_clause = soft_lit * soft_lit list

type subst

type !'a bind = 'a * int

val mk_literal : symbol -> [< `Symbol of symbol | `Var of int ] list -> literal

val of_soft_lit : soft_lit -> literal

val mk_literal_s : 
  string ->
  [< `Symbol of string | `Var of int ] list ->
  literal

val open_literal : literal -> soft_lit

val mk_clause : literal -> literal list -> clause

val of_soft_clause : soft_clause -> clause

val open_clause : clause -> soft_clause

val is_var : int -> bool

val is_ground : literal -> bool

val arity : literal -> int

val eq_literal : literal -> literal -> bool

val hash_literal : literal -> int

val compare_literal : literal -> literal -> int

val check_safe : clause -> bool

val is_fact : clause -> bool

val compare_clause : clause -> clause -> int

val eq_clause : clause -> clause -> bool

val hash_clause : clause -> int

exception UnifFailure

val empty_subst : subst

val offset : clause -> int

val matching : ?subst:subst -> literal bind -> literal bind -> subst

val unify : ?subst:subst -> literal bind -> literal bind -> subst

val alpha_equiv : ?subst:subst -> literal bind -> literal bind -> subst

val subst_literal : subst -> literal bind -> literal

val subst_clause : subst -> clause bind -> clause

val pp_literal : Format.formatter -> literal -> unit

val pp_clause : Format.formatter -> clause -> unit

val pp_subst : Format.formatter -> subst -> unit

exception UnsafeClause

type db

type explanation =

| Axiom
| Resolution of clause * literal

val db_create : unit -> db

val db_mem : db -> clause -> bool

val db_add : db -> clause -> unit

val db_add_fact : db -> literal -> unit

val db_goal : db -> literal -> unit

val db_match : db -> literal -> (literal bind -> subst -> unit) -> unit

val db_size : db -> int

val db_fold : ('a -> clause -> 'a) -> 'a -> db -> 'a

type fact_handler = literal -> unit

type goal_handler = literal -> unit

val db_subscribe_fact : db -> symbol -> fact_handler -> unit

val db_subscribe_goal : db -> goal_handler -> unit

val db_goals : db -> (literal -> unit) -> unit

val db_explain : db -> literal -> literal list

val db_premises : db -> literal -> clause * literal list

val db_explanations : db -> clause -> explanation list

package datalog