Module Context.Named

This module represents contexts that can capture non-anonymous variables. Individual declarations are then designated by the identifiers they bind.

module Declaration : sig ... end

Representation of local declarations.

type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list

Named-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 named-context

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

Return a new named-context enriched by with a given inner-most declaration.

val length : ('c, 't) pt -> int

Return the number of local declarations in a given named-context.

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

Return a declaration designated by an identifier of the variable bound in that declaration.

raises Not_found

if the designated identifier is not bound in a given named-context.

val equal : ('c -> 'c -> bool) -> ('c, 'c) pt -> ('c, 'c) pt -> bool

Check whether given two named-contexts are equal.

val map : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt

Map all terms in a given named-context.

val iter : ('c -> unit) -> ('c, 'c) pt -> unit

Perform a given action on every declaration in a given named-context.

val fold_inside : ('a -> ('c, 't) Declaration.pt -> 'a) -> init:'a -> ('c, 't) pt -> 'a

Reduce all terms in a given named-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 named-context to a single value. Outermost declarations are processed first.

val to_vars : ('c, 't) pt -> Names.Id.Set.t

Return the set of all identifiers bound in a given named-context.

val drop_bodies : ('c, 't) pt -> ('c, 't) pt

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

val to_instance : (Names.Id.t -> 'r) -> ('c, 't) pt -> 'r list

to_instance Ω builds an instance args such that Ω ⊢ args:Ω where Ω is a named-context and with the local definitions of Ω skipped. Example: for id1:T,id2:=c,id3:U, it gives Var id1, Var id3. All idj are supposed distinct.