Previous  Up  

Module type Dot.Arg

module type Arg = sig .. end

Term printing for DOT

This module defines what functions are required in order to export a proof to the DOT format.

type atom
The type of atomic formuals
type lemma
The type of theory-specifi proofs (also called lemmas).
val print_atom : Format.formatter -> atom -> unit
Print the contents of the given atomic formulas. WARNING: this function should take care to esapce and/or not output special reserved characters for the dot format (such as quotes and so on).
val lemma_info : lemma ->
       string * string option * (Format.formatter -> unit -> unit) list
Generate some information about a theory specific lemmas. This backend does not support printing of proper proofs in DOT format, so all proofs are printed as leafs of the resolution tree. This function should return a triplet (rule, color, l), such that: