package acgtk

  1. Overview
  2. Docs
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Lambda.MakeVarEnvSource

This modules is a functor that returns a map from the de Bruijn indices of a variable to some info that was recorded when the corresponding binder was crossed.

Parameters

module I : sig ... end

Signature

Sourcetype level = int
Sourcetype info = I.info
Sourcetype t
Sourceval empty : t
Sourceval add : info -> t -> t
Sourceval set : level -> info -> t -> t
Sourceval get : level -> t -> info
Sourceval current_level : t -> level
Sourceval get_opt : level -> t -> info option
Sourceval exists : (info -> bool) -> t -> bool
Sourceval shift : info:info -> level:level -> t -> t

shift ~info ~level e changes e into e' where: if level l < level maps to info i, then l maps to i in e' as well. If l >= level maps to info i, then l+1 maps to i. Finally, in e', level maps to info.

Sourceval pp : Format.formatter -> t -> unit