dolmen

A parser library for automated deduction
Legend:
Library
Module
Module type
Parameter
Class
Class type
Library dolmen.std
Module Dolmen_std . Escape . Make

Parameters

module Id : Arg

Signature

type t

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

Create 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 -> unit

Remove all the stored information about escaping and renaming.

val print : t -> Stdlib.Format.formatter -> Id.t -> unit

A printing function that automatically escapes and rename if needed to avoid name clashes, and then print to the given formatter.