Language/Symantic/Expr/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.Expr.Error where
   9
  10 import Data.Proxy (Proxy(..))
  11 import Data.Text (Text)
  12 import qualified Data.Text as Text
  13
  14 import Language.Symantic.Lib.Data.Bool
  15 import Language.Symantic.Type
  16 import Language.Symantic.Expr.Root
  17 import Language.Symantic.Expr.Alt
  18
  19 -- * Type family 'Error_of_Expr'
  20 -- | The error(s) of an expression.
  21 type family Error_of_Expr (ast:: *) (ex:: *) :: *
  22 type instance Error_of_Expr ast (Expr_Root ex)
  23  =            Error_Expr_Alt (Error_Expr (Error_of_Type ast (Type_Root_of_Expr (ex (Expr_Root ex))))
  24                                          (Type_Root_of_Expr (ex (Expr_Root ex)))
  25                                          ast)
  26                              (Error_of_Expr ast (ex (Expr_Root ex)))
  27 type instance Error_of_Expr ast (Expr_Alt curr next root)
  28  = Error_of_Expr_Alt ast (Error_of_Expr ast (curr root))
  29                          (Error_of_Expr ast (next root))
  30
  31 -- ** Type family 'Error_of_Expr_Alt'
  32 -- | Remove 'No_Error_Expr' type when building the error of an expression.
  33 type family Error_of_Expr_Alt ast curr next where
  34         Error_of_Expr_Alt ast No_Error_Expr next          = next
  35         Error_of_Expr_Alt ast curr          No_Error_Expr = curr
  36         Error_of_Expr_Alt ast curr          next          = Error_Expr_Alt curr next
  37
  38 -- * Type 'Error_Expr_Alt'
  39 -- | Error expression making an alternative between two error expressions.
  40 data Error_Expr_Alt curr next
  41  =   Error_Expr_Alt_Curr curr
  42  |   Error_Expr_Alt_Next next
  43  deriving (Eq, Show)
  44
  45 -- ** Type 'Lift_Error_Expr'
  46 -- | Apply 'Peano_of_Error_Expr' on 'Lift_Error_ExprP'.
  47 type Lift_Error_Expr err errs
  48  =   Lift_Error_ExprP (Peano_of_Error_Expr err errs) err errs
  49
  50 -- | Convenient wrapper around 'lift_error_exprP',
  51 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
  52 lift_error_expr
  53  :: forall err errs.
  54  Lift_Error_Expr err errs => err -> errs
  55 lift_error_expr = lift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr err errs))
  56
  57 -- *** Type family 'Peano_of_Error_Expr'
  58 -- | Return a 'Peano' number derived from the location
  59 -- of a given error expression within a given error expression stack,
  60 -- which is used to avoid @OverlappingInstances@.
  61 type family Peano_of_Error_Expr (err:: *) (errs:: *) :: * where
  62         Peano_of_Error_Expr err   err                        = Zero
  63         Peano_of_Error_Expr err   (Error_Expr_Alt err  next) = Zero
  64         Peano_of_Error_Expr other (Error_Expr_Alt curr next) = Succ (Peano_of_Error_Expr other next)
  65
  66 -- *** Class 'Lift_Error_ExprP'
  67 -- | Lift a given expression to the top of a given expression stack including it,
  68 -- by constructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
  69 class Lift_Error_ExprP (p:: *) err errs where
  70         lift_error_exprP :: Proxy p -> err -> errs
  71 instance Lift_Error_ExprP Zero curr curr where
  72         lift_error_exprP _ = id
  73 instance Lift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
  74         lift_error_exprP _ = Error_Expr_Alt_Curr
  75 instance
  76  Lift_Error_ExprP p other next =>
  77  Lift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
  78         lift_error_exprP _ = Error_Expr_Alt_Next . lift_error_exprP (Proxy::Proxy p)
  79
  80 -- ** Type 'Unlift_Error_Expr'
  81 -- | Apply 'Peano_of_Error_Expr' on 'Unlift_Error_ExprP'.
  82 type Unlift_Error_Expr ex exs
  83  =   Unlift_Error_ExprP (Peano_of_Error_Expr ex exs) ex exs
  84
  85 -- | Convenient wrapper around 'unlift_error_exprP',
  86 -- passing it the 'Peano' number from 'Peano_of_Error_Expr'.
  87 unlift_error_expr
  88  :: forall ex exs.
  89  Unlift_Error_Expr ex exs => exs -> Maybe ex
  90 unlift_error_expr = unlift_error_exprP (Proxy::Proxy (Peano_of_Error_Expr ex exs))
  91
  92 -- *** Class 'Unlift_Error_ExprP'
  93 -- | Try to unlift a given expression error out of a given expression error stack including it,
  94 -- by deconstructing the appropriate sequence of 'Error_Expr_Alt_Curr' and 'Error_Expr_Alt_Next'.
  95 class Unlift_Error_ExprP (p:: *) ex exs where
  96         unlift_error_exprP :: Proxy p -> exs -> Maybe ex
  97 instance Unlift_Error_ExprP Zero curr curr where
  98         unlift_error_exprP _ = Just
  99 instance Unlift_Error_ExprP Zero curr (Error_Expr_Alt curr next) where
 100         unlift_error_exprP _ (Error_Expr_Alt_Curr x) = Just x
 101         unlift_error_exprP _ (Error_Expr_Alt_Next _) = Nothing
 102 instance
 103  Unlift_Error_ExprP p other next =>
 104  Unlift_Error_ExprP (Succ p) other (Error_Expr_Alt curr next) where
 105         unlift_error_exprP _ (Error_Expr_Alt_Next x) = unlift_error_exprP (Proxy::Proxy p) x
 106         unlift_error_exprP _ (Error_Expr_Alt_Curr _) = Nothing
 107
 108 -- * Type 'Error_Expr_Read'
 109 -- | Common expression errors.
 110 data Error_Expr err_ty ty ast
 111  =   Error_Expr_Wrong_number_of_arguments ast Int
 112  -- ^ Wrong number of arguments applied to a term,
 113  -- the integer is the number of arguments expected.
 114  |   Error_Expr_Type_mismatch ast (Exists_Type ty) (Exists_Type ty)
 115  -- ^ Mismatch between respectively expected and actual type.
 116  |   Error_Expr_Constraint_missing ast {-Exists_Dict-} (Exists_Type ty)
 117  -- ^ A 'Constraint' is missing.
 118  |   Error_Expr_Read Error_Read ast
 119  -- ^ Error when reading a literal.
 120  |   Error_Expr_Type err_ty ast
 121  -- ^ Error when parsing a type.
 122  |   Error_Expr_Unsupported ast
 123  -- ^ Given syntax is supported by none
 124  -- of the expression parser components
 125  -- of the expression stack.
 126  |   Error_Expr_Unsupported_here ast
 127  -- ^ Given syntax not supported by
 128  -- the current expression parser component.
 129  deriving (Eq, Show)
 130
 131 -- | Convenient type alias.
 132 type Error_Expr_of_Root ast root
 133  =   Error_Expr (Error_of_Type ast (Type_Root_of_Expr root))
 134                 (Type_Root_of_Expr root)
 135                 ast
 136
 137 -- | Convenient wrapper around 'lift_error_expr',
 138 -- passing the type family boilerplate.
 139 error_expr
 140  :: forall ast ex ty.
 141  (ty ~ Type_Root_of_Expr ex)
 142  => Lift_Error_Expr
 143    (Error_Expr (Error_of_Type ast ty) ty ast)
 144    (Error_of_Expr ast (Root_of_Expr ex))
 145  => Proxy ex
 146  -> Error_Expr (Error_of_Type ast ty) ty ast
 147  -> Error_of_Expr ast (Root_of_Expr ex)
 148 error_expr _ = lift_error_expr
 149
 150 -- | Parsing utility to return 'Error_Expr_Unsupported'
 151 -- or 'Error_Expr_Unsupported_here'
 152 -- according to the given expression.
 153 error_expr_unsupported
 154  :: forall ast ex ty root.
 155  ( root ~ Root_of_Expr ex
 156  , ty ~ Type_Root_of_Expr ex
 157  , IBool (Is_Last_Expr ex root)
 158  , Lift_Error_Expr (Error_Expr (Error_of_Type ast ty) ty ast)
 159                    (Error_of_Expr ast root)
 160  ) => Proxy ex -> ast
 161  -> Error_of_Expr ast (Root_of_Expr ex)
 162 error_expr_unsupported ex ast =
 163         case iBool :: SBool (Is_Last_Expr ex root) of
 164          STrue  -> error_expr ex $ Error_Expr_Unsupported ast
 165          SFalse -> error_expr ex $ Error_Expr_Unsupported_here ast
 166
 167 -- ** Type 'No_Error_Expr'
 168 -- | A discarded error.
 169 data No_Error_Expr
 170  =   No_Error_Expr
 171  deriving (Eq, Show)
 172
 173 -- * Type 'Error_Read'
 174 -- | Error parsing a host-term.
 175 data Error_Read
 176  =   Error_Read Text
 177  deriving (Eq, Show)
 178
 179 -- | Parse a host-term.
 180 read_safe :: Read h => Text -> Either Error_Read h
 181 read_safe t =
 182         case reads $ Text.unpack t of
 183          [(x, "")] -> Right x
 184          _         -> Left $ Error_Read t