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

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