sig
type t = private InnerTerm.t
type term = FOTerm.t
type var = Type.t HVar.t
type view = private
AppBuiltin of Builtin.t * FOTerm.t list
| DB of int
| Var of FOTerm.var
| Const of ID.t
| App of FOTerm.t * FOTerm.t list
val view : FOTerm.t -> FOTerm.view
module Classic :
sig
type view = private
Var of FOTerm.var
| DB of int
| App of ID.t * FOTerm.t list
| AppBuiltin of Builtin.t * FOTerm.t list
| NonFO
val view : FOTerm.t -> FOTerm.Classic.view
end
val subterm : sub:FOTerm.t -> FOTerm.t -> bool
val equal : t -> t -> bool
val hash_fun : t -> CCHash.state -> CCHash.state
val hash : t -> int
val compare : t -> t -> int
val ty : FOTerm.t -> Type.t
module Set :
sig
type elt = t
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_seq : elt CCSet.sequence -> t
val add_seq : t -> elt CCSet.sequence -> t
val to_seq : t -> elt CCSet.sequence
val of_list : elt list -> t
val add_list : t -> elt list -> t
val to_list : t -> elt list
val pp :
?start:string ->
?stop:string -> ?sep:string -> elt CCSet.printer -> t CCSet.printer
val print :
?start:string ->
?stop:string ->
?sep:string -> elt CCSet.formatter -> t CCSet.formatter
end
module Map :
sig
type key = t
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val get : key -> 'a t -> 'a option
val get_or : key -> 'a t -> or_:'a -> 'a
val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
val merge_safe :
f:(key ->
[ `Both of 'a * 'b | `Left of 'a | `Right of 'b ] -> 'c option) ->
'a t -> 'b t -> 'c t
val of_seq : (key * 'a) CCMap.sequence -> 'a t
val add_seq : 'a t -> (key * 'a) CCMap.sequence -> 'a t
val to_seq : 'a t -> (key * 'a) CCMap.sequence
val of_list : (key * 'a) list -> 'a t
val add_list : 'a t -> (key * 'a) list -> 'a t
val keys : 'a t -> key CCMap.sequence
val values : 'a t -> 'a CCMap.sequence
val to_list : 'a t -> (key * 'a) list
val pp :
?start:string ->
?stop:string ->
?arrow:string ->
?sep:string ->
key CCMap.printer -> 'a CCMap.printer -> 'a t CCMap.printer
val print :
?start:string ->
?stop:string ->
?arrow:string ->
?sep:string ->
key CCMap.formatter -> 'a CCMap.formatter -> 'a t CCMap.formatter
end
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_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 fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val get : 'a t -> key -> 'a option
val get_or : 'a t -> key -> or_:'a -> 'a
val add_list : 'a list t -> key -> 'a -> unit
val incr : ?by:int -> int t -> key -> unit
val decr : ?by:int -> int t -> key -> unit
val keys : 'a t -> key CCHashtbl.sequence
val values : 'a t -> 'a CCHashtbl.sequence
val keys_list : 'a t -> key list
val values_list : 'a t -> 'a list
val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
val add_seq_count : int t -> key CCHashtbl.sequence -> unit
val of_seq_count : key CCHashtbl.sequence -> int t
val to_list : 'a t -> (key * 'a) list
val of_list : (key * 'a) list -> 'a t
val update : 'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
val print :
key CCHashtbl.printer ->
'a CCHashtbl.printer -> 'a t CCHashtbl.printer
end
val same_l : FOTerm.t list -> FOTerm.t list -> bool
val var : FOTerm.var -> FOTerm.t
val var_of_int : ty:Type.t -> int -> FOTerm.t
val bvar : ty:Type.t -> int -> FOTerm.t
val builtin : ty:Type.t -> Builtin.t -> FOTerm.t
val app_builtin : ty:Type.t -> Builtin.t -> FOTerm.t list -> FOTerm.t
val const : ty:Type.t -> ID.t -> FOTerm.t
val tyapp : FOTerm.t -> Type.t list -> FOTerm.t
val app : FOTerm.t -> FOTerm.t list -> FOTerm.t
val app_full : FOTerm.t -> Type.t list -> FOTerm.t list -> FOTerm.t
val true_ : FOTerm.t
val false_ : FOTerm.t
val is_var : FOTerm.t -> bool
val is_bvar : FOTerm.t -> bool
val is_app : FOTerm.t -> bool
val is_const : FOTerm.t -> bool
val of_term_unsafe : InnerTerm.t -> FOTerm.t
val of_ty : Type.t -> FOTerm.t
module VarSet :
sig
type elt = var
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_seq : elt CCSet.sequence -> t
val add_seq : t -> elt CCSet.sequence -> t
val to_seq : t -> elt CCSet.sequence
val of_list : elt list -> t
val add_list : t -> elt list -> t
val to_list : t -> elt list
val pp :
?start:string ->
?stop:string -> ?sep:string -> elt CCSet.printer -> t CCSet.printer
val print :
?start:string ->
?stop:string ->
?sep:string -> elt CCSet.formatter -> t CCSet.formatter
end
module VarMap :
sig
type key = var
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
val get : key -> 'a t -> 'a option
val get_or : key -> 'a t -> or_:'a -> 'a
val update : key -> ('a option -> 'a option) -> 'a t -> 'a t
val merge_safe :
f:(key ->
[ `Both of 'a * 'b | `Left of 'a | `Right of 'b ] -> 'c option) ->
'a t -> 'b t -> 'c t
val of_seq : (key * 'a) CCMap.sequence -> 'a t
val add_seq : 'a t -> (key * 'a) CCMap.sequence -> 'a t
val to_seq : 'a t -> (key * 'a) CCMap.sequence
val of_list : (key * 'a) list -> 'a t
val add_list : 'a t -> (key * 'a) list -> 'a t
val keys : 'a t -> key CCMap.sequence
val values : 'a t -> 'a CCMap.sequence
val to_list : 'a t -> (key * 'a) list
val pp :
?start:string ->
?stop:string ->
?arrow:string ->
?sep:string ->
key CCMap.printer -> 'a CCMap.printer -> 'a t CCMap.printer
val print :
?start:string ->
?stop:string ->
?arrow:string ->
?sep:string ->
key CCMap.formatter -> 'a CCMap.formatter -> 'a t CCMap.formatter
end
module VarTbl :
sig
type key = var
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_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 fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val length : 'a t -> int
val stats : 'a t -> Hashtbl.statistics
val get : 'a t -> key -> 'a option
val get_or : 'a t -> key -> or_:'a -> 'a
val add_list : 'a list t -> key -> 'a -> unit
val incr : ?by:int -> int t -> key -> unit
val decr : ?by:int -> int t -> key -> unit
val keys : 'a t -> key CCHashtbl.sequence
val values : 'a t -> 'a CCHashtbl.sequence
val keys_list : 'a t -> key list
val values_list : 'a t -> 'a list
val map_list : (key -> 'a -> 'b) -> 'a t -> 'b list
val to_seq : 'a t -> (key * 'a) CCHashtbl.sequence
val of_seq : (key * 'a) CCHashtbl.sequence -> 'a t
val add_seq : 'a t -> (key * 'a) CCHashtbl.sequence -> unit
val add_seq_count : int t -> key CCHashtbl.sequence -> unit
val of_seq_count : key CCHashtbl.sequence -> int t
val to_list : 'a t -> (key * 'a) list
val of_list : (key * 'a) list -> 'a t
val update : 'a t -> f:(key -> 'a option -> 'a option) -> k:key -> unit
val print :
key CCHashtbl.printer ->
'a CCHashtbl.printer -> 'a t CCHashtbl.printer
end
module Seq :
sig
val vars : FOTerm.t -> FOTerm.var Sequence.t
val subterms : FOTerm.t -> FOTerm.t Sequence.t
val subterms_depth : FOTerm.t -> (FOTerm.t * int) Sequence.t
val symbols : FOTerm.t -> ID.t Sequence.t
val max_var : FOTerm.var Sequence.t -> int
val min_var : FOTerm.var Sequence.t -> int
val ty_vars : FOTerm.t -> FOTerm.var Sequence.t
val typed_symbols : FOTerm.t -> (ID.t * Type.t) Sequence.t
val add_set : FOTerm.Set.t -> FOTerm.t Sequence.t -> FOTerm.Set.t
end
val var_occurs : var:FOTerm.var -> FOTerm.t -> bool
val is_ground : FOTerm.t -> bool
val monomorphic : FOTerm.t -> bool
val max_var : FOTerm.VarSet.t -> int
val min_var : FOTerm.VarSet.t -> int
val add_vars : unit FOTerm.VarTbl.t -> FOTerm.t -> unit
val vars : FOTerm.t Sequence.t -> FOTerm.VarSet.t
val vars_prefix_order : FOTerm.t -> FOTerm.var list
val depth : FOTerm.t -> int
val head : FOTerm.t -> ID.t option
val head_exn : FOTerm.t -> ID.t
val size : FOTerm.t -> int
val weight : ?var:int -> ?sym:(ID.t -> int) -> FOTerm.t -> int
val ty_vars : FOTerm.t -> Type.VarSet.t
module Pos :
sig
val at : FOTerm.t -> Position.t -> FOTerm.t
val replace : FOTerm.t -> Position.t -> by:FOTerm.t -> FOTerm.t
end
val replace : FOTerm.t -> old:FOTerm.t -> by:FOTerm.t -> FOTerm.t
val symbols : ?init:ID.Set.t -> FOTerm.t -> ID.Set.t
val contains_symbol : ID.t -> FOTerm.t -> bool
val all_positions :
?vars:bool ->
?ty_args:bool ->
?pos:Position.t -> FOTerm.t -> (FOTerm.t * Position.t) Sequence.t
module type AC_SPEC =
sig val is_ac : ID.t -> bool val is_comm : ID.t -> bool end
module AC :
functor (A : AC_SPEC) ->
sig
val flatten : ID.t -> FOTerm.t list -> FOTerm.t list
val normal_form : FOTerm.t -> FOTerm.t
val equal : FOTerm.t -> FOTerm.t -> bool
val symbols : FOTerm.t Sequence.t -> ID.Set.t
val seq_symbols : FOTerm.t -> ID.t Sequence.t
end
val print_all_types : bool Pervasives.ref
val pp : t CCFormat.printer
val to_string : t -> string
type print_hook =
int -> t CCFormat.printer -> Format.formatter -> t -> bool
val pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
val add_hook : print_hook -> unit
val default_hooks : unit -> print_hook list
val debugf : Format.formatter -> FOTerm.t -> unit
module Arith :
sig
val floor : FOTerm.t
val ceiling : FOTerm.t
val truncate : FOTerm.t
val round : FOTerm.t
val prec : FOTerm.t
val succ : FOTerm.t
val sum : FOTerm.t
val difference : FOTerm.t
val uminus : FOTerm.t
val product : FOTerm.t
val quotient : FOTerm.t
val quotient_e : FOTerm.t
val quotient_t : FOTerm.t
val quotient_f : FOTerm.t
val remainder_e : FOTerm.t
val remainder_t : FOTerm.t
val remainder_f : FOTerm.t
val less : FOTerm.t
val lesseq : FOTerm.t
val greater : FOTerm.t
val greatereq : FOTerm.t
val pp_hook : print_hook
end
module TPTP :
sig
val pp : t CCFormat.printer
val to_string : t -> string
val pp_depth : ?hooks:print_hook list -> int -> t CCFormat.printer
end
module Conv :
sig
type ctx
val create : unit -> FOTerm.Conv.ctx
val of_simple_term : FOTerm.Conv.ctx -> TypedSTerm.t -> FOTerm.t option
val of_simple_term_exn : FOTerm.Conv.ctx -> TypedSTerm.t -> FOTerm.t
val to_simple_term :
?env:TypedSTerm.t Var.t DBEnv.t -> FOTerm.t -> TypedSTerm.t
end
end