summaryrefslogtreecommitdiff
path: root/tests/examples/ghc86/Arith.hs
blob: f516d3a3b447133dad6de9c09d74555ee1c482cc (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}

module Arith where

data E a b = E (a -> b) (b -> a)

eqRefl :: E a a
eqRefl = E id id

-- just to construct unique strings
data W
data M a

-- terms
data Var a where
  VarW :: Var W
  VarM :: Var (M a)

-- expose s in the type level making sure it is a string
data Abs s e1  where
  Abs :: (Var s) -> e1 -> Abs (Var s) e1

data App e1 e2 = App e1 e2
data Lit       = Lit

data TyBase      = TyBase
data TyArr t1 t2 = TyArr t1 t2

-- (x:ty) in G
data IN g p where
  INOne :: IN (g,(x,ty)) (x,ty)
  INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty)

data INEX g x where
  INEX :: IN g (x,v) -> INEX g x


-- G1 subseteq G2
type SUP g1 g2 = forall a. IN g1 a -> IN g2 a

-- typing derivations
data DER g a ty where
  DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty
  DApp :: DER g a1 (TyArr ty1 ty2) ->
            DER g a2 ty1 -> DER g (App a1 a2) ty2
  DAbs :: DER (g,(Var a,ty1)) e ty2 ->
            DER g (Abs (Var a) e) (TyArr ty1 ty2)
  DLit :: DER g Lit TyBase

-- G |- \x.x : a -> a
test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty)
test1 = DAbs (DVar INOne)

-- G |- (\x.x) Lit : Lit
test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase
test2 = DApp (DAbs (DVar INOne)) DLit

-- G |- \x.\y. x y : (C -> C) -> C -> C
test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty))
test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne)))

data ISVAL e where
 ISVALAbs :: ISVAL (Abs (Var v) e)
 ISVALLit :: ISVAL Lit

data React e1 e2 where
  SUBSTReact :: React (Abs (Var y) e) v

-- evaluation
data EDER e1 e2 where
 -- EVar    :: IN (a,val) -> ISVAL val -> EDER c a val
 EApp1   :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2)
 EApp2   :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')
 EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1

-- (\x.x) 3 -> 3
-- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit
-- test4 = EAppAbs ISVALLit SUBSTEqVar


-- existential
data REDUCES e1 where
   REDUCES :: EDER e1 e2 -> REDUCES e1

-- data WFEnv x c g  where
--  WFOne ::  ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))
--  WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))

-- data WFENVWRAP c g where
--    WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g


-- data INEXVAL c x where
--   INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x

-- -- the first cool theorem!
-- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g ->  INEXVAL c x
-- fromTEnvToEnv INOne (WFOne isv _)  = INEXVAL INOne isv
-- fromTEnvToEnv (INShift ind1) (WFShift ind2) =
--           case (fromTEnvToEnv ind1 ind2) of
--              INEXVAL i isv -> INEXVAL (INShift i) isv


data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)
data ISLIT v where ISLIT :: ISLIT Lit

data EXISTAbs where
  EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs

bot = bot

canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v
canFormsLam ISVALAbs _ = ISLAMBDA
-- canFormsLam ISVALLit _ = bot         <== unfortunately I cannot catch this ... requires some exhaustiveness check :-(

canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v
canFormsLit ISVALLit _ = ISLIT

data NULL

progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e)

progress (DAbs prem)  = Left ISVALAbs
progress (DLit)       = Left ISVALLit
-- progress (DVar iw)    = bot             <== here is the cool trick! I cannot even wite this down!
progress (DApp e1 e2)  =
     case (progress e1) of
         Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
         Left  isv1         -> case (progress e2) of
                                    Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
                                    Left isv2 -> case (canFormsLam isv1 e1) of
                                                    ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))


--    case fromTEnvToEnv iw (f iw) of
--      INEXVAL i isv -> Right (REDUCES (EVar i isv))
-- progress (WFENVWRAP f) (DApp e1 e2) =
--       case (progress (WFENVWRAP f) e1) of
--          Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))
--          Left  isv1         -> case (progress (WFENVWRAP f) e2) of
--                                  Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2))
--                                  Left isv2 -> case (canFormsLam isv1 e1) of
--                                                ISLAMBDA -> EAppAbs isv2 e1