    {-# LANGUAGE ScopedTypeVariables,
                 FlexibleInstances, UndecidableInstances #-}

    -- |
    -- Module      :  Test.ChasingBottoms.Approx
    -- Copyright   :  (c) Nils Anders Danielsson 2004-2022
    -- License     :  See the file LICENCE.
    --
    -- Maintainer  :  http://www.cse.chalmers.se/~nad/
    -- Stability   :  experimental
    -- Portability :  non-portable (GHC-specific)
    --

    module Test.ChasingBottoms.Approx
      ( Approx(..)
      ) where

    import Test.ChasingBottoms.Nat
    import Data.Function
    import Data.Generics
    import qualified Data.List as List

    {-|
    'Approx' is a class for approximation functions as described
    in The generic approximation lemma, Graham Hutton and Jeremy
    Gibbons, Information Processing Letters, 79(4):197-201, Elsevier
    Science, August 2001, <http://www.cs.nott.ac.uk/~gmh/bib.html>.

    Instances are provided for all members of the 'Data' type class. Due
    to the limitations of the "Data.Generics" approach to generic
    programming, which is not really aimed at this kind of application,
    the implementation is only guaranteed to perform correctly, with
    respect to the paper (and modulo any bugs), on non-mutually-recursive
    sum-of-products datatypes. In particular, nested and mutually
    recursive types are not handled correctly with respect to the
    paper. The specification below is correct, though (if we assume that
    the 'Data' instances are well-behaved).

    In practice the 'approxAll' function can probably be more useful than
    'approx'. It traverses down /all/ subterms, and it should be possible
    to prove a variant of the approximation lemma which 'approxAll'
    satisfies.
    -}

    class Approx a where
      -- | @'approxAll' n x@ traverses @n@ levels down in @x@ and replaces all
      -- values at that level with bottoms.
      approxAll :: Nat -> a -> a

      -- | 'approx' works like 'approxAll', but the traversal and
      -- replacement is only performed at subterms of the same monomorphic
      -- type as the original term. For polynomial datatypes this is
      -- exactly what the version of @approx@ described in the paper above
      -- does.
      approx :: Nat -> a -> a

    instance Data a => Approx a where
      approxAll :: Nat -> a -> a
    approxAll = Nat -> a -> a
    forall a. Data a => Nat -> a -> a
    approxAllGen
      approx :: Nat -> a -> a
    approx    = Nat -> a -> a
    forall a. Data a => Nat -> a -> a
    approxGen

    -- From The generic approximation lemma (Hutton, Gibbons):

    -- Generic definition for arbitrary datatype \mu F:
    --   approx (n+1) = in . F (approx n) . out

    -- Approximation lemma (valid if F is locally continuous),
    -- for x, y :: \mu F:
    --   x = y  <=>  forall n in Nat corresponding to natural numbers.
    --                  approx n x = approx n y

    approxGen :: Data a => Nat -> a -> a
    approxGen :: forall a. Data a => Nat -> a -> a
    approxGen Nat
    n | Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0    = [Char] -> a -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "approx 0 = _|_"
                | Bool
    otherwise =
      \(a
    x :: a) -> (forall b. Data b => b -> b) -> a -> a
    forall a. Data a => (forall b. Data b => b -> b) -> a -> a
    gmapT ((a -> a) -> b -> b
    forall a b. (Typeable a, Typeable b) => (b -> b) -> a -> a
    mkT (Nat -> a -> a
    forall a. Data a => Nat -> a -> a
    approxGen (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n) :: a -> a)) a
    x

    -- We use mkT to only recurse on the original type. This solution is
    -- actually rather nice! But sadly it doesn't work for nested or
    -- mutually recursive types...

    -- Note that the function is defined in the \n -> \x -> style, not
    -- \n x -> which would mean something subtly different.

    ------------------------------------------------------------------------

    -- Recurses on everything...

    approxAllGen :: Data a => Nat -> a -> a
    approxAllGen :: forall a. Data a => Nat -> a -> a
    approxAllGen Nat
    n | Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0    = [Char] -> a -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "approx 0 = _|_"
                   | Bool
    otherwise = \a
    x -> (forall b. Data b => b -> b) -> a -> a
    forall a. Data a => (forall b. Data b => b -> b) -> a -> a
    gmapT (Nat -> b -> b
    forall a. Data a => Nat -> a -> a
    approxAllGen (Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n)) a
    x

    ------------------------------------------------------------------------

    -- Behaves exactly like approxGen. (?)

    approxGen' :: Data a => Nat -> a -> a
    approxGen' :: forall a. Data a => Nat -> a -> a
    approxGen' Nat
    n
      | Nat
    n Nat -> Nat -> Bool
    forall a. Eq a => a -> a -> Bool
    == Nat
    0    = [Char] -> a -> a
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "approx 0 = _|_"
      | Bool
    otherwise = \a
    x ->
         let d :: DataType
    d = a -> DataType
    forall a. Data a => a -> DataType
    dataTypeOf a
    x
             n' :: Nat
    n' = Nat -> Nat
    forall a. Enum a => a -> a
    pred Nat
    n
             fun :: a -> a
    fun a
    childTerm = if a -> DataType
    forall a. Data a => a -> DataType
    dataTypeOf a
    childTerm DataType -> DataType -> Bool
    === DataType
    d then
                               Nat -> a -> a
    forall a. Data a => Nat -> a -> a
    approxGen' Nat
    n' a
    childTerm
                              else
                               a
    childTerm
         in (forall b. Data b => b -> b) -> a -> a
    forall a. Data a => (forall b. Data b => b -> b) -> a -> a
    gmapT b -> b
    forall b. Data b => b -> b
    fun a
    x
        where === :: DataType -> DataType -> Bool
    (===) = DataRep -> DataRep -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (DataRep -> DataRep -> Bool)
    -> (DataType -> DataRep) -> DataType -> DataType -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` DataType -> DataRep
    dataTypeRep