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