Лучшее отображение булевых формул


Я хочу реализовать метод отображения пропозициональной формулы в SML. Решения, которые я нашел до сих пор, были такого типа:

fun show (Atom a) = a
  | show (Neg p) = "(~ " ^ show p ^ ")"
  | show (Conj(p,q)) = "(" ^ show p ^ " & " ^ show q ^ ")"
  | show (Disj(p,q)) = "(" ^ show p ^ " | " ^ show q ^ ")";

Это приводит к ненужным скобкам:

((~p) & (q | r))

Когда, что я хотел бы иметь:

~ p & (q | r)

Я видел, что у Хаскелла есть функция (дисплей?) что делает это прекрасно. Кто-нибудь может мне немного помочь. Как я должен это сделать?

1 3

1 ответ:

Если вы хотите устранить избыточные скобки,вам нужно будет передать некоторую информацию о приоритете. Например, в Haskell функция showsPrec воплощает этот паттерн; она имеет тип

showsPrec :: Show a => Int -> a -> String -> String

Где первый аргумент Int является приоритетом текущего контекста печати. Дополнительный аргумент String - это трюк, чтобы получить эффективное добавление списка. Я покажу, как написать подобную функцию для вашего типа, хотя, по общему признанию, в Haskell (так как я знаю этот язык лучше всего) и без использования дополнительного трюка эффективности.

Идея состоит в том, чтобы сначала построить строку, которая не имеет скобок верхнего уровня , но имеет все скобки, необходимые для устранения неоднозначности подтем , а затем добавлять скобки только в случае необходимости. Нижеприведенное вычисление unbracketed делает первый шаг. Тогда единственный вопрос: когда мы должны поставить скобки вокруг нашего термина? Ну, ответ на это состоит в том, что вещи должны быть заключены в скобки, когда термин с низким приоритетом является аргументом для оператора с высоким приоритетом. Поэтому нам нужно сравнить приоритет нашего непосредственного "родителя" - вызываемого dCntxt в приведенном ниже коде-с приоритетом термина, который мы в данный момент визуализируем-вызываемого dHere в приведенном ниже коде. Функция bracket ниже либо добавляет скобки, либо оставляет строку в покое на основе результата этого сравнения.
data Formula
    = Atom String
    | Neg  Formula
    | Conj Formula Formula
    | Disj Formula Formula

precedence :: Formula -> Int
precedence Atom{} = 4
precedence Neg {} = 3
precedence Conj{} = 2
precedence Disj{} = 1

displayPrec :: Int -> Formula -> String
displayPrec dCntxt f = bracket unbracketed where
    dHere       = precedence f
    recurse     = displayPrec dHere
    unbracketed = case f of
        Atom s   -> s
        Neg  p   -> "~ " ++ recurse p
        Conj p q -> recurse p ++ " & " ++ recurse q
        Disj p q -> recurse p ++ " | " ++ recurse q
    bracket
        | dCntxt > dHere = \s -> "(" ++ s ++ ")"
        | otherwise      = id

display :: Formula -> String
display = displayPrec 0

Вот как это выглядит в действии.

*Main> display (Neg (Conj (Disj (Conj (Atom "a") (Atom "b")) (Atom "c")) (Conj (Atom "d") (Atom "e"))))
"~ ((a & b | c) & d & e)"