Module FOTerm

module FOTerm: sig .. end

First-order terms

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.



Term


type t = private InnerTerm.t 
type term = t 
type var = Type.t HVar.t 
Variables are typed with Type.t
type view = private 
| AppBuiltin of Builtin.t * t list
| DB of int (*
Bound variable (De Bruijn index)
*)
| Var of var (*
Term variable
*)
| Const of ID.t (*
Typed constant
*)
| App of t * t list (*
Application to a list of terms (cannot be left-nested)
*)
val view : t -> view
module Classic: sig .. end
Classic view
val subterm : sub:t -> t -> bool
checks whether sub is a (non-strict) subterm of t
include Interfaces.HASH
include Interfaces.ORD
val ty : t -> Type.t
Obtain the type of a term..
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 length
Raises Assert_failure if lists have not the same length

Constructors


val var : var -> t
val var_of_int : ty:Type.t -> int -> t
val bvar : ty:Type.t -> int -> t
Create a bound variable. Providing a type is mandatory. Warning: be careful and try not to use this function directly.
Raises InnerTerm.IllFormedTerm if the index is < 0
val 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
Create a typed constant
val tyapp : t -> Type.t list -> t
Apply a term to types
Raises Type.Error if types do not match.
val app : t -> t list -> t
Apply a term to a list of terms
Raises Type.ApplyError if types do not match.
val app_full : t -> Type.t list -> t list -> t
Apply the term to types, then to terms
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
NOTE: this can break the invariants and make FOTerm.view fail. Only apply with caution.
val of_ty : Type.t -> t
Upcast from type
module VarSet: CCSet.S  with type elt = var
module VarMap: CCMap.S  with type key = var
module VarTbl: CCHashtbl.S  with type key = var

Sequences


module Seq: sig .. end
val var_occurs : var:var -> t -> bool
var_occurs ~var t true iff var in t
val is_ground : t -> bool
is the term ground? (no free vars)
val monomorphic : t -> bool
true if the term contains no type var
val max_var : VarSet.t -> int
find the maximum variable
val min_var : VarSet.t -> int
minimum variable
val add_vars : unit VarTbl.t -> t -> unit
add variables of the term to the set
val vars : t Sequence.t -> VarSet.t
compute variables of the terms
val vars_prefix_order : t -> var list
variables in prefix traversal order
val depth : t -> int
depth of the term
val head : t -> ID.t option
head ID.t
val head_exn : t -> ID.t
head ID.t (or Invalid_argument)
val size : t -> int
Size (number of nodes)
val weight : ?var:int -> ?sym:(ID.t -> int) -> t -> int
Compute the weight of a term, given a weight for variables and one for ID.ts.
Since 0.5.3
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
Set of free type variables

Subterms and Positions


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.

High-level operations


val symbols : ?init:ID.Set.t -> t -> ID.Set.t
Symbols of the term (keys of signature)
val contains_symbol : ID.t -> t -> bool
Does the term contain this given ID.t?

Fold



Fold



High level fold-like combinators
val all_positions : ?vars:bool ->
?ty_args:bool ->
?pos:Position.t -> t -> (t * Position.t) Sequence.t
Iterate on all sub-terms with their position.
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)

Some AC-utils


module type AC_SPEC = sig .. end
module AC (A : AC_SPEC) : sig .. end

Printing/parsing


val print_all_types : bool Pervasives.ref
If true, pp will print the types of all annotated terms
include Interfaces.PRINT
include Interfaces.PRINT_DE_BRUIJN
val add_hook : print_hook -> unit
Hook used by default for printing
val default_hooks : unit -> print_hook list
List of default hooks
val debugf : Format.formatter -> t -> unit
debugf printing, with sorts

Arith


module Arith: sig .. end

TPTP


module TPTP: sig .. end
module Conv: sig .. end