Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / Arith.hs
1 {-# LANGUAGE GADTs #-}
2
3 module Arith where
4
5 data E a b = E (a -> b) (b -> a)
6
7 eqRefl :: E a a
8 eqRefl = E id id
9
10 -- just to construct unique strings
11 data W
12 data M a
13
14 -- terms
15 data Var a where
16 VarW :: Var W
17 VarM :: Var (M a)
18
19 -- expose s in the type level making sure it is a string
20 data Abs s e1 where
21 Abs :: (Var s) -> e1 -> Abs (Var s) e1
22
23 data App e1 e2 = App e1 e2
24 data Lit = Lit
25
26 data TyBase = TyBase
27 data TyArr t1 t2 = TyArr t1 t2
28
29 -- (x:ty) in G
30 data IN g p where
31 INOne :: IN (g,(x,ty)) (x,ty)
32 INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty)
33
34 data INEX g x where
35 INEX :: IN g (x,v) -> INEX g x
36
37
38 -- G1 subseteq G2
39 type SUP g1 g2 = forall a. IN g1 a -> IN g2 a
40
41 -- typing derivations
42 data DER g a ty where
43 DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty
44 DApp :: DER g a1 (TyArr ty1 ty2) ->
45 DER g a2 ty1 -> DER g (App a1 a2) ty2
46 DAbs :: DER (g,(Var a,ty1)) e ty2 ->
47 DER g (Abs (Var a) e) (TyArr ty1 ty2)
48 DLit :: DER g Lit TyBase
49
50 -- G |- \x.x : a -> a
51 test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty)
52 test1 = DAbs (DVar INOne)
53
54 -- G |- (\x.x) Lit : Lit
55 test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase
56 test2 = DApp (DAbs (DVar INOne)) DLit
57
58 -- G |- \x.\y. x y : (C -> C) -> C -> C
59 test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty))
60 test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne)))
61
62 data ISVAL e where
63 ISVALAbs :: ISVAL (Abs (Var v) e)
64 ISVALLit :: ISVAL Lit
65
66 data React e1 e2 where
67 SUBSTReact :: React (Abs (Var y) e) v
68
69 -- evaluation
70 data EDER e1 e2 where
71 -- EVar :: IN (a,val) -> ISVAL val -> EDER c a val
72 EApp1 :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2)
73 EApp2 :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')
74 EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1
75
76 -- (\x.x) 3 -> 3
77 -- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit
78 -- test4 = EAppAbs ISVALLit SUBSTEqVar
79
80
81 -- existential
82 data REDUCES e1 where
83 REDUCES :: EDER e1 e2 -> REDUCES e1
84
85 -- data WFEnv x c g where
86 -- WFOne :: ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))
87 -- WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))
88
89 -- data WFENVWRAP c g where
90 -- WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g
91
92
93 -- data INEXVAL c x where
94 -- INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x
95
96 -- -- the first cool theorem!
97 -- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g -> INEXVAL c x
98 -- fromTEnvToEnv INOne (WFOne isv _) = INEXVAL INOne isv
99 -- fromTEnvToEnv (INShift ind1) (WFShift ind2) =
100 -- case (fromTEnvToEnv ind1 ind2) of
101 -- INEXVAL i isv -> INEXVAL (INShift i) isv
102
103
104 data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)
105 data ISLIT v where ISLIT :: ISLIT Lit
106
107 data EXISTAbs where
108 EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs
109
110 bot = bot
111
112 canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v
113 canFormsLam ISVALAbs _ = ISLAMBDA
114 -- canFormsLam ISVALLit _ = bot <== unfortunately I cannot catch this ... requires some exhaustiveness check :-(
115
116 canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v
117 canFormsLit ISVALLit _ = ISLIT
118
119 data NULL
120
121 progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e)
122
123 progress (DAbs prem) = Left ISVALAbs
124 progress (DLit) = Left ISVALLit
125 -- progress (DVar iw) = bot <== here is the cool trick! I cannot even wite this down!
126 progress (DApp e1 e2) =
127 case (progress e1) of
128 Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
129 Left isv1 -> case (progress e2) of
130 Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
131 Left isv2 -> case (canFormsLam isv1 e1) of
132 ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))
133
134
135 -- case fromTEnvToEnv iw (f iw) of
136 -- INEXVAL i isv -> Right (REDUCES (EVar i isv))
137 -- progress (WFENVWRAP f) (DApp e1 e2) =
138 -- case (progress (WFENVWRAP f) e1) of
139 -- Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
140 -- Left isv1 -> case (progress (WFENVWRAP f) e2) of
141 -- Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
142 -- Left isv2 -> case (canFormsLam isv1 e1) of
143 -- ISLAMBDA -> EAppAbs isv2 e1
144
145
146