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
  27 -- ** Type family 'Error_of_Type_Alt'
  28 -- | Remove 'No_Error_Type' type when building 'Error_of_Type'.
  29 type family Error_of_Type_Alt ast curr next where
  30         Error_of_Type_Alt ast curr          No_Error_Type = curr
  31         Error_of_Type_Alt ast No_Error_Type next          = next
  32         Error_of_Type_Alt ast curr          next          = Error_Type_Alt curr next
  33
  34 -- * Type 'Error_Type_Alt'
  35 -- | Error type making an alternative between two error types.
  36 data Error_Type_Alt curr next
  37  =   Error_Type_Alt_Curr curr
  38  |   Error_Type_Alt_Next next
  39  deriving (Eq, Show)
  40
  41 -- ** Type 'Lift_Error_Type'
  42 type Lift_Error_Type err errs
  43  =   Lift_Error_TypeP (Peano_of_Error_Type err errs) err errs
  44
  45 -- *** Type 'Peano_of_Error_Type'
  46 -- | Return a 'Peano' number derived from the location
  47 -- of a given error type within a given error type stack.
  48 type family Peano_of_Error_Type (err:: *) (errs:: *) :: * where
  49         Peano_of_Error_Type err   err                        = Zero
  50         Peano_of_Error_Type err   (Error_Type_Alt err  next) = Zero
  51         Peano_of_Error_Type other (Error_Type_Alt curr next) = Succ (Peano_of_Error_Type other next)
  52
  53 -- *** Class 'Lift_Error_TypeP'
  54 -- | Lift a given error type to the top of a given error type stack including it,
  55 -- by constructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
  56 class Lift_Error_TypeP (p:: *) err errs where
  57         lift_error_typeP :: Proxy p -> err -> errs
  58 instance Lift_Error_TypeP Zero curr curr where
  59         lift_error_typeP _ = id
  60 instance Lift_Error_TypeP Zero curr (Error_Type_Alt curr next) where
  61         lift_error_typeP _ = Error_Type_Alt_Curr
  62 instance
  63  Lift_Error_TypeP p other next =>
  64  Lift_Error_TypeP (Succ p) other (Error_Type_Alt curr next) where
  65         lift_error_typeP _ = Error_Type_Alt_Next . lift_error_typeP (Proxy::Proxy p)
  66
  67 -- | Convenient wrapper around 'error_type_unliftN',
  68 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
  69 lift_error_type
  70  :: forall err errs.
  71  Lift_Error_Type err errs =>
  72  err -> errs
  73 lift_error_type = lift_error_typeP (Proxy::Proxy (Peano_of_Error_Type err errs))
  74
  75 -- ** Type 'Unlift_Error_Type'
  76 -- | Apply 'Peano_of_Error_Type' on 'Error_Type_UnliftN'.
  77 type Unlift_Error_Type ty tys
  78  =   Error_Type_UnliftN (Peano_of_Error_Type ty tys) ty tys
  79
  80 -- | Convenient wrapper around 'error_type_unliftN',
  81 -- passing it the 'Peano' number from 'Peano_of_Error_Type'.
  82 unlift_error_type
  83  :: forall ty tys.
  84  Unlift_Error_Type ty tys =>
  85  tys -> Maybe ty
  86 unlift_error_type = error_type_unliftN (Proxy::Proxy (Peano_of_Error_Type ty tys))
  87
  88 -- *** Class 'Error_Type_UnliftN'
  89 -- | Try to unlift a given type error out of a given type error stack including it,
  90 -- by deconstructing the appropriate sequence of 'Error_Type_Alt_Curr' and 'Error_Type_Alt_Next'.
  91 class Error_Type_UnliftN (p:: *) ty tys where
  92         error_type_unliftN :: Proxy p -> tys -> Maybe ty
  93 instance Error_Type_UnliftN Zero curr curr where
  94         error_type_unliftN _ = Just
  95 instance Error_Type_UnliftN Zero curr (Error_Type_Alt curr next) where
  96         error_type_unliftN _ (Error_Type_Alt_Curr x) = Just x
  97         error_type_unliftN _ (Error_Type_Alt_Next _) = Nothing
  98 instance
  99  Error_Type_UnliftN p other next =>
 100  Error_Type_UnliftN (Succ p) other (Error_Type_Alt curr next) where
 101         error_type_unliftN _ (Error_Type_Alt_Next x) = error_type_unliftN (Proxy::Proxy p) x
 102         error_type_unliftN _ (Error_Type_Alt_Curr _) = Nothing
 103
 104 -- ** Type 'Error_Type_Read'
 105 -- | Common type errors.
 106 data Error_Type ast
 107  =   Error_Type_Unsupported ast
 108  -- ^ Given syntax is supported by none
 109  -- of the type parser components
 110  -- of the type stack.
 111  |   Error_Type_Unsupported_here ast
 112  -- ^ Given syntax not supported by the current type parser component.
 113  |   Error_Type_Wrong_number_of_arguments ast Int
 114  |   Error_Type_Constraint_missing ast {-Exists_Dict-} {-Exists_Type ty-}
 115  |   Error_Type_No_TypeFamily ast
 116  -- ^ A 'Constraint' is missing.
 117  deriving (Eq, Show)
 118
 119 -- | Convenient wrapper around 'lift_error_type',
 120 -- passing the type family boilerplate.
 121 error_type
 122  :: Lift_Error_Type (Error_Type ast)
 123                     (Error_of_Type ast (Root_of_Type ty))
 124  => Proxy ty
 125  -> Error_Type ast
 126  -> Error_of_Type ast (Root_of_Type ty)
 127 error_type _ = lift_error_type
 128
 129 error_type_unsupported
 130  :: forall ast ty.
 131  ( IBool (Is_Last_Type ty (Root_of_Type ty))
 132  , Lift_Error_Type (Error_Type ast) (Error_of_Type ast (Root_of_Type ty))
 133  ) => Proxy ty -> ast
 134  -> Error_of_Type ast (Root_of_Type ty)
 135 error_type_unsupported ty ast =
 136         case iBool :: SBool (Is_Last_Type ty (Root_of_Type ty)) of
 137          STrue  -> error_type ty $ Error_Type_Unsupported ast
 138          SFalse -> error_type ty $ Error_Type_Unsupported_here ast
 139
 140 -- ** Type 'No_Error_Type'
 141 -- | A discarded error.
 142 data No_Error_Type
 143  =   No_Error_Type
 144  deriving (Eq, Show)
 145