content: {-# LANGUAGE Arrows #-}
  {-# LANGUAGE DeriveAnyClass #-}
  {-# LANGUAGE DeriveGeneric #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE ImplicitParams #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
  module TestPrograms where
  
  import           Prelude hiding (lookup,Bounded,Bool(..),fail,not,and)
  
  import           Control.Arrow
  import           Control.Arrow.Fix as F
  import           Control.Arrow.Fix.Cache
  import           Control.Arrow.Fix.Stack
  import           Control.Arrow.Order hiding (bottom)
  
  import           Data.Boolean(Logic(..))
  import           Data.Abstract.Boolean(Bool(..))
  import           Data.Abstract.InfiniteNumbers as Inf
  import           Data.Abstract.Interval (Interval)
  import qualified Data.Abstract.Interval as I
  import           Data.Abstract.Terminating
  
  import           Data.Metric (Metric,Product)
  import qualified Data.Metric as M
  import           Data.Order
  import           Data.Hashable
  import           Data.Profunctor
  
  import           Prettyprinter
  
  import           GHC.Generics
  
  fib :: Arr IV IV
  fib = fix $ \f ->
    ifLowerThan 0
      (proc _ -> returnA -< I.Interval 0 0)
      (ifLowerThan 1 (proc _ -> returnA -< I.Interval 1 1)
                     (proc n -> do
                        x <- f -< n - I.Interval 1 1
                        y <- f -< n - I.Interval 2 2
                        returnA -< x + y))
  {-# INLINE fib #-}
  
  fact :: Arr IV IV
  fact = fix $ \f ->
    ifLowerThan 1 (proc _ -> returnA -< iv 1 1)
                  (proc n -> do x <- f -< (n - iv 1 1)
                                returnA -< n * x)
  {-# INLINE fact #-}
  
  ackermann :: Arr (IV,IV) IV
  ackermann = fix $ \f -> proc (m,n) ->
    ifLowerThan 0
      (proc _ -> returnA -< n + iv 1 1)
      (proc m' -> ifLowerThan 0
                    (proc _ -> f -< (m'- iv 1 1, iv 1 1))
                    (proc n' -> do x <- f -< (m,n'-iv 1 1)
                                   f -< (m'- iv 1 1, x)) -<< n)
      -<< m
  {-# INLINE ackermann #-}
  
  data EvenOdd = Even | Odd deriving (Eq,Generic,Show,Hashable)
  instance Pretty EvenOdd where pretty = viaShow
  instance PreOrd EvenOdd where e1 ⊑ e2 = e1 == e2
  
  evenOdd :: Arr (EvenOdd,IV) Bool
  evenOdd = fix $ \f -> proc (e,x) -> case e of
    Even -> ifLowerThan 0 (proc _ -> returnA -< true)
                          (ifLowerThan 1 (proc _ -> returnA -< false)
                                         (proc x -> f -< (Odd,x-I.Interval 1 1))) -< x
    Odd -> ifLowerThan 0 (proc _ -> returnA -< false)
                          (ifLowerThan 1 (proc _ -> returnA -< true)
                                         (proc x -> f -< (Even,x-I.Interval 1 1))) -< x
  {-# INLINE evenOdd #-}
  
  diverge :: Arr Int IV
  diverge = fix $ \f -> proc n -> case n of
    0 -> f -< 0
    _ -> f -< (n-1)
  {-# INLINE diverge #-}
  
  data Fun = Main | F | G Bool Bool | H Bool | HF deriving (Eq,Show,Generic,Hashable)
  instance Pretty Fun where pretty = viaShow
  
  -- | Example program that demonstrates unsoundness of a fixpoint algorithm without a stack.
  -- Pretty printed the program looks like this:
  -- main = g(f(x),f(x))
  -- f(x) = h(f(x)) ⊔ c
  unsoundExample :: Arr Fun Bool
  unsoundExample = fix $ \call -> proc fun -> case fun of
    Main -> do
      x <- call -< F
      y <- call -< F
      call -< G x y
    F -> (call -< HF) <⊔> (returnA -< c)
    G x y -> returnA -< y `implies` x
    H x -> returnA -< not x
    HF -> do
      y <- call -< F
      call -< H y
    where
      c = True
  
  type Arr x y = forall c.
                 (?fixpointAlgorithm :: (Fix (c x y) -> Fix (c x y)) -> Fix (c x y),
                  ArrowChoice c, Profunctor c, ArrowApply c, ArrowComplete y c, ArrowFix (c x y))
                => c x y
  newtype Strat x y =
    Strat { getStrat :: forall c.
                      ( ArrowChoice c
                      , Profunctor c
                      , ArrowStack x c
                      , ArrowStackDepth c
                      , ArrowStackElements x c
                      , ArrowCache x (Terminating y) c
                      )
                     => FixpointCombinator c x (Terminating y)
          }
  type IV = Interval (InfiniteNumber Int)
  
  iv :: InfiniteNumber Int -> InfiniteNumber Int -> IV
  iv = I.Interval
  {-# INLINE iv #-}
  
  ifLowerThan :: (Num n, Ord n, ArrowChoice c, ArrowComplete x c) => n -> c (Interval n) x -> c (Interval n) x -> c (Interval n) x
  ifLowerThan l f g = proc x -> case x of
    I.Interval m n
      | n <= l -> f -< x
      | l < m -> g -< x
      | m <= l && l+1 <= n -> (f -< I.Interval m l) <⊔> (g -< I.Interval (l+1) n)
      | otherwise -> f -< I.Interval m l
  {-# INLINABLE ifLowerThan #-}
  
  euclid :: Metric IV (Product (InfiniteNumber Int) (InfiniteNumber Int))
  euclid = I.metric (Inf.metric M.euclid)
  {-# INLINE euclid #-}
  
  