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

import Data.Proxy (Proxy(..))
import Data.Text (Text)
import qualified Data.Text as Text

import Language.Symantic.Lib.Data.Bool
import Language.Symantic.Type
import Language.Symantic.Expr.Root
import Language.Symantic.Expr.Alt

-- * Type family 'Error_of_Expr'
-- | The error(s) of an expression.
type family Error_of_Expr (ast:: *) (ex:: *) :: *
type instance Error_of_Expr ast (Expr_Root ex)
 =            Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
                                         (Type_Root_of_Expr (ex (Expr_Root ex)))
                                         ast)
                             (Error_of_Expr ast (ex (Expr_Root ex)))
type instance Error_of_Expr ast (Expr_Alt curr next root)
 = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
                         (Error_of_Expr ast (next root))

-- ** Type family 'Error_of_Expr_Alt'
-- | Remove 'No_Error_Expr' type when building the error of an expression.
type family Error_of_Expr_Alt ast curr next where
	Error_of_Expr_Alt ast No_Error_Expr next          = next
	Error_of_Expr_Alt ast curr          No_Error_Expr = curr
	Error_of_Expr_Alt ast curr          next          = Error_Expr_Alt curr next

-- * Type 'Error_Expr_Alt'
-- | Error expression making an alternative between two error expressions.
data Error_Expr_Alt curr next
 =   Error_Expr_Alt_Curr curr
 |   Error_Expr_Alt_Next next
 deriving (Eq, Show)

-- ** Type 'Error_Expr_Lift'
-- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_LiftP'.
type Error_Expr_Lift err errs
 =   Error_Expr_LiftP (Peano_of_Error_Expr err errs) err errs

-- | Convenient wrapper around 'error_expr_liftP',
-- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
error_expr_lift
 :: forall err errs.
 Error_Expr_Lift err errs => err -> errs
error_expr_lift = error_expr_liftP (Proxy::Proxy (Peano_of_Error_Expr err errs))

-- *** Type family 'Peano_of_Error_Expr'
-- | Return a 'Peano' number derived from the location
-- of a given error expression within a given error expression stack,
-- which is used to avoid @OverlappingInstances@.
type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
	Peano_of_Error_Expr err   err                        = Zero
	Peano_of_Error_Expr err   (Error_Expr_Alt err  next) = Zero
	Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)

-- *** Class 'Error_Expr_LiftP'
-- | Lift a given expression to the top of a given expression stack including it,
-- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
class Error_Expr_LiftP (p:: *) err errs where
	error_expr_liftP :: Proxy p -> err -> errs
instance Error_Expr_LiftP Zero curr curr where
	error_expr_liftP _ = id
instance Error_Expr_LiftP Zero curr (Error_Expr_Alt curr next) where
	error_expr_liftP _ = Error_Expr_Alt_Curr
instance
 Error_Expr_LiftP p other next =>
 Error_Expr_LiftP (Succ p) other (Error_Expr_Alt curr next) where
	error_expr_liftP _ = Error_Expr_Alt_Next . error_expr_liftP (Proxy::Proxy p)

-- ** Type 'Error_Expr_Unlift'
-- | Apply 'Peano_of_Error_Expr' on 'Error_Expr_UnliftP'.
type Error_Expr_Unlift ex exs
 =   Error_Expr_UnliftP (Peano_of_Error_Expr ex exs) ex exs

-- | Convenient wrapper around 'error_expr_unliftP',
-- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
error_expr_unlift
 :: forall ex exs.
 Error_Expr_Unlift ex exs => exs -> Maybe ex
error_expr_unlift = error_expr_unliftP (Proxy::Proxy (Peano_of_Error_Expr ex exs))

-- *** Class 'Error_Expr_UnliftP'
-- | Try to unlift a given expression error out of a given expression error stack including it,
-- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
class Error_Expr_UnliftP (p:: *) ex exs where
	error_expr_unliftP :: Proxy p -> exs -> Maybe ex
instance Error_Expr_UnliftP Zero curr curr where
	error_expr_unliftP _ = Just
instance Error_Expr_UnliftP Zero curr (Error_Expr_Alt curr next) where
	error_expr_unliftP _ (Error_Expr_Alt_Curr x) = Just x
	error_expr_unliftP _ (Error_Expr_Alt_Next _) = Nothing
instance
 Error_Expr_UnliftP p other next =>
 Error_Expr_UnliftP (Succ p) other (Error_Expr_Alt curr next) where
	error_expr_unliftP _ (Error_Expr_Alt_Next x) = error_expr_unliftP (Proxy::Proxy p) x
	error_expr_unliftP _ (Error_Expr_Alt_Curr _) = Nothing

-- * Type 'Error_Expr_Read'
-- | Common expression errors.
data Error_Expr err_ty ty ast
 =   Error_Expr_Wrong_number_of_arguments ast Int
 -- ^ Wrong number of arguments applied to a term,
 -- the integer is the number of arguments expected.
 |   Error_Expr_Type_mismatch ast (Exists_Type0 ty) (Exists_Type0 ty)
 -- ^ Mismatch between respectively expected and actual type.
 |   Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type0 ty)
 -- ^ A 'Constraint' is missing.
 |   Error_Expr_Read Error_Read ast
 -- ^ Error when reading a literal.
 |   Error_Expr_Type err_ty ast
 -- ^ Error when parsing a type.
 |   Error_Expr_Unsupported ast
 -- ^ Given syntax is supported by none
 -- of the expression parser components
 -- of the expression stack.
 |   Error_Expr_Unsupported_here ast
 -- ^ Given syntax not supported by
 -- the current expression parser component.
 deriving (Eq, Show)

-- | Convenient type alias.
type Error_Expr_of_Root ast root
 =   Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
                (Type_Root_of_Expr root)
                ast

-- | Convenient wrapper around 'error_expr_lift',
-- passing the type family boilerplate.
error_expr
 :: forall ast ex ty.
 (ty ~ Type_Root_of_Expr ex)
 => Error_Expr_Lift
   (Error_Expr (Error_of_Type ast ty) ty ast)
   (Error_of_Expr ast (Root_of_Expr ex))
 => Proxy ex
 -> Error_Expr (Error_of_Type ast ty) ty ast
 -> Error_of_Expr ast (Root_of_Expr ex)
error_expr _ = error_expr_lift

-- | Parsing utility to return 'Error_Expr_Unsupported'
-- or 'Error_Expr_Unsupported_here'
-- according to the given expression.
error_expr_unsupported
 :: forall ast ex ty root.
 ( root ~ Root_of_Expr ex
 , ty ~ Type_Root_of_Expr ex
 , IBool (Is_Last_Expr ex root)
 , Error_Expr_Lift (Error_Expr (Error_of_Type ast ty) ty ast)
                   (Error_of_Expr ast root)
 ) => Proxy ex -> ast
 -> Error_of_Expr ast (Root_of_Expr ex)
error_expr_unsupported ex ast =
	case iBool :: SBool (Is_Last_Expr ex root) of
	 STrue  -> error_expr ex $ Error_Expr_Unsupported ast
	 SFalse -> error_expr ex $ Error_Expr_Unsupported_here ast

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

-- * Type 'Error_Read'
-- | Error parsing a host-term.
data Error_Read
 =   Error_Read Text
 deriving (Eq, Show)

-- | Parse a host-term.
read_safe :: Read h => Text -> Either Error_Read h
read_safe t =
	case reads $ Text.unpack t of
	 [(x, "")] -> Right x
	 _         -> Left $ Error_Read t