This module defines the type of propositional formulae, a parser, a
pretty-printer, and functions for building and decomposing.
> module Term(Term(..), parse, var, sub1, sub2,
> isVar, isNeg, isConj, isDisj, isImp)
> where
> import ParseLib hiding (parse)
> data Term = Var {var :: String}
> | Neg {sub1 :: Term}
> | Conj {sub1, sub2 :: Term}
> | Disj {sub1, sub2 :: Term}
> | Imp {sub1, sub2 :: Term}
> deriving (Eq)
Discussion:
- We could add the constants T and F.
- We could replace the three of Conj, Disj, and Imp by one single
constructor "Infix String Term Term", where the String argument
represents the operator. Advantage: the end user can extend the
logic by introducing new operators without modifying this module.
Disadvantage: inference rules will look more clumsy. The same goes
for Neg. One could further unify operators of different arities by
adopting higher-order logic.
- Here we export all the constructors and field labels. We could
(and should) hide them and provide our own functions for construction
and subterm extraction. This leads to runtime overhead but makes
software engineering sense. (E.g., what if you want to implement
the suggestion in the previous paragraph?)
The top-down parser. We use ParseLib from Hugs. We also integrate
this parser into the Read framework of Haskell.
> instance Read Term where
> readsPrec _ = papply term
> parse :: String -> Term
> parse = read
> term = ParseLib.parse impterm
> impterm = disjterm `chainr1` (symbol "==>" >> return Imp)
> disjterm = conjterm `chainl1` (symbol "||" >> return Disj)
> conjterm = primary `chainl1` (symbol "&&" >> return Conj)
> primary = varterm +++ parenterm +++ negterm
> negterm = do symbol "~"
> t <- primary
> return (Neg t)
> parenterm = bracket (symbol "(") term (symbol ")")
> varterm = do t <- identifier []
> return (Var t)
The pretty-printer in the framework of the Show class in Haskell.
> instance Show Term where
> showsPrec _ (Var s) = showString s
> showsPrec _ (Neg t) = showChar '~' . showsPrec 10 t
> showsPrec n (Conj s t) = showParen (n > 9) (showsPrec 9 s .
> showString " && " .
> showsPrec 10 t)
> showsPrec n (Disj s t) = showParen (n > 8) (showsPrec 8 s .
> showString " || " .
> showsPrec 9 t)
> showsPrec n (Imp s t) = showParen (n > 7) (showsPrec 8 s .
> showString " ==> " .
> showsPrec 7 t)
Discussion: we fudge with the precedence contexts, e.g.,
showsPrec 8 s . showString " ==> " . showsPrec 7 t
to implement the association of the binary operators, so that, e.g.,
(a ==> b) ==> c
is printed with the parentheses.
Auxilliary functions to determine the root operator in a formula.
> isVar (Var _) = True
> isVar _ = False
> isNeg (Neg _) = True
> isNeg _ = False
> isImp (Imp _ _) = True
> isImp _ = False
> isConj (Conj _ _) = True
> isConj _ = False
> isDisj (Disj _ _) = True
> isDisj _ = False