{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}


-- |
--  This module defines three altenative representations for certain propositional normal forms, namely
--
-- > data XPDNF a          -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
-- > data XPCNF a          -- a representation for Prime Disjunctive Normal Forms or PDNF's on a given atom type a
-- > data MixForm a        -- a type made of pairwise minimal DNF's and CNF's on a given atom type a
--
--  For each of these types there is a converter from and a converter to propositional formulas
--
--  >    fromXPDNF :: Ord a => XPDNF a -> PropForm a             toXPDNF :: Ord a => PropForm a -> XPDNF a
--  >    fromXPCNF :: Ord a => XPCNF a -> PropForm a             toXPCNF :: Ord a => PropForm a -> XPCNF a
--  >  fromMixForm :: Ord a => MixForm a -> PropForm a         toMixForm :: Ord a => PropForm a -> MixForm a
--
--  Each of these three types is turned into a propositional algebra 'PropAlg', i.e. for every ordered type @a@ of /atoms/
--  we have three instances
--
-- > PropAlg a (XPDNF a)
-- > PropAlg a (XPCNF a)
-- > PropAlg a (MixForm a)
--
--  Different to the two default propositional algebras on propositional formulas and truth tables, these three algebras comprise fast
--  function implementations and thus provide practical versions for propositional algebras, where propositions of arbitrary size
--  are processed in reasonable time.
--  In more detail the involved complexities are given in the table below (see ......).
--  It also explains, which of the three algebras should be chosen in an actual application.
--
--  Actually, this module is essentially a re-implementation of already explained concepts from "PropLogicCore" and "DefaultPropLogic"
--  and for the user it shouldn't be necessary to further explain how the algorithms work.
--  The remainder of this document is an attempt to do just that.
--  However, if you at least want an idea of what is going on here, it may suffice to read the first section with the introductory
--  example below.

{-
  This module defines three altenative representations for certain propositional normal forms, namely

  'XPDNF' a representation for Prime Disjunctive Normal Forms 'DefaultPropLogic.PDNF',
  'XPCNF' a representation for Prime Conjunctive Normal Forms 'DefaultPropLogic.PCNF', and
  'MixForm' a type comprising pairwise minimal DNFs and CNFs.

  For each of these types there is a converter from and a converter to propositional formulas 'PropLogicCore.PropForm'.
  For example, for 'XPDNF' this is @fromXPDNF :: XPDNF a -> PropForm a@ and  @toXPDNF :: PropForm a -> XPDNF a@.

  Each of these three types is turned into a propositional algebra, i.e. it becomes an instance of 'PropLogicCore.PropAlg'.
  Different to the two default propositional algebras on propositional formulas and truth tables (see 'DefaultPropLogic.PropForm' and 'DefaultPropLogic.TruthTable'), these three algebras comprise fast function implementations and thus provide practical versions for propositional algebras for propositions of any size, not just for formulas with very small atoms sets.
-}

module FastPropLogic (

  -- * Introductory example

  -- ** Generating a Prime Disjunctive Normal Form, the default and the fast way

  -- | Recall, that we already defined /Disjunctive Normal Forms/ and /Prime Disjunctive Normal Forms/ in "DefaultPropLogic" as
  -- special versions of propositional formulas, along with a canonizer @pdnf@ to obtain these normal forms
  --
  -- > type DNF a = PropForm a
  -- > type PDNF a = DNF a
  -- > pdnf :: PropForm a -> PDNF a
  --
  -- For a simple example formula @p@, given by
  --
  -- > > p = DJ [EJ [A "x", A "y"], N (A "z")]  ::  PropForm String
  --
  --  more conveniently displayed by
  --
  -- > > display p
  -- > [[x <-> y] + -z]
  --
  --  the PDNF of @p@ is then generated by
  --
  -- > > pdnf p
  -- > DJ [CJ [EJ [A "x",F],EJ [A "y",F]],CJ [EJ [A "x",T],EJ [A "y",T]],CJ [EJ [A "z",F]]]
  -- > > display (pdnf p)
  -- > [[[x <-> false] * [y <-> false]] + [[x <-> true] * [y <-> true]] + [* [z <-> false]]]
  --
  --  or more conveniently displayed in its evaluated form
  --
  -- > > display (eval (pdnf p))
  -- > [[-x * -y] + [x * y] + -z]
  --
  -- .............!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!..............................
  --
  --  (Actually, each converter pair is also part of each of the given algebras. For example, in the XPDNF instance holds:
  --   'fromXPDNF' = 'toPropForm' and 'toXPDNF' = 'fromPropForm'.)
  --

  -- ** XPDNF as a propositional algebra
  --
  -- | ,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,,

  -- ** The canonization steps
  --

  -- * Syntax
  IAtom,
  ILit,
  ILine,
  IForm,
  XLit,
  XLine,
  XForm,
  XPDNF(..), XPCNF(..),
  MixForm(..),

  -- * Conversions

  -- ** IdxPropForm -- indexed propositional formulas
  IdxPropForm,
  tr,
  -- | @tr f form@ replaces each atom form occurrence @(A x)@ in the formula @form@ by the new atom @(A (f x))@. Everything else remains.
  iTr,
  -- | @iTr [i_1,...,i_n] iform@ replaces each index @j@ in @iform@ by @i_j@. For example,
  --
  -- > > let iform =  iForm [[-1,3,-4,5],[-2,-3,4,6]] :: IForm
  -- > > iform
  -- > COSTACK [COSTACK [-1,3,-4,5],COSTACK [-2,-3,4,6]]
  -- > > iTr [7,8,9,10,11,12,13] iform
  -- > COSTACK [COSTACK [-7,9,-10,11],COSTACK [-8,-9,10,12]]
  -- > > iTr [2,4] iform
  -- > -- error, because the index list [2,4] must at least be of length 6 to cover the indices 1,..,6 of iform.
  idx,
  -- | @idx [i_1,...,i_n] i_k@ returns @k@, i.e. the index of the index in the given index list.
  -- Note, that the first member of the list starts with index 1, not 0. For example,
  --
  -- > > idx [2,4,6,8] 6
  -- > 3
  nth,
  -- | @nth [i_1,...,i_n] k@ returns @i_k@, i.e. the @k@'s element in the list @[i_1,...,i_n]@, counting from @1@. For example,
  --
  -- > > nth [2,4,6,8] 3
  -- > 6

  itr,
  iUni,
  unifyIdxPropForms,
  unifyXForms,
  fromIdxPropForm,
  toIdxPropForm,
  newAtomsXForm,

  -- ** Purely syntactical conversions to propositional formulas
  iLIT, iNLC, iNLD, iCNF, iDNF,
  xLIT, xNLC, xNLD, xCNF, xDNF,

  -- ** Conversions to and from propositional formulas
  toXPDNF,
  toXPCNF,
  toM2DNF, toM2CNF,
  fromXPDNF,
  fromXPCNF,
  fromMixForm,

  -- * The IForm algebra

  -- ** Basic operations
  isIAtom,
  isILit,
  isILine,
  isIForm,
  iLine,
  iForm,
  iAtom,
  iBool,
  negLit,
  lineIndices,
  formIndices,
  lineLength,
  formLength,
  volume,
  isOrderedForm,
  orderForm,

  -- ** The propositional algebra operations
  atomForm,
  botForm,
  topForm,
  formJoinForm,
  formListJoin,
  lineMeetLine,
  lineMeetForm,
  formMeetForm,
  formListMeet,
  dualLine,
  dualForm,
  invertLine,
  invertForm,
  negLine,
  negForm,
  formCojoinLine,
  formCojoinForm,
  formAntijoinLine,
  formAntijoinForm,
  elimLine,
  elimForm,
  lineCovLine,
  lineCovForm,
  formCovForm,

  -- ** Generation of pairwise minimal, minimal and prime forms

  -- *** Generation of prime and pairwise minimal forms of two lines
  pairPartition,
  CaseSymbol(..),
  caseSymbol,
  pairPrim',
  pairMin',
  xprim',
  xmin',
  xprim,
  xmin,
  pairPrim,
  pairMin,

  -- *** Implementation of the M- and the P-Procedure
  isMinimalPair,
  allPairs,
  isPairwiseMinimal,
  cPrime,
  cPrimes,
  mrec,
  m2form,
  iformJoinM2form,
  primForm,
  iformJoinPrimForm,

  -- * The XForm operations
  xformAtoms,
  xformRedAtoms,
  xformIrrAtoms,

  -- * The propositional algebras

  -- ** XPDNF and XPCNF

  -- ** MixForm
  mixToPDNF,
  mixToPCNF,

  -- * Complexities and choice of a algebra
  -- |
  --
  -- >                                         DefaultPropLogic.                               FastPropLogic
  -- >                                         --------------------------------------         -----------------------------------
  -- >                                         PropForm            TruthTable                 XPDNF       XPCNF          MixForm
  -- > --------------------------------------------------------------------------------------------------------------------------
  -- > at
  -- > false
  -- > true
  -- > neg
  -- > conj, disj, subj, equij
  -- > valid
  -- > satisfiable
  -- > subvalent
  -- > equivalent
  -- > covalent, disvalent,
  -- > properSubvalent, properDisvalent
  -- > atoms
  -- > redAtoms, irrAtoms
  -- > nullatomic
  -- > subatomic, equiatomic
  -- > .........
  -- > .........

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

-- import

  import qualified Data.List   as L
  import qualified TextDisplay as D
  import qualified Olist       as O
  import qualified Costack     as C
  import PropLogicCore
  import DefaultPropLogic (NegNormForm, negNormForm)

-- the types

  type IAtom = Int                                    -- I-Atom

  type IdxPropForm a = (O.Olist a, PropForm IAtom)    -- indexed propositional formula
  -- type IntLitNormForm = PropForm ILit                 -- integer literal normal form

  type ILit = Int                                     -- I-Literal or integer literal type
  type ILine = C.Costack ILit                         -- I-Line or integer line type
  type IForm = C.Costack ILine                        -- I-Form or integer form type
  type XLit a = (O.Olist a, ILit)                     -- X-Literal or indexed literal type
  type XLine a = (O.Olist a, ILine)                   -- X-Line or indexed line type
  type XForm a = (O.Olist a, IForm)                   -- X-Form or indexed form type

  data XPDNF a = XPDNF (XForm a)                      -- Indexed/Extended Prime Disjunctive Normal Forms
    deriving (Show, Read, Eq)
  data XPCNF a = XPCNF (XForm a)                      -- Indexed/Extended Prime Conjunctive Normal Forms
    deriving (Show, Read, Eq)

  data MixForm a                                      -- Mixed Forms:
    = M2DNF (XForm a)                                 --   Pairwise Minimal Disjunctive Normal Forms
    | M2CNF (XForm a)                                 --   Pairwise Minimal Conjunctive Normal Forms
    | PDNF  (XForm a)                                 --   Prime Disjunctive Normal Forms
    | PCNF  (XForm a)                                 --   Prime Conjunctive Normal Forms
    deriving (Show, Read, Eq)

-- display

  instance D.Display IForm where
    textFrame form = textframe
      where indices = formIndices form
            oneRow line iL = if C.isEmpty line
                             then if null iL
                                  then []
                                  else [""] : (oneRow line (Prelude.tail iL))
                             else case compare (iAtom (C.head line)) (Prelude.head iL) of
                                    GT -> [""] : (oneRow line (Prelude.tail iL))
                                    EQ -> if iBool (C.head line)
                                          then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))
                                          else [show (C.head line)]         : (oneRow (C.tail line) (Prelude.tail iL))
            frameTable = map (\ line -> oneRow line indices) (C.toList form)
            textframe = D.gridMerge (D.normalTextFrameTable frameTable)

  instance D.Display a => D.Display (XForm a) where
    textFrame (aL, form) = textframe
      where headRow = map D.textFrame aL
            indices = [1..(length aL)] :: [IAtom]
            oneRow line iL = if C.isEmpty line
                             then if null iL
                                  then []
                                  else [""] : (oneRow line (Prelude.tail iL))
                             else case compare (iAtom (C.head line)) (Prelude.head iL) of
                                    GT -> [""] : (oneRow line (Prelude.tail iL))
                                    EQ -> if iBool (C.head line)
                                          then ['+' : (show (C.head line))] : (oneRow (C.tail line) (Prelude.tail iL))
                                          else [show (C.head line)]         : (oneRow (C.tail line) (Prelude.tail iL))
            tableBody = map (\ line -> oneRow line indices) (C.toList form)
            textframe = D.gridMerge (D.normalTextFrameTable (headRow:tableBody))

  titledTextFrame :: D.Display a => (String,String,String) -> XForm a -> D.TextFrame
  titledTextFrame (empty, full, title) (aL,iform) =
    if null aL
    then if C.isEmpty iform
         then D.textFrameBox (D.correctTextFrame [title,empty])
         else D.textFrameBox (D.correctTextFrame [title,full])
    else let body = D.textFrame (aL,iform)
             textframe = D.textFrameBox (D.plainMerge (D.normalTextFrameTable [[[title]],[body]]))
         in textframe

  instance D.Display a => D.Display (XPDNF a) where
    textFrame (XPDNF xform) = titledTextFrame ("false", "true", "XPDNF") xform

  instance D.Display a => D.Display (XPCNF a) where
    textFrame (XPCNF xform) = titledTextFrame ("true", "false", "XPCNF") xform

  instance D.Display a => D.Display (MixForm a) where
    textFrame (M2DNF xform) = titledTextFrame ("false", "true", "M2DNF") xform
    textFrame (M2CNF xform) = titledTextFrame ("true", "false", "M2CNF") xform
    textFrame (PDNF  xform) = titledTextFrame ("false", "true", "PDNF")  xform
    textFrame (PCNF  xform) = titledTextFrame ("true", "false", "PCNF")  xform

-- order

  instance Ord ILine where
    compare left right =
      if C.isEmpty left
      then if C.isEmpty right
           then EQ
           else LT
      else if C.isEmpty right
           then GT
           else case compare (iAtom (C.head left)) (iAtom (C.head right)) of
             LT -> LT
             GT -> GT
             EQ -> case compare (iBool (C.head left)) (iBool (C.head right)) of
                     LT -> LT
                     GT -> GT
                     EQ -> compare (C.tail left) (C.tail right)

  instance Ord IForm where
    compare form1 form2 = if C.isEmpty form1
                          then if C.isEmpty form2
                               then EQ
                               else LT
                          else if C.isEmpty form2
                               then GT
                               else case compare (C.head form1) (C.head form2) of
                                      LT -> LT
                                      GT -> GT
                                      EQ -> compare (C.tail form1) (C.tail form2)

-- convertions via IntLitNormForm

  toXPDNF :: Ord a => PropForm a -> XPDNF a
  toXPDNF p = XPDNF (aL, primForm iform)
    where (aL, iprop) = toIdxPropForm p
          iform = fromNegNF (negNormForm iprop)
          fromNegNF (A n) = atomForm n
          fromNegNF (N (A n)) = atomForm (negLit n)
          fromNegNF F = botForm
          fromNegNF T = topForm
          fromNegNF (CJ pL) = formListMeet (map fromNegNF pL)
          fromNegNF (DJ pL) = formListJoin (map fromNegNF pL)

  toXPCNF :: Ord a => PropForm a -> XPCNF a
  toXPCNF p = XPCNF (aL, primForm iform)
    where (aL, iprop) = toIdxPropForm p
          iform = fromNegNF (negNormForm iprop)
          fromNegNF (A n) = atomForm n
          fromNegNF (N (A n)) = atomForm (negLit n)
          fromNegNF F = topForm
          fromNegNF T = botForm
          fromNegNF (CJ pL) = formListJoin (map fromNegNF pL)
          fromNegNF (DJ pL) = formListMeet (map fromNegNF pL)

  fromXPDNF :: Ord a => XPDNF a -> PropForm a
  fromXPDNF (XPDNF xform) = xDNF xform

  fromXPCNF :: Ord a => XPCNF a -> PropForm a
  fromXPCNF (XPCNF xform) = xCNF xform

  toM2DNF :: Ord a => PropForm a -> MixForm a
  toM2DNF p = M2DNF (aL, m2form iform)
    where (aL, iprop) = toIdxPropForm p
          iform = fromIntLitNormForm (negNormForm iprop)
          fromIntLitNormForm (A n) = atomForm n
          fromIntLitNormForm F = botForm
          fromIntLitNormForm T = topForm
          fromIntLitNormForm (CJ pL) = formListMeet (map fromIntLitNormForm pL)
          fromIntLitNormForm (DJ pL) = formListJoin (map fromIntLitNormForm pL)

  toM2CNF :: Ord a => PropForm a -> MixForm a
  toM2CNF p = M2CNF (aL, m2form iform)
    where (aL, iprop) = toIdxPropForm p
          iform = fromIntLitNormForm (negNormForm iprop)
          fromIntLitNormForm (A n) = atomForm n
          fromIntLitNormForm F = topForm
          fromIntLitNormForm T = botForm
          fromIntLitNormForm (CJ pL) = formListJoin (map fromIntLitNormForm pL)
          fromIntLitNormForm (DJ pL) = formListMeet (map fromIntLitNormForm pL)

  fromMixForm :: Ord a => MixForm a -> PropForm a
  fromMixForm (M2DNF xform) = xDNF xform
  fromMixForm (M2CNF xform) = xCNF xform
  fromMixForm (PDNF xform)  = xDNF xform
  fromMixForm (PCNF xform)  = xCNF xform

-- translations, indices and unifications

  tr :: (s -> t) -> PropForm s -> PropForm t
  tr f (A x) = A (f x)
  tr f F = F
  tr f T = T
  tr f (N prop) = N (tr f prop)
  tr f (CJ propL) = CJ (map (tr f) propL)
  tr f (DJ propL) = DJ (map (tr f) propL)
  tr f (SJ propL) = SJ (map (tr f) propL)
  tr f (EJ propL) = EJ (map (tr f) propL)

  iTr :: O.Olist IAtom -> IForm -> IForm
  iTr aL form = C.map (iTr' aL 1) form
    where iTr' aL n line = if C.isEmpty line
                          then line
                          else case compare n (iAtom (C.head line)) of
                            EQ -> if (iBool (C.head line))
                                  then C.cons (head aL)          (iTr' (tail aL) (n + 1) (C.tail line))
                                  else C.cons (negLit (head aL)) (iTr' (tail aL) (n + 1) (C.tail line))
                            LT -> iTr' (tail aL) (n + 1) line

  idx :: Ord a => O.Olist a -> a -> IAtom
  idx [] x = error "idx -- empty list"
  idx (y:yL) x = case compare y x of
                   LT -> 1 + (idx yL x)
                   EQ -> 1
                   GT -> error "idx -- atom is not a list member"

  nth :: Ord a => O.Olist a -> IAtom -> a
  nth oli n = if n < 1
              then error ("nth -- undefined IAtom " ++ (show n))
              else iter (n, oli)
                 where iter (i, []) = error ("nth -- index " ++ (show n) ++ " exceeds the list length")
                       iter (i, (x:xL)) = if i == 1
                                         then x
                                         else iter (i - 1, xL)

  itr :: Ord a => O.Olist a -> O.Olist a -> Maybe (O.Olist IAtom)
  itr s1 s2 = iter True s1 s2 1 []  -- True means that s1 == s2
    where iter b []     []     n nL = if b then Nothing else (Just (reverse nL))
          iter b []     (y:yL) n nL = iter False [] yL (n + 1) nL
          iter b (x:xL) (y:yL) n nL = case compare x y of
                                        EQ -> iter b xL yL (n + 1) (n:nL)
                                        GT -> iter False (x:xL) yL (n + 1) nL
                                        LT -> error "itr -- first list is not included by second list"

  iUni :: Ord a => [O.Olist a] -> (O.Olist a, [Maybe (O.Olist IAtom)])
  iUni sL = (aL, map (\ s -> itr s aL) sL)
    where aL = O.unionList sL

  unifyIdxPropForms :: Ord a => [IdxPropForm a] -> (O.Olist a, [PropForm IAtom])
  unifyIdxPropForms pL = (aL, ipropL)
    where (aL, maybeL) = iUni (map fst pL)
          update (iprop, Nothing) = iprop
          update (iprop, Just iL) = tr (nth iL) iprop
          ipropL = map update (zip (map snd pL) maybeL)

  unifyXForms :: Ord a => [XForm a] -> (O.Olist a, [IForm])
  unifyXForms xformL = (aL, iformL)
    where (aL, maybeL) = iUni (map fst xformL)
          update (iform, Nothing) = iform
          update (iform, Just iL) = iTr iL iform
          iformL = map update (zip (map snd xformL) maybeL)

  newAtomsXForm :: Ord a => XForm a -> O.Olist a -> XForm a
  newAtomsXForm (oldAts, iform) newAts = (newAts, updateIForm (updateList oldAts newAts) iform)
    where updateList :: Ord a => O.Olist a -> O.Olist a -> [Maybe IAtom]
          updateList oldAts newAts = updateList' oldAts 1 newAts
            where updateList' []     n newAts = []
                  updateList' (x:xL) n []     = L.replicate (length (x:xL)) Nothing
                  updateList' (x:xL) n (y:yL) = case compare x y of
                    LT -> Nothing : (updateList' xL n (y:yL))
                    EQ -> (Just n) : (updateList' xL (n + 1) yL)
                    GT -> updateList' (x:xL) (n + 1) yL
          updateIForm :: [Maybe IAtom] -> IForm -> IForm
          updateIForm maL iform = C.map (updateILine maL) iform
          updateILine :: [Maybe IAtom] -> ILine -> ILine
          updateILine maL iline = updateILine' 1 maL iline
            where updateILine' _ [] _ = C.empty
                  updateILine' n (x:xL) iline =
                    if C.isEmpty iline
                    then iline
                    else case compare n (iAtom (C.head iline)) of
                      LT -> updateILine' (n + 1) xL iline
                      EQ -> case x of
                             Nothing -> updateILine' (n + 1) xL (C.tail iline)
                             Just i  -> if iBool (C.head iline)
                                        then C.cons i          (updateILine' (n + 1) xL (C.tail iline))
                                        else C.cons (negLit i) (updateILine' (n + 1) xL (C.tail iline))

-- X-Prop conversions

  fromIdxPropForm :: Ord a => IdxPropForm a -> PropForm a
  fromIdxPropForm (s, iprop) = tr (nth s) iprop

  toIdxPropForm :: Ord a => PropForm a -> IdxPropForm a
  toIdxPropForm prop = (s, tr (idx s) prop)
    where s = propFormAtoms prop

  propFormAtoms :: Ord a => PropForm a -> O.Olist a
  propFormAtoms p = case p of
    (A a)   -> [a]
    F       -> []
    T       -> []
    (N p)   -> propFormAtoms p
    (CJ pL) -> O.unionList (map propFormAtoms pL)
    (DJ pL) -> O.unionList (map propFormAtoms pL)
    (SJ pL) -> O.unionList (map propFormAtoms pL)
    (EJ pL) -> O.unionList (map propFormAtoms pL)

-- I-Form conversion

  iLIT :: ILit -> PropForm IAtom
  iLIT l | l < 0 = N (A (negLit l))
         | l > 0 = A l
         | otherwise = error "iLIT -- zero literal"

  iNLC :: ILine -> PropForm IAtom
  iNLC line = CJ (map iLIT (C.toList line))

  iNLD :: ILine -> PropForm IAtom
  iNLD line = DJ (map iLIT (C.toList line))

  iCNF :: IForm -> PropForm IAtom
  iCNF form = CJ (map iNLD (C.toList form))

  iDNF :: IForm -> PropForm IAtom
  iDNF form = DJ (map iNLC (C.toList form))

-- X-Form conversion

  xLIT :: Ord a => XLit a -> PropForm a
  xLIT (s, l) = fromIdxPropForm (s, iLIT l)

  xNLC :: Ord a => XLine a -> PropForm a
  xNLC (s, line) = fromIdxPropForm (s, iNLC line)

  xNLD :: Ord a => XLine a -> PropForm a
  xNLD (s, line) = fromIdxPropForm (s, iNLD line)

  xCNF :: Ord a => XForm a -> PropForm a
  xCNF (s, form) = fromIdxPropForm (s, iCNF form)

  xDNF :: Ord a => XForm a -> PropForm a
  xDNF (s, form) = fromIdxPropForm (s, iDNF form)

-- type correctness and type constructors

  isIAtom :: Int -> Bool
  isIAtom n = n > 0

  isILit :: Int -> Bool
  isILit n = n /= 0

  isILine :: C.Costack Int -> Bool
  isILine x = iter (C.toList x)
    where iter [] = True
          iter [n] = isILit(n)
          iter (n1:n2:nL) = isILit(n1) && iAtom(n1) < iAtom(n2) && iter(n2:nL)

  isIForm :: C.Costack (C.Costack Int) -> Bool
  isIForm x = iter (C.toList x)
    where iter [] = True
          iter (c:cL) = (isILine c) && iter cL

  iLine :: [Int] -> ILine
  iLine iL = C.fromList (iter (zeroCheck iL))
    where iter [] = []
          iter [i] = [i]
          iter (j:i:iL) = if (abs j) < (abs i)
                          then j:(iter (i:iL))
                          else error ("IForm.iLine -- in literal order " ++ (show j) ++
                                      " is not before " ++ (show i))
          zeroCheck [] = []
          zeroCheck (i:iL) = if i == 0
                             then error "Iform.iLine -- there is a 0 in the list"
                             else i:(zeroCheck iL)

  iForm :: [[Int]] -> IForm
  iForm iLL = C.fromList (map iLine iLL)

-- literal operations

  iAtom :: ILit -> IAtom
  iAtom = abs

  iBool :: ILit -> Bool
  iBool l | l < 0 = False
          | l > 0 = True
          | l == 0 = error "IForm.iBool -- zero literal integer"

  negLit :: ILit -> ILit
  negLit = Prelude.negate

-- index lists

  lineIndices :: ILine -> O.Olist IAtom
  lineIndices line = map iAtom (C.toList line)

  formIndices :: IForm -> O.Olist IAtom
  formIndices form = O.unionList (C.toList (C.map lineIndices form))

-- syntactic sizes

  lineLength :: ILine -> Int
  lineLength = C.length

  formLength :: IForm -> Int
  formLength = C.length

  volume :: IForm -> Int
  volume form = C.foldr (+) 0 (C.map lineLength form)

-- ordered forms

  isOrderedForm :: IForm -> Bool
  isOrderedForm form = C.strictSorted form

  orderForm :: IForm -> IForm
  orderForm form = C.strictSort form

-- the propositional algebra operations

  atomForm :: IAtom -> IForm
  atomForm atom = C.singleton (C.singleton atom)

  botForm :: IForm
  botForm = C.empty

  topForm :: IForm
  topForm = C.singleton C.empty

  formJoinForm :: IForm -> IForm -> IForm
  formJoinForm form1 form2 = C.append form1 form2

  formListJoin :: [IForm] -> IForm
  formListJoin formL = C.concat formL

  lineMeetLine :: ILine -> ILine -> IForm
  lineMeetLine line1 line2 = jrec (line1, line2, C.empty)
    where jrec (first, second, third) =
            if C.isEmpty first
            then C.singleton (C.append third second)
            else if C.isEmpty second
                 then C.singleton (C.append third first)
                 else case compare (iAtom (C.head first)) (iAtom (C.head second)) of
                        LT -> jrec (C.tail first, second, C.cocons third (C.head first))
                        GT -> jrec (first, C.tail second, C.cocons third (C.head second))
                        EQ -> if (iBool (C.head first)) == (iBool (C.head second))
                              then jrec (C.tail first, C.tail second, C.cocons third (C.head first))
                              else C.empty

  lineMeetForm :: ILine -> IForm -> IForm
  lineMeetForm line form = formListJoin (map (lineMeetLine line) (C.toList form))

  formMeetForm :: IForm -> IForm -> IForm
  formMeetForm form1 form2 = formListJoin (map (\ line -> lineMeetForm line form2) (C.toList form1))

  formListMeet :: [IForm] -> IForm
  formListMeet [] = C.singleton C.empty
  formListMeet [form] = form
  formListMeet (form1:form2:formL) = formListMeet ((formMeetForm form1 form2) : formL)

  dualLine :: ILine -> IForm
  dualLine line = C.map C.singleton line

  dualForm :: IForm -> IForm
  dualForm form = formListMeet (map dualLine (C.toList form))

  invertLine :: ILine -> ILine
  invertLine = C.map negLit

  invertForm :: IForm -> IForm
  invertForm = C.map invertLine

  negLine :: ILine -> IForm
  negLine line = C.map (\ l -> (C.singleton (negLit l))) line

  negForm :: IForm -> IForm
  negForm form = formListMeet (map negLine (C.toList form))

  formCojoinLine :: IForm -> ILine -> IForm
  formCojoinLine form line = formJoinForm form (dualLine line)

  formCojoinForm :: IForm -> IForm -> IForm
  formCojoinForm form1 form2 = formListMeet (C.toList (C.map (formCojoinLine form1) form2))

  formAntijoinLine :: IForm -> ILine -> IForm
  formAntijoinLine form line = formJoinForm form (negLine line)

  formAntijoinForm :: IForm -> IForm -> IForm
  formAntijoinForm form1 form2 = formListMeet (C.toList (C.map (formAntijoinLine form1) form2))

  elimLine :: ILine -> O.Olist IAtom -> ILine
  elimLine line aL | C.isEmpty line = C.empty
                   | O.isEmpty aL = line
                   | otherwise = case compare (iAtom (C.head line)) (head aL) of
                                   LT -> C.cons (C.head line) (elimLine (C.tail line) aL)
                                   GT -> elimLine line (tail aL)
                                   EQ -> elimLine (C.tail line) (tail aL)

  elimForm :: IForm -> O.Olist IAtom -> IForm
  elimForm form aL = C.map (\ line -> (elimLine line aL)) form

  lineCovLine :: ILine -> ILine -> Bool
  lineCovLine line1 line2 | C.isEmpty line2 = True
                          | C.isEmpty line1 = False
                          | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
                                          LT -> lineCovLine (C.tail line1) line2
                                          GT -> False
                                          EQ -> if (iBool (C.head line1)) == (iBool (C.head line2))
                                                then lineCovLine (C.tail line1) (C.tail line2)
                                                else False

  lineCovForm :: ILine -> IForm -> Bool
  lineCovForm line form = if C.isEmpty form
                          then False
                          else if lineCovLine line (C.head form)
                               then True
                               else lineCovForm line (C.tail form)

  formCovForm :: IForm -> IForm -> Bool
  formCovForm form1 form2 = if C.isEmpty form1
                            then True
                            else if lineCovForm (C.head form1) form2
                                 then formCovForm (C.tail form1) form2
                                 else False

-- Generation of the prime and minimal form of two lines

  pairPartition :: ILine -> ILine -> (ILine,ILine,ILine,ILine)
  pairPartition line1 line2 = iter (C.empty, C.empty, C.empty, C.empty, line1, line2)
    where iter :: (ILine,ILine,ILine,ILine,ILine,ILine) -> (ILine,ILine,ILine,ILine)
          iter (piL, rhoL, sigmaL, tauL, line1, line2) =
            if C.isEmpty line1
            then (piL, rhoL, sigmaL, C.append tauL line2)
            else if C.isEmpty line2
                 then (piL, rhoL, C.append sigmaL line1, tauL)
                 else case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
                    LT -> iter (piL, rhoL, C.cocons sigmaL (C.head line1), tauL, C.tail line1, line2)
                    GT -> iter (piL, rhoL, sigmaL, C.cocons tauL (C.head line2), line1, C.tail line2)
                    EQ -> if iBool (C.head line1) ==  iBool (C.head line2)
                          then iter (C.cocons piL (C.head line1), rhoL, sigmaL, tauL, C.tail line1, C.tail line2)
                          else iter (piL, C.cocons rhoL (C.head line1), sigmaL, tauL, C.tail line1, C.tail line2)

  data CaseSymbol = NOOO | NOOP | NOPO | NOPP | NIOO | NIOP | NIPO | NIPP | NMNN
    deriving (Show, Read, Eq, Ord)

  caseSymbol :: ILine -> ILine -> CaseSymbol
  caseSymbol left right
    | p >= 0 && r == 0 && s == 0 && t == 0 = NOOO
    | p >= 0 && r == 0 && s == 0 && t >= 1 = NOOP
    | p >= 0 && r == 0 && s >= 1 && t == 0 = NOPO
    | p >= 0 && r == 0 && s >= 1 && t >= 1 = NOPP
    | p >= 0 && r == 1 && s == 0 && t == 0 = NIOO
    | p >= 0 && r == 1 && s == 0 && t >= 1 = NIOP
    | p >= 0 && r == 1 && s >= 1 && t == 0 = NIPO
    | p >= 0 && r == 1 && s >= 1 && t >= 1 = NIPP
    | p >= 0 && r >= 2 && s >= 0 && t >= 0 = NMNN
    where (piL, rhoL, sigmaL, tauL) = pairPartition left right
          (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)

-- First version

  pairPrim' :: ILine -> ILine -> IForm
  pairPrim' left right
    | p >= 0 && r == 0 && s == 0 && t == 0 = C.singleton left
    | p >= 0 && r == 0 && s == 0 && t >= 1 = C.singleton left
    | p >= 0 && r == 0 && s >= 1 && t == 0 = C.singleton right
    | p >= 0 && r == 0 && s >= 1 && t >= 1 = C.fromList [left,right]
    | p >= 0 && r == 1 && s == 0 && t == 0 = C.singleton piL
    | p >= 0 && r == 1 && s == 0 && t >= 1 = C.fromList [left, lineMerge piL tauL]
    | p >= 0 && r == 1 && s >= 1 && t == 0 = C.fromList [lineMerge piL sigmaL, right]
    | p >= 0 && r == 1 && s >= 1 && t >= 1 = C.fromList [left, right, lineMerge piL (lineMerge sigmaL tauL)]
    | p >= 0 && r >= 2 && s >= 0 && t >= 0 = C.fromList [left, right]
    where (piL, rhoL, sigmaL, tauL) = pairPartition left right
          (p,r,s,t) = (C.length piL, C.length rhoL, C.length sigmaL, C.length tauL)
          lineMerge line1 line2 | C.isEmpty line1 = line2
                                | C.isEmpty line2 = line1
                                | otherwise = case compare (iAtom (C.head line1)) (iAtom (C.head line2)) of
                                                LT -> C.cons (C.head line1) (lineMerge (C.tail line1) line2)
                                                GT -> C.cons (C.head line2) (lineMerge line1 (C.tail line2))

  pairMin' :: ILine -> ILine -> IForm
  pairMin' left right = C.take 2 (pairPrim' left right)

  xprim' :: ILine -> ILine -> (CaseSymbol, IForm)
  xprim' left right = (caseSymbol left right, pairPrim' left right)

  xmin' :: ILine -> ILine -> (CaseSymbol, IForm)
  xmin' left right = (caseSymbol left right, pairMin' left right)

-- Second, fast and final version

  xprim :: ILine -> ILine -> (CaseSymbol, IForm)
  xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)
    where xprec (left, left', right, right', c1, c2, c3, r, s, t)
            | r > 1 =
              (NMNN, C.fromList [C.append left left', C.append right right'])
            | C.isEmpty left' && r == 0 && s == 0 && C.isEmpty right' && t == 0 =
              (NOOO, C.singleton left)
            | C.isEmpty left' && r == 0 && s == 0 =
              (NOOP, C.singleton left)
            | C.isEmpty left' && r == 0 && s > 0 && C.isEmpty right' && t == 0 =
              (NOPO, C.singleton right)
            | C.isEmpty left' && r == 0 && s > 0 =
              (NOPP, C.fromList [left, C.append right right'])
            | C.isEmpty left' && r == 1 && s == 0 && C.isEmpty right' && t == 0 =
              (NIOO, C.singleton c1)
            | C.isEmpty left' && r == 1 && s == 0 =
              (NIOP, C.fromList [left, C.append c2 right'])
            | C.isEmpty left' && r == 1 && s > 0 && C.isEmpty right' && t == 0 =
              (NIPO, C.fromList [c1, C.append right right'])
            | C.isEmpty left' && r == 1 && s > 0 =
              (NIPP, C.fromList [left, C.append right right', C.append c3 right'])
            | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t == 0 =
              (NOPO, C.singleton right)
            | not (C.isEmpty left') && C.isEmpty right' && r == 0 && t > 0 =
              (NOPP, C.fromList [C.append left left', right])
            | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t == 0 =
              (NIPO, C.fromList [C.append c1 left', right])
            | not (C.isEmpty left') && C.isEmpty right' && r == 1 && t > 0 =
              (NIPP, C.fromList [C.append left left', right, C.append c3 left'])
            | not (C.isEmpty left') && not (C.isEmpty right') =
              let x = C.head left'
                  y = C.head right'
              in case compare (iAtom x) (iAtom y) of
                  LT -> xprec (C.cocons left x, C.tail left', right, right',
                               C.cocons c1 x, c2, C.cocons c3 x, r, s + 1, t)
                  GT -> xprec (left, left', C.cocons right y, C.tail right',
                               c1, C.cocons c2 y, C.cocons c3 y, r, s, t + 1)
                  EQ -> if iBool x == iBool y
                        then xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',
                                    C.cocons c1 x, C.cocons c2 y, C.cocons c3 y, r, s, t)
                        else xprec (C.cocons left x, C.tail left', C.cocons right y, C.tail right',
                                    c1, c2, c3, r + 1, s, t)

{-- old version of xprim
  xprim :: ILine -> ILine -> (CaseSymbol, IForm)
  xprim left right = xprec (C.empty, left, C.empty, right, C.empty, C.empty, C.empty, 0, 0, 0)
    where xprec (left, left', right, right', cboth, cleft, cright, r, s, t) =
            if r > 1
            then (NMNN, C.fromList [C.append left left', C.append right right'])
            else if C.isEmpty left'
                 then if r == 0
                      then if s == 0
                           then if (C.isEmpty right' && t == 0)
                                then (NOOO, C.singleton left)
                                else (NOOP, C.singleton left)
                           else if (C.isEmpty right' && t == 0)
                                then (NOPO, C.singleton right)
                                else (NOPP, C.fromList [left, C.append right right'])
                      else if s == 0
                           then if (C.isEmpty right' && t == 0)
                                then (NIOO, C.singleton cboth)
                                else (NIOP, C.fromList [left, C.append cleft right'])
                           else if (C.isEmpty right' && t == 0)
                                then (NIPO, C.fromList [cboth, C.append right right'])
                                else (NIPP, C.fromList [cboth, C.append right right', C.append cright right'])
                 else if C.isEmpty right'
                      then if r == 0
                           then if t == 0
                                then (NOPO, C.singleton right)
                                else (NOPP, C.fromList [C.append left left', right])
                           else if t == 0
                                then (NIPO, C.fromList [C.append cboth left', right])
                                else (NIPP, C.fromList [C.append left left', right, C.append cright left'])
                      else case compare (iAtom (C.head left')) (iAtom (C.head right')) of
                            LT -> xprec ( C.cocons left (C.head left'),
                                           C.tail left',
                                           right,
                                           right',
                                           C.cocons cboth (C.head left'),
                                           cleft,
                                           C.cocons cright (C.head left'),
                                           r, s+1, t)
                            GT -> xprec ( left,
                                          left',
                                          C.cocons right (C.head right'),
                                          C.tail right',
                                          cboth,
                                          C.cocons cleft (C.head right'),
                                          C.cocons cright (C.head right'),
                                          r, s, t+1)
                            EQ -> if iBool (C.head left') == iBool (C.head right')
                                  then xprec ( C.cocons left (C.head left'),
                                               C.tail left',
                                               C.cocons right (C.head right'),
                                               C.tail right',
                                               C.cocons cboth (C.head left'),
                                               C.cocons cleft (C.head left'),
                                               C.cocons cright (C.head right'),
                                               r, s, t)
                                  else xprec ( C.cocons left (C.head left'),
                                               C.tail left',
                                               C.cocons right (C.head right'),
                                               C.tail right',
                                               cboth, cleft, cright,
                                               r+1, s, t)
--}

  xmin :: ILine -> ILine -> (CaseSymbol, IForm)
  xmin left right = case xprim left right of
    (NIPP, form) -> (NIPP, C.take 2 form)
    (symb, form) -> (symb, form)

  pairPrim :: ILine -> ILine -> IForm
  pairPrim left right = snd (xprim left right)

  pairMin :: ILine -> ILine -> IForm
  pairMin left right = snd (xmin left right)

-- Pairwise minimality and complementary prime list

  isMinimalPair :: ILine -> ILine -> Bool
  isMinimalPair left right = [left, right] == C.toList (pairMin' left right)

  allPairs :: [a] -> [(a,a)]
  allPairs [] = []
  allPairs [x] = []
  allPairs (x:xL) = (iter x xL) ++ (allPairs xL)
     where iter x [] = []
           iter x (y:yL) = (x,y):(iter x yL)

  isPairwiseMinimal :: IForm -> Bool
  isPairwiseMinimal form = Prelude.all isMinPair (allPairs (C.toList form))
    where isMinPair (x,y) = isMinimalPair x y

-- C-Primes

  cPrime :: ILine -> ILine -> Maybe ILine
  cPrime left right = case xprim left right of
    (NIPP, form) -> Just (C.head (C.tail (C.tail form)))
    (symb, form) -> Nothing

  cPrimes :: IForm -> IForm
  cPrimes form = C.fromList (concat (map cp (allPairs (C.toList form))))
    where cp (left ,right) = case cPrime left right of
            Just line -> [line]
            Nothing   -> []

-- The M-Procedure and functions with pairwise minimal IForm results

  mrec :: (IForm,IForm,IForm) -> IForm
  mrec (gammaL, muL, muL') =
    if C.isEmpty gammaL
    then C.append muL muL'
    else if C.isEmpty muL'
         then mrec (C.tail gammaL, C.empty, C.cons (C.head gammaL) muL)
         else case xmin (C.head gammaL) (C.head muL') of
          (NOOO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')
          (NOOP, pp) -> mrec (C.append (C.tail gammaL) (C.tail muL'), C.empty, C.cons (C.head gammaL) muL)
          (NOPO, pp) -> mrec (C.tail gammaL, C.empty, C.append muL muL')
          (NOPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')
          (NIOO, pp) -> mrec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'))
          (NIOP, pp) -> mrec (C.concat [C.tail gammaL, C.tail pp, C.tail muL'], C.empty, C.cons (C.head gammaL) muL)
          (NIPO, pp) -> mrec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL')
          (NIPP, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')
          (NMNN, pp) -> mrec (gammaL, C.cocons muL (C.head muL'), C.tail muL')

  m2form :: IForm -> IForm
  m2form form = mrec (form, C.empty, C.empty)

  iformJoinM2form :: IForm -> IForm -> IForm
  iformJoinM2form iform m2form = mrec (iform, C.empty, m2form)

-- The P-Procedure and functions with prime IForm results

  primFormFromOrdM2form :: IForm -> IForm
  primFormFromOrdM2form ordM2form =
    let ordM2form' = orderForm (iformJoinM2form (cPrimes ordM2form) ordM2form)
    in if ordM2form' == ordM2form
       then ordM2form'
       else primFormFromOrdM2form ordM2form'

  primForm :: IForm -> IForm
  primForm iform = primFormFromOrdM2form $ orderForm $ m2form iform

  iformJoinPrimForm :: IForm -> IForm -> IForm
  iformJoinPrimForm iform pform = primFormFromOrdM2form $ orderForm $ iformJoinM2form iform pform

{-- the following prec, primform, ordPrimForm are obsolete -----------------------------------------------------------

  prec :: (IForm, IForm, IForm, IForm) -> IForm
  prec (gammaL, muL, muL', piL)
    | C.isEmpty gammaL && C.isEmpty piL =
      C.append muL muL'
    | C.isEmpty gammaL =
      prec (piL, C.empty, C.append muL muL', C.empty)
    | C.isEmpty muL' =
      prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)
    | otherwise =
      case xprim (C.head gammaL) (C.head muL') of
        (NOOO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
        (NOOP, pp) -> prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
        (NOPO, pp) -> prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
        (NOPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
        (NIOO, pp) -> prec (C.append (C.tail gammaL) pp, C.empty, C.append muL (C.tail muL'), C.empty)
        (NIOP, pp) -> prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
        (NIPO, pp) -> prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
        (NIPP, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)
        (NMNN, pp) -> prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)

  -- OLD VERSION --------

  prec :: (IForm, IForm, IForm, IForm) -> IForm
  prec (gammaL, muL, muL', piL) =
    if C.isEmpty gammaL
    then if C.isEmpty piL
         then C.append muL muL'
         else prec (piL, C.empty, C.append muL muL', C.empty)
    else if C.isEmpty muL'
         then prec (C.append (C.tail gammaL) piL, C.empty, C.cons (C.head gammaL) muL, C.empty)
         else case xprim (C.head gammaL) (C.head muL') of
          (NOOO, pp) ->
            prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
          (NOOP, pp) ->
            prec (C.concat [C.tail gammaL, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
          (NOPO, pp) ->
            prec (C.tail gammaL, C.empty, C.append muL muL', C.empty)
          (NOPP, pp) ->
            prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)
          (NIOO, pp) ->
            -- old version: --!!
            -- prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
            prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL (C.tail muL'), C.empty)
          (NIOP, pp) ->
            prec (C.concat [C.tail gammaL, C.tail pp, C.tail muL', piL], C.empty, C.cons (C.head gammaL) muL, C.empty)
          (NIPO, pp) ->
            prec (C.cocons (C.tail gammaL) (C.head pp), C.empty, C.append muL muL', C.empty)
          (NIPP, pp) ->
            prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', C.append (C.tail (C.tail pp)) piL)
          (NMNN, pp) ->
            prec (gammaL, C.cocons muL (C.head muL'), C.tail muL', piL)

  primForm :: IForm -> IForm
  primForm form = prec (form, C.empty, C.empty, C.empty)

  ordPrimForm :: IForm -> IForm
  ordPrimForm = orderForm . primForm
------------------------------------------------------------------------------------------------------------------}

-- XForm operations

  xformAtoms :: Ord a => XForm a -> O.Olist a
  xformAtoms (aL,iform) = aL

  xformRedAtoms :: Ord a => XForm a -> O.Olist a
  xformRedAtoms xform = O.difference (xformAtoms xform) (xformIrrAtoms xform)

  xformIrrAtoms :: Ord a => XForm a -> O.Olist a
  xformIrrAtoms (aL, iform) = iter aL 1 (formIndices iform)
    where iter aL n [] = []
          iter (a:aL) n (i:iL) = case compare n i of
            EQ -> a : (iter aL (n + 1) iL)
            LT -> iter aL (n + 1) (i:iL)

-- The XPDNF algebra

  instance Ord a => PropAlg a (XPDNF a) where
    at x = XPDNF ([x], atomForm 1)
    false = XPDNF ([], botForm)
    true = XPDNF ([], topForm)
    neg (XPDNF (aL, iform)) = XPDNF (aL, primForm (negForm iform))
    conj pL = XPDNF (aL, primForm (formListMeet iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
    disj pL = XPDNF (aL, primForm (formListJoin iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
    subj pL = XPDNF (aL, primForm (subj' iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
            subj' [] = topForm
            subj' [iform] = topForm
            subj' (iform1:iform2:iformL) = formMeetForm (formJoinForm (negForm iform1) iform2) (subj' (iform2:iformL))
    equij pL = XPDNF (aL, primForm (iform))
      where (aL, iformL) = unifyXForms (map (\ (XPDNF xform) -> xform) pL)
            iform = formJoinForm (formListMeet iformL) (negForm (formListJoin iformL))
    valid (XPDNF (aL, iform)) = iform == topForm
    satisfiable (XPDNF (aL, iform)) = iform /= botForm
    subvalent (XPDNF xform1) (XPDNF xform2) = formCovForm iform1 iform2
      where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]
    equivalent = (==)
    covalent p1 p2 = satisfiable (conj [p1, p2])
    properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2
    properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2
    atoms (XPDNF xform) = xformAtoms xform
    redAtoms (XPDNF xform) = xformRedAtoms xform
    irrAtoms (XPDNF xform) = xformIrrAtoms xform
    ext (XPDNF (xL, iform)) yL = XPDNF (yL', primForm iform')
      where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))
    infRed (XPDNF (xL, iform)) yL = XPDNF (yL', iform''')
      where iform' = primForm (dualForm iform)
            (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)
            iform''' = primForm (dualForm iform'')
    supRed (XPDNF xform) yL = XPDNF (yL', primForm iform')
      where (yL', iform') = newAtomsXForm xform (O.olist yL)
    infElim (XPDNF (xL, iform)) yL = infRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))
    supElim (XPDNF (xL, iform)) yL = supRed (XPDNF (xL, iform)) (O.difference xL (O.olist yL))
    toPropForm = fromXPDNF
    fromPropForm = toXPDNF

  instance Ord a => PropAlg a (XPCNF a) where
    at x = XPCNF ([x], atomForm 1)
    false = XPCNF ([], topForm)
    true = XPCNF ([], botForm)
    neg (XPCNF (aL, iform)) = XPCNF (aL, primForm (negForm iform))
    conj pL = XPCNF (aL, primForm (formListJoin iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
    disj pL = XPCNF (aL, primForm (formListMeet iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
    subj pL = XPCNF (aL, primForm (subj' iformL))
      where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
            subj' [] = botForm
            subj' [iform] = botForm
            subj' (iform1:iform2:iformL) = formJoinForm (formMeetForm (negForm iform1) iform2) (subj' (iform2:iformL))
    equij pL = XPCNF (aL, primForm (iform))
      where (aL, iformL) = unifyXForms (map (\ (XPCNF xform) -> xform) pL)
            iform = formMeetForm (formListJoin iformL) (negForm (formListMeet iformL))
    valid (XPCNF (aL, iform)) = iform == botForm
    satisfiable (XPCNF (aL, iform)) = iform /= topForm
    subvalent (XPCNF xform1) (XPCNF xform2) = formCovForm iform2 iform1
      where (aL, [iform1, iform2]) = unifyXForms [xform1, xform2]
    equivalent = (==)
    covalent p1 p2 = satisfiable (conj [p1, p2])
    properSubvalent p1 p2 = p1 /= p2 && subvalent p1 p2
    properDisvalent p1 p2 = satisfiable p1 && satisfiable p2 && disvalent p1 p2
    atoms (XPCNF xform) = xformAtoms xform
    redAtoms (XPCNF xform) = xformRedAtoms xform
    irrAtoms (XPCNF xform) = xformIrrAtoms xform
    ext (XPCNF (xL, iform)) yL = XPCNF (yL', primForm iform')
       where (yL', iform') = newAtomsXForm (xL, iform) (O.union xL (O.olist yL))
    infRed (XPCNF xform) yL = XPCNF (yL', primForm iform')
      where (yL', iform') = newAtomsXForm xform (O.olist yL)
    supRed (XPCNF (xL, iform)) yL = XPCNF (yL', iform''')
      where iform' = primForm (dualForm iform)
            (yL', iform'') = newAtomsXForm (xL, iform') (O.olist yL)
            iform''' = primForm (dualForm iform'')
    infElim (XPCNF (xL, iform)) yL = infRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))
    supElim (XPCNF (xL, iform)) yL = supRed (XPCNF (xL, iform)) (O.difference xL (O.olist yL))
    toPropForm = fromXPCNF
    fromPropForm = toXPCNF

  dualizeXPDNF :: Ord a => XPDNF a -> XPCNF a
  dualizeXPDNF (XPDNF (aL, iform)) = XPCNF (aL, primForm (dualForm iform))

  dualizeXPCNF :: Ord a => XPCNF a -> XPDNF a
  dualizeXPCNF (XPCNF (aL, iform)) = XPDNF (aL, primForm (dualForm iform))

-- The MixForm algebra

  instance Ord a => PropAlg a (MixForm a) where
    at x = PDNF ([x], atomForm 1)  -- alernatively = PCNF ([x], atomForm 1)
    false = PDNF ([], botForm)
    true = PCNF ([], botForm)
    neg (M2DNF (aL, iform)) = M2CNF (aL, invertForm iform)
    neg (M2CNF (aL, iform)) = M2DNF (aL, invertForm iform)
    neg (PDNF  (aL, iform)) = PCNF  (aL, invertForm iform)
    neg (PCNF  (aL, iform)) = PDNF  (aL, invertForm iform)
    conj [] = true
    conj [form] = form
    conj formL = M2CNF (aL, m2form (formListJoin iformL))
      where (aL,iformL) = unifyXForms cnfL
            cnfL = map cnf formL
            cnf (M2CNF (aL,iform)) = (aL, iform)
            cnf (M2DNF (aL,iform)) = (aL, dualForm iform)
            cnf (PCNF (aL,iform))  = (aL, iform)
            cnf (PDNF (aL,iform))  = (aL, dualForm iform)
    disj [] = false
    disj [form] = form
    disj formL = M2DNF (aL, m2form (formListJoin iformL))
      where (aL,iformL) = unifyXForms dnfL
            dnfL = map dnf formL
            dnf (M2CNF (aL,iform)) = (aL, dualForm iform)
            dnf (M2DNF (aL,iform)) = (aL, iform)
            dnf (PCNF (aL,iform))  = (aL, dualForm iform)
            dnf (PDNF (aL,iform))  = (aL, iform)
    subj [] = true
    subj [form] = PCNF (atoms form, botForm)
    subj formL = fromPropForm (SJ (map toPropForm formL))
    equij [] = true
    equij [form] = PCNF (atoms form, botForm)
    equij formL = fromPropForm (EJ (map toPropForm formL))
    valid (M2DNF (aL,iform)) = primForm iform == topForm
    valid (M2CNF (aL,iform)) = iform == botForm
    valid (PDNF  (aL,iform)) = iform == topForm
    valid (PCNF  (aL,iform)) = iform == botForm
    satisfiable (M2DNF (aL,iform)) = iform /= botForm
    satisfiable (M2CNF (aL,iform)) = primForm iform /= topForm
    satisfiable (PDNF  (aL,iform)) = iform /= botForm
    satisfiable (PCNF  (aL,iform)) = iform /= topForm
    subvalent form1 form2 = valid (subj [form1, form2])
    equivalent form1 form2 = valid (equij [form1, form2])
    covalent form1 form2 = satisfiable (conj [form1, form2])
    properSubvalent form1 form2 = subvalent form1 form2 && not (equivalent form1 form2)
    properDisvalent form1 form2 = disvalent form1 form2 && satisfiable form1 && satisfiable form2
    atoms (M2DNF (aL,iform)) = aL
    atoms (M2CNF (aL,iform)) = aL
    atoms (PDNF  (aL,iform)) = aL
    atoms (PCNF  (aL,iform)) = aL
    redAtoms (M2DNF (aL,iform)) = xformRedAtoms (aL, primForm iform)
    redAtoms (M2CNF (aL,iform)) = xformRedAtoms (aL, primForm iform)
    redAtoms (PDNF xform) = xformRedAtoms xform
    redAtoms (PCNF xform) = xformRedAtoms xform
    irrAtoms (M2DNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)
    irrAtoms (M2CNF (aL,iform)) = xformIrrAtoms (aL, primForm iform)
    irrAtoms (PDNF xform) = xformIrrAtoms xform
    irrAtoms (PCNF xform) = xformIrrAtoms xform
    ext (M2DNF xform) aL = M2DNF (newAtomsXForm xform aL)
    ext (M2CNF xform) aL = M2CNF (newAtomsXForm xform aL)
    ext (PDNF  xform) aL = PDNF  (newAtomsXForm xform aL)
    ext (PCNF  xform) aL = PCNF  (newAtomsXForm xform aL)

    infRed form yL = M2CNF (yL', m2form iform')
      where (PCNF (xL, iform)) = mixToPCNF form
            (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)
    supRed form yL = M2DNF (yL', m2form iform')
      where (PDNF (xL, iform)) = mixToPDNF form
            (yL',iform') = newAtomsXForm (xL, iform) (O.olist yL)
    infElim form yL = infRed form (O.difference (atoms form) (O.olist yL))
    supElim form yL = supRed form (O.difference (atoms form) (O.olist yL))
    toPropForm = fromMixForm
    fromPropForm = toM2DNF  -- alternatively: toM2CNF

  mixToPDNF :: Ord a => MixForm a -> MixForm a
  mixToPDNF (M2DNF (aL, iform)) = PDNF (aL, primForm iform)
  mixToPDNF (M2CNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))
  mixToPDNF (PDNF xform) = PDNF xform
  mixToPDNF (PCNF (aL, iform)) = PDNF (aL, primForm (dualForm iform))

  mixToPCNF :: Ord a => MixForm a -> MixForm a
  mixToPCNF (M2DNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))
  mixToPCNF (M2CNF (aL, iform)) = PCNF (aL, primForm iform)
  mixToPCNF (PDNF (aL, iform)) = PCNF (aL, primForm (dualForm iform))
  mixToPCNF (PCNF xform) = PCNF xform