Module `Context.Rel`

Representation of contexts that can capture anonymous as well as non-anonymous variables. Individual declarations are then designated by de Bruijn indexes.

module Declaration : sig ... end

type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list: Rel-context is represented as a list of declarations. Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list.

val empty : ('c, 't) pt: empty rel-context

val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt: Return a new rel-context enriched by with a given inner-most declaration.

val length : ('c, 't) pt -> int: Return the number of local declarations in a given context.

val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool: Check whether given two rel-contexts are equal.

val nhyps : ('c, 't) pt -> int: Return the number of local assumptions in a given rel-context.

val lookup : int -> ('c, 't) pt -> ('c, 't) Declaration.pt

Return a declaration designated by a given de Bruijn index.

raises Not_found: if the designated de Bruijn index outside the range.

val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt: Map all terms in a given rel-context.

val iter : ('c -> unit) -> ('c, 'c) pt -> unit: Perform a given action on every declaration in a given rel-context.

val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a: Reduce all terms in a given rel-context to a single value. Innermost declarations are processed first.

val fold_outside : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a: Reduce all terms in a given rel-context to a single value. Outermost declarations are processed first.

val to_tags : ('c, 't) pt -> bool list: Map a given rel-context to a list where each local assumption is mapped to true and each local definition is mapped to false.

val drop_bodies : ('c, 't) pt -> ('c, 't) pt: Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

val to_extended_list : (int -> 'r) -> int -> ('c, 't) pt -> 'r list: extended_list mk n Γ builds an instance args such that Γ,Δ ⊢ args:Γ with n = |Δ| and with the local definitions of Γ skipped in args where mk is used to build the corresponding variables. Example: for x:T, y:=c, z:U and n=2, it gives mk 5, mk 3.

val to_extended_vect : (int -> 'r) -> int -> ('c, 't) pt -> 'r array: extended_vect n Γ does the same, returning instead an array.