{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE NoImplicitPrelude #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
-- | Generalized DeBruijn abstraction
module Language.LOL.Calculus.Abstraction 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 (($), (.), 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)

-- | Aka. /instantiating/.
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