ampersand-3.0.0: src/lib/DatabaseDesign/Ampersand/Fspec/ToFspec/Calc.hs
{-# OPTIONS_GHC -Wall #-}
module DatabaseDesign.Ampersand.Fspec.ToFspec.Calc
( deriveProofs
, lambda
, checkMono
, showProof, showPrf
-- , testInterface
)
where
import DatabaseDesign.Ampersand.Basics (fatalMsg,Collection (isc),Identified(..),eqCl)
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 (subst,isNeg)
import DatabaseDesign.Ampersand.Classes
import DatabaseDesign.Ampersand.Fspec.Fspec (Fspc(..),Clauses(..),RuleClause(..),Quad(..),ECArule(..),InsDel(..),PAclause(..), DnfClause(..), dnf2expr)
import DatabaseDesign.Ampersand.Fspec.ShowADL (ShowADL(..))
import DatabaseDesign.Ampersand.Fspec.ShowECA (showECA)
import DatabaseDesign.Ampersand.Fspec.ToFspec.ADL2Fspec
import DatabaseDesign.Ampersand.Fspec.ToFspec.NormalForms (conjNF,disjNF,cfProof,dfProof,nfProof,simplify,normPA,exprIsc2list, exprUni2list, exprCps2list, exprRad2list) --,proofPA) -- proofPA may be used to test derivations of PAclauses.
import DatabaseDesign.Ampersand.Misc (Lang(..),Options(..),PandocFormat(ReST),string2Blocks)
import Text.Pandoc
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 :: Fspc -> 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 :: Options -> Fspc -> Interface -> String
-- testInterface flags 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 (allClauses flags rule) | rule<-invs]++"\n"++
--{-
-- " - ECA rules:"++concat [ "\n\n "++showECA fSpec "\n> " (eca{ecaAction=normPA (ecaAction eca)})
-- ++"\n------ Derivation ----->"++showProof (showECA fSpec "\n> ") (proofPA (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<-objatsLegacy obj, editable (objctx o)]++[r | o<-objatsLegacy 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 qs
---- 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
deriveProofs :: Options -> Fspc -> [Inline]
deriveProofs flags fSpec
= [ Str ("Rules and their conjuncts for "++name fSpec), LineBreak
] ++
-- conjuncts = map disjuncts.exprIsc2list.conjNF.rrexp
intercalate [LineBreak,Str "-- next rule ------------", LineBreak]
[ [ Str "rule r: ", Str (showADL r), LineBreak]++
[ Str "rrexp r: ", Str (showADL (rrexp r)), LineBreak]++
[ Str "conjNF: ", Str (showADL (conjNF (rrexp r))), LineBreak]++
intercalate [LineBreak] [ [Str " conj: ", Str (showADL conj)] | conj<-conjuncts r]
| r<-grules fSpec++vrules fSpec] ++
[ --"\nSignals for "++name fSpec++"\n--------------\n"++
--proof (signals fSpec)++
LineBreak
, Str ("Transformation of user specified rules into ECA rules for "++name fSpec)
, LineBreak, Str "--------------", LineBreak, Str "--------------", LineBreak
, LineBreak, Str "First step: determine all (", Str (show (length qs)), Str ") quads", LineBreak
, LineBreak, Str "-- first quad ------------", LineBreak
]
++
intercalate [LineBreak,Str "-- next quad ------------",LineBreak]
[ [ Str "When relation ", Str (showADL rel), Str " is changed,"
, LineBreak, Str (showADL r)
]++ (if length (cl_conjNF ccrs)<=1 then [Space] else [Str " (", Str (show (length (cl_conjNF ccrs))), Str " conjuncts)"]) ++
[ Str " must be restored.", LineBreak, Str "This quad has conjunct: ", Str (showADL (rc_conjunct x))
, Str " and ", Str (show (length (rc_dnfClauses x))), Str " dnf clauses."
]++
[ inl
| dc<-(rc_dnfClauses x), inl<-[LineBreak, Str "Dnf clause ", Str (showADL dc)]]
| Quad rel ccrs<-qs, let r=cl_rule ccrs , x<-cl_conjNF ccrs ]
++
[ LineBreak, Str "-- end ------------", LineBreak, LineBreak, Str "Second step: assemble dnf clauses."
, LineBreak, Str "-- first dnf clause ------------", LineBreak]
++
intercalate [LineBreak,Str "-- next dnf clause ------------",LineBreak]
[ [ Str "Dnf clause ", Str (showADL dc)
, LineBreak, Str "is derived from rule ", Str (showADL r)
, LineBreak
, Str ( case ms of
[] -> "no relations affect this clause"
[rel] -> "It can be called when relation " ++showADL rel++" is affected."
_ -> "It can be called when relations "++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
]
]
++
[ LineBreak, Str "-- end ------------", LineBreak, LineBreak, Str "Third step: determine ECA rules"] ++
[ if verboseP flags
then Str " (Turn --verbose off if you want to see ECA rules only)"
else Str " (Turn on --verbose if you want to see more detail)" ] ++
[ LineBreak ]
++
concat
[ [ LineBreak,Str "-- ECA Rule ", Str (show (ecaNum ecarule)), Str " ---------", LineBreak
, Str (showECA fSpec "\n " ecarule{ecaAction=normPA (ecaAction ecarule)}) ]++
concat [ [ LineBreak, Str "delta expression", LineBreak, Space, Str (showADL d)
, LineBreak, Str "derivation:"
, LineBreak, Space]++
(showProof showADL. nfProof showADL) d ++ -- nfProof produces its result in disjunctive normal form
[ LineBreak, Str "disjunctly normalized delta expression"
, LineBreak, Str (showADL (disjNF d))
]
| verboseP flags, e@Do{}<-[ecaAction ecarule], let d = paDelta e ]
| ecarule <- ecaRs]
++
[ LineBreak, Str "--------------", LineBreak, LineBreak, Str "Fourth step: cascade blocking rules"
, LineBreak
]++
intercalate []
[ [LineBreak, Str ("-- Raw ECA rule "++show (ecaNum er)++"------------"), LineBreak, Str (showECA fSpec "\n " er)]
| er<- ecaRs]
++
[ LineBreak, Str "--------------", LineBreak, LineBreak, Str "Fifth step: preEmpt the rules (= optimize)"
, LineBreak
]++
{- TODO: readdress preEmpt. It is wrong
intercalate []
[ [LineBreak, Str ("-- Preempted ECA rule "++show (ecaNum er)++"------------"), LineBreak, Str (showECA fSpec "\n " er)]
| er<- preEmpt ecaRs]
++ -}
[ Str "--------------", LineBreak, Str "Final step: derivations --------------", LineBreak]
++
intercalate [LineBreak, Str "--------------", LineBreak]
[ derivation rule
| rule<-udefrules fSpec]++
[Str ("Aantal Rules: "++(show.length.udefrules) fSpec)]
{-
++
[ LineBreak, Str "--------------", LineBreak]
++ -- TODO: make an ontological analysis, which explains the delete behaviour.
[ Str "Ontological analysis: ", LineBreak, Str " "]
++
intercalate [LineBreak, LineBreak, Str " "]
[ [Str (name ifc), Str "("]
++ intercalate [Str ", "]
[[Str (name a), Str "[", Str ((name.target.ctx) a), Str "]"]
|a<-attributes (ifcObj ifc)]
++ [Str "):", LineBreak, Str " "]
| ifc<-interfaceS fSpec]
++
[ LineBreak, Str "--------------", LineBreak
, Str "Analyzing interfaces:", LineBreak, Str " "]
++
intercalate [LineBreak, Str " "]
[[Str (testInterface flags fSpec ifc)]
| ifc<-take 1 (interfaceG fSpec)]
++
[ LineBreak, Str "--------------", LineBreak]
-}
where
-- visible _ = True -- We take all quads into account.
qs = vquads fSpec -- 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).
-- assembleECAs :: (Relation Concept->Bool) -> [Quad] -> [ECArule]
ecaRs = assembleECAs qs -- this creates all ECA rules from the available quads. They are still raw (unoptimized).
-- relEqCls = eqCl fst4 [(rel,dnfClauses,conj,cl_rule ccrs) | Quad rel ccrs<-qs, (conj,dnfClauses)<-cl_conjNF ccrs]
-- This is what ADL2Fpsec has to say about computing ECA rules:
-- ecas
-- = [ ECA (On ev rel) delt act
-- | relEq <- relEqCls -- The material required for one relation
-- , let (rel,_,_,_) = head relEq -- This is the relation
-- , let ERel delt _ = delta (sign rel) -- delt is a placeholder for the pairs that have been inserted or deleted in rel.
-- , ev<-[Ins,Del] -- This determines the event: On ev rel
-- , let act = ALL [ CHC [ (if isTrue clause' || isTrue step then Nop else
-- if isFalse clause' then Blk else
---- if not (visible rel) then Blk else
-- let visible _ = True in genPAclause visible ev toExpr viols)
-- [(conj,causes)] -- the motivation for these actions
-- | dc@(Dnf antcs conss) <- dnfClauses
-- , let clause = dnf2expr dc
-- , let sgn = sign clause
-- , let clause' = conjNF (subst (rel, actSem Ins rel (delta (sign rel))) clause)
-- , let step = conjNF (notCpl clause .\/. clause')
-- , let viols = conjNF (notCpl clause')
-- , let negs = EUni [notCpl f | f<-antcs]
-- , let poss = EUni conss
-- , let frExpr = if ev==Ins
-- then conjNF negs
-- else conjNF poss
-- , rel `elem` relsUsedIn frExpr
-- , let toExpr = if ev==Ins
-- then conjNF poss
-- else conjNF (notCpl negs)
-- ]
-- [(conj,causes)] -- to supply motivations on runtime
-- | conjEq <- eqCl snd3 [(dnfClauses,conj,rule) | (_,dnfClauses,conj,rule)<-relEq]
-- , let causes = nub (map thd3 conjEq)
-- , let (dnfClauses,conj,_) = head conjEq
-- ]
-- [(conj,nub [r |(_,_,_,r)<-cl]) | cl<-eqCl thd4 relEq, let (_,_,conj,_) = head cl] -- to supply motivations on runtime
-- ]
-- fst4 (w,_,_,_) = w
-- snd3 (_,y,_) = y
-- thd3 (_,_,z) = z
-- thd4 (_,_,z,_) = z
--TODO: See ticket #105
derivation :: Rule -> [Inline]
derivation rule
= [Str (showADL rule)]++
( if exx'==e
then [Str " is already in conjunctive normal form", LineBreak]
else [LineBreak, Str "Convert into conjunctive normal form", LineBreak] ++ showProof showADL ((e,[],"<=>"):prf)
)++
[ LineBreak, Str "Violations are computed by (disjNF . ECpl . normexpr) rule:\n " ]++
(disjProof. notCpl. rrexp) rule++[ LineBreak, LineBreak ] ++
concat [ [LineBreak, Str "Conjunct: ", Space, Space, Space, Space, Space, Str (showADL (rc_conjunct x))]++
concat [ [LineBreak, Str "This conjunct has ", Str (show (length (rc_dnfClauses x))), Str " clauses:"] | length (rc_dnfClauses x)>1 ]++
concat [ [LineBreak, Str " Clause: ", Str (showADL clause)] | clause<-(rc_dnfClauses x)]++[ LineBreak]++
concat [ [LineBreak, Str "For each clause, let us analyse the insert- and delete events."] | length (rc_dnfClauses x)>1 ]++
concat [ [LineBreak, Str " Clause: ", Str (showADL clause), Str " may be affected by the following events:",LineBreak]++
concat [ [Str "event = ", Str (show ev), Space, Str (showADL dcl), Str " means doing the following substitution", LineBreak ] ++
[Str (showADL clause++"["++showADL dcl++":="++showADL (actSem ev dcl (delta (sign dcl)))++"] = clause'"), LineBreak ] ++
[Str ("clause' = "++showADL ex'), LineBreak ] ++
concat [ [Str ("which has CNF: "++showADL ex'), LineBreak] | clause'/=ex'] ++
[Str ("Computing the violations means to negate the conjunct: "++showADL (notClau)), LineBreak ] ++
concat [ [Str ("which has CNF: "++showADL viols), LineBreak] | notClau/=viols] ++
[Str "Now try to derive whether clause |- clause' is true... ", LineBreak, Str (showADL (notClau .\/. clause')), LineBreak, Str "<=>", LineBreak, Str (showADL step), LineBreak ]
| dcl <-relsUsedIn r
, ev<-[Ins,Del]
, let ex' = subst (dcl, actSem ev dcl (delta (sign dcl))) expr
, let clause' = conjNF ex'
, let notClau = notCpl clause'
, let step = conjNF (notClau .\/. clause')
, let viols = conjNF (notClau)
, let negs = foldr (./\.) (EDcV sgn) antcs
, let poss = foldr (.\/.) (notCpl (EDcV sgn)) conss
, let frExpr = if ev==Ins
then conjNF negs
else conjNF poss
, dcl `elem` relsUsedIn frExpr
-- , let toExpr = if ev==Ins
-- then conjNF poss
-- else conjNF (notCpl negs)
]
| clause@(Dnf antcs conss) <- rc_dnfClauses x
, let expr = dnf2expr clause, let sgn = sign expr ]
| let Clauses ts r = allClauses flags rule, x <-ts] ++
[LineBreak]
{-
[ Str ("Available code fragments on rule "++name rule++":", LineBreak ]++
intercalate [LineBreak] [showADL rule++ " yields\n"++intercalate "\n\n"
[ [Str "event = ", Str (show ev), Space, Str (showADL rel), LineBreak ] ++
[Str (showADL r++"["++showADL rel++":="++showADL (actSem ev rel (delta (sign rel)))++"] = r'"), LineBreak ] ++
[Str "r' = "] ++ conjProof r' ++ [LineBreak ] ++
[Str "viols = r'-"] ++ disjProof (ECpl r') ++ [ LineBreak ] ++
"violations, considering that the valuation of "++showADL rel++" has just been changed to "++showADL (actSem ev rel (delta (sign rel)))++
" "++conjProof (ECpl r) ++"\n"++
"reaction? evaluate r |- r' ("++(showADL.conjNF) (notCpl r .\/. r')++")"++
conjProof (notCpl r .\/. r')++"\n"++
"delta: r-/\\r' = "++conjProof (EIsc[notCpl r,r'])++
"\nNow compute a reaction\n(isTrue.conjNF) (notCpl r .\/. r') = "++show ((isTrue.conjNF) (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"++(intercalate "\n\n".map showPr.lambda ev (ERel rel)) r++"\n"++
-- "derivMono ("++showADL r++") "++show ev++" "++showADL rel++"\n = "++({-intercalate "\n". map -}showPr.derivMono r ev) rel++"\n"++
-- "\nNow compute checkMono r ev rel = \n"++show (checkMono r ev rel)++"\n"++
if (isTrue.conjNF) (notCpl r .\/. r')
then "A reaction is not required, because r |- r'. Proof:"++conjProof (notCpl r .\/. r')++"\n"
else if checkMono r ev rel
then "A reaction is not required, because r |- r'. Proof:"{-++(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 fSpec "\n " (ECA (On ev rel) delt (genPAclause visible Ins r viols conj [rule]) 0)
)
| rel<-nub [x |x<-relsUsedIn r, not (isIdent x)] -- TODO: include proofs that allow: isIdent rel'
, ev<-[Ins,Del]
, r'<-[subst (rel, actSem ev rel (delta (sign rel))) r]
-- , viols<-[conjNF (ECpl r')]
, True ] -- (isTrue.conjNF) (notCpl r .\/. r')
| r<-[dc | cs<-[allClauses flags rule], (_,dnfClauses)<-cl_conjNF cs, dc<-dnfClauses]
]
-}
where e = rrexp rule
prf = cfProof showADL e
(exx',_,_) = last prf
-- conjProof = showProof showADL . cfProof showADL
disjProof = showProof showADL . dfProof showADL
-- showPr = showProof showADL -- hoort bij de uitgecommentaarde code hierboven...
--TODO: See ticket #105
commaEng :: String -> [String] -> String
commaEng _ [] = ""
commaEng _ [x] = x
commaEng str [x,y] = x++" "++str++" "++y
commaEng str (x:y:ys) = x++", "++commaEng str (y:ys)
-- 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 :: 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 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->String) -> Proof expr -> [Inline]
showProof shw [(expr,_,_)] = [ LineBreak, Space, Space, Space, Space, Space, Space, Str (shw expr), LineBreak]
showProof shw ((expr,ss,equ):prf) = [ LineBreak, Space, Space, Space, Space, Space, Space, Str (shw expr), LineBreak] ++
(if null ss then [ Space, Space, Space, Str equ ] else
if null equ then [ Str (unwords ss) ] else
[ Space, Space, Space, Str equ, Str (" { "++intercalate " and " ss++" }") ])++
showProof shw prf
--where e'= if null prf then "" else let (expr,_,_):_ = prf in showHS options "" expr
showProof _ [] = []
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
, r_sgl = fatal 336 $ "erroneous reference to r_sgl 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)")] --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
, r_sgl = fatal 352 $ "illegal reference to r_sgl 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{} -> "\\"
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'',text,op)
| (e'',_,text,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{} = foldr (./\.) (EDcV sgn) [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 _ str _ _ = str
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