package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module GenlambdaSource

Intermediate language used by both the VM and native.

Sourcetype reloc_table = (int * int) array
Sourcetype 'v lambda =
  1. | Lrel of Names.Name.t * int
  2. | Lvar of Names.Id.t
  3. | Levar of Evar.t * 'v lambda array
  4. | Lprod of 'v lambda * 'v lambda
  5. | Llam of Names.Name.t Context.binder_annot array * 'v lambda
  6. | Llet of Names.Name.t Context.binder_annot * 'v lambda * 'v lambda
  7. | Lapp of 'v lambda * 'v lambda array
  8. | Lconst of Constr.pconstant
  9. | Lproj of Names.Projection.Repr.t * 'v lambda
  10. | Lprim of Constr.pconstant * CPrimitives.t * 'v lambda array
  11. | Lcase of case_annot * 'v lambda * 'v lambda * 'v lam_branches
  12. | Lfix of int array * Names.inductive array * int * 'v fix_decl
  13. | Lcofix of int * 'v fix_decl
  14. | Lint of int
  15. | Lparray of 'v lambda array * 'v lambda
  16. | Lmakeblock of Names.inductive * int * 'v lambda array
  17. | Luint of Uint63.t
  18. | Lfloat of Float64.t
  19. | Lval of 'v
  20. | Lsort of Sorts.t
  21. | Lind of Constr.pinductive
  22. | Lforce
Sourceand 'v lam_branches = {
  1. constant_branches : 'v lambda array;
  2. nonconstant_branches : (Names.Name.t Context.binder_annot array * 'v lambda) array;
}
Sourceand 'v fix_decl = Names.Name.t Context.binder_annot array * 'v lambda array * 'v lambda array
Sourcetype evars = {
  1. 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
Sourceval decompose_Llam : 'v lambda -> Names.Name.t Context.binder_annot array * 'v lambda
Sourceval decompose_Llam_Llet : 'v lambda -> (Names.Name.t Context.binder_annot * 'v lambda option) array * 'v lambda
Sourceval 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
Sourceval 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
Sourceval lam_subst_args : 'v lambda Esubst.subs -> 'v lambda array -> 'v lambda array
Sourceval 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 make_args : int -> int -> 'v lambda array
Sourceval makeblock : (int -> 'v lambda array -> 'v option) -> Names.inductive -> int -> int -> int -> 'v lambda array -> 'v lambda
Sourceval 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct