{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module Calculus.Abstraction.DeBruijn.Generalized where

import Control.Applicative (Applicative(..))
import Control.Monad
import Control.Monad.Trans.Class (MonadTrans(..))
import Data.Bool (Bool(..))
import Data.Eq (Eq(..))
import Data.Foldable (Foldable(..))
import Data.Function (($), (.))
import Data.Function (on)
import Data.Maybe (Maybe(..))
import Data.Ord (Ord(..), Ordering(..))
import Data.String (IsString(..), String)
import Data.Text (Text)
import Data.Text.Buildable (Buildable(..))
import Data.Traversable (Traversable(..))
import Prelude (Int)
import Text.Show (Show(..), ShowS, showChar, showParen, showString)

-- * Type 'Abstraction'
-- | 'Abstraction' @bound@ @expr@ @var@:
-- encodes an 'abstract'-ion
-- over an expression of type @expr@,
-- by segretating its variables between:
--
-- * /bound variables/ of type: @bound@,
-- * and /unbound variables/ (aka. /free variables/) of type: @var@.
--
-- Note that /unbound variables/ may later themselves be made /bound variables/
-- of an enclosing 'Abstraction', effectively encoding
-- /DeBruijn indices/ using Haskell’s /data constructors/,
-- that is, not like in a /traditional DeBruijn indexing/:
-- where an integer is used in each /bound variable/
-- to indicate which one of its enclosing 'Abstraction's is bounding it,
-- but by the nesting of 'Var_Free' data constructors.
-- As a side note, this is also different from the /DeBruijn indexing/
-- encoded at Haskell’s /type level/ by using @GADTs@
-- (done for instance in https://hackage.haskell.org/package/glambda ).
--
-- Moreover, /unbound variables/ are wrapped within a second level of expression
-- in order to improve the time complexity of /traditional DeBruijn indexing/
-- when 'unabstract'-ing (aka. /instantiating/)
-- (see 'Var' and instance 'MonadTrans' of 'Abstraction').
--
-- 'Abstraction' enables:
--
-- * /locally-nameless/ variables (nameless in 'Var_Bound', named in the deepest 'Var_Free');
-- * substitution of /bound variables/ in an expression using /DeBruijn indices/
--   (hence enabling capture-avoiding /β-reduction/
--   and reducing /α-equivalence/ to a structural equality (==));
-- * shifting /DeBruijn indices/ within an expression without traversing it
--   (hence generalizing and speeding up /traditional DeBruijn indices/);
-- * simultaneous substitution of several /bound variables/
--   (hence enabling expressions implementing recursive-@let@).
--
-- __Ressources:__
--
-- * /Bound/, Edward Kmett, 19 August 2013,
--   https://www.schoolofhaskell.com/user/edwardk/bound
newtype Abstraction bound expr var
 =      Abstraction (expr (Var bound (expr var)))
 deriving (Foldable, Functor, Traversable)
instance (Monad expr, Eq bound, Eq1 expr, Show bound)
 => Eq1 (Abstraction bound expr) where
	(==#) = (==#) `on` abstract_normalize
instance (Monad expr, Eq bound, Eq1 expr, Eq var, Show var, Show bound)
 => Eq (Abstraction bound expr var) where
	(==) = (==#)
instance (Monad expr, Ord bound, Ord1 expr, Show bound)
 => Ord1 (Abstraction bound expr) where
	compare1 = compare1 `on` abstract_normalize
instance (Monad expr, Ord bound, Ord1 expr, Ord var, Show var, Show bound)
 => Ord (Abstraction bound expr var) where
	compare = compare1
instance (Functor expr, Show bound, Show1 expr)
 => Show1 (Abstraction bound expr) where
	showsPrec1 d (Abstraction e) =
		showsUnaryWith "Abstraction" d $
			(Lift1 `fmap`) `fmap` e
instance (Functor expr, Show bound, Show1 expr, Show var)
 => Show (Abstraction bound expr var) where
	showsPrec = showsPrec1
instance Monad expr => Applicative (Abstraction bound expr) where
	pure  = return
	(<*>) = ap
-- | A 'Monad' instance capturing the notion of /variable substitution/,
-- used by 'unabstract' to decrement the /DeBruijn indices/.
instance Monad expr => Monad (Abstraction bound expr) where
	return = Abstraction . return . Var_Free . return
	Abstraction expr >>= f = Abstraction $ expr >>= \var ->
		case var of
		 Var_Bound bound -> return (Var_Bound bound)
		 Var_Free  e     -> e >>= (\(Abstraction ex) -> ex) . f
instance MonadTrans (Abstraction bound) where
	lift = Abstraction . return . Var_Free
-- | 'Monad_Module_Left' instance capturing the notion
-- of /variable substitution/ with /capture-avoiding/.
instance Monad_Module_Left (Abstraction bound) where
	l >>>= f = l >>= lift . f

-- | WARNING: 'abstract' 'fmap'-s the given expression,
-- thus repetitive 'abstract'-ings have a quadratic time-complexity.
abstract
 :: Monad expr
 => (var -> Maybe bound)
 -> expr var
 -> Abstraction bound expr var
abstract f = Abstraction . fmap (\var ->
	case f var of
	 Nothing -> Var_Free (return var)
	 Just b  -> Var_Bound b)

unabstract
 :: Monad expr
 => (bound -> expr var)
 -> Abstraction bound expr var
 -> expr var
unabstract unbound (Abstraction ex) = ex >>= \var ->
	case var of
	 Var_Bound b -> unbound b
	 Var_Free  v -> v

-- | @'abstract_normalize'@ normalize
-- the possible placements of 'Var_Free' in 'Abstraction'
-- by moving them all to the leaves of the 'abstract'-ed expression.
--
-- This gives /traditional DeBruijn indices/ for /bound variables/.
abstract_normalize
 :: Monad expr
 => Abstraction bound expr var
 -> expr (Var bound var)
abstract_normalize (Abstraction expr) = expr >>= \var ->
	case var of
	 Var_Bound bound -> return $ Var_Bound bound
	 Var_Free  e     -> Var_Free `fmap`{-on var of expr-} e

-- | Convert from /traditional DeBruijn indices/
-- to /generalized DeBruijn indices/,
-- by wrapping all the leaves within the 'Monad'
-- of the given expression.
--
-- This requires a full traversal of the given expression.
abstract_generalize
 :: Monad expr
 => expr (Var bound var)
 -> Abstraction bound expr var
abstract_generalize = Abstraction .
	((return{-of expr-}
	 `fmap`{-on var of Var-})
	 `fmap`{-on var of expr-})

-- ** Class 'Monad_Module_Left'
-- | Like ('>>=') but whose 'Monad' is within a wrapping type @left@
-- (aka. /left module over a monad/).
--
-- __Laws:__
--
-- ('>>>=') should satisfy the following equations
-- in order to be used within a 'Monad' instance:
--
-- @
-- ('>>>=' 'return') = id
-- ('>>>=' (('>>=' g) . f)) = ('>>>=' f) . ('>>>=' g)
-- @
--
-- If @left@ has a 'MonadTrans' instance, then:
--
-- @
-- ('>>>=' f) = ('>>=' ('lift' . f))
-- @
--
-- which implies the above equations,
-- see 'MonadTrans' instance of ('Abstraction' @bound@).
--
-- __Uses:__
--
-- * Useful for expression constructors containing 'Abstraction' data.
--
-- __Ressources:__
--
-- * André Hirschowitz, Marco Maggesi, /Modules over monads and initial semantics/.
--   Information and Computation 208 (2010), pp. 545-564,
--   http://www.sciencedirect.com/science/article/pii/S0890540109002405
class Monad_Module_Left left where
  (>>>=) :: Monad expr
         => left expr var
         -> (var -> expr bound)
         -> left expr bound
infixl 1 >>>=

-- ** Type 'Var'

-- | 'Var' @bound@ @var@: a variable segregating between:
--
-- * 'Var_Bound', containing data of type @bound@,
--   considered /bound/ by the first enclosing 'Abstraction',
--   hence playing the role of a @Zero@ in /DeBruijn indexing/ terminology.
--   
--   Note that the presence of this @bound@ enables the substitution
--   of a 'Var_Bound' by different values,
--   which is used to keep the 'Var_Name' given in the source code,
--   (note that it could also be used to implement a @recursive-let@).
--
-- * 'Var_Free', containing data of type @var@,
--   considered /free/ with respect to the first enclosing 'Abstraction',
--   hence playing the role of a @Succ@ in /DeBruijn indexing/ terminology.
--   
--   Note that @var@ is not constrained to be itself a 'Var',
--   this in order to make it possible in 'Abstraction'
--   to insert @expr@ in between the @Succ@ nesting,
--   which optimizes the /DeBruijn indexing/ when 'unabstract'-ing,
--   by avoiding to traverse ('fmap') an @expr@ to @Succ@ its variables
--   (see instance 'MonadTrans' for 'Abstraction').
data Var bound var
 =   Var_Bound bound -- ^ @Zero@
 |   Var_Free  var -- ^ @Succ@
 deriving (Eq, Foldable, Functor, Ord, Show, Traversable)
instance (Buildable bound, Buildable var) => Buildable (Var bound var) where
	build var =
		case var of
		 Var_Bound b -> build b
		 Var_Free  f -> build f

-- | A convenient operator for 'abstract'-ing.
(=?) :: Eq a => a -> a -> Maybe (Suggest a)
(=?) x y = if x == y then Just (Suggest x) else Nothing

-- | A convenient type synonym for clarity.
type Var_Name = Text

-- | A convenient class synonym for brievety.
class (Show var, Buildable var) => Variable var
instance Variable Var_Name
instance (Variable bound, Variable var) => Variable (Var bound var)
instance Variable var => Variable (Suggest var)

-- * Higher-order @Prelude@ classes

-- ** Class 'Eq1'
-- | Lift the 'Eq' class to unary type constructors,
-- to avoid the @UndecidableInstances@ language extension.
--
-- __Ressources:__
--
-- * /Simulating Quantified Class Constraints/, Valery Trifonov, 2003,
--   http://flint.cs.yale.edu/trifonov/papers/sqcc.pdf
-- * /prelude-extras/, Edward Kmett, 2011,
--   https://hackage.haskell.org/package/prelude-extras
-- * /base/ 'Data.Functor.Classes', Ross Paterson, 2013,
--   https://hackage.haskell.org/package/base/docs/Data-Functor-Classes.html
class Eq1 f where
	(==#) :: (Eq a, Show a) => f a -> f a -> Bool

class Eq1 f => Ord1 f where
	compare1 :: Ord a => f a -> f a -> Ordering

-- ** Class 'Show1'
-- | Lift the 'Show' class to unary type constructors,
-- to avoid the @UndecidableInstances@ language extension.
class Show1 f where
	showsPrec1 :: Show a => Int -> f a -> ShowS

showsUnaryWith :: (Show1 f, Show a) => String -> Int -> f a -> ShowS
showsUnaryWith name d x =
	showParen (d > 10) $
	showString name . showChar ' ' . showsPrec1 11 x

-- ** Type 'Lift1'
-- | Lift the 'Lift' class to unary type constructors,
-- to avoid the @UndecidableInstances@ language extension.
newtype Lift1 f a = Lift1 { lower1 :: f a }
	deriving (Functor, Foldable, Traversable, Eq1, Ord1, Show1)
instance (Eq1 f, Eq a, Show a) => Eq   (Lift1 f a) where (==) = (==#)
instance (Ord1 f, Ord a, Show a) => Ord (Lift1 f a) where compare = compare1
instance (Show1 f, Show a) => Show (Lift1 f a) where showsPrec = showsPrec1

-- ** Type 'Suggest'

-- | A convenient wrapper to include data ignored by /α-equivalence/.
newtype Suggest n
 =      Suggest n
 deriving (Functor, Show)
-- | Always return 'True', in order to be transparent for 'alpha_equiv'.
instance Eq (Suggest n) where
	_ == _ = True
instance Ord (Suggest n) where
	_ `compare` _ = EQ
instance Buildable var
 =>      Buildable (Suggest var) where
	build (Suggest var) = build var
instance IsString x => IsString (Suggest x) where
	fromString = Suggest . fromString