{-# 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