ampersand-3.0.3: src/Database/Design/Ampersand/FSpec/ToFSpec/Calc.hs
{-# LANGUAGE ScopedTypeVariables, OverloadedStrings #-}
module Database.Design.Ampersand.FSpec.ToFSpec.Calc
( deriveProofs
, showProof, showPrf, assembleECAs, conjuncts, genPAclause
, commaEngPandoc, commaNLPandoc, commaEngPandoc', commaNLPandoc'
, quadsOfRules
-- , testInterface
) where
import Database.Design.Ampersand.Basics
import Data.List hiding (head)
import Data.Monoid
import GHC.Exts (sortWith)
--import Data.ByteString.Char8
--import Data.ByteString.Lazy.Char8
import Database.Design.Ampersand.Core.AbstractSyntaxTree hiding (sortWith)
import Database.Design.Ampersand.ADL1
import Database.Design.Ampersand.ADL1.Expression
import Database.Design.Ampersand.Classes
import Database.Design.Ampersand.FSpec.FSpec
import Database.Design.Ampersand.FSpec.ShowADL (ShowADL(..), showREL)
import Database.Design.Ampersand.FSpec.ShowECA (showECA)
import Database.Design.Ampersand.FSpec.ToFSpec.NormalForms
import Database.Design.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
-- testInterface :: FSpec -> Interface -> String
-- Deze functie is bedoeld om te bedenken hoe interfaces moeten worden afgeleid uit een vers vertaalde ObjectDef.
-- Nadat deze goed werkt kunnen de bewijsgenerator en de codegenerator worden gemaakt.
-- testInterface :: FSpec -> Interface -> String
-- testInterface fSpec ifc
-- = "\nInterface "++ name ifc++"("++intercalate ", " [showADL r++":"++name (target r) | r<-rels]++")\n"++
-- " - The parameters correspond to editable fields in a user interface.\n "++
-- showADL ifc++"\n"++
-- " - Invariants:\n "++intercalate "\n " [showADL rule | rule<-invs]++"\n"++
-- " - Derivation of clauses for ECA-rules:" ++
-- concat [showClause fSpec (makeCjcts (getOpts fSpec) rule) | rule<-invs]++"\n"++
--{-
-- " - ECA rules:"++concat [ "\n\n "++showECA "\n " (eca{ecaAction=normPA (getOpts fSpec) (ecaAction eca)})
-- ++"\n------ Derivation ----->"++showProof (codeBlock . ("\n "++) . showECA "\n ") (proofPA (getOpts fSpec) (ecaAction eca))++"\n<------End Derivation --"
-- | eca<-ecaRs]++"\n\n"++
---}
-- " - Visible relations:\n "++intercalate "\n " (spread 80 ", " [showADL r | r<-vis])++"\n"
-- where
---- showQ i (rel, shs,conj,r)
---- = "\nQuad "++show i++":\nrelation: "++showADL rel++":\nshifts: "++concat ["\n"++showADLe s |s<-shs]++"\nconjunct: "++showADL conj++"\nrule: "++showADL r++""
----TODO: Deze code komt ook voor in ADL2FSpec.hs. Dat lijkt dubbelop, en derhalve niet goed.
-- rels = nub (recur (ifcObj ifc))
-- where recur obj = [editMph (objctx o) | o<-attributes obj, editable (objctx o)]++[r | o<-attributes obj, r<-recur o]
-- vis = nub (rels++map (I . target) rels)
-- -- visible r = r `elem` vis
-- invs = [rule | rule<-invariants fSpec, (not.null) (map makeDeclaration (relsUsedIn rule) `isc` vis)]
-- -- qs = vquads fSpec
-- -- (ecaRs, _) = assembleECAs fSpec (allDecls fSpec)
---- editable (ERel Rel{} _) = True --WHY?? Stef, welke functie is de juiste?? TODO deze functie staat ook in ADL2FSpec.hs, maar is daar ANDERS(!)...
---- editable _ = False
---- editMph (ERel r@Rel{} _) = r --WHY?? Stef, welke functie is de juiste?? TODO deze functie staat ook in ADL2FSpec.hs, maar is daar ANDERS(!)...
---- editMph e = fatal 64 $ "cannot determine an editable declaration in a composite expression: "++show e
-- -- De functie spread verspreidt strings over kolommen met een breedte van n.
-- -- Deze functie garandeert dat alle strings worden afgedrukt in de aangegeven volgorde.
-- -- Hij probeert daarbij zo weinig mogelijk regels te gebruiken,
-- -- en alleen de grens van n te overschrijden als een string zelf langer is dan n.
-- spread :: Int -> String -> [String] -> [String]
-- spread n str = f ""
-- where f stored [] = [stored | not (null stored)]
-- f [] (cs:css) = f cs css
-- f stored (cs:css) | length stored > n = stored: f cs css
-- | length new <= n = f new css
-- | otherwise = stored: f cs css
-- where new = stored++str++cs
testConfluence :: A_Context -> Blocks
testConfluence context
= let tcss = [(expr,tcs) | expr<-expressionsIn context, let tcs=dfProofs expr, length tcs>1]
sumt = sum (map (length.snd) tcss)
in
para ("Confluence analysis statistics from "<>(str.show.length.expressionsIn) context<>" expressions."<>linebreak)<>
para ("This script contains "<>linebreak<>(str.show.length) tcss<> " non-confluent expressions "<>linebreak)<>
para (linebreak<>"Total number of derived expressions: "<>(str.show) sumt<>linebreak)<>
para ("Confluence analysis for "<>(str.name) context)<>
mconcat
[ para (linebreak<>"expression: "<>(str . showADL) expr<>linebreak)<>
bulletList [ showProof (para.str.showADL) prf | (_,prf)<-tcs ]
| (expr,tcs)<-tcss]
deriveProofs :: Options -> A_Context -> Blocks
deriveProofs opts context
= testConfluence context<>
para (linebreak<>"--------------"<>linebreak)<>
para ("Rules and their conjuncts for "<>(str.name) context)<>
bulletList [ para ("rule r: "<>str (showADL r)<>linebreak<>
"rrexp r: "<>str (showADL (rrexp r))<>linebreak<>
"conjNF: "<>str (showADL (conjNF opts (rrexp r)))<>linebreak<>
interText linebreak [ " conj: "<>str (showADL conj) | conj<-conjuncts opts r ]
)
| r<-allRules context]<>
para ("Transformation of user specified rules into ECA rules for "<>(str.name) context)<>
para (linebreak<>"--------------"<>linebreak<>"First step: determine the "<>(str.show.length) quads<>" quads:")<>
bulletList [ para ( "-- quad ------------"<>linebreak<>"When relation "<>(str . showADL . qDcl) q<>" is changed,"
<>linebreak<>(str . showADL . qRule) q
<>(if (length . qConjuncts) q<=1 then space else " ("<>(str . show . length . qConjuncts) q<>" 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]
| q<-quads, x<-qConjuncts q ] <>
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) [(qDcl q,dc,qRule q) |q<-quads, x<-qConjuncts q, dc<-rc_dnfClauses x]
, let (_,dc,r) = head cl
]
]<>
para (linebreak<>"Third step: determine "<>(str.show.length.udefrules) context<>" ECA rules"<>
if verboseP opts
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 opts then para ( "--------------"<>linebreak)<>bulletList derivations else fromList [] )<>
bulletList [ para ( "-- ECA Rule "<>(str.show.ecaNum) ecarule<>" ---------")<>
codeBlock ("\n "++showECA "\n " ecarule{ecaAction=normPA opts (ecaAction ecarule)})<>
bulletList [ para (linebreak<>"delta expression"<>linebreak<>space<>str (showADL d)
<>linebreak<>"derivation:"
)<>
(showProof (para.str.showADL).dfProof opts) d<> -- Produces its result in disjunctive normal form
para ("disjunctly normalized delta expression"<>linebreak<>(str.showADL.disjNF opts) d)
| verboseP opts, e@Do{}<-[ecaAction ecarule], let d = paDelta e ]
| ecarule <- ecaRs]
{-
++
[ linebreak<>"--------------", linebreak, linebreak<>"Fourth step: cascade blocking rules"
, linebreak
]++
interText []
[ [linebreak<>"-- Raw ECA rule "<>(str.show.ecaNum) er<>"------------"<>linebreak<>str (showECA "\n " er)]
| er<- ecaRs]
++
[ linebreak<>"--------------", linebreak, linebreak<>"Fifth step: preEmpt the rules (= optimize)"
, linebreak
]++
{- TODO: readdress preEmpt. It is wrong
interText []
[ [linebreak<>"-- Preempted ECA rule "<>(str.show.ecaNum) er<>"------------"<>linebreak<>str (showECA "\n " er)]
| er<- preEmpt opts ecaRs]
++ -}
{-
[ linebreak<>"--------------", linebreak]
++ -- TODO: make an ontological analysis, which explains the delete behaviour.
[ Str "Ontological analysis: ", linebreak<>" "]
++
interText [linebreak, linebreak<>" "]
[ [Str (name ifc)<>"("]
++ interText ", "
[str (name a)<>"["<>(str.name.target.ctx) a<>"]"
|a<-attributes (ifcObj ifc)]
++ [Str "):", linebreak<>" "]
| ifc<-interfaceS fSpec]
++
[ linebreak<>"--------------", linebreak
<>"Analyzing interfaces:", linebreak<>" "]
++
interText [linebreak<>" "]
[[Str (testInterface fSpec ifc)]
| ifc<-take 1 (interfaceG fSpec)]
++
[ linebreak<>"--------------", linebreak]
-}
-}
where
-- visible _ = True -- We take all quads into account.
quads = quadsOfRules opts (allRules context) -- the quads that are derived for this fSpec specify dnf clauses, meant to maintain rule r, to be called when relation rel is affected (rel is in r).
-- interText :: (Data.String.IsString a, Data.Monoid.Monoid a) => a -> [a] -> a
interText _ [] = ""
interText inbetween (xs:xss) = xs<>inbetween<>interText inbetween xss
derivations :: [Blocks]
ecaRs :: [ECArule]
(ecaRs, derivations) = assembleECAs opts context (relsDefdIn context)
{-
[ str ("Available code fragments on rule "<>name rule<>":", linebreak ]<>
interText [linebreak] [showADL rule<> " yields\n"<>interText "\n\n"
[ ["event = ", str (show ev), space, str (showADL rel), linebreak ] <>
[str (showADL r<>"["<>showADL rel<>":="<>showADL (actSem opts ev (EDcD rel) (delta (sign rel)))<>"] = r'"), linebreak ] <>
["r' = "] <> conjProof r' <> [linebreak ] <>
["viols = r'-"] <> disjProof (ECpl r') <> [ linebreak ] <>
"violations, considering that the valuation of "<>showADL rel<>" has just been changed to "<>showADL (actSem opts ev (EDcD rel) (delta (sign rel)))<>
" "<>conjProof (ECpl r) <>"\n"<>
"reaction? evaluate r |- r' ("<>(str.showADL.conjNF opts) (notCpl r .\/. r')<>")"<>
conjProof (notCpl r .\/. r')<>"\n"<>
"delta: r-/\\r' = "<>conjProof (EIsc[notCpl r,r'])<>
"\nNow compute a reaction\n(isTrue.conjNF opts) (notCpl r .\/. r') = "<>show ((isTrue.conjNF opts) (notCpl r .\/. r'))<>"\n"<>
(if null (lambda ev (ERel rel ) r)
then "lambda "<>showADL rel<>" ("<>showADL r<>") = empty\n"
else -- for debug purposes:
-- "lambda "<>show ev<>" "<>showADL rel<>" ("<>showADL r<>") = \n"<>(interText "\n\n".map showPr.lambda ev (ERel rel)) r<>"\n"<>
-- "derivMono ("<>showADL r<>") "<>show ev<>" "<>showADL rel<>"\n = "<>({-interText "\n". map -}showPr.derivMono r ev) rel<>"\n"<>
-- "\nNow compute checkMono opts r ev rel = \n"<>show (checkMono opts r ev rel)<>"\n"<>
if (isTrue.conjNF opts) (notCpl r .\/. r')
then "A reaction is not required, because r |- r'. Proof:"<>conjProof (notCpl r .\/. r')<>"\n"
else if checkMono opts r ev rel
then "A reaction is not required, because r |- r'. Proof:"{-<>(str.showPr.derivMono r ev) rel-}<>"NIET TYPECORRECT: (showPr.derivMono r ev) rel"<>"\n" --WHY? Stef, gaarne herstellen...Deze fout vond ik nadat ik het type van showProof had opgegeven.
else let ERel _ _ = delta (sign rel) in
"An appropriate reaction on this event is required."
-- showECA "\n " (ECA (On ev rel) delt (genPAclause visible Ins r viols conj [rule]) 0)
)
| rel<-relsUsedIn r -- nub [x |x<-relsUsedIn r, not (isIdent x)] -- TODO: include proofs that allow: isIdent rel'
, ev<-[Ins,Del]
, r'<-[subst (rel, actSem opts ev (EDcD rel) (delta (sign rel))) r]
-- , viols<-[conjNF opts (ECpl r')]
, True ] -- (isTrue.conjNF opts) (notCpl r .\/. r')
| r<-[dc | cs<-[makeCjcts opts rule], (_,dnfClauses)<-cs, dc<-dnfClauses]
]
where e = rrexp rule
prf = cfProof (getOpts fSpec) e
(exx',_,_) = last prf
-- conjProof = showProof (para.str.showADL) . cfProof (getOpts fSpec)
disjProof = showProof (para.str.showADL) . dfProof (getOpts fSpec)
-- showPr = showProof (para.str.showADL) -- hoort bij de uitgecommentaarde code hierboven...
--TODO: See ticket #105
-}
-- Stel we voeren een actie a uit, die een(1) van de volgende twee is:
-- {r} INS rel INTO expr {r'} ofwel
-- {r} DEL rel FROM expr {r'}
-- Dan toetst checkMono of r|-r' waar is op grond van de afleiding uit derivMono.
-- Als dat waar is, betekent dat dat invariant r waar blijft wanneer actie a wordt uitgevoerd.
checkMono :: Options
-> Expression
-> InsDel
-> Declaration
-> Bool
checkMono opts 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 opts 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,ss,_)] = shw expr<> para ( str(" { "++intercalate " and " ss++" }"))
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
--where e'= if null prf then "" else let (expr,_,_):_ = prf in showHS options "" expr
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 provides a derivation to prove that (precondition) r is a subset of (postcondition) r'.
-- This is useful in proving that an action {expr} a {expr'} maintains its invariant, i.e. that expr|-expr' holds (proven by monotony properties)
-- Derivmono gives a derivation only.
derivMono :: Expression -> InsDel -> Declaration -> [(Rule, [String], String)]
derivMono expr -- preconditie van actie a
tOp -- de actie (Ins of Del)
dcl' -- re relatie, zodat de actie bestaat uit INSERT rel' INTO expr of DELETE rel' FROM expr
= 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)")] --TODO Stef, gaarne de explanations aanvullen/verwijderen. Dank! Han.
, rrmsg = []
, rrviol = Nothing
, rrtyp = sign neg' {- (neg `meet` pos) -}
, rrdcl = Nothing
, r_env = ""
, r_usr = Multiplicity
, isSignal = fatal 336 $ "erroneous reference to isSignal 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)")] --TODO Stef, gaarne de explanations aanvullen/verwijderen. Dank! Han.
, rrmsg = []
, rrviol = Nothing
, rrtyp = sign neg' {- (neg `meet` pos) -}
, rrdcl = Nothing
, r_env = ""
, r_usr = Multiplicity
, isSignal = fatal 352 $ "illegal reference to isSignal 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{} -> "-"
_ -> ""
{- The purpose of function lambda is to generate a derivation.
Rewrite rules:
-r;-s -> -(r!s)
-}
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
] -- isNeg is nog niet helemaal correct.
| 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] -- isNeg is nog niet helemaal correct.
| 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 rc-1) (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!"
-- lam tOp e f = []
-- longstcomn determines the longest prefix common to all xs in xss.
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 determines the remainders.
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
-- | Action semantics for inserting a delta into a relation dcl.
actSem :: Options -> InsDel -> Expression -> Expression -> Expression
actSem opts Ins dcl delt | sign dcl/=sign delt = fatal 598 "Type error in actSem Ins"
| dcl==delt = dcl
| otherwise = disjNF opts (dcl .\/. delt)
actSem opts Del dcl delt | sign dcl/=sign delt = fatal 598 "Type error in actSem Del"
| dcl==delt = notCpl (EDcV (sign dcl))
| otherwise = conjNF opts (dcl ./\. notCpl delt)
-- | assembleECAs assembles larger chunks of code, because it combines acts that are triggered by the same event.
assembleECAs :: Options -> A_Context -> [Declaration] -> ([ECArule],[Blocks])
assembleECAs options context editables
= unzip [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 <- editables -- allDecls fSpec ++ [ Isn c | c<-allConcepts fSpec, c/=ONE] -- This is the relation in which a delta is being inserted or deleted.
-- , let relEq = [ q | q<-vquads fSpec, qDcl q==rel] -- Gather the quads with the same declaration (qDcl). A quad has a declaration (qDcl), a rule (qRule) and clauses qConjuncts
, let EDcD delt = delta (sign rel) -- delt is a placeholder for the pairs that have been inserted or deleted in rel.
, ev<-[Ins,Del]
, let acts = [ -- go through all the events that affect that clause:
( normPA options act -- a normalized action for this event-conjunct combination
, conjunct -- the conjunct
, map snd conjEqClass -- the rule-expression of which conjunct is a part
, para ("Let us analyse clause "<>str (showADL expr)<>" from rule "<>commaEngPandoc' "and" (map (singleQuoted.str.name.snd) conjEqClass)<>".")<>
para ("event = "<>str (show ev)<>space<>str (showREL rel)<>" means doing the following substitution")<>
para (str (showADL clause<>"["<>showREL rel<>":="<>showADL (actSem options 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 options) 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 options) (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 options negs))<>" into "<> str (showADL (disjNF options poss))<>"."
else str (showADL (disjNF options poss))<>" into "<> str (showADL (conjNF options negs))<>"."
)<>linebreak<>"deltFr: ")<>
(showProof (para.str.showADL). dfProof options) deltFr<>
( let pr=proofPA options act in
if length pr>1
then para "Now let us remove redundancy from the ECA action:\n "<>
showProof (codeBlock . ("\n "++) . showECA "\n ") (proofPA options act)
else fromList []
)
{- <> "To finish the analysis of case "<>str (show ev)<>space<>str (showADL rel)
<>", let us compute the contents of "<>str (showADL toExpr)<>" after insertion of viols."<>linebreak
<>
( if length (nub [sign viols, sign viols', sign toExpr])>1
then fatal 248 ("viols"<>showSign (sign viols) <>" "<>showADL viols <>"\n"<>
"viols'"<>showSign (sign viols')<>" "<>showADL viols'<>"\n"<>
"toExpr"<>showSign (sign toExpr)<>" "<>showADL toExpr)
else if ev==Ins
then (showProof (para.str.showADL). cfProof options) (viols'.\/.toExpr)<>linebreak
else (showProof (para.str.showADL). dfProof options) (notCpl viols./\.toExpr)<>linebreak
) -}
)
)
| conjEqClass <- [] -- TODO: implement this once we can test it (note: computing eq. class is no longer necessary)
-- conjEqClass <- eqCl fst [ (qConjuncts q, qRule q) | q<-relEq ]
, conjunct <- (fst.head) conjEqClass -- get conjuncts from the clauses
, clause <- rc_dnfClauses conjunct -- the DNF form of each clause
, let expr = dnf2expr clause -- Note that this differs from: rc_conjunct conjunct, because the type may be different.
, let vee = EDcV (sign expr)
, let ex' = subst (rel, actSem options ev (EDcD rel) (delta (sign rel))) expr -- the clause after the edit action
, let clause' = conjNF options ex' -- its CNF
, not (isTrue clause')
, let notClau = notCpl clause' -- the violations after the edit action
, let viols = conjNF options notClau -- the violations after the edit action
, let viols' = disjNF options notClau -- the violations after the edit action
, let negs = if (length.nub.map sign) (vee:antcs clause)>1
then fatal 265 ("type inconsistencies in antcs: "++show (map showADL (vee:antcs clause)))
else foldr (./\.) vee (antcs clause)
, let poss = if (length.nub.map sign) (vee:conss clause)>1
then fatal 265 ("type inconsistencies in conss: "++show (map showADL (vee:conss clause)))
else foldr (.\/.) (notCpl vee) (conss clause)
, let frExpr = case ev of
Ins -> disjNF options (notCpl negs)
Del -> disjNF options 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 options ev (EDcD rel) (delta (sign rel)))) negs ./\. notCpl poss
else (notCpl . subst (rel, actSem options ev (EDcD rel) (delta (sign rel)))) poss ./\. negs
, let deltFr' = disjNF options deltFr
, rel `elem` relsMentionedIn frExpr
, let toExpr = if ev==Ins
then disjNF options poss
else disjNF options (notCpl negs)
, let visible r = r `elem` editables
, if length (nub (map sign [toExpr, deltFr', expr]))>1
then fatal 285 "type problem"
else True
, let act = genPAclause visible Ins toExpr deltFr' [(expr, map snd conjEqClass)]
]
, let ecaAct = ALL (map fst4 acts
-- The following acts add the implicit rules, which allows the user to add and delete atoms from concepts in a safe way.
++ [act' | (ev',rel',act')<-rulesDecls++rulesGens rel, ev==ev', rel==rel' ]
)
[ (rc_conjunct conj,ruls) | (_,conj,ruls,_)<-acts] --motivation is of type [(Expression,[Rule])]
, let normEcaAct = normPA options ecaAct
, let ecaProof = proofPA options ecaAct
, let ecaEvt = On ev rel
, let ecaRule = ECA ecaEvt delt normEcaAct
]
-- the following eca-rules are derived from the typing rules, rather than explicit rules specified by users.
-- This concerns the following rules:
-- Each declaration "RELATION r[A*B]" represents the rule "RULE r[A*B] |- V[A*B]"
-- Besides, for every A, B: "RULE I[A]*I[B] = V[A*B]"
-- For every "CLASSIFY A ISA B" we get "RULE I[A] |- I[B]"
-- For every "CLASSIFY A IS B /\ C" we get "RULE I[A] |- I[B]" and "RULE I[A] |- I[C]"
-- The results of both classify statements are available through vgens.
-- Finally, for every Atom c a there is a rule "RULE 'a' |- I[c]"
-- The eca-rules that can be derived from these rules are produced by ecasFromTypes
{- V[A*B] is implicit, so we don't generate ECA (On Ins rel) delt (Do Ins (Vs (Sign a b)) delt motive).
Neither do we generate ECA (On Del (Vs (Sign a b))) delt (Do Del rel delt motive).
However, we do generate: ECA (On Ins rel) delt (Do Ins (Isn a) ((dlt.<>.flp dlt).-.EDcI a) motive)
and: ECA (On Ins rel) delt (Do Ins (Isn b) ((flp dlt.<>.dlt).-.EDcI b) motive),
because the delta to be inserted might contain new atoms.
Similarly, upon deletion of an atom from a concept we must delete the appropriate links from relations that share this concept.
So, we generate ECA (On Del (Isn a)) delt (Do Del rel (delt.:.V[A*B]) motive)
and: ECA (On Del (Isn b)) delt (Do Del rel (V[A*B].:.delt) motive)
ECA-rules that are derivable from relation declarations are generated by rulesDecls
-}
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 <- relsDefdIn context
, let dlt = delta (sign rel)
, let a=source rel, let b=target rel
, let vee = (EDcV . sign) rel
]
{- We generate:
for every "RULE I[A] |- I[B]": ECA (On Ins (Isn a)) delt (Do Ins (Isn b) (EDcD delt) motive)
and: ECA (On Del (Isn b)) delt (Do Del (Isn a) (EDcD delt) motive)
for every "RULE 'a' |- I[c]": ECA (On Del (Isn c)) ('a','a') (Blk motive)
-}
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) <- concatMap genericAndSpecifics (gens context)
]
fst4 (x,_,_,_) = x
-- | de functie genPAclause beschrijft de voornaamste mogelijkheden om een expressie delta' te verwerken in expr (met tOp'==Ins of tOp==Del)
-- TODO: Vind een wetenschappelijk artikel waar de hier beschreven transformatie uitputtend wordt behandeld.
-- TODO: Deze code is onvolledig en misschien zelfs fout....
genPAclause :: (Declaration->Bool) -- ^True if a relation may be changed (i.e. is editable)
-> InsDel -- ^the type of action: Insert or Delete
-> Expression -- ^the expression in which a delete or insert takes place
-> Expression -- ^the delta to be inserted or deleted
-> [(Expression,[Rule])] -- ^the motivation, consisting of the conjuncts (traced back to their rules) that are being restored by this code fragment.
-> 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{-, not (f==expr1 && Ins/=tOp') -}] motive -- the filter prevents self compensating PA-clauses.
(Ins, EIsc{}) -> ALL [ genPAcl deltaX Ins f | f<-exprIsc2list expr ] motive
(Del, EUni{}) -> ALL [ genPAcl deltaX Del f | f<-exprUni2list expr {-, not (f==expr1 && Del/=tOp') -}] motive -- the filter prevents self compensating PA-clauses.
(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])]
{- (_ , _) -> fatal 767 ( "(Stef?) Non-exhaustive patterns in the recursive call\n"
++"doCod ("++showADL deltaX++") -- deltaX\n "++show tOp++" -- tOp\n ("++showADL expr++") -- expr\n"++
"within function\ndoCode "++show tOp'++" -- tOp'\n ("++showADL expr1++") -- expr1\n ("++showADL delta1++") -- delta1\n"++
concat
[ "while trying to maintain conjunct "++showADL conjunct++
"\nfrom rule "++intercalate "\n " [show r | r<-rs]
| (conjunct,rs)<-motive ] ++
if null motive then "null motive" else ""
)
-}
deltaK0 :: t -> InsDel -> t1 -> t
deltaK0 delta' Ins _ = delta' -- error! (tijdelijk... moet berekenen welke paren in x gezet moeten worden zodat delta |- x*)
deltaK0 delta' Del _ = delta' -- error! (tijdelijk... moet berekenen welke paren uit x verwijderd moeten worden zodat delta/\x* leeg is)
deltaK1 :: t -> InsDel -> t1 -> t
deltaK1 delta' Ins _ = delta' -- error! (tijdelijk... moet berekenen welke paren in x gezet moeten worden zodat delta |- x+)
deltaK1 delta' Del _ = delta' -- error! (tijdelijk... moet berekenen welke paren uit x verwijderd moeten worden zodat delta/\x+ leeg is)
commaEngPandoc' :: Inlines -> [Inlines] -> Inlines
commaEngPandoc' s [a,b,c] = a <> ", " <> b <> ", " <> s <> space <> c
commaEngPandoc' s [a,b] = a <> space <> s <> space <> b
commaEngPandoc' _ [a] = a
commaEngPandoc' s (a:as) = a <> ", " <> commaEngPandoc' s as
commaEngPandoc' _ [] = mempty
commaEngPandoc :: Inline -> [Inline] -> [Inline]
commaEngPandoc s [a,b,c] = [a,Str ", ",b,Str ", ",s, Str " ", c]
commaEngPandoc s [a,b] = [a,Str " ",s, Str " ", b]
commaEngPandoc _ [a] = [a]
commaEngPandoc s (a:as) = [a, Str ", "]++commaEngPandoc s as
commaEngPandoc _ [] = []
commaNLPandoc' :: Inlines -> [Inlines] -> Inlines
commaNLPandoc' s [a,b] = a <> space <> s <> space <> b
commaNLPandoc' _ [a] = a
commaNLPandoc' s (a:as) = a <> ", " <> commaNLPandoc' s as
commaNLPandoc' _ [] = mempty
commaNLPandoc :: Inline -> [Inline] -> [Inline]
commaNLPandoc s [a,b] = [a,Str " ",s, Str " ", b]
commaNLPandoc _ [a] = [a]
commaNLPandoc s (a:as) = [a, Str ", "]++commaNLPandoc s as
commaNLPandoc _ [] = []
quadsOfRules :: Options -> [Rule] -> [Quad]
quadsOfRules opts rules
= makeAllQuads (converse [ (conj, rc_orgRules conj) | conj <- makeAllConjs opts rules ])
-- Quads embody the "switchboard" of rules. A quad represents a "proto-rule" with the following meaning:
-- whenever relation r is affected (i.e. tuples in r are inserted or deleted),
-- the rule may have to be restored using functionality from one of the clauses.
makeAllQuads :: [(Rule, [Conjunct])] -> [Quad]
makeAllQuads conjsPerRule =
[ Quad { qDcl = d
, qRule = rule
, qConjuncts = conjs
}
| (rule,conjs) <- conjsPerRule, d <-relsUsedIn rule
]
{-
-- If one rule r blocks upon an event, e.g. e@(ON Ins rel), while another ECA rule r'
-- maintains something else with that same event e, we can save r' the trouble.
-- After all, event e will block anyway.
-- preEmpt tries to simplify ECArules by predicting whether a rule will block.
preEmpt :: Options -> [ECArule] -> [ECArule]
preEmpt opts ers = pr [length ers] (10::Int)
where
pr :: [Int] -> Int -> [ECArule]
pr ls n
| n == 0 = fatal 633 $ "too many cascading levels in preEmpt "++show ls
| (not.null) cascaded = pr (length cascaded:ls)
-- ([er{ecaAction=normPA opts (ecaAction er)} | er<-cascaded] ++uncasced)
(n-1)
| otherwise = [er{ecaAction=normPA opts (ecaAction er)} | er<-uncasced]
where
-- preEmpt divides all ECA rules in uncascaded rules and cascaded rules.
-- cascaded rules are those rules that have a Do component with event e, where e is known to block (for some other reason)
new = [er{ecaAction=normPA opts (ecaAction er)} | er<-ers]
cascaded = [er{ecaAction=action'} | er<-new, let (c,action') = cascade (eDcl (ecaTriggr er)) (ecaAction er), c]
uncasced = [er | er<-new, let (c,_) = cascade (eDcl (ecaTriggr er)) (ecaAction er), not c]
-- cascade inserts a block on the place where a Do component exists that matches the blocking event.
-- cascade :: Relation -> PAclause -> (Bool, PAclause)
cascade dcl (Do srt to _ _) | (not.null) blkErs = (True, ecaAction (head blkErs))
where blkErs = [er | er<-ers
, Blk _<-[ecaAction er]
, let t = ecaTriggr er
, eSrt t == srt
, eDcl t == to
, not (dcl ==to)
]
cascade _ c@Do{} = (False, c)
cascade rel (New c clause m) = ((fst.cascade rel.clause) "dummystr", New c (snd.cascade rel.clause) m)
cascade rel (Rmv c clause m) = ((fst.cascade rel.clause) "dummystr", Rmv c (snd.cascade rel.clause) m)
--cascade rel (Sel c e cl m) = ((fst.cascade rel.cl) "dummystr", Sel c e (snd.cascade rel.cl) m)
cascade rel (CHC ds m) = (any (fst.cascade rel) ds, CHC (map (snd.cascade rel) ds) m)
cascade rel (ALL ds m) = (any (fst.cascade rel) ds, ALL (map (snd.cascade rel) ds) m)
cascade _ (Nop m) = (False, Nop m)
cascade _ (Blk m) = (False, Blk m)
cascade _ (Let _ _ _) = fatal 611 "Deze constructor is niet gedefinieerd" -- HJO, 20131205:Toegevoegd om warning te verwijderen
cascade _ (Ref _) = fatal 612 "Deze constructor is niet gedefinieerd" -- HJO, 20131205:Toegevoegd om warning te verwijderen
cascade _ (GCH{}) = fatal 655 "Deze constructor is niet gedefinieerd" -- SJO, 20140428:Toegevoegd om warning te verwijderen
-}