package datalog

  1. Overview
  2. Docs
type symbol = string
type term = private
  1. | Var of int
  2. | 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 : Stdlib.Format.formatter -> term -> unit
val pp_literal : Stdlib.Format.formatter -> literal -> unit
val pp_clause : Stdlib.Format.formatter -> clause -> unit
exception UnsafeClause
type db
type explanation =
  1. | Axiom
  2. | Resolution of clause * literal
  3. | 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
type vartbl = {
  1. mutable vartbl_count : int;
  2. vartbl_tbl : (string, int) Stdlib.Hashtbl.t;
}
val mk_vartbl : unit -> vartbl
val literal_of_ast : ?tbl:vartbl -> Ast.literal -> literal
val clause_of_ast : Ast.clause -> clause
val query_of_ast : Ast.query -> int array * literal list * literal list