package dolmen
On This Page
package dolmen
-
dolmen
-
dolmen_intf
-
-
dolmen_line
-
dolmen_smtlib2
-
dolmen_smtlib2_v6
-
dolmen_std
-
-
dolmen_tptp
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library
Module
Module type
Parameter
Class
Class type
Parameters
Signature
The type of environnment/escaper for a given language. Identifiers printed using a given environment, are escaped, and its actual printed string recorded, in order to avoid future conflicts with other escaped identifiers.
val mk :
lang:string ->
name:(Id.t -> string) ->
escape:(string -> string) ->
rename:(string -> string) ->
tCreate an escaper from scratch. The name function is called to determine the name of an identifier. The escape function is assumed to be idempotent and have a lot of fixpoints (i.e. all valid identifiers name should map to themselves) whereas the renaming function should have absolutely no fixpoint (i.e. for all strings rename s <> s)
val flush : t -> unitRemove all the stored information about escaping and renaming.
val print : t -> Format.formatter -> Id.t -> unitA printing function that automatically escapes and rename if needed to avoid name clashes, and then print to the given formatter.
On This Page