Module type TermInner.UTIL

module type UTIL = sig .. end

include TermInner.UTIL_REPR

val build : t_ TermInner.view -> t_

val const : TermInner.id -> t_

val builtin : t_ TermInner.Builtin.t -> t_

val app_builtin : t_ TermInner.Builtin.t -> t_ list -> t_

val var : t_ TermInner.var -> t_

val app : t_ -> t_ list -> t_

val app_const : ID.t -> t_ list -> t_

val fun_ : t_ TermInner.var -> t_ -> t_

val mu : t_ TermInner.var -> t_ -> t_

val let_ : t_ TermInner.var -> t_ -> t_ -> t_

val match_with : t_ -> t_ TermInner.cases -> t_

val ite : t_ -> t_ -> t_ -> t_

val forall : t_ TermInner.var -> t_ -> t_

val exists : t_ TermInner.var -> t_ -> t_

val eq : t_ -> t_ -> t_

val neq : t_ -> t_ -> t_

val imply : t_ -> t_ -> t_

val imply_l : t_ list -> t_ -> t_

val true_ : t_

val false_ : t_

val and_ : t_ list -> t_

val or_ : t_ list -> t_

val not_ : t_ -> t_

val undefined_self : t_ -> t_

fresh undefined term

val undefined_atom : ty:t_ -> t_

fresh undefined constant

val data_test : ID.t -> t_ -> t_

val data_select : ID.t -> int -> t_ -> t_

val unparsable : ty:t_ -> t_

val and_nodup : t_ list -> t_

val asserting : t_ -> t_ list -> t_

val assuming : t_ -> t_ list -> t_

val guard : t_ -> t_ TermInner.Builtin.guard -> t_

val mk_bind : TermInner.Binder.t -> t_ TermInner.var -> t_ -> t_

val mk_bind_l : TermInner.Binder.t -> t_ TermInner.var list -> t_ -> t_

val ty_type : t_

Type of types

val ty_kind : t_

Type of ty_type

val ty_prop : t_

Propositions

val ty_unitype : t_

val ty_builtin : TermInner.TyBuiltin.t -> t_

val ty_const : TermInner.id -> t_

val ty_app : t_ -> t_ list -> t_

val ty_arrow : t_ -> t_ -> t_

val ty_arrow_l : t_ list -> t_ -> t_

val ty_var : t_ TermInner.var -> t_

val ty_meta : t_ MetaVar.t -> t_

val ty_forall : t_ TermInner.var -> t_ -> t_

val fun_l : t_ TermInner.var list -> t_ -> t_

val forall_l : t_ TermInner.var list -> t_ -> t_

val exists_l : t_ TermInner.var list -> t_ -> t_

val ty_forall_l : t_ TermInner.var list -> t_ -> t_

val let_l : (t_ TermInner.var * t_) list -> t_ -> t_

val close_forall : t_ -> t_

close_forall t universally quantifies over free variables of t

val hash_fun : t_ CCHash.hash_fun

val hash : t_ -> int

Hash into a positive integer

val hash_fun_alpha_eq : t_ CCHash.hash_fun

val hash_alpha_eq : t_ -> int

Hash function that is not sensitive to alpha-renaming

val equal : t_ -> t_ -> bool

Syntactic equality

Misc

module Tbl: CCHashtbl.S  with type key = t_

Hashtbl with terms as key.

module Map: CCMap.S  with type key = t_

Map with terms as key.

val remove_dup : t_ list -> t_ list

Use a hashset to remove duplicates from the list. Order is not preserved.

Traversal

val fold : f:('acc -> 'b_acc -> t_ -> 'acc) ->
       bind:('b_acc -> t_ Var.t -> 'b_acc) -> 'acc -> 'b_acc -> t_ -> 'acc

Non recursive fold.

f : used to update the regular accumulator (that is returned)

bind : updates the binding accumulator with the bound variable

val iter : f:('b_acc -> t_ -> unit) ->
       bind:('b_acc -> t_ Var.t -> 'b_acc) -> 'b_acc -> t_ -> unit

Non recursive iter.

f : called on immediate subterms and on the regular accumulator

bind : updates the binding accumulator with the bound variable

val map' : f:('b_acc -> t_ -> 'a) ->
       bind:('b_acc -> t_ Var.t -> 'b_acc * 'a Var.t) ->
       'b_acc -> t_ -> 'a TermInner.view

Non recursive polymorphic map, returning a new view. Combine with T.build in the special case of terms.

f : maps a term to a term

bind : updates the binding accumulator and returns a new variable

val map : f:('b_acc -> t_ -> t_) ->
       bind:('b_acc -> t_ Var.t -> 'b_acc * t_ Var.t) -> 'b_acc -> t_ -> t_

Special version of TermInner.UTIL.map' for terms

val map_pol : f:('b_acc -> Polarity.t -> t_ -> t_) ->
       bind:('b_acc -> t_ Var.t -> 'b_acc * t_ Var.t) ->
       'b_acc -> Polarity.t -> t_ -> t_

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

val approx_infinite_quant_pol : [ `Eq | `Exists | `Forall ] ->
       Polarity.t -> [ `Keep | `Unsat_means_unknown of t_ ]

Approximation of q under the polarity pol: either

`Unsat_means_unknown replacement means that we lost completeness, and should return replacement instead
`Keep means to keep the quantifier as is

val size : t_ -> int

Number of AST nodes

Substitution Utils

type subst = (t_, t_) Var.Subst.t

type renaming = (t_, t_ Var.t) Var.Subst.t

val equal_with : subst:subst -> t_ -> t_ -> bool

Equality modulo substitution

val deref : subst:subst -> t_ -> t_

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

val rename_var : subst -> t_ Var.t -> subst * t_ Var.t

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

type apply_error = {

	`ae_msg : string;`
	`ae_term : t_ option;`
	`ae_ty : t_;`
	`ae_args : t_ list;`
	`ae_args_ty : t_ list;`
	`ae_subst : subst;`

}

exception ApplyError of apply_error

Raised when a type application fails

val eval : ?rec_:bool -> subst:subst -> t_ -> t_

Applying a substitution

rec_ : if true, when replacing v with t because (v -> t) in subst, we call eval subst t instead of assuming t is preserved by subst (default false)

val eval_renaming : subst:renaming -> t_ -> t_

Applying a variable renaming

val renaming_to_subst : renaming -> subst

val ty_apply : t_ -> terms:t_ list -> tys:t_ list -> t_

apply t ~terms ~tys computes the type of f terms for some function f, where f : t and terms : ty.
Raises ApplyError if the arguments do not match

val ty_apply_full : t_ -> terms:t_ list -> tys:t_ list -> t_ * subst

ty_apply_full ty l is like apply t l, but it returns a pair ty' , subst such that subst ty' = apply t l.
Raises ApplyError if the arguments do not match

val ty_apply_mono : t_ -> tys:t_ list -> t_

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

Invalid_argument if t is not monomorphic (i.e. not TyForall)
ApplyError if the arguments do not match

type signature = TermInner.id -> t_ option

A signature is a way to obtain the type of a variable

val ty : sigma:signature -> t_ -> t_ TermInner.or_error

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

val ty_exn : sigma:signature -> t_ -> t_

Same as TermInner.UTIL.ty but unsafe.
Raises

Failure in case of error at an application
Undefined in case some symbol is not defined

exception UnifError of string * t_ * t_

Raised for unification or matching errors

val match_exn : ?subst2:subst -> t_ -> t_ -> subst

match_exn ~subst2 t1 t2 matches the pattern t1 against subst2 t2. Variables in subst2 t2 are not bound. We assume t1 and subst2 t2 do not share variables, and we assume that t1 is a mostly first-order pattern (no binders, but variables in head position is accepted and will only match an application).
Raises

UnifError if they dont_ match
Invalid_argument if t1 is not a valid pattern

val match_ : ?subst2:subst -> t_ -> t_ -> subst option

Safe version of TermInner.UTIL.match_exn
Raises Invalid_argument if t1 is not a valid pattern