# LANGUAGE ViewPatterns #


module OpenTheory (
    module OpenTheory
    , module Theory.ProofSkeleton
    , module Rule
    , module Items.OpenTheoryItem
    ) where
import Control.Basics
import Control.Category
import Control.Monad.Reader
import Data.Either
import Data.List
import Data.Maybe
import qualified Data.Set as S
import Extension.Data.Label hiding (get)
import qualified Extension.Data.Label as L
import Items.OpenTheoryItem
import Theory.ProofSkeleton
import Rule
import Safe
import Term.Positions
import Theory.Model
import Theory.Proof
import TheoryObject
import Utils.Misc
import Prelude hiding (id, (.))

import Pretty
import Theory.Text.Pretty
import Control.Parallel.Strategies


  remove Sapic items and convert other items to identical item but with unit type for sapic elements
removeTranslationItems :: OpenTheory -> OpenTranslatedTheory
removeTranslationItems thy =
  Theory {_thyName=(L.get thyName thy)
          ,_thyHeuristic=(L.get thyHeuristic thy)
          ,_thyTactic=(L.get thyTactic thy)
          ,_thySignature=(L.get thySignature thy)
          ,_thyCache=(L.get thyCache thy)
          ,_thyItems = newThyItems
          ,_thyOptions =(L.get thyOptions thy)}
    where
      newThyItems = map removeTranslationElement (L.get thyItems thy)
      removeTranslationElement :: TheoryItem r p TranslationElement -> TheoryItem r p ()
      removeTranslationElement (TranslationItem _) = TranslationItem ()
      removeTranslationElement (RuleItem r) = RuleItem r
      removeTranslationElement (LemmaItem l) = LemmaItem l
      removeTranslationElement (RestrictionItem rl) = RestrictionItem rl
      removeTranslationElement (TextItem t) = TextItem t
      removeTranslationElement (PredicateItem predi) = PredicateItem predi

--open translated theory again
openTranslatedTheory :: OpenTranslatedTheory -> OpenTheory
openTranslatedTheory thy =
  Theory {_thyName=(L.get thyName thy)
          ,_thyHeuristic=(L.get thyHeuristic thy)
          ,_thyTactic=(L.get thyTactic thy)
          ,_thySignature=(L.get thySignature thy)
          ,_thyCache=(L.get thyCache thy)
          ,_thyItems = newThyItems
          ,_thyOptions =(L.get thyOptions thy)}
    where
      newThyItems = mapMaybe addTranslationElement (L.get thyItems thy)
      addTranslationElement :: TheoryItem r p () -> Maybe (TheoryItem r p s)
      addTranslationElement (RuleItem r) = Just $ RuleItem r
      addTranslationElement (LemmaItem l) = Just $ LemmaItem l
      addTranslationElement (RestrictionItem rl) = Just $ RestrictionItem rl
      addTranslationElement (TextItem t) = Just $ TextItem t
      addTranslationElement (PredicateItem predi) = Just $ PredicateItem predi
      addTranslationElement (TranslationItem _) = Nothing

-- | Add an auto-generated sources lemma if possible
addAutoSourcesLemmaDiff :: MaudeHandle
                        -> String
                        -> ClosedRuleCache
                        -> ClosedRuleCache
                        -> [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof IncrementalProof]
                        -> [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof IncrementalProof]
addAutoSourcesLemmaDiff hnd lemmaName crcLeft crcRight items =
    diffPart ++ lhsPart ++ rhsPart
  where
  We split items into three . DiffRules , DiffLemmas , and DiffTextItems are
    -- kept as is. We apply addAutoSourcesLemma on each side (rules, lemmas and
    -- restrictions), and recompose everything.
    diffPart = mapMaybe f items
      where
        f (DiffRuleItem r)  = Just (DiffRuleItem r)
        f (DiffLemmaItem l) = Just (DiffLemmaItem l)
        f (DiffTextItem t)  = Just (DiffTextItem t)
        f _                 = Nothing

    lhsPart = if containsPartialDeconstructions crcLeft
        then mapMaybe (toSide LHS) $
                addAutoSourcesLemma hnd (lemmaName ++ "_LHS") crcLeft $
                  mapMaybe (filterItemSide LHS) items
        else mapMaybe (toSide LHS) $
                  mapMaybe (filterItemSide LHS) items
    rhsPart = if containsPartialDeconstructions crcRight
        then mapMaybe (toSide RHS) $
                addAutoSourcesLemma hnd (lemmaName ++ "_RHS") crcRight $
                  mapMaybe (filterItemSide RHS) items
        else mapMaybe (toSide RHS) $
                  mapMaybe (filterItemSide RHS) items

    filterItemSide s (EitherRuleItem (s', r))        | s == s' = Just (RuleItem r)
    filterItemSide s (EitherLemmaItem (s', l))       | s == s' = Just (LemmaItem l)
    filterItemSide s (EitherRestrictionItem (s', r)) | s == s' = Just (RestrictionItem r)
    filterItemSide _ _                                         = Nothing

    toSide s (RuleItem r)        = Just $ EitherRuleItem (s, r)
    toSide LHS (LemmaItem l)     = Just $ EitherLemmaItem (LHS, addLeftLemma  l)
    toSide RHS (LemmaItem l)     = Just $ EitherLemmaItem (RHS, addRightLemma l)
    toSide s (RestrictionItem r) = Just $ EitherRestrictionItem (s, r)
    toSide _ (TextItem t)        = Just $ DiffTextItem t
  FIXME : We currently ignore predicates and  stuff as they should not
    --        be generated by addAutoSourcesLemma
    toSide _ (PredicateItem _)   = Nothing
    toSide _ (TranslationItem _)       = Nothing

-- | Add an auto-generated sources lemma if possible
addAutoSourcesLemma :: MaudeHandle
                    -> String
                    -> ClosedRuleCache
                    -> [TheoryItem ClosedProtoRule IncrementalProof s]
                    -> [TheoryItem ClosedProtoRule IncrementalProof s]
addAutoSourcesLemma hnd lemmaName (ClosedRuleCache _ raw _ _) items =
  -- We only add the lemma if there is no lemma of the same name
  case find lemma items of
    Nothing  -> items'++[LemmaItem l]
    (Just _) -> items'
  where
    runMaude   = (`runReader` hnd)

    -- searching for the lemma
    lemma (LemmaItem (Lemma name _ _ _ _)) | name == lemmaName = True
    lemma _                                                    = False

    -- build the lemma
    l = fmap skeletonToIncrementalProof $ unprovenLemma lemmaName [SourceLemma] AllTraces formula

    -- extract all rules from theory items
    rules = mapMaybe itemToRule items

    -- compute all encrypted subterms that are output by protocol rules
    allOutConcs :: [(ClosedProtoRule, LNTerm)]
    allOutConcs = do
        ru                                <- rules
        (_, protoOrOutFactView -> Just t) <- enumConcs $ L.get cprRuleAC ru
        unifyProtC                        <- concatMap allProtSubterms t
        return (ru, unifyProtC)

    -- compute all fact that are conclusions in protocol rules (not OutFact)
    allOutConcsNotProt :: [(ClosedProtoRule, LNFact)]
    allOutConcsNotProt = do
        ru              <- rules
        (_, unifyFactC) <- enumConcs $ L.get cprRuleAC ru
        -- we ignore cases where the fact is OutFact
        guard (getFactTag unifyFactC /= OutFact)
        return (ru, unifyFactC)

  We use the raw sources here to generate one lemma to rule them all ...
    (items', formula, _) = foldl computeFormula (items, ltrue, []) chains

    -- Generate a list of all cases that contain open chains
    chains = concatMap (multiply unsolvedChains . duplicate) $
                   concatMap (map snd . getDisj . L.get cdCases) raw

    -- Given a list of theory items, a formula, a source with an open chain,
    -- return an updated list of theory items and an update formula for the sources lemma.
    computeFormula :: ([TheoryItem ClosedProtoRule IncrementalProof s], LNFormula, [(RuleInfo ProtoRuleName IntrRuleACInfo, ExtendedPosition)])
                   -> ((NodeConc, NodePrem), System)
                   -> ([TheoryItem ClosedProtoRule IncrementalProof s], LNFormula, [(RuleInfo ProtoRuleName IntrRuleACInfo, ExtendedPosition)])
    computeFormula (its, form, done) ((conc,_), source) = (its', form', done')
      where
        -- The new items are the old ones but with added labels
        its'  = addLabels inputsAndOutputs its
        -- The new formula is the old one AND the new formula
        form' = addFormula inputsAndOutputs form
        -- The new list of treated cases
        done' = addCases inputsAndOutputs done

        -- Variable causing the open chain
        v     = head $ getFactTerms $ nodeConcFact conc source

        -- Compute all rules that contain v, and the position of v inside the input term
        inputRules :: [(ClosedProtoRule, Either LNTerm LNFact, ExtendedPosition)]
        inputRules = concat $ mapMaybe g $ allPrems source
          where
            g (nodeid, pid, tidx, term) = do
              position <- findPos v term
              ruleSys  <- nodeRuleSafe nodeid source
              rule     <- find ((ruleName ruleSys ==).ruleName) rules
              premise  <- lookupPrem pid $ L.get cprRuleAC rule
              t'       <- protoOrInFactView premise
              t        <- atMay t' tidx
              return (terms position rule t ++ facts position rule t premise)
                where
                  terms position rule t = do
                    -- iterate over all positions found
                    pos     <- position
                    return (rule, Left t, (pid, tidx, pos))
                  facts position rule t premise = do
                        -- we only consider protocol facts and unprotected terms
                    guard $ isProtoFact premise && (isPair t || isAC t || isMsgVar t)
                        -- we only consider facts which are not already solved in the source
                        && ((nodeid, pid) `elem` map fst (unsolvedPremises source))
                    -- iterate over all positions found
                    pos     <- position
                    return (rule, Right premise, (pid, tidx, pos))

        -- a list of all input subterms to unify : Left for protected subterm and Right for non protected subterm
        premiseTermU :: [(ClosedProtoRule, Either (LNTerm, LNTerm) LNFact, ExtendedPosition)]
        premiseTermU = mapMaybe f inputRules
          where
  cases for protected subterms : we consider the deepest protected subterm
            f (x, Left y, (pidx, tidx, z)) = do
              v'        <- y `atPosMay` z
              protTerm' <- deepestProtSubterm y z
              -- We do not consider the case where the computed deepest
  protected subterm is the variable in question , as this
              -- against the definition (a variable is not a function).
              -- Moreover, this case
  1 . often leads to false lemmas as we do not unify with all
              --    conclusion facts, in particular not with fresh facts
  2 . blows up the lemma as a variable unifies with all outputs
  3 . typically only happens if a value is stored in a state fact ,
              --    which is handled by the other case
              protTerm  <- if protTerm' == v'
                then Nothing
                else Just protTerm'
              return (x, Left (protTerm, v'), (pidx, tidx, z))
            -- cases for non-protected subterms : we consider the Fact
            f (x, Right fact, (pidx, tidx, z)) =
              return (x, Right fact, (pidx, tidx, z))

        -- compute matching outputs
        -- returns a list of inputs together with their list of matching outputs
        inputsAndOutputs :: [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
        inputsAndOutputs = do
            -- iterate over all inputs
            (rin, unify, pos) <- filterFacts premiseTermU
            -- find matching conclusions
            let matches = matchingConclusions rin unify
            return (rin, matches, pos)
          where
            -- we ignore fact cases which are covered by the protected subterms
            filterFacts cases = mapMaybe f cases
              where
                f c@(r, Left  _, p) = do
                  guard $ notElem (ruleName r, p) done
                  return c
                f c@(r, Right _, p) = do
                  guard $ notElem (ruleName r, p) done
                         && null subtermCasePositions
                  return c
                -- check if there are protected subterms for this variable
                subtermCasePositions = filter (isLeft . snd3) cases

            matchingConclusions rin (Left (unify, vin)) = Left (unify, vin, do
              (rout, tout) <- allOutConcs
              -- generate fresh instance of conclusion, avoiding the premise variables
              let fout = tout `renameAvoiding` unify
              -- we ignore outputs of the same rule
              guard ((ruleName . L.get cprRuleE) rin /= (ruleName . L.get cprRuleE) rout)
              -- check whether input and output are unifiable
              guard (runMaude $ unifiableLNTerms unify fout)
              return (rout, tout))
            matchingConclusions rin (Right unify) = Right (unify, do
              (rout, fout) <- allOutConcsNotProt
              -- we ignore outputs of the same rule
              guard ((ruleName . L.get cprRuleE) rin /= (ruleName . L.get cprRuleE) rout)
              -- we ignore cases where the output fact and the input fact have different name
              guard (factTagName (getFactTag unify) == factTagName (getFactTag fout))
              -- check whether input and output are unifiable
              let unifout = fout `renameAvoiding` unify
              guard (runMaude $ unifiableLNFacts unify unifout)
              return (rout, fout))

        -- construct action facts for the rule annotations and formula
        inputFactTerm pos ru terms var = Fact {factTag = ProtoFact Linear
              ("AUTO_IN_TERM_" ++ printPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (1 + length terms),
              factAnnotations = S.empty, factTerms = terms ++[var]}
        inputFactFact pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_IN_FACT_" ++ printFactPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}
        outputFactTerm pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_OUT_TERM_" ++ printPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}
        outputFactFact pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_OUT_FACT_" ++ printFactPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}

        -- add labels to rules for typing lemma
        addLabels :: [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
                  -> [TheoryItem ClosedProtoRule IncrementalProof s]
                  -> [TheoryItem ClosedProtoRule IncrementalProof s]
        addLabels matches = map update
          where
            update (RuleItem ru) = RuleItem $ foldr up ru $
                   filter ((ruleName ru ==). ruleName . fst3) acts
              where
                up (r, p, Left  (Left  (t, v'))) r' = addActionClosedProtoRule r' (inputFactTerm  p r [t] v')
                up (r, p, Left  (Right f))       r' = addActionClosedProtoRule r' (inputFactFact  p r (getFactTerms f))
                up (_, p, Right (r, Left  t))    r' = addActionClosedProtoRule r' (outputFactTerm p r [t])
                up (_, p, Right (r, Right f))    r' = addActionClosedProtoRule r' (outputFactFact p r (getFactTerms f))
            update item          = item

            acts = concatMap prepare matches
            -- Left Left means Input Term
            -- Left Right means Input Fact
            -- Right Left means Output Term
            -- Right Left means Output Fact
            prepare (r, Left  (t, v', tl), p) = (r, p, Left (Left  (t, v'))) : map (\(r', t') -> (r', p, Right (r, Left  t'))) tl
            prepare (r, Right (f, fl)    , p) = (r, p, Left (Right f))       : map (\(r', f') -> (r', p, Right (r, Right f'))) fl

        listOfM :: Int -> [String]
        listOfM n = zipWith (++) (replicate n "m") $ fmap show [1..n]

        -- add formula to lemma
        addFormula ::
             [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
          -> LNFormula
          -> LNFormula
        addFormula matches f = foldr addForm f matches
          where
            addForm ::
                 (ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)
              -> LNFormula
              -> LNFormula
            -- protected subterms: if there are no matching outputs, do add a formula with only KU
            addForm (ru, Left (_, _, []), p) f' = f' .&&. Qua All ("x", LSortMsg)
              (Qua All ("m", LSortMsg) (Qua All ("i", LSortNode)
              (Conn Imp (Ato (Action (varTerm (Bound 0))
              (inputFactTerm p ru [varTerm (Bound 1)] (varTerm (Bound 2)))))
              orKU)))
            -- protected subterms
            addForm (ru, Left _, p) f' = f' .&&. Qua All ("x", LSortMsg)
              (Qua All ("m", LSortMsg) (Qua All ("i", LSortNode)
              (Conn Imp (Ato (Action (varTerm (Bound 0))
              (inputFactTerm p ru [varTerm (Bound 1)] (varTerm (Bound 2)))))
              (toFactsTerm ru p orKU))))
            -- facts: even if there are no matching outputs, do add a formula with "false"
            addForm (ru, Right (m, []),     p) f' = f' .&&. formulaMultArity (factArity m)
              where formulaMultArity nb = foldr (\h -> Qua All (h,LSortMsg))
                           (Qua All ("i", LSortNode)
                           (Conn Imp (Ato (Action (varTerm (Bound 0))
                           (inputFactFact p ru (listVarTerm (toInteger $ factArity m) 1))))
                           lfalse)) (listOfM nb)
            -- facts
            addForm (ru, Right (m, outs:_), p) f' = f' .&&. formulaMultArity (factArity m)
              where formulaMultArity nb = foldr (\h -> Qua All (h,LSortMsg))
                           (Qua All ("i", LSortNode)
                           (Conn Imp (Ato (Action (varTerm (Bound 0))
                           (inputFactFact p ru (listVarTerm (toInteger $ factArity m) 1))))
                           (toFactsFact ru p (snd outs)))) (listOfM nb)
            orKU = Qua Ex ("j",LSortNode)
                   (Conn And (Ato (Action (varTerm (Bound 0))
                    Fact {factTag = KUFact, factAnnotations = S.empty,
                          factTerms = [varTerm (Bound 3)]} ))
                   (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1)))))
            toFactsTerm ru p f'' =
              Conn Or f''
              (Qua Ex ("j",LSortNode)
              (Conn And (Ato (Action (varTerm (Bound 0))
              (outputFactTerm p ru [varTerm (Bound 2)]) ))
              (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1))))))
            toFactsFact ru p outn =
              Qua Ex ("j",LSortNode)
              (Conn And (Ato (Action (varTerm (Bound 0))
              (outputFactFact p ru (listVarTerm (toInteger $ 1 + factArity outn) 2)) ))
              (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1)))))
            listVarTerm q s | q == s    = [varTerm (Bound q)]
            listVarTerm q s | otherwise = varTerm (Bound q) : listVarTerm (q-1) s

        -- add all cases (identified by rule name and input variable position) to the list of treated cases
        addCases matches d = d ++ map (\(r, _, p) -> (ruleName r, p)) matches

-- | Add a new process expression.  since expression (and not definitions)
-- could appear several times, checking for doubled occurrence isn't necessary

------------------------------------------------------------------------------
-- Open theory construction / modification
------------------------------------------------------------------------------
defaultOption :: Option
defaultOption = Option False False False False False False False S.empty [] 10 5



-- | Default theory
defaultOpenTheory :: Bool -> OpenTheory
defaultOpenTheory flag = Theory "default" [] [] (emptySignaturePure flag) [] [] defaultOption

-- | Default diff theory
defaultOpenDiffTheory :: Bool -> OpenDiffTheory
defaultOpenDiffTheory flag = DiffTheory "default" [] [] (emptySignaturePure flag) [] [] [] [] [] defaultOption

-- Add the default Diff lemma to an Open Diff Theory
addDefaultDiffLemma:: OpenDiffTheory -> OpenDiffTheory
addDefaultDiffLemma thy = fromMaybe thy $ addDiffLemma (unprovenDiffLemma "Observational_equivalence" []) thy

-- Add the rule labels to an Open Diff Theory
addProtoRuleLabel :: OpenProtoRule -> OpenProtoRule
addProtoRuleLabel rule = addProtoDiffLabel rule ("DiffProto" ++ (getOpenProtoRuleName rule))

-- Get the left openProtoRules
getLeftProtoRule :: DiffProtoRule -> OpenProtoRule
getLeftProtoRule (DiffProtoRule ruE Nothing)       = OpenProtoRule (getLeftRule ruE) []
getLeftProtoRule (DiffProtoRule _   (Just (l, _))) = l

  Get the  openProtoRules
getRightProtoRule :: DiffProtoRule -> OpenProtoRule
getRightProtoRule (DiffProtoRule ruE Nothing)       = OpenProtoRule (getRightRule ruE) []
getRightProtoRule (DiffProtoRule _   (Just (_, r))) = r

-- Add the rule labels to an Open Diff Theory
addIntrRuleLabels:: OpenDiffTheory -> OpenDiffTheory
addIntrRuleLabels thy =
    modify diffThyCacheLeft (map addRuleLabel) $ modify diffThyDiffCacheLeft (map addRuleLabel) $ modify diffThyDiffCacheRight (map addRuleLabel) $ modify diffThyCacheRight (map addRuleLabel) thy
  where
    addRuleLabel :: IntrRuleAC -> IntrRuleAC
    addRuleLabel rule = addDiffLabel rule ("DiffIntr" ++ (getRuleName rule))

-- | Returns true if there are OpenProtoRules containing manual variants
containsManualRuleVariants :: [TheoryItem OpenProtoRule p s] -> Bool
containsManualRuleVariants = foldl f False
  where
    f hasVariants (RuleItem (OpenProtoRule _ [])) = hasVariants
    f _           (RuleItem (OpenProtoRule _ _ )) = True
    f hasVariants _                               = hasVariants

-- | Merges variants of the same protocol rule modulo E
mergeOpenProtoRules :: [TheoryItem OpenProtoRule p s] -> [TheoryItem OpenProtoRule p s]
mergeOpenProtoRules = concatMap (foldr mergeRules []) . groupBy comp
  where
    comp (RuleItem (OpenProtoRule ruE _)) (RuleItem (OpenProtoRule ruE' _)) = ruE == ruE'
    comp (RuleItem _) _ = False
    comp _ (RuleItem _) = False
    comp _ _            = True

    mergeRules (RuleItem r)                          []                                              = [RuleItem r]
    mergeRules (RuleItem (OpenProtoRule ruE' ruAC')) [RuleItem (OpenProtoRule ruE ruAC)] | ruE==ruE' = [RuleItem (OpenProtoRule ruE (ruAC'++ruAC))]
    mergeRules (RuleItem _)                          _                                               = error "Error in mergeOpenProtoRules. Please report bug."
    mergeRules item                                  l                                               = item:l

-- | Returns true if there are DiffProtoRules containing manual instances or variants
containsManualRuleVariantsDiff :: [DiffTheoryItem DiffProtoRule r p p2] -> Bool
containsManualRuleVariantsDiff = foldl f False
  where
    f hasVariants (DiffRuleItem (DiffProtoRule _ Nothing )) = hasVariants
    f _           (DiffRuleItem (DiffProtoRule _ (Just _))) = True
    f hasVariants _                                         = hasVariants

-- | Merges variants of the same protocol rule modulo E
mergeOpenProtoRulesDiff :: [DiffTheoryItem r OpenProtoRule p p2] -> [DiffTheoryItem r OpenProtoRule p p2]
mergeOpenProtoRulesDiff = concatMap (foldr mergeRules []) . groupBy comp
  where
    comp (EitherRuleItem (s, OpenProtoRule ruE _)) (EitherRuleItem (s', OpenProtoRule ruE' _)) = ruE==ruE' && s==s'
    comp (EitherRuleItem _) _ = False
    comp _ (EitherRuleItem _) = False
    comp _ _                  = True

    mergeRules (EitherRuleItem r)                             [] = [EitherRuleItem r]
    mergeRules (EitherRuleItem (s, OpenProtoRule ruE' ruAC')) [EitherRuleItem (s', OpenProtoRule ruE ruAC)]
                                            | ruE==ruE' && s==s' = [EitherRuleItem (s, OpenProtoRule ruE (ruAC'++ruAC))]
    mergeRules (EitherRuleItem _)                             _  = error "Error in mergeOpenProtoRulesDiff. Please report bug."
    mergeRules item                                           l  = item:l

-- | Merges left and right instances with initial diff rule
mergeLeftRightRulesDiff :: (Show p, Show p2) => [DiffTheoryItem DiffProtoRule OpenProtoRule p p2] -> [DiffTheoryItem DiffProtoRule OpenProtoRule p p2]
mergeLeftRightRulesDiff rs = map clean $ concatMap (foldr mergeRules []) $ groupBy comp' $ sortBy comp rs
  where
    comp (EitherRuleItem (_, OpenProtoRule ruE _)) (EitherRuleItem (_, OpenProtoRule ruE' _)) = compare (ruleName ruE) (ruleName ruE')
    comp (EitherRuleItem (_, OpenProtoRule ruE _)) (DiffRuleItem (DiffProtoRule ruE' _))      = compare (ruleName ruE) (ruleName ruE')
    comp (DiffRuleItem (DiffProtoRule ruE _))      (EitherRuleItem (_, OpenProtoRule ruE' _)) = compare (ruleName ruE) (ruleName ruE')
    comp (DiffRuleItem (DiffProtoRule ruE _))      (DiffRuleItem (DiffProtoRule ruE' _))      = compare (ruleName ruE) (ruleName ruE')
    comp (EitherRuleItem _) _ = LT
    comp _ (EitherRuleItem _) = GT
    comp (DiffRuleItem _) _   = LT
    comp _ (DiffRuleItem _)   = GT
    comp _ _                  = EQ

    comp' a b = comp a b == EQ

    mergeRules (EitherRuleItem r)                                 [] = [EitherRuleItem r]
    mergeRules (DiffRuleItem r)                                   [] = [DiffRuleItem r]
    mergeRules (EitherRuleItem (s, ru@(OpenProtoRule ruE _)))     [EitherRuleItem (s', ru'@(OpenProtoRule ruE' _))]
                                            | ruleName ruE==ruleName ruE' && s==LHS && s'==RHS = [DiffRuleItem (DiffProtoRule ruE (Just (ru, ru')))]
    mergeRules (EitherRuleItem (s, ru@(OpenProtoRule ruE _)))     [EitherRuleItem (s', ru'@(OpenProtoRule ruE' _))]
                                            | ruleName ruE==ruleName ruE' && s==RHS && s'==LHS = [DiffRuleItem (DiffProtoRule ruE (Just (ru', ru)))]
    mergeRules (EitherRuleItem (_, ru@(OpenProtoRule ruE _)))     [DiffRuleItem (DiffProtoRule dru Nothing)]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru Nothing))         [EitherRuleItem (_, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru)))]
    mergeRules (EitherRuleItem (LHS, ru@(OpenProtoRule ruE _)))   [DiffRuleItem (DiffProtoRule dru (Just (_, ru')))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru')))]
    mergeRules (EitherRuleItem (RHS, ru@(OpenProtoRule ruE _)))   [DiffRuleItem (DiffProtoRule dru (Just (ru', _)))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru', ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (_, ru')))) [EitherRuleItem (LHS, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru')))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (ru', _)))) [EitherRuleItem (RHS, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru', ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))) [DiffRuleItem (DiffProtoRule dru' Nothing)]
                                            | ruleName dru==ruleName dru' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru Nothing))         [DiffRuleItem (DiffProtoRule dru' (Just (lr, rr)))]
                                            | ruleName dru==ruleName dru' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))) [DiffRuleItem (DiffProtoRule dru' (Just (lr', rr')))]
                                            | ruleName dru==ruleName dru' && equalOpenRuleUpToDiffAnnotation lr lr' && equalOpenRuleUpToDiffAnnotation rr rr' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (EitherRuleItem _)                                 _  = error "Error in mergeLeftRightRulesDiff. Please report bug."
    mergeRules (DiffRuleItem _)                                   _  = error "Error in mergeLeftRightRulesDiff. Please report bug."
    mergeRules item                                               l  = item:l

    clean (DiffRuleItem (DiffProtoRule ruE (Just (OpenProtoRule ruEL [], OpenProtoRule ruER []))))
       | getLeftRule ruE `equalRuleUpToDiffAnnotation` ruEL
        && getRightRule ruE `equalRuleUpToDiffAnnotation` ruER = DiffRuleItem (DiffProtoRule ruE Nothing)
    clean i                                                    = i


-- | Find the open protocol rule with the given name.
lookupOpenProtoRule :: ProtoRuleName -> OpenTheory -> Maybe OpenProtoRule
lookupOpenProtoRule name =
    find ((name ==) . L.get (preName . rInfo . oprRuleE)) . theoryRules

-- | Find the open protocol rule with the given name.
lookupOpenDiffProtoDiffRule :: ProtoRuleName -> OpenDiffTheory -> Maybe DiffProtoRule
lookupOpenDiffProtoDiffRule name =
    find ((name ==) . L.get (preName . rInfo . dprRule)) . diffTheoryDiffRules

-- | Add new protocol rules. Fails, if a protocol rule with the same name
-- exists.
addOpenProtoRule :: OpenProtoRule -> OpenTheory -> Maybe OpenTheory
addOpenProtoRule ru@(OpenProtoRule ruE ruAC) thy = do
    guard nameNotUsedForDifferentRule
    guard allRuleNamesAreDifferent
    return $ modify thyItems (++ [RuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenProtoRule (L.get (preName . rInfo . oprRuleE) ru) thy
    allRuleNamesAreDifferent = (S.size (S.fromList (ruleName ruE:map ruleName ruAC)))
        == ((length ruAC) + 1)

-- | Add a new protocol rules. Fails, if a protocol rule with the same name
-- exists.
addOpenProtoDiffRule :: DiffProtoRule -> OpenDiffTheory -> Maybe OpenDiffTheory
addOpenProtoDiffRule ru@(DiffProtoRule _ Nothing)  thy = do
    guard nameNotUsedForDifferentRule
    return $ modify diffThyItems (++ [DiffRuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo . dprRule) ru) thy
addOpenProtoDiffRule ru@(DiffProtoRule _ (Just (lr, rr))) thy = do
    guard nameNotUsedForDifferentRule
    guard $ allRuleNamesAreDifferent lr
    guard $ allRuleNamesAreDifferent rr
    guard leftAndRightHaveSameName
    return $ modify diffThyItems (++ [DiffRuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo . dprRule) ru) thy
    allRuleNamesAreDifferent (OpenProtoRule ruE ruAC) = (S.size (S.fromList (ruleName ruE:map ruleName ruAC)))
        == ((length ruAC) + 1)
    leftAndRightHaveSameName = ruleName ru == ruleName lr && ruleName lr == ruleName rr

-- | Add new protocol rules. Fails, if a protocol rule with the same name
-- exists. Ignore _restrict construct.
addProtoRule :: ProtoRuleE -> OpenTheory -> Maybe OpenTheory
addProtoRule ruE thy = do
    guard nameNotUsedForDifferentRule
    return $ modify thyItems (++ [RuleItem (OpenProtoRule ruE [])]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ruE ==) $ fmap (L.get oprRuleE) $ lookupOpenProtoRule (L.get (preName . rInfo) ruE) thy

-- | Add a new protocol rules. Fails, if a protocol rule with the same name
-- exists.
addProtoDiffRule :: ProtoRuleE -> OpenDiffTheory -> Maybe OpenDiffTheory
addProtoDiffRule ruE thy = do
    guard nameNotUsedForDifferentRule
    return $ modify diffThyItems (++ [DiffRuleItem (DiffProtoRule ruE Nothing)]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ruE ==) $ fmap (L.get dprRule) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo) ruE) thy

  | Add intruder proof rules after Translate .
addIntrRuleACsAfterTranslate :: [IntrRuleAC] -> OpenTranslatedTheory -> OpenTranslatedTheory
addIntrRuleACsAfterTranslate rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')

-- | Add intruder proof rules.
addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheory
addIntrRuleACs rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')

-- | Add intruder proof rules for all diff and non-diff caches.
addIntrRuleACsDiffAll :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffAll rs' thy = addIntrRuleACsDiffBoth rs' (addIntrRuleACsDiffBothDiff rs' thy)

-- | Add intruder proof rules for both diff caches.
addIntrRuleACsDiffBothDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffBothDiff rs' thy = addIntrRuleACsDiffRightDiff rs' (addIntrRuleACsDiffLeftDiff rs' thy)

-- | Add intruder proof rules for both caches.
addIntrRuleACsDiffBoth :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffBoth rs' thy = addIntrRuleACsDiffRight rs' (addIntrRuleACsDiffLeft rs' thy)

-- | Add intruder proof rules to left diff cache.
addIntrRuleACsDiffLeftDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffLeftDiff rs' thy = modify (diffThyDiffCacheLeft) (\rs -> nub $ rs ++ rs') thy

-- | Add intruder proof rules to left cache.
addIntrRuleACsDiffLeft :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffLeft rs' thy = modify (diffThyCacheLeft) (\rs -> nub $ rs ++ rs') thy

-- | Add intruder proof rules to right diff cache.
addIntrRuleACsDiffRightDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffRightDiff rs' thy = modify (diffThyDiffCacheRight) (\rs -> nub $ rs ++ rs') thy

-- | Add intruder proof rules to right cache.
addIntrRuleACsDiffRight :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffRight rs' thy = modify (diffThyCacheRight) (\rs -> nub $ rs ++ rs') thy

-- | Normalize the theory representation such that they remain semantically
  equivalent . Use this function when you want to compare two theories ( quite
-- strictly) for semantic equality; e.g., when testing the parser.
normalizeTheory :: OpenTheory -> OpenTheory
normalizeTheory =
    L.modify thyCache sort
  . L.modify thyItems (\items -> do
      item <- items
      return $ case item of
          LemmaItem lem ->
              LemmaItem $ L.modify lProof stripProofAnnotations $ lem
          RuleItem _    -> item
          TextItem _    -> item
          RestrictionItem _   -> item
          TranslationItem _   -> item
          PredicateItem _   -> item
          )
  where
    stripProofAnnotations :: ProofSkeleton -> ProofSkeleton
    stripProofAnnotations = fmap stripProofStepAnnotations
    stripProofStepAnnotations (ProofStep method ()) =
        ProofStep (case method of
                     Sorry _         -> Sorry Nothing
                     Contradiction _ -> Contradiction Nothing
                     _               -> method)
                  ()








-- | Pretty print an open rule together with its assertion soundness proof.
prettyOpenProtoRule :: HighlightDocument d => OpenProtoRule -> d
prettyOpenProtoRule (OpenProtoRule ruE [])       = prettyProtoRuleE ruE
prettyOpenProtoRule (OpenProtoRule _   [ruAC])   = prettyProtoRuleACasE ruAC
prettyOpenProtoRule (OpenProtoRule ruE variants) = prettyProtoRuleE ruE $-$
    nest 1 (kwVariants $-$ nest 1 (ppList prettyProtoRuleAC variants))
  where
    ppList _  []     = emptyDoc
    ppList pp [x]    = pp x
    ppList pp (x:xr) = pp x $-$ comma $-$ ppList pp xr

-- | Pretty print an open rule together with its assertion soundness proof.
prettyOpenProtoRuleAsClosedRule :: HighlightDocument d => OpenProtoRule -> d
prettyOpenProtoRuleAsClosedRule (OpenProtoRule ruE [])
    = prettyProtoRuleE ruE $--$
    -- cannot show loop breakers here, as we do not have the information
    (nest 2 $ emptyDoc $-$
     multiComment_ ["has exactly the trivial AC variant"])
prettyOpenProtoRuleAsClosedRule (OpenProtoRule _ [ruAC@(Rule (ProtoRuleACInfo _ _ (Disj disj) _) _ _ _ _)])
    = prettyProtoRuleACasE ruAC $--$
    (nest 2 $ prettyLoopBreakers (L.get rInfo ruAC) $-$
     if length disj == 1 then
       multiComment_ ["has exactly the trivial AC variant"]
     else
       multiComment $ prettyProtoRuleAC ruAC
    )
prettyOpenProtoRuleAsClosedRule (OpenProtoRule ruE variants) = prettyProtoRuleE ruE $-$
    nest 1 (kwVariants $-$ nest 1 (ppList prettyProtoRuleAC variants))
  where
    ppList _  []     = emptyDoc
    ppList pp [x]    = pp x
    ppList pp (x:xr) = pp x $-$ comma $-$ ppList pp xr

-- | Pretty print a diff rule
prettyDiffRule :: HighlightDocument d => DiffProtoRule -> d
prettyDiffRule (DiffProtoRule ruE Nothing           ) = prettyProtoRuleE ruE
prettyDiffRule (DiffProtoRule ruE (Just (ruL,  ruR))) = prettyProtoRuleE ruE $-$
    nest 1
    (kwLeft  $-$ nest 1 (prettyOpenProtoRule ruL) $-$
     kwRight $-$ nest 1 (prettyOpenProtoRule ruR))

-- | Pretty print an either rule
prettyEitherRule :: HighlightDocument d => (Side, OpenProtoRule) -> d
prettyEitherRule (_, p) = prettyProtoRuleE $ L.get oprRuleE p




-- | Pretty print an open theory.
prettyOpenTheory :: HighlightDocument d => OpenTheory -> d
prettyOpenTheory thy =
    prettyTheory (prettySignaturePureExcept funsyms)
                 (const emptyDoc) prettyOpenProtoRule prettyProof prettyTranslationElement thy
                 -- prettyIntrVariantsSection prettyOpenProtoRule prettyProof
                 where
                    funsyms = S.fromList $ map fst' $ theoryFunctionTypingInfos thy
  function symbols that are printed by sapic printer already
                    fst' (a,_,_) = a

-- | Pretty print an open theory.
prettyOpenDiffTheory :: HighlightDocument d => OpenDiffTheory -> d
prettyOpenDiffTheory =
    prettyDiffTheory prettySignaturePure
                 (const emptyDoc) prettyEitherRule prettyDiffProof prettyProof
                 -- prettyIntrVariantsSection prettyOpenProtoRule prettyProof

-- | Pretty print a translated Open Theory
prettyOpenTranslatedTheory :: HighlightDocument d => OpenTranslatedTheory -> d
prettyOpenTranslatedTheory =
    prettyTheory prettySignaturePure
                 (const emptyDoc) prettyOpenProtoRule prettyProof emptyString


-- | Pretty print a diff theory.
prettyDiffTheory :: HighlightDocument d
                 => (sig -> d) -> (c -> d) -> ((Side, r2) -> d) -> (p -> d) -> (p2 -> d)
                 -> DiffTheory sig c DiffProtoRule r2 p p2 -> d
prettyDiffTheory ppSig ppCache ppRule ppDiffPrf ppPrf thy = vsep $
    [ kwTheoryHeader $ text $ L.get diffThyName thy
    , lineComment_ "Function signature and definition of the equational theory E"
    , ppSig $ L.get diffThySignature thy
    , if thyT == [] then text "" else vcat $ map prettyTactic thyT
    , if thyH == [] then text "" else text "heuristic: " <> text (prettyGoalRankings thyH)
    , ppCache $ L.get diffThyCacheLeft thy
    , ppCache $ L.get diffThyCacheRight thy
    , ppCache $ L.get diffThyDiffCacheLeft thy
    , ppCache $ L.get diffThyDiffCacheRight thy
    ] ++
    parMap rdeepseq ppItem (L.get diffThyItems thy) ++
    [ kwEnd ]
  where
    ppItem = foldDiffTheoryItem
        prettyDiffRule ppRule (prettyDiffLemma ppDiffPrf) (prettyEitherLemma ppPrf) prettyEitherRestriction (uncurry prettyFormalComment)
    thyH = L.get diffThyHeuristic thy
    thyT = L.get diffThyTactic thy


open translated theory again
 | Add an auto-generated sources lemma if possible
 kept as is. We apply addAutoSourcesLemma on each side (rules, lemmas and
 restrictions), and recompose everything.
        be generated by addAutoSourcesLemma
 | Add an auto-generated sources lemma if possible
 We only add the lemma if there is no lemma of the same name
 searching for the lemma
 build the lemma
 extract all rules from theory items
 compute all encrypted subterms that are output by protocol rules
 compute all fact that are conclusions in protocol rules (not OutFact)
 we ignore cases where the fact is OutFact
 Generate a list of all cases that contain open chains
 Given a list of theory items, a formula, a source with an open chain,
 return an updated list of theory items and an update formula for the sources lemma.
 The new items are the old ones but with added labels
 The new formula is the old one AND the new formula
 The new list of treated cases
 Variable causing the open chain
 Compute all rules that contain v, and the position of v inside the input term
 iterate over all positions found
 we only consider protocol facts and unprotected terms
 we only consider facts which are not already solved in the source
 iterate over all positions found
 a list of all input subterms to unify : Left for protected subterm and Right for non protected subterm
 We do not consider the case where the computed deepest
 against the definition (a variable is not a function).
 Moreover, this case
    conclusion facts, in particular not with fresh facts
    which is handled by the other case
 cases for non-protected subterms : we consider the Fact
 compute matching outputs
 returns a list of inputs together with their list of matching outputs
 iterate over all inputs
 find matching conclusions
 we ignore fact cases which are covered by the protected subterms
 check if there are protected subterms for this variable
 generate fresh instance of conclusion, avoiding the premise variables
 we ignore outputs of the same rule
 check whether input and output are unifiable
 we ignore outputs of the same rule
 we ignore cases where the output fact and the input fact have different name
 check whether input and output are unifiable
 construct action facts for the rule annotations and formula
 add labels to rules for typing lemma
 Left Left means Input Term
 Left Right means Input Fact
 Right Left means Output Term
 Right Left means Output Fact
 add formula to lemma
 protected subterms: if there are no matching outputs, do add a formula with only KU
 protected subterms
 facts: even if there are no matching outputs, do add a formula with "false"
 facts
 add all cases (identified by rule name and input variable position) to the list of treated cases
 | Add a new process expression.  since expression (and not definitions)
 could appear several times, checking for doubled occurrence isn't necessary
----------------------------------------------------------------------------
 Open theory construction / modification
----------------------------------------------------------------------------
 | Default theory
 | Default diff theory
 Add the default Diff lemma to an Open Diff Theory
 Add the rule labels to an Open Diff Theory
 Get the left openProtoRules
 Add the rule labels to an Open Diff Theory
 | Returns true if there are OpenProtoRules containing manual variants
 | Merges variants of the same protocol rule modulo E
 | Returns true if there are DiffProtoRules containing manual instances or variants
 | Merges variants of the same protocol rule modulo E
 | Merges left and right instances with initial diff rule
 | Find the open protocol rule with the given name.
 | Find the open protocol rule with the given name.
 | Add new protocol rules. Fails, if a protocol rule with the same name
 exists.
 | Add a new protocol rules. Fails, if a protocol rule with the same name
 exists.
 | Add new protocol rules. Fails, if a protocol rule with the same name
 exists. Ignore _restrict construct.
 | Add a new protocol rules. Fails, if a protocol rule with the same name
 exists.
 | Add intruder proof rules.
 | Add intruder proof rules for all diff and non-diff caches.
 | Add intruder proof rules for both diff caches.
 | Add intruder proof rules for both caches.
 | Add intruder proof rules to left diff cache.
 | Add intruder proof rules to left cache.
 | Add intruder proof rules to right diff cache.
 | Add intruder proof rules to right cache.
 | Normalize the theory representation such that they remain semantically
 strictly) for semantic equality; e.g., when testing the parser.
 | Pretty print an open rule together with its assertion soundness proof.
 | Pretty print an open rule together with its assertion soundness proof.
$
 cannot show loop breakers here, as we do not have the information
$
 | Pretty print a diff rule
 | Pretty print an either rule
 | Pretty print an open theory.
 prettyIntrVariantsSection prettyOpenProtoRule prettyProof
 | Pretty print an open theory.
 prettyIntrVariantsSection prettyOpenProtoRule prettyProof
 | Pretty print a translated Open Theory
 | Pretty print a diff theory.
# LANGUAGE ViewPatterns #


module OpenTheory (
    module OpenTheory
    , module Theory.ProofSkeleton
    , module Rule
    , module Items.OpenTheoryItem
    ) where
import Control.Basics
import Control.Category
import Control.Monad.Reader
import Data.Either
import Data.List
import Data.Maybe
import qualified Data.Set as S
import Extension.Data.Label hiding (get)
import qualified Extension.Data.Label as L
import Items.OpenTheoryItem
import Theory.ProofSkeleton
import Rule
import Safe
import Term.Positions
import Theory.Model
import Theory.Proof
import TheoryObject
import Utils.Misc
import Prelude hiding (id, (.))

import Pretty
import Theory.Text.Pretty
import Control.Parallel.Strategies


  remove Sapic items and convert other items to identical item but with unit type for sapic elements
removeTranslationItems :: OpenTheory -> OpenTranslatedTheory
removeTranslationItems thy =
  Theory {_thyName=(L.get thyName thy)
          ,_thyHeuristic=(L.get thyHeuristic thy)
          ,_thyTactic=(L.get thyTactic thy)
          ,_thySignature=(L.get thySignature thy)
          ,_thyCache=(L.get thyCache thy)
          ,_thyItems = newThyItems
          ,_thyOptions =(L.get thyOptions thy)}
    where
      newThyItems = map removeTranslationElement (L.get thyItems thy)
      removeTranslationElement :: TheoryItem r p TranslationElement -> TheoryItem r p ()
      removeTranslationElement (TranslationItem _) = TranslationItem ()
      removeTranslationElement (RuleItem r) = RuleItem r
      removeTranslationElement (LemmaItem l) = LemmaItem l
      removeTranslationElement (RestrictionItem rl) = RestrictionItem rl
      removeTranslationElement (TextItem t) = TextItem t
      removeTranslationElement (PredicateItem predi) = PredicateItem predi

openTranslatedTheory :: OpenTranslatedTheory -> OpenTheory
openTranslatedTheory thy =
  Theory {_thyName=(L.get thyName thy)
          ,_thyHeuristic=(L.get thyHeuristic thy)
          ,_thyTactic=(L.get thyTactic thy)
          ,_thySignature=(L.get thySignature thy)
          ,_thyCache=(L.get thyCache thy)
          ,_thyItems = newThyItems
          ,_thyOptions =(L.get thyOptions thy)}
    where
      newThyItems = mapMaybe addTranslationElement (L.get thyItems thy)
      addTranslationElement :: TheoryItem r p () -> Maybe (TheoryItem r p s)
      addTranslationElement (RuleItem r) = Just $ RuleItem r
      addTranslationElement (LemmaItem l) = Just $ LemmaItem l
      addTranslationElement (RestrictionItem rl) = Just $ RestrictionItem rl
      addTranslationElement (TextItem t) = Just $ TextItem t
      addTranslationElement (PredicateItem predi) = Just $ PredicateItem predi
      addTranslationElement (TranslationItem _) = Nothing

addAutoSourcesLemmaDiff :: MaudeHandle
                        -> String
                        -> ClosedRuleCache
                        -> ClosedRuleCache
                        -> [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof IncrementalProof]
                        -> [DiffTheoryItem DiffProtoRule ClosedProtoRule IncrementalDiffProof IncrementalProof]
addAutoSourcesLemmaDiff hnd lemmaName crcLeft crcRight items =
    diffPart ++ lhsPart ++ rhsPart
  where
  We split items into three . DiffRules , DiffLemmas , and DiffTextItems are
    diffPart = mapMaybe f items
      where
        f (DiffRuleItem r)  = Just (DiffRuleItem r)
        f (DiffLemmaItem l) = Just (DiffLemmaItem l)
        f (DiffTextItem t)  = Just (DiffTextItem t)
        f _                 = Nothing

    lhsPart = if containsPartialDeconstructions crcLeft
        then mapMaybe (toSide LHS) $
                addAutoSourcesLemma hnd (lemmaName ++ "_LHS") crcLeft $
                  mapMaybe (filterItemSide LHS) items
        else mapMaybe (toSide LHS) $
                  mapMaybe (filterItemSide LHS) items
    rhsPart = if containsPartialDeconstructions crcRight
        then mapMaybe (toSide RHS) $
                addAutoSourcesLemma hnd (lemmaName ++ "_RHS") crcRight $
                  mapMaybe (filterItemSide RHS) items
        else mapMaybe (toSide RHS) $
                  mapMaybe (filterItemSide RHS) items

    filterItemSide s (EitherRuleItem (s', r))        | s == s' = Just (RuleItem r)
    filterItemSide s (EitherLemmaItem (s', l))       | s == s' = Just (LemmaItem l)
    filterItemSide s (EitherRestrictionItem (s', r)) | s == s' = Just (RestrictionItem r)
    filterItemSide _ _                                         = Nothing

    toSide s (RuleItem r)        = Just $ EitherRuleItem (s, r)
    toSide LHS (LemmaItem l)     = Just $ EitherLemmaItem (LHS, addLeftLemma  l)
    toSide RHS (LemmaItem l)     = Just $ EitherLemmaItem (RHS, addRightLemma l)
    toSide s (RestrictionItem r) = Just $ EitherRestrictionItem (s, r)
    toSide _ (TextItem t)        = Just $ DiffTextItem t
  FIXME : We currently ignore predicates and  stuff as they should not
    toSide _ (PredicateItem _)   = Nothing
    toSide _ (TranslationItem _)       = Nothing

addAutoSourcesLemma :: MaudeHandle
                    -> String
                    -> ClosedRuleCache
                    -> [TheoryItem ClosedProtoRule IncrementalProof s]
                    -> [TheoryItem ClosedProtoRule IncrementalProof s]
addAutoSourcesLemma hnd lemmaName (ClosedRuleCache _ raw _ _) items =
  case find lemma items of
    Nothing  -> items'++[LemmaItem l]
    (Just _) -> items'
  where
    runMaude   = (`runReader` hnd)

    lemma (LemmaItem (Lemma name _ _ _ _)) | name == lemmaName = True
    lemma _                                                    = False

    l = fmap skeletonToIncrementalProof $ unprovenLemma lemmaName [SourceLemma] AllTraces formula

    rules = mapMaybe itemToRule items

    allOutConcs :: [(ClosedProtoRule, LNTerm)]
    allOutConcs = do
        ru                                <- rules
        (_, protoOrOutFactView -> Just t) <- enumConcs $ L.get cprRuleAC ru
        unifyProtC                        <- concatMap allProtSubterms t
        return (ru, unifyProtC)

    allOutConcsNotProt :: [(ClosedProtoRule, LNFact)]
    allOutConcsNotProt = do
        ru              <- rules
        (_, unifyFactC) <- enumConcs $ L.get cprRuleAC ru
        guard (getFactTag unifyFactC /= OutFact)
        return (ru, unifyFactC)

  We use the raw sources here to generate one lemma to rule them all ...
    (items', formula, _) = foldl computeFormula (items, ltrue, []) chains

    chains = concatMap (multiply unsolvedChains . duplicate) $
                   concatMap (map snd . getDisj . L.get cdCases) raw

    computeFormula :: ([TheoryItem ClosedProtoRule IncrementalProof s], LNFormula, [(RuleInfo ProtoRuleName IntrRuleACInfo, ExtendedPosition)])
                   -> ((NodeConc, NodePrem), System)
                   -> ([TheoryItem ClosedProtoRule IncrementalProof s], LNFormula, [(RuleInfo ProtoRuleName IntrRuleACInfo, ExtendedPosition)])
    computeFormula (its, form, done) ((conc,_), source) = (its', form', done')
      where
        its'  = addLabels inputsAndOutputs its
        form' = addFormula inputsAndOutputs form
        done' = addCases inputsAndOutputs done

        v     = head $ getFactTerms $ nodeConcFact conc source

        inputRules :: [(ClosedProtoRule, Either LNTerm LNFact, ExtendedPosition)]
        inputRules = concat $ mapMaybe g $ allPrems source
          where
            g (nodeid, pid, tidx, term) = do
              position <- findPos v term
              ruleSys  <- nodeRuleSafe nodeid source
              rule     <- find ((ruleName ruleSys ==).ruleName) rules
              premise  <- lookupPrem pid $ L.get cprRuleAC rule
              t'       <- protoOrInFactView premise
              t        <- atMay t' tidx
              return (terms position rule t ++ facts position rule t premise)
                where
                  terms position rule t = do
                    pos     <- position
                    return (rule, Left t, (pid, tidx, pos))
                  facts position rule t premise = do
                    guard $ isProtoFact premise && (isPair t || isAC t || isMsgVar t)
                        && ((nodeid, pid) `elem` map fst (unsolvedPremises source))
                    pos     <- position
                    return (rule, Right premise, (pid, tidx, pos))

        premiseTermU :: [(ClosedProtoRule, Either (LNTerm, LNTerm) LNFact, ExtendedPosition)]
        premiseTermU = mapMaybe f inputRules
          where
  cases for protected subterms : we consider the deepest protected subterm
            f (x, Left y, (pidx, tidx, z)) = do
              v'        <- y `atPosMay` z
              protTerm' <- deepestProtSubterm y z
  protected subterm is the variable in question , as this
  1 . often leads to false lemmas as we do not unify with all
  2 . blows up the lemma as a variable unifies with all outputs
  3 . typically only happens if a value is stored in a state fact ,
              protTerm  <- if protTerm' == v'
                then Nothing
                else Just protTerm'
              return (x, Left (protTerm, v'), (pidx, tidx, z))
            f (x, Right fact, (pidx, tidx, z)) =
              return (x, Right fact, (pidx, tidx, z))

        inputsAndOutputs :: [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
        inputsAndOutputs = do
            (rin, unify, pos) <- filterFacts premiseTermU
            let matches = matchingConclusions rin unify
            return (rin, matches, pos)
          where
            filterFacts cases = mapMaybe f cases
              where
                f c@(r, Left  _, p) = do
                  guard $ notElem (ruleName r, p) done
                  return c
                f c@(r, Right _, p) = do
                  guard $ notElem (ruleName r, p) done
                         && null subtermCasePositions
                  return c
                subtermCasePositions = filter (isLeft . snd3) cases

            matchingConclusions rin (Left (unify, vin)) = Left (unify, vin, do
              (rout, tout) <- allOutConcs
              let fout = tout `renameAvoiding` unify
              guard ((ruleName . L.get cprRuleE) rin /= (ruleName . L.get cprRuleE) rout)
              guard (runMaude $ unifiableLNTerms unify fout)
              return (rout, tout))
            matchingConclusions rin (Right unify) = Right (unify, do
              (rout, fout) <- allOutConcsNotProt
              guard ((ruleName . L.get cprRuleE) rin /= (ruleName . L.get cprRuleE) rout)
              guard (factTagName (getFactTag unify) == factTagName (getFactTag fout))
              let unifout = fout `renameAvoiding` unify
              guard (runMaude $ unifiableLNFacts unify unifout)
              return (rout, fout))

        inputFactTerm pos ru terms var = Fact {factTag = ProtoFact Linear
              ("AUTO_IN_TERM_" ++ printPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (1 + length terms),
              factAnnotations = S.empty, factTerms = terms ++[var]}
        inputFactFact pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_IN_FACT_" ++ printFactPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}
        outputFactTerm pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_OUT_TERM_" ++ printPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}
        outputFactFact pos ru terms = Fact {factTag = ProtoFact Linear
              ("AUTO_OUT_FACT_" ++ printFactPosition pos ++ "_" ++ getRuleName (L.get cprRuleAC ru)) (length terms),
              factAnnotations = S.empty, factTerms = terms}

        addLabels :: [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
                  -> [TheoryItem ClosedProtoRule IncrementalProof s]
                  -> [TheoryItem ClosedProtoRule IncrementalProof s]
        addLabels matches = map update
          where
            update (RuleItem ru) = RuleItem $ foldr up ru $
                   filter ((ruleName ru ==). ruleName . fst3) acts
              where
                up (r, p, Left  (Left  (t, v'))) r' = addActionClosedProtoRule r' (inputFactTerm  p r [t] v')
                up (r, p, Left  (Right f))       r' = addActionClosedProtoRule r' (inputFactFact  p r (getFactTerms f))
                up (_, p, Right (r, Left  t))    r' = addActionClosedProtoRule r' (outputFactTerm p r [t])
                up (_, p, Right (r, Right f))    r' = addActionClosedProtoRule r' (outputFactFact p r (getFactTerms f))
            update item          = item

            acts = concatMap prepare matches
            prepare (r, Left  (t, v', tl), p) = (r, p, Left (Left  (t, v'))) : map (\(r', t') -> (r', p, Right (r, Left  t'))) tl
            prepare (r, Right (f, fl)    , p) = (r, p, Left (Right f))       : map (\(r', f') -> (r', p, Right (r, Right f'))) fl

        listOfM :: Int -> [String]
        listOfM n = zipWith (++) (replicate n "m") $ fmap show [1..n]

        addFormula ::
             [(ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)]
          -> LNFormula
          -> LNFormula
        addFormula matches f = foldr addForm f matches
          where
            addForm ::
                 (ClosedProtoRule, Either (LNTerm, LNTerm, [(ClosedProtoRule, LNTerm)]) (LNFact, [(ClosedProtoRule, LNFact)]), ExtendedPosition)
              -> LNFormula
              -> LNFormula
            addForm (ru, Left (_, _, []), p) f' = f' .&&. Qua All ("x", LSortMsg)
              (Qua All ("m", LSortMsg) (Qua All ("i", LSortNode)
              (Conn Imp (Ato (Action (varTerm (Bound 0))
              (inputFactTerm p ru [varTerm (Bound 1)] (varTerm (Bound 2)))))
              orKU)))
            addForm (ru, Left _, p) f' = f' .&&. Qua All ("x", LSortMsg)
              (Qua All ("m", LSortMsg) (Qua All ("i", LSortNode)
              (Conn Imp (Ato (Action (varTerm (Bound 0))
              (inputFactTerm p ru [varTerm (Bound 1)] (varTerm (Bound 2)))))
              (toFactsTerm ru p orKU))))
            addForm (ru, Right (m, []),     p) f' = f' .&&. formulaMultArity (factArity m)
              where formulaMultArity nb = foldr (\h -> Qua All (h,LSortMsg))
                           (Qua All ("i", LSortNode)
                           (Conn Imp (Ato (Action (varTerm (Bound 0))
                           (inputFactFact p ru (listVarTerm (toInteger $ factArity m) 1))))
                           lfalse)) (listOfM nb)
            addForm (ru, Right (m, outs:_), p) f' = f' .&&. formulaMultArity (factArity m)
              where formulaMultArity nb = foldr (\h -> Qua All (h,LSortMsg))
                           (Qua All ("i", LSortNode)
                           (Conn Imp (Ato (Action (varTerm (Bound 0))
                           (inputFactFact p ru (listVarTerm (toInteger $ factArity m) 1))))
                           (toFactsFact ru p (snd outs)))) (listOfM nb)
            orKU = Qua Ex ("j",LSortNode)
                   (Conn And (Ato (Action (varTerm (Bound 0))
                    Fact {factTag = KUFact, factAnnotations = S.empty,
                          factTerms = [varTerm (Bound 3)]} ))
                   (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1)))))
            toFactsTerm ru p f'' =
              Conn Or f''
              (Qua Ex ("j",LSortNode)
              (Conn And (Ato (Action (varTerm (Bound 0))
              (outputFactTerm p ru [varTerm (Bound 2)]) ))
              (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1))))))
            toFactsFact ru p outn =
              Qua Ex ("j",LSortNode)
              (Conn And (Ato (Action (varTerm (Bound 0))
              (outputFactFact p ru (listVarTerm (toInteger $ 1 + factArity outn) 2)) ))
              (Ato (Less (varTerm (Bound 0)) (varTerm (Bound 1)))))
            listVarTerm q s | q == s    = [varTerm (Bound q)]
            listVarTerm q s | otherwise = varTerm (Bound q) : listVarTerm (q-1) s

        addCases matches d = d ++ map (\(r, _, p) -> (ruleName r, p)) matches


defaultOption :: Option
defaultOption = Option False False False False False False False S.empty [] 10 5



defaultOpenTheory :: Bool -> OpenTheory
defaultOpenTheory flag = Theory "default" [] [] (emptySignaturePure flag) [] [] defaultOption

defaultOpenDiffTheory :: Bool -> OpenDiffTheory
defaultOpenDiffTheory flag = DiffTheory "default" [] [] (emptySignaturePure flag) [] [] [] [] [] defaultOption

addDefaultDiffLemma:: OpenDiffTheory -> OpenDiffTheory
addDefaultDiffLemma thy = fromMaybe thy $ addDiffLemma (unprovenDiffLemma "Observational_equivalence" []) thy

addProtoRuleLabel :: OpenProtoRule -> OpenProtoRule
addProtoRuleLabel rule = addProtoDiffLabel rule ("DiffProto" ++ (getOpenProtoRuleName rule))

getLeftProtoRule :: DiffProtoRule -> OpenProtoRule
getLeftProtoRule (DiffProtoRule ruE Nothing)       = OpenProtoRule (getLeftRule ruE) []
getLeftProtoRule (DiffProtoRule _   (Just (l, _))) = l

  Get the  openProtoRules
getRightProtoRule :: DiffProtoRule -> OpenProtoRule
getRightProtoRule (DiffProtoRule ruE Nothing)       = OpenProtoRule (getRightRule ruE) []
getRightProtoRule (DiffProtoRule _   (Just (_, r))) = r

addIntrRuleLabels:: OpenDiffTheory -> OpenDiffTheory
addIntrRuleLabels thy =
    modify diffThyCacheLeft (map addRuleLabel) $ modify diffThyDiffCacheLeft (map addRuleLabel) $ modify diffThyDiffCacheRight (map addRuleLabel) $ modify diffThyCacheRight (map addRuleLabel) thy
  where
    addRuleLabel :: IntrRuleAC -> IntrRuleAC
    addRuleLabel rule = addDiffLabel rule ("DiffIntr" ++ (getRuleName rule))

containsManualRuleVariants :: [TheoryItem OpenProtoRule p s] -> Bool
containsManualRuleVariants = foldl f False
  where
    f hasVariants (RuleItem (OpenProtoRule _ [])) = hasVariants
    f _           (RuleItem (OpenProtoRule _ _ )) = True
    f hasVariants _                               = hasVariants

mergeOpenProtoRules :: [TheoryItem OpenProtoRule p s] -> [TheoryItem OpenProtoRule p s]
mergeOpenProtoRules = concatMap (foldr mergeRules []) . groupBy comp
  where
    comp (RuleItem (OpenProtoRule ruE _)) (RuleItem (OpenProtoRule ruE' _)) = ruE == ruE'
    comp (RuleItem _) _ = False
    comp _ (RuleItem _) = False
    comp _ _            = True

    mergeRules (RuleItem r)                          []                                              = [RuleItem r]
    mergeRules (RuleItem (OpenProtoRule ruE' ruAC')) [RuleItem (OpenProtoRule ruE ruAC)] | ruE==ruE' = [RuleItem (OpenProtoRule ruE (ruAC'++ruAC))]
    mergeRules (RuleItem _)                          _                                               = error "Error in mergeOpenProtoRules. Please report bug."
    mergeRules item                                  l                                               = item:l

containsManualRuleVariantsDiff :: [DiffTheoryItem DiffProtoRule r p p2] -> Bool
containsManualRuleVariantsDiff = foldl f False
  where
    f hasVariants (DiffRuleItem (DiffProtoRule _ Nothing )) = hasVariants
    f _           (DiffRuleItem (DiffProtoRule _ (Just _))) = True
    f hasVariants _                                         = hasVariants

mergeOpenProtoRulesDiff :: [DiffTheoryItem r OpenProtoRule p p2] -> [DiffTheoryItem r OpenProtoRule p p2]
mergeOpenProtoRulesDiff = concatMap (foldr mergeRules []) . groupBy comp
  where
    comp (EitherRuleItem (s, OpenProtoRule ruE _)) (EitherRuleItem (s', OpenProtoRule ruE' _)) = ruE==ruE' && s==s'
    comp (EitherRuleItem _) _ = False
    comp _ (EitherRuleItem _) = False
    comp _ _                  = True

    mergeRules (EitherRuleItem r)                             [] = [EitherRuleItem r]
    mergeRules (EitherRuleItem (s, OpenProtoRule ruE' ruAC')) [EitherRuleItem (s', OpenProtoRule ruE ruAC)]
                                            | ruE==ruE' && s==s' = [EitherRuleItem (s, OpenProtoRule ruE (ruAC'++ruAC))]
    mergeRules (EitherRuleItem _)                             _  = error "Error in mergeOpenProtoRulesDiff. Please report bug."
    mergeRules item                                           l  = item:l

mergeLeftRightRulesDiff :: (Show p, Show p2) => [DiffTheoryItem DiffProtoRule OpenProtoRule p p2] -> [DiffTheoryItem DiffProtoRule OpenProtoRule p p2]
mergeLeftRightRulesDiff rs = map clean $ concatMap (foldr mergeRules []) $ groupBy comp' $ sortBy comp rs
  where
    comp (EitherRuleItem (_, OpenProtoRule ruE _)) (EitherRuleItem (_, OpenProtoRule ruE' _)) = compare (ruleName ruE) (ruleName ruE')
    comp (EitherRuleItem (_, OpenProtoRule ruE _)) (DiffRuleItem (DiffProtoRule ruE' _))      = compare (ruleName ruE) (ruleName ruE')
    comp (DiffRuleItem (DiffProtoRule ruE _))      (EitherRuleItem (_, OpenProtoRule ruE' _)) = compare (ruleName ruE) (ruleName ruE')
    comp (DiffRuleItem (DiffProtoRule ruE _))      (DiffRuleItem (DiffProtoRule ruE' _))      = compare (ruleName ruE) (ruleName ruE')
    comp (EitherRuleItem _) _ = LT
    comp _ (EitherRuleItem _) = GT
    comp (DiffRuleItem _) _   = LT
    comp _ (DiffRuleItem _)   = GT
    comp _ _                  = EQ

    comp' a b = comp a b == EQ

    mergeRules (EitherRuleItem r)                                 [] = [EitherRuleItem r]
    mergeRules (DiffRuleItem r)                                   [] = [DiffRuleItem r]
    mergeRules (EitherRuleItem (s, ru@(OpenProtoRule ruE _)))     [EitherRuleItem (s', ru'@(OpenProtoRule ruE' _))]
                                            | ruleName ruE==ruleName ruE' && s==LHS && s'==RHS = [DiffRuleItem (DiffProtoRule ruE (Just (ru, ru')))]
    mergeRules (EitherRuleItem (s, ru@(OpenProtoRule ruE _)))     [EitherRuleItem (s', ru'@(OpenProtoRule ruE' _))]
                                            | ruleName ruE==ruleName ruE' && s==RHS && s'==LHS = [DiffRuleItem (DiffProtoRule ruE (Just (ru', ru)))]
    mergeRules (EitherRuleItem (_, ru@(OpenProtoRule ruE _)))     [DiffRuleItem (DiffProtoRule dru Nothing)]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru Nothing))         [EitherRuleItem (_, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru)))]
    mergeRules (EitherRuleItem (LHS, ru@(OpenProtoRule ruE _)))   [DiffRuleItem (DiffProtoRule dru (Just (_, ru')))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru')))]
    mergeRules (EitherRuleItem (RHS, ru@(OpenProtoRule ruE _)))   [DiffRuleItem (DiffProtoRule dru (Just (ru', _)))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru', ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (_, ru')))) [EitherRuleItem (LHS, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru, ru')))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (ru', _)))) [EitherRuleItem (RHS, ru@(OpenProtoRule ruE _))]
                                            | ruleName ruE==ruleName dru = [DiffRuleItem (DiffProtoRule dru (Just (ru', ru)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))) [DiffRuleItem (DiffProtoRule dru' Nothing)]
                                            | ruleName dru==ruleName dru' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru Nothing))         [DiffRuleItem (DiffProtoRule dru' (Just (lr, rr)))]
                                            | ruleName dru==ruleName dru' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))) [DiffRuleItem (DiffProtoRule dru' (Just (lr', rr')))]
                                            | ruleName dru==ruleName dru' && equalOpenRuleUpToDiffAnnotation lr lr' && equalOpenRuleUpToDiffAnnotation rr rr' = [DiffRuleItem (DiffProtoRule dru (Just (lr, rr)))]
    mergeRules (EitherRuleItem _)                                 _  = error "Error in mergeLeftRightRulesDiff. Please report bug."
    mergeRules (DiffRuleItem _)                                   _  = error "Error in mergeLeftRightRulesDiff. Please report bug."
    mergeRules item                                               l  = item:l

    clean (DiffRuleItem (DiffProtoRule ruE (Just (OpenProtoRule ruEL [], OpenProtoRule ruER []))))
       | getLeftRule ruE `equalRuleUpToDiffAnnotation` ruEL
        && getRightRule ruE `equalRuleUpToDiffAnnotation` ruER = DiffRuleItem (DiffProtoRule ruE Nothing)
    clean i                                                    = i


lookupOpenProtoRule :: ProtoRuleName -> OpenTheory -> Maybe OpenProtoRule
lookupOpenProtoRule name =
    find ((name ==) . L.get (preName . rInfo . oprRuleE)) . theoryRules

lookupOpenDiffProtoDiffRule :: ProtoRuleName -> OpenDiffTheory -> Maybe DiffProtoRule
lookupOpenDiffProtoDiffRule name =
    find ((name ==) . L.get (preName . rInfo . dprRule)) . diffTheoryDiffRules

addOpenProtoRule :: OpenProtoRule -> OpenTheory -> Maybe OpenTheory
addOpenProtoRule ru@(OpenProtoRule ruE ruAC) thy = do
    guard nameNotUsedForDifferentRule
    guard allRuleNamesAreDifferent
    return $ modify thyItems (++ [RuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenProtoRule (L.get (preName . rInfo . oprRuleE) ru) thy
    allRuleNamesAreDifferent = (S.size (S.fromList (ruleName ruE:map ruleName ruAC)))
        == ((length ruAC) + 1)

addOpenProtoDiffRule :: DiffProtoRule -> OpenDiffTheory -> Maybe OpenDiffTheory
addOpenProtoDiffRule ru@(DiffProtoRule _ Nothing)  thy = do
    guard nameNotUsedForDifferentRule
    return $ modify diffThyItems (++ [DiffRuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo . dprRule) ru) thy
addOpenProtoDiffRule ru@(DiffProtoRule _ (Just (lr, rr))) thy = do
    guard nameNotUsedForDifferentRule
    guard $ allRuleNamesAreDifferent lr
    guard $ allRuleNamesAreDifferent rr
    guard leftAndRightHaveSameName
    return $ modify diffThyItems (++ [DiffRuleItem ru]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ru ==) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo . dprRule) ru) thy
    allRuleNamesAreDifferent (OpenProtoRule ruE ruAC) = (S.size (S.fromList (ruleName ruE:map ruleName ruAC)))
        == ((length ruAC) + 1)
    leftAndRightHaveSameName = ruleName ru == ruleName lr && ruleName lr == ruleName rr

addProtoRule :: ProtoRuleE -> OpenTheory -> Maybe OpenTheory
addProtoRule ruE thy = do
    guard nameNotUsedForDifferentRule
    return $ modify thyItems (++ [RuleItem (OpenProtoRule ruE [])]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ruE ==) $ fmap (L.get oprRuleE) $ lookupOpenProtoRule (L.get (preName . rInfo) ruE) thy

addProtoDiffRule :: ProtoRuleE -> OpenDiffTheory -> Maybe OpenDiffTheory
addProtoDiffRule ruE thy = do
    guard nameNotUsedForDifferentRule
    return $ modify diffThyItems (++ [DiffRuleItem (DiffProtoRule ruE Nothing)]) thy
  where
    nameNotUsedForDifferentRule =
        maybe True (ruE ==) $ fmap (L.get dprRule) $ lookupOpenDiffProtoDiffRule (L.get (preName . rInfo) ruE) thy

  | Add intruder proof rules after Translate .
addIntrRuleACsAfterTranslate :: [IntrRuleAC] -> OpenTranslatedTheory -> OpenTranslatedTheory
addIntrRuleACsAfterTranslate rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')

addIntrRuleACs :: [IntrRuleAC] -> OpenTheory -> OpenTheory
addIntrRuleACs rs' = modify (thyCache) (\rs -> nub $ rs ++ rs')

addIntrRuleACsDiffAll :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffAll rs' thy = addIntrRuleACsDiffBoth rs' (addIntrRuleACsDiffBothDiff rs' thy)

addIntrRuleACsDiffBothDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffBothDiff rs' thy = addIntrRuleACsDiffRightDiff rs' (addIntrRuleACsDiffLeftDiff rs' thy)

addIntrRuleACsDiffBoth :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffBoth rs' thy = addIntrRuleACsDiffRight rs' (addIntrRuleACsDiffLeft rs' thy)

addIntrRuleACsDiffLeftDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffLeftDiff rs' thy = modify (diffThyDiffCacheLeft) (\rs -> nub $ rs ++ rs') thy

addIntrRuleACsDiffLeft :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffLeft rs' thy = modify (diffThyCacheLeft) (\rs -> nub $ rs ++ rs') thy

addIntrRuleACsDiffRightDiff :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffRightDiff rs' thy = modify (diffThyDiffCacheRight) (\rs -> nub $ rs ++ rs') thy

addIntrRuleACsDiffRight :: [IntrRuleAC] -> OpenDiffTheory -> OpenDiffTheory
addIntrRuleACsDiffRight rs' thy = modify (diffThyCacheRight) (\rs -> nub $ rs ++ rs') thy

  equivalent . Use this function when you want to compare two theories ( quite
normalizeTheory :: OpenTheory -> OpenTheory
normalizeTheory =
    L.modify thyCache sort
  . L.modify thyItems (\items -> do
      item <- items
      return $ case item of
          LemmaItem lem ->
              LemmaItem $ L.modify lProof stripProofAnnotations $ lem
          RuleItem _    -> item
          TextItem _    -> item
          RestrictionItem _   -> item
          TranslationItem _   -> item
          PredicateItem _   -> item
          )
  where
    stripProofAnnotations :: ProofSkeleton -> ProofSkeleton
    stripProofAnnotations = fmap stripProofStepAnnotations
    stripProofStepAnnotations (ProofStep method ()) =
        ProofStep (case method of
                     Sorry _         -> Sorry Nothing
                     Contradiction _ -> Contradiction Nothing
                     _               -> method)
                  ()








prettyOpenProtoRule :: HighlightDocument d => OpenProtoRule -> d
prettyOpenProtoRule (OpenProtoRule ruE [])       = prettyProtoRuleE ruE
prettyOpenProtoRule (OpenProtoRule _   [ruAC])   = prettyProtoRuleACasE ruAC
prettyOpenProtoRule (OpenProtoRule ruE variants) = prettyProtoRuleE ruE $-$
    nest 1 (kwVariants $-$ nest 1 (ppList prettyProtoRuleAC variants))
  where
    ppList _  []     = emptyDoc
    ppList pp [x]    = pp x
    ppList pp (x:xr) = pp x $-$ comma $-$ ppList pp xr

prettyOpenProtoRuleAsClosedRule :: HighlightDocument d => OpenProtoRule -> d
prettyOpenProtoRuleAsClosedRule (OpenProtoRule ruE [])
    (nest 2 $ emptyDoc $-$
     multiComment_ ["has exactly the trivial AC variant"])
prettyOpenProtoRuleAsClosedRule (OpenProtoRule _ [ruAC@(Rule (ProtoRuleACInfo _ _ (Disj disj) _) _ _ _ _)])
    (nest 2 $ prettyLoopBreakers (L.get rInfo ruAC) $-$
     if length disj == 1 then
       multiComment_ ["has exactly the trivial AC variant"]
     else
       multiComment $ prettyProtoRuleAC ruAC
    )
prettyOpenProtoRuleAsClosedRule (OpenProtoRule ruE variants) = prettyProtoRuleE ruE $-$
    nest 1 (kwVariants $-$ nest 1 (ppList prettyProtoRuleAC variants))
  where
    ppList _  []     = emptyDoc
    ppList pp [x]    = pp x
    ppList pp (x:xr) = pp x $-$ comma $-$ ppList pp xr

prettyDiffRule :: HighlightDocument d => DiffProtoRule -> d
prettyDiffRule (DiffProtoRule ruE Nothing           ) = prettyProtoRuleE ruE
prettyDiffRule (DiffProtoRule ruE (Just (ruL,  ruR))) = prettyProtoRuleE ruE $-$
    nest 1
    (kwLeft  $-$ nest 1 (prettyOpenProtoRule ruL) $-$
     kwRight $-$ nest 1 (prettyOpenProtoRule ruR))

prettyEitherRule :: HighlightDocument d => (Side, OpenProtoRule) -> d
prettyEitherRule (_, p) = prettyProtoRuleE $ L.get oprRuleE p




prettyOpenTheory :: HighlightDocument d => OpenTheory -> d
prettyOpenTheory thy =
    prettyTheory (prettySignaturePureExcept funsyms)
                 (const emptyDoc) prettyOpenProtoRule prettyProof prettyTranslationElement thy
                 where
                    funsyms = S.fromList $ map fst' $ theoryFunctionTypingInfos thy
  function symbols that are printed by sapic printer already
                    fst' (a,_,_) = a

prettyOpenDiffTheory :: HighlightDocument d => OpenDiffTheory -> d
prettyOpenDiffTheory =
    prettyDiffTheory prettySignaturePure
                 (const emptyDoc) prettyEitherRule prettyDiffProof prettyProof

prettyOpenTranslatedTheory :: HighlightDocument d => OpenTranslatedTheory -> d
prettyOpenTranslatedTheory =
    prettyTheory prettySignaturePure
                 (const emptyDoc) prettyOpenProtoRule prettyProof emptyString


prettyDiffTheory :: HighlightDocument d
                 => (sig -> d) -> (c -> d) -> ((Side, r2) -> d) -> (p -> d) -> (p2 -> d)
                 -> DiffTheory sig c DiffProtoRule r2 p p2 -> d
prettyDiffTheory ppSig ppCache ppRule ppDiffPrf ppPrf thy = vsep $
    [ kwTheoryHeader $ text $ L.get diffThyName thy
    , lineComment_ "Function signature and definition of the equational theory E"
    , ppSig $ L.get diffThySignature thy
    , if thyT == [] then text "" else vcat $ map prettyTactic thyT
    , if thyH == [] then text "" else text "heuristic: " <> text (prettyGoalRankings thyH)
    , ppCache $ L.get diffThyCacheLeft thy
    , ppCache $ L.get diffThyCacheRight thy
    , ppCache $ L.get diffThyDiffCacheLeft thy
    , ppCache $ L.get diffThyDiffCacheRight thy
    ] ++
    parMap rdeepseq ppItem (L.get diffThyItems thy) ++
    [ kwEnd ]
  where
    ppItem = foldDiffTheoryItem
        prettyDiffRule ppRule (prettyDiffLemma ppDiffPrf) (prettyEitherLemma ppPrf) prettyEitherRestriction (uncurry prettyFormalComment)
    thyH = L.get diffThyHeuristic thy
    thyT = L.get diffThyTactic thy

