module Ctx: sig .. end
type
val create : ?default:TypeInference.type_ -> unit -> t
New context with a signature and default types.
default : which types are inferred by default (if not provided
then type_erm will be used)
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 : t -> ID.t -> TypeInference.type_ -> unit
Declare the type of a symbol, possibly shadowing a previous version
val pop_new_types : t -> (ID.t * TypeInference.type_) list
Obtain the list of symbols whose type has been inferred recently,
and reset it.