datalog 0.4.1 · OCaml Package

type symbol

type term = private

| Var of int
| Const of symbol

val mk_var : int -> term

val mk_const : symbol -> term

type literal

type clause

type soft_lit = symbol * term list

type soft_clause = soft_lit * soft_lit list

val mk_literal : symbol -> term list -> literal

val of_soft_lit : soft_lit -> 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_ground : literal -> bool

val arity : literal -> int

val eq_term : term -> term -> bool

val eq_literal : literal -> literal -> bool

val hash_literal : literal -> int

val check_safe : clause -> bool

val is_fact : clause -> bool

val eq_clause : clause -> clause -> bool

val hash_clause : clause -> int

val pp_term : Format.formatter -> term -> unit

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

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

exception UnsafeClause

type db

type explanation =

| Axiom
| Resolution of clause * literal
| ExtExplanation of string * Univ.t

val db_create : unit -> db

val db_copy : db -> db

val db_mem : db -> clause -> bool

val db_add : ?expl:explanation -> db -> clause -> unit

val db_add_fact : ?expl:explanation -> db -> literal -> unit

val db_goal : db -> literal -> unit

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

val db_query : db -> literal -> int list -> (symbol list -> 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_all_facts : db -> fact_handler -> unit

val db_subscribe_goal : db -> goal_handler -> unit

type user_fun = soft_lit -> soft_lit

val db_add_fun : db -> symbol -> user_fun -> 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

module Query : sig ... end

package datalog