Binding (subml.Binding)

Binding relating functions

bindings of a type in a type and ordinals

val bind_kuvar : Ast.kuvar -> Ast.kind -> (Ast.kind, Ast.kind) LibTools.Bindlib.binder

binding a unification variable in a kind

Kind variable instanciation

exception Occur_check

Raised by set_kuvar if instanciation is illegal because it creates cyclic types

val safe_set_kuvar : Ast.occur -> Ast.kuvar -> Ast.kind Ast.from_ordis -> Ast.ordi array -> unit

Set kuvar with kind.

use the previous function 'make_safe'
does the occur check
if the kuvar_state is not Free, is uses the state and ignore the argumemt. Therefore it is not safe to assume that the unification variables is related to k after seting

instanciate type unification variables from state

val uvar_use_state : Ast.kuvar -> Ast.ordi array -> bool

Force a type unification variable to use its state. Return true if the variable is changed

bindings of ordinals in type and ordinals

The main difficulty here is for unification variable for kind or ordinals If we bind o in a variable ?1(o1,...,on) that may use o while o is not among its parameter, we must create a new variable ?2 and set ?1(x1,...,xn) to ?2(x1,...,xn,o). This appends in general for more than one variable. See the comment in the KUVar and OUVar cases

val index : Ast.ordi array -> 'a array -> Ast.ordi -> 'a

index os x u searches the index i of u in os and returns x.(i)

val bind_both : ?from_generalise:bool -> Ast.ordi array -> Ast.obox array -> AstMap.self_kind * AstMap.self_ord

val bind_fn : ?from_generalise:bool -> Ast.ordi array -> Ast.obox array -> Ast.kind -> Ast.kind LibTools.Bindlib.box

bind_fn ?(from_generalise=false) os x k Bind an array os of ordinals in the kind k. x is the array of bindlib variables to be used

val bind_gn : ?from_generalise:bool -> Ast.ordi array -> Ast.obox array -> Ast.ordi -> Ast.ordi LibTools.Bindlib.box

bind_gn ?(from_generalise=false) len os x o Bind an array os of ordinals in the ordinal o. x is the array of bindlib variables to be used

val obind_ordis : Ast.ordi array -> Ast.ordi -> (Ast.ordi, Ast.ordi) LibTools.Bindlib.mbinder

binding ordinals in one ordinal

val bind_ordis : Ast.ordi array -> Ast.kind -> (Ast.ordi, Ast.kind) LibTools.Bindlib.mbinder

binding ordinals in one kind

val bind_ouvar : Ast.ouvar -> Ast.kind -> (Ast.ordi, Ast.kind) LibTools.Bindlib.binder

binding of one ordinal in one kind

Instanciate ordinal unification variables from state

val ouvar_use_state : (Ast.ordi -> 'a) -> Ast.ordi list -> Ast.ouvar -> Ast.ordi array -> bool

Force an ordinal unification variable to use its state. Return true if the variable is changed