Index of values

Add a constant term interpretation

add_default term dt adds term as a default case for every sub-case of dt that does not already have a default value

Map the type to its finite domain.

add_list ~subst v t add each binding v_i -> t_i to the subst.

Add the mapping name <=> id to the state.

Add an option to Utils.options_others_

Update the signature with the content of the given statement

Add any statement

Add any statements

Add a value interpretation

app_whnf f l applies f to l, then computes the weak head normal form

apply dt arg returns the sub-tree of dt for when dt's variable is equal to arg.

apply the dt to a list of arguments

Approximation of q under the polarity pol: either

arg_choice ~kind l f picks a CLI option among the string in l, and apply f to the result.

as_ty t returns Some view if is_ty t, repr t = view, and returns None otherwise

Axioms without additional assumptions

Axiom that is part of an admissible (mutual, partial) definition.

Axiom that can be ignored if not explicitely depended upon by the goal

backward f is the identity in the direct way, and the same as f in the way back

bind ~var t binds ref to t.

bind_unfold binder (bind binder x1...xn. t) returns x1...xn, t

bound v is not (can_bind v)

call1 l x is short for iter l ~f:(fun f -> f x)

call2 l x y is short for iter l ~f:(fun f -> f x y)

call_dep t id arg is to be called during term traversal (typically, in dispatch.do_term) to indicate the will of traversing the pair (id,arg)

can_bind t returns true iff t.deref = None

cardinality_ty ty computes the cardinality of the type ty, which must be monomorphic.

cardinality id computes the cardinality of the type named id.

check pipe checks that the features of each component of the pipeline fit with their input.

check t ~spec returns Check_ok if all features required by spec are valid in t, and Check_fail (key, expected, actual) otherwise

check some invariants

check_non_zero env stmt checks that stmt is not a definition of an empty datatype

Check invariants on all the problem's statements

check_statement t st checks that st is well typed and well-formed, and then return a new t that can be used to check subsequent statements

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

close_forall t universally quantifies over free variables of t

Position that spans the two given positions.

N-ary version of Location.combine.

Fast total ordering on values of type t.

Total order based on Var.id

concat s ~into:s2 adds every binding of s into s2

const vars ret is the constant function over vars, that always return ret

convert the statement.

Unsafe version of convert

convert ~env ty converts the raw, unscoped type ty into a type from the representation Ty.t.

Unsafe version of convert

convert ~env ty converts the raw, unscoped type ty into a type from the representation Ty.t.

create a new traversal object.

Create a new environment

Current debug level, with parent inheritance

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

declare a type/function/predicate

Declare a symbol's type (as undefined, for now)

Similar to Env.rec_funs, but only declares the functions, without adding their definition

Decode the given model

Define a new set of mutually recursive (co)data types.

deref ~subst t dereferences t as long as it is a variable bound in subst.

Access the content

For renamings, follow the substitution until we find an unbound var

Convert a term into a decision tree, or emit a warning and return a trivial tree with "unparsable" inside

Empty model

For writing specifications

empty_copy m is a empty model that has the same additional information (such as potentially_spurious) as m

Make a new, empty environment.

Build an environment defining/declaring every symbol of the problem.

Syntactic equality

Name equality (ignores the deref field)

Equality, purely by identifier.

Equality modulo substitution

Used to map IDs to names during printing

Make an error out of an exception, with the stack trace

Eta-reduction at the root of the term.

Applying a substitution

Applying a variable renaming

Eval the tree with the given substitution (which does not capture the tree's variables)

A sprintf implementation for formatters, that calls an exception raising function f

Format version of failwith

filter_map ~test ~yield dt filters the branches of dt using test v lhs on every test v=lhs, and maps the leaves using yield

find_deref_rec ~subst v returns Some (deref_rec subst v') if v is bound, or None otherwise

Safe version of Env.find_ty_exn

Find the type of a symbol

Map each statement to a list of statements, and flatten the result into a new problem

Flatten as an old style flat decision tree

Non recursive fold.

The free type meta-variables in t

Compute the set of free meta variables that can be bound, mapped to their meta-variable

free_vars t computes the set of free variables of t.

Fresh copy each element of the list

fresh_copy v makes a variable that looks like v but has a fresh identifier

fresh_copy v makes a new identifier with the same name as v

Update the type, and make a new variable with it with a fresh ID.

Every feature is on

Full path to the section

fun_unfold (fun x y z. t) = [x;y;z], t.

Generalize a T.t t by parametrizing it over its free type variables.

Specific level of this section, if any

Current debug level for Section.root

Obtain the filename

get_statements t sorts topologically and merges the pieces of statements previously added by push_rec, push_pred, etc.

Number of seconds elapsed between Utils.Time.start_timer and now, or between Utils.Time.start_timer and Utils.Time.stop_timer

get_ty_arg ty n gets the n-th argument of ty, if ty is a function type with at least n arguments.

The goal of the problem

goal pb returns the unique goal of pb, or fails.

Has mark_processed already been called with those arguments?

Hash into a positive integer

Hash function that is not sensitive to alpha-renaming

Search for a head symbol

Id of the variable

ignore_catch f x computes f x, ignores the result, and also ignores any exception raised by f x.

info_of_ty ~env ty finds the information related to the given type.

Unsafe version of info_of_ty

Is the type a quotient over the input types (i.e.

is_closed t means to_seq_free_vars t = empty

spec/rec

Is the type incomplete, that is, some values from the input type are not present in this encoding?

pol = Neg

Pol = NoPol

pol <> NoPol

pol = Pos

rec

Is this warning enabled?

Non recursive iter.

Iterate on callbacks

all registered sections

join a b applies b to every leaf of a, grafting the resulting sub-tree in place of the leaf, using Model.DT_util.apply.

make f creates a new task that will execute f in a separate thread.

Build a problem from statements

Constructor

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

New reference, with a fresh ID

make ~ty ~name makes a new variable with the given name and type.

make_gen ~names creates a new generator of fresh variables whose names follow the naming scheme names (a formatter with one "%d")

printf-ready make function

serialize the whole type into a flat name

Special version of TermInner.UTIL.map' for terms

Map the result

Non recursive polymorphic map, returning a new view.

Similar to Statement.map, but accumulating some value of type b_acc when entering binders

Similar to TermInner.UTIL.map but also keeping the subterm polarity

Apply the substitution to the tree's variables and terms

map_with ~add ~term ~ty pb is similar to map ~term ~ty pb, but after processing each statement st, after () and before() are called, and the statements they return are added respectively before or after the translation of st.

To be used by callbacks in dispatch to indicate that some additional IDs have been processed (e.g.

Safe version of TermInner.UTIL.match_exn

match_exn ~subst2 t1 t2 matches the pattern t1 against subst2 t2.

merge a b concatenates the cases of a and b, merging the common cases recursively, favoring a over b when needed.

n-ary version of Model.DT_util.merge

Invariants: to_ = app id vars snd abstract = of_ -> to_ snd concrete = to_ -> of_

Constructor for Statement.tydef

Use the two positions of lexbufs.

Filter and specialize definitions of the problem.

Should this ID be printed with a "@"?

Parse the next S-expression or return an error if the input isn't long enough or isn't a proper S-expression

expr has no tuples

Transformation that does nothing

Raise an exception saying the given feature is not implemented

Format-based version of Utils.not_implemented

of_flat vars ~tests ~default builds a decision tree on vars, in that order, asssuming tests only range over vars.

of_fut f is similar to Scheduling.Task.make, but f produces a future, not a direct result

of_id ~ty id makes a variable with the given ID

Recover a position from a lexbuf

of_list vars l = add_list ~subst:empty vars l

on_encoded tr ~f registers f to be called on every value obtained by encoding through tr

expr has exactly one tuple

Parse a S-expression from the given channel.

Open the file and read a S-exp from it

Open the file and read a S-exp from it

Parse a string

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component

Pipeline component.

Pipeline component.

Generic Pipe Component

Generic Pipe Component

Generic Pipe Component

Generic Pipe Component

Generic Pipe Component

Generic Pipe Component

Similar to LambdaLift.pipe but with a generic decode function.

Generic Pipe Component

Similar to Skolem.pipe but with a generic decode function.

Obtain polarity of the id

Polarize inductive predicates and possibly some other predicates in the problem.

popen cmd ~f starts a subprocess executing cmd, and calls f with the (stdin,stdout) of the sub-process, in a new thread.

Pretty-printer nice on human eyes (including indentation)

Debug printing

Print with the unique integer ID

print result, not content (i.e.

Print only the name, nothing else

Printer suitable for parsing from the caller

All processed pairs

≥ 1

anything ≥ 0

re-bind an already bound reference (for instance, for path compression).

Add a definition of functions/predicates.

Register a new callback

Remove the callback with given ID

Remove binding for this variable.

Use a hashset to remove duplicates from the list.

remove the first variable, using Model.DT_util.remove_vars.

remove_recursion m transforms definitions such as f x = if x=0 then 0 else if x=1 then f 0 else ... into f x = if x=0 then 0 else if x=1 then 0 else ...

Remove the given variables, using Model.DT_util.merge_l to merge their sub-cases.

rename m performs a renaming of domain constants and bound variables that should be regular and readable.

Same as Subst.rename_var but wraps the renamed var in a term

rename_var subst v returns subst', v' where v' is a fresh copy of v, and subst' = add v v' subst

Rename all variables in dt

reorder vars dt rebalances dt so it has the given order of variables.

repr t returns the view of t as a type.

Present a type-centric view of a term.

View that fails on meta variables

representation that follows the substitution.

Default section, with no parent

run ~j tasks runs the given list of tasks in at most j simultaneous threads, possibly exiting early if a task returns Return_shortcut.

run ~pipe x runs x through the pipe pipe, in a lazy way, and yields values of type 'b along with a conversion function back

Debug level for section (and its descendants)

Set debug level of Section.root

Change the file name used for positions in this lexbuf

Change the type of the variable

Gather the signature of every declared symbol

Number of AST nodes

skolemize ~state pol t returns t', new_syms where t' is the skolemization of t under polarity pol, and new_syms is a set of new symbols with their type

smaller p ~than is true if p is included in than, ie p is a sub-location of than (interval inclusion)

Strong Normal Form (reduce under functions)

expr has at least one tuple

Add a definition of functions/predicates.

time at which the program started

Stop timer, or does nothing if stopped already

to_name state id maps id to a unique name, and remembers the inverse mapping so that of_name state (to_name state id) = id.

Iterate on sub-terms

subterms

IDs occurring as Const

Iterate on free variables.

Iterate on variables

for model display

S-expr output suitable for parsing from the caller

Pure alphanumerical identifier, see https://en.wikipedia.org/wiki/Semantic_URL#Slug

Convert the decision tree to a term

Enable/disable the given warning

time elapsed since start of program

transform a propositional term into a conjunction of condition => term, where each condition is orthogonal to the previous ones

Traverse the given statement, adding its translation to the result, updating the environment, etc.

Cartesian product of given tuples

Compute the type of the given term in the given signature.

Compute type of this term

apply t ~terms ~tys computes the type of f terms for some function f, where f : t and terms : ty.

ty_apply_full ty l is like apply t l, but it returns a pair ty' , subst such that subst ty' = apply t l.

apply t ~tys computes the type of f terms for some function f, where f : t and terms : ty.

Type of the discrimination tree arguments, seen as a function

Same as TermInner.UTIL.ty but unsafe.

type == Kind?

t == Prop?

t == Type?

Type of ty_type

Number of type variables that must be bound in the type.

Propositions

follow forall/arrows to get return type.

t == forall ...

Type of types

ty_unfold ty decomposes ty into a list of quantified type variables, a list of parameters, and a return type (which is not an arrow).

fresh undefined constant

fresh undefined term

Unify the two types, modifying their binding in place.

Unmangles constants that have been collapsed with their type arguments

Unmangle a single term: replace mangled constants by their definition

update k v t sets the key k to v in t.

Update the linked content, if any

Update the type, and make a new variable with it with THE SAME ID.

List of variables decided upon

Observe the structure of the term

Emit the given warning with the associated message

whnf f l applies f to l and returns its WHNF, as a tuple f', l', subst, guard where f l ---> subst ((f guard) l)

Weak Head Normal Form

with_loc ?loc x makes a value with the given location

DT on 0 variables, that returns its argument