1 files changed, 146 insertions, 0 deletions
diff --git a/testsuite/tests/gadt/Arith.hs b/testsuite/tests/gadt/Arith.hs
new file mode 100644
index 0000000000..a98ee729a9
--- /dev/null
+++ b/testsuite/tests/gadt/Arith.hs
@@ -0,0 +1,146 @@
+{-# LANGUAGE GADTs #-}
+
+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 
+                              
+
+