VerboseFormula

    let rec VerboseFormula formula =
        match formula with
        | Var(n) -> n
        | Const(n) -> n.ToString()
        | Disj(n, m) -> $"({VerboseFormula(n)} || {VerboseFormula(m)})"
        | Conj(n, m) -> $"({VerboseFormula(n)} && {VerboseFormula(m)})"
        | Neg(n) -> $"~{VerboseFormula(n)}"
        | Bic(n, m) -> $"({VerboseFormula(n)} <=> {VerboseFormula(m)})"
        | Impl(n, m) -> $"({VerboseFormula(n)} -> {VerboseFormula(m)})"

VerboseVormula is a recursive function the main goal of which is to represent a formula in a verbose way we are familiar with. The rules are obvious from the code. To reduce possible display errors there are no special Unicode characters are used. The basic character set is used instead.

• Disjunction ∨ replaced with ||
• Conjunction ∧ replaced with &&
• Negation ¬ replaced with ~
• Biconditional ⇔ replaced with <=>
• Implication → replaced with ->

These rules allow to produces a cross-platform verbatim string with clear meaning.

All parentheses are presented and never omitted.

Example

Input: Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))

Output: ((P && Q) -> (R <=> ~S))

Output': ((P ∧ Q) → (R ⇔ ¬S))

Usage

    let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S"))) // initialize a formula
    printf "%s" (VerboseFormula frm) // verbose the formula and print it