{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
module Language.Symantic.Type.Error where

import Data.Proxy
import Language.Symantic.Lib.Data.Peano
import Language.Symantic.Lib.Data.Bool

import Language.Symantic.Type.Root
import Language.Symantic.Type.Alt

-- * Type family 'Error_of_Type'
-- | Return the error type of a type.
type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
type instance Error_of_Type ast (Type_Root ty)
 = Error_Type_Alt (Error_Type ast)
                  (Error_of_Type ast (ty (Type_Root ty)))
type instance Error_of_Type ast (Type_Alt curr next root)
 = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
                         (Error_of_Type ast (next root))

-- ** Type family 'Error_of_Type_Alt'
-- | Remove 'No_Error_Type' type when building 'Error_of_Type'.
type family Error_of_Type_Alt ast curr next where
	Error_of_Type_Alt ast curr          No_Error_Type = curr
	Error_of_Type_Alt ast No_Error_Type next          = next
	Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next

-- * Type 'Error_Type_Alt'
-- | Error type making an alternative between two error types.
data Error_Type_Alt curr next
 =   Error_Type_Alt_Curr curr
 |   Error_Type_Alt_Next next
 deriving (Eq, Show)

-- ** Type 'Lift_Error_Type'
type Lift_Error_Type err errs
 =   Lift_Error_TypeP (Peano_of_Error_Type err errs) err errs

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

-- *** Class 'Lift_Error_TypeP'
-- | Lift a given error type to the top of a given error type stack including it,
-- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
class Lift_Error_TypeP (p:: *) err errs where
	lift_error_typeP :: Proxy p -> err -> errs
instance Lift_Error_TypeP Zero curr curr where
	lift_error_typeP _ = id
instance Lift_Error_TypeP Zero curr (Error_Type_Alt curr next) where
	lift_error_typeP _ = Error_Type_Alt_Curr
instance
 Lift_Error_TypeP p other next =>
 Lift_Error_TypeP (Succ p) other (Error_Type_Alt curr next) where
	lift_error_typeP _ = Error_Type_Alt_Next . lift_error_typeP (Proxy::Proxy p)

-- | Convenient wrapper around 'error_type_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Error_Type'.
lift_error_type
 :: forall err errs.
 Lift_Error_Type err errs =>
 err -> errs
lift_error_type = lift_error_typeP (Proxy::Proxy (Peano_of_Error_Type err errs))

-- ** Type 'Unlift_Error_Type'
-- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
type Unlift_Error_Type ty tys
 =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys

-- | Convenient wrapper around 'error_type_unliftN',
-- passing it the 'Peano' number from 'Peano_of_Error_Type'.
unlift_error_type
 :: forall ty tys.
 Unlift_Error_Type ty tys =>
 tys -> Maybe ty
unlift_error_type = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))

-- *** Class 'Error_Type_UnliftN'
-- | Try to unlift a given type error out of a given type error stack including it,
-- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
class Error_Type_UnliftN (p:: *) ty tys where
	error_type_unliftN :: Proxy p -> tys -> Maybe ty
instance Error_Type_UnliftN Zero curr curr where
	error_type_unliftN _ = Just
instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
	error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
	error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
instance
 Error_Type_UnliftN p other next =>
 Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
	error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
	error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing

-- ** Type 'Error_Type_Read'
-- | Common type errors.
data Error_Type ast
 =   Error_Type_Unsupported ast
 -- ^ Given syntax is supported by none
 -- of the type parser components
 -- of the type stack.
 |   Error_Type_Unsupported_here ast
 -- ^ Given syntax not supported by the current type parser component.
 |   Error_Type_Wrong_number_of_arguments ast Int
 deriving (Eq, Show)

-- | Convenient wrapper around 'lift_error_type',
-- passing the type family boilerplate.
error_type
 :: Lift_Error_Type (Error_Type ast)
                    (Error_of_Type ast (Root_of_Type ty))
 => Proxy ty
 -> Error_Type ast
 -> Error_of_Type ast (Root_of_Type ty)
error_type _ = lift_error_type

error_type_unsupported
 :: forall ast ty.
 ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 , Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 ) => Proxy ty -> ast
 -> Error_of_Type ast (Root_of_Type ty)
error_type_unsupported ty ast =
	case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
	 HTrue  -> error_type ty $ Error_Type_Unsupported ast
	 HFalse -> error_type ty $ Error_Type_Unsupported_here ast

-- ** Type 'No_Error_Type'
-- | A discarded error.
data No_Error_Type
 =   No_Error_Type
 deriving (Eq, Show)