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