module FOTerm:sig
..end
Those terms provide a first-order presentation of higher-order terms (without functions), in the sense that they make currying possible (as well as applying functions to other terms).
This is as if terms had an `apply` symbol everywhere, but more lightweight.
Types and terms are mixed because it makes application much easier.
typet = private
InnerTerm.t
typeterm =
t
typevar =
Type.t HVar.t
Type.t
type
view = private
| |
AppBuiltin of |
|||
| |
DB of |
(* |
Bound variable (De Bruijn index)
| *) |
| |
Var of |
(* |
Term variable
| *) |
| |
Const of |
(* |
Typed constant
| *) |
| |
App of |
(* |
Application to a list of terms (cannot be left-nested)
| *) |
val view : t -> view
module Classic:sig
..end
val subterm : sub:t -> t -> bool
sub
is a (non-strict) subterm of t
include Interfaces.HASH
include Interfaces.ORD
val ty : t -> Type.t
module Set:CCSet.S
with type elt = t
module Map:CCMap.S
with type key = t
module Tbl:CCHashtbl.S
with type key = t
val same_l : t list -> t list -> bool
same_l l1 l2
returns true
if terms of l1
and l2
are pairwise
equal, false
otherwise.
Precondition: both lists have the same lengthAssert_failure
if lists have not the same lengthval var : var -> t
val var_of_int : ty:Type.t -> int -> t
val bvar : ty:Type.t -> int -> t
InnerTerm.IllFormedTerm
if the index is < 0val builtin : ty:Type.t -> Builtin.t -> t
val app_builtin : ty:Type.t -> Builtin.t -> t list -> t
val const : ty:Type.t -> ID.t -> t
val tyapp : t -> Type.t list -> t
Type.Error
if types do not match.val app : t -> t list -> t
Type.ApplyError
if types do not match.val app_full : t -> Type.t list -> t list -> t
val true_ : t
val false_ : t
val is_var : t -> bool
val is_bvar : t -> bool
val is_app : t -> bool
val is_const : t -> bool
val of_term_unsafe : InnerTerm.t -> t
FOTerm.view
fail. Only
apply with caution.val of_ty : Type.t -> t
module VarSet:CCSet.S
with type elt = var
module VarMap:CCMap.S
with type key = var
module VarTbl:CCHashtbl.S
with type key = var
module Seq:sig
..end
val var_occurs : var:var -> t -> bool
var_occurs ~var t
true iff var
in tval is_ground : t -> bool
val monomorphic : t -> bool
val max_var : VarSet.t -> int
val min_var : VarSet.t -> int
val add_vars : unit VarTbl.t -> t -> unit
val vars : t Sequence.t -> VarSet.t
val vars_prefix_order : t -> var list
val depth : t -> int
val head : t -> ID.t option
val head_exn : t -> ID.t
val size : t -> int
val weight : ?var:int -> ?sym:(ID.t -> int) -> t -> int
var
: unique weight for every variable (default 1)sym
: function from ID.ts to their weight (default const 1
)val ty_vars : t -> Type.VarSet.t
module Pos:sig
..end
val replace : t -> old:t -> by:t -> t
replace t ~old ~by
syntactically replaces all occurrences of old
in t
by the term by
.val symbols : ?init:ID.Set.t -> t -> ID.Set.t
val contains_symbol : ID.t -> t -> bool
val all_positions : ?vars:bool ->
?ty_args:bool ->
?pos:Position.t -> t -> (t * Position.t) Sequence.t
vars
: specifies whether variables are folded on (default false).ty_args
: specifies whether type arguments are folded on (default true).pos
: the initial position (default empty)module type AC_SPEC =sig
..end
module AC(
A
:
AC_SPEC
)
:sig
..end
val print_all_types : bool Pervasives.ref
pp
will print the types of all annotated termsinclude Interfaces.PRINT
include Interfaces.PRINT_DE_BRUIJN
val add_hook : print_hook -> unit
val default_hooks : unit -> print_hook list
val debugf : Format.formatter -> t -> unit
module Arith:sig
..end
module TPTP:sig
..end
module Conv:sig
..end