ampersand-3.0.2: src/lib/DatabaseDesign/Ampersand/Fspec/ToFspec/NormalForms.hs
{-# OPTIONS_GHC -Wall #-}
module DatabaseDesign.Ampersand.Fspec.ToFspec.NormalForms
(delta,conjNF,disjNF,normPA,nfProof,cfProof,dfProof,proofPA,simplify)
where
import DatabaseDesign.Ampersand.Basics
import DatabaseDesign.Ampersand.ADL1.ECArule
import DatabaseDesign.Ampersand.Classes.Relational
import DatabaseDesign.Ampersand.ADL1.Expression
import DatabaseDesign.Ampersand.Core.AbstractSyntaxTree
import DatabaseDesign.Ampersand.Fspec.Fspec
import DatabaseDesign.Ampersand.Fspec.ShowADL -- for debug purposes only
import Data.List (nub {- , intercalate -} )
-- import Debug.Trace
import Prelude hiding (head)
fatal :: Int -> String -> a
fatal = fatalMsg "Fspec.ToFspec.NormalForms"
head :: [a] -> a
head [] = fatal 30 "head must not be used on an empty list!"
head (a:_) = a
-- | This delta is meant to be used as a placeholder for inserting or removing links from expressions.
delta :: Sign -> Expression
delta sgn
= EDcD Sgn { decnm = "Delta"
, decsgn = sgn
, decprps = []
, decprps_calc = Nothing
, decprL = ""
, decprM = ""
, decprR = ""
, decMean = AMeaning [ -- A_Markup Dutch ReST (string2Blocks ReST "Delta is bedoeld als variabele, die de plaats in een expressie vasthoudt waar paren worden ingevoegd of verwijderd.")
-- , A_Markup English ReST (string2Blocks ReST "Delta is meant as a variable, to be used as a placeholder for inserting or removing links from expressions.")
]
, decfpos = Origin ("generated relation (Delta "++show sgn++")")
, deciss = True
, decusr = False
, decpat = ""
, decplug = True
}
{- Normalization of process algebra clauses -}
normPA :: PAclause -> PAclause
normPA pac = pac'
where (pac',_,_) = if null (proofPA pac) then fatal 21 "last: empty list" else last (proofPA pac)
type Proof a = [(a, [String], String)]
proofPA :: PAclause -> Proof PAclause
proofPA = {-reverse.take 3.reverse.-}pPA
where pPA pac' = case normstepPA pac' of
( _ , [] ,equ) -> [(pac',[] ,equ)] -- is dus (pac,[],"<=>")
(res,steps,equ) -> (pac',steps,equ):pPA res
{- The following rewriter is used to simplify the actions inside eca rules.
-- WHY? Stef, kan je uitleggen wat hier gebeurt? Enig commentaar is hier wel op zijn plaats.
-- Ook zou het helpen om bij de verschillende constructoren van PAclause een beschrijving te geven van het idee er achter.
-- BECAUSE! Kan ik wel uitleggen, maar het is een heel verhaal. Dat moet tzt in een wetenschappelijk artikel gebeuren, zodat het er goed staat.
-- Het idee is dat een procesalgebra is weergegeven in Haskell combinatoren (gedefinieerd als PAclause(..), zie ADL.ECArule).
-- Die kun je vervolgens normaliseren met herschrijfregels op basis van gelijkheden die gelden in de bewuste procesalgebra.
-- Helaas zijn de herschrijfregels nu nog hard gecodeerd, zodat ik voor PAclause een afzonderlijke Haskell functie moet schrijven.
-- Hierna volgt de normalisator voor relatiealgebra-expressies, genaamd normStep. Die heeft dezelfde structuur,
-- maar gebruikt herschrijfregels vanuit gelijkheden die gelden in relatiealgebra.
-}
normstepPA :: PAclause -> (PAclause,[String],String)
normstepPA pac = (res,ss,"<=>")
where
(res,ss) = norm pac
norm :: PAclause -> (PAclause,[String])
norm (CHC [] ms) = (Blk ms, ["Run out of options"])
norm (CHC [r] ms) = (r', ["Flatten ONE"])
where r' = case r of
Blk{} -> r
_ -> r{paMotiv = ms}
norm (CHC ds ms) | (not.null) msgs = (CHC ops ms, msgs)
| (not.null) [d | d<-ds, isCHC d] = (CHC (nub [ d' | d<-ds, d'<-if isCHC d then let CHC ops' _ = d in ops' else [d] ]) ms, ["flatten CHC"]) -- flatten
| (not.null) [Nop | Nop{}<-ops] = (Nop{paMotiv=ms}, ["Choose to do nothing"])
| (not.null) [Blk | Blk{}<-ops] = (CHC [op | op<-ops, not (isBlk op)] ms, ["Choose anything but block"])
| (not.null) doubles = (CHC [ head cl | cl<-eqClass (==) ds ] ms, ["remove double occurrences"])
| otherwise = (CHC ds ms, [])
where nds = map norm ds
msgs = concatMap snd nds
ops = map fst nds
doubles = [ d | cl<-eqClass (==) ds, length cl>1, d<-cl ]
norm (GCH [] ms) = (Blk ms, ["Run out of options"])
norm (GCH ds ms) | (not.null) [() | (_,links,_)<-normds, isFalse links] = (GCH [(tOp,links,p) | (tOp,links,p)<-normds, not (isFalse links)] ms, ["Remove provably empty guard(s)."])
| (not.null) [() | (_, _ ,p)<-normds, isNop p]
= (GCH [(tOp,links,p) | (tOp,links,p)<-normds, not (isNop p)] ms, ["Remove unneccessary SELECT."])
| (not.null) doubles = (GCH [ (fst3 (head cl), foldr1 (.\/.) (map snd3 cl), thd3 (head cl)) | cl<-eqCl (\(tOp,_,p)->(tOp,p)) ds ] ms, ["remove double occurrences"])
| otherwise = (GCH ds ms, [])
where normds = [ (tOp, conjNF links, let (p',_)=norm p in p') | (tOp,links,p)<-ds]
doubles = [ d | cl<-eqCl (\(tOp,_,p)->(tOp,p)) ds, length cl>1, d<-cl ]
norm (ALL [] ms) = (Nop ms, ["ALL [] = No Operation"])
norm (ALL [d] ms) = (d', ["Flatten ONE"])
where d' = case d of
Blk{} -> d
_ -> d{paMotiv = ms}
norm (ALL ds ms) | (not.null) msgs = (ALL ops ms, msgs)
| (not.null) [d | d<-ds, isAll d] = (ALL (nub [ d' | d<-ds, d'<-if isAll d then let ALL ops' _ = d in ops' else [d] ]) ms, ["flatten ALL"]) -- flatten
| (not.null) [Blk | Blk{}<-ops] = (Blk{paMotiv = [m | op@Blk{}<-ops,m<-paMotiv op]}, ["Block all"])
| (not.null) [Nop | Nop{}<-ops] = (ALL [op | op<-ops, not (isNop op)] ms, ["Ignore Nop"])
| (not.null) doubles = (CHC [ head cl | cl<-eqClass (==) ds ] ms, ["remove double occurrences"])
| (not.null) long = (ALL ds' ms, ["Take the expressions for "++commaEng "and" [name (paTo (head cl)) |cl<-long]++"together"])
| otherwise = (ALL ds ms, [])
where ds' = [ let p=head cl in
if length cl==1 then p else p{paDelta=disjNF (foldr1 (.\/.) [paDelta c | c<-cl]), paMotiv=concatMap paMotiv cl}
| cl<-dCls {- not (null cl) is guaranteed by eqCl -} ]
++[d | d<-ds, not (isDo d)]
nds = map norm ds
msgs = concatMap snd nds
ops = map fst nds
doubles = [ d | cl<-eqClass (==) ds, length cl>1, d<-cl ]
dCls :: [[PAclause]]
dCls = eqCl to [d | d<-ds, isDo d]
long :: [[PAclause]]
long = [cl | cl<-dCls, length cl>1]
to d = case d of
Do{} -> (paSrt d, paTo d)
_ -> fatal 74 "illegal call of to(d)"
norm (New c p ms) = ( case p' of
Blk{} -> p'{paMotiv = ms}
_ -> New c (\x->let (p'', _) = norm (p x) in p'') ms
, msgs)
where (p', msgs) = norm (p "x")
norm (Rmv c p ms) = ( case p' of
Blk{} -> p'{paMotiv = ms}
_ -> Rmv c (\x->let (p'', _) = norm (p x) in p'') ms
, msgs)
where (p', msgs) = norm (p "x")
norm p = (p, [])
{- Normalization of expressions -}
simplify :: Expression -> Expression
simplify expr = expr'
where (expr',_,_) = if null (simpProof shw expr) then fatal 101 "last: empty list" else last (simpProof shw expr)
shw _ = ""
simpProof :: (Expression -> String) -> Expression -> Proof Expression
simpProof shw expr
= if expr==res
then [(expr,[],"<=>")]
else (expr,steps,equ):simpProof shw res
where (res,steps,equ) = normStep shw True True True expr
-- | The purpose of "normStep" is to elaborate a single step in a rewrite process,
-- in which the expression is normalized by means of rewrite rules.
-- This function can be used for simplification, which means that an Expression is standardized
-- using associativity and other 'trivial' rules only.
-- These 'trivial' rules do not produce a step in the proof.
-- Use normstep shw eq True expr to do simplification only.
-- Use normstep shw eq False expr to obtain a single proof step or none when no rule is applicable.
-- This function returns a resulting expression that is closer to a normal form.
-- The normal form is not unique. This function simply uses the first rewrite rule it encounters.
normStep :: (Expression -> String) -> Bool -> Bool -> Bool ->
Expression -> (Expression,[String],String) -- This might be generalized to "Expression" if it weren't for the fact that flip is embedded in the Relation type.
normStep shw -- a function to print an expression. Might be "showADL"
eq -- If eq==True, only equivalences are used. Otherwise, implications are used as well.
dnf -- If dnf==True, the result is in disjunctive normal form, otherwise in conjunctive normal form
simpl -- If True, only simplification rules are used, which is a subset of all rules. Consequently, simplification is implied by normalization.
expr = (res,ss,equ)
where
(res,ss,equ) = nM True expr []
nM :: Bool -> Expression -> [Expression] -> (Expression,[String],String)
-- posCpl indicates whether the expression is positive under a complement. It is False when expr is inside a complemented expression.
nM posCpl (EEqu (l,r)) _ | simpl = (t .==. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l [] -- TODO: the use of posCpl is erroneous
(f,steps',equ'') = nM posCpl r [] -- TODO: the use of posCpl is erroneous
nM posCpl (EImp (l,r)) _ | simpl = (t .|-. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM (not posCpl) l []
(f,steps',equ'') = nM posCpl r []
nM posCpl (EUni (EUni (l,k),r)) rs = nM posCpl (l .\/. (k .\/. r)) rs -- standardize, using associativity of .\/.
nM posCpl (EUni (l,r)) rs | simpl = (t .\/. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM posCpl (EIsc (EIsc (l,k),r)) rs = nM posCpl (l ./\. (k ./\. r)) rs -- standardize, using associativity of ./\.
nM posCpl (EIsc (l,r)) rs | simpl = (t ./\. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM posCpl (ECps (ECps (l,k),r)) rs = nM posCpl (l .:. (k .:. r)) rs -- standardize, using associativity of .:.
-- Note: function shiftL and shiftR make use of the fact that this normalizes to (l .:. (k .:. r))
nM posCpl (ECps (l,r)) rs | simpl = (t .:. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM posCpl (ELrs (l,r)) _ | simpl = (t ./. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM (not posCpl) r []
nM posCpl (ERrs (l,r)) _ | simpl = (t .\. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM (not posCpl) l []
(f,steps',equ'') = nM posCpl r []
nM posCpl (EDia (l,r)) _ | simpl = (t .<>. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l [] -- TODO: the use of posCpl is erroneous
(f,steps',equ'') = nM posCpl r [] -- TODO: the use of posCpl is erroneous
nM posCpl (ERad (ERad (l,k),r)) rs = nM posCpl (l .!. (k .!. r)) rs -- standardize, using associativity of .!.
nM posCpl (ERad (l,r)) rs | simpl = (t .!. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM posCpl (EPrd (EPrd (l,k),r)) rs = nM posCpl (l .*. (k .*. r)) rs -- standardize, using associativity of .*.
nM posCpl (EPrd (l,r)) _ | simpl = (t .*. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r []
nM posCpl (EKl0 e) _ = (EKl0 res', steps, equ')
where (res',steps,equ') = nM posCpl e []
nM posCpl (EKl1 e) _ = (EKl1 res', steps, equ')
where (res',steps,equ') = nM posCpl e []
nM posCpl (ECpl (ECpl e)) rs = nM posCpl e rs
nM posCpl (ECpl e) _ | simpl = (notCpl res',steps,equ')
where (res',steps,equ') = nM (not posCpl) e []
nM posCpl (EBrk e) _ = nM posCpl e []
nM posCpl (EFlp (ECpl e)) rs = nM posCpl (notCpl (flp e)) rs
nM _ x _ | simpl = (x,[],"<=>")
-- up to here, simplification has been treated. The remaining rules can safely assume simpl==False
nM _ (EEqu (l,r)) _ = ((l .|-. r) ./\. (r .|-. l), ["remove ="],"<=>")
nM _ (EImp (x,ELrs (z,y))) _ = (x .:. y .|-. z, ["remove left residual (/)"],"<=>")
nM _ (EImp (y,ERrs (x,z))) _ = (x .:. y .|-. z, ["remove right residual (\\)"],"<=>")
nM _ (EImp (l,r)) _ = (notCpl l .\/. r, ["remove |-"],"<=>")
-- nM posCpl e@(ECpl EIsc{}) _ | posCpl==dnf = (deMorganEIsc e, ["De Morgan"], "<=>")
-- nM posCpl e@(ECpl EUni{}) _ | posCpl/=dnf = (deMorganEUni e, ["De Morgan"], "<=>")
nM _ e@(ECpl EIsc{}) _ = (deMorganEIsc e, ["De Morgan"], "<=>")
nM _ e@(ECpl EUni{}) _ = (deMorganEUni e, ["De Morgan"], "<=>")
nM _ e@(ECpl (ERad (_,ECpl{}))) _ = (deMorganERad e, ["De Morgan"], "<=>")
nM _ e@(ECpl (ERad (ECpl{},_))) _ = (deMorganERad e, ["De Morgan"], "<=>")
nM _ e@(ECpl (ECps (ECpl{},ECpl{}))) _ = (deMorganECps e, ["De Morgan"], "<=>")
nM posCpl (ECpl e) _ = (notCpl res',steps,equ')
where (res',steps,equ') = nM (not posCpl) e []
nM _ (ECps (EEps c (Sign s _),EEps c' (Sign _ t'))) _ | c ==c' = (EEps c (Sign s t'), [], "<=>")
nM _ (ECps (EEps c (Sign s t),EEps c' (Sign _ t'))) _ | c ==t = (EEps c' (Sign s t'), [], "<=>")
nM _ (ECps (EEps c (Sign s _),EEps c' (Sign s' t'))) _ | s'==c' = (EEps c (Sign s t'), [], "<=>")
nM _ (ECps (EEps c (Sign s _),ECps(EEps c' (Sign _ t'),r))) _ | c ==c' = (ECps (EEps c (Sign s t'),r), [], "<=>")
nM _ (ECps (EEps c (Sign s t),ECps(EEps c' (Sign _ t'),r))) _ | c ==t = (ECps (EEps c' (Sign s t'),r), [], "<=>")
nM _ (ECps (EEps c (Sign s _),ECps(EEps c' (Sign s' t'),r))) _ | s'==c' = (ECps (EEps c (Sign s t'),r), [], "<=>")
nM _ (ECps (ERrs (x,e),y)) _ | not eq && isIdent e = (ERrs (x,y), ["Jipsen&Tsinakis: (x\\I);y |- x\\y"], "==>")
nM _ (ECps (x,ELrs (e,y))) _ | not eq && isIdent e = (ELrs (x,y), ["Jipsen&Tsinakis: x;(I/y) |- x/y"], "==>")
nM _ (ECps (ERrs (x,y),z)) _ | not eq = (ERrs (x,ECps (y,z)), ["Jipsen&Tsinakis: (x\\y);z |- x\\(y;z)"], "==>")
nM _ (ECps (x,ELrs (y,z))) _ | not eq = (ERrs (x,ECps (y,z)), ["Jipsen&Tsinakis: x;(y/z) |- (x;y)/z"], "==>")
nM _ (ECps (ERrs (x,y),ERrs (y',z))) _ | not eq && y==y' = (ERrs (x,z), ["Jipsen&Tsinakis: (x\\y);(y\\z) |- x\\z"], "==>")
nM _ (ECps (ELrs (x,y),ELrs (y',z))) _ | not eq && y==y' = (ERrs (x,z), ["Jipsen&Tsinakis: (x/y);(y/z) |- x/z"], "==>")
nM _ (ECps (ERrs (x,y),ERrs (y',z))) _ | y==y' && x==y && x==z = (ERrs (x,z), ["Jipsen&Tsinakis: (x\\x);(x\\x) = x\\x"], "<=>")
nM _ (ECps (ELrs (x,y),ELrs (y',z))) _ | y==y' && x==y && x==z = (ERrs (x,z), ["Jipsen&Tsinakis: (x/x);(x/x) = x/x"], "<=>")
nM _ (ECps (x,ERrs (y,z))) _ | x==y && x==z = (x, ["Jipsen&Tsinakis: x;(x\\x) = x"], "<=>")
nM _ (ECps (ELrs (x,y),z)) _ | x==z && y==z = (x, ["Jipsen&Tsinakis: (x/x);x = x"], "<=>")
nM _ (ECps (l,r)) _ | isIdent l = (r, ["I;x = x"], "<=>")
nM _ (ECps (l,r)) _ | isIdent r = (l, ["x;I = x"], "<=>")
nM True (ECps (r,ERad (s,q))) _ | not eq = ((r.:.s).!.q, ["Peirce: r;(s!q) |- (r;s)!q"],"==>")
nM True (ECps (ERad (r,s),q)) _ | not eq = (r.!.(s.:.q), ["Peirce: (r!s);q |- r!(s;q)"],"==>")
nM True (ECps (EIsc (r,s),q)) _ | not eq = ((r.:.q)./\.(s.:.q), ["distribute ; over /\\"],"==>")
nM True (ECps (r,EIsc (s,q))) _ | not eq = ((r.:.s)./\.(r.:.q), ["distribute ; over /\\"],"==>")
nM _ (ECps (EUni (q,s),r)) _ = ((q.:.r).\/.(s.:.r), ["distribute ; over \\/"],"<=>")
nM _ (ECps (l,EUni (q,s))) _ = ((l.:.q).\/.(l.:.s), ["distribute ; over \\/"],"<=>")
nM _ x@(ECps (l@EFlp{},r)) _ | not eq && flp l==r && isInj l = (EDcI (source x), ["r~;r |- I (r is univalent)"], "==>")
nM _ x@(ECps (l, r)) _ | not eq && l==flp r && isInj l = (EDcI (source x), ["r;r~ |- I (r is injective)"], "==>")
nM _ x@(ECps (l@EFlp{},r)) _ | flp l==r && isInj l && isTot l = (EDcI (source x), ["r~;r=I because r is univalent and surjective"], "<=>")
nM _ x@(ECps (l, r)) _ | l==flp r && isInj l && isTot l = (EDcI (source x), ["r;r~=I because r is injective and total"], "<=>")
nM posCpl (ECps (l,r)) rs = (t .:. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM _ x@(EEps i sgn) _ | source sgn==i && i==target sgn = (EDcI i, ["source and target are equal to "++name i++", so "++showADL x++"="++showADL (EDcI i)], "<=>")
nM _ (ELrs (ECps (x,y),z)) _ | not eq && y==z = (x, ["(x;y)/y |- x"], "==>")
nM _ (ELrs (ECps (x,y),z)) _ | not eq && flp x==z= (flp y, [case (x, y) of
(EFlp _, EFlp _) -> "(SJ) (x~;y~)/x |- y"
( _, EFlp _) -> "(SJ) (x;y~)/x~ |- y"
(EFlp _, _) -> "(SJ) (x~;y)/x |- y~"
( _, _) -> "(SJ) (x;y)/x~ |- y~"], "==>")
nM _ (ELrs (ELrs (x,z),y)) _ = (ELrs (x,ECps (y,z)), ["Jipsen&Tsinakis: x/yz = (x/z)/y"], "<=>")
nM posCpl (ELrs (l,r)) _ = (t ./. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM (not posCpl) r []
nM _ (ERrs (y,ERrs (x,z))) _ = (ERrs (ECps (x,y),z), ["Jipsen&Tsinakis: xy\\z = y\\(x\\z)"], "<=>")
nM _ (ERrs (x,ECps (y,z))) _ | not eq && x==y = (z, ["x\\(x;y) |- y"], "==>")
nM posCpl (ERrs (l,r)) _ = (t .\. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM (not posCpl) l []
(f,steps',equ'') = nM posCpl r []
nM posCpl (EDia (l,r)) _ = (t .<>. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r []
nM _ (ERad (l,r)) _ | isImin l = (r, ["-I!x = x"], "<=>")
nM _ (ERad (l,r)) _ | isImin r = (l, ["x!-I = x"], "<=>")
-- nM False (ERad (ECps (r,s),q)) _ | not eq = (r.:.(s.!.q), ["Peirce: (r;s)!q |- r;(s!q)"],"==>") -- SJ 20131124 TODO: check this rule. It is wrong!
-- nM False (ERad (r,ECps (s,q))) _ | not eq = ((r.!.s).:.q, ["Peirce: (r!s);q |- r!(s;q)"],"==>") -- SJ 20131124 TODO: check this rule. It is wrong!
nM False (ERad (EUni (r,s),q)) _ | not eq = ((r.!.q).\/.(s.!.q), ["distribute ! over \\/"],"==>")
nM False (ERad (r,EUni (s,q))) _ | not eq = ((r.!.s).\/.(r.!.q), ["distribute ! over \\/"],"==>")
nM _ (ERad (EIsc (q,s),r)) _ = ((q.!.r)./\.(s.!.r), ["distribute ! over /\\"],"<=>")
nM _ (ERad (l,EIsc (q,s))) _ = ((l.!.q)./\.(l.!.s), ["distribute ! over /\\"],"<=>")
nM _ (ERad(ECpl l,r)) _ = (flp l .\. r, [case l of EFlp{} -> "-l~!r = l\\r"; _ -> "-l!r = l~\\r"], "<=>")
nM _ (ERad(l,ECpl r)) _ = (l ./. flp r, [case r of EFlp{} -> "l!-r~ = l/r"; _ -> "l!-r = l/r~"], "<=>")
nM posCpl (ERad (l,r)) rs = (t .!. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
nM _ (EPrd (l,EPrd (_,r))) _ = (l .*. r, ["eliminate middle in cartesian product"], "<=>")
nM posCpl (EPrd (l,r)) _ = (t .*. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r []
nM posCpl (EIsc (EUni (l,k),r)) _ | posCpl==dnf = ((l./\.r) .\/. (k./\.r), ["distribute /\\ over \\/"],"<=>")
nM posCpl (EIsc (l,EUni (k,r))) _ | posCpl==dnf = ((l./\.k) .\/. (l./\.r), ["distribute /\\ over \\/"],"<=>")
nM posCpl x@(EIsc (l,r)) rs
-- Absorb equals: r/\r --> r
| or [length cl>1 |cl<-absorbClasses]
= ( case absorbClasses of [] -> fatal 243 "Going into foldr1 with empty absorbClasses"; _ -> foldr1 (./\.) [head cl | cl<-absorbClasses]
, [shw e++" /\\ "++shw e++" = "++shw e | cl<-absorbClasses, length cl>1, let e=head cl]
, "<=>"
)
-- Absorb True: r/\V --> r
| isTrue l = (r, ["V/\\x = x"], "<=>")
| isTrue r = (l, ["x/\\V = x"], "<=>")
-- Inconsistency: r/\-r --> False
| not (null incons)
= let i = head incons in (notCpl (EDcV (sign i)), [shw (notCpl i)++" /\\ "++shw i++" = V-"], "<=>")
-- Inconsistency: x/\\V- --> False
| isFalse l = (notCpl (EDcV (sign x)), ["-V/\\x = -V"], "<=>")
| isFalse r = (notCpl (EDcV (sign x)), ["x/\\-V = -V"], "<=>")
-- Absorb if r is antisymmetric: r/\r~ --> I
| not eq && or [length cl>1 |cl<-absorbAsy]
= ( foldr1 (./\.) [if length cl>1 then EDcI (source e) else e | cl<-absorbAsy, let e=head cl]
, [shw e++" /\\ "++shw (flp e)++" |- I, because"++shw e++" is antisymmetric" | cl<-absorbAsy, let e=head cl]
, "==>"
)
-- Absorb if r is antisymmetric and reflexive: r/\r~ = I
| or [length cl>1 |cl<-absorbAsyRfx]
= ( foldr1 (./\.) [if length cl>1 then EDcI (source e) else e | cl<-absorbAsyRfx, let e=head cl]
, [shw e++" /\\ "++shw (flp e)++" = I, because"++shw e++" is antisymmetric and reflexive" | cl<-absorbAsyRfx, let e=head cl]
, "<=>"
)
-- Absorb: (x\\/y)/\\y = y
| isEUni l && not (null absor0)
= let t'=head absor0 in (r, ["absorb "++shw l++" because of "++shw t'++", using law (x\\/y)/\\y = y"], "<=>")
| isEUni r && not (null absor0')
= let t'=head absor0' in (r, ["absorb "++shw r++" because of "++shw t'++", using law (x\\/y)/\\x = x"], "<=>")
-- Absorb: (x\\/-y)/\\y = x/\\y
| isEUni l && not (null absor1)
= ( case head absor1 of
(_,[]) -> r
(_,ts) -> foldr1 (.\/.) ts ./\. r
, ["absorb "++shw t'++", using law (x\\/-y)/\\y = x/\\y" | (t',_)<-absor1]
, "<=>"
)
| isEUni r && not (null absor1')
= ( case head absor1' of
(_,[]) -> l
(_,ts) -> l ./\. foldr1 (.\/.) ts
, ["absorb "++shw t'++", using law x/\\(y\\/-x) = x/\\y" | (t',_)<-absor1']
, "<=>"
)
| otherwise = (t ./\. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
absorbClasses = eqClass (==) (exprIsc2list l++exprIsc2list r)
incons = [conjunct |conjunct<-exprIsc2list r,conjunct==notCpl l]
absor0 = [disjunct | disjunct<-exprUni2list l, f'<-rs++exprIsc2list r, disjunct==f']
absor0' = [disjunct | disjunct<-exprUni2list r, f'<-rs++exprIsc2list l, disjunct==f']
absor1 = [(disjunct, exprUni2list l>-[disjunct]) | disjunct<-exprUni2list l, ECpl f'<-rs++exprIsc2list r, disjunct==f']++
[(disjunct, exprUni2list l>-[disjunct]) | disjunct@(ECpl t')<-exprUni2list l, f'<-rs++exprIsc2list r, t'==f']
absor1' = [(disjunct, exprUni2list r>-[disjunct]) | disjunct<-exprUni2list r, ECpl f'<-rs++exprIsc2list l, disjunct==f']++
[(disjunct, exprUni2list r>-[disjunct]) | disjunct@(ECpl t')<-exprUni2list r, f'<-rs++exprIsc2list l, t'==f']
absorbAsy = eqClass same eList where e `same` e' = isAsy e && isAsy e' && e == flp e'
absorbAsyRfx = eqClass same eList where e `same` e' = isRfx e && isAsy e && isRfx e' && isAsy e' && e == flp e'
eList = rs++exprIsc2list l++exprIsc2list r
nM posCpl (EUni (EIsc (l,k),r)) _ | posCpl/=dnf = ((l.\/.r) ./\. (k.\/.r), ["distribute \\/ over /\\"],"<=>")
nM posCpl (EUni (l,EIsc (k,r))) _ | posCpl/=dnf = ((l.\/.k) ./\. (l.\/.r), ["distribute \\/ over /\\"],"<=>")
nM posCpl x@(EUni (l,r)) rs
-- Absorb equals: r\/r --> r
| or [length cl>1 |cl<-absorbClasses] -- yields False if absorbClasses is empty
= ( foldr1 (.\/.) [head cl | cl<-absorbClasses] -- cl cannot be empty, because it is made by eqClass
, [shw e++" \\/ "++shw e++" = "++shw e | cl<-absorbClasses, length cl>1, let e=head cl]
, "<=>"
)
-- Tautologies:
| (not.null) tauts = (EDcV (sign x), ["let e = "++ shw (head tauts)++". Since -e\\/e = V we get"], "<=>") -- r\/-r --> V
| isTrue l = (EDcV (sign x), ["V\\/x = V"], "<=>") -- r\/V --> V
| isTrue r = (EDcV (sign x), ["x\\/V = V"], "<=>")
-- Absorb -V: r\/-V --> r
| isFalse l = (r, ["-V\\/x = x"], "<=>")
| isFalse r = (l, ["x\\/-V = x"], "<=>")
-- Absorb: (x/\\y)\\/y = y
| isEIsc l && not (null absor0) = let t'=head absor0 in (r, ["absorb "++shw l++" because of "++shw t'++", using law (x/\\y)\\/y = y"], "<=>")
| isEIsc r && not (null absor0') = let t'=head absor0' in (r, ["absorb "++shw r++" because of "++shw t'++", using law (x/\\y)\\/x = x"], "<=>")
-- Absorb: (x/\\-y)\\/y = x\\/y
| isEIsc l && not (null absor1)
= ( case head absor1 of
(_,[]) -> r
(_,ts) -> foldr1 (./\.) ts .\/. r
, ["absorb "++shw t'++", using law (x/\\-y)\\/y = x\\/y" | (t',_)<-absor1]
, "<=>"
)
| isEIsc r && not (null absor1')
= ( case head absor1' of
(_,[]) -> l
(_,ts) -> l .\/. foldr1 (./\.) ts
, ["absorb "++shw t'++", using law x\\/(y/\\-x) = x\\/y" | (t',_)<-absor1' ]
, "<=>"
)
| otherwise = (t .\/. f, steps++steps', fEqu [equ',equ''])
where (t,steps, equ') = nM posCpl l []
(f,steps',equ'') = nM posCpl r (l:rs)
-- absorption can take place if two terms are equal. So let us make a list of equal terms: absorbClasses (for substituting r\/r by r)
absorbClasses = eqClass (==) (exprUni2list l++exprUni2list r)
-- tautologies occur if -r\/r, so we are looking for pairs, (x,l) such that x== -l
tauts = [t' |disjunct<-exprUni2list r,disjunct==notCpl l, ECpl t'<-[disjunct,l]]
absor0 = [t' | t'<-exprIsc2list l, f'<-rs++exprUni2list r, t'==f']
absor0' = [t' | t'<-exprIsc2list r, f'<-rs++exprUni2list l, t'==f']
absor1 = [(t', exprIsc2list l>-[t']) | t'<-exprIsc2list l, ECpl f'<-rs++exprUni2list r, t'==f']++[(e, exprIsc2list l>-[e]) | e@(ECpl t')<-exprIsc2list l, f'<-rs++exprUni2list r, t'==f']
absor1' = [(t', exprIsc2list r>-[t']) | t'<-exprIsc2list r, ECpl f'<-rs++exprUni2list l, t'==f']++[(e, exprIsc2list r>-[e]) | e@(ECpl t')<-exprIsc2list r, f'<-rs++exprUni2list l, t'==f']
nM _ (EFlp e) _ | isSym e = (e,[shw e++" is symmetric"],"<=>")
nM _ x _ = (x,[],"<=>")
fEqu :: [String] -> String
fEqu ss = if and [s=="<=>" | s<-ss] then "<=>" else "==>"
nfProof :: (Expression -> String) -> Expression -> Proof Expression
nfProof shw = nfPr shw True True -- The first boolean True means that clauses are derived using <=> derivations. The second True means that a disjunctive normal form is produced.
nfPr :: (Expression -> String) -> Bool -> Bool -> Expression -> [(Expression, [String], String)]
nfPr shw eq dnf expr
= {-if showADL expr=="r \\/ s"
then fatal 360 ("Diagnose expr: "++showADL expr++"\n"++
"eq: "++show eq++"\n"++
"dnf: "++show eq++"\n"++
"res: "++showADL res++"\n"++
"expr==res: "++show (expr==res)
) else-}
if expr==res
then [(expr,[],"<=>")]
else (expr,steps,equ):nfPr shw eq dnf (simplify res)
where (res,steps,equ) = normStep shw eq dnf False expr
cfProof :: (Expression -> String) -> Expression -> Proof Expression
cfProof shw expr
= [line | step, line<-init pr]++
[line | step', line<-init pr']++
[last ([(expr,[],"<=>")]++
[line | step, line<-pr]++
[line | step', line<-pr']
)]
where pr = nfPr shw True False (simplify expr)
(expr',_,_) = if null pr then fatal 328 "last: empty list" else last pr
step = simplify expr/=expr' -- obsolete? || and [null s | (_,ss,_)<-pr, s<-ss]
pr' = nfPr shw True False (simplify expr')
step' = simplify expr'/=simplify expr'' -- obsolete? || and [null s | (_,ss,_)<-pr', s<-ss]
(expr'',_,_) = if null pr' then fatal 337 "last: empty list" else last pr'
conjNF :: Expression -> Expression
conjNF expr = e where (e,_,_) = if null (cfProof (\_->"") expr) then fatal 340 "last: empty list" else last (cfProof (\_->"") expr)
disjNF :: Expression -> Expression
disjNF expr = e where (e,_,_) = if null (dfProof (\_->"") expr) then fatal 343 "last: empty list" else last (dfProof (\_->"") expr)
dfProof :: (Expression -> String) -> Expression -> Proof Expression
dfProof shw expr
= [line | step, line<-init pr]++
[line | step', line<-init pr']++
[last ([(expr,[],"<=>")]++
[line | step, line<-pr]++
[line | step', line<-pr']
)]
where pr = nfPr shw True True expr
(expr',_,_) = if null pr then fatal 356 "last: empty list" else last pr
step = simplify expr/=simplify expr'
pr' = nfPr shw True True expr'
step' = simplify expr'/=simplify expr''
(expr'',_,_) = if null pr' then fatal 365 "last: empty list" else last pr'
isEUni :: Expression -> Bool
isEUni EUni{} = True
isEUni _ = False
isEIsc :: Expression -> Bool
isEIsc EIsc{} = True
isEIsc _ = False