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, 'r) pt = ('constr, 'types, 'r) 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, 'r) pt

empty named-context

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

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

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

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

val lookup : Names.Id.t -> ('c, 't, 'r) pt -> ('c, 't, 'r) 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 : ('r -> 'r -> bool) -> ('c -> 'c -> bool) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt -> bool

Check whether given two named-contexts are equal.

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

Map all terms in a given named-context.

val map_with_relevance : ('r -> 'r) -> ('c -> 'c) -> ('c, 'c, 'r) pt -> ('c, 'c, 'r) pt

Map all terms in a given rel-context.

val map_het : ('r1 -> 'r2) -> ('c -> 'd) -> ('c, 'c, 'r1) pt -> ('d, 'd, 'r2) pt

Map all terms in a given named-context.

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

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

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

Reduce all terms in a given named-context to a single value. Innermost declarations are processed first.

val fold_outside : (('c, 't, 'r) Declaration.pt -> 'a -> 'a) -> ('c, 't, 'r) 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, 'r) pt -> Names.Id.Set.t

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

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

Turn all LocalDef into LocalAssum, leave LocalAssum unchanged.

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

to_instance Ω builds an instance args in reverse order 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.

val instance : (Names.Id.t -> 'v) -> ('c, 't, 'r) pt -> 'v array

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

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

instance_list is like instance but returning a list.