Module Lambda.Lambda

This is the actual module

module type VarEnvSig = sig ... end

This signature represents maps from the de Bruijn indices of a variable to some info that was recorded when the corresponding binder was crossed.

module MakeVarEnv (I : sig ... end) : VarEnvSig with type info = I.info

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.

module VNEnv : VarEnvSig with type info = string

This module implements a map from the de Bruijn indices of a variable to strings that was recorded when the corresponding binder was crossed.

type env = VNEnv.t
type kind =
  1. | Type
  2. | Depend of stype * kind
and stype =
  1. | Atom of int
  2. | DAtom of int
  3. | LFun of stype * stype
  4. | Fun of stype * stype
  5. | Dprod of string * stype * stype
  6. | Record of int * stype list
  7. | Variant of int * stype list
  8. | TAbs of string * stype
  9. | TApp of stype * term
and term =
  1. | Var of int
  2. | LVar of int
  3. | Const of int
  4. | DConst of int
  5. | Abs of string * term
  6. | LAbs of string * term
  7. | App of term * term
  8. | Rcons of int * term list
  9. | Proj of int * int * term
  10. | Vcons of int * int * term
  11. | Case of int * term * (string * term) list
  12. | Unknown of int
val generate_var_name : string -> (env * env) -> string
val unfold_labs : string list -> (env * env) -> term -> string list * (env * env) * term
val unfold_abs : string list -> (env * env) -> term -> string list * (env * env) * term
val unfold_app : term list -> term -> term list * term
val is_binder : int -> consts -> bool
val is_infix : int -> consts -> bool
val is_prefix : int -> consts -> bool
val unfold_binder : int -> consts -> string list -> (env * env) -> term -> string list * (env * env) * term
val pp_kind : consts -> Stdlib.Format.formatter -> kind -> unit
val pp_type : consts -> Stdlib.Format.formatter -> stype -> unit
val pp_term : ?env:(env * env) -> consts -> Stdlib.Format.formatter -> term -> unit
val raw_to_string : term -> string
val raw_type_to_string : stype -> string
val raw_to_caml : term -> string
val raw_type_to_caml : stype -> string
val normalize : ?id_to_term:(int -> term) -> term -> term
val unlinearize_term : term -> term
val unlinearize_type : stype -> stype
val eta_long_form : term -> stype -> (int -> stype) -> term

eta_long_form t ty type_of_cst returns the eta-long form of t with respect of type ty. t is supposed to be in beta-normal form and all the definitions of t and ty should have been unfolded. type_of_cst i returns the type (with unfolded definitions) of the constant whose id is i. i is supposed to be an actual id of a constant.

val is_2nd_order : stype -> (int -> stype) -> bool

is_2nd_order ty type_definition returns true if ty is 2nd order. ty should have been unfolded and type_definition i is returns the unfolded type of a defined type (DAtom) whose id is i. i is supposed to be an actual id of such a defined type.

val is_atomic : stype -> (int -> stype) -> bool

is_atomic ty type_definition returns true if ty is atomic. type_definition i returns the unfolded type of a defined type (DAtom) whose id is i. i is supposed to be an actual id of such a defined type.

val size : id_to_term:(int -> term) -> term -> int * int
val alpha_eq : term -> term -> bool

alpha_eq t u returns true if t and u are alpha-equivalent, false otherwise.

val equal : id_to_term:(int -> term) -> type_of_const:(int -> stype) -> (term * stype) -> (term * stype) -> bool