sig
module type CONST =
sig
type t
val equal : TopDown.CONST.t -> TopDown.CONST.t -> bool
val hash : TopDown.CONST.t -> int
val to_string : TopDown.CONST.t -> string
val of_string : string -> TopDown.CONST.t
val query : TopDown.CONST.t
end
module type S =
sig
module Const : CONST
type const = Const.t
val set_debug : bool -> unit
module T :
sig
type t = private
Var of int
| Apply of TopDown.S.const * TopDown.S.T.t array
val mk_var : int -> TopDown.S.T.t
val mk_const : TopDown.S.const -> TopDown.S.T.t
val mk_apply :
TopDown.S.const -> TopDown.S.T.t array -> TopDown.S.T.t
val mk_apply_l :
TopDown.S.const -> TopDown.S.T.t list -> TopDown.S.T.t
val is_var : TopDown.S.T.t -> bool
val is_apply : TopDown.S.T.t -> bool
val is_const : TopDown.S.T.t -> bool
val eq : TopDown.S.T.t -> TopDown.S.T.t -> bool
val hash : TopDown.S.T.t -> int
val ground : TopDown.S.T.t -> bool
val vars : TopDown.S.T.t -> int list
val max_var : TopDown.S.T.t -> int
val head_symbol : TopDown.S.T.t -> TopDown.S.const
val to_string : TopDown.S.T.t -> string
val pp : Pervasives.out_channel -> TopDown.S.T.t -> unit
val fmt : Format.formatter -> TopDown.S.T.t -> unit
val pp_tuple : Pervasives.out_channel -> TopDown.S.T.t list -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Lit :
sig
type aggregate = {
left : TopDown.S.T.t;
constructor : TopDown.S.const;
var : TopDown.S.T.t;
guard : TopDown.S.T.t;
}
type t =
LitPos of TopDown.S.T.t
| LitNeg of TopDown.S.T.t
| LitAggr of TopDown.S.Lit.aggregate
val mk_pos : TopDown.S.T.t -> TopDown.S.Lit.t
val mk_neg : TopDown.S.T.t -> TopDown.S.Lit.t
val mk : bool -> TopDown.S.T.t -> TopDown.S.Lit.t
val mk_aggr :
left:TopDown.S.T.t ->
constructor:TopDown.S.const ->
var:TopDown.S.T.t -> guard:TopDown.S.T.t -> TopDown.S.Lit.t
val eq : TopDown.S.Lit.t -> TopDown.S.Lit.t -> bool
val hash : TopDown.S.Lit.t -> int
val to_term : TopDown.S.Lit.t -> TopDown.S.T.t
val fmap :
(TopDown.S.T.t -> TopDown.S.T.t) ->
TopDown.S.Lit.t -> TopDown.S.Lit.t
val to_string : TopDown.S.Lit.t -> string
val pp : Pervasives.out_channel -> TopDown.S.Lit.t -> unit
val fmt : Format.formatter -> TopDown.S.Lit.t -> unit
end
module C :
sig
type t = private {
head : TopDown.S.T.t;
body : TopDown.S.Lit.t list;
}
exception Unsafe
val mk_clause :
TopDown.S.T.t -> TopDown.S.Lit.t list -> TopDown.S.C.t
val mk_fact : TopDown.S.T.t -> TopDown.S.C.t
val eq : TopDown.S.C.t -> TopDown.S.C.t -> bool
val hash : TopDown.S.C.t -> int
val head_symbol : TopDown.S.C.t -> TopDown.S.const
val max_var : TopDown.S.C.t -> int
val fmap :
(TopDown.S.T.t -> TopDown.S.T.t) ->
TopDown.S.C.t -> TopDown.S.C.t
val to_string : TopDown.S.C.t -> string
val pp : Pervasives.out_channel -> TopDown.S.C.t -> unit
val fmt : Format.formatter -> TopDown.S.C.t -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Subst :
sig
type t
type scope = int
type renaming
val empty : TopDown.S.Subst.t
val bind :
TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.Subst.scope ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.Subst.t
val deref :
TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.Subst.scope -> TopDown.S.T.t * TopDown.S.Subst.scope
val create_renaming : unit -> TopDown.S.Subst.renaming
val reset_renaming : TopDown.S.Subst.renaming -> unit
val rename :
renaming:TopDown.S.Subst.renaming ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
val eval :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.T.t -> TopDown.S.Subst.scope -> TopDown.S.T.t
val eval_lit :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.Lit.t -> TopDown.S.Subst.scope -> TopDown.S.Lit.t
val eval_lits :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.Lit.t list ->
TopDown.S.Subst.scope -> TopDown.S.Lit.t list
val eval_clause :
TopDown.S.Subst.t ->
renaming:TopDown.S.Subst.renaming ->
TopDown.S.C.t -> TopDown.S.Subst.scope -> TopDown.S.C.t
end
type scope = TopDown.S.Subst.scope
exception UnifFail
val unify :
?oc:bool ->
?subst:TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.scope ->
TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
val match_ :
?oc:bool ->
?subst:TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.scope ->
TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
val alpha_equiv :
?subst:TopDown.S.Subst.t ->
TopDown.S.T.t ->
TopDown.S.scope ->
TopDown.S.T.t -> TopDown.S.scope -> TopDown.S.Subst.t
val are_alpha_equiv : TopDown.S.T.t -> TopDown.S.T.t -> bool
val clause_are_alpha_equiv : TopDown.S.C.t -> TopDown.S.C.t -> bool
module BuiltinFun :
sig
type t = TopDown.S.T.t -> TopDown.S.T.t option
type map
val create : unit -> TopDown.S.BuiltinFun.map
val add :
TopDown.S.BuiltinFun.map ->
Const.t -> TopDown.S.BuiltinFun.t -> unit
val add_list :
TopDown.S.BuiltinFun.map ->
(Const.t * TopDown.S.BuiltinFun.t) list -> unit
val interpreted : TopDown.S.BuiltinFun.map -> Const.t -> bool
val eval :
TopDown.S.BuiltinFun.map -> TopDown.S.T.t -> TopDown.S.T.t
end
module TVariantTbl :
sig
type key = T.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module CVariantTbl :
sig
type key = C.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module Index :
functor (Data : Hashtbl.HashedType) ->
sig
type t
val empty : unit -> TopDown.S.Index.t
val copy : TopDown.S.Index.t -> TopDown.S.Index.t
val clear : TopDown.S.Index.t -> unit
val add :
TopDown.S.Index.t ->
TopDown.S.T.t -> Data.t -> TopDown.S.Index.t
val remove :
TopDown.S.Index.t ->
TopDown.S.T.t -> Data.t -> TopDown.S.Index.t
val generalizations :
?oc:bool ->
TopDown.S.Index.t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope ->
(Data.t -> TopDown.S.Subst.t -> unit) -> unit
val unify :
?oc:bool ->
TopDown.S.Index.t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope ->
(Data.t -> TopDown.S.Subst.t -> unit) -> unit
val iter :
TopDown.S.Index.t -> (TopDown.S.T.t -> Data.t -> unit) -> unit
val size : TopDown.S.Index.t -> int
end
module Rewriting :
sig
type rule = TopDown.S.T.t * TopDown.S.T.t
type t
val create : unit -> TopDown.S.Rewriting.t
val copy : TopDown.S.Rewriting.t -> TopDown.S.Rewriting.t
val add : TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule -> unit
val add_list :
TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule list -> unit
val to_list :
TopDown.S.Rewriting.t -> TopDown.S.Rewriting.rule list
val rewrite_root :
TopDown.S.Rewriting.t -> TopDown.S.T.t -> TopDown.S.T.t
val rewrite :
TopDown.S.Rewriting.t -> TopDown.S.T.t -> TopDown.S.T.t
end
exception NonStratifiedProgram
module DB :
sig
type t
type interpreter = TopDown.S.T.t -> TopDown.S.C.t list
val create : ?parent:TopDown.S.DB.t -> unit -> TopDown.S.DB.t
val copy : TopDown.S.DB.t -> TopDown.S.DB.t
val clear : TopDown.S.DB.t -> unit
val add_fact : TopDown.S.DB.t -> TopDown.S.T.t -> unit
val add_facts : TopDown.S.DB.t -> TopDown.S.T.t list -> unit
val add_clause : TopDown.S.DB.t -> TopDown.S.C.t -> unit
val add_clauses : TopDown.S.DB.t -> TopDown.S.C.t list -> unit
val interpret :
?help:string ->
TopDown.S.DB.t ->
TopDown.S.const -> TopDown.S.DB.interpreter -> unit
val interpret_list :
TopDown.S.DB.t ->
(TopDown.S.const * string * TopDown.S.DB.interpreter) list ->
unit
val is_interpreted : TopDown.S.DB.t -> TopDown.S.const -> bool
val add_builtin :
TopDown.S.DB.t -> Const.t -> TopDown.S.BuiltinFun.t -> unit
val builtin_funs : TopDown.S.DB.t -> TopDown.S.BuiltinFun.map
val eval : TopDown.S.DB.t -> TopDown.S.T.t -> TopDown.S.T.t
val help : TopDown.S.DB.t -> string list
val num_facts : TopDown.S.DB.t -> int
val num_clauses : TopDown.S.DB.t -> int
val size : TopDown.S.DB.t -> int
val find_facts :
?oc:bool ->
TopDown.S.DB.t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope ->
(TopDown.S.T.t -> TopDown.S.Subst.t -> unit) -> unit
val find_clauses_head :
?oc:bool ->
TopDown.S.DB.t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope ->
(TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
val find_interpretation :
?oc:bool ->
TopDown.S.DB.t ->
TopDown.S.scope ->
TopDown.S.T.t ->
TopDown.S.scope ->
(TopDown.S.C.t -> TopDown.S.Subst.t -> unit) -> unit
end
val ask :
?oc:bool ->
?with_rules:TopDown.S.C.t list ->
?with_facts:TopDown.S.T.t list ->
TopDown.S.DB.t -> TopDown.S.T.t -> TopDown.S.T.t list
val ask_lits :
?oc:bool ->
?with_rules:TopDown.S.C.t list ->
?with_facts:TopDown.S.T.t list ->
TopDown.S.DB.t ->
TopDown.S.T.t list -> TopDown.S.Lit.t list -> TopDown.S.T.t list
end
module Make :
functor (Const : CONST) ->
sig
module Const :
sig
type t = Const.t
val equal : t -> t -> bool
val hash : t -> int
val to_string : t -> string
val of_string : string -> t
val query : t
end
type const = Const.t
val set_debug : bool -> unit
module T :
sig
type t = private Var of int | Apply of const * t array
val mk_var : int -> t
val mk_const : const -> t
val mk_apply : const -> t array -> t
val mk_apply_l : const -> t list -> t
val is_var : t -> bool
val is_apply : t -> bool
val is_const : t -> bool
val eq : t -> t -> bool
val hash : t -> int
val ground : t -> bool
val vars : t -> int list
val max_var : t -> int
val head_symbol : t -> const
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
val pp_tuple : out_channel -> t list -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Lit :
sig
type aggregate = {
left : T.t;
constructor : const;
var : T.t;
guard : T.t;
}
type t = LitPos of T.t | LitNeg of T.t | LitAggr of aggregate
val mk_pos : T.t -> t
val mk_neg : T.t -> t
val mk : bool -> T.t -> t
val mk_aggr :
left:T.t -> constructor:const -> var:T.t -> guard:T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val to_term : t -> T.t
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
end
module C :
sig
type t = private { head : T.t; body : Lit.t list; }
exception Unsafe
val mk_clause : T.t -> Lit.t list -> t
val mk_fact : T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val head_symbol : t -> const
val max_var : t -> int
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Subst :
sig
type t
type scope = int
type renaming
val empty : t
val bind : t -> T.t -> scope -> T.t -> scope -> t
val deref : t -> T.t -> scope -> T.t * scope
val create_renaming : unit -> renaming
val reset_renaming : renaming -> unit
val rename : renaming:renaming -> T.t -> scope -> T.t
val eval : t -> renaming:renaming -> T.t -> scope -> T.t
val eval_lit : t -> renaming:renaming -> Lit.t -> scope -> Lit.t
val eval_lits :
t -> renaming:renaming -> Lit.t list -> scope -> Lit.t list
val eval_clause : t -> renaming:renaming -> C.t -> scope -> C.t
end
type scope = Subst.scope
exception UnifFail
val unify :
?oc:bool ->
?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val match_ :
?oc:bool ->
?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val alpha_equiv :
?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val are_alpha_equiv : T.t -> T.t -> bool
val clause_are_alpha_equiv : C.t -> C.t -> bool
module BuiltinFun :
sig
type t = T.t -> T.t option
type map
val create : unit -> map
val add : map -> Const.t -> t -> unit
val add_list : map -> (Const.t * t) list -> unit
val interpreted : map -> Const.t -> bool
val eval : map -> T.t -> T.t
end
module TVariantTbl :
sig
type key = T.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module CVariantTbl :
sig
type key = C.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module Index :
functor (Data : Hashtbl.HashedType) ->
sig
type t
val empty : unit -> t
val copy : t -> t
val clear : t -> unit
val add : t -> T.t -> Data.t -> t
val remove : t -> T.t -> Data.t -> t
val generalizations :
?oc:bool ->
t ->
scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
val unify :
?oc:bool ->
t ->
scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
val iter : t -> (T.t -> Data.t -> unit) -> unit
val size : t -> int
end
module Rewriting :
sig
type rule = T.t * T.t
type t
val create : unit -> t
val copy : t -> t
val add : t -> rule -> unit
val add_list : t -> rule list -> unit
val to_list : t -> rule list
val rewrite_root : t -> T.t -> T.t
val rewrite : t -> T.t -> T.t
end
exception NonStratifiedProgram
module DB :
sig
type t
type interpreter = T.t -> C.t list
val create : ?parent:t -> unit -> t
val copy : t -> t
val clear : t -> unit
val add_fact : t -> T.t -> unit
val add_facts : t -> T.t list -> unit
val add_clause : t -> C.t -> unit
val add_clauses : t -> C.t list -> unit
val interpret : ?help:string -> t -> const -> interpreter -> unit
val interpret_list :
t -> (const * string * interpreter) list -> unit
val is_interpreted : t -> const -> bool
val add_builtin : t -> Const.t -> BuiltinFun.t -> unit
val builtin_funs : t -> BuiltinFun.map
val eval : t -> T.t -> T.t
val help : t -> string list
val num_facts : t -> int
val num_clauses : t -> int
val size : t -> int
val find_facts :
?oc:bool ->
t -> scope -> T.t -> scope -> (T.t -> Subst.t -> unit) -> unit
val find_clauses_head :
?oc:bool ->
t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
val find_interpretation :
?oc:bool ->
t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
end
val ask :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list -> DB.t -> T.t -> T.t list
val ask_lits :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list -> DB.t -> T.t list -> Lit.t list -> T.t list
end
module type PARSABLE_CONST =
sig
type t
val of_string : string -> TopDown.PARSABLE_CONST.t
val of_int : int -> TopDown.PARSABLE_CONST.t
end
module type PARSE =
sig
type term
type lit
type clause
type name_ctx = (string, TopDown.PARSE.term) Hashtbl.t
val create_ctx : unit -> TopDown.PARSE.name_ctx
val term_of_ast :
ctx:TopDown.PARSE.name_ctx -> TopDownAst.term -> TopDown.PARSE.term
val lit_of_ast :
ctx:TopDown.PARSE.name_ctx -> TopDownAst.literal -> TopDown.PARSE.lit
val clause_of_ast :
?ctx:TopDown.PARSE.name_ctx ->
TopDownAst.clause -> TopDown.PARSE.clause
val clauses_of_ast :
?ctx:TopDown.PARSE.name_ctx ->
TopDownAst.clause list -> TopDown.PARSE.clause list
val parse_chan :
Pervasives.in_channel ->
[ `Error of string | `Ok of TopDown.PARSE.clause list ]
val parse_file :
string -> [ `Error of string | `Ok of TopDown.PARSE.clause list ]
val parse_string :
string -> [ `Error of string | `Ok of TopDown.PARSE.clause list ]
val clause_of_string : string -> TopDown.PARSE.clause
val term_of_string : string -> TopDown.PARSE.term
end
module MakeParse :
functor
(C : PARSABLE_CONST) (TD : sig
module Const :
sig
type t = C.t
val equal : t -> t -> bool
val hash : t -> int
val to_string : t -> string
val of_string : string -> t
val query : t
end
type const = Const.t
val set_debug : bool -> unit
module T :
sig
type t = private
Var of int
| Apply of const * t array
val mk_var : int -> t
val mk_const : const -> t
val mk_apply : const -> t array -> t
val mk_apply_l : const -> t list -> t
val is_var : t -> bool
val is_apply : t -> bool
val is_const : t -> bool
val eq : t -> t -> bool
val hash : t -> int
val ground : t -> bool
val vars : t -> int list
val max_var : t -> int
val head_symbol : t -> const
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt :
Format.formatter -> t -> unit
val pp_tuple :
out_channel -> t list -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add :
'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt :
'a t -> key -> 'a option
val find_all :
'a t -> key -> 'a list
val replace :
'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter :
(key -> 'a -> unit) ->
'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) ->
'a t -> unit
val fold :
(key -> 'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val length : 'a t -> int
val stats :
'a t -> Hashtbl.statistics
end
end
module Lit :
sig
type aggregate = {
left : T.t;
constructor : const;
var : T.t;
guard : T.t;
}
type t =
LitPos of T.t
| LitNeg of T.t
| LitAggr of aggregate
val mk_pos : T.t -> t
val mk_neg : T.t -> t
val mk : bool -> T.t -> t
val mk_aggr :
left:T.t ->
constructor:const ->
var:T.t -> guard:T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val to_term : t -> T.t
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt :
Format.formatter -> t -> unit
end
module C :
sig
type t = private {
head : T.t;
body : Lit.t list;
}
exception Unsafe
val mk_clause : T.t -> Lit.t list -> t
val mk_fact : T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val head_symbol : t -> const
val max_var : t -> int
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt :
Format.formatter -> t -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add :
'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt :
'a t -> key -> 'a option
val find_all :
'a t -> key -> 'a list
val replace :
'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter :
(key -> 'a -> unit) ->
'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) ->
'a t -> unit
val fold :
(key -> 'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val length : 'a t -> int
val stats :
'a t -> Hashtbl.statistics
end
end
module Subst :
sig
type t
type scope = int
type renaming
val empty : t
val bind :
t ->
T.t -> scope -> T.t -> scope -> t
val deref :
t -> T.t -> scope -> T.t * scope
val create_renaming : unit -> renaming
val reset_renaming : renaming -> unit
val rename :
renaming:renaming ->
T.t -> scope -> T.t
val eval :
t ->
renaming:renaming ->
T.t -> scope -> T.t
val eval_lit :
t ->
renaming:renaming ->
Lit.t -> scope -> Lit.t
val eval_lits :
t ->
renaming:renaming ->
Lit.t list -> scope -> Lit.t list
val eval_clause :
t ->
renaming:renaming ->
C.t -> scope -> C.t
end
type scope = Subst.scope
exception UnifFail
val unify :
?oc:bool ->
?subst:Subst.t ->
T.t -> scope -> T.t -> scope -> Subst.t
val match_ :
?oc:bool ->
?subst:Subst.t ->
T.t -> scope -> T.t -> scope -> Subst.t
val alpha_equiv :
?subst:Subst.t ->
T.t -> scope -> T.t -> scope -> Subst.t
val are_alpha_equiv : T.t -> T.t -> bool
val clause_are_alpha_equiv :
C.t -> C.t -> bool
module BuiltinFun :
sig
type t = T.t -> T.t option
type map
val create : unit -> map
val add : map -> Const.t -> t -> unit
val add_list :
map -> (Const.t * t) list -> unit
val interpreted :
map -> Const.t -> bool
val eval : map -> T.t -> T.t
end
module TVariantTbl :
sig
type key = T.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt :
'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace :
'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter :
(key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) ->
'a t -> unit
val fold :
(key -> 'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module CVariantTbl :
sig
type key = C.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt :
'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace :
'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter :
(key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) ->
'a t -> unit
val fold :
(key -> 'a -> 'b -> 'b) ->
'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module Index :
functor (Data : Hashtbl.HashedType) ->
sig
type t
val empty : unit -> t
val copy : t -> t
val clear : t -> unit
val add : t -> T.t -> Data.t -> t
val remove : t -> T.t -> Data.t -> t
val generalizations :
?oc:bool ->
t ->
scope ->
T.t ->
scope ->
(Data.t -> Subst.t -> unit) ->
unit
val unify :
?oc:bool ->
t ->
scope ->
T.t ->
scope ->
(Data.t -> Subst.t -> unit) ->
unit
val iter :
t ->
(T.t -> Data.t -> unit) -> unit
val size : t -> int
end
module Rewriting :
sig
type rule = T.t * T.t
type t
val create : unit -> t
val copy : t -> t
val add : t -> rule -> unit
val add_list : t -> rule list -> unit
val to_list : t -> rule list
val rewrite_root : t -> T.t -> T.t
val rewrite : t -> T.t -> T.t
end
exception NonStratifiedProgram
module DB :
sig
type t
type interpreter = T.t -> C.t list
val create : ?parent:t -> unit -> t
val copy : t -> t
val clear : t -> unit
val add_fact : t -> T.t -> unit
val add_facts : t -> T.t list -> unit
val add_clause : t -> C.t -> unit
val add_clauses :
t -> C.t list -> unit
val interpret :
?help:string ->
t -> const -> interpreter -> unit
val interpret_list :
t ->
(const * string * interpreter) list ->
unit
val is_interpreted :
t -> const -> bool
val add_builtin :
t -> Const.t -> BuiltinFun.t -> unit
val builtin_funs : t -> BuiltinFun.map
val eval : t -> T.t -> T.t
val help : t -> string list
val num_facts : t -> int
val num_clauses : t -> int
val size : t -> int
val find_facts :
?oc:bool ->
t ->
scope ->
T.t ->
scope ->
(T.t -> Subst.t -> unit) -> unit
val find_clauses_head :
?oc:bool ->
t ->
scope ->
T.t ->
scope ->
(C.t -> Subst.t -> unit) -> unit
val find_interpretation :
?oc:bool ->
t ->
scope ->
T.t ->
scope ->
(C.t -> Subst.t -> unit) -> unit
end
val ask :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list ->
DB.t -> T.t -> T.t list
val ask_lits :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list ->
DB.t ->
T.t list -> Lit.t list -> T.t list
end) ->
sig
type term = TD.T.t
type lit = TD.Lit.t
type clause = TD.C.t
type name_ctx = (string, term) Hashtbl.t
val create_ctx : unit -> name_ctx
val term_of_ast : ctx:name_ctx -> TopDownAst.term -> term
val lit_of_ast : ctx:name_ctx -> TopDownAst.literal -> lit
val clause_of_ast : ?ctx:name_ctx -> TopDownAst.clause -> clause
val clauses_of_ast :
?ctx:name_ctx -> TopDownAst.clause list -> clause list
val parse_chan :
in_channel -> [ `Error of string | `Ok of clause list ]
val parse_file : string -> [ `Error of string | `Ok of clause list ]
val parse_string :
string -> [ `Error of string | `Ok of clause list ]
val clause_of_string : string -> clause
val term_of_string : string -> term
end
type const = Int of int | String of string
module Default :
sig
module Const :
sig
type t = const
val equal : t -> t -> bool
val hash : t -> int
val to_string : t -> string
val of_string : string -> t
val query : t
end
type const = Const.t
val set_debug : bool -> unit
module T :
sig
type t = private Var of int | Apply of const * t array
val mk_var : int -> t
val mk_const : const -> t
val mk_apply : const -> t array -> t
val mk_apply_l : const -> t list -> t
val is_var : t -> bool
val is_apply : t -> bool
val is_const : t -> bool
val eq : t -> t -> bool
val hash : t -> int
val ground : t -> bool
val vars : t -> int list
val max_var : t -> int
val head_symbol : t -> const
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
val pp_tuple : out_channel -> t list -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Lit :
sig
type aggregate = {
left : T.t;
constructor : const;
var : T.t;
guard : T.t;
}
type t = LitPos of T.t | LitNeg of T.t | LitAggr of aggregate
val mk_pos : T.t -> t
val mk_neg : T.t -> t
val mk : bool -> T.t -> t
val mk_aggr :
left:T.t -> constructor:const -> var:T.t -> guard:T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val to_term : t -> T.t
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
end
module C :
sig
type t = private { head : T.t; body : Lit.t list; }
exception Unsafe
val mk_clause : T.t -> Lit.t list -> t
val mk_fact : T.t -> t
val eq : t -> t -> bool
val hash : t -> int
val head_symbol : t -> const
val max_var : t -> int
val fmap : (T.t -> T.t) -> t -> t
val to_string : t -> string
val pp : out_channel -> t -> unit
val fmt : Format.formatter -> t -> unit
module Tbl :
sig
type key = t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace :
(key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
end
module Subst :
sig
type t
type scope = int
type renaming
val empty : t
val bind : t -> T.t -> scope -> T.t -> scope -> t
val deref : t -> T.t -> scope -> T.t * scope
val create_renaming : unit -> renaming
val reset_renaming : renaming -> unit
val rename : renaming:renaming -> T.t -> scope -> T.t
val eval : t -> renaming:renaming -> T.t -> scope -> T.t
val eval_lit : t -> renaming:renaming -> Lit.t -> scope -> Lit.t
val eval_lits :
t -> renaming:renaming -> Lit.t list -> scope -> Lit.t list
val eval_clause : t -> renaming:renaming -> C.t -> scope -> C.t
end
type scope = Subst.scope
exception UnifFail
val unify :
?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val match_ :
?oc:bool -> ?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val alpha_equiv :
?subst:Subst.t -> T.t -> scope -> T.t -> scope -> Subst.t
val are_alpha_equiv : T.t -> T.t -> bool
val clause_are_alpha_equiv : C.t -> C.t -> bool
module BuiltinFun :
sig
type t = T.t -> T.t option
type map
val create : unit -> map
val add : map -> Const.t -> t -> unit
val add_list : map -> (Const.t * t) list -> unit
val interpreted : map -> Const.t -> bool
val eval : map -> T.t -> T.t
end
module TVariantTbl :
sig
type key = T.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module CVariantTbl :
sig
type key = C.t
type 'a t
val create : int -> 'a t
val clear : 'a t -> unit
val reset : 'a t -> unit
val copy : 'a t -> 'a t
val add : 'a t -> key -> 'a -> unit
val remove : 'a t -> key -> unit
val find : 'a t -> key -> 'a
val find_opt : 'a t -> key -> 'a option
val find_all : 'a t -> key -> 'a list
val replace : 'a t -> key -> 'a -> unit
val mem : 'a t -> key -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val filter_map_inplace : (key -> 'a -> 'a option) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
end
module Index :
functor (Data : Hashtbl.HashedType) ->
sig
type t
val empty : unit -> t
val copy : t -> t
val clear : t -> unit
val add : t -> T.t -> Data.t -> t
val remove : t -> T.t -> Data.t -> t
val generalizations :
?oc:bool ->
t ->
scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
val unify :
?oc:bool ->
t ->
scope -> T.t -> scope -> (Data.t -> Subst.t -> unit) -> unit
val iter : t -> (T.t -> Data.t -> unit) -> unit
val size : t -> int
end
module Rewriting :
sig
type rule = T.t * T.t
type t
val create : unit -> t
val copy : t -> t
val add : t -> rule -> unit
val add_list : t -> rule list -> unit
val to_list : t -> rule list
val rewrite_root : t -> T.t -> T.t
val rewrite : t -> T.t -> T.t
end
exception NonStratifiedProgram
module DB :
sig
type t
type interpreter = T.t -> C.t list
val create : ?parent:t -> unit -> t
val copy : t -> t
val clear : t -> unit
val add_fact : t -> T.t -> unit
val add_facts : t -> T.t list -> unit
val add_clause : t -> C.t -> unit
val add_clauses : t -> C.t list -> unit
val interpret : ?help:string -> t -> const -> interpreter -> unit
val interpret_list :
t -> (const * string * interpreter) list -> unit
val is_interpreted : t -> const -> bool
val add_builtin : t -> Const.t -> BuiltinFun.t -> unit
val builtin_funs : t -> BuiltinFun.map
val eval : t -> T.t -> T.t
val help : t -> string list
val num_facts : t -> int
val num_clauses : t -> int
val size : t -> int
val find_facts :
?oc:bool ->
t -> scope -> T.t -> scope -> (T.t -> Subst.t -> unit) -> unit
val find_clauses_head :
?oc:bool ->
t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
val find_interpretation :
?oc:bool ->
t -> scope -> T.t -> scope -> (C.t -> Subst.t -> unit) -> unit
end
val ask :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list -> DB.t -> T.t -> T.t list
val ask_lits :
?oc:bool ->
?with_rules:C.t list ->
?with_facts:T.t list -> DB.t -> T.t list -> Lit.t list -> T.t list
val default_interpreters :
(TopDown.const * string * DB.interpreter) list
val builtin : (TopDown.const * BuiltinFun.t) list
val setup_default : DB.t -> unit
type term = T.t
type lit = Lit.t
type clause = C.t
type name_ctx = (string, term) Hashtbl.t
val create_ctx : unit -> name_ctx
val term_of_ast : ctx:name_ctx -> TopDownAst.term -> term
val lit_of_ast : ctx:name_ctx -> TopDownAst.literal -> lit
val clause_of_ast : ?ctx:name_ctx -> TopDownAst.clause -> clause
val clauses_of_ast :
?ctx:name_ctx -> TopDownAst.clause list -> clause list
val parse_chan :
in_channel -> [ `Error of string | `Ok of clause list ]
val parse_file : string -> [ `Error of string | `Ok of clause list ]
val parse_string : string -> [ `Error of string | `Ok of clause list ]
val clause_of_string : string -> clause
val term_of_string : string -> term
end
end