Index of values

Infix version of Comparison.lexico

Alias to TypedSTerm.Ty.fun_

General function type.

Lexicographic combination starting with the given function

Combination of comparators that work on the same values.

Add one occurrence of the element

Index the given (in)equation

Index the clause

Add several occurrences of the element

Add a print hook that will be used from now on

Hook used by default for printing

Update precedence with symbols

Update the precedence with the given symbols

Add a new command line option

Add new command line options

Update precedence with signature

add variables of the term to the set

Iterate on all sub-terms with their position.

alphabetic ordering on symbols, themselves bigger than builtin

Parametrized type

Apply a term to a list of terms

Apply the term to types, then to terms

app_infer f l computes the type ty of f l, and return app ~ty f l

append s1 s2 is the substitution that maps t to s2 (s1 t).

Append two positions

Apply the substitution to the given term/type.

Apply the substitution to the given term.

Given a function/forall type, and arguments, return the type that results from applying the function/forall to the arguments.

apply1 a b is short for apply a [b].

Same as Substs.SPECIALIZED.apply, but performs no renaming of free variables.

Same as Substs.apply, but performs no renaming of free variables.

Apply the given simple substitution to variables in t; if some variable v is bound to t', then t' can be open and will be shifted as required.

apply_unify f_ty args compute the type of a function of type f_ty, when applied to parameters args.

Similar to Type.apply, but assumes its arguments are well-formed types without more ado.

Arg position at the end

arity ty returns (n,m) where ty = forall x1..xn (a1 ... am -> ret)

decreasing arity constraint (big arity => high in precedence)

Arity of the given symbol, or failure.

Number of arguments the type expects.

arrow l r is the type l -> r.

if id is a constructor of ity, then as_constructor id returns Some (cstor, ity)

Unsafe version of Ind_ty.as_constructor

as_defined_cst id returns Some level if id is a constant defined at stratification level level, None otherwise

Unsafe version of Ind_ty.as_inductive_ty

retrieve subterm at pos

retrieve subterm at pos, or raise Invalid_argument

bind subst v t binds v to t, but fails if v occurs in t (performs an occur-check first)

Add v -> t to the substitution.

Add v -> t to the substitution.

bind_vars ~ty b vars t binds each v in vars with the binder b, with body t, and each intermediate result has type ty (not suitable for functions)

bound variable

Create a bound variable.

Choose ordering by name among registered ones, or

Call a lexicographic combination on arguments

Remove common elements from the multisets.

Number of unique occurrences of elements (the multiplicity of each element is considered)

Number of symbols

Change the type

Chose one element, or

Clear the content of the congruence.

Clear debug level (will be same as parent's)

Bind all free vars with the symbol

Bind all free vars with the symbol

bind free variables

Close all free variables of the term using the binding symbol

closed t is true iff all bound variables of t occur under a binder (i.e.

check whether the term is closed (all DB vars are bound within the term).

Transform the clause into proper CNF; returns a list of statements, including type declarations for new Skolem symbols or formulas proxys.

Codomain (image terms) of substitution

Position that spans the two given positions.

combine two partial comparisons, that are assumed to be compatible, ie they do not order differently if Incomparable is not one of the values.

N-ary version of ParseLocation.combine.

Compare two multisets with the multiset extension of E.compare

Compare two clauses

Total order on equations

Compare two terms using the given ordering

Compare two symbols using the precedence

Compare two multisets with the multiset extension of the given ordering.

Compare two multisets represented as list of elements

compose a b uses a to compare symbols; if a cannot decide, then we use b.

compose_sort l sorts the list by increasing priority (the lower, the earlier an ordering is applied, and therefore the more impact it has) before composing

Constant sort

Create a typed constant

Obtain the constraint

Safe version of TypeInference.constrain_term_term_exn

Force the two terms to have the same type in this context

Safe version of TypeInference.constrain_term_type_exn

Force the term's type and the given type to be the same.

Does t contains the De Bruijn variable of index n?

true iff the term contains at least one subterm with an inductive type

Does the term contain this given ID.t?

Converts statements based on TypedSTerm into statements based on FOTerm and Type

Copy with a new ID

Copy of the context

copy v is similar to v but with a fresh ID

occurrences of ID.t in negative clause

occurrences of ID.t in positive clause

create n makes a new cache of arrays up to length n

New congruence.

New skolem contex.

make a precedence from the given constraints.

New context with a signature and default types.

New generator

Current debug level, with parent inheritance

Checks whether there are cycles in inequalities.

Cheap non-formatting version of Util.debugf

Print a debug message, with the given section and verbosity level.

debugf printing, with sorts

Declare the type of a symbol, possibly shadowing a previous version

Declare the symbol, or

Make the ID satisfy Ind_ty.is_inductive_constant

Change the status of the given precedence

Declare the given inductive type.

default precedence.

List of default hooks

default ordering on terms (RPO6) using default precedence

default precedence on the given sequence of symbols

rename_form ~ctx f returns a new predicate for f, with the free variables of f as arguments.

Depth of the type (length of the longest path to some leaf)

depth of the term

While t is a bound Meta variable, follow its link

deref t s_t dereferences t as long as t is a variable bound in subst

Follow meta-variables links in all subterms

diff s1 s2 contains the symbols of s1 that do not appear in s2.

Difference of multisets.

List of non-trivial strict divisors of the int.

Domain of substitution

dominates f l1 l2 returns true iff for all element y of l2, there is some x in l1 with f x y = Gt

Empty multiset

Empty index

Empty signature

The identity substitution

Empty builder (position=Stop)

Empty environment

Empty index, using the given fingerprint function

Enable/disable profiling

Enter the profiler

Check equality of two multisets

Syntactic equality on terms

Check whether the two precedences are equal (same snapshot)

equal subst t1 s1 t2 s2 returns true iff the two terms are equal under the given substitution, i.e.

Check whether the two terms are AC-equal.

Version of sprintf that adds a colored "error" prefix

error msg raises Error msg

Formatting version of Util.error

Evaluate the term in the given De Bruijn environment, by replacing De Bruijn indices by their value in the environment.

Exit the profiler

Exit the current scope (formula, clause), meaning that all free variables' types are forgotten.

Types expected as function argument by ty.

Number of type parameters expected.

Obtain a representation of the (in)equation.

Build a set of features from the given signature.

Filter out elements that don't satisfy the predicate

Only keep part of the signature

More powerful mapping

finally ~do_ f calls f () and returns its result.

Return the multiplicity of the element within the multiset.

Current representative of this term

Lookup the type of a symbol

Find to which value the given De Bruijn index is bound to, or return None

Lookup the type of a symbol

Lookup variable in substitution.

Unsafe version of DBEnv.find.

replace each element by a multiset in its own

flatten_ac f l flattens the list of terms l by deconstructing all its elements that have f as head ID.t.

Fold on values

fold on occurrences of elements

Fold on elements with their multiplicity

Match the indexed terms against the given query term

Match the query term against the indexed terms

Quantify over one type variable.

Quantify over n type variable.

Return array to the cache.

Just obtain a fresh skolem symbol.

Fresh symbol with a different name

Fresh type variable

Unique ID that will never occur again in this table (modulo 2^63...)

fresh free variable with the given type.

make a new sourced item.

db_from_var t ~var replace var by a De Bruijn symbol in t.

Full path to the section

Generate a new ID with a new, unique name

Specific level of this section, if any

Current debug level for Section.root

New flag from the generator (2*previous flag)

Lookup recursively the var in the substitution, until it is not a variable anymore, or it is not bound.

Hash function on terms

Hashcons the elements

head ID.t

Head symbol, or None if the term is a (bound) variable

head ID.t (or Invalid_argument)

individuals

Safe version of TypeInference.infer_exn.

Convert a clause.

Infer the type of this term under the given signature.

Same as TypeInference.infer_exn but forces the type of its result to be TypedSTerm.prop

infer_statement ctx ~f st checks and convert st into a typed statements, and a list of auxiliary type declarations for symbols that were inferred implicitely.

Infer all statements

Type conversion from TypeInference.untyped.

Type conversion from TypeInference.untyped.

integers

Intersection of multisets (min of multiplicies)

Variables introduced by the substitution (ie vars of codomain)

symbols with high frequency are smaller.

Any arithmetic operator, or constant

Has the symbol a boolean return sort?

true if the symbol is an inductive constructor (zero, successor...)

Is the multiset empty?

Is the substitution empty?

Are there bindings?

Returns true if the two terms are equal in the congruence.

true iff there is no free variable

Only ground types?

Is the type ground? (means that no Var not BVar occurs in it)

is the term ground? (no free vars)

true if the term contains no free variables

An ID whose type is inductive; nothing more

is_inductive_type ty holds iff ty is an instance of some registered type (registered with Ind_ty.declare_ty).

is_infix s returns true if the way the symbol is printed should be used in an infix way if applied to two arguments

Returns true if the first term is strictly lower than the second one in the congruence

Is the given element maximal (ie not dominated by any other element) within the multiset?

true if there are no type variables

is_infix s returns true if the way the symbol is printed should be used in a prefix way if applied to 1 argument

Check whether the substitution is a variable renaming

is_skolem id returns true iff id is a Skolem symbol

is_subterm a ~of_:b is true if a is a subterm of b.

Iterate on distinct occurrences of elements

Iterate on terms that are explicitely present in the congruence.

Iterate on indexed equations

all registered sections

Iterate on elements with their multiplicity

Iterate on the congruence classes' representative elements.

Knuth-Bendix simplification ordering

Same as CCFormat.ksprintf, but without colors

Last comparator

Add left at the end

Lexicographic combination (the second is used only if the first is Incomparable

make cache i x is like Array.make i x, but might return a cached array instead of allocating one.

Makes a fresh ID

Create a new partial order.

Produce of list of options suitable for Arg.parse, that may modify global parameters and the given option reference.

Empty environment of the given size

make ?parent ?inheriting name makes a new section with the given name.

Apply a function to all elements

Map bound objects to other bound objects

Apply a function to all coefficients.

matching ~pattern scope_p b scope_b returns sigma such that sigma pattern = b, or fails.

Call either Unif_intf.S.matching or Unif_intf.S.matching_same_scope depending on whether the given scopes are the same or not.

matches pattern (more general) with the other term.

Maximal elements of the multiset, w.r.t the given ordering.

maximal symbols, in decreasing order

maximal depth of symb in negative clause

maximal depth of symb in positive clause

Maximal elements of a list

Fold on maximal elements

max var

find the maximum variable

Is the element part of the multiset?

Is the element present in this table?

Is the ID.t part of the precedence?

Is the symbol declared?

Check whether the variable is bound by the substitution

mem env i returns true iff find env i returns Some _ rather than None, ie.

Merge two signatures together.

minimal symbols, in decreasing order

min var

minimum variable

Apply miniscoping transformation to the term.

mk_eq congruence t1 t2 asserts that t1 = t2 belongs to the congruence

mk_less congruence t1 t2 asserts that t1 < t2 belongs to the congruence

Create a named profiler

true if the term contains no type var

type of multisets

Name that describes this ordering

negation of literal

All terms are incomparable (equality still works).

normal form of the term modulo AC

convert a nanosecond time to a time in seconds

How many variables are actually bound?

propositions

Take ownership of the given array.

From list of elements with multiplicities.

From immutable array

Recover a position from a lexbuf

Multiset from list

Map indices to objects

Start from a given position

convert a simple typed term into a type.

Make a constant from this string

Parse a $word into a builtin

Make a fresh ID before calling Var.make

NOTE: this can break the invariants and make Type.view fail.

NOTE: this can break the invariants and make FOTerm.view fail.

Conversion from a total order

Upcast from type

open_binder b (b v1 (b v2... (b vn t))) returns [v1,...,vn], t

open_fun ty "unrolls" function arrows from the left, so that open_fun (a -> (b -> (c -> d))) returns [a;b;c], d.

open_poly_fun ty "unrolls" polymorphic function arrows from the left, so that open_fun (forall a b. f a -> (g b -> (c -> d))) returns 2; [f a;g b;c], d.

Opposite of the relation: a R b becomes b R a

Opposite position, when it makes sense (left/right)

Output format

Restore to the previous checkpoint.

Exit a scope, removing the top binding.

pop_many env n calls pop env n times

List of new definitions, that were introduced since the last call to new_definitions.

Remove and return the list of newly created symbols

Obtain the list of symbols whose type has been inferred recently, and reset it.

Run the given command cmd with the given input, wait for it to terminate, and return its stdout.

printer for backtraces, if enabled (print nothing otherwise)

Prints the ID with its internal number

Prints the ID with its internal number colored in gray (better for readability).

With color

hook to print arithmetic expressions

Print a list without begin/end separators

printer for the stack with given depth

Current precedence

Prefix the builder with the given position

If true, pp will print the types of all annotated terms

if enabled, every term will be printed with its unique ID

How "useful" this equation is.

Multiply all multiplicities with the given coefficient

Push a checkpoint on the stack of the congruence.

Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to the given value

Create a new environment, when entering a scope, where the De Bruijn index 0 is bound to nothing.

Call push_none n times (after we've entered n scopes, for instances)

rationals

reals

Build a record with possibly a row variable.

Register a new ordering, which can depend on a precedence.

Un-index the clause

Remove the given binding.

replace t pos ~by replaces the subterm at position pos in t by the term by.

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

replace t|_p by the second term

db_from_term t ~sub replaces sub by a fresh De Bruijn index in t.

replace t ~old ~by syntactically replaces all occurrences of old in t by the term by.

Restore all references to their state at snapshot.

retrieve ~sign (idx,si) (t,st) acc iterates on (in)equations l ?= r of given sign and substitutions subst, such that subst(l, si) = t.

Retrieve clauses that are potentially alpha-equivalent to the given clause

Fold on a set of indexed candidate clauses, that may be subsumed by the given clause

Fold on a set of indexed candidate clauses, that may subsume the given clause.

Reverse the position

Add left at the end

Default section, with no parent

Efficient implementation of RPO (recursive path ordering)

same_l l1 l2 returns true if terms of l1 and l2 are pairwise equal, false otherwise.

Check whether id : ty has an inductive type; if yes, then call Ind_ty.declare_inductive_constant

scan_stmt stmt examines stmt, and, if the statement is a declaration of inductive types or constants, it declares them using Ind_ty.declare_ty or Ind_ty.declare_inductive_constant.

Try and declare defined constants in the given statement

Sequence of AC symbols in this term

Copy the array and modify its copy

set v x is x with the same scope as v

Set the n-th variable to the given objects.

Debug level for section (and its descendants)

Set debug level of Section.root

Used by PRINT.pp...

Change the file name used for positions in this lexbuf

Limit the amount of memory available to the process (in MB)

Limit the CPU time available to the process (in seconds)

Change the weight function of the precedence

shift the non-captured De Bruijn indexes in the term by n

Compute signature when the types are using Type

Single binding

Number of distinct elements.

Number of indexed (in)equations

Number of scopes (number of times DBEnv.push or DBEnv.push_none were called to produce the given environement)

Size of type, in number of "nodes"

Size (number of nodes)

size of negative clause

size of positive clause

skolem_form ~ctx subst ty f returns a term t made of a new symbol applied to the free variables of f that do not occur in subst.

smaller p1 p2 is true if p1 is included in p2, ie p1 is a sub-location of p2 (interval inclusion)

Save current state

Current list of symbols, in increasing order

Number of calls to Congruence.S.push that lead to the current state of the congruence.

time at which the program started

Enable printing of statistics?

Status of the symbol

Subterms

Subterm ordering.

is sub a (strict?) subterm of the other arg?

checks whether sub is a (non-strict) subterm of t

Subterms of the term (possibly empty list)

subterm and variables bound at this subterm

Append position at the end

Sum of multiplicies

sum of depths of symbols

switch_opt b f is an option that, when parsed, will call f b.

switch_set x r is the option that, enabled, calls r := x

Set of ID.ts occurring in the terms, that are AC

Symbols of the term (keys of signature)

The root of the type system.

print the index in the DOT format

print oneself in DOT into the given file

Gather all values into a list

List of elements with their coefficients

Iterate on literals of the clause

Extract current position

Iterate on values

Set of symbols of the signature

convert a type to a prolog term.

Conversion to a total ordering.

time elapsed since start of program, in seconds

Obtain the type of a term..

Type of the term, if any

Same as InnerTerm.ty, but fails if the term has no type

Set of free type variables

Apply a term to types

Compute the types declared in the statement sequence

Unify terms, returns a subst or

unifies destructively the two given terms, by modifying references that occur under Meta.

Union of multisets (max of multiplicies)

unshift n t unshifts the term t's bound variables by n.

Replace immediate subterms by the given list.

Make a fresh variable with a new type and same ID

wildcard

var_occurs ~var t is true iff var occurs in t

var_occurs ~var t true iff var in t

Build a type variable.

Convert a variable (and its type), and remember the binding.

Succeeds iff the first term is a variant of the second, ie if they are alpha-equivalent

List of free variables

compute variables of the terms

variables in prefix traversal order

Add the free variables to the given set

Arith centered view of symbols

Type-centric view of the head of this type.

View on the term's head form

Emit warning

Emit warning, with formatting

Weight of a symbol (for KBO).

Compute the weight of a term, given a weight for variables and one for ID.ts.

Are there some symbols of arity 0 in the signature?

$_ for type inference

Combines AllocCache.Arr.make and AllocCache.Arr.free

Section for all Libzipperposition-related things