{-# LANGUAGE ViewPatterns, DeriveDataTypeable, TupleSections, TypeOperators, TemplateHaskell, TypeSynonymInstances, FlexibleInstances, FlexibleContexts, GeneralizedNewtypeDeriving #-}
-- |
-- Copyright   : (c) 2010-2012 Benedikt Schmidt & Simon Meier
-- License     : GPL v3 (see LICENSE)
--
-- Maintainer  : Simon Meier <iridcode@gmail.com>
-- Portability : GHC only
--
-- Proof states and their transformations; i.e., logical deduction.
module Theory.Proof.Sequent (
  -- * Sequent construction
    sequentFromFormula

  -- * Prove methods

  -- ** SeProof monad
  , SeProof
  , execSeProof
  , runSeProof
  , getMaudeHandle

  -- ** Goals
  , openGoals
  , solveGoal

  -- ** Equalitiy solving
  , solveSubstEqs

  -- ** Conjunction with other sequents
  , conjoinSequent

  -- ** Simplification
  , simplifySequent

  -- * Contradiction
  , proveCyclic
  , hasNonNormalTerms
  , hasForbiddenExp
  , formulasFalse
  , nonUniqueFactInstances
  , contradictorySequent

  -- * Convenience export of used modules
  , module Theory.Proof.Types
  , module Theory.Proof.EquationStore
  ) where

import           Debug.Trace

import           Prelude hiding ( (.), id )

import           Data.List
import           Data.Either
import qualified Data.DAG.Simple  as D (cyclic, reachableSet)
import qualified Data.Set         as S
import qualified Data.Map         as M
import           Data.Monoid (Monoid, mappend )

import           Control.Basics
import           Control.Category
import           Control.Monad.Disj
import           Control.Monad.Reader
import           Control.Monad.Bind
import           Control.Monad.State (StateT, runStateT, execStateT, gets, put)

import           Text.Isar

import           Extension.Prelude
import           Extension.Data.Label

import           Logic.Connectives

import           Theory.Rule
import           Theory.Proof.SolveGuarded
import           Theory.Proof.Types
import           Theory.Proof.EquationStore

------------------------------------------------------------------------------
-- Sequents
------------------------------------------------------------------------------

-- Construction
---------------

-- | Returns the sequent that has to be proven to show that
--   given formula holds in the context of the given theory.
sequentFromFormula :: CaseDistKind -> LNFormula -> Sequent
sequentFromFormula kind f = 
    set sFormulas (S.singleton gf) (emptySequent kind)
  where 
    gf = either error id (fromFormulaNegate f)


------------------------------------------------------------------------------
-- Graph reasoning
------------------------------------------------------------------------------

-- | True iff there are terms in the sequent that are not in normal form wrt.
-- to 'Term.Rewriting.Norm.norm' (DH/AC).
--
-- FIXME: Might also want to check clauses, equation store, and other
-- components of sequent.
hasNonNormalTerms :: SignatureWithMaude -> Sequent -> Bool
hasNonNormalTerms sig se =
    any (not . (`runReader` (get sigmMaudeHandle sig)) . nfRule) . M.elems . get sNodes $ se

-- | True if there is no @EXP-down@ rule that should be replaced by an
-- @EXP-up@ rule.
hasForbiddenExp :: Sequent -> Bool
hasForbiddenExp se =
    any (isForbiddenExp) $ M.elems $ get sNodes se

-- | @isForbiddenExp ru@ returns @True@ if @ru@ is not allowed in
-- a normal dependency graph.
-- > isForbiddenExp (Rule () [undefined, Fact KUFact [undefined, Mult (Inv x1) x2]]
--                           [Fact KDFact [expTagToTerm IsExp, Exp p1 (Mult x2 x3)]] [])
-- > False
-- > isForbiddenExp (Rule () [undefined, Fact KUFact [undefined, Mult (Inv x1) x2]]
--                           [Fact KDFact [expTagToTerm IsExp, Exp p1 x2]] [])
-- > True
isForbiddenExp :: Rule a -> Bool
isForbiddenExp ru = maybe False id $ do
    [_,p2] <- return $ get rPrems ru
    [conc] <- return $ get rConcs ru
    (UpK, _,          b)       <- kFactView p2
    (DnK, Just IsExp, FApp (NonAC ("exp",2)) [g,c]) <- kFactView conc

    -- g should be public and the required inputs for c already required by b
    guard (sortOfTerm g == LSortPub && (input c \\ input b == []))
    return True
  where
    sortOfTerm (Lit (Var lv)) = lvarSort lv
    sortOfTerm (Lit (Con n))  = sortOfName n
    sortOfTerm _              = LSortMsg


-- | Compute all contradictions to unique fact instances.
--
-- Constraint systems are contradictory, where 'f' is a fact symbol
-- with unique instances and temporal variables i, j, and k are ordered
-- according to i < j < k, j requires a premise f(t), and i provides a
-- conclusion f(t) for the node k. Graphically, the edge from i to k is
-- interrupted by the node j that requires the same fact carried on the edge.
nonUniqueFactInstances :: SignatureWithMaude -> Sequent 
                       -> [(NodeId, NodeId, NodeId)]
nonUniqueFactInstances sig se = do
    Edge c@(NodeConc (i, _)) (NodePrem (k, _)) <- S.toList $ get sEdges se
    let tag = factTag (nodeConcFact c se)
    guard (tag `S.member` get sigmUniqueInsts sig)
    j <- S.toList $ D.reachableSet [i] less

    let isCounterExample = (j /= i) && (j /= k) && 
                           maybe False checkRule (M.lookup j $ get sNodes se)

        checkRule jRu    = any ((tag ==) . factTag) (get rPrems jRu) &&
                           k `S.member` D.reachableSet [j] less

    guard isCounterExample
    return (i, j, k) -- counter-example to unique fact instances
  where
    less = sRawLessRel se



-- Under-approximating minimal deducability
-------------------------------------------

-- | @proveCyclic se@ under-approximates @|se| ==> Ex v. v >+> v@.
proveCyclic :: Sequent -> Bool
proveCyclic = D.cyclic . sRawLessRel

-- | @formulasFalse se@ returns @True@ if False is included in the formulas of @se@
formulasFalse :: Sequent -> Bool
formulasFalse = S.member gfalse . get sFormulas

-- | @contradictorySequent se@ holds if the sequent is trivially contradictory.
--   FIXME: duplication with contradictions in Proof
contradictorySequent :: SignatureWithMaude -> Sequent -> Bool
contradictorySequent sig se =
    formulasFalse se                              ||
    eqsIsFalse (get sEqStore se)                  ||
    proveCyclic se                                ||
    hasNonNormalTerms sig se                      ||
    hasForbiddenExp se                            ||
    not (null (nonUniqueFactInstances sig se))


-- SeProof monad
----------------

-- | A proof with respect to a sequent. The fresh variables are existential
-- variables of the sequent and the multiple results are to be interpreted as a
-- disjunction while the inner-most maybe indicates if the proof method is
-- applicable/was successful or not.
type SeProof = StateT Sequent (FreshT (DisjT (Reader ProofContext)))

-- | Run a proof step.
runSeProof :: SeProof a -> ProofContext -> Sequent -> FreshState 
           -> Disj ((a, Sequent), FreshState)
runSeProof m ctxt se fs = 
    Disj $ (`runReader` ctxt) $ runDisjT $ (`runFreshT` fs) $ runStateT m se

-- | Run a proof step, returning only the updated states.
execSeProof :: SeProof a -> ProofContext -> Sequent -> FreshState 
            -> [(Sequent, FreshState)]
execSeProof m ctxt se fs = 
    (`runReader` ctxt) . runDisjT . (`runFreshT` fs) $ execStateT m se

-- | Retrieve the 'MaudeHandle' from the 'ProofContext'.
getMaudeHandle :: SeProof MaudeHandle
getMaudeHandle = get sigmMaudeHandle <$> askM pcSignature

-- | Import a rule with fresh variables.
importRule :: MonadFresh m
           => RuleAC
           -> m (RuleACInst, Maybe RuleACConstrs)
importRule ru = someRuleACInst ru `evalBindT` noBindings

-- | @proveLinearConc se (v,i)@ tries to prove that the @i@-th conclusion of node
-- @v@ is a linear fact.
proveLinearConc :: Sequent -> NodeConc -> Bool
proveLinearConc se (NodeConc (v,i)) =
    maybe False (isLinearFact . (get (rConc i))) $ M.lookup v $ get sNodes se

-- | Create a node labelled with a fresh instance of one of the rules and solve
-- it's fresh conditions immediatly.
--
-- PRE: Node must not yet be labelled with a rule.
ruleNode :: NodeId -> [RuleAC] -> SeProof RuleACInst
ruleNode i rules = do
    (ru, mrconstrs) <- importRule =<< disjunctionOfList rules
    solveRuleConstraints mrconstrs i
    modM sNodes (M.insert i ru)
    let inFacts = do
          (v, Fact InFact [m]) <- zip [0..] $ get rPrems ru
          return $ do
            j <- freshLVar "vf" LSortNode
            ruKnows <- mkISendRuleAC m
            modM sNodes (M.insert j ruKnows)
            modM sEdges (S.insert $ Edge (NodeConc (j,0)) (NodePrem (i,v)))
    let freshFacts = do
          (v, Fact FreshFact [m]) <- zip [0..] $ get rPrems ru
          return $ do
            j <- freshLVar "vf" LSortNode
            modM sNodes (M.insert j (mkFreshRuleAC m))
            unless (isFreshVar m) $ do 
                -- 'm' must be of sort fresh
                n <- varTerm <$> freshLVar "n" LSortFresh
                solveTermEqs SplitNow [Equal m n]
            modM sEdges (S.insert $ Edge (NodeConc (j,0)) (NodePrem (i,v)))
    -- solve all Fr and In premises
    sequence_ inFacts
    sequence_ freshFacts
    return ru
  where
    mkISendRuleAC m = do
        faPrem <- kuFact Nothing m
        return $ Rule (ProtoInfo ISendRule) [faPrem] [inFact m] [kLogFact m]

    mkFreshRuleAC m = Rule (ProtoInfo FreshRule) [] [freshFact m] []

-- | Create a fresh node labelled with a fresh instance of one of the rules
-- and solve it's 'Fr' and 'In' facts immediatly.
freshRuleNode :: [RuleAC] -> SeProof (NodeId, RuleACInst)
freshRuleNode rules = do
    i <- freshLVar "vr" LSortNode
    (,) i <$> ruleNode i rules

-- | Generate a fresh coerce rule node; return node-index, premise, and
-- conclusion.
freshCoerceRuleNode :: SeProof (LVar, (LNFact, LNFact))
freshCoerceRuleNode = do
    i <- freshLVar "vc" LSortNode
    x <- varTerm <$> freshLVar "x" LSortMsg
    v <- freshLVar "f_" LSortMsg
    let faPrem = Fact KDFact [varTerm v, x]
        faConc = Fact KUFact [varTerm v, x]
    modM sNodes (M.insert i (Rule (IntrInfo CoerceRule) [faPrem] [faConc] []))
    return (i, (faPrem, faConc))

-- | Create a fresh node labelled with a fresh instance of one of the rules
-- and return one of the conclusions.
freshRuleConc :: [RuleAC]
              -> SeProof (RuleACInst, NodeConc, LNFact)
freshRuleConc rules = do
    (i, ru) <- freshRuleNode rules
    (v, fa) <- disjunctionOfList $ zip [0..] $ get rConcs ru
    return (ru, NodeConc (i,v), fa)

-- | Insert the edges and ensure the equality between the facts
-- at either end of the edge.
insertEdges :: [(NodeConc, LNFact, LNFact, NodePrem)] -> SeProof ()
insertEdges edges = do
    solveFactEqs SplitNow [ Equal fa1 fa2 | (_, fa1, fa2, _) <- edges ]
    modM sEdges (\es -> foldr S.insert es [ Edge c p | (c,_,_,p) <- edges])


-- Simplification
-----------------

-- | Repeatedly apply the following simplifications to the sequent:
--
--   - merge nodes with equal instances of Fresh rules
--   - remove sequents that violate the sort constraints
--   - merge nodes marked as the last node
--   - merge multiple rule labels of the same node
--   - merge nodes with equal non-pair message conclusions
--   - merge targets of multiple edges from a linear fact and
--     sources of multiple incoming edges to the same fact.
--   - solve Pub and Fresh goals
--   - solve unique action atoms
--
-- The simplification stops when the sequent doesn't change anymore.
--
simplifySequent :: SeProof ()
simplifySequent = do
    -- start simplification, indicating that some change happened
    go (0 :: Int) [True]
    -- ensure that the substitution is applied to the whole sequent
    substSequent
    exploitUniqueMsgOrder
  where
    go n changes0
      | not (or changes0) = return ()
      | otherwise        = do
          -- perform one simplification pass
          substSequent
          -- exploit uniqueness of 'Fresh' rule instances
          c1 <- exploitFreshUnique
          when c1 (substNodes >> return ())
          -- exploit that conclusions deriving the same message can be merged
          -- except for merging coerce nodes with non-coerce nodes.
          c2 <- exploitUniqueMsgConcs
          when c2 (substNodes >> return ())
          -- exploit the special properties of the last node
          c3 <- exploitLastNode
          when c3 (substNodes >> return ())

          c4 <- solveSimpleUpK
          substPart sEdges
          c5 <- exploitEdgeProps
          substPart sAtoms
          c6 <- solveUniqueActions 
          substPart sFormulas
          substPart sSolvedFormulas
          c7 <- simplifyNegativeOrderings
          c8 <- saturateFormulas

          -- report on looping behaviour if necessary
          se <- gets id
          let changes = [c1, c2, c3, c4, c5, c6, c7, c8]
              traceLoop
                | n <= 10   = id
                | otherwise = 
                      trace ("   simplify: " ++ show n ++ " " ++ show changes)
                    . trace (render $ prettySequent se)

          -- Repeat simplification, if there was some change in this step.
          traceLoop $ go (n + 1) changes


-- | Saturate the formulas. Return True, if the sequent was changed.
saturateFormulas :: SeProof Bool
saturateFormulas = do
    se     <- gets id
    hnd    <- getMaudeHandle
    result <- saturateGuarded hnd se
    case result of
      Nothing         -> do return False
      Just (eqs, se') -> do put se'
                            solveTermEqs SplitNow eqs
                            return True


-- | Solve premise goals that can be solved directly by exploiting special
-- properties of normalized derivation graphs.
--
-- Solve K-up premises can just be connected to already derived knowledge.
--
solveSimpleUpK :: SeProof Bool
solveSimpleUpK = do
    nodes <- M.toList <$> getM sNodes
    let (down, up) = partitionEithers $ do
            (i, ru)   <- nodes
            (v, fa)   <- zip [0..] $ get rConcs ru
            (d, _, m) <- maybe mzero return $ kFactView fa
            let tag = case d of UpK -> Right; DnK -> Left
            return $ tag (m, (d, fa, NodeConc (i, v)))
        -- retain the up-entry if there are duplicates
        derived = M.fromList $ down ++ up

    goals <- gets (map snd . openPremiseGoals)
    or <$> mapM (trySolveGoal derived) goals
  where
    trySolveGoal derived (PremUpKG p m) = trySolveMessage derived m
            (\c _ -> modM sMsgEdges (S.insert (MsgEdge c p)))

    trySolveGoal derived (PremiseG p faPrem) = case kFactView faPrem of
        Just (UpK, _, m) -> trySolveMessage derived m
            -- For premise goals we have 'inp m == [m]'. We must insert a
            -- direct edge and ensure the equality wrt. an additional coerce
            -- node.
            (\c faConc -> insertEdges [(c, faConc, faPrem, p)])

        _                -> return False
    -- all other goals cannot be solved => the sequent doesn't change
    trySolveGoal _ _ = return False
    
    trySolveMessage derived m solveWith = case M.lookup m derived of
        Just (UpK, faConc, c) -> solveWith c faConc >> return True
        Just (DnK, faConc, c) -> do
            (j, (faPrem', faConc')) <- freshCoerceRuleNode
            insertEdges [ (c, faConc , faPrem', NodePrem (j,0)) ]
            _ <- solveWith (NodeConc (j,0)) faConc'
            return True

        Nothing               -> return False


-- | Solve unique actions. Returns 'True' iff the sequent was changed.
solveUniqueActions :: SeProof Bool
solveUniqueActions = do
    rules       <- nonSilentRules <$> askM pcRules
    actionAtoms <- gets sActionAtoms

    let uniqueActions = [ x | [x] <- group (sort allActions) ]
        allActions    = [ (tag, length ts) 
                        | ru <- rules, Fact tag ts <- get rActs ru ]

        isUnique (Fact tag ts) = (tag, length ts) `elem` uniqueActions

        trySolve (i, fa)
          | isUnique fa = solveAction rules (i, fa) >> return True
          | otherwise   = return False

    or <$> mapM trySolve actionAtoms


-- | Exploit that up-premises must always be deduced before the same
-- down-premise.
exploitUniqueMsgOrder :: SeProof ()
exploitUniqueMsgOrder = do
    nodes     <- M.toList <$> getM sNodes
    dedBefore <- gets sDedBeforeAtoms
    let prems = M.fromList $ 
            dedBefore <|> -- also incorporate deducible-before atoms.
            do (i, ru) <- nodes
               fa      <- get rPrems ru
               case kFactView fa of
                 Just (UpK, _, m) -> [ (m', i) | m' <- input m ]
                 _                -> mzero

        concs = M.fromList $ do
            (i, ru) <- nodes
            fa      <- get rConcs ru
            case kFactView fa of
              Just (DnK, _, m) -> return (m, i)
              _                -> mzero

        mkLess i j = Less (varTerm i) (varTerm j)

    -- we can add all elements where we have an intersection
    modM sAtoms $ flip S.union $ S.fromList
                $ M.elems $ M.intersectionWith mkLess concs prems

-- | Exploit that instances of the 'Fresh' rule are unique.
--
-- Returns 'True' if a change was done.
exploitFreshUnique :: SeProof Bool
exploitFreshUnique = do
    -- gather fresh rule nodes and merge nodes with identical conclusions
    updates <- gets ( map merge
                    . groupSortOn (get (rConc 0) . snd)
                    . filter (isFreshRule . snd)
                    . M.toList
                    . get sNodes
                    )
    -- check if there are changes to be applied
    if all (null . snd) updates
      then do return False
      else do modM sNodes (foldr (.) id $ map fst updates)
              solveNodeIdEqs $ concatMap snd updates
              return True
  where
    -- merge duplicate ones by removing all but one node and adding the
    -- equalities between the kept nodes and the removed nodes
    merge []            = error "exploitFreshUnique: impossible"
    merge (keep:remove) =
      ( \nodes -> foldl' (flip M.delete) nodes (map fst remove)
      , map (Equal (fst keep) . fst) remove
      )

-- | Merge multiple incoming edges to all facts and multiple outgoing edges
-- from linear facts.
exploitEdgeProps :: SeProof Bool -- True, if a simplification step happened.
exploitEdgeProps = do
    se <- gets id
    let edges  = [ (getNodeConc src, getNodePrem prem)
                 | Edge src prem <- S.toList (get sEdges se) ]
        rawEqs = mergeEqs fst snd edges ++
                 mergeEqs snd fst (filter (proveLinearConc se . NodeConc . fst) edges)
    -- check if there are changes to be applied
    if all null rawEqs
      then do return False
      else do
        let eqs = concat rawEqs
        -- all indices of merged premises and conclusions must be equal
        contradictoryIf (not $ and [snd l == snd r | Equal l r <- eqs])
        -- nodes must be equal
        solveNodeIdEqs $ map (fmap fst) eqs
        return True
  where
    mergeEqs :: Ord c => (a -> b) -> (a -> c) -> [a] -> [[Equal b]]
    mergeEqs what on = map (merge what) . groupSortOn on

    merge :: (a -> b) -> [a] -> [Equal b]
    merge _    []            = error "exploitEdgeProps: impossible"
    merge proj (keep:remove) = map (Equal (proj keep) . proj) remove


-- | Merge nodes with equal non-pair msg conclusions.
--
-- PRE: There must not be any node in the sequent with a 'KU' conclusion
-- deriving a pair, inversion, or multiplication. This is in invariant of
-- our constraint solver.
exploitUniqueMsgConcs :: SeProof Bool
exploitUniqueMsgConcs = do
    nodes <- M.toList <$> getM sNodes
    let (coerce, nonCoerce) = partitionEithers $ do
          node@(_, ru) <- nodes
          fa      <- get rConcs ru
          case kFactView fa of
            Nothing                          -> mzero
            Just (_, _, m) | isCoerceRule ru -> return $ Left  (m, node)
                           | otherwise       -> return $ Right (m, node)

        -- coerce nodes can only be merged with themselves.
        (removals1, eqs1) = analyze coerce
        -- all other nodes can be merged with each other.
        (removals2, eqs2) = analyze nonCoerce
        eqs               = eqs1 ++ eqs2

    -- check if there are any changes to be done
    if null eqs
        then return False
        else do
            modM sNodes (removals1 . removals2)
            solveNodeIdEqs          $ map (fmap fst) eqs
            solveRuleEqs   SplitNow $ map (fmap snd) eqs
            return True
  where
    analyze = (foldr (.) id *** concat) . unzip . map merge . groupSortOn fst

    merge []            = error "exploitUniqueMsgs: impossible"
    merge (keep:remove) =
      ( \nodes -> foldl' (flip M.delete) nodes (map (fst . snd) remove)
      , map (Equal (snd keep) . snd) remove
      )

-- | Apply a list of changes to the proof state. Return True, if at least one
-- change was applied; i.e., the list of changes is not null.
applyChanges :: [SeProof ()] -> SeProof Bool
applyChanges changes = sequence_ changes >> return (not $ null changes)

-- | Are these two rule instances unifiable.
unifiableRuleACInsts :: MaudeHandle -> RuleACInst -> RuleACInst -> Bool
unifiableRuleACInsts maude ru1 ru2 = 
    not $ null $ (`runReader` maude) $ unifyRuleACInstEqs [Equal ru1 ru2]

-- | Simplify implications of the form @ (i < j) ==> F @: They are left-alone,
-- if either @i@ or @j@ have not yet a node associated, converted to @j < i@,
-- if the nodes of @j@ and @i@ are non-unifiable, and converted to the
-- disjunction @i = j | j < i@, otherwise.
--
-- True is returned if some change was performed.
simplifyNegativeOrderings :: SeProof Bool
simplifyNegativeOrderings = do
    fms   <- getM sFormulas
    nodes <- getM sNodes
    maude <- getMaudeHandle
    applyChanges $ do
        fm@(GGuarded All [] [Less i0 j0] gf) <- S.toList fms
        guard (gf == gfalse)
        case  unifiableRuleACInsts maude <$> M.lookup (nodeFromTerm i0) nodes
                                         <*> M.lookup (nodeFromTerm j0) nodes
         of
          Just b  -> return $ do
            modM sFormulas       $ S.delete fm
            modM sSolvedFormulas $ S.insert fm
            if b
              then modM sFormulas $ S.insert $ 
                       gdisj $ [GAto (EqE i0 j0), GAto (Less j0 i0)]
              else modM sAtoms $ S.insert $ bvarToLVar $ Less j0 i0
          Nothing -> []
  where
    nodeFromTerm (Lit (Var (Free v))) | lvarSort v == LSortNode = v
    nodeFromTerm t                                              = error $
        "expected free node variable, but got '" ++ show t ++ "'"


-- | Exploit that no node with a label can be after the last node. For
-- non-unifiable nodes the ordering is introduced directly. For the
-- remaining ones a disjunction is introduced.
--
-- True is returned if some change was performed.
exploitLastNode :: SeProof Bool
exploitLastNode = do
    lasts <- gets sLastAtoms
    nodes <- getM sNodes
    case lasts of
      []      -> return False
      [iLast] -> -- single last node => add ordering constraints
         case M.lookup iLast nodes of
           Nothing     -> return False
           Just ruLast -> do
              beforeLast <- gets (D.reachableSet lasts . sRawGreaterRel)
              fms        <- getM sFormulas
              maude      <- getMaudeHandle
              applyChanges $ do
                  (i, ru) <- M.toList nodes
                  let disj = mkOrdDisj i iLast
                  guard $ (i /= iLast) &&
                           -- only consider nodes with action constraints
                          (not $ null $ get rActs ru)  && 
                          (i `S.notMember` beforeLast) &&
                          (disj `S.notMember` fms)
                  if unifiableRuleACInsts maude ru ruLast
                    then return $ modM sFormulas $ S.insert disj
                    else return $ modM sAtoms $ S.insert $ 
                             Less (varTerm i) (varTerm iLast)

      _ -> do -- multiple last nodes => merge them
              solveTermEqs SplitNow $ zipWith mkEq lasts (tail lasts)
              return True
  where
    mkEq i j        = Equal (varTerm i) (varTerm j)
    mkOrdDisj i0 j0 = gdisj $ [GAto (EqE i j), GAto (Less i j)]
      where
        i = Lit $ Var $ Free i0
        j = Lit $ Var $ Free j0

-- | @setNodes nodes@ normalizes the @nodes@ such that node ids are unique and
-- then updates the @sNodes@ field of the proof state to the corresponding map.
-- Return @True@ iff new equalities have been added to the equation store.
setNodes :: [(NodeId, RuleACInst)] -> SeProof Bool
setNodes nodes0 = do
    sNodes =: M.fromList nodes
    if null ruleEqs then                         return False
                    else solveRuleEqs SplitLater ruleEqs >> return True
  where
    -- merge nodes with equal node id
    (ruleEqs, nodes) = first concat $ unzip $ map merge $ groupSortOn fst nodes0

    merge []            = error "setNodes: impossible"
    merge (keep:remove) = (map (Equal (snd keep) . snd) remove, keep)

-- | Apply the current substitution of the equation store to the domain
-- of the '_sNodes' field and restore the one-rule-per-node property. Returns
-- @True@ if there were additional equalities added to the equation store.
substNodesDomain :: SeProof Bool
substNodesDomain =
    go False
  where
    go changed = do
        subst <- getM sSubst
        nodes <- gets (map (first (apply subst)) . M.toList . get sNodes)
        changed' <- setNodes nodes
        if changed' then go True
                    else return changed

-- | Apply the current substitution of the equation store to the '_sNodes'
-- field. Returns @True@ if there were additional equalities added to the
-- equation store.
substNodes :: SeProof Bool
substNodes = do
    changed <- substNodesDomain
    (modM sNodes . M.map . apply) =<< getM sSubst
    return changed

-- | Apply the current substitution of the equation store to the remainder of
-- the sequent.
substSequent :: SeProof ()
substSequent = do
    _ <- substNodes
    substPart sEdges
    substPart sMsgEdges
    substPart sChains
    substPart sAtoms
    substPart sFormulas
    substPart sSolvedFormulas
    substPart sLemmas

-- | Apply the current substitution of the equation store to a part of the
-- sequent.
substPart :: Apply a => (Sequent :-> a) -> SeProof ()
substPart l = modM l =<< (apply <$> getM sSubst)

-- | @conjoinSequent se@ conjoins the logical information in @se@ to the proof
-- state. It assumes that the free variables in @se@ are shared with the free
-- variables in the proof state.
conjoinSequent :: Sequent -> SeProof ()
conjoinSequent se = do
    kind <- getM sCaseDistKind 
    unless (kind == get sCaseDistKind se) $
        error "conjoinSequent: typing-kind mismatch"
    joinSets sEdges
    joinSets sMsgEdges
    joinSets sChains
    joinSets sAtoms
    joinSets sFormulas
    joinSets sSolvedFormulas
    joinSets sLemmas
    -- update nodes
    _ <- (setNodes . (M.toList (get sNodes se) ++) . M.toList) =<< getM sNodes
    -- conjoin equation store
    modM sConjDisjEqs (`mappend` get sConjDisjEqs se)
    solveSubstEqs SplitNow $ get sSubst se
    -- propagate substitution changes
    substSequent
  where
    joinSets :: Ord a => (Sequent :-> S.Set a) -> SeProof ()
    joinSets proj = modM proj (`S.union` get proj se)


-- Unification through the equation store of the embedded sequent
-----------------------------------------------------------------

-- | @noContradictoryEqStore@ suceeds iff the equation store is not
-- contradictory.
noContradictoryEqStore :: SeProof ()
noContradictoryEqStore =
    (contradictoryIf . eqsIsFalse) =<< getM sEqStore

-- | Add a list of term equalities to the equation store. And
--  split resulting disjunction of equations according
--  to given split strategy.
solveTermEqs :: SplitStrategy -> [Equal LNTerm] -> SeProof ()
solveTermEqs splitStrat eqs = do
    hnd <- getMaudeHandle
    setM sEqStore =<< simp hnd
                  =<< disjunctionOfList
                  =<< addEqs splitStrat hnd eqs
                  =<< getM sEqStore
    noContradictoryEqStore

-- | Add a list of equalities in substitution form to the equation store
solveSubstEqs :: SplitStrategy -> LNSubst -> SeProof ()
solveSubstEqs split subst =
    solveTermEqs split [Equal (varTerm v) t | (v, t) <- substToList subst]

-- | Add a list of node equalities to the equation store.
solveNodeIdEqs :: [Equal NodeId] -> SeProof ()
solveNodeIdEqs = solveTermEqs SplitNow . map (fmap varTerm)

-- | Add a list of fact equalities to the equation store, if possible.
solveFactEqs :: SplitStrategy -> [Equal LNFact] -> SeProof ()
solveFactEqs split eqs = do
    contradictoryIf (not $ all evalEqual $ map (fmap factTag) eqs)
    solveListEqs (solveTermEqs split) $ map (fmap factTerms) eqs

-- | Add a list of rule equalities to the equation store, if possible.
solveRuleEqs :: SplitStrategy -> [Equal RuleACInst] -> SeProof ()
solveRuleEqs split eqs = do
    contradictoryIf (not $ all evalEqual $ map (fmap (get rInfo)) eqs)
    solveListEqs (solveFactEqs split) $
        map (fmap (get rConcs)) eqs ++ map (fmap (get rPrems)) eqs

-- | Solve a list of equalities using the given solver.
solveListEqs :: ([Equal a] -> SeProof b) -> [(Equal [a])] -> SeProof b
solveListEqs solver eqs = do
    contradictoryIf (not $ all evalEqual $ map (fmap length) eqs)
    solver $ concatMap flatten eqs
  where
    flatten (Equal l r) = zipWith Equal l r


-- | Solve the constraints associated with a rule with the given vertex.
solveRuleConstraints :: Maybe RuleACConstrs -> NodeId -> SeProof ()
solveRuleConstraints (Just eqConstr) _v = do
    hnd <- getMaudeHandle
    setM sEqStore
        =<< (simp hnd . addRuleVariants eqConstr)
        =<< getM sEqStore
    noContradictoryEqStore
solveRuleConstraints Nothing _ = return ()

------------------------------------------------------------------------------
-- Extracting and solving goals
------------------------------------------------------------------------------

data Usefulness = Useful | Useless
  deriving (Show, Eq, Ord)

-- FIXME: SM: Remove support for requires facts.
-- | All open premises stemming both from labelled nodes and requires facts.
openPremiseGoals :: Sequent -> [(Usefulness, Goal)]
openPremiseGoals se = do
    (i, ru) <- oneOfMap $ get sNodes se
    (u, fa) <- zip [0..] $ get rPrems ru
    let p = NodePrem (i, u)
    case fa of
      -- up-K facts
      (kFactView -> Just (UpK, _, m))  -> case input m of
          [m'] | m == m' -> do
            guard (not (trivial m') && (p, m') `S.notMember` coveredMsgPrems)
            return $ markUseless m' i $ PremiseG p fa
          m's            -> do
            m' <- sortednub m's
            guard (not (trivial m') && (p, m') `S.notMember` coveredMsgPrems)
            return $ markUseless m' i $ PremUpKG p m'

      -- down-K facts
      (kFactView -> Just (DnK, _, _))
        | p `S.member` coveredPrems -> mzero
        | otherwise                 -> return . (Useful,)  $ PremDnKG p
      -- all other facts
      _ | p `S.member` coveredPrems -> mzero
        | otherwise                 -> return . (Useful,) $ PremiseG p fa
  where
    coveredPrems     = S.fromList $ eTgt <$> S.toList (get sEdges se) <|>
                                    cTgt <$> S.toList (get sChains se)

    coveredMsgPrems  = S.fromList $ do
        (c, p) <- [ (c, p) | MsgEdge c p <- S.toList (get sMsgEdges se) ] <|>
                  [ (c, p) | Edge c p    <- S.toList (get sEdges se)    ]

        case kFactView =<< resolveNodeConcFact c se of
          Just (UpK, _, m) -> return (p, m)
          _                -> []

    existingDeps = sRawLessRel se

    -- We use the following heuristic for marking KU-goals as useful (worth
    -- solving now) or useless (to be delayed until no more useful goal
    -- remain). We ignore all goals that do not contain a fresh variable
    -- or where there exists a node, not after the premise or the last node,
    -- providing an Out or KD conclusion that provides the message we are
    -- looking for as a toplevel term.
    --
    -- If such a node exist, then solving the goal will result in at least one
    -- case where we didn't make real progress except.
    markUseless m i
        | not (containsFreshVars m) || deducible = (,) Useless
        | otherwise                              = (,) Useful
        where
          containsFreshVars = any ((LSortFresh ==) . lvarSort) . frees

          toplevelTerms t@(destPair -> Just (t1, t2)) = 
              t : toplevelTerms t1 ++ toplevelTerms t2
          toplevelTerms t@(destInv -> Just t1) = t : toplevelTerms t1
          toplevelTerms t = [t]

          deducible = or $ do
              (j, ru) <- M.toList $ get sNodes se
              -- We cannot deduce a message from a last node.
              guard (Last (varTerm j) `S.notMember` get sAtoms se)
              let derivedMsgs = concatMap toplevelTerms $
                      [ t | Fact OutFact [t] <- get rConcs ru] <|>
                      [ t | Just (DnK, _, t) <- kFactView <$> get rConcs ru]
              -- m is deducible from j without an immediate contradiction
              -- if it is a derived message of 'ru' and the dependency does
              -- not make the graph cyclic.
              return $ m `elem` derivedMsgs && 
                       not (D.cyclic ((j, i) : existingDeps))


-- | All open chain goals. These are all the chains that do not end in a
-- message variable in the sequent because they are deleted upon solving.
openChainGoals :: Sequent -> [Goal]
openChainGoals se = do
    ch@(Chain c _) <- S.toList $ get sChains se
    case kFactView (nodeConcFact c se) of
      Just (DnK, _, m) | isMsgVar m -> mzero
                       | otherwise  -> return $ ChainG ch
      fa -> error $ "openChainGoals: impossible fact: " ++ show fa

-- | All open splitting goals.
openSplitGoals :: Sequent -> [Goal]
openSplitGoals se = SplitG <$> eqSplits (get sEqStore se)

-- | All open action goals.
openActionGoals :: Sequent -> [Goal]
openActionGoals se = uncurry ActionG <$> sActionAtoms se

-- | All open goals (non-deterministic choices of possible proof steps) in the
-- sequent.
openGoals :: Sequent -> [Goal]
openGoals se = delayUseless $ concat $
   [ (Useful,) <$> openActionGoals se
   , (Useful,) <$> openDisjunctionGoals se
   , (Useful,) <$> openChainGoals se
   , preferProtoFactGoals $ openPremiseGoals se
   -- SM: Commented out as automatic saturation works again.
   -- , (Useful,) <$> openImplicationGoals se
   , (Useful,) <$> openSplitGoals se
   ]
  where
    isProtoFactGoal (_, PremiseG _ _) = True
    isProtoFactGoal _                 = False
    preferProtoFactGoals goals =
        uncurry (++) $ partition isProtoFactGoal goals

    delayUseless = map snd . sortOn fst


-- | Solve an action goal.
solveAction :: [RuleAC]       -- ^ All rules labelled with an action
            -> (LVar, LNFact) -- ^ The action we are looking for.
            -> SeProof String -- ^ Sensible case name.
solveAction rules (i, fa) = do
    modM sAtoms (S.delete (Action (varTerm i) fa))
    mayRu <- M.lookup i <$> getM sNodes
    showRuleCaseName <$> case mayRu of
        Nothing -> do ru  <- ruleNode i rules
                      act <- disjunctionOfList $ get rActs ru
                      solveFactEqs SplitNow [Equal fa act]
                      return ru
        Just ru -> do unless (fa `elem` get rActs ru) $ do
                        act <- disjunctionOfList $ get rActs ru
                        solveFactEqs SplitNow [Equal fa act]
                      return ru

-- | Solve a K-up-knowledge premise.
solvePremUpK :: [RuleAC]  -- ^ All construction rules.
             -> NodePrem
             -> LNTerm
             -> SeProof String
solvePremUpK rules p m = do
    (ru, c, faConc) <- freshRuleConc rules
    case kFactView faConc of
      Just (UpK, _, m') ->
        do solveTermEqs SplitNow [(Equal m m')]
           modM sMsgEdges (S.insert (MsgEdge c p))
           return $ showRuleCaseName ru

      _ -> error $ "solvePremUpK: unexpected fact: " ++ show faConc

-- | Solve a premise with a direct edge from a unifying conclusion.
--
-- Note that 'In' and 'Fr' facts are solved directly when adding a 'ruleNode'.
solvePremise :: [RuleAC]       -- ^ All construction and protocol rules.
             -> NodePrem       -- ^ Premise to solve.
             -> LNFact         -- ^ Fact required at this premise.
             -> SeProof String -- ^ Case name to use
solvePremise rules p faPrem = do
    (ru, c, faConc) <- freshRuleConc rules
    solveFactEqs SplitNow [(Equal faPrem faConc)]
    modM sEdges (S.insert (Edge c p))
    return $ showRuleCaseName ru

-- | Solve a K-down-knowledge premise.
solvePremDnK :: [RuleAC] -- ^ All rules that derive a send fact.
             -> NodePrem -- ^ The K-down premise to solve.
             -> SeProof String
solvePremDnK rules p = do
    iLearn    <- freshLVar "vl" LSortNode
    mLearn    <- varTerm <$> freshLVar "t" LSortMsg
    concLearn <- kdFact (Just IsNoExp) mLearn
    let premLearn = outFact mLearn
        ruLearn = Rule (ProtoInfo IRecvRule) [premLearn] [concLearn] []
        cLearn = NodeConc (iLearn, 0)
        pLearn = NodePrem (iLearn, 0)
    modM sNodes  (M.insert iLearn ruLearn)
    modM sChains (S.insert (Chain cLearn p))
    solvePremise rules pLearn premLearn

-- | Solve a chain constraint.
solveChain :: [RuleAC]        -- ^ All destruction rules.
           -> Chain           -- ^ The chain to extend by one step
           -> SeProof String
solveChain rules ch@(Chain c p) = do
    modM sChains (S.delete ch)
    faConc  <- gets $ nodeConcFact c
    (do -- solve it by a direct edge
        faPrem <- gets $ nodePremFact p
        solveFactEqs SplitNow [(Equal faPrem faConc)]
        modM sEdges  (S.insert (Edge c p))
        let m = case kFactView faConc of
                  Just (DnK, _, m') -> m'
                  _                 -> error $ "solveChain: impossible"
            caseName (FApp o _) = show o
            caseName t          = show t
        return $ caseName m 
     `disjunction`
     do -- extend it with one step
        (i, ru)     <- freshRuleNode rules
        (v, faPrem) <- disjunctionOfList $ zip [0..] $ get rPrems ru
        solveFactEqs SplitNow [(Equal faPrem faConc)]
        modM sEdges (S.insert (Edge c (NodePrem (i,v))))
        modM sChains (S.insert (Chain (NodeConc (i,0)) p))
        return $ showRuleCaseName ru
     )

-- | Solve an equation split.
solveSplit :: SplitId -> SeProof String
solveSplit x = do
    split <- gets ((`splitAtPos` x) . get sEqStore)
    let errMsg = error "solveSplit: split of equations on unconstrained variable!"
    store  <- maybe errMsg disjunctionOfList split
    hnd    <- getMaudeHandle
    store' <- simp hnd store
    contradictoryIf (eqsIsFalse store')
    sEqStore =: store'
    return "split"

-- | Solve a disjunction of guarded formulas using splitting.
-- Returns a case name.
solveDisjunction :: Disj LNGuarded -> SeProof String
solveDisjunction disj = do
    modM sSolvedFormulas (S.insert $ GDisj disj)
    modM sSolvedFormulas (S.insert $ GDisj disj)
    (i, gfm) <- disjunctionOfList $ zip [(1::Int)..] $ getDisj disj
    modM sFormulas (S.insert gfm)
    return $ "case_" ++ show i

-- | @solveGoal rules goal@ enumerates all possible solutions how this goal
-- could be solved in the context of the given @rules@.
--
-- Returns a usable case name.
--
solveGoal :: Goal -> SeProof String
solveGoal goal = do
    rules <- askM pcRules
    trace ("   solving goal: " ++ render (prettyGoal goal)) $
      case goal of
        ActionG i fa   -> solveAction  (nonSilentRules rules) (i, fa) 
        PremiseG p fa  -> 
            solvePremise (get crProtocol rules ++ get crConstruct rules) p fa
        PremDnKG p     -> solvePremDnK (get crProtocol  rules) p
        PremUpKG p m   -> solvePremUpK (get crConstruct rules) p m
        ChainG ch      -> solveChain   (get crDestruct  rules) ch
        SplitG i       -> solveSplit i
        DisjG disj     -> solveDisjunction disj
        ImplG gf       -> modM sFormulas (S.insert gf) >> return "add_formula"