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