Module Dot

module Dot: sig .. end

Dot backend for proofs

This module provides functions to export proofs into the dot graph format. Graphs in dot format can be used to generates images using the graphviz tool.

module type S = Backend_intf.S

Interface for exporting proofs.

module type Arg = sig .. end

module Default: functor (S : Res.S) -> Arg  with type atom := S.atom
                                 and type hyp := S.clause
                                 and type lemma := S.clause
                                 and type assumption := S.clause

Provides a reasonnable default to instantiate the Make functor, assuming the original printing functions are compatible with DOT html labels.

module Make: functor (S : Res.S) -> functor (A : Arg  with type atom := S.atom
                                and type hyp := S.clause
                                and type lemma := S.clause
                                and type assumption := S.clause) -> S  with type t := S.proof

Functor for making a module to export proofs to the DOT format.

module Simple: functor (S : Res.S) -> functor (A : Arg  with type atom := S.St.formula
                                  and type hyp = S.St.formula list
                                  and type lemma := S.lemma
                                  and type assumption = S.St.formula) -> S  with type t := S.proof

Functor for making a module to export proofs to the DOT format.