{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

{- |
  This module comprises the abstract definition of two core concepts of propositional logic:

    * The data type @('PropForm' a)@ of /propositional formulas/, based on a given /atom/ type @a@.

    * The two-parameter type class @('PropAlg' a p)@ of a /propositional algebra/, where @a@ is the /atom/ type and @p@ the type of
    /propositions/. Operations of such a structure include a decision if two propositions are 'equivalent', if a given proposition is
    'satisfiable', a converter 'toPropForm' and the inverse 'fromPropForm', which turns a propositional formula into a proposition.
-}

module PropLogicCore (

  -- * Propositional formulas
  PropForm (..),

  -- | A typical example of a propositional formula φ in standard mathematical notation is given by
  --
  -- @¬(rain ∧ snow) ∧ (wet ↔ (rain ∨ snow)) ∧ (rain → hot) ∧ (snow → ¬ hot)@
  --
  -- The primitive elements @hot@, @rain@, @snow@ and @wet@ are the /atoms/ of φ.
  -- In Haskell, we define propositional formulas as members of the data type (@PropForm a@), where the type parameter @a@ is the
  -- chosen atom type. A suitable choice for our example would be the atom type @String@ and φ becomes a member of
  -- @PropForm String@ type, namely
  --
  -- > CJ [N (CJ [A "rain", A "snow"]), EJ [A "wet", DJ [A "rain", A "snow"]], SJ [A "rain", A "hot"], SJ [A "snow", N (A "hot")]]
  --
  -- This Haskell version is more tedious and we introduce a third notation for nicer output by making @PropForm@ an instance of the
  -- 'Display' type class. A call of @'display' φ@ then returns
  --
  -- > [-[rain * snow] * [wet <-> [rain + snow]] * [rain -> hot] * [snow -> -hot]]
  --
  -- The following overview compares the different representations:
  --
  -- >   Haskell            displayed as              kind of formula
  -- >   --------------------------------------------------------------------
  -- >   A x                x   (without quotes)      atomic formula
  -- >   F                  false                     the boolean zero value
  -- >   T                  true                      the boolean unit value
  -- >   N p                -p                        negation
  -- >   CJ [p1,...,pN]     [p1 * ... * pN]           conjunction
  -- >   DJ [p1,...,pN]     [p1 + ... + pN]           disjunction
  -- >   SJ [p1,...,pN]     [p1 -> ... -> pN]         subjunction
  -- >   EJ [p1,...,pN]     [p1 <-> ... <-> pN]       equijunction
  --
  -- Note, that the negation is unary, as usual, but the last four constructors are all multiary junctions, i.e. the list @[p1,...,pN]@
  -- may have any number @N@ of arguments, including @N=0@ and @N=1@.
  --
  -- @PropForm a@ is an instance of @Eq@ and @Ord@, two formulas can be compared for linear order with @<@ or @compare@ and
  -- @PropForm a@ alltogther is linearly ordered, provided that @a@ itself is.
  -- But note, that this order is a pure formal expression order does neither reflect the atomical quasi-order structure
  -- (induced by the @subatomic@ relation; see below) nor the semantical quasi-order structure (induced by @subvalent@).
  -- So this is not the order that reflects the idea of propositional logic.
  -- But we do use it however for the sorting and order of formulas to reduce ambiguities and increase
  -- the efficiency of algorithmes on certain normal forms.
  -- In "DefaultPropLogic" we introduce the normal forms 'OrdPropForm' and the normalizer 'ordPropForm'.
  --
  -- @PropForm a@ is also an instance of @'Read'@ and @'Show'@, so String conversion (and displaying results in the interpreter) are
  -- well defined. For example
  --
  -- > show (CJ [A 3, N (A 7), A 4])  ==  "CJ [A 3,N (A 7),A 4]"
  --
  -- Note, that reading a formula, e.g.
  --
  -- > read "SJ [A 3, A 4, T]"
  --
  -- issues a complaint due to the ambiguity of the atom type. But that can be fixed, e.g. by stating the type explicitely,
  -- as in
  --
  -- > (read "SJ [A 3, A 4, T]") :: PropForm Integer
  --

  -- ** Parsing propositional formulas on string atoms
  stringToProp,

  -- | ... CONTINUEHERE ....

  -- * Propositional algebras
  PropAlg (..),

  -- | @PropAlg a p@ is a structure, made of
  --
  -- @a@ is the /atom/ type
  --
  -- @p@ is the type of /propositions/
  --
  -- @'at' :: a -> p@ is the /atomic proposition/ constructor, similar to the constructor 'A' for atomic formulas.
  --
  -- Similar to the definition of 'PropForm', we have the same set of boolean junctors on propositions:
  -- @'false', 'true' :: p@, @'neg' :: p-> p@ and @'conj', 'disj', 'subj', 'equij' :: [p] -> p@
  --
  -- There the set of
  -- ......................................................................

) where ---------------------------------------------------------------------------------------------------------------

-- imports

  import qualified Data.List   as L
  import qualified TextDisplay as D
  import qualified Olist       as O

-- the PropForm data type

  data PropForm a
    = A a
    | F
    | T
    | N (PropForm a)
    | CJ [PropForm a]
    | DJ [PropForm a]
    | SJ [PropForm a]
    | EJ [PropForm a]
    deriving (Show, Read, Eq)

-- the PropAlg class

  class Ord a => PropAlg a p | p -> a where
  -- the signature
    -- atomic proposition constructor
    at :: a -> p
    -- boolean junctors
    false :: p
    true :: p
    neg :: p -> p
    conj :: [p] -> p
    disj :: [p] -> p
    subj :: [p] -> p
    equij :: [p] -> p
    -- semantic properties and relations
    valid :: p -> Bool
    satisfiable :: p -> Bool
    contradictory :: p -> Bool
    subvalent :: p -> p -> Bool
    equivalent :: p -> p -> Bool
    covalent :: p -> p -> Bool
    disvalent :: p -> p -> Bool
    properSubvalent :: p -> p -> Bool
    properDisvalent :: p -> p -> Bool
    -- atom sets
    atoms :: p -> O.Olist a
    redAtoms :: p -> O.Olist a
    irrAtoms :: p -> O.Olist a
    -- atomic properties and relations
    nullatomic :: p -> Bool
    subatomic :: p -> p -> Bool
    equiatomic :: p -> p -> Bool
    coatomic :: p -> p -> Bool
    disatomic :: p -> p -> Bool
    properSubatomic :: p -> p -> Bool
    properDisatomic :: p -> p -> Bool
    -- atomic modifiers
    ext :: p -> [a] -> p
    infRed :: p -> [a] -> p
    supRed :: p -> [a] -> p
    infElim :: p -> [a] -> p
    supElim :: p -> [a] -> p
    -- biequivalence
    biequivalent :: p -> p -> Bool
    -- meta properties
    pointwise :: (p -> Bool) -> [p] -> Bool
    pairwise :: (p -> p -> Bool) -> [p] -> Bool
    -- formula conversions
    toPropForm :: p -> PropForm a
    fromPropForm :: PropForm a -> p
  -- some implementations
    pointwise = all
    pairwise property pL =
       case pL of
         []     -> True
         [x]    -> True
         (x:xL) -> (all (property x) xL)  && (pairwise property xL)
    contradictory p = not (satisfiable p)
    satisfiable p = not (contradictory p)
    covalent p1 p2 = not (disvalent p1 p2)
    disvalent p1 p2 = not (covalent p1 p2)
    nullatomic p = O.isEmpty (atoms p)
    subatomic p1 p2 = O.included (atoms p1) (atoms p2)
    equiatomic p1 p2 = O.equal (atoms p1) (atoms p2)
    coatomic p1 p2 = not (disatomic p1 p2)
    disatomic p1 p2 = O.disjunct (atoms p1) (atoms p2)
    properSubatomic p1 p2 = O.properlyIncluded (atoms p1) (atoms p2)
    properDisatomic p1 p2 = O.disjunct aL1 aL2 && not (O.isEmpty aL1) && not (O.isEmpty aL2)
      where aL1 = atoms p1
            aL2 = atoms p2
    biequivalent p1 p2 = equiatomic p1 p2 && equivalent p1 p2

-- displaying formulas

  instance D.Display a => D.Display (PropForm a) where
    textFrame form =
      let falseSymbol = "false"
          trueSymbol  = "true"
          negSymbol   = "-"
          conjSymbol  = "*"
          disjSymbol  = "+"
          subjSymbol  = "->"
          equijSymbol = "<->"
          multiJuncTextFrame symb pL = case pL of
            []  -> ["[" ++ symb ++ "]"]
            [p] -> D.textFrameBracket (D.plainMerge (D.normalTextFrameTable
                     [[[symb ++ " "], D.textFrame p]]))
            pL  -> D.textFrameBracket (D.plainMerge (D.normalTextFrameTable
                     [(L.intersperse [" " ++ symb ++ " "] (map D.textFrame pL))]))
      in case form of
        A x    -> D.textFrame x
        F      -> [falseSymbol]
        T      -> [trueSymbol]
        N p    -> D.plainMerge (D.normalTextFrameTable [[[negSymbol], D.textFrame p]])
        CJ pL -> multiJuncTextFrame conjSymbol pL
        DJ pL -> multiJuncTextFrame disjSymbol pL
        SJ pL -> multiJuncTextFrame subjSymbol pL
        EJ pL -> multiJuncTextFrame equijSymbol pL

-- parsing formulas on string atoms

  type Parser a = String -> [(a, String)]

  parseProp :: Parser (PropForm String)
  parseProp = parseAtom `plus` parseFalse `plus` parseTrue `plus` parseNeg `plus`
              parseConj `plus` parseDisj  `plus` parseSubj `plus` parseEquij
    where
      -- eight functions of type Parser (PropForm String)
      parseAtom = \ inp -> [ (A out',inp') | (out',inp') <- (skipWhite atomToken) inp ]
      parseFalse = \ inp -> [ (F, inp') | (out', inp') <- (skipWhite falseToken) inp ]
      parseTrue = \ inp -> [ (T, inp') | (out', inp') <- (skipWhite trueToken) inp ]
      parseNeg = \ inp -> [ (N out2, inp2) | (out1, inp1) <- (skipWhite negToken) inp,
                                             (out2, inp2) <- (skipWhite parseProp) inp1 ]
      parseConj = parseJunction CJ conjToken
      parseDisj = parseJunction DJ disjToken
      parseSubj = parseJunction SJ subjToken
      parseEquij = parseJunction EJ equijToken
      -- auxiliary function
      parseJunction :: ([PropForm String] -> PropForm String) -> Parser String -> Parser (PropForm String)
      parseJunction junc token = \ inp ->
        [ (junc [], i3) | (o1,i1) <- (skipWhite leftToken) inp,
                          (o2,i2) <- (skipWhite token) i1,
                          (o3,i3) <- (skipWhite rightToken) i2 ]
        ++
        [ (junc [o3], i4) | (o1,i1) <- (skipWhite leftToken) inp,
                            (o2,i2) <- (skipWhite token) i1,
                            (o3,i3) <- (skipWhite parseProp) i2,
                            (o4,i4) <- (skipWhite rightToken) i3 ]
        ++
        [ (junc (o2:o4:o5), i6) | (o1,i1) <- (skipWhite leftToken) inp,
                                  (o2,i2) <- (skipWhite parseProp) i1,
                                  (o3,i3) <- (skipWhite token) i2,
                                  (o4,i4) <- (skipWhite parseProp) i3,
                                  (o5,i5) <- tokenPropSeq i4,
                                  (o6,i6) <- (skipWhite rightToken) i5]
          where tokenPropSeq :: Parser [PropForm String]
                tokenPropSeq = \ inp -> case (skipWhite token) inp of
                  []         -> [([],inp)]
                  [(t,inp')] -> [ (o1:o2, i2) | (o1,i1) <- (skipWhite parseProp) inp',
                                                (o2,i2) <- (skipWhite tokenPropSeq) i1 ]
      -- the token parser of type Parser String
      atomToken = \ inp -> [ (out',inp') | (out',inp') <- (grab1 isAlphanum) inp,
                                           out' /= "false", out' /= "true" ]
      leftToken  = string "["         :: Parser String
      rightToken = string "]"         :: Parser String
      falseToken = string "false"     :: Parser String
      trueToken  = string "true"      :: Parser String
      negToken   = string "-"         :: Parser String
      conjToken  = string "*"         :: Parser String
      disjToken  = string "+"         :: Parser String
      subjToken  = string "->"        :: Parser String
      equijToken = string "<->"       :: Parser String
      -- the parser combinators
      string :: String -> Parser String
      string s = \ inp -> let (s1,s2,s3) = iter (s,inp,[])
                          -- iter(s,inp,[]) = (s1,s2,s3) so that
                          -- s1++s2=s and s1++s3=inp with s1 of maximal length
                          in if null s2
                             then [(s1,s3)]
                             else []
        where iter ([],y,z) = (reverse z,[],y)
              iter (x,[],z) = (reverse z,x,[])
              iter (x:xL,y:yL,z) = if x == y
                                   then iter (xL, yL, x:z)
                                   else (reverse z, x:xL, y:yL)
      grab :: (Char -> Bool) -> Parser String
      grab chf = \ inp -> iter ("",inp)
        where iter (xL, [])   = [(reverse xL, [])]
              iter (xL, y:yL) = if chf y
                                then iter (y:xL, yL)
                                else [(reverse xL, y:yL)]
      grab1 :: (Char -> Bool) -> Parser String
      grab1 chf = \ inp -> filter (\ (x,y) -> not (null x)) (grab chf inp)
      plus :: Parser a -> Parser a -> Parser a
      p `plus` q = \ inp -> (p inp ++ q inp)
      -- some character predicates of type Char -> Bool
      isDigit c = '0' <= c && c <= '9'
      isLower c = 'a' <= c && c <= 'z'
      isUpper c = 'A' <= c && c <= 'Z'
      isLetter c = isLower c || isUpper c
      isAlphanum c = isDigit c || isLetter c
      isWhite c = c == ' '   -- space char
               || c == '\n'  -- newline
               || c == '\t'  -- horizontal tab
               || c == '\v'  -- vertical tab
               || c == '\f'  -- form feed
               || c == '\r'  -- carriage return
      -- white space
      whiteSpace :: Parser String
      whiteSpace = grab isWhite
      skipWhite :: Parser a -> Parser a
      skipWhite p = \ inp -> [ (out1, inp1) | (out0, inp0) <- whiteSpace inp, (out1, inp1) <- p inp0 ]

  stringToProp :: String -> PropForm String
  stringToProp inp = case parseProp inp of
    []            -> error ("stringToProp -- input is not a proper fancy formula:\n" ++ inp)
    [(form,inp')] -> form
    _             -> error ("stringToProp -- Fatal error! Input doesn't parse unambiguously:\n" ++ inp)