@@ -0,0 +1,79 @@
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+