@@ -1,79 +0,0 @@
1−module Main
2−
3−import Language.Reflection
4−import Language.Reflection.Errors
5−import Language.Reflection.Utils
6−
7−%language ErrorReflection
8−
9−-- Well-typed terms
10−
11−data Ty = TUnit | TFun Ty Ty
12−
13−instance Show Ty where
14− show TUnit = "()"
15− show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"
16−
17−using (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
21−
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'
27−
28−-- Extract the type from a reflected term type
29−
30−namespace ErrorReports
31− data Ty' = TUnit
32− | TFun Ty' Ty'
33− | TVar Int String -- To show in unification failures
34−
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 ++ ")"
39−
40−getTmTy : TT -> Maybe TT
41−getTmTy (App (App (App (P (TCon _ _) (NS (UN "Tm") _) _) _) _) ty) = Just ty
42−getTmTy _ = Nothing
43−
44−
45−reifyTy : TT -> Maybe Ty'
46−reifyTy (P (DCon _ _) (NS (UN "TUnit") _) _) = Just TUnit
47−reifyTy (App (App (P (DCon _ _) (NS (UN "TFun") _) _) t1) t2) = do ty1 <- reifyTy t1
48− ty2 <- reifyTy t2
49− return $ TFun ty1 ty2
50−reifyTy (P _ (MN i n) _) = Just (TVar i n)
51−reifyTy _ = Nothing
52−
53−-- Friendly error reporting
54−
55−total %error_handler
56−dslerr : Err -> Maybe (List ErrorReportPart)
57−dslerr (CantUnify _ tm1 tm2 _ _ _) = do tm1' <- getTmTy tm1
58− tm2' <- getTmTy tm2
59− ty1 <- reifyTy tm1'
60− ty2 <- reifyTy tm2'
61− return [TextPart $ "DSL type error: " ++ (show ty1) ++ " doesn't match " ++(show ty2)]
62−dslerr (At (FileLoc f l c) err) = do err' <- dslerr err
63− return [ TextPart "In file"
64− , TextPart f
65− , TextPart "line", TextPart (cast l)
66− , TextPart "column", TextPart (cast c)
67− , SubReport err']
68−dslerr (Elaborating s n err) = do err' <- dslerr err
69− return ([ TextPart $ "When elaborating " ++ s
70− , NamePart n
71− , TextPart ":"
72− , SubReport err'])
73−dslerr _ = Nothing
74−
75−
76−-- Report the error
77−bad : Tm [] TUnit
78−bad = Lam (Var Here)
79−