{-# LANGUAGE TemplateHaskell, FlexibleContexts, DeriveDataTypeable #-}
-- |
-- Copyright   : (c) 2011, 2012 Benedikt Schmidt & Simon Meier
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Simon Meier <iridcode@gmail.com>
-- Portability : GHC only
--
-- Facts used to formulate and reason about protocol execution.
module Theory.Fact (

  -- * Fact
    Fact(..)
  , Multiplicity(..)
  , FactTag(..)

  -- ** Queries
  , isLinearFact   
  , isPersistentFact
  , isProtoFact

  , showFactTag
  , showFactTagArity
  , factTagArity
  , factTagMultiplicity
  , factArity
  , factMultiplicity

  -- ** Message deduction facts
  , ExpTag(..)
  , expTagToTerm
  , termToExpTag

  , DirTag(..)
  , kFactView
  , isKFact
  , kuFact
  , kdFact

  -- ** Construction
  , freshFact
  , outFact
  , inFact
  , kLogFact
  , protoFact

  -- * NFact
  , NFact

  -- * LFact
  , LFact
  , LNFact
  , unifyLNFactEqs
  , matchLNFact

  -- * Pretty-Printing
  
  , prettyFact
  , prettyNFact
  , prettyLNFact

  -- * Convenience exports
  , module Term.Unification

  ) where

import Control.Basics
import Control.Monad.Fresh
import Control.DeepSeq

import Data.DeriveTH
import Data.Foldable (Foldable(..))
import Data.Traversable (Traversable(..))
import Data.Binary
import Data.Generics 
import Data.Maybe (isJust)

import Term.Unification

import Text.Isar


------------------------------------------------------------------------------
-- Fact
------------------------------------------------------------------------------

data Multiplicity = Persistent | Linear
                  deriving( Eq, Ord, Show, Typeable, Data )

-- | Fact tags/symbols
data FactTag = ProtoFact Multiplicity String Int
               -- ^ A protocol fact together with its arity and multiplicity.
             | FreshFact  -- ^ Freshly generated value.
             | OutFact   -- ^ Sent by the protocol
             | InFact  -- ^ Officially known by the intruder/network.
             | KUFact     -- ^ Up-knowledge fact in messsage deduction.
             | KDFact     -- ^ Down-knowledge fact in message deduction.
    deriving( Eq, Ord, Show, Typeable, Data )

-- | Facts.
data Fact t = Fact 
    { factTag   :: FactTag 
    , factTerms :: [t]
    }
    deriving( Eq, Ord, Show, Typeable, Data )


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

instance Functor Fact where
    fmap f (Fact tag ts) = Fact tag (fmap f ts)

instance Foldable Fact where
    foldMap f (Fact _ ts) = foldMap f ts
    
instance Traversable Fact where
    sequenceA (Fact tag ts) = Fact tag <$> sequenceA ts
    traverse f (Fact tag ts) = Fact tag <$> traverse f ts

instance Sized t => Sized (Fact t) where
  size (Fact _ args) = size args

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

instance Apply t => Apply (Fact t) where
    apply subst = fmap (apply subst)


-- KU and KD facts
------------------

-- | Message fact exponentation tag.
data ExpTag = IsExp | IsNoExp
            deriving( Eq, Ord, Show)

-- | Exponentiation-symbol to term.
expTagToTerm :: ExpTag -> LNTerm
expTagToTerm IsExp   = Lit (Con (Name PubName (NameId ("exp"))))
expTagToTerm IsNoExp = Lit (Con (Name PubName (NameId ("noexp"))))

-- | Term to exponentiation-symbol.
termToExpTag :: LNTerm -> Maybe ExpTag
termToExpTag (Lit (Con (Name PubName (NameId ("exp")))))   = return IsExp
termToExpTag (Lit (Con (Name PubName (NameId ("noexp"))))) = return IsNoExp
termToExpTag _                                             = mzero


-- | A direction tag 
data DirTag = UpK | DnK
            deriving( Eq, Ord, Show )

-- | Construct a message fact. If no 'ExpTag' is given, then
-- a fresh variable that matches any 'ExpTag' is constructed.
kuFact, kdFact :: MonadFresh m => Maybe ExpTag -> LNTerm -> m LNFact
kuFact = mkFact KUFact
kdFact = mkFact KDFact

-- | A generic fact creation function.
mkFact :: MonadFresh m => FactTag -> Maybe ExpTag -> LNTerm -> m LNFact
mkFact tag (Just t) m = return $ Fact tag [expTagToTerm t, m]
mkFact tag Nothing  m = do
    v <- freshLVar "f_" LSortMsg
    return $ Fact tag [varTerm v, m]

-- | View a message-deduction fact.
kFactView :: LNFact -> Maybe (DirTag, Maybe ExpTag, LNTerm)
kFactView fa = case fa of
    Fact KUFact [e, m] -> Just (UpK, termToExpTag e, m)
    Fact KUFact _      -> errMalformed
    Fact KDFact [e, m] -> Just (DnK, termToExpTag e, m)
    Fact KDFact _      -> errMalformed
    _                  -> Nothing
  where
    errMalformed = error $ show "viewKFact: malformed fact: " ++ show fa

-- | True if the fact is a message-deduction fact.
isKFact :: LNFact -> Bool
isKFact = isJust . kFactView

-- Constructing facts
---------------------

-- | A fact denoting a message sent by the protocol to the intruder.
outFact :: t -> Fact t
outFact = Fact OutFact . return

-- | A fresh fact denotes a fresh unguessable name.
freshFact :: t -> Fact t
freshFact = Fact FreshFact . return

-- | A fact denoting that the intruder sent a message to the protocol.
inFact :: t -> Fact t
inFact = Fact InFact . return

-- | A fact logging that the intruder knows a message.
kLogFact :: t -> Fact t
kLogFact = protoFact Linear "K" . return

-- | A protocol fact denotes a fact generated by a protocol rule.
protoFact :: Multiplicity -> String -> [t] -> Fact t
protoFact multi name ts = Fact (ProtoFact multi name (length ts)) ts


-- Queries on facts
-------------------

-- | True iff the fact is a non-special protocol fact.
isProtoFact :: Fact t -> Bool
isProtoFact (Fact (ProtoFact _ _ _) _) = True
isProtoFact _                          = False

-- | True if the fact is a linear fact.
isLinearFact :: Fact t -> Bool
isLinearFact = (Linear ==) . factMultiplicity

-- | True if the fact is a persistent fact.
isPersistentFact :: Fact t -> Bool
isPersistentFact = (Persistent ==) . factMultiplicity

-- | The multiplicity of a 'FactTag'.
factTagMultiplicity :: FactTag -> Multiplicity
factTagMultiplicity tag = case tag of 
    ProtoFact multi _ _ -> multi
    KUFact              -> Persistent
    KDFact              -> Persistent
    _                   -> Linear

-- | The arity of a 'FactTag'.
factTagArity :: FactTag -> Int
factTagArity tag = case tag of 
    ProtoFact _ _ k -> k
    KUFact          -> 2
    KDFact          -> 2
    FreshFact       -> 1
    InFact       -> 1
    OutFact        -> 1

-- | The arity of a 'Fact'.
factArity :: Fact t -> Int
factArity (Fact tag ts)
  | length ts == k = k
  | otherwise      = error $ "factArity: tag of arity " ++ show k ++ 
                             " applied to " ++ show (length ts) ++ " terms"
  where
    k = factTagArity tag

-- | The multiplicity of a 'Fact'.
factMultiplicity :: Fact t -> Multiplicity
factMultiplicity = factTagMultiplicity . factTag


------------------------------------------------------------------------------
-- NFact
------------------------------------------------------------------------------

-- | Facts with literals containing names and arbitrary variables.
type NFact v = Fact (NTerm v)


------------------------------------------------------------------------------
-- LFact
------------------------------------------------------------------------------

-- | Facts with literals arbitrary constants and logical variables.
type LFact c = Fact (LTerm c)

-- | Facts used for proving; i.e. variables fixed to logical variables
-- and constant fixed to names.
type LNFact = Fact LNTerm

-- | Unify a list of @LFact@ equalities.
unifyLNFactEqs :: [Equal LNFact] -> WithMaude [LNSubstVFresh]
unifyLNFactEqs eqs 
  -- TODO: Check if the arity of the facts is also checked.
  | all (evalEqual . fmap factTag) eqs = 
      unifyLNTerm (map (fmap (listToTerm . factTerms)) eqs)
  | otherwise = return []
 
-- | @matchLFact t p@ is a complete set of AC matchers for the term fact @t@
-- and the pattern fact @p@.
matchLNFact :: LNFact -- ^ Term
            -> LNFact -- ^ Pattern
            -> WithMaude [LNSubst]
matchLNFact t p
  | (factTag t == factTag p && length (factTerms t) == length (factTerms p)) =
       matchLNTerm $ zipWith MatchWith (factTerms t) (factTerms p)
  | otherwise = return []


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

-- | Show a fact tag as a 'String'.
showFactTag :: FactTag -> String
showFactTag tag = case tag of
    KUFact            -> "!KU"
    KDFact            -> "!KD"
    InFact            -> "In"
    OutFact           -> "Out"
    FreshFact         -> "Fr"
    (ProtoFact m n _) -> multi m ++ n
  where
    multi Linear     = ""
    multi Persistent = "!"

-- | Show a fact tag together with its aritiy.
showFactTagArity :: FactTag -> String
showFactTagArity tag = showFactTag tag ++ "/" ++ show (factTagArity tag)

-- | Pretty print a fact.
prettyFact :: Document d => (t -> d) -> Fact t -> d
prettyFact ppTerm (Fact tag ts)
  | factTagArity tag /= length ts = ppFact ("MALFORMED-" ++ show tag) ts
  | otherwise                     = ppFact (showFactTag tag) ts
  where
    ppFact n = nestShort' (n ++ "(") ")" . fsep . punctuate comma . map ppTerm

-- | Pretty print a 'NFact'.
prettyNFact :: Document d => LNFact -> d
prettyNFact = prettyFact prettyNTerm

-- | Pretty print a 'LFact'.
prettyLNFact :: Document d => LNFact -> d
prettyLNFact fa = prettyFact prettyNTerm fa

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

$( derive makeBinary ''Multiplicity)
$( derive makeBinary ''FactTag)
$( derive makeBinary ''Fact)

$( derive makeNFData ''Multiplicity)
$( derive makeNFData ''FactTag)
$( derive makeNFData ''Fact)