Module `Genlambda`Source

Intermediate language used by both the VM and native.

Sourcetype reloc_table = (int * int) array

type case_annot =
  Constr.case_info * reloc_table * Declarations.recursivity_kind

Sourcetype 'v lambda =

| Lrel of Names.Name.t * int
| Lvar of Names.Id.t
| Levar of Evar.t * 'v lambda array
| Lprod of 'v lambda * 'v lambda
| Llam of Names.Name.t Context.binder_annot array * 'v lambda
| Llet of Names.Name.t Context.binder_annot * 'v lambda * 'v lambda
| Lapp of 'v lambda * 'v lambda array
| Lconst of Constr.pconstant
| Lproj of Names.Projection.Repr.t * 'v lambda
| Lprim of Constr.pconstant * CPrimitives.t * 'v lambda array
| Lcase of case_annot * 'v lambda * 'v lambda * 'v lam_branches
| Lfix of int array * Names.inductive array * int * 'v fix_decl
| Lcofix of int * 'v fix_decl
| Lint of int
| Lparray of 'v lambda array * 'v lambda
| Lmakeblock of Names.inductive * int * 'v lambda array
| Luint of Uint63.t
| Lfloat of Float64.t
| Lval of 'v
| Lsort of Sorts.t
| Lind of Constr.pinductive
| Lforce

Sourceand 'v lam_branches = {

constant_branches : 'v lambda array;
nonconstant_branches : (Names.Name.t Context.binder_annot array * 'v lambda) array;

}

Source

and 'v fix_decl =
  Names.Name.t Context.binder_annot array * 'v lambda array * 'v lambda array

Sourcetype evars = {

evars_val : Constr.constr Constr.evar_handler;

}

Sourceval empty_evars : evars

Manipulation functions

Sourceval mkLapp : 'v lambda -> 'v lambda array -> 'v lambda

Sourceval mkLlam : Names.Name.t Context.binder_annot array -> 'v lambda -> 'v lambda

Source

val decompose_Llam : 
  'v lambda ->
  Names.Name.t Context.binder_annot array * 'v lambda

Source

val decompose_Llam_Llet : 
  'v lambda ->
  (Names.Name.t Context.binder_annot * 'v lambda option) array * 'v lambda

Source

val map_lam_with_binders : 
  (int -> 'a -> 'a) ->
  ('a -> 'v lambda -> 'v lambda) ->
  'a ->
  'v lambda ->
  'v lambda

Sourceval lam_exlift : Esubst.lift -> 'v lambda -> 'v lambda

Sourceval lam_lift : int -> 'v lambda -> 'v lambda

Source

val lam_subst_rel : 
  'v lambda ->
  Names.Name.t ->
  int ->
  'v lambda Esubst.subs ->
  'v lambda

Sourceval lam_exsubst : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda

Source

val lam_subst_args : 
  'v lambda Esubst.subs ->
  'v lambda array ->
  'v lambda array

Source

val simplify : 
  ('v lambda -> bool) ->
  'v lambda Esubst.subs ->
  'v lambda ->
  'v lambda

Sourceval remove_let : 'v lambda Esubst.subs -> 'v lambda -> 'v lambda

Translation functions

Sourceval get_alias : Environ.env -> Names.Constant.t -> Names.Constant.t

Sourceval make_args : int -> int -> 'v lambda array

Source

val makeblock : 
  (int -> 'v lambda array -> 'v option) ->
  Names.inductive ->
  int ->
  int ->
  int ->
  'v lambda array ->
  'v lambda

Source

val lambda_of_prim : 
  Environ.env ->
  Constr.pconstant ->
  CPrimitives.t ->
  'v lambda array ->
  'v lambda

Sourcemodule type S = sig ... end

Sourcemodule Make (Val : S) : sig ... end

Printing

Sourceval pp_lam : 'v lambda -> Pp.t

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Genlambda/index.html

Module `Genlambda`Source

Manipulation functions

Translation functions

Printing

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.kernel/Genlambda/index.html

Module GenlambdaSource

Manipulation functions

Translation functions

Printing

Module `Genlambda`Source