git.iko.soy/Idris-dev
on ebb4fee help sign in
Idris-dev/test/error003/ErrorReflection.idr
69 lines 2.1 kB history raw
1module Main
3import Language.Reflection
4import Language.Reflection.Errors
5import Language.Reflection.Utils
6import Data.Vect
8%language ErrorReflection
10-- Well-typed terms
12data Ty = TUnit | TFun Ty Ty
14implementation Show Ty where
15 show TUnit = "()"
16 show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"
18using (n : Nat, G : Vect n Ty)
19 data HasType : Vect n Ty -> Ty -> Type where
20 Here : HasType (t::G) t
21 There : HasType G t -> HasType (t' :: G) t
23 data Tm : Vect n Ty -> Ty -> Type where
24 U : Tm G TUnit
25 Var : HasType G t -> Tm G t
26 Lam : Tm (t :: G) t' -> Tm G (TFun t t')
27 App : Tm G (TFun t t') -> Tm G t -> Tm G t'
29-- Extract the type from a reflected term type
31namespace ErrorReports
32 data Ty' = TUnit
33 | TFun Ty' Ty'
34 | TVar Int String -- To show in unification failures
36 implementation Show Ty' where
37 show TUnit = "()"
38 show (TFun x y) = "(" ++ show x ++ " => " ++ show y ++ ")"
39 show (TVar i n) = n ++ "(" ++ cast i ++ ")"
41getTmTy : TT -> Maybe TT
42getTmTy (App (App (App (P (TCon _ _) (NS (UN "Tm") _) _) _) _) ty) = Just ty
43getTmTy _ = Nothing
46reifyTy : TT -> Maybe Ty'
47reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit
48reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1
49 ty2 <- reifyTy t2
50 pure $ TFun ty1 ty2
51reifyTy (P _ (MN i n) _) = Just (TVar i n)
52reifyTy _ = Nothing
54-- Friendly error reporting
56total %error_handler
57dslerr : Err -> Maybe (List ErrorReportPart)
58dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1
59 tm2' <- getTmTy tm2
60 ty1 <- reifyTy tm1'
61 ty2 <- reifyTy tm2'
62 Just [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]
63dslerr _ = Nothing
66-- Report the error
67bad : Tm [] TUnit
68bad = Lam (Var Here)