{-# 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 (Triggered a -> Triggered a -> Bool
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
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, 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
<$ :: forall a b. a -> Triggered b -> Triggered a
$c<$ :: forall a b. a -> Triggered b -> Triggered a
fmap :: forall a b. (a -> b) -> Triggered a -> Triggered b
$cfmap :: forall a b. (a -> b) -> Triggered a -> Triggered b
Functor, 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
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
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. 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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k Trigger
t Doc -> Doc -> Doc
<+> String -> Doc
text String
":" Doc -> Doc -> Doc
<+> forall a. PPrint a => Tidy -> a -> Doc
pprintTidy Tidy
k a
x)

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

defaultTrigger :: e -> Triggered e
defaultTrigger :: forall e. e -> Triggered e
defaultTrigger = 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
_) = 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 forall a. Eq a => a -> a -> Bool
== Brel
Eq Bool -> Bool -> Bool
|| Brel
eq 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 S.Store Trigger
instance NFData   Trigger

instance (S.Store a) => S.Store (Triggered a)
instance (NFData a)   => NFData   (Triggered a)