module FastPropLogic (
IAtom,
ILit,
ILine,
IForm,
XLit,
XLine,
XForm,
XPDNF(..), XPCNF(..),
MixForm(..),
IdxPropForm,
tr,
iTr,
idx,
nth,
itr,
iUni,
unifyIdxPropForms,
unifyXForms,
fromIdxPropForm,
toIdxPropForm,
newAtomsXForm,
iLIT, iNLC, iNLD, iCNF, iDNF,
xLIT, xNLC, xNLD, xCNF, xDNF,
toXPDNF,
toXPCNF,
toM2DNF, toM2CNF,
fromXPDNF,
fromXPCNF,
fromMixForm,
isIAtom,
isILit,
isILine,
isIForm,
iLine,
iForm,
iAtom,
iBool,
negLit,
lineIndices,
formIndices,
lineLength,
formLength,
volume,
isOrderedForm,
orderForm,
atomForm,
botForm,
topForm,
formJoinForm,
formListJoin,
lineMeetLine,
lineMeetForm,
formMeetForm,
formListMeet,
dualLine,
dualForm,
invertLine,
invertForm,
negLine,
negForm,
formCojoinLine,
formCojoinForm,
formAntijoinLine,
formAntijoinForm,
elimLine,
elimForm,
lineCovLine,
lineCovForm,
formCovForm,
pairPartition,
CaseSymbol(..),
caseSymbol,
pairPrim',
pairMin',
xprim',
xmin',
xprim,
xmin,
pairPrim,
pairMin,
isMinimalPair,
allPairs,
isPairwiseMinimal,
cPrime,
cPrimes,
mrec,
m2form,
iformJoinM2form,
primForm,
iformJoinPrimForm,
xformAtoms,
xformRedAtoms,
xformIrrAtoms,
mixToPDNF,
mixToPCNF,
) where
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)
type IAtom = Int
type IdxPropForm a = (O.Olist a, PropForm IAtom)
type ILit = Int
type ILine = C.Costack ILit
type IForm = C.Costack ILine
type XLit a = (O.Olist a, ILit)
type XLine a = (O.Olist a, ILine)
type XForm a = (O.Olist a, IForm)
data XPDNF a = XPDNF (XForm a)
deriving (Show, Read, Eq)
data XPCNF a = XPCNF (XForm a)
deriving (Show, Read, Eq)
data MixForm a
= M2DNF (XForm a)
| M2CNF (XForm a)
| PDNF (XForm a)
| PCNF (XForm a)
deriving (Show, Read, Eq)
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
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)
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
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 []
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))
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)
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))
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)
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)
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
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))
lineLength :: ILine -> Int
lineLength = C.length
formLength :: IForm -> Int
formLength = C.length
volume :: IForm -> Int
volume form = C.foldr (+) 0 (C.map lineLength form)
isOrderedForm :: IForm -> Bool
isOrderedForm form = C.strictSorted form
orderForm :: IForm -> IForm
orderForm form = C.strictSort form
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
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)
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)
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)
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)
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
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 -> []
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)
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
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)
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))
instance Ord a => PropAlg a (MixForm a) where
at x = PDNF ([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
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