module DatabaseDesign.Ampersand.Fspec.ToFspec.Calc
( deriveProofs
, lambda
, checkMono
, showProof, showPrf, assembleECAs, conjuncts, genPAclause
)
where
import DatabaseDesign.Ampersand.Basics (fatalMsg,Collection (isc),Identified(..),eqCl,Flippable(..))
import Data.List hiding (head)
import GHC.Exts (sortWith)
import DatabaseDesign.Ampersand.Core.AbstractSyntaxTree hiding (sortWith)
import DatabaseDesign.Ampersand.ADL1
import DatabaseDesign.Ampersand.ADL1.Expression
import DatabaseDesign.Ampersand.Classes
import DatabaseDesign.Ampersand.Fspec.Fspec
import DatabaseDesign.Ampersand.Fspec.ShowADL (ShowADL(..), showREL)
import DatabaseDesign.Ampersand.Fspec.ShowECA (showECA)
import DatabaseDesign.Ampersand.Fspec.ToFspec.NormalForms (delta,conjNF,disjNF,cfProof,dfProof,nfProof,simplify,normPA,proofPA)
import DatabaseDesign.Ampersand.Misc (Lang(..),Options(..),PandocFormat(ReST),string2Blocks)
import Text.Pandoc.Builder
import Prelude hiding (head)
fatal :: Int -> String -> a
fatal = fatalMsg "Fspec.ToFspec.Calc"
head :: [a] -> a
head [] = fatal 30 "head must not be used on an empty list!"
head (a:_) = a
conjuncts :: Rule -> [DnfClause]
conjuncts = map disjuncts.exprIsc2list.conjNF.rrexp
disjuncts :: Expression -> DnfClause
disjuncts conj = (split (Dnf [] []).exprUni2list) conj
where split :: DnfClause -> [Expression] -> DnfClause
split (Dnf antc cons) (ECpl e: rest) = split (Dnf (e:antc) cons) rest
split (Dnf antc cons) ( e: rest) = split (Dnf antc (e:cons)) rest
split dc [] = dc
--{-
---}
deriveProofs :: Options -> Fspc -> Blocks
deriveProofs flags fSpec
= para ("Rules and their conjuncts for "<>(str.name) fSpec)<>
bulletList [ para ("rule r: "<>str (showADL r)<>linebreak<>
"rrexp r: "<>str (showADL (rrexp r))<>linebreak<>
"conjNF: "<>str (showADL (conjNF (rrexp r)))<>linebreak<>
interText linebreak [ " conj: "<>str (showADL conj) | conj<-conjuncts r ]
)
| r<-grules fSpec++vrules fSpec]<>
para ("Transformation of user specified rules into ECA rules for "<>(str.name) fSpec)<>
para (linebreak<>"--------------"<>linebreak<>"First step: determine the "<>(str.show.length) qs<>" quads:")<>
bulletList [ para ( "-- quad ------------"<>linebreak<>"When relation "<>str (showADL rel)<>" is changed,"
<>linebreak<>str (showADL r)
<>(if length (cl_conjNF ccrs)<=1 then space else " ("<>(str.show.length.cl_conjNF) ccrs<>" conjuncts)")
<>" must be restored."<>linebreak<>"This quad has conjunct: "<>(str.showADL.rc_conjunct) x
<>" and "<>(str.show.length.rc_dnfClauses) x<>" dnf clauses."
) <>
bulletList [ para (linebreak<>"Dnf clause "<>str (showADL dc)) | dc<-rc_dnfClauses x]
| Quad rel ccrs<-qs, let r=cl_rule ccrs , x<-cl_conjNF ccrs ] <>
para (linebreak<>linebreak<>"Second step: assemble dnf clauses.") <>
bulletList [ para ( "Dnf clause "<>str (showADL dc)
<>linebreak<>"is derived from rule "<>str (showADL r)
<>linebreak
<>case ms of
[] -> "No relations affect this clause."
[rel] -> "It can be called when relation " <>str (showADL rel)<>" is affected."
_ -> "It can be called when relations "<>str (commaEng "or" [showADL rel | rel<-ms])<>" are affected."
)
| (ms,dc,r)<-
[ (nub [ dcl |(dcl,_,_)<-cl],dc,r)
| cl<-eqCl (\(_,_,dc)->dc) [(dcl,dc,r) |Quad dcl ccrs<-qs, let r=cl_rule ccrs, x<-cl_conjNF ccrs, dc<-rc_dnfClauses x]
, let (_,dc,r) = head cl
]
]<>
para (linebreak<>"Third step: determine "<>(str.show.length.udefrules) fSpec<>" ECA rules"<>
if verboseP flags
then " (Turn --verbose off if you want to see ECA rules only)"
else " (Turn on --verbose if you want to see more detail)"
)<>
( if verboseP flags then para ( "--------------"<>linebreak)<>bulletList derivations else fromList [] )<>
bulletList [ para ( "-- ECA Rule "<>(str.show.ecaNum) ecarule<>" ---------")<>
codeBlock ("\n "++showECA "\n " ecarule{ecaAction=normPA (ecaAction ecarule)})<>
bulletList [ para (linebreak<>"delta expression"<>linebreak<>space<>str (showADL d)
<>linebreak<>"derivation:"
)<>
(showProof (para.str.showADL).nfProof showADL) d<>
para ("disjunctly normalized delta expression"<>linebreak<>(str.showADL.disjNF) d)
| verboseP flags, e@Do{}<-[ecaAction ecarule], let d = paDelta e ]
| ecarule <- ecaRs]
where
qs = vquads fSpec
commaEng :: String -> [String] -> String
commaEng _ [] = ""
commaEng _ [x] = x
commaEng chs [x,y] = x++" "++chs++" "++y
commaEng chs (x:y:ys) = x++", "++commaEng chs (y:ys)
interText _ [] = ""
interText inbetween (xs:xss) = xs<>inbetween<>interText inbetween xss
derivations :: [Blocks]
ecaRs :: [ECArule]
(ecaRs, derivations) = unzip (assembleECAs fSpec)
checkMono :: Expression
-> InsDel
-> Declaration
-> Bool
checkMono expr ev dcl
= case ruleType conclusion of
Truth -> fatal 247 "derivMono came up with a Truth!"
_ -> simplify expr == simplify (antecedent conclusion) &&
simplify (subst (dcl, actSem ev (EDcD dcl) (delta (sign dcl))) expr) ==
simplify (consequent conclusion)
where (conclusion,_,_) = last (derivMono expr ev dcl)
type Proof expr = [(expr,[String],String)]
reversePrf :: Proof e -> Proof e
reversePrf [] = []
reversePrf [s] = [s]
reversePrf ((r,cs,e'):prf@((r',_ ,_):_)) = init rp++[(r',cs,rev e'),(r,[],"")]
where rp = reversePrf prf
rev "==>" = "<=="
rev "<==" = "==>"
rev "-->" = "<--"
rev "<--" = "-->"
rev x = x
showProof :: (expr->Blocks) -> Proof expr -> Blocks
showProof shw [(expr,_,_)] = shw expr
showProof shw ((expr,ss,equ):prf) = shw expr<>
para (if null ss then str equ else
if null equ then str (unwords ss) else
str equ<>str (" { "++intercalate " and " ss++" }"))<>
showProof shw prf
showProof _ [] = fromList []
showPrf :: (expr->String) -> Proof expr -> [String]
showPrf shw [(expr,_,_)] = [ " "++shw expr]
showPrf shw ((expr,ss,equ):prf) = [ " "++shw expr] ++
(if null ss then [ equ ] else
if null equ then [ unwords ss ] else
[ equ++" { "++intercalate " and " ss++" }" ])++
showPrf shw prf
showPrf _ [] = []
derivMono :: Expression -> InsDel -> Declaration -> [(Rule, [String], String)]
derivMono expr
tOp
dcl'
= f (head (lambda tOp (EDcD dcl') expr++[[]])) (start tOp)
where
f :: [(Expression, [String], whatever)]
-> (Expression, Expression)
-> [(Rule, [String], String)]
f [] (_,_) = []
f [(e',_,_)] (neg',pos')
= [(rule (subst (dcl',neg') e') (subst (dcl',pos') e'),[],"")]
f ((e',["invert"],_): prf@((_,_,_):_)) (neg',pos')
= (rule (subst (dcl',neg') e') (subst (dcl',pos') e'),["r |- s <=> s- |- r-"],"<=>"):
f prf (pos',neg')
f ((e1,_,_): prf@((e2,_,_):_)) (neg',pos')
= (rule (subst (dcl',neg') e1) (subst (dcl',pos') e1),["Monotony of "++showOp e2],"==>"):
f prf (neg',pos')
start Ins = (EDcD dcl',EDcD dcl' .\/. delta (sign dcl'))
start Del = (EDcD dcl' ./\. notCpl (delta (sign dcl')),EDcD dcl')
rule :: Expression -> Expression -> Rule
rule neg' pos' | isTrue neg' = Ru { rrnm = ""
, rrfps = Origin "rule generated for isTrue neg' by Calc"
, rrexp = pos'
, rrmean = AMeaning
[A_Markup Dutch ReST (string2Blocks ReST "Waarom wordt deze regel hier aangemaakt? (In Calc.hs, regel 402)")
,A_Markup English ReST (string2Blocks ReST "Why is this rule created? (In Calc.hs, line 403)")]
, rrmsg = []
, rrviol = Nothing
, rrtyp = sign neg'
, rrdcl = Nothing
, r_env = ""
, r_usr = Multiplicity
, isSignal = fatal 336 $ "erroneous reference to isSignal in rule ("++showADL neg'++") |- ("++showADL pos'++")"
, srrel = fatal 337 $ "erroneous reference to srrel in rule ("++showADL neg'++") |- ("++showADL pos'++")"
}
| otherwise = Ru { rrnm = ""
, rrfps = Origin "rule generated for not(isTrue neg') by Calc"
, rrexp = neg' .|-. pos'
, rrmean = AMeaning
[A_Markup Dutch ReST (string2Blocks ReST "Waarom wordt deze regel hier aangemaakt? (In Calc.hs, regel 332)")
,A_Markup English ReST (string2Blocks ReST "Why is this rule created? (In Calc.hs, line 333)")]
, rrmsg = []
, rrviol = Nothing
, rrtyp = sign neg'
, rrdcl = Nothing
, r_env = ""
, r_usr = Multiplicity
, isSignal = fatal 352 $ "illegal reference to isSignal in rule ("++showADL neg'++") |- ("++showADL pos'++")"
, srrel = fatal 353 $ "illegal reference to srrel in rule ("++showADL neg'++") |- ("++showADL pos'++")"
}
showOp expr' = case expr' of
EEqu{} -> "="
EImp{} -> "|-"
EIsc{} -> "/\\"
EUni{} -> "\\/"
EDif{} -> "-"
ELrs{} -> "/"
ERrs{} -> "\\"
EDia{} -> "<>"
ECps{} -> ";"
ERad{} -> "!"
EPrd{} -> "*"
EKl0{} -> "*"
EKl1{} -> "+"
EFlp{} -> "~"
ECpl{} -> "-"
_ -> ""
lambda :: InsDel -> Expression
-> Expression
-> [Proof Expression]
lambda tOp' e' expr' = [reversePrf[(e'',txt,op)
| (e'',_,txt,op)<-prf]
| prf<-lam tOp' e' expr' ]
where
lam :: InsDel -> Expression -> Expression ->
[[(Expression,Expression -> Expression,[String],String)]]
lam tOp e3 expr =
case expr of
EIsc{} | e3==expr -> [[(e3,id,[],"")]]
| length (const' expr)>0 -> [(expr,\_->expr, [derivtext tOp "mono" (inter' expr) expr],"<--") :prf
| prf<-lam tOp e3 (inter' expr)
]
| and [isNeg f |f<-exprIsc2list expr]
-> let deMrg = deMorganEIsc expr in
[(expr, deMorganEIsc, [derivtext tOp "equal" deMrg expr],"==") :prf | prf<-lam tOp e3 deMrg]
| or[null p |p<-fPrfs] -> []
| otherwise -> [(expr,\_->expr, [derivtext tOp "mono" (first lc) expr],"<--") : lc]
EUni{} | e3==expr -> [[(e3,id,[],"")]]
| length (const' expr)>0 -> [(expr,\_->expr, [derivtext tOp "mono" (inter' expr) expr],"<--") :prf
| prf<-lam tOp e3 (inter' expr)
]
| and [isNeg f |f<-exprUni2list expr]
-> let deMrg = deMorganEUni expr in
[(expr, deMorganEUni, [derivtext tOp "equal" deMrg expr],"==") :prf | prf<-lam tOp e3 deMrg]
| or[null p |p<-fPrfs] -> []
| otherwise -> [(expr,\_->expr, [derivtext tOp "mono" (first lc) expr],"<--") : lc]
ECps{} | e3==expr -> [[(e3,id,[],"")]]
| and [isNeg f |f<-exprCps2list expr]
-> let deMrg = deMorganECps expr in
[(expr, deMorganECps, [derivtext tOp "equal" deMrg expr],"==")
:prf
| prf<-lam tOp e3 deMrg
]
| or[null p|p<-fPrfs] -> []
| otherwise -> [(expr,\_->expr, [derivtext tOp "mono" (first lc) expr],"<--"): lc]
ERad{} | e3==expr -> [[(e3,id,[],"")]]
| and [isNeg f |f<-exprRad2list expr]
-> let deMrg = deMorganERad expr in
[(expr, deMorganERad, [derivtext tOp "equal" deMrg expr],"==") :prf | prf<-lam tOp e3 deMrg]
| or[null p |p<-fPrfs] -> []
| otherwise -> [(expr,\_->expr, [derivtext tOp "mono" (first lc) expr],"<--"): lc]
EKl0 x -> [(expr,\e->EKl0 e,[derivtext tOp "mono" x expr],"<--") :prf | prf<-lam tOp e3 x]
EKl1 x -> [(expr,\e->EKl1 e,[derivtext tOp "mono" x expr],"<--") :prf | prf<-lam tOp e3 x]
ECpl x -> [(expr,\e->ECpl e,["invert"],"<--") :prf | prf<-lam (inv tOp) e3 x]
EBrk x -> lam tOp e3 x
_ -> [[(e3,id,[],"")]]
where
sgn = sign expr
fPrfs = case expr of
EUni{} -> [lam tOp e3 f |f<-exprUni2list expr, isVar f e3]
EIsc{} -> [lam tOp e3 f |f<-exprIsc2list expr, isVar f e3]
ECps{} -> [lam tOp e3 f |f<-exprCps2list expr, isVar f e3]
ERad{} -> [lam tOp e3 f |f<-exprRad2list expr, isVar f e3]
_ -> fatal 428 ("fPrfs is not defined.Consult your dealer!")
lc = longstcomn vars++concat (drop (length rc1) (sortWith length rc))
rc = remainders vars vars
vars = map head fPrfs
const' e@EUni{} = [f |f<-exprUni2list e, isConst f e3]
const' e@EIsc{} = [f |f<-exprIsc2list e, isConst f e3]
const' expr'' = fatal 440 $ "'const'("++ show expr''++")' is not defined.Consult your dealer!"
inter' e@EUni{} = foldr (.\/.) (notCpl (EDcV sgn)) [f |f<-exprUni2list e, isVar f e3]
inter' e@EIsc{} = if and [sgn==sign f | f<-exprIsc2list e, isVar f e3]
then foldr (./\.) (EDcV sgn) [f | f<-exprIsc2list e, isVar f e3]
else fatal 532 ("signature error in inter' "++show [(showADL f,showSign (sign f)) | f<-exprIsc2list e, isVar f e3])
inter' expr'' = fatal 443 $ "'inter'("++ show expr''++")' is not defined.Consult your dealer!"
longstcomn :: (Eq a) => [[(a, b, c, d)]] -> [(a, b, c, d)]
longstcomn xss | or [null xs | xs<-xss] = []
| length (eqCl first xss)==1 = head [head prf | prf<-xss]: longstcomn [tail prf | prf<-xss]
| otherwise = []
remainders :: (Eq a) => [[(a, b, c, d)]] -> [[(a, b, c, d)]] -> [[(a, b, c, d)]]
remainders _ xss | or [null xs | xs<-xss] = xss
| length (eqCl first xss)==1 = remainders xss [tail prf | prf<-xss]
| otherwise = xss
isConst :: (ConceptStructure a, ConceptStructure b) => a->b->Bool
isConst e f = null (relsUsedIn e `isc` relsUsedIn f)
isVar :: (ConceptStructure a, ConceptStructure b) => a->b->Bool
isVar e f = not (isConst e f)
derivtext :: InsDel -> String -> Expression -> Expression -> String
derivtext tOp "invert" e'' expr = sh tOp++showADL e''++" means "++sh (inv tOp)++showADL expr++"."
derivtext tOp "mono" e'' expr = "("++showADL e''++"->"++showADL expr++") is monotonous, so "++sh tOp++showADL e''++" means "++sh tOp++showADL expr++"."
derivtext _ txt _ _ = txt
sh :: InsDel -> String
sh Ins = "insert into "
sh Del = "delete from "
inv :: InsDel -> InsDel
inv Ins = Del
inv Del = Ins
first :: [(a,b,c,d)] -> a
first ((e'',_,_,_):_) = e''
first _ = fatal 472 "wrong pattern in first"
ruleType :: Rule -> RuleType
ruleType r = case rrexp r of
EEqu{} -> Equivalence
EImp{} -> Implication
_ -> Truth
actSem :: InsDel -> Expression -> Expression -> Expression
actSem Ins dcl delt | sign dcl/=sign delt = fatal 598 "Type error in actSem Ins"
| dcl==delt = dcl
| otherwise = disjNF (dcl .\/. delt)
actSem Del dcl delt | sign dcl/=sign delt = fatal 598 "Type error in actSem Del"
| dcl==delt = notCpl (EDcV (sign dcl))
| otherwise = conjNF (dcl ./\. notCpl delt)
assembleECAs :: Fspc -> [(ECArule,Blocks)]
assembleECAs fSpec
= [eca i | (eca,i) <- zip ecas [(1::Int)..]]
where
ecas :: [Int->(ECArule,Blocks)]
ecas
= [ (\ruleNr->( ECA ecaEvt delt normEcaAct ruleNr
, para ("Let us analyse what happens "<>str (show (On ev rel))<>".")<>
bulletList [ txt | (_,_,_,txt)<-acts]<>
( if length ecaProof>1
then para ("The resulting action is:\n ")<>
showProof (codeBlock . ("\n "++) . showECA "\n ") ecaProof
else fromList []
)<>
para ("These results lead to the following ECA-rule:\n ")<>
(codeBlock . ("\n "++) . showECA "\n ".ecaRule) ruleNr
)
)
| rel <- allDecls fSpec ++ [ Isn c | c<-allConcepts fSpec, c/=ONE]
, let relEq = [ q | q<-vquads fSpec, qDcl q==rel]
, let quadClauses = (nub.map qClauses) relEq
, let EDcD delt = delta (sign rel)
, ev<-[Ins,Del]
, let acts = [
(normPA act, conj, rule,
para ("Let us analyse clause "<>str (showADL expr)<>" from rule "<>(singleQuoted.str.name) rule<>".")<>
para ("event = "<>str (show ev)<>space<>str (showREL rel)<>" means doing the following substitution")<>
para (str (showADL clause<>"["<>showREL rel<>":="<>showADL (actSem ev (EDcD rel) (delta (sign rel)))<>"] = clause'"))<>
para ("clause' = "<>str (showADL ex')<>
if clause'==ex'
then ", which is already in conjunctive normal form."<>linebreak
else ", which has conjunctive normal form: "<>linebreak<>str (showADL clause')
)<>
para ("Let us compute the violations to see whether invariance is maintained."<>linebreak<>
"This means to negate the result (notClau = notCpl clause'): ")<>
(showProof (para.str.showADL). cfProof showADL) notClau<>
para ("So, notClau has CNF: "<>str (showADL viols )<>linebreak<>
( if viols==viols'
then "This expression is in disjunctive normal form as well."
else str ("In DNF, notClau is: "<>showADL viols'<>".")))<>
( if isTrue clause'
then para ("This result proves the absence of violations, so a reaction of doing nothing is appropriate."<>linebreak
<>"Just for fun, let us try to derive whether clause |- clause' is true... ")<>
(showProof (para.str.showADL). cfProof showADL) (expr .|-. clause')
else para ("This result does not prove the absence of violations, so we cannot conclude that invariance is maintained."<>linebreak<>
"We must compute a reaction to compensate for violations..."<>linebreak<>
"That would be to reinsert violations that originate from "<>
( if ev==Ins
then str (showADL (conjNF negs))<>" into "<> str (showADL (disjNF poss))<>"."
else str (showADL (disjNF poss))<>" into "<> str (showADL (conjNF negs))<>"."
)<>linebreak<>"deltFr: ")<>
(showProof (para.str.showADL). dfProof showADL) deltFr<>
( let pr=proofPA act in
if length pr>1
then para "Now let us remove redundancy from the ECA action:\n "<>
showProof (codeBlock . ("\n "++) . showECA "\n ") (proofPA act)
else fromList []
)
))
| Clauses ts rule<-quadClauses, conj<-ts
, clause@(Dnf antcs conss) <- rc_dnfClauses conj
, let expr = dnf2expr clause
, let vee = EDcV (sign expr)
, let ex' = subst (rel, actSem ev (EDcD rel) (delta (sign rel))) expr
, let clause' = conjNF ex'
, not (isTrue clause')
, let notClau = notCpl clause'
, let viols = conjNF notClau
, let viols' = disjNF notClau
, let negs = if (length.nub.map sign) (vee:antcs)>1
then fatal 265 ("type inconsistencies in antcs: "++show (map showADL (vee:antcs)))
else foldr (./\.) vee antcs
, let poss = if (length.nub.map sign) (vee:conss)>1
then fatal 265 ("type inconsistencies in conss: "++show (map showADL (vee:conss)))
else foldr (.\/.) (notCpl vee) conss
, let frExpr = case ev of
Ins -> disjNF (notCpl negs)
Del -> disjNF poss
, let deltFr = if sign poss/=sign negs
then fatal 274 ("type inconsistencies in deltFr: "++showADL clause)
else if ev==Ins
then (subst (rel, actSem ev (EDcD rel) (delta (sign rel)))) negs ./\. notCpl poss
else (notCpl . subst (rel, actSem ev (EDcD rel) (delta (sign rel)))) poss ./\. negs
, let deltFr' = disjNF deltFr
, rel `elem` relsMentionedIn frExpr
, let toExpr = if ev==Ins
then disjNF poss
else disjNF (notCpl negs)
, let visible _ = True
, if length (nub (map sign [toExpr, deltFr', expr]))>1
then fatal 285 "type problem"
else True
, let act = genPAclause visible Ins toExpr deltFr' [(expr,[rule])]
]
, let ecaAct = ALL (map fst4 acts
++ [act' | (ev',rel',act')<-rulesDecls++rulesGens rel, ev==ev', rel==rel' ]
)
[ (rc_conjunct conj,[rule]) | (_,conj,rule,_)<-acts]
, let normEcaAct = normPA ecaAct
, let ecaProof = proofPA ecaAct
, let ecaEvt = On ev rel
, let ecaRule = ECA ecaEvt delt normEcaAct
]
rulesDecls :: [(InsDel, Declaration, PAclause)]
rulesDecls
= concat
[ [ (Ins, rel, Do Ins (Isn a) ((dlt.:.flp dlt ./\. EDcI a).-.EDcI a) [])
, (Ins, rel, Do Ins (Isn b) ((flp dlt.:.dlt ./\. EDcI b).-.EDcI b) [])
, (Del, Isn a, Do Del rel (delta (Sign a a).:.vee) [])
, (Del, Isn b, Do Del rel (vee.:.delta (Sign b b)) [])
]
| rel <- allDecls fSpec, let dlt = delta (sign rel)
, let a=source rel, let b=target rel
, let vee = (EDcV . sign) rel
]
rulesGens :: Declaration -> [(InsDel, Declaration, PAclause)]
rulesGens rel
= concat
[ [ (Ins, Isn s, Do Ins (Isn g) dlt [])
, (Del, Isn g, Do Del (Isn s) dlt [])
]
| let dlt = delta (sign rel), (s,g) <- fsisa fSpec
]
fst4 (x,_,_,_) = x
genPAclause :: (Declaration->Bool)
-> InsDel
-> Expression
-> Expression
-> [(Expression,[Rule])]
-> PAclause
genPAclause editAble tOp' expr1 delta1 motive = genPAcl delta1 tOp' expr1
where
testPA i l r ex
= if (source l,target r)/=(source ex,target ex)
then fatal i ("test with sign deltaX = ["++show (source l)++"*"++show (target r)++"], and sign expr = "++show (sign ex)++":\ndeltaX = "++showADL (l.:.r)++"\nexpr = "++show ex)
else if source r/=target l
then fatal i ("test with source r = "++show (source r)++", and target l = "++show (target l)++":\nl"++showSign (sign l)++" = "++showADL l++"\nr"++showSign (sign r)++" = "++showADL r++"\nexpr = "++show ex)
else id
genPAcl deltaX tOp expr =
case (tOp, expr) of
(_ , EEqu{}) -> Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EImp{}) -> Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EFlp x) -> genPAcl (flp deltaX) tOp x
(_ , EBrk x) -> genPAcl deltaX tOp x
(Ins, ECpl x) -> genPAcl deltaX Del x
(Del, ECpl x) -> genPAcl deltaX Ins x
(Ins, EUni{}) -> CHC [ genPAcl deltaX Ins f | f<-exprUni2list expr] motive
(Ins, EIsc{}) -> ALL [ genPAcl deltaX Ins f | f<-exprIsc2list expr ] motive
(Del, EUni{}) -> ALL [ genPAcl deltaX Del f | f<-exprUni2list expr ] motive
(Del, EIsc{}) -> CHC [ genPAcl deltaX Del f | f<-exprIsc2list expr ] motive
(Ins, EDif (l,r)) -> CHC [ genPAcl deltaX Ins l, genPAcl deltaX Del r ] motive
(Del, EDif (l,r)) -> CHC [ genPAcl deltaX Del l, genPAcl deltaX Ins r ] motive
(Ins, EDia (l,r)) -> CHC [ ALL [ genPAcl (testPA 986 (deltaX) (flp r) l $ deltaX.:.flp r ) Ins l
, genPAcl (testPA 987 (flp l) (deltaX) r $ flp l.:.deltaX ) Ins r] motive
, ALL [ genPAcl (testPA 988 (deltaX) (notCpl (flp r)) l $ deltaX.:.notCpl (flp r)) Del l
, genPAcl (testPA 989 (deltaX) (flp r) l $ deltaX.:.flp r ) Ins l] motive
, ALL [ genPAcl (testPA 990 (notCpl (flp l)) (deltaX) r $ notCpl (flp l).:.deltaX) Del r
, genPAcl (testPA 991 (flp l) (deltaX) r $ flp l.:.deltaX ) Ins r] motive
, ALL [ genPAcl (testPA 992 (deltaX) (notCpl (flp r)) l $ deltaX.:.notCpl (flp r)) Del l
, genPAcl (testPA 993 (notCpl (flp l)) (deltaX) r $ notCpl (flp l).:.deltaX) Del r] motive
] motive
(Del, EDia (l,r)) -> GCH [ (Del, (testPA 995 (deltaX) (flp r) l $ deltaX.:.flp r), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
, (Ins, (testPA 996 (deltaX) (flp (notCpl r)) l $ deltaX.:.flp (notCpl r)), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
, (Del, (testPA 997 (flp l) (deltaX) r $ flp l.:.deltaX), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
, (Ins, (testPA 998 (notCpl (flp l)) (deltaX) r $ notCpl (flp l).:.deltaX), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
] motive
(Ins, ERrs (l,r)) -> CHC [ genPAcl (testPA 1000 (notCpl r) (flp deltaX) l $ notCpl r.:.flp deltaX) Del l
, genPAcl (testPA 1001 (l) (deltaX) r $ l.:.deltaX) Ins r
] motive
(Del, ERrs (l,r)) -> GCH [ (Ins, (testPA 1003 (notCpl r) (flp deltaX) l $ notCpl r.:.flp deltaX), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
, (Del, (testPA 1004 (l) (deltaX) r $ l.:.deltaX), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
] motive
(Ins, ELrs (l,r)) -> CHC [ genPAcl (testPA 1006 (flp deltaX) (notCpl l) r $ flp deltaX.:.notCpl l) Del r
, genPAcl (testPA 1007 (deltaX) (r) l $ deltaX.:.r ) Ins l
] motive
(Del, ELrs (l,r)) -> GCH [ (Ins, (testPA 1009 (flp deltaX) (notCpl l) r $ flp deltaX.:.notCpl l), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
, (Del, (testPA 1010 (deltaX) (r) l $ deltaX.:.r), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
] motive
(Ins, ECps (l,r)) -> CHC [ GCH [ (Ins, (testPA 1012 (deltaX) (flp r) l $ deltaX.:.flp r), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
, (Ins, (testPA 1013 (flp l) (deltaX) r $ flp l.:.deltaX), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
] motive
, New (source r) (\x->ALL [ genPAcl (deltaX.*.EMp1 x (target l)) Ins l
, genPAcl (EMp1 x (source r).*.deltaX) Ins r] motive) motive
] motive
(Del, ECps (l,r)) -> CHC [ genPAcl (testPA 1018 (deltaX) (flp r) l $ deltaX.:.flp r) Del l
, genPAcl (testPA 1019 (flp l) (deltaX) r $ flp l.:.deltaX) Del r
] motive
(Ins, ERad (l,r)) -> CHC [ genPAcl (testPA 1021 (deltaX) (notCpl (flp r)) l $ deltaX.:.notCpl (flp r)) Ins l
, genPAcl (testPA 1022 (notCpl (flp l)) (deltaX) r $ notCpl (flp l).:.deltaX) Ins r
] motive
(Del, ERad (l,r)) -> CHC [ GCH [ (Del, (testPA 1024 (deltaX) (flp r) l $ deltaX.:.flp r), genPAcl (EMp1 "a" (source l).*.EMp1 "b" (target l)) tOp l)
, (Del, (testPA 1025 (flp l) (deltaX) r $ flp l.:.deltaX), genPAcl (EMp1 "a" (source r).*.EMp1 "b" (target r)) tOp r)
] motive
, New (source r) (\_->Nop motive) motive
] motive
(Ins, EPrd (l,r)) -> ALL [ genPAcl (EDcV (Sign ONE (source deltaX)).:.deltaX) Ins (EDcV (Sign ONE (source r)).:.r)
, genPAcl (deltaX.:.EDcV (Sign (target deltaX) ONE)) Ins (l.:.EDcV (Sign (target l) ONE))
] motive
(Del, EPrd (l,r)) -> ALL [ genPAcl (EDcV (Sign ONE (source deltaX)).:.deltaX) Del (EDcV (Sign ONE (source r)).:.r)
, genPAcl (deltaX.:.EDcV (Sign (target deltaX) ONE)) Del (l.:.EDcV (Sign (target l) ONE))
] motive
(_ , EKl0 x ) -> genPAcl (deltaK0 deltaX tOp x) tOp x
(_ , EKl1 x ) -> genPAcl (deltaK1 deltaX tOp x) tOp x
(_ , EDcD d) -> if editAble d then Do tOp d deltaX motive else Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EDcI c) -> if editAble (Isn c) then Do tOp (Isn c) deltaX motive else Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EDcV{}) -> Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EMp1{}) -> Blk [(expr, nub [r |(_,rs)<-motive, r<-rs])]
(_ , EEps{}) -> Nop [(expr, nub [r |(_,rs)<-motive, r<-rs])]
deltaK0 :: t -> InsDel -> t1 -> t
deltaK0 delta' Ins _ = delta'
deltaK0 delta' Del _ = delta'
deltaK1 :: t -> InsDel -> t1 -> t
deltaK1 delta' Ins _ = delta'
deltaK1 delta' Del _ = delta'