summaryrefslogtreecommitdiff
path: root/tests/examples/ghc86/Arith.hs
diff options
context:
space:
mode:
Diffstat (limited to 'tests/examples/ghc86/Arith.hs')
-rw-r--r--tests/examples/ghc86/Arith.hs145
1 files changed, 145 insertions, 0 deletions
diff --git a/tests/examples/ghc86/Arith.hs b/tests/examples/ghc86/Arith.hs
new file mode 100644
index 0000000..f516d3a
--- /dev/null
+++ b/tests/examples/ghc86/Arith.hs
@@ -0,0 +1,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
+