content: {-# LANGUAGE DeriveFunctor              #-}
  {-# LANGUAGE DeriveGeneric              #-}
  
  module Language.Fixpoint.Types.Triggers (
  
      Triggered (..), Trigger(..),
  
      noTrigger, defaultTrigger,
  
      makeTriggers
  
      ) where
  
  import qualified Data.Store as S
  import           Control.DeepSeq
  import           GHC.Generics              (Generic)
  import           Text.PrettyPrint.HughesPJ
  
  import Language.Fixpoint.Types.Refinements
  import Language.Fixpoint.Types.PrettyPrint
  import Language.Fixpoint.Misc              (errorstar)
  
  
  data Triggered a = TR Trigger a
    deriving (Eq, Show, Functor, Generic)
  
  data Trigger = NoTrigger | LeftHandSide
    deriving (Eq, Show, Generic)
  
  instance PPrint Trigger where
    pprintTidy _ = text . show
  
  instance PPrint a => PPrint (Triggered a) where
    pprintTidy k (TR t x) = parens (pprintTidy k t <+> text ":" <+> pprintTidy k x)
  
  noTrigger :: e -> Triggered e
  noTrigger = TR NoTrigger
  
  defaultTrigger :: e -> Triggered e
  defaultTrigger = TR LeftHandSide
  
  makeTriggers :: Triggered Expr -> [Expr]
  makeTriggers (TR LeftHandSide e) = [getLeftHandSide e]
  makeTriggers (TR NoTrigger    _) = errorstar "makeTriggers on NoTrigger"
  
  
  getLeftHandSide :: Expr -> Expr
  getLeftHandSide (ECst e _)
    = getLeftHandSide e
  getLeftHandSide (PAll _ e)
    = getLeftHandSide e
  getLeftHandSide (PExist _ e)
    = getLeftHandSide e
  getLeftHandSide (PAtom eq lhs _)
    | eq == Eq || eq == Ueq
    = lhs
  getLeftHandSide (PIff lhs _)
    = lhs
  getLeftHandSide _
   = defaltPatter
  
  -- NV TODO find out a valid, default pattern that does not instantiate the axiom
  defaltPatter :: Expr
  defaltPatter = PFalse
  
  instance S.Store Trigger
  instance NFData   Trigger
  
  instance (S.Store a) => S.Store (Triggered a)
  instance (NFData a)   => NFData   (Triggered a)
  