datalog 0.5 · OCaml Package

module StringSymbol : sig ... end

type symbol = string

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

val quantify1 : (term -> 'a) -> 'a

val quantify2 : (term -> term -> 'a) -> 'a

val quantify3 : (term -> term -> term -> 'a) -> 'a

val quantify4 : (term -> term -> term -> term -> 'a) -> 'a

val quantifyn : int -> (term list -> 'a) -> 'a

exception UnsafeClause

type db

type explanation =

| Axiom
| Resolution of clause * literal
| ExtExplanation of string * BottomUp.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

type vartbl = {

mutable vartbl_count : int;
vartbl_tbl : (string, int) Hashtbl.t;

}

val mk_vartbl : unit -> vartbl

val literal_of_ast : ?tbl:vartbl -> BottomUpAst.literal -> literal

val clause_of_ast : BottomUpAst.clause -> clause

val query_of_ast : BottomUpAst.query -> int array * literal list * literal list

package datalog