Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
First-ever Idris DSL with domain-specific error messages!
module ErrorTest
import Language.Reflection
import Language.Reflection.Errors
import Language.Reflection.Utils
%language ErrorReflection
data Ty = TUnit | TFun Ty Ty
instance Show Ty where
show TUnit = "()"
show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"
using (n : Nat, G : Vect n Ty)
data HasType : Vect n Ty -> Ty -> Type where
Here : HasType (t::G) t
There : HasType G t -> HasType (t' :: G) t
data Tm : Vect n Ty -> Ty -> Type where
U : Tm G TUnit
Var : HasType G t -> Tm G t
Lam : Tm (t :: G) t' -> Tm G (TFun t t')
App : Tm G (TFun t t') -> Tm G t -> Tm G t'
-- Extract the type from a reflected term type
namespace ErrorReports
data Ty' = TUnit
| TFun Ty' Ty'
| TVar Int String -- To show in unification failures
instance Show Ty' where
show TUnit = "()"
show (TFun x y) = "(" ++ show x ++ " => " ++ show y ++ ")"
show (TVar i n) = n ++ "(" ++ cast i ++ ")"
getTmTy : TT -> Maybe TT
getTmTy (App (App (App (P (TCon _ _) (NS (UN "Tm") _) _) _) _) ty) = Just ty
getTmTy _ = Nothing
reifyTy : TT -> Maybe Ty'
reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit
reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1
ty2 <- reifyTy t2
return $ TFun ty1 ty2
reifyTy (P _ (MN i n) _) = Just (TVar i n)
reifyTy _ = Nothing
total %error_handler
dslerr : Err -> Maybe (List ErrorReportPart)
dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1
tm2' <- getTmTy tm2
ty1 <- reifyTy tm1'
ty2 <- reifyTy tm2'
return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]
dslerr _ = Nothing
____ __ _
/ _/___/ /____(_)____
/ // __ / ___/ / ___/ Version 0.9.10.1-git:95960ce
_/ // /_/ / / / (__ ) http://www.idris-lang.org/
/___/\__,_/_/ /_/____/ Type :? for help
Type checking ./ErrorTest.idr
*ErrorTest> (the (Tm [] TUnit) (Lam (Var Here)))
DSL type error: (t'(1000) => t'(1000)) doesn't match ()
Original error:
Can't unify
Tm [] (ErrorTest.TFun t' t')
with
Tm [] ErrorTest.TUnit
Specifically:
Can't unify
ErrorTest.TFun t' t'
with
ErrorTest.TUnit
*ErrorTest>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.