Module `TypeInference.Ctx`

type t

val create : ?⁠def_as_rewrite:bool -> ?⁠default:type_ -> ?⁠on_var:[ `Default | `Infer ] -> ?⁠on_undef:[ `Warn | `Fail | `Guess ] -> ?⁠on_shadow:[ `Warn | `Ignore ] -> implicit_ty_args:bool -> unit -> t

New context with a signature and default types.

parameter default: which types are inferred by default (if not provided then type_erm will be used)

parameter def_as_rewrite: if true, definitions will be treated like rewrite rules

parameter on_undef: behavior when an undefined identifier is met

parameter is_tptp: if true, interpret some constants as in TPTP

parameter on_var: behavior when a variable without type annotation is met

val copy : t -> t: Copy of the context

val exit_scope : t -> unit: Exit the current scope (formula, clause), meaning that all free variables' types are forgotten. Some free variables are bound to the default type provided at creation of the context. Some ree variables will be generalized, i.e., kept as (free) variables

val declare : ?⁠loc:loc -> t -> ID.t -> type_ -> unit: Declare the type of a symbol, possibly shadowing a previous version

val with_var : t -> type_ Var.t -> f:(unit -> 'a) -> 'a: Execute a function f with an additional declared variable

val with_vars : t -> type_ Var.t list -> f:(unit -> 'a) -> 'a: Execute a function f with additional declared variables

val pop_new_types : t -> (ID.t * type_) list: Obtain the list of symbols whose type has been inferred recently, and reset it.