package mc2

  1. Overview
  2. Docs
package mc2
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Dot.DefaultSource

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

Term printing for DOT

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

Sourceval print_atom : Format.formatter -> Mc2_core.Atom.t -> unit

Print the contents of the given atomic formulas. WARNING: this function should take care to escape and/or not output special reserved characters for the dot format (such as quotes and so on).

Sourceval hyp_info : Mc2_core.Clause.t -> string * string option * (Format.formatter -> unit -> unit) list
Sourceval lemma_info : Mc2_core.Clause.t -> string * string option * (Format.formatter -> unit -> unit) list
Sourceval assumption_info : Mc2_core.Clause.t -> string * string option * (Format.formatter -> unit -> unit) list

Generate some information about the leafs of the proof tree. Currently this backend print each lemma/assumption/hypothesis as a single leaf of the proof tree. These function should return a triplet (rule, color, l), such that:

  • rule is a name for the proof (arbitrary, does not need to be unique, but should rather be descriptive)
  • color is a color name (optional) understood by DOT
  • l is a list of printers that will be called to print some additional information
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct