BuildFormulaCalcList

    let rec BuildFormulaCalcList formula =
        match formula with
        | Var (n) -> [ Var(n) ]
        | Disj (n, m) ->
            formula
            :: (BuildFormulaCalcList(n) @ BuildFormulaCalcList(m))
        | Conj (n, m) ->
            formula
            :: (BuildFormulaCalcList(n) @ BuildFormulaCalcList(m))
        | Neg (n) -> formula :: BuildFormulaCalcList(n)
        | Bic (n, m) ->
            formula
            :: (BuildFormulaCalcList(n) @ BuildFormulaCalcList(m))
        | Impl (n, m) ->
            formula
            :: (BuildFormulaCalcList(n) @ BuildFormulaCalcList(m))
        | _ -> [ formula ]

This function builds the sequence of calculation steps, based on the recursion from the very bottom level of variables to the highest one of formulas. Execution ordering supports by the formula definition syntax.

Example

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

Output:

    Var "P"
    Var "Q"
    Var "R"
    Var "S"
    Neg (Var "S")
    Conj (Var "P", Var "Q")
    Bic (Var "R", Neg (Var "S"))
    Impl (Conj (Var "P", Var "Q"), Bic (Var "R", Neg (Var "S")))

Usage

    let frm = Formula.Impl(Conj(Var "P", Var "Q"), Bic(Var "R", Neg(Var "S")))
    let formulaCalcList =
        BuildFormulaCalcList frm
        |> List.sortBy (fun f -> CalcFormulaDepth f)