lambdapi 2.5.1 · OCaml Package

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).

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

Symbols necessary to encode STT.

type builtin =

| Set
| Prop
| Arr
| El
| Imp
| All
| Prf
| Eq
| Or
| And
| Ex
| Not

val index_of_builtin : builtin -> int

val nb_builtins : int

val builtin_of_index : int -> builtin

val index_of_name : string -> int option

val name_of_index : int -> string

val builtin : Core.Term.qident array

val sym : builtin -> Core.Term.qident

Set renaming map from file.

val rmap : Lplib.Extra.StrMap.key Lplib.Extra.StrMap.t Stdlib.ref

val set_renaming : string -> unit

Set symbols whose declarations have to be erased.

val erase : Lplib.Extra.StrSet.t Stdlib.ref

module Qid : sig ... end

module QidMap : sig ... end

val map_erased_qid_coq : string QidMap.t Stdlib.ref

val set_erasing : string -> unit

Set encoding.

val map_qid_builtin : builtin QidMap.t Stdlib.ref

val set_encoding : string -> unit

val out : ('a, Stdlib.out_channel, unit) Stdlib.format -> 'a

Basic printing functions. We use Printf for efficiency reasons.

val char : Stdlib.out_channel -> char -> unit

val string : Stdlib.out_channel -> string -> unit

val prefix : 
  string ->
  (Stdlib.out_channel -> 'a -> 'b) ->
  Stdlib.out_channel ->
  'a ->
  'b

val suffix : 
  (Stdlib.out_channel -> 'a -> 'b) ->
  string ->
  Stdlib.out_channel ->
  'a ->
  unit

val list : 
  (Stdlib.out_channel -> 'a -> unit) ->
  string ->
  Stdlib.out_channel ->
  'a list ->
  unit

Translation of identifiers.

val translate_ident : string -> string

val raw_ident : Stdlib.out_channel -> string -> unit

val ident : Stdlib.out_channel -> string Common.Pos.loc -> unit

val param_id : Stdlib.out_channel -> string Common.Pos.loc option -> unit

val param_ids : Stdlib.out_channel -> string Common.Pos.loc option list -> unit

val raw_path : Stdlib.out_channel -> string list -> unit

val path : Stdlib.out_channel -> string list Common.Pos.loc -> unit

val qident : 
  Stdlib.out_channel ->
  (string list * string) Common.Pos.loc ->
  unit

Translation of terms.

val stt : bool Stdlib.ref

val use_implicits : bool Stdlib.ref

val use_notations : bool Stdlib.ref

val p_get_args : 
  Parsing.Syntax.p_term ->
  Parsing.Syntax.p_term * Parsing.Syntax.p_term list

val app : 
  Parsing.Syntax.p_term ->
  (Parsing.Syntax.p_term -> Parsing.Syntax.p_term list -> 'a) ->
  (Parsing.Syntax.p_term ->
    Parsing.Syntax.p_term list ->
    bool ->
    builtin ->
    'a) ->
  'a

val term : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_term_aux Common.Pos.loc ->
  unit

val arrow : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_term ->
  Parsing.Syntax.p_term ->
  unit

val abst : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term ->
  unit

val prod : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_params list ->
  Parsing.Syntax.p_term ->
  unit

val paren : Stdlib.out_channel -> Parsing.Syntax.p_term -> unit

val raw_params : Stdlib.out_channel -> Parsing.Syntax.p_params -> unit

val params : Stdlib.out_channel -> Parsing.Syntax.p_params -> unit

val params_list : Stdlib.out_channel -> Parsing.Syntax.p_params list -> unit

val params_list_in_abs : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_params list ->
  unit

val typopt : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_term_aux Common.Pos.loc option ->
  unit

Translation of commands.

val is_lem : Parsing.Syntax.p_modifier_aux Common.Pos.loc -> bool

val command : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_command_aux Common.Pos.loc ->
  unit

val ast : 
  Stdlib.out_channel ->
  Parsing.Syntax.p_command_aux Common.Pos.loc Stream.t ->
  unit

Set Coq required file.

val require : string option Stdlib.ref

val set_requiring : string -> unit

val print : Parsing.Syntax.ast -> unit

package lambdapi