Module Export.CoqSource

Translate the parser-level AST to Coq.

There are two modes:

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_erasing : 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