content: {-# LANGUAGE Arrows #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PartialTypeSignatures #-}
  {-# LANGUAGE QuantifiedConstraints #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE UndecidableInstances #-}
  {-# OPTIONS_GHC -fsimpl-tick-factor=200 -fno-warn-redundant-constraints -fno-warn-partial-type-signatures #-}
  module ContextSensitivitySpec where
  
  import           Prelude hiding (lookup,Bounded,fail,Bool)
  
  import           TestPrograms hiding (Fun(..))
  
  import           Control.Monad(forM_)
  import           Control.Arrow
  import           Control.Arrow.Fix as F
  import           Control.Arrow.Fix.Context(ArrowContext,callsiteSensitive)
  import           Control.Arrow.Fix.Chaotic
  import qualified Control.Arrow.Trans as Arrow
  import           Control.Arrow.Transformer.Abstract.Terminating
  import           Control.Arrow.Transformer.Abstract.Fix
  import           Control.Arrow.Transformer.Abstract.Fix.Trace
  import           Control.Arrow.Transformer.Abstract.Fix.Component
  import           Control.Arrow.Transformer.Abstract.Fix.Stack
  import           Control.Arrow.Transformer.Abstract.Fix.Cache.Immutable as Cache hiding (Widening)
  import           Control.Arrow.Transformer.Abstract.Fix.Context as Ctx
  import           Control.Arrow.Transformer.Abstract.Fix.CallSite as CallSite
  
  import qualified Data.Abstract.Boolean as Abs
  import           Data.Abstract.Terminating (Terminating)
  import qualified Data.Abstract.Terminating as T
  import           Data.Abstract.Widening (Widening)
  import qualified Data.Abstract.Widening as W
  import           Data.Abstract.CallString
  
  import           Data.Boolean
  import           Data.Identifiable
  import           Data.Order
  import           Data.Hashable
  
  import           Prettyprinter
  
  import           GHC.Generics
  
  import           Test.Hspec
  
  main :: IO ()
  main = hspec spec
  
  spec :: Spec
  spec =
    -- do
    --describe "Parallel" (sharedSpec (\f -> snd . Arrow.run (toParallel f) (S.stackWidening ?stackWiden (S.parallel (T.widening ?widen)))))
    describe "Chaotic" $ do
      describe "inner component" $
        callsiteSpec $ \f a ->
          let ?contextWidening = ?widenA
              ?cacheWidening = T.widening ?widenB in
          let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . innermost) in
          snd $ Arrow.run (f :: ChaoticT _ _ _) a
      describe "outer component" $
        callsiteSpec $ \f a ->
          let ?contextWidening = ?widenA
              ?cacheWidening = T.widening ?widenB in
          let ?fixpointAlgorithm = fixpointAlgorithm (callsiteSensitive ?sensitivity fst . outermost) in
          snd $ Arrow.run (f :: ChaoticT _ _ _) a
  
  data Val = Num IV | Unit | Top deriving (Show,Eq,Generic,Hashable)
  instance Pretty Val where pretty = viaShow
  
  type Line = Int
  
  {-# INLINE callsiteSpec #-}
  callsiteSpec :: (forall lab a b.
                   (Pretty lab, Show lab, PreOrd lab, Identifiable lab,
                    Pretty a, Show a, PreOrd a, Identifiable a,
                    Pretty b, Show b, Complete b, Pretty (CallString lab),
                    ?sensitivity :: Int, ?widenA :: Widening a, ?widenB :: Widening b)
                  => Arr (lab,a) b -> (lab,a) -> Terminating b) -> Spec
  callsiteSpec run = do
    describe "diamond" $ do
      let diamond :: Arr ((Line,Fun),Val) Val
          diamond = fix $ \call -> proc ((_,fun),x) -> case fun of
            Main -> do
              call -< ((1,Fun1),Num (iv 1 1))
              call -< ((2,Fun2),Num (iv 2 2))
              call -< ((3,Fun1),Num (iv 3 3))
            Fun1 ->
              call -< ((4,Id),x)
            Fun2 ->
              call -< ((5,Id),x)
            Id ->
              returnA -< x
  
      let ?widenA = W.finite
      let ?widenB = W.finite
  
      it "context insensitive" $
        let ?sensitivity = 0 in
        run diamond ((0,Main),Unit) `shouldBe` return Top
  
      it "1-callsite sensitive" $
        let ?sensitivity = 1 in
        run diamond ((0,Main),Unit) `shouldBe` return (Num (iv 1 3))
  
      it "2-callsite sensitive" $
        let ?sensitivity = 2 in
        run diamond ((0,Main),Unit) `shouldBe` return (Num (iv 3 3))
  
    describe "mutual recursive functions" $ do
      let ?widenA = W.finite
      let ?widenB = W.finite
  
      let runTests :: (?sensitivity :: Int) => [(EvenOdd,Int,Abs.Bool)] -> IO ()
          runTests l = forM_ l $ \(eo,arg,res) ->
            run evenOdd (eo,iv (fromIntegral arg) (fromIntegral arg)) `shouldBe` return res
  
      it "context insensitive" $ do
        let ?sensitivity = 0
        runTests [
          (Even,1,false), (Odd,1,true),
          (Even,2,top),  (Odd,2,top)
          ]
  
      it "1-callsite sensitive" $ do
        let ?sensitivity = 1
        runTests [
          (Even,1,false), (Odd,1,true),
          (Even,2,true), (Odd,2,false),
          (Even,3,top) , (Odd,3,top)
          ]
  
      it "2-callsite sensitive" $ do
        let ?sensitivity = 2
        runTests [
          (Even,1,false), (Odd,1,true),
          (Even,2,true),  (Odd,2,false),
          (Even,3,false), (Odd,3,true),
          (Even,4,top),   (Odd,4,top)
          ]
  
  instance PreOrd Val where
    _ ⊑ Top = True
    Num x ⊑ Num y = x ⊑ y
    Unit ⊑ Unit = True
    _ ⊑ _ = False
  
  instance Complete Val where
    Num x ⊔ Num y = Num (x ⊔ y)
    Unit ⊔ Unit = Unit
    _ ⊔ _ = Top
  
  data Fun = Main | Fun1 | Fun2 | Id deriving (Show,Eq,Generic)
  instance Hashable Fun
  instance PreOrd Fun where
    e1 ⊑ e2 = e1 == e2
  instance Pretty Fun where
    pretty = viaShow
  
  type ChaoticT lab a b =
    TerminatingT
      (FixT
        (ComponentT Component (lab,a)
          (StackT Stack (lab,a)
            (CacheT Cache (lab,a) (Terminating b)
              (CallSiteT lab
                (ContextT (Ctx.Second Context) (CallString lab) (lab,a)
                  (->))))))) (lab,a) b
  