Language/Symantic/Type/Error.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE FlexibleContexts #-}
   3 {-# LANGUAGE FlexibleInstances #-}
   4 {-# LANGUAGE MultiParamTypeClasses #-}
   5 {-# LANGUAGE ScopedTypeVariables #-}
   6 {-# LANGUAGE TypeFamilies #-}
   7 {-# LANGUAGE UndecidableInstances #-}
   8 module Language.Symantic.Type.Error where
   9
  10 import Data.Proxy
  11 import Language.Symantic.Lib.Data.Peano
  12 import Language.Symantic.Lib.Data.Bool
  13
  14 import Language.Symantic.Type.Root
  15 import Language.Symantic.Type.Alt
  16
  17 -- ** Type family 'Error_of_Type'
  18 -- | Return the error type of a type.
  19 type family Error_of_Type (ast:: *) (ty:: * -> *) :: *
  20 type instance Error_of_Type ast (Type_Root ty)
  21  = Error_Type_Alt (Error_Type ast)
  22                   (Error_of_Type ast (ty (Type_Root ty)))
  23 type instance Error_of_Type ast (Type_Alt curr next root)
  24  = Error_of_Type_Alt ast (Error_of_Type ast (curr root))
  25                          (Error_of_Type ast (next root))
  26 -- ** Type family 'Error_of_Type_Alt'
  27 -- | Remove 'No_Error_Type' type when building 'Error_of_Type'.
  28 type family Error_of_Type_Alt ast curr next where
  29         Error_of_Type_Alt ast curr          No_Error_Type = curr
  30         Error_of_Type_Alt ast No_Error_Type next          = next
  31         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
  32
  33 -- * Type 'Error_Type_Alt'
  34 -- | Error type making an alternative between two error types.
  35 data Error_Type_Alt curr next
  36  =   Error_Type_Alt_Curr curr
  37  |   Error_Type_Alt_Next next
  38  deriving (Eq, Show)
  39
  40 -- ** Type 'Lift_Error_Type'
  41 type Lift_Error_Type err errs
  42  =   Lift_Error_TypeP (Peano_of_Error_Type err errs) err errs
  43
  44 -- *** Type 'Peano_of_Error_Type'
  45 -- | Return a 'Peano' number derived from the location
  46 -- of a given error type within a given error type stack.
  47 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
  48         Peano_of_Error_Type err   err                        = Zero
  49         Peano_of_Error_Type err   (Error_Type_Alt err  next) = Zero
  50         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
  51
  52 -- *** Class 'Lift_Error_TypeP'
  53 -- | Lift a given error type to the top of a given error type stack including it,
  54 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
  55 class Lift_Error_TypeP (p:: *) err errs where
  56         lift_error_typeP :: Proxy p -> err -> errs
  57 instance Lift_Error_TypeP Zero curr curr where
  58         lift_error_typeP _ = id
  59 instance Lift_Error_TypeP Zero curr (Error_Type_Alt curr next) where
  60         lift_error_typeP _ = Error_Type_Alt_Curr
  61 instance
  62  Lift_Error_TypeP p other next =>
  63  Lift_Error_TypeP (Succ p) other (Error_Type_Alt curr next) where
  64         lift_error_typeP _ = Error_Type_Alt_Next . lift_error_typeP (Proxy::Proxy p)
  65
  66 -- | Convenient wrapper around 'error_type_unliftN',
  67 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
  68 lift_error_type
  69  :: forall err errs.
  70  Lift_Error_Type err errs =>
  71  err -> errs
  72 lift_error_type = lift_error_typeP (Proxy::Proxy (Peano_of_Error_Type err errs))
  73
  74 -- ** Type 'Unlift_Error_Type'
  75 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
  76 type Unlift_Error_Type ty tys
  77  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
  78
  79 -- | Convenient wrapper around 'error_type_unliftN',
  80 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
  81 unlift_error_type
  82  :: forall ty tys.
  83  Unlift_Error_Type ty tys =>
  84  tys -> Maybe ty
  85 unlift_error_type = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
  86
  87 -- *** Class 'Error_Type_UnliftN'
  88 -- | Try to unlift a given type error out of a given type error stack including it,
  89 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
  90 class Error_Type_UnliftN (p:: *) ty tys where
  91         error_type_unliftN :: Proxy p -> tys -> Maybe ty
  92 instance Error_Type_UnliftN Zero curr curr where
  93         error_type_unliftN _ = Just
  94 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
  95         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
  96         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
  97 instance
  98  Error_Type_UnliftN p other next =>
  99  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 100         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 101         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 102
 103 -- ** Type 'Error_Type_Read'
 104 -- | Common type errors.
 105 data Error_Type ast
 106  =   Error_Type_Unsupported ast
 107  -- ^ Given syntax is supported by none
 108  -- of the type parser components
 109  -- of the type stack.
 110  |   Error_Type_Unsupported_here ast
 111  -- ^ Given syntax not supported by the current type parser component.
 112  |   Error_Type_Wrong_number_of_arguments ast Int
 113  deriving (Eq, Show)
 114
 115 -- | Convenient wrapper around 'lift_error_type',
 116 -- passing the type family boilerplate.
 117 error_type
 118  :: Lift_Error_Type (Error_Type ast)
 119                     (Error_of_Type ast (Root_of_Type ty))
 120  => Proxy ty
 121  -> Error_Type ast
 122  -> Error_of_Type ast (Root_of_Type ty)
 123 error_type _ = lift_error_type
 124
 125 error_type_unsupported
 126  :: forall ast ty.
 127  ( Implicit_HBool (Is_Last_Type ty (Root_of_Type ty))
 128  , Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 129  ) => Proxy ty -> ast
 130  -> Error_of_Type ast (Root_of_Type ty)
 131 error_type_unsupported ty ast =
 132         case hbool :: HBool (Is_Last_Type ty (Root_of_Type ty)) of
 133          HTrue  -> error_type ty $ Error_Type_Unsupported ast
 134          HFalse -> error_type ty $ Error_Type_Unsupported_here ast
 135
 136 -- ** Type 'No_Error_Type'
 137 -- | A discarded error.
 138 data No_Error_Type
 139  =   No_Error_Type
 140  deriving (Eq, Show)
 141