Module DeBruijn

module DeBruijn: sig .. end

Dealing with binders.

val lift : int -> TypeCore.typ -> TypeCore.typ

lift i t lifts type t by i

val tsubst : TypeCore.typ -> int -> TypeCore.typ -> TypeCore.typ

tsubst t1 i t2 substitues t1 for index i in t2

val tsubst_branch : TypeCore.typ -> int -> TypeCore.branch -> TypeCore.branch

Same thing with a data type branch.

val tsubst_data_type_group : TypeCore.typ -> int -> TypeCore.data_type_group -> TypeCore.data_type_group

Same thing with a data type group.

val bind_rigid_in_type : TypeCore.env ->
       TypeCore.type_binding ->
       TypeCore.typ -> TypeCore.env * TypeCore.typ * TypeCore.var

bind_rigid_in_type env binding ty opens the binding binding, whose scope is the type ty, by replacing the bound variable with a rigid variable. It returns a triple of an extended environment, the new ty, and the variable that was created.

val bind_flexible_in_type : TypeCore.env ->
       TypeCore.type_binding ->
       TypeCore.typ -> TypeCore.env * TypeCore.typ * TypeCore.var

bind_rigid_in_type env binding ty opens the binding binding, whose scope is the type ty, by replacing the bound variable with a new flexible variable.