{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.LOL.Symantic.Expr.Common where

import Data.Proxy (Proxy(..))
import GHC.Prim (Constraint)
import Data.Text (Text)
import Data.Peano

import Language.LOL.Symantic.AST
import Language.LOL.Symantic.Type

-- * Class 'Sym_from'

class Sym_from raw (ex:: *) where
	sym_from
	 :: forall hs ret
	 .  Proxy ex
	 -- ^ Select the 'Sym_from' instance for the expression @ex@.
	 -> Context (Var (Root_of_Expr ex)) hs
	 -- ^ The bound variables and their types held in the heterogeneous list @hs@
	 -- (types being constructed within: 'Type_Root_of_Expr' @ex@.
	 -> raw
	 -- ^ The input data to parse.
	 -> ( forall h
	    .  Type_Root_of_Expr ex h
	    -- The type of the parsed symantic expression.
	    -> Forall_Repr_with_Context ex hs h
	    -- The parsed symantic expression
	    -- (still abstracted by a 'Context' at this point).
	    -> Either (Maybe (Error_of_Expr raw (Root_of_Expr ex))) ret
	    )
	 -- ^ The accumulating continuation.
	 ->    Either (Maybe (Error_of_Expr raw (Root_of_Expr ex))) ret

-- ** Type 'Context'

-- | GADT for a typing context,
-- accumulating an @item@ at each lambda;
-- used to accumulate object-types of lambda variables in 'Sym_from'
-- or host-terms of lambda variables in 'Repr_Host'.
data Context :: (* -> *) -> [*] -> * where
	Context_Empty :: Context item '[]
	Context_Next  :: item h -> Context item hs -> Context item (h ': hs)
infixr 5 `Context_Next`

-- ** Type 'Var'
-- | Join a name and a type;
-- used to handle lambda variables by name
-- (instead of DeBruijn indices for instance).
data Var ex h
 =   Var Var_Name (Type_Root_of_Expr ex h)
type Var_Name = Text

-- ** Type 'Forall_Repr_with_Context'
-- | A data type embedding a universal quantification over @repr@
-- to construct a symantic expression polymorphic enough to stay
-- interpretable by different interpreters;
-- moreover the symantic expression is abstracted by a 'Context'
-- built at parsing time.
data Forall_Repr_with_Context ex hs h
 =   Forall_Repr_with_Context
 (   forall repr. ( Sym_of_Expr ex repr
                  , Sym_of_Expr (Root_of_Expr ex) repr
                  ) => Context repr hs -> repr h )

-- *** Type 'Forall_Repr'
data Forall_Repr ex h
 =   Forall_Repr
 { unForall_Repr :: forall repr
                 .  Sym_of_Expr ex repr
                 => repr h }

-- ** Type 'Root_of_Expr'
-- | The root expression, closing an expression with itself.
type family Root_of_Expr (ex:: *) :: *

-- ** Type 'Sym_of_Expr'
-- | The symantic of an expression.
type family Sym_of_Expr (ex:: *) (repr:: * -> *) :: Constraint

-- ** Type 'Error_of_Expr'
-- | The error(s) of an expression.
type family Error_of_Expr (raw:: *) (ex:: *) :: *

-- ** Type 'Type_of_Expr'
-- | The type of an expression, parameterized by a root type.
type family Type_of_Expr (ex:: *) :: {-root-}(* -> *) -> {-h-}* -> *

-- ** Type 'Type_Root_of_Expr'
type Type_Root_of_Expr ex
 =   Type_Root (Type_of_Expr (Root_of_Expr ex))

-- * Type 'Expr_Root'
-- | The root expression, passing itself as parameter to the given expression.
newtype Expr_Root (ex:: * -> *)
 =      Expr_Root (ex (Expr_Root ex))
type instance Root_of_Expr (Expr_Root ex) = Expr_Root ex
type instance Type_of_Expr (Expr_Root ex)
 =            Type_of_Expr (ex (Expr_Root ex))
 -- NOTE: require UndecidableInstances.
type instance Error_of_Expr raw (Expr_Root ex)
 =            Error_Expr_Cons (Error_Expr_Read raw)
                             (Error_of_Expr raw (ex (Expr_Root ex)))
 -- NOTE: require UndecidableInstances.
type instance Sym_of_Expr (Expr_Root ex) repr
 =            Sym_of_Expr (ex (Expr_Root ex)) repr
 -- NOTE: require UndecidableInstances.
instance -- Sym_from
 ( Sym_from raw (ex (Expr_Root ex))
 , Root_of_Expr (ex (Expr_Root ex)) ~ Expr_Root ex
 ) => Sym_from raw (Expr_Root ex) where
	sym_from _px_ex ctx raw k =
		sym_from (Proxy::Proxy (ex (Expr_Root ex)))
		 ctx raw $ \ty (Forall_Repr_with_Context repr) ->
			k ty (Forall_Repr_with_Context repr)

-- ** Class 'Expr_Root_Lift'
-- | Lift a given type to a given root type.
class Expr_Root_Lift ex root where
	expr_root_lift :: ex root -> root
instance
 Expr_Lift ex root =>
 Expr_Root_Lift ex (Expr_Root root) where
	expr_root_lift = Expr_Root . expr_lift


-- * Type 'Expr_Cons'
-- | Combine two types into one.
data Expr_Cons curr next (root:: *)
 =   Expr_Curr (curr root)
 |   Expr_Next (next root)
type instance Root_of_Expr (Expr_Cons curr next root) = root
type instance Type_of_Expr (Expr_Cons curr next root)
 = Type_Cons (Type_of_Expr (curr root))
             (Type_of_Expr (next root))
type instance Error_of_Expr raw (Expr_Cons curr next root)
 = Error_Expr_Cons (Error_of_Expr raw (curr root))
                   (Error_of_Expr raw (next root))
type instance Sym_of_Expr (Expr_Cons curr next root) repr
 = ( Sym_of_Expr (curr root) repr
   , Sym_of_Expr (next root) repr
   )
instance -- Sym_from
 ( Sym_from raw (curr root)
 , Sym_from raw (next root)
 , Root_of_Expr (curr root) ~ root
 , Root_of_Expr (next root) ~ root
 ) => Sym_from raw (Expr_Cons curr next root) where
	sym_from _px_ex ctx raw k =
		case sym_from (Proxy::Proxy (curr root)) ctx raw $
		 \ty (Forall_Repr_with_Context repr) ->
			Right $ k ty (Forall_Repr_with_Context repr) of
		 Right ret -> ret
		 Left Nothing -> sym_from (Proxy::Proxy (next root)) ctx raw $
			 \ty (Forall_Repr_with_Context repr) ->
				k ty (Forall_Repr_with_Context repr)
		 Left err -> Left err

-- ** Type 'Peano_of_Expr'
-- | Return a 'Peano' number derived from the location
-- of a given extension within a given extension stack.
type family Peano_of_Expr
 (ex::  * -> *)
 (exs:: * -> *) :: Peano where
	Peano_of_Expr ex ex                       = 'Zero
	Peano_of_Expr ex (Expr_Cons ex next)      = 'Zero
	Peano_of_Expr other (Expr_Cons curr next) = 'Succ (Peano_of_Expr other next)

-- ** Type 'Expr_Lift'
-- | Apply 'Peano_of_Expr' on 'Expr_LiftN'.
type Expr_Lift ex exs
 =   Expr_LiftN (Peano_of_Expr ex exs) ex exs

-- *** Class 'Expr_LiftN'
-- | Construct the sequence of 'Expr_Curr' and 'Expr_Next'
-- lifting a given extension to the top of a given extension stack.
class Expr_LiftN (n::Peano) ex exs where
	expr_liftN :: forall (root:: *). Proxy n -> ex root -> exs root
instance Expr_LiftN 'Zero curr curr where
	expr_liftN _ = id
instance Expr_LiftN 'Zero curr (Expr_Cons curr next) where
	expr_liftN _ = Expr_Curr
instance
 Expr_LiftN n other next =>
 Expr_LiftN ('Succ n) other (Expr_Cons curr next) where
	expr_liftN _ = Expr_Next . expr_liftN (Proxy::Proxy n)

-- | Lift an expression within an expression stack to its top,
-- using a 'Peano' number calculated by 'Peano_of_Expr'
-- to avoid the overlapping of the 'Expr_LiftN' instances.
expr_lift
 :: forall ex exs (root:: *).
 Expr_Lift ex exs =>
 ex root -> exs root
expr_lift = expr_liftN (Proxy::Proxy (Peano_of_Expr ex exs))

-- ** Type 'Expr_Unlift'
-- | Apply 'Peano_of_Expr' on 'Expr_UnliftN'.
type Expr_Unlift ex exs
 =   Expr_UnliftN (Peano_of_Expr ex exs) ex exs

-- *** Class 'Expr_UnliftN'
-- | Deconstruct a sequence of 'Expr_Curr' and 'Expr_Next'
-- trying to unlift a given extension out of a given extension stack.
class Expr_UnliftN (n::Peano) ex exs where
	expr_unliftN :: forall (root:: *). Proxy n -> exs root -> Maybe (ex root)
instance Expr_UnliftN 'Zero curr curr where
	expr_unliftN _ = Just
instance Expr_UnliftN 'Zero curr (Expr_Cons curr next) where
	expr_unliftN _ (Expr_Curr x) = Just x
	expr_unliftN _ (Expr_Next _) = Nothing
instance
 Expr_UnliftN n other next =>
 Expr_UnliftN ('Succ n) other (Expr_Cons curr next) where
	expr_unliftN _ (Expr_Next x) = expr_unliftN (Proxy::Proxy n) x
	expr_unliftN _ (Expr_Curr _) = Nothing

-- | Unlift an expression within an expression stack,
-- using a 'Peano' number calculated by 'Peano_of_Expr'
-- to avoid the overlapping of the 'Expr_UnliftN' instances.
expr_unlift
 :: forall ex exs (root:: *).
 Expr_Unlift ex exs =>
 exs root -> Maybe (ex root)
expr_unlift = expr_unliftN (Proxy::Proxy (Peano_of_Expr ex exs))

-- * Type 'Error_Expr_Cons'
-- | Combine two error expressions into one.
data Error_Expr_Cons curr next
 =   Error_Expr_Curr curr
 |   Error_Expr_Next next
 deriving (Eq, Show)

-- ** Class 'Error_Expr_LiftN'
-- | Construct the sequence of 'Error_Expr_Curr' and 'Error_Expr_Next'
-- lifting a given error type to the top of a given error type stack.
class Error_Expr_LiftN (n::Peano) err errs where
	error_expr_liftN :: Proxy n -> err -> errs
instance Error_Expr_LiftN 'Zero curr curr where
	error_expr_liftN _ = id
instance Error_Expr_LiftN 'Zero curr (Error_Expr_Cons curr next) where
	error_expr_liftN _ = Error_Expr_Curr
instance
 Error_Expr_LiftN n other next =>
 Error_Expr_LiftN ('Succ n) other (Error_Expr_Cons curr next) where
	error_expr_liftN _ = Error_Expr_Next . error_expr_liftN (Proxy::Proxy n)

-- | Lift an error type within a type stack to its top,
-- using a 'Peano' number calculated by 'Peano_of_Error_Expr'
-- to avoid the overlapping of the 'Error_Expr_LiftN' instances.
error_expr_lift
 :: forall err errs.
 Error_Expr_Lift err errs =>
 err -> errs
error_expr_lift = error_expr_liftN (Proxy::Proxy (Peano_of_Error_Expr err errs))

type Error_Expr_Lift err errs
 =   Error_Expr_LiftN (Peano_of_Error_Expr err errs) err errs
-- | Return a 'Peano' number derived from the location
-- of a given error type within a given error type stack.
type family Peano_of_Error_Expr (err:: *) (errs:: *) :: Peano where
	Peano_of_Error_Expr err err                           = 'Zero
	Peano_of_Error_Expr err (Error_Expr_Cons err next)    = 'Zero
	Peano_of_Error_Expr other (Error_Expr_Cons curr next) = 'Succ (Peano_of_Error_Expr other next)

-- ** Type 'Error_Expr_Read'
data Error_Expr_Read raw
 =   Error_Expr_Read Error_Read raw
 deriving (Eq, Show)