Commit 7d53bf6f authored by simonpj's avatar simonpj
Browse files

[project @ 2006-01-06 16:08:57 by simonpj]

Add GADT tests
parent 0b3c43cf
{-# OPTIONS_GHC -fglasgow-exts #-}
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
......@@ -30,3 +30,15 @@ test('Nilsson', normal, compile, [''])
test('records', normal, compile_and_run, [''])
test('records-fail1', normal, compile_fail, [''])
# New ones from Dimitrios
# test('gadt-dim1', normal, compile, [''])
# test('gadt-dim2', normal, compile_fail, [''])
# test('gadt-dim3', normal, compile_fail, [''])
# test('gadt-dim4', normal, compile, [''])
# test('gadt-dim5', normal, compile, [''])
# test('gadt-dim6', normal, compile, [''])
# test('gadt-dim7', normal, compile, [''])
# test('gadt-dim8', normal, compile, [''])
# test('Arith', normal, compile, [''])
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldCompile where
data T a where
C :: Int -> T Int
D :: Bool -> T Bool
foo :: T a -> a
foo (C x) = x
foo (D x) = x
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldFail2 where
data T a where
C :: Int -> T Int
D :: Bool -> T Bool
-- should fail because variable is wobbly
foo (C x) = x
foo (D b) = b
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed5 where
data T a where
C :: T Bool
D :: T Int
data Y a where
E :: Y Bool
-- should succeed, the first branch is simply inaccessible
foo :: T Bool -> Bool
foo (D) = True
foo (C) = False
-- should succeed, the branch is inaccessible and not even type checked
baz :: Y Int -> Int
baz (E) = "dimitris!"
-- should fail => it is an attempt to call an inaccessible branch
test = baz (E)
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed1 where
data T1 a where
C :: (T2 b) -> b -> T1 Int
D :: Bool -> T1 Bool
-- should this work?
data T2 a where
F :: Int -> T2 Int
-- Should work, even though we start as wobbly
-- the existential makes us rigid again
foo x = case x of
C (F _) z -> (z + 1)
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed2 where
data T a where
C :: Int -> T Int
D :: Bool -> T Bool
foo :: T a -> a
foo (C x) = x + 1
foo (D x) = True
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed3 where
data T a where
C :: (T b) -> b -> T Int
D :: T Bool
-- Tests scoped annotations
foo :: T a -> a -> a
foo (C (x::b)) (z::a) = z + 1
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed4 where
data Z
data S a
data Add n m r where
PZero :: Add Z m m
PSucc :: Add n m p -> Add (S n) m (S p)
data XList n a where
XNil :: XList Z a
XCons :: a -> XList n a -> XList (S n) a
-- simple safe append function
append :: (Add n m r) -> XList n a -> XList m a -> XList r a
append PZero XNil l = l
append (PSucc prf) (XCons x xs) l = XCons x (append prf xs l)
{-# OPTIONS_GHC -fglasgow-exts #-}
module ShouldSucceed5 where
data T a where
C :: T Bool
D :: T Int
data Y a where
E :: T Bool
-- should succeed, the first branch is simply inaccessible
foo :: T Bool -> Bool
foo (D) = True
foo (C) = False
-- should succeed, the branch is inaccessible and not een type checked
baz :: Y Int -> Int
baz (E) = "dimitris!"
Should fail
gadt13.hs:13:5:
Couldn't match `Bool' against `Int'
Expected boxy type: Int
Inferred boxy type: Bool
In the pattern: B t
In the definition of `shw': shw (B t) = (("B " ++)) . (shows t)
......@@ -18,15 +18,16 @@ i2 :: T a -> a -> Int
i2 t (y::b) = case t of { K -> y+(1::Int) }
i3 :: forall a. T a -> a -> Int
i3 t y = let (t :: T b) = t in
let (y :: b) = y in
case t of K -> y
i3 t y
= let t1 = t in
let y1 = y in
case t1 of K -> y1
i4 :: forall a. T a -> a -> Int
i4 (t :: T c) (y :: c) =
let (t :: T b) = t in
let (y :: b) = y in
case t of K -> y
i4 (t :: T a) (y :: a)
= let t1 = t in
let y1 = y in
case t1 of K -> y1
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment