{-# LANGUAGE DeriveDataTypeable         #-}
{-# LANGUAGE DeriveFunctor              #-}
{-# LANGUAGE DeriveGeneric              #-}

module Language.Fixpoint.Types.Triggers (

    Triggered (..), Trigger(..),

    noTrigger, defaultTrigger,

    makeTriggers

    ) where

import qualified Data.Binary as B
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 (Triggered a -> Triggered a -> Bool
(Triggered a -> Triggered a -> Bool)
-> (Triggered a -> Triggered a -> Bool) -> Eq (Triggered a)
forall a. Eq a => Triggered a -> Triggered a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Triggered a -> Triggered a -> Bool
$c/= :: forall a. Eq a => Triggered a -> Triggered a -> Bool
== :: Triggered a -> Triggered a -> Bool
$c== :: forall a. Eq a => Triggered a -> Triggered a -> Bool
Eq, Int -> Triggered a -> ShowS
[Triggered a] -> ShowS
Triggered a -> String
(Int -> Triggered a -> ShowS)
-> (Triggered a -> String)
-> ([Triggered a] -> ShowS)
-> Show (Triggered a)
forall a. Show a => Int -> Triggered a -> ShowS
forall a. Show a => [Triggered a] -> ShowS
forall a. Show a => Triggered a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Triggered a] -> ShowS
$cshowList :: forall a. Show a => [Triggered a] -> ShowS
show :: Triggered a -> String
$cshow :: forall a. Show a => Triggered a -> String
showsPrec :: Int -> Triggered a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Triggered a -> ShowS
Show, a -> Triggered b -> Triggered a
(a -> b) -> Triggered a -> Triggered b
(forall a b. (a -> b) -> Triggered a -> Triggered b)
-> (forall a b. a -> Triggered b -> Triggered a)
-> Functor Triggered
forall a b. a -> Triggered b -> Triggered a
forall a b. (a -> b) -> Triggered a -> Triggered b
forall (f :: * -> *).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
<$ :: a -> Triggered b -> Triggered a
$c<$ :: forall a b. a -> Triggered b -> Triggered a
fmap :: (a -> b) -> Triggered a -> Triggered b
$cfmap :: forall a b. (a -> b) -> Triggered a -> Triggered b
Functor, (forall x. Triggered a -> Rep (Triggered a) x)
-> (forall x. Rep (Triggered a) x -> Triggered a)
-> Generic (Triggered a)
forall x. Rep (Triggered a) x -> Triggered a
forall x. Triggered a -> Rep (Triggered a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (Triggered a) x -> Triggered a
forall a x. Triggered a -> Rep (Triggered a) x
$cto :: forall a x. Rep (Triggered a) x -> Triggered a
$cfrom :: forall a x. Triggered a -> Rep (Triggered a) x
Generic)

data Trigger = NoTrigger | LeftHandSide
  deriving (Trigger -> Trigger -> Bool
(Trigger -> Trigger -> Bool)
-> (Trigger -> Trigger -> Bool) -> Eq Trigger
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Trigger -> Trigger -> Bool
$c/= :: Trigger -> Trigger -> Bool
== :: Trigger -> Trigger -> Bool
$c== :: Trigger -> Trigger -> Bool
Eq, Int -> Trigger -> ShowS
[Trigger] -> ShowS
Trigger -> String
(Int -> Trigger -> ShowS)
-> (Trigger -> String) -> ([Trigger] -> ShowS) -> Show Trigger
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Trigger] -> ShowS
$cshowList :: [Trigger] -> ShowS
show :: Trigger -> String
$cshow :: Trigger -> String
showsPrec :: Int -> Trigger -> ShowS
$cshowsPrec :: Int -> Trigger -> ShowS
Show, (forall x. Trigger -> Rep Trigger x)
-> (forall x. Rep Trigger x -> Trigger) -> Generic Trigger
forall x. Rep Trigger x -> Trigger
forall x. Trigger -> Rep Trigger x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep Trigger x -> Trigger
$cfrom :: forall x. Trigger -> Rep Trigger x
Generic)

instance PPrint Trigger where 
  pprintTidy :: Tidy -> Trigger -> Doc
pprintTidy Tidy
_ = String -> Doc
text (String -> Doc) -> (Trigger -> String) -> Trigger -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trigger -> String
forall a. Show a => a -> String
show 

instance PPrint a => PPrint (Triggered a) where 
  pprintTidy :: Tidy -> Triggered a -> Doc
pprintTidy Tidy
k (TR Trigger
t a
x) = Doc -> Doc
parens (Tidy -> Trigger -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Trigger
t Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> Tidy -> a -> Doc
forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
x)

noTrigger :: e -> Triggered e
noTrigger :: e -> Triggered e
noTrigger = Trigger -> e -> Triggered e
forall a. Trigger -> a -> Triggered a
TR Trigger
NoTrigger

defaultTrigger :: e -> Triggered e
defaultTrigger :: e -> Triggered e
defaultTrigger = Trigger -> e -> Triggered e
forall a. Trigger -> a -> Triggered a
TR Trigger
LeftHandSide

makeTriggers :: Triggered Expr -> [Expr]
makeTriggers :: Triggered Expr -> [Expr]
makeTriggers (TR Trigger
LeftHandSide Expr
e) = [Expr -> Expr
getLeftHandSide Expr
e]
makeTriggers (TR Trigger
NoTrigger    Expr
_) = String -> [Expr]
forall a. (?callStack::CallStack) => String -> a
errorstar String
"makeTriggers on NoTrigger"


getLeftHandSide :: Expr -> Expr
getLeftHandSide :: Expr -> Expr
getLeftHandSide (ECst Expr
e Sort
_)
  = Expr -> Expr
getLeftHandSide Expr
e
getLeftHandSide (PAll [(Symbol, Sort)]
_ Expr
e)
  = Expr -> Expr
getLeftHandSide Expr
e
getLeftHandSide (PExist [(Symbol, Sort)]
_ Expr
e)
  = Expr -> Expr
getLeftHandSide Expr
e
getLeftHandSide (PAtom Brel
eq Expr
lhs Expr
_)
  | Brel
eq Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
eq Brel -> Brel -> Bool
forall a. Eq a => a -> a -> Bool
== Brel
Ueq
  = Expr
lhs
getLeftHandSide (PIff Expr
lhs Expr
_)
  = Expr
lhs
getLeftHandSide Expr
_
 = Expr
defaltPatter

-- NV TODO find out a valid, default pattern that does not instantiate the axiom
defaltPatter :: Expr
defaltPatter :: Expr
defaltPatter = Expr
PFalse

instance B.Binary Trigger
instance NFData   Trigger

instance (B.Binary a) => B.Binary (Triggered a)
instance (NFData a)   => NFData   (Triggered a)