{-# LANGUAGE StandaloneDeriving
           , FlexibleContexts
           , TypeSynonymInstances
           , FlexibleInstances
           , DeriveDataTypeable
           , TupleSections
           , TemplateHaskell
           , ViewPatterns
  #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
  -- spurious warnings for view patterns
-- |
-- Copyright   : (c) 2011, 2012 Benedikt Schmidt & Simon Meier
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Simon Meier <iridcode@gmail.com>
-- Portability : GHC only
--
-- Formulas that represent security properties.
module Theory.Atom(

  -- * Atoms
    Atom(..)
  , NAtom
  , LNAtom

  -- * LFormula
  , BLVar
  , BLAtom

  -- * Pretty-Printing
  , prettyNAtom
  )
where

-- import Term.Rewriting.NormAC
import Theory.Rule
import Theory.Pretty

import Data.Monoid   (mappend)
import Data.Foldable (Foldable, foldMap)
import Data.Traversable 
import Data.Generics
import Data.DeriveTH
import Data.Binary

import Control.Basics
import Control.DeepSeq

------------------------------------------------------------------------------
-- Atoms
------------------------------------------------------------------------------

-- | @Atom@'s are the atoms of trace formulas parametrized over arbitrary
-- terms. 
data Atom t = Action   t (Fact t)
            | EqE  t t
            | Less t t
            | Last t
            | DedBefore t t
            | EdgeA (t, ConcIdx) (t, PremIdx)
            deriving( Eq, Ord, Show, Data, Typeable )

-- | @LAtom@ are the atoms we actually use in graph formulas input by the user.
type NAtom v = Atom (VTerm Name v)

-- | @LAtom@ are the atoms we actually use in graph formulas input by the user.
type LNAtom = Atom LNTerm

-- | 'LVar's combined with quantified variables. They occur only in 'LFormula's.
type BLVar = BVar LVar

-- | Terms built over names and 'LVar's combined with quantified variables.
type BLTerm = NTerm BLVar

-- | Atoms built over 'BLTerm's.
type BLAtom = Atom BLTerm


-- Instances
------------

instance Functor Atom where
    fmap f (Action   i fa) = Action    (f i) (fmap f fa)
    fmap f (EqE l r)       = EqE       (f l) (f r)
    fmap f (Less v u)      = Less      (f v) (f u)
    fmap f (Last i)        = Last      (f i)
    fmap f (DedBefore t i) = DedBefore (f t) (f i)
    fmap f (EdgeA x y)     = EdgeA     (first f x) (first f y)

instance Foldable Atom where
    foldMap f (Action i fa)   = 
        f i `mappend` (foldMap f fa)
    foldMap f (EqE l r)       = f l `mappend` f r
    foldMap f (Less i j)      = f i `mappend` f j
    foldMap f (Last i)        = f i
    foldMap f (DedBefore t i) = f t `mappend` f i
    foldMap f (EdgeA x y)     = f (fst x) `mappend` f (fst y)

instance Traversable Atom where
    traverse f (Action i fa)   = 
        Action <$> f i <*> traverse f fa
    traverse f (EqE l r)       = EqE <$> f l <*> f r
    traverse f (Less v u)      = Less <$> f v <*> f u
    traverse f (Last i)        = Last <$> f i
    traverse f (DedBefore t i) = DedBefore <$> f t <*> f i
    traverse f (EdgeA (x,i) (y,j)) = 
        EdgeA <$> ((,i) <$> f x) <*> ((,j) <$> f y)

instance HasFrees t => HasFrees (Atom t) where
    foldFrees f = foldMap (foldFrees f)
    mapFrees  f = traverse (mapFrees f)

instance Apply LNAtom where
    apply subst (Action i fact)   = Action (apply subst i) (apply subst fact)
    apply subst (EqE l r)         = EqE (apply subst l) (apply subst r)
    apply subst (Less i j)        = Less (apply subst i) (apply subst j)
    apply subst (Last i)          = Last (apply subst i)
    apply subst (DedBefore t i)   = DedBefore (apply subst t) (apply subst i)
    apply subst (EdgeA x y)       = 
        EdgeA (first (apply subst) x) (first (apply subst) y)

instance Apply BLVar where
    apply _     x@(Bound _) = x
    apply subst x@(Free  v) = maybe x extractVar $ imageOf subst v
      where
        extractVar (viewTerm -> Lit (Var v')) = Free v'
        extractVar _t                     = 
          error $ "apply (BLVar): variable '" ++ show v ++ 
                  "' substituted with term '" -- ++ show _t ++ "'"

instance Apply BLTerm where
    apply subst = (`bindTerm` applyBLLit)
      where
        applyBLLit :: Lit Name BLVar -> BLTerm
        applyBLLit l@(Var (Free v)) = 
            maybe (lit l) (fmapTerm (fmap Free)) (imageOf subst v)
        applyBLLit l                = lit l

instance Apply BLAtom where
    apply subst (Action i fact)   = Action (apply subst i) (apply subst fact)
    apply subst (EqE l r)         = EqE (apply subst l) (apply subst r)
    apply subst (Less i j)        = Less (apply subst i) (apply subst j)
    apply subst (Last i)          = Last (apply subst i)
    apply subst (DedBefore t i)   = DedBefore (apply subst t) (apply subst i)
    apply subst (EdgeA x y)       = 
        EdgeA (first (apply subst) x) (first (apply subst) y)


------------------------------------------------------------------------------
-- Pretty-Printing
------------------------------------------------------------------------------

prettyNAtom :: (Show v, HighlightDocument d) => NAtom v -> d
prettyNAtom (Action v fa) = 
    prettyFact prettyNTerm fa <-> opAction <-> text (show v) 
prettyNAtom (EqE l r) =
    sep [prettyNTerm l <-> opEqual, prettyNTerm r]
    -- sep [prettyNTerm l <-> text "≈", prettyNTerm r]
prettyNAtom (Less u v) = text (show u) <-> opLess <-> text (show v)
prettyNAtom (Last i)   = operator_ "Last" <> parens (text (show i))
prettyNAtom (DedBefore t i) = text (show t) <-> opDedBefore <-> text (show i)
prettyNAtom (EdgeA x y) = text (show x) <-> opEdge <-> text (show y)


-- derived instances
--------------------

$( derive makeNFData ''Atom)
$( derive makeBinary ''Atom)