package lambdapi

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

Module Export.CoqSource

Translate the parser-level AST to Coq.

There are two modes:

  • raw_coq mode (option -o raw_coq): translation of the AST as it is (lambdapi-calculus is a subset system of coq if we ignore rules)
  • stt_coq mode (option -o stt_coq): translation of the AST as an encoding in simple type theory.

The encoding can be specified through a lambdapi file (option --encoding).

In both modes, a renaming map can be provided to rename some identifiers.

The renaming map can be specified through a lambdapi file (option --renaming).

Sourceval log : 'a Lplib.Base.outfmt -> 'a

Symbols necessary to encode STT.

Sourcetype builtin =
  1. | Set
  2. | Prop
  3. | Arr
  4. | El
  5. | Imp
  6. | All
  7. | Prf
  8. | Eq
  9. | Or
  10. | And
  11. | Ex
  12. | Not
Sourceval index_of_builtin : builtin -> int
Sourceval nb_builtins : int
Sourceval builtin_of_index : int -> builtin
Sourceval index_of_name : string -> int option
Sourceval name_of_index : int -> string
Sourceval builtin : Core.Term.qident array

Set renaming map from file.

Sourceval set_renaming : string -> unit

Set symbols whose declarations have to be erased.

Sourcemodule Qid : sig ... end
Sourcemodule QidMap : sig ... end
Sourceval map_erased_qid_coq : string QidMap.t ref
Sourceval set_mapping : string -> unit

Set encoding.

Sourceval map_qid_builtin : builtin QidMap.t ref
Sourceval set_encoding : string -> unit
Sourceval out : ('a, out_channel, unit) format -> 'a

Basic printing functions. We use Printf for efficiency reasons.

Sourceval char : out_channel -> char -> unit
Sourceval string : out_channel -> string -> unit
Sourceval prefix : string -> (out_channel -> 'a -> 'b) -> out_channel -> 'a -> 'b
Sourceval suffix : (out_channel -> 'a -> 'b) -> string -> out_channel -> 'a -> unit
Sourceval list : (out_channel -> 'a -> unit) -> string -> out_channel -> 'a list -> unit

Translation of identifiers.

Sourceval translate_ident : string -> string
Sourceval raw_ident : out_channel -> string -> unit
Sourceval ident : out_channel -> string Common.Pos.loc -> unit
Sourceval param_id : out_channel -> string Common.Pos.loc option -> unit
Sourceval param_ids : out_channel -> string Common.Pos.loc option list -> unit
Sourceval raw_path : out_channel -> string list -> unit
Sourceval path : out_channel -> string list Common.Pos.loc -> unit
Sourceval qident : out_channel -> (string list * string) Common.Pos.loc -> unit

Translation of terms.

Sourceval stt : bool ref
Sourceval use_implicits : bool ref
Sourceval use_notations : bool ref
Sourceval raw_params : out_channel -> Parsing.Syntax.p_params -> unit
Sourceval params_list : out_channel -> Parsing.Syntax.p_params list -> unit
Sourceval params_list_in_abs : out_channel -> Parsing.Syntax.p_params list -> unit

Translation of commands.

Set Coq required file.

Sourceval require : string option ref
Sourceval set_requiring : string -> unit
Sourceval print : Parsing.Syntax.ast -> unit
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