Module `Smyth.Type_ctx`

val empty : Lang.type_ctx: The empty type context.

val all_type : Lang.type_ctx -> Lang.type_binding list: all_type gamma returns all name-to-Lang.typ (and Lang.bind_spec) bindings in the type context gamma.

val all_poly : Lang.type_ctx -> string list: all_poly gamma returns all polymorphic type variables in the type context gamma.

val concat : Lang.type_ctx list -> Lang.type_ctx: Concatenates a list of type contexts.

val add_type : Lang.type_binding -> Lang.type_ctx -> Lang.type_ctx: Adds a name-to-Lang.typ binding to the beginning of a type context.

val concat_type : Lang.type_binding list -> Lang.type_ctx -> Lang.type_ctx: Concatenates a list of name-to-Lang.typ bindings to the beginning of a type context.

val add_poly : Lang.poly_binding -> Lang.type_ctx -> Lang.type_ctx: Adds a polymorphic type variable to a type context.

val concat_poly : Lang.poly_binding list -> Lang.type_ctx -> Lang.type_ctx: Concatenates a list of polymorphic type variables to the beginning of a type context.

val peel_type : Lang.type_ctx -> (Lang.type_binding * Lang.type_ctx) option: peel_type gamma "pattern matches" on gamma. If gamma is nonempty, the first name-to-Lang.typ binding in it is returned along with the result of removing that binding from gamma (i.e., the "rest" of gamma). If gamma is empty, None is returned.

val names : Lang.type_ctx -> string list: names gamma returns a list of all bound names in gamma; that is, both the names of the name-to-Lang.typ bindings as well as the polymorphic type variables of gamma.