{-# 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 'Error_Type_Lift'
type Error_Type_Lift err errs
 =   Error_Type_LiftP (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 'Error_Type_LiftP'
-- | 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 Error_Type_LiftP (p:: *) err errs where
	error_type_liftP :: Proxy p -> err -> errs
instance Error_Type_LiftP Zero curr curr where
	error_type_liftP _ = id
instance Error_Type_LiftP Zero curr (Error_Type_Alt curr next) where
	error_type_liftP _ = Error_Type_Alt_Curr
instance
 Error_Type_LiftP p other next =>
 Error_Type_LiftP (Succ p) other (Error_Type_Alt curr next) where
	error_type_liftP _ = Error_Type_Alt_Next . error_type_liftP (Proxy::Proxy p)

-- | Convenient wrapper around 'error_type_unliftP',
-- passing it the 'Peano' number from 'Peano_of_Error_Type'.
error_type_lift
 :: forall err errs.
 Error_Type_Lift err errs =>
 err -> errs
error_type_lift = error_type_liftP (Proxy::Proxy (Peano_of_Error_Type err errs))

-- ** Type 'Error_Type_Unlift'
-- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftP'.
type Error_Type_Unlift ty tys
 =   Error_Type_UnliftP (Peano_of_Error_Type ty tys) ty tys

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

-- *** Class 'Error_Type_UnliftP'
-- | 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_UnliftP (p:: *) ty tys where
	error_type_unliftP :: Proxy p -> tys -> Maybe ty
instance Error_Type_UnliftP Zero curr curr where
	error_type_unliftP _ = Just
instance Error_Type_UnliftP Zero curr (Error_Type_Alt curr next) where
	error_type_unliftP _ (Error_Type_Alt_Curr x) = Just x
	error_type_unliftP _ (Error_Type_Alt_Next _) = Nothing
instance
 Error_Type_UnliftP p other next =>
 Error_Type_UnliftP (Succ p) other (Error_Type_Alt curr next) where
	error_type_unliftP _ (Error_Type_Alt_Next x) = error_type_unliftP (Proxy::Proxy p) x
	error_type_unliftP _ (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
 |   Error_Type_Constraint_missing ast {-Exists_Dict-} {-Exists_Type0 ty-}
 |   Error_Type_No_Type_Family ast
 -- ^ A 'Constraint' is missing.
 deriving (Eq, Show)

-- | Convenient wrapper around 'error_type_lift',
-- passing the type family boilerplate.
error_type
 :: Error_Type_Lift (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 _ = error_type_lift

error_type_unsupported
 :: forall ast ty.
 ( IBool (Is_Last_Type ty (Root_of_Type ty))
 , Error_Type_Lift (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 iBool :: SBool (Is_Last_Type ty (Root_of_Type ty)) of
	 STrue  -> error_type ty $ Error_Type_Unsupported ast
	 SFalse -> 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)