diff options
author | Thomas Miedema <thomasmiedema@gmail.com> | 2016-06-18 22:44:19 +0200 |
---|---|---|
committer | Thomas Miedema <thomasmiedema@gmail.com> | 2016-06-20 16:22:07 +0200 |
commit | 915e07c33b143126e3c8de1d2ec22ccc709a9a24 (patch) | |
tree | fcde0a7ffc1466b6e53dbee6df835af07e9a7ecc /testsuite/tests/gadt | |
parent | 46ff80f26d1892e1b50e3f10c5d3fded33da6e81 (diff) | |
download | haskell-915e07c33b143126e3c8de1d2ec22ccc709a9a24.tar.gz |
Testsuite: tabs -> spaces [skip ci]
Diffstat (limited to 'testsuite/tests/gadt')
-rw-r--r-- | testsuite/tests/gadt/Nilsson.hs | 130 | ||||
-rw-r--r-- | testsuite/tests/gadt/T3169.hs | 4 | ||||
-rw-r--r-- | testsuite/tests/gadt/T7205.hs | 10 | ||||
-rw-r--r-- | testsuite/tests/gadt/gadt2.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/gadt/gadt25.hs | 18 | ||||
-rw-r--r-- | testsuite/tests/gadt/gadt5.hs | 16 | ||||
-rw-r--r-- | testsuite/tests/gadt/gadt8.hs | 8 | ||||
-rw-r--r-- | testsuite/tests/gadt/josef.hs | 20 | ||||
-rw-r--r-- | testsuite/tests/gadt/nbe.hs | 82 | ||||
-rw-r--r-- | testsuite/tests/gadt/records.hs | 9 | ||||
-rw-r--r-- | testsuite/tests/gadt/red-black.hs | 6 | ||||
-rw-r--r-- | testsuite/tests/gadt/scoped.hs | 2 | ||||
-rw-r--r-- | testsuite/tests/gadt/set.hs | 6 | ||||
-rw-r--r-- | testsuite/tests/gadt/termination.hs | 18 | ||||
-rw-r--r-- | testsuite/tests/gadt/ubx-records.hs | 10 | ||||
-rw-r--r-- | testsuite/tests/gadt/while.hs | 70 |
16 files changed, 205 insertions, 206 deletions
diff --git a/testsuite/tests/gadt/Nilsson.hs b/testsuite/tests/gadt/Nilsson.hs index bb2fa1ba20..50dd3c58fc 100644 --- a/testsuite/tests/gadt/Nilsson.hs +++ b/testsuite/tests/gadt/Nilsson.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GADTs, ScopedTypeVariables #-} --- Supplied by Henrik Nilsson, showed up a bug in GADTs +-- Supplied by Henrik Nilsson, showed up a bug in GADTs module Nilsson where @@ -12,7 +12,7 @@ fromEvent = undefined usrErr :: String -> String -> String -> a usrErr = undefined -type DTime = Double -- [s] +type DTime = Double -- [s] data SF a b = SF {sfTF :: a -> Transition a b} @@ -53,13 +53,13 @@ sfArr (FDG f) = sfArrG f sfId :: SF' a a sfId = sf where - sf = SFArr (\_ a -> (sf, a)) FDI + sf = SFArr (\_ a -> (sf, a)) FDI sfConst :: b -> SF' a b sfConst b = sf where - sf = SFArr (\_ _ -> (sf, b)) (FDC b) + sf = SFArr (\_ _ -> (sf, b)) (FDC b) sfNever :: SF' a (Event b) @@ -76,7 +76,7 @@ sfArrE f fne = sf sfArrG :: (a -> b) -> SF' a b sfArrG f = sf where - sf = SFArr (\_ a -> (sf, f a)) (FDG f) + sf = SFArr (\_ a -> (sf, f a)) (FDG f) sfAcc :: (c -> a -> (c, b)) -> c -> b -> SF' (Event a) b @@ -107,10 +107,10 @@ sfAcc f c bne = sf -- * We still want to be able to get hold of the original function. data FunDesc a b where - FDI :: FunDesc a a -- Identity function - FDC :: b -> FunDesc a b -- Constant function - FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun - FDG :: (a -> b) -> FunDesc a b -- General function + FDI :: FunDesc a a -- Identity function + FDC :: b -> FunDesc a b -- Constant function + FDE :: (Event a -> b) -> b -> FunDesc (Event a) b -- Event-processing fun + FDG :: (a -> b) -> FunDesc a b -- General function fdFun :: FunDesc a b -> (a -> b) fdFun FDI = id @@ -142,17 +142,17 @@ vfyNoEv :: Event a -> b -> b vfyNoEv NoEvent b = b vfyNoEv _ _ = usrErr "AFRP" "vfyNoEv" "Assertion failed: Functions on events must not \ - \map NoEvent to Event." + \map NoEvent to Event." compPrim :: SF a b -> SF b c -> SF a c compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} where - tf0 a0 = (cpXX sf1 sf2, c0) - where - (sf1, b0) = tf10 a0 - (sf2, c0) = tf20 b0 + tf0 a0 = (cpXX sf1 sf2, c0) + where + (sf1, b0) = tf10 a0 + (sf2, c0) = tf20 b0 - -- Naming convention: cp<X><Y> where <X> and <Y> is one of: + -- Naming convention: cp<X><Y> where <X> and <Y> is one of: -- X - arbitrary signal function -- A - arbitrary pure arrow -- C - constant arrow @@ -165,35 +165,35 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} cpXX sf1 (SFArr _ fd2) = cpXA sf1 fd2 cpXX (SFAcc _ f1 s1 bne) (SFAcc _ f2 s2 cne) = sfAcc f (s1, s2) (vfyNoEv bne cne) - where - f (s1, s2) a = - case f1 s1 a of - (s1', NoEvent) -> ((s1', s2), cne) - (s1', Event b) -> - let (s2', c) = f2 s2 b in ((s1', s2'), c) + where + f (s1, s2) a = + case f1 s1 a of + (s1', NoEvent) -> ((s1', s2), cne) + (s1', Event b) -> + let (s2', c) = f2 s2 b in ((s1', s2'), c) cpXX (SFCpAXA _ fd11 sf12 fd13) (SFCpAXA _ fd21 sf22 fd23) = cpAXA fd11 (cpXX (cpXA sf12 (fdComp fd13 fd21)) sf22) fd23 - cpXX sf1 sf2 = SF' tf - where - tf dt a = (cpXX sf1' sf2', c) - where - (sf1', b) = (sfTF' sf1) dt a - (sf2', c) = (sfTF' sf2) dt b + cpXX sf1 sf2 = SF' tf + where + tf dt a = (cpXX sf1' sf2', c) + where + (sf1', b) = (sfTF' sf1) dt a + (sf2', c) = (sfTF' sf2) dt b cpAXA :: FunDesc a b -> SF' b c -> FunDesc c d -> SF' a d cpAXA FDI sf2 fd3 = cpXA sf2 fd3 cpAXA fd1 sf2 FDI = cpAX fd1 sf2 cpAXA (FDC b) sf2 fd3 = cpCXA b sf2 fd3 - cpAXA fd1 sf2 (FDC d) = sfConst d + cpAXA fd1 sf2 (FDC d) = sfConst d cpAXA fd1 (SFArr _ fd2) fd3 = sfArr (fdComp (fdComp fd1 fd2) fd3) - cpAX :: FunDesc a b -> SF' b c -> SF' a c + cpAX :: FunDesc a b -> SF' b c -> SF' a c cpAX FDI sf2 = sf2 cpAX (FDC b) sf2 = cpCX b sf2 cpAX (FDE f1 f1ne) sf2 = cpEX f1 f1ne sf2 cpAX (FDG f1) sf2 = cpGX f1 sf2 - cpXA :: SF' a b -> FunDesc b c -> SF' a c + cpXA :: SF' a b -> FunDesc b c -> SF' a c cpXA sf1 FDI = sf1 cpXA sf1 (FDC c) = sfConst c cpXA sf1 (FDE f2 f2ne) = cpXE sf1 f2 f2ne @@ -204,13 +204,13 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} cpCX b (SFAcc _ _ _ cne) = sfConst (vfyNoEv b cne) cpCX b (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 fd23 - cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI - where - tf dt _ = (cpCX b sf2', c) - where - (sf2', c) = (sfTF' sf2) dt b + cpCX b sf2 = SFCpAXA tf (FDC b) sf2 FDI + where + tf dt _ = (cpCX b sf2', c) + where + (sf2', c) = (sfTF' sf2) dt b --- For SPJ: The following version did not work. +-- For SPJ: The following version did not work. -- The commented out one below did work, by lambda-lifting cpCXAux cpCXA :: b -> SF' b c -> FunDesc c d -> SF' a d cpCXA b sf2 FDI = cpCX b sf2 @@ -219,7 +219,7 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} where f3 = fdFun fd3 - cpCXAAux :: SF' b c -> SF' a d + cpCXAAux :: SF' b c -> SF' a d cpCXAAux (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b)) cpCXAAux (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne)) cpCXAAux (SFCpAXA _ fd21 sf22 fd23) = cpCXA ((fdFun fd21) b) sf22 (fdComp fd23 fd3) @@ -231,7 +231,7 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} cpCXA b sf2 fd3 = cpCXAAux b fd3 (fdFun fd3) sf2 where -- f3 = fdFun fd3 - -- Really something like: cpCXAAux :: SF' b c -> SF' a d + -- Really something like: cpCXAAux :: SF' b c -> SF' a d cpCXAAux :: b -> FunDesc c d -> (c -> d) -> SF' b c -> SF' a d cpCXAAux b fd3 f3 (SFArr _ fd2) = sfConst (f3 ((fdFun fd2) b)) cpCXAAux b fd3 f3 (SFAcc _ _ _ cne) = sfConst (vfyNoEv b (f3 cne)) @@ -239,44 +239,44 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} -} cpGX :: (a -> b) -> SF' b c -> SF' a c - cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2) + cpGX f1 (SFArr _ fd2) = sfArr (fdComp (FDG f1) fd2) cpGX f1 (SFCpAXA _ fd21 sf22 fd23) = cpAXA (fdComp (FDG f1) fd21) sf22 fd23 - cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI - where - tf dt a = (cpGX f1 sf2', c) - where - (sf2', c) = (sfTF' sf2) dt (f1 a) + cpGX f1 sf2 = SFCpAXA tf (FDG f1) sf2 FDI + where + tf dt a = (cpGX f1 sf2', c) + where + (sf2', c) = (sfTF' sf2) dt (f1 a) cpXG :: SF' a b -> (b -> c) -> SF' a c - cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2)) + cpXG (SFArr _ fd1) f2 = sfArr (fdComp fd1 (FDG f2)) cpXG (SFAcc _ f1 s bne) f2 = sfAcc f s (f2 bne) where f s a = let (s', b) = f1 s a in (s', f2 b) - cpXG (SFCpAXA _ fd11 sf12 fd22) f2 = + cpXG (SFCpAXA _ fd11 sf12 fd22) f2 = cpAXA fd11 sf12 (fdComp fd22 (FDG f2)) - cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2) - where - tf dt a = (cpXG sf1' f2, f2 b) - where - (sf1', b) = (sfTF' sf1) dt a + cpXG sf1 f2 = SFCpAXA tf FDI sf1 (FDG f2) + where + tf dt a = (cpXG sf1' f2, f2 b) + where + (sf1', b) = (sfTF' sf1) dt a cpEX :: (Event a -> b) -> b -> SF' b c -> SF' (Event a) c - cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2) - cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne) + cpEX f1 f1ne (SFArr _ fd2) = sfArr (fdComp (FDE f1 f1ne) fd2) + cpEX f1 f1ne (SFAcc _ f2 s cne) = sfAcc f s (vfyNoEv f1ne cne) where f s a = f2 s (fromEvent (f1 (Event a))) - cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) = + cpEX f1 f1ne (SFCpAXA _ fd21 sf22 fd23) = cpAXA (fdComp (FDE f1 f1ne) fd21) sf22 fd23 - cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI - where - tf dt ea = (cpEX f1 f1ne sf2', c) - where + cpEX f1 f1ne sf2 = SFCpAXA tf (FDE f1 f1ne) sf2 FDI + where + tf dt ea = (cpEX f1 f1ne sf2', c) + where (sf2', c) = case ea of - NoEvent -> (sfTF' sf2) dt f1ne - _ -> (sfTF' sf2) dt (f1 ea) + NoEvent -> (sfTF' sf2) dt f1ne + _ -> (sfTF' sf2) dt (f1 ea) - cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c + cpXE :: SF' a (Event b) -> (Event b -> c) -> c -> SF' a c cpXE (SFArr _ fd1) f2 f2ne = sfArr (fdComp fd1 (FDE f2 f2ne)) cpXE (SFAcc _ f1 s bne) f2 f2ne = sfAcc f s (vfyNoEv bne f2ne) where @@ -285,9 +285,9 @@ compPrim (SF {sfTF = tf10}) (SF {sfTF = tf20}) = SF {sfTF = tf0} case eb of NoEvent -> (s', f2ne); _ -> (s', f2 eb) cpXE (SFCpAXA _ fd11 sf12 fd13) f2 f2ne = cpAXA fd11 sf12 (fdComp fd13 (FDE f2 f2ne)) - cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne) - where - tf dt a = (cpXE sf1' f2 f2ne, + cpXE sf1 f2 f2ne = SFCpAXA tf FDI sf1 (FDE f2 f2ne) + where + tf dt a = (cpXE sf1' f2 f2ne, case eb of NoEvent -> f2ne; _ -> f2 eb) - where + where (sf1', eb) = (sfTF' sf1) dt a diff --git a/testsuite/tests/gadt/T3169.hs b/testsuite/tests/gadt/T3169.hs index b52ec2cf87..bc4326c8a4 100644 --- a/testsuite/tests/gadt/T3169.hs +++ b/testsuite/tests/gadt/T3169.hs @@ -9,8 +9,8 @@ class Key k where instance (Key a, Key b) => Key (a,b) where type Map (a,b) = MP a b - lookup (a,b) (m :: Map (a,b) elt) + lookup (a,b) (m :: Map (a,b) elt) = case lookup a m :: Maybe (Map b elt) of - Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt + Just (m2 :: Map b elt) -> lookup b m2 :: Maybe elt data MP a b elt = MP (Map a (Map b elt)) diff --git a/testsuite/tests/gadt/T7205.hs b/testsuite/tests/gadt/T7205.hs index e8c555972f..e6f0eb25b3 100644 --- a/testsuite/tests/gadt/T7205.hs +++ b/testsuite/tests/gadt/T7205.hs @@ -7,9 +7,9 @@ data Abs env g v where class Eval g env h v where eval :: env -> g env h v -> v -evalAbs :: Eval g2 (a2, env) h2 v2 - => env - -> Abs env (g2 (a2, env) h2 v2) (a2->v2) - -> (a2->v2) -evalAbs env (Abs e) x +evalAbs :: Eval g2 (a2, env) h2 v2 + => env + -> Abs env (g2 (a2, env) h2 v2) (a2->v2) + -> (a2->v2) +evalAbs env (Abs e) x = eval (x, env) e -- e :: g (a,env) h v diff --git a/testsuite/tests/gadt/gadt2.hs b/testsuite/tests/gadt/gadt2.hs index 886b702ce7..d1c6b4d7af 100644 --- a/testsuite/tests/gadt/gadt2.hs +++ b/testsuite/tests/gadt/gadt2.hs @@ -15,4 +15,4 @@ g (T n) | n >= 3 = if n>3 then GT else EQ g (T n) = LT main = do print [f (T 0), f (T 1)] - print [g (T 2), g (T 3), g (T 4)] + print [g (T 2), g (T 3), g (T 4)] diff --git a/testsuite/tests/gadt/gadt25.hs b/testsuite/tests/gadt/gadt25.hs index 99aecad3fb..452da8cd4a 100644 --- a/testsuite/tests/gadt/gadt25.hs +++ b/testsuite/tests/gadt/gadt25.hs @@ -5,7 +5,7 @@ module Foo where data TValue t where - TList :: [a] -> TValue [a] + TList :: [a] -> TValue [a] instance (Eq b) => Eq (TValue b) where (==) (TList p) (TList q) = (==) p q @@ -15,19 +15,19 @@ instance (Eq b) => Eq (TValue b) where Here's the reasoning (I have done a bit of renaming). * The TList constructor really has type - TList :: forall a. forall x. (a~[x]) => [x] -> TValue a + TList :: forall a. forall x. (a~[x]) => [x] -> TValue a * So in the pattern match we have - (Eq b) available from the instance header - TList p :: TValue b - x is a skolem, existentially bound by the pattern - p :: [x] - b ~ [x] available from the pattern match + (Eq b) available from the instance header + TList p :: TValue b + x is a skolem, existentially bound by the pattern + p :: [x] + b ~ [x] available from the pattern match * On the RHS we find we need (Eq [x]). * So the constraint problem we have is - (Eq b, b~[x]) => Eq [x] + (Eq b, b~[x]) => Eq [x] ["Given" => "Wanted"] Can we prove this? From the two given constraints we can see that we also have Eq [x], and that certainly proves Eq [x]. @@ -38,4 +38,4 @@ consequences of the "given" constraints, we might use the top-level Eq a => Eq [a] instance to solve the wanted Eq [x]. And now we need Eq x, which *isn't* a consequence of (Eq b, b~[x]). --}
\ No newline at end of file +-} diff --git a/testsuite/tests/gadt/gadt5.hs b/testsuite/tests/gadt/gadt5.hs index 5db3deef8c..2dce68fffa 100644 --- a/testsuite/tests/gadt/gadt5.hs +++ b/testsuite/tests/gadt/gadt5.hs @@ -3,21 +3,21 @@ module Main where data Term a where - Lit :: Int -> Term Int + Lit :: Int -> Term Int IsZero :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a - Pr :: Term a -> Term b -> Term (a, b) - Fst :: Term (a, b) -> Term a - Snd :: Term (a, b) -> Term b + Pr :: Term a -> Term b -> Term (a, b) + Fst :: Term (a, b) -> Term a + Snd :: Term (a, b) -> Term b eval :: Term v -> v -eval (Lit n) = n +eval (Lit n) = n eval (IsZero t) = eval t == 0 eval (If t1 t2 t3) = if eval t1 then eval t2 else eval t3 eval (Pr t1 t2) = (eval t1, eval t2) -eval (Fst t) = case (eval t) of { (a,b) -> a } -eval (Snd t) = case (eval t) of { (a,b) -> b } +eval (Fst t) = case (eval t) of { (a,b) -> a } +eval (Snd t) = case (eval t) of { (a,b) -> b } term = If (IsZero (Lit 1)) (Pr (Lit 2) (Lit 3)) (Pr (Lit 3) (Lit 4)) -main = print (eval term)
\ No newline at end of file +main = print (eval term) diff --git a/testsuite/tests/gadt/gadt8.hs b/testsuite/tests/gadt/gadt8.hs index 1cad8f65cc..ebd8b04c49 100644 --- a/testsuite/tests/gadt/gadt8.hs +++ b/testsuite/tests/gadt/gadt8.hs @@ -1,15 +1,15 @@ {-# LANGUAGE GADTs, KindSignatures #-} -- Test a couple of trivial things: --- explicit layout --- trailing semicolons --- kind signatures +-- explicit layout +-- trailing semicolons +-- kind signatures module ShouldCompile where data Expr :: * -> * where { EInt :: Int -> Expr Int ; EBool :: Bool -> Expr Bool ; EIf :: (Expr Bool) -> (Expr a) -> (Expr a) -> Expr a ; - -- Note trailing semicolon, should be ok + -- Note trailing semicolon, should be ok } diff --git a/testsuite/tests/gadt/josef.hs b/testsuite/tests/gadt/josef.hs index 3be7dc28dc..34bd41ba3f 100644 --- a/testsuite/tests/gadt/josef.hs +++ b/testsuite/tests/gadt/josef.hs @@ -1,7 +1,7 @@ {-# LANGUAGE GADTs, KindSignatures, MultiParamTypeClasses, FunctionalDependencies #-} --- Program from Josef Svenningsson +-- Program from Josef Svenningsson -- Just a short explanation of the program. It contains -- some class declarations capturing some definitions from @@ -10,7 +10,7 @@ -- function defining the semantics for lambda terms called -- 'interp'. --- Made GHC 6.4 bleat +-- Made GHC 6.4 bleat -- Quantified type variable `t' is unified with -- another quantified type variable `terminal' -- When trying to generalise the type inferred for `interp' @@ -38,14 +38,14 @@ class Category arr => inRight :: arr b (coprod a b) ccase :: arr a c -> arr b c -> arr (coprod a b) c -class ProductCategory prod arr => +class ProductCategory prod arr => Exponential exp prod arr | arr -> exp where eval :: arr (prod (exp a b) a) b curryA :: arr (prod c a) b -> arr c (exp a b) -class (Exponential exp prod arr, Terminal terminal arr) => - CartesianClosed terminal exp prod arr | arr -> terminal exp prod +class (Exponential exp prod arr, Terminal terminal arr) => + CartesianClosed terminal exp prod arr | arr -> terminal exp prod data V prod env t where Z :: V prod (prod env t) t @@ -55,13 +55,13 @@ data Lambda terminal (exp :: * -> * -> *) prod env t where Unit :: Lambda foo exp prod env foo Var :: V prod env t -> Lambda terminal exp prod env t {- Lam :: Lambda terminal exp prod (prod env a) t - -> Lambda terminal exp prod env (exp a t) - App :: Lambda terminal exp prod env (exp t t') - -> Lambda terminal exp prod env t -> Lambda terminal exp prod env t' + -> Lambda terminal exp prod env (exp a t) + App :: Lambda terminal exp prod env (exp t t') + -> Lambda terminal exp prod env t -> Lambda terminal exp prod env t' -} -interp :: CartesianClosed terminal exp prod arr => - Lambda terminal exp prod s t -> arr s t +interp :: CartesianClosed terminal exp prod arr => + Lambda terminal exp prod s t -> arr s t interp (Unit) = terminal -- Terminal terminal arr => arr a terminal -- interp (Var Z) = second -- interp (Var (S v)) = first `comp` interp (Var v) diff --git a/testsuite/tests/gadt/nbe.hs b/testsuite/tests/gadt/nbe.hs index 60141291fc..103319ad1d 100644 --- a/testsuite/tests/gadt/nbe.hs +++ b/testsuite/tests/gadt/nbe.hs @@ -11,10 +11,10 @@ data Ty t where Arr :: Ty a -> Ty b -> Ty (a -> b) data Exp g t where - Var :: Var g t -> Exp g t - Lam :: Ty a -> Exp (g,a) b -> Exp g (a->b) - App :: Exp g (s -> t) -> Exp g s -> Exp g t - If :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t + Var :: Var g t -> Exp g t + Lam :: Ty a -> Exp (g,a) b -> Exp g (a->b) + App :: Exp g (s -> t) -> Exp g s -> Exp g t + If :: Exp g Bool -> Exp g t -> Exp g t -> Exp g t ETrue :: Exp g Bool EFalse :: Exp g Bool @@ -72,12 +72,12 @@ data TyEnv g where Cons :: Ty t -> TyEnv h -> TyEnv (h,t) infer :: TyEnv g -> Exp g t -> Ty t -infer g (Var x) = inferVar g x -infer g (Lam t e) = Arr t (infer (Cons t g) e) -infer g (App e e') = case infer g e of Arr _ t -> t -infer g (ETrue) = Bool -infer g (EFalse) = Bool -infer g (If _ e _) = infer g e +infer g (Var x) = inferVar g x +infer g (Lam t e) = Arr t (infer (Cons t g) e) +infer g (App e e') = case infer g e of Arr _ t -> t +infer g (ETrue) = Bool +infer g (EFalse) = Bool +infer g (If _ e _) = infer g e inferVar :: TyEnv g -> Var g t -> Ty t inferVar (Cons t h) (SVar x) = inferVar h x @@ -87,8 +87,8 @@ inferVar (Cons t h) (ZVar) = t data Tree a = Val a | Choice (Tree a) (Tree a) -- doesn't yet force trees to be fully balanced: --- Val :: a -> Tree a Z --- Choice :: Tree a n -> Tree a n -> Tree a (S n) +-- Val :: a -> Tree a Z +-- Choice :: Tree a n -> Tree a n -> Tree a (S n) instance Functor Tree where fmap = liftM @@ -114,8 +114,8 @@ flatten t = flatten_ t [] -- quote & friends ------------------------------------------------------------- -- for values -------------------------- -enumV :: Ty t -> Tree t -questionsV :: Ty t -> [t -> Bool] +enumV :: Ty t -> Tree t +questionsV :: Ty t -> [t -> Bool] enumV Bool = Choice (Val True) (Val False) @@ -123,46 +123,46 @@ enumV (Arr s t) = mkEnum (questionsV s) (enumV t) where mkEnum [] t = tmap const t mkEnum (q:qs) es = do - f1 <- mkEnum qs es - f2 <- mkEnum qs es - return (\d -> if q d then f1 d else f2 d) + f1 <- mkEnum qs es + f2 <- mkEnum qs es + return (\d -> if q d then f1 d else f2 d) -questionsV Bool = return (\x -> x) -questionsV (Arr s t) = do - d <- flatten (enumV s) - q <- questionsV t - return (\f -> q (f d)) +questionsV Bool = return (\x -> x) +questionsV (Arr s t) = do + d <- flatten (enumV s) + q <- questionsV t + return (\f -> q (f d)) -- for expressions --------------------- -enumE :: Ty t -> Tree (Exp g t) -questionsE :: Ty t -> [Exp g t -> Exp g Bool] +enumE :: Ty t -> Tree (Exp g t) +questionsE :: Ty t -> [Exp g t -> Exp g Bool] enumE Bool = Choice (Val ETrue) (Val EFalse) enumE (Arr s t) = tmap (lamE s) (mkEnumE (questionsE s) (enumE t)) where mkEnumE [] t = tmap const t mkEnumE (q:qs) es = do - f1 <- mkEnumE qs es - f2 <- mkEnumE qs es - return (\d -> ifE (q d) (f1 d) (f2 d)) - -questionsE Bool = return (\x -> x) -questionsE (Arr s t) = do - d <- flatten (enumE s) - q <- questionsE t - return (\f -> q (App f d)) - --- should be --- find (List (Exp g Bool) n) -> Tree (Exp g a) n -> Exp g a + f1 <- mkEnumE qs es + f2 <- mkEnumE qs es + return (\d -> ifE (q d) (f1 d) (f2 d)) + +questionsE Bool = return (\x -> x) +questionsE (Arr s t) = do + d <- flatten (enumE s) + q <- questionsE t + return (\f -> q (App f d)) + +-- should be +-- find (List (Exp g Bool) n) -> Tree (Exp g a) n -> Exp g a find :: [Exp g Bool] -> Tree (Exp g a) -> Exp g a -find [] (Val a) = a -find (b:bs) (Choice l r) = ifE b (find bs l) (find bs r) -find _ _ = error "bad arguments to find" +find [] (Val a) = a +find (b:bs) (Choice l r) = ifE b (find bs l) (find bs r) +find _ _ = error "bad arguments to find" quote :: Ty t -> t -> Exp g t quote Bool t = case t of True -> ETrue; False -> EFalse quote (Arr s t) f = lamE s (\e -> find (do q <- questionsE s; return (q e)) - (tmap (quote t . f) (enumV s))) + (tmap (quote t . f) (enumV s))) -- normalization (by evaluation) ----------------------------------------------- data BoxExp t = Box (forall g. Exp g t) @@ -183,4 +183,4 @@ test = [ eqB (nf b22b thrice) (nf b22b once) , eqB (nf b22b twice) (nf b22b once)] where nf = normalize -main = print test
\ No newline at end of file +main = print test diff --git a/testsuite/tests/gadt/records.hs b/testsuite/tests/gadt/records.hs index e28add3fb6..eaa2fd4196 100644 --- a/testsuite/tests/gadt/records.hs +++ b/testsuite/tests/gadt/records.hs @@ -18,8 +18,7 @@ g (T1 {x=xv, y=yv}) = T2 { x = xv } h v = x v + 1 main = do { let t1 = T1 { y = "foo", x = 4 } - t2 = g t1 - ; print (h (f 8 undefined)) - ; print (h t2) - } -
\ No newline at end of file + t2 = g t1 + ; print (h (f 8 undefined)) + ; print (h t2) + } diff --git a/testsuite/tests/gadt/red-black.hs b/testsuite/tests/gadt/red-black.hs index 29bb324310..016ac83017 100644 --- a/testsuite/tests/gadt/red-black.hs +++ b/testsuite/tests/gadt/red-black.hs @@ -5,7 +5,7 @@ module ShouldCompile where -- data RBTree = forall n. Root (SubTree Black n) -- Kind Colour -data Red +data Red data Black -- Kind Nat @@ -20,12 +20,12 @@ data SubTree c n where ins :: Int -> SubTree c n -> SubTree c n -ins n Leaf = (Fix (RNode Leaf n Leaf)) +ins n Leaf = (Fix (RNode Leaf n Leaf)) ins n (BNode x m y) | n <= m = black (ins n x) m y ins n (BNode x m y) | n > m = black x m (ins n y) ins n (RNode x m y) | n <= m = RNode (ins n x) m y ins n (RNode x m y) | n > m = RNode x m (ins n y) - + black :: SubTree c n -> Int -> SubTree d n -> SubTree Black (S n) black (RNode (Fix u) v c) w (x@(RNode _ _ _)) = Fix(RNode (blacken u) v (BNode c w x)) diff --git a/testsuite/tests/gadt/scoped.hs b/testsuite/tests/gadt/scoped.hs index cafa738697..ea321a53c4 100644 --- a/testsuite/tests/gadt/scoped.hs +++ b/testsuite/tests/gadt/scoped.hs @@ -28,6 +28,6 @@ g2 (C (p :: x)) = () g3 :: forall x y . D x y -> () -- D (..) :: D x y -- C (..) :: C sk y --- sk = y +-- sk = y -- p :: sk g3 (D (C (p :: y))) = () diff --git a/testsuite/tests/gadt/set.hs b/testsuite/tests/gadt/set.hs index 3a78bbb64b..daafe8e22a 100644 --- a/testsuite/tests/gadt/set.hs +++ b/testsuite/tests/gadt/set.hs @@ -1,6 +1,6 @@ {-# LANGUAGE GADTs #-} --- Provoked by +-- Provoked by -- http://www.haskell.org/pipermail/haskell-cafe/2007-January/021086.html module ShouldCompile where @@ -29,7 +29,7 @@ unionC1 (SM1 p1 m1) (SM1 p2 m2) --------------------- data SetM2 a where SM2 :: Ord w => Teq a w -> Set.Set w -> SetM2 a - -- Different order of args in Teq + -- Different order of args in Teq unionA2 :: SetM2 a -> SetM2 a -> SetM2 a unionA2 (SM2 Teq m1) (SM2 Teq m2) @@ -40,6 +40,6 @@ unionB2 (SM2 p1 m1) (SM2 p2 m2) = case p1 of Teq -> case p2 of Teq -> SM2 Teq (m1 `Set.union` m2) unionC2 :: SetM2 a -> SetM2 a -> SetM2 a -unionC2 (SM2 p1 m1) (SM2 p2 m2) +unionC2 (SM2 p1 m1) (SM2 p2 m2) = case (p1,p2) of (Teq,Teq) -> SM2 Teq (m1 `Set.union` m2) diff --git a/testsuite/tests/gadt/termination.hs b/testsuite/tests/gadt/termination.hs index f290322fa5..920091b7f1 100644 --- a/testsuite/tests/gadt/termination.hs +++ b/testsuite/tests/gadt/termination.hs @@ -164,20 +164,20 @@ test4 :: NonTerminating test4 = NonTerminating (Apply omega omega) help3 help1 :: Reducible (Apply Omega Omega) -help1 = Reducible (ReduceSimple - (ReplaceApply (ReplaceVarEq Equal (LiftLambda - (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero)))) - (ReplaceVarEq Equal (LiftLambda (LiftApply - (LiftVarLess LessZero) (LiftVarLess LessZero)))))) +help1 = Reducible (ReduceSimple + (ReplaceApply (ReplaceVarEq Equal (LiftLambda + (LiftApply (LiftVarLess LessZero) (LiftVarLess LessZero)))) + (ReplaceVarEq Equal (LiftLambda (LiftApply + (LiftVarLess LessZero) (LiftVarLess LessZero)))))) help2 :: ReduceEventually (Apply Omega Omega) t -> Equal (Apply Omega Omega) t help2 ReduceZero = Equal -help2 (ReduceSucc (ReduceSimple (ReplaceApply - (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))) - (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y) +help2 (ReduceSucc (ReduceSimple (ReplaceApply + (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))) + (ReplaceVarEq _ (LiftLambda (LiftApply (LiftVarLess _) (LiftVarLess _)))))) y) = case help2 y of Equal -> Equal help3 :: Infinite (Apply Omega Omega) help3 x = case help2 x of - Equal -> help1 + Equal -> help1 diff --git a/testsuite/tests/gadt/ubx-records.hs b/testsuite/tests/gadt/ubx-records.hs index ab21dc65fe..c31b66ffd4 100644 --- a/testsuite/tests/gadt/ubx-records.hs +++ b/testsuite/tests/gadt/ubx-records.hs @@ -9,7 +9,7 @@ data T a where T1 :: { w :: !(Int, Int), x :: a, y :: b } -> T (a,b) T2 :: { w :: !(Int, Int), x :: a } -> T (a,b) T3 :: { z :: Int } -> T Bool - + -- T1 :: forall c a b. (c~(a,b)) => (Int,Int) -> a -> b -> T c f xv yv = T1 { w = (0,0), x = xv, y = yv } @@ -23,8 +23,8 @@ h v = x v + 1 i v = let (x,y) = w v in x + y main = do { let t1 = T1 { w = (0,0), y = "foo", x = 4 } - t2 = g t1 - ; print (h (f 8 undefined)) - ; print (h t2) + t2 = g t1 + ; print (h (f 8 undefined)) + ; print (h t2) ; print (i t1) - } + } diff --git a/testsuite/tests/gadt/while.hs b/testsuite/tests/gadt/while.hs index 2040511c0f..c5bbcde9ff 100644 --- a/testsuite/tests/gadt/while.hs +++ b/testsuite/tests/gadt/while.hs @@ -7,21 +7,21 @@ succeed = return data V s t where Z :: V (t,m) t - S :: V m t -> V (x,m) t - + S :: V m t -> V (x,m) t + data Exp s t where - IntC :: Int -> Exp s Int -- 5 - BoolC :: Bool -> Exp s Bool -- True - Plus :: Exp s Int -> Exp s Int -> Exp s Int -- x + 3 - Lteq :: Exp s Int -> Exp s Int -> Exp s Bool -- x <= 3 - Var :: V s t -> Exp s t -- x + IntC :: Int -> Exp s Int -- 5 + BoolC :: Bool -> Exp s Bool -- True + Plus :: Exp s Int -> Exp s Int -> Exp s Int -- x + 3 + Lteq :: Exp s Int -> Exp s Int -> Exp s Bool -- x <= 3 + Var :: V s t -> Exp s t -- x data Com s where - Set :: V s t -> Exp s t -> Com s -- x := e - Seq :: Com s -> Com s -> Com s -- { s1; s2; } - If :: Exp s Bool -> Com s -> Com s -> Com s -- if e then x else y - While :: Exp s Bool -> Com s -> Com s -- while e do s - Declare :: Exp s t -> Com (t,s) -> Com s -- { int x = 5; s } + Set :: V s t -> Exp s t -> Com s -- x := e + Seq :: Com s -> Com s -> Com s -- { s1; s2; } + If :: Exp s Bool -> Com s -> Com s -> Com s -- if e then x else y + While :: Exp s Bool -> Com s -> Com s -- while e do s + Declare :: Exp s t -> Com (t,s) -> Com s -- { int x = 5; s } update :: (V s t) -> t -> s -> s update Z n (x,y) = (n,y) @@ -42,8 +42,8 @@ exec (Seq x y) s = exec y (exec x s) exec (If test x1 x2) s = if (eval test s) then exec x1 s else exec x2 s exec (While test body) s = loop s - where loop s = if (eval test s) - then loop (exec body s) + where loop s = if (eval test s) + then loop (exec body s) else s exec (Declare e body) s = store where (_,store) = (exec body (eval e s,s)) @@ -54,19 +54,19 @@ v2 = S (S Z) v3 = S (S (S Z)) e2 = Lteq (Plus (Var v0)(Var v1)) (Plus (Var v0) (IntC 1)) - + sum_var = Z x = S Z prog :: Com (Int,(Int,a)) -prog = +prog = Seq (Set sum_var (IntC 0)) (Seq (Set x (IntC 1)) (While (Lteq (Var x) (IntC 5)) (Seq (Set sum_var (Plus (Var sum_var)(Var x))) (Set x (Plus (Var x) (IntC 1)))))) - -ans = exec prog (34,(12,1)) + +ans = exec prog (34,(12,1)) main = print ans {- { sum = 0 ; @@ -75,7 +75,7 @@ main = print ans { sum = sum + x; x = x + 1; } -} +} -} @@ -87,15 +87,15 @@ data TyAst = I | B | P TyAst TyAst data TypeR t where IntR :: TypeR Int BoolR :: TypeR Bool - PairR :: TypeR a -> TypeR b -> TypeR (a,b) + PairR :: TypeR a -> TypeR b -> TypeR (a,b) -- Judgments for Types -data TJudgment = forall t . TJ (TypeR t) +data TJudgment = forall t . TJ (TypeR t) checkT :: TyAst -> TJudgment checkT I = TJ IntR checkT B = TJ BoolR -checkT (P x y) = +checkT (P x y) = case (checkT x,checkT y) of (TJ a, TJ b) -> TJ(PairR a b) @@ -111,7 +111,7 @@ match (PairR a b) (PairR c d) = do { EqProof <- match a c ; EqProof <- match b d ; succeed EqProof } -match _ _ = fail "match fails" +match _ _ = fail "match fails" ---------------------------------------------- @@ -121,13 +121,13 @@ checkV :: Int -> TypeR t -> TypeR s -> Maybe(V s t) checkV 0 t1 (PairR t2 p) = do { EqProof <- match t1 t2 ; return Z } -checkV n t1 (PairR ty p) = +checkV n t1 (PairR ty p) = do { v <- checkV (n-1) t1 p; return(S v)} checkV n t1 sr = Nothing ----------------------------------------------------- -data ExpAst +data ExpAst = IntCA Int | BoolCA Bool | PlusA ExpAst ExpAst @@ -135,7 +135,7 @@ data ExpAst | VarA Int TyAst -- Judgments for Expressions -data EJudgment s = forall t . EJ (TypeR t) (Exp s t) +data EJudgment s = forall t . EJ (TypeR t) (Exp s t) checkE :: ExpAst -> TypeR s -> Maybe (EJudgment s) checkE (IntCA n) sr = succeed(EJ IntR (IntC n)) @@ -146,13 +146,13 @@ checkE (PlusA x y) sr = ; EJ t2 e2 <- checkE y sr ; EqProof <- match t2 IntR ; succeed(EJ IntR (Plus e1 e2))} -checkE (VarA n ty) sr = +checkE (VarA n ty) sr = do { TJ t <- succeed(checkT ty) - ; v <- checkV n t sr + ; v <- checkV n t sr ; return(EJ t (Var v)) } ----------------------------------------------------- -data ComAst +data ComAst = SetA Int TyAst ExpAst | SeqA ComAst ComAst | IfA ExpAst ComAst ComAst @@ -168,22 +168,22 @@ checkC (SetA n ty e) sr = ; EJ t2 e1 <- checkE e sr ; EqProof <- match t1 t2 ; return(EC (Set v e1))} -checkC (SeqA x y) sr = +checkC (SeqA x y) sr = do { EC c1 <- checkC x sr ; EC c2 <- checkC y sr ; return(EC (Seq c1 c2)) } -checkC (IfA e x y) sr = +checkC (IfA e x y) sr = do { EJ t1 e1 <- checkE e sr ; EqProof <- match t1 BoolR ; EC c1 <- checkC x sr ; EC c2 <- checkC y sr ; return(EC(If e1 c1 c2)) } -checkC (WhileA e x) sr = +checkC (WhileA e x) sr = do { EJ t1 e1 <- checkE e sr ; EqProof <- match t1 BoolR ; EC c1 <- checkC x sr ; return(EC(While e1 c1)) } -checkC (DeclareA ty e c) sr = +checkC (DeclareA ty e c) sr = do { TJ t1 <- succeed(checkT ty) ; EJ t2 e2 <- checkE e sr ; EqProof <- match t1 t2 @@ -195,7 +195,7 @@ checkC (DeclareA ty e c) sr = e1 = Lteq (Plus (Var sum_var)(Var x)) (Plus (Var x) (IntC 1)) {- -data Store s +data Store s = M (Code s) | forall a b . N (Code a) (Store b) where s = (a,b) @@ -213,4 +213,4 @@ eval2 (Var (S v)) (M x) = eval2 (Var v) (M [| snd $x |]) test e = [| \ (x,(y,z)) -> $(eval2 e (N [|x|] (N [|y|] (M [|z|])))) |] -- test e1 ---> [| \ (x,(y,z)) -> x + y <= y + 1 |] --}
\ No newline at end of file +-} |