val string : string Lplib.Base.pp

Translation of identifiers. Lambdapi identifiers that are Dedukti keywords or invalid Dedukti identifiers are escaped, a feature offered by Dedukti.

val keyword_table : ( string, Parsing.DkTokens.token ) Hashtbl.t
val is_keyword : string -> bool
val is_ident : string -> bool
val escape : string Lplib.Base.pp
val replace_spaces : string -> string
val ident : string Lplib.Base.pp

Translation of paths. Paths equal to the !current_path are not printed. Non-empty paths end with a dot. We assume that the module p1.p2.p3 is in the file p1_p2_p3.dk.

val path_elt : string Lplib.Base.pp
val current_path : string list ref
val qid : (Common.Path.t * string) Lplib.Base.pp
type decl =
| Sym of Core.Term.sym
| Rule of Common.Path.t * string * Core.Term.rule

Type of Dedukti declarations.

Declarations are ordered wrt their positions in the source.

val pos_of_decl : decl -> Common.Pos.popt

Translation of terms.

val term : bool -> Core.Term.term Lplib.Base.pp

Translation of declarations.

val modifiers : Core.Term.sym -> string list
val rule_decl : (Common.Path.t * string * Core.Term.rule) Lplib.Base.pp
val decl : decl Lplib.Base.pp
val decls_of_sign : Core.Sign.t -> decl list

decls_of_sign sign computes a list of declarations for the signature sign, in order of appearance in the source.

Translation of a signature.

val require : Common.Path.t -> 'a -> unit
val sign : Core.Sign.t -> unit