Testsuite: delete Windows line endings [skip ci] (#11631)
authorThomas Miedema <thomasmiedema@gmail.com>
Mon, 22 Feb 2016 20:32:51 +0000 (21:32 +0100)
committerThomas Miedema <thomasmiedema@gmail.com>
Tue, 23 Feb 2016 11:27:57 +0000 (12:27 +0100)
34 files changed:
testsuite/tests/deriving/should_compile/T3012.hs
testsuite/tests/deriving/should_compile/T6031.hs
testsuite/tests/deriving/should_compile/T6031a.hs
testsuite/tests/deriving/should_compile/T8893.hs
testsuite/tests/deriving/should_fail/T2701.hs
testsuite/tests/deriving/should_fail/T4846.hs
testsuite/tests/deriving/should_run/T4136.hs
testsuite/tests/deriving/should_run/drvrun019.hs
testsuite/tests/driver/Shared001.hs
testsuite/tests/driver/recomp010/X1.hs
testsuite/tests/driver/recomp010/X2.hs
testsuite/tests/dynlibs/T4464H.hs
testsuite/tests/eyeball/inline4.hs
testsuite/tests/eyeball/record1.hs
testsuite/tests/ffi/should_compile/ffi-deriv1.hs
testsuite/tests/ffi/should_run/T1288.hs
testsuite/tests/ffi/should_run/T1288_ghci.hs
testsuite/tests/ffi/should_run/T2276.hs
testsuite/tests/ffi/should_run/T2276_ghci.hs
testsuite/tests/ffi/should_run/ffi014.hs
testsuite/tests/gadt/Arith.hs
testsuite/tests/gadt/T2587.hs
testsuite/tests/gadt/data1.hs
testsuite/tests/gadt/data2.hs
testsuite/tests/gadt/gadt-fd.hs
testsuite/tests/gadt/gadt14.hs
testsuite/tests/gadt/gadt18.hs
testsuite/tests/gadt/gadt9.hs
testsuite/tests/gadt/karl1.hs
testsuite/tests/gadt/karl2.hs
testsuite/tests/gadt/lazypat.hs
testsuite/tests/gadt/lazypatok.hs
testsuite/tests/gadt/rw.hs
testsuite/tests/gadt/tc.hs

index 44b1d64..e897bfb 100644 (file)
@@ -1,10 +1,10 @@
-{-# LANGUAGE GADTs, StandaloneDeriving #-}\r
-\r
-module T3012 where\r
-\r
-data T a where\r
-    Foo :: T Int\r
-    Bar :: T Bool\r
-\r
-deriving instance Show (T a)\r
-\r
+{-# LANGUAGE GADTs, StandaloneDeriving #-}
+
+module T3012 where
+
+data T a where
+    Foo :: T Int
+    Bar :: T Bool
+
+deriving instance Show (T a)
+
index b1ca4e1..eb0e712 100644 (file)
@@ -1,7 +1,7 @@
-{-# LANGUAGE StandaloneDeriving #-}\r
-\r
-module T6031 where\r
-\r
-import T6031a\r
-\r
-deriving instance Show Empty\r
+{-# LANGUAGE StandaloneDeriving #-}
+
+module T6031 where
+
+import T6031a
+
+deriving instance Show Empty
index 2ebcc94..8c69c45 100644 (file)
@@ -1,11 +1,11 @@
-{-# OPTIONS_GHC -Wall #-}\r
-{-# Language DeriveFunctor #-}\r
-{-# Language PolyKinds #-}\r
-\r
-module T8893 where\r
-\r
-data V a = V [a] deriving Functor\r
-\r
-data C x a = C (V (P x a)) deriving Functor\r
-\r
-data P x a = P (x a) deriving Functor\r
+{-# OPTIONS_GHC -Wall #-}
+{-# Language DeriveFunctor #-}
+{-# Language PolyKinds #-}
+
+module T8893 where
+
+data V a = V [a] deriving Functor
+
+data C x a = C (V (P x a)) deriving Functor
+
+data P x a = P (x a) deriving Functor
index 37bffc8..0d6dab3 100644 (file)
@@ -1,10 +1,10 @@
-{-# LANGUAGE MagicHash, DeriveDataTypeable #-}\r
-module T2700 where\r
-\r
-import GHC.Prim\r
-\r
-import Data.Data\r
-import Data.Typeable\r
-\r
-data Foo = MkFoo Int#\r
-           deriving (Typeable, Data)\r
+{-# LANGUAGE MagicHash, DeriveDataTypeable #-}
+module T2700 where
+
+import GHC.Prim
+
+import Data.Data
+import Data.Typeable
+
+data Foo = MkFoo Int#
+           deriving (Typeable, Data)
index 66621c0..e9cd180 100755 (executable)
@@ -1,37 +1,37 @@
-{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving, GADTs, GeneralizedNewtypeDeriving, DeriveDataTypeable #-}\r
-\r
-module Main where\r
-\r
-import Data.Typeable\r
-\r
-data Expr a where\r
-    Lit :: Typeable a => a -> Expr a\r
-\r
-class A a where\r
-    mk :: a\r
-\r
-class (Typeable a, A a) => B a where\r
-    mkExpr :: Expr a\r
-    mkExpr = Lit mk\r
-\r
--- dfunAE\r
-instance B a => A (Expr a) where\r
-    mk = mkExpr\r
-\r
--- dfunAB\r
-instance A Bool where\r
-    mk = True\r
-\r
-newtype BOOL = BOOL Bool\r
-  deriving (Typeable, A)\r
-\r
-instance B Bool\r
-deriving instance B BOOL   --dfunBB\r
-\r
-showType :: forall a . Expr a -> String\r
-showType (Lit _) = show (typeOf (undefined :: a))\r
-\r
-test1 = showType (mk     :: Expr BOOL) -- Prints "Bool" (wrong?)\r
-test2 = showType (Lit mk :: Expr BOOL) -- Prints "Main.BOOL" (correct)\r
-\r
-main = do { print test1; print test2 }\r
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving, GADTs, GeneralizedNewtypeDeriving, DeriveDataTypeable #-}
+
+module Main where
+
+import Data.Typeable
+
+data Expr a where
+    Lit :: Typeable a => a -> Expr a
+
+class A a where
+    mk :: a
+
+class (Typeable a, A a) => B a where
+    mkExpr :: Expr a
+    mkExpr = Lit mk
+
+-- dfunAE
+instance B a => A (Expr a) where
+    mk = mkExpr
+
+-- dfunAB
+instance A Bool where
+    mk = True
+
+newtype BOOL = BOOL Bool
+  deriving (Typeable, A)
+
+instance B Bool
+deriving instance B BOOL   --dfunBB
+
+showType :: forall a . Expr a -> String
+showType (Lit _) = show (typeOf (undefined :: a))
+
+test1 = showType (mk     :: Expr BOOL) -- Prints "Bool" (wrong?)
+test2 = showType (Lit mk :: Expr BOOL) -- Prints "Main.BOOL" (correct)
+
+main = do { print test1; print test2 }
index d47014b..c8363dc 100644 (file)
@@ -1,9 +1,9 @@
-module Main where\r
-\r
-data T = (:=:) {- | (:!=:) -} deriving (Show,Read)\r
-\r
-main\r
- = do  putStrLn ("show (:=:) = " ++ show (:=:))\r
-       putStrLn ("read (show (:=:)) :: T = " ++\r
-                  show (read (show (:=:)) :: T)) \r
-\r
+module Main where
+
+data T = (:=:) {- | (:!=:) -} deriving (Show,Read)
+
+main
+ = do  putStrLn ("show (:=:) = " ++ show (:=:))
+       putStrLn ("read (show (:=:)) :: T = " ++
+                  show (read (show (:=:)) :: T))
+
index 663fb38..c79d401 100644 (file)
@@ -1,15 +1,15 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-\r
--- Tests newtype deriving with\r
--- a non-type constructor in the representation\r
-\r
-module Main where\r
-\r
-newtype Wrap m a = Wrap { unWrap :: m a } \r
-    deriving (Functor, Applicative, Monad, Eq)\r
-\r
-foo :: Int -> Wrap IO a -> Wrap IO ()\r
-foo 0 a = return ()\r
-foo n a = do { a; foo (n-1) a }\r
-\r
-main = do { unWrap (foo 3 (Wrap (putChar 'x'))); putChar '\n' }\r
+
+-- Tests newtype deriving with
+-- a non-type constructor in the representation
+
+module Main where
+
+newtype Wrap m a = Wrap { unWrap :: m a }
+    deriving (Functor, Applicative, Monad, Eq)
+
+foo :: Int -> Wrap IO a -> Wrap IO ()
+foo 0 a = return ()
+foo n a = do { a; foo (n-1) a }
+
+main = do { unWrap (foo 3 (Wrap (putChar 'x'))); putChar '\n' }
index 4f6a3d9..4d827b8 100644 (file)
@@ -1,9 +1,9 @@
-{-# LANGUAGE ForeignFunctionInterface #-}\r
-module Shared001 where\r
-\r
--- Test for building DLLs with ghc -shared, see #2745\r
-\r
-f :: Int -> Int\r
-f x = x+1\r
-\r
-foreign export ccall f :: Int -> Int\r
+{-# LANGUAGE ForeignFunctionInterface #-}
+module Shared001 where
+
+-- Test for building DLLs with ghc -shared, see #2745
+
+f :: Int -> Int
+f x = x+1
+
+foreign export ccall f :: Int -> Int
index 7906d4b..84768c9 100644 (file)
@@ -1,10 +1,10 @@
-module X (x, D1(..), D2(..))\r
-where\r
-\r
-data D1 = D { f :: D2 } -- deriving Show\r
-data D2 = A | B -- deriving Show\r
-\r
-x :: D1\r
-x = D { f = A }\r
-\r
-\r
+module X (x, D1(..), D2(..))
+where
+
+data D1 = D { f :: D2 } -- deriving Show
+data D2 = A | B -- deriving Show
+
+x :: D1
+x = D { f = A }
+
+
index e120124..d57bda6 100644 (file)
@@ -1,10 +1,10 @@
-module X (x, D1(..), D2(..))\r
-where\r
-\r
-data D1 = D { f :: D2 } -- deriving Show\r
-data D2 = A | B -- deriving Show\r
-\r
-x :: D1\r
-x = D { f = B }\r
-\r
-\r
+module X (x, D1(..), D2(..))
+where
+
+data D1 = D { f :: D2 } -- deriving Show
+data D2 = A | B -- deriving Show
+
+x :: D1
+x = D { f = B }
+
+
index f620866..e3b511a 100644 (file)
@@ -1,7 +1,7 @@
-{-# LANGUAGE ForeignFunctionInterface #-}\r
-module T4464H where\r
-\r
-f :: Int -> Int\r
-f x = x + 1\r
-\r
-foreign export ccall f :: Int -> Int\r
+{-# LANGUAGE ForeignFunctionInterface #-}
+module T4464H where
+
+f :: Int -> Int
+f x = x + 1
+
+foreign export ccall f :: Int -> Int
index 2648c9e..a673de9 100644 (file)
@@ -1,40 +1,40 @@
-module CmmTx where\r
-\r
-data TxRes a = TxRes Bool a\r
-\r
-instance Monad TxRes where\r
-    return = TxRes False\r
-\r
-{-  Here you can get a simplifier loop thus:\r
-NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52\r
-NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52\r
-NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52\r
-NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52\r
-\r
-Reason: 'a' is inline (not pre/post unconditionally; just ordinary inlining)\r
-Then, since ($dm>>) has arity 3, the rhs of (>>) is a PAP, so the arg is\r
-floated out, past the big lambdas.\r
-\r
-See Note [Unsaturated functions] in SimplUtils \r
-\r
-------------------------------------------------------------\r
-a_s9f{v} [lid] =\r
-  base:GHC.Base.:DMonad{v r5} [gid]\r
-    @ main:CmmTx.TxRes{tc rd}\r
-    >>={v a6E} [lid]\r
-    >>{v a6H} [lid]\r
-    return{v a6J} [lid]\r
-    fail{v a6M} [lid]\r
->>{v a6H} [lid] [ALWAYS LoopBreaker Nothing] :: forall a{tv a6F} [tv]\r
-                                                       b{tv a6G} [tv].\r
-                                                main:CmmTx.TxRes{tc rd} a{tv a6F} [tv]\r
-                                                -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]\r
-                                                -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]\r
-[Arity 2\r
- Str: DmdType LL]\r
->>{v a6H} [lid] =\r
-  \ (@ a{tv a78} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d})\r
-    (@ b{tv a79} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d}) ->\r
-    base:GHC.Base.$dm>>{v r5f} [gid]\r
-      @ main:CmmTx.TxRes{tc rd} a_s9f{v} [lid] @ a{tv a78} [sk] @ b{tv a79} [sk]\r
- -}\r
+module CmmTx where
+
+data TxRes a = TxRes Bool a
+
+instance Monad TxRes where
+    return = TxRes False
+
+{-  Here you can get a simplifier loop thus:
+NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52
+NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52
+NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52
+NOTE: Simplifier still going after 4 iterations; bailing out.  Size = 52
+
+Reason: 'a' is inline (not pre/post unconditionally; just ordinary inlining)
+Then, since ($dm>>) has arity 3, the rhs of (>>) is a PAP, so the arg is
+floated out, past the big lambdas.
+
+See Note [Unsaturated functions] in SimplUtils
+
+------------------------------------------------------------
+a_s9f{v} [lid] =
+  base:GHC.Base.:DMonad{v r5} [gid]
+    @ main:CmmTx.TxRes{tc rd}
+    >>={v a6E} [lid]
+    >>{v a6H} [lid]
+    return{v a6J} [lid]
+    fail{v a6M} [lid]
+>>{v a6H} [lid] [ALWAYS LoopBreaker Nothing] :: forall a{tv a6F} [tv]
+                                                       b{tv a6G} [tv].
+                                                main:CmmTx.TxRes{tc rd} a{tv a6F} [tv]
+                                                -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]
+                                                -> main:CmmTx.TxRes{tc rd} b{tv a6G} [tv]
+[Arity 2
+ Str: DmdType LL]
+>>{v a6H} [lid] =
+  \ (@ a{tv a78} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d})
+    (@ b{tv a79} [sk] :: ghc-prim:GHC.Prim.*{(w) tc 34d}) ->
+    base:GHC.Base.$dm>>{v r5f} [gid]
+      @ main:CmmTx.TxRes{tc rd} a_s9f{v} [lid] @ a{tv a78} [sk] @ b{tv a79} [sk]
+ -}
index 1f9084b..dde6f5e 100644 (file)
@@ -1,17 +1,17 @@
--- Check that the record selector for maskMB unfolds in the body of f\r
--- At one stage it didn't because the implicit unfolding looked too big\r
-\r
--- Trac #2581\r
-\r
-module ShouldCompile where\r
-import Data.Array.Base\r
-\r
-data MBloom s a = MB {\r
-     shiftMB :: {-# UNPACK #-} !Int\r
-    , maskMB :: {-# UNPACK #-} !Int\r
-    , bitArrayMB :: {-# UNPACK #-} !(STUArray s Int Int)\r
-    }\r
-\r
-f a b c = case maskMB (MB a b c) of \r
-           3 -> True\r
-           _ -> False\r
+-- Check that the record selector for maskMB unfolds in the body of f
+-- At one stage it didn't because the implicit unfolding looked too big
+
+-- Trac #2581
+
+module ShouldCompile where
+import Data.Array.Base
+
+data MBloom s a = MB {
+     shiftMB :: {-# UNPACK #-} !Int
+    , maskMB :: {-# UNPACK #-} !Int
+    , bitArrayMB :: {-# UNPACK #-} !(STUArray s Int Int)
+    }
+
+f a b c = case maskMB (MB a b c) of
+            3 -> True
+            _ -> False
index 1e5d27a..dba0eaa 100644 (file)
@@ -1,25 +1,25 @@
-{-# LANGUAGE GeneralizedNewtypeDeriving #-}\r
-\r
--- Tests newtype unwrapping for the IO monad itself\r
--- Notice the RenderM monad, which is used in the\r
--- type of the callback function\r
-\r
-module ShouldCompile where\r
-\r
-import Control.Applicative (Applicative)\r
-\r
-import Foreign.Ptr\r
-newtype RenderM a = RenderM (IO a) deriving (Functor, Applicative, Monad)\r
-\r
-type RenderCallback = Int -> Int -> RenderM ()\r
-\r
-foreign import ccall duma_onRender :: FunPtr RenderCallback -> RenderM ()\r
-\r
-foreign import ccall "wrapper" mkRenderCallback\r
-     :: RenderCallback -> RenderM (FunPtr RenderCallback)\r
-\r
-onRender :: RenderCallback -> RenderM ()\r
-onRender f = mkRenderCallback f >>= duma_onRender\r
-\r
-\r
-\r
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+-- Tests newtype unwrapping for the IO monad itself
+-- Notice the RenderM monad, which is used in the
+-- type of the callback function
+
+module ShouldCompile where
+
+import Control.Applicative (Applicative)
+
+import Foreign.Ptr
+newtype RenderM a = RenderM (IO a) deriving (Functor, Applicative, Monad)
+
+type RenderCallback = Int -> Int -> RenderM ()
+
+foreign import ccall duma_onRender :: FunPtr RenderCallback -> RenderM ()
+
+foreign import ccall "wrapper" mkRenderCallback
+     :: RenderCallback -> RenderM (FunPtr RenderCallback)
+
+onRender :: RenderCallback -> RenderM ()
+onRender f = mkRenderCallback f >>= duma_onRender
+
+
+
index 8b3a8f8..c57b7c4 100644 (file)
@@ -1,6 +1,6 @@
-import Foreign\r
-import Foreign.C\r
-\r
-foreign import stdcall "test" ctest :: CInt -> IO ()\r
-\r
-main = ctest 3\r
+import Foreign
+import Foreign.C
+
+foreign import stdcall "test" ctest :: CInt -> IO ()
+
+main = ctest 3
index 8b3a8f8..c57b7c4 100644 (file)
@@ -1,6 +1,6 @@
-import Foreign\r
-import Foreign.C\r
-\r
-foreign import stdcall "test" ctest :: CInt -> IO ()\r
-\r
-main = ctest 3\r
+import Foreign
+import Foreign.C
+
+foreign import stdcall "test" ctest :: CInt -> IO ()
+
+main = ctest 3
index 0ee1ee9..c7b14bd 100644 (file)
@@ -1,7 +1,7 @@
-import Foreign\r
-import Foreign.C\r
-\r
-foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())\r
-foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()\r
-\r
-main = ctest ptest 3\r
+import Foreign
+import Foreign.C
+
+foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())
+foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()
+
+main = ctest ptest 3
index 0ee1ee9..c7b14bd 100644 (file)
@@ -1,7 +1,7 @@
-import Foreign\r
-import Foreign.C\r
-\r
-foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())\r
-foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()\r
-\r
-main = ctest ptest 3\r
+import Foreign
+import Foreign.C
+
+foreign import stdcall "&test" ptest :: FunPtr (CInt -> IO ())
+foreign import stdcall "dynamic" ctest :: FunPtr (CInt -> IO ()) -> CInt -> IO ()
+
+main = ctest ptest 3
index 4434bef..8a1a286 100644 (file)
@@ -1,29 +1,29 @@
--- exposed a bug in GHC 6.4 threaded RTS, fixed in Schedule.c rev. 1.232\r
-\r
-module Main where\r
-\r
-import Control.Concurrent\r
-import Control.Monad\r
-import Foreign.Ptr\r
-import Data.IORef\r
-\r
-main = do\r
-  ms <- replicateM 100 $ do putStrLn "." \r
-                                   m <- newEmptyMVar \r
-                           forkOS (thread >> putMVar m ())\r
-                           thread\r
-                           return m\r
-  mapM takeMVar ms\r
-\r
-thread = do var <- newIORef 0\r
-            let f = modifyIORef var (1+)\r
-            callC =<< mkFunc f\r
-\r
-type FUNC  =  IO ()\r
-\r
-foreign import ccall unsafe "wrapper"\r
-   mkFunc :: FUNC -> IO (FunPtr FUNC)\r
-\r
-foreign import ccall safe "ffi014_cbits.h callC"\r
-   callC:: FunPtr FUNC -> IO ()\r
-\r
+-- exposed a bug in GHC 6.4 threaded RTS, fixed in Schedule.c rev. 1.232
+
+module Main where
+
+import Control.Concurrent
+import Control.Monad
+import Foreign.Ptr
+import Data.IORef
+
+main = do
+  ms <- replicateM 100 $ do putStrLn "."
+                            m <- newEmptyMVar
+                            forkOS (thread >> putMVar m ())
+                            thread
+                            return m
+  mapM takeMVar ms
+
+thread = do var <- newIORef 0
+            let f = modifyIORef var (1+)
+            callC =<< mkFunc f
+
+type FUNC  =  IO ()
+
+foreign import ccall unsafe "wrapper"
+   mkFunc :: FUNC -> IO (FunPtr FUNC)
+
+foreign import ccall safe "ffi014_cbits.h callC"
+   callC:: FunPtr FUNC -> IO ()
+
index a98ee72..97d7573 100644 (file)
-{-# LANGUAGE GADTs #-}\r
-\r
-module Arith where \r
-\r
-data E a b = E (a -> b) (b -> a) \r
-\r
-eqRefl :: E a a \r
-eqRefl = E id id \r
-\r
--- just to construct unique strings\r
-data W \r
-data M a \r
-\r
--- terms\r
-data Var a where \r
-  VarW :: Var W \r
-  VarM :: Var (M a) \r
-\r
--- expose s in the type level making sure it is a string\r
-data Abs s e1  where \r
-  Abs :: (Var s) -> e1 -> Abs (Var s) e1 \r
-\r
-data App e1 e2 = App e1 e2 \r
-data Lit       = Lit \r
-\r
-data TyBase      = TyBase\r
-data TyArr t1 t2 = TyArr t1 t2 \r
-\r
--- (x:ty) in G\r
-data IN g p where \r
-  INOne :: IN (g,(x,ty)) (x,ty)\r
-  INShift :: IN g0 (x,ty) -> IN (g0,a) (x,ty) \r
-\r
-data INEX g x where \r
-  INEX :: IN g (x,v) -> INEX g x \r
-\r
-\r
--- G1 subseteq G2 \r
-type SUP g1 g2 = forall a. IN g1 a -> IN g2 a \r
\r
--- typing derivations \r
-data DER g a ty where \r
-  DVar :: IN (g,g0) ((Var a),ty) -> DER (g,g0) (Var a) ty -- the g,g0 makes sure that env is non-empty\r
-  DApp :: DER g a1 (TyArr ty1 ty2) -> \r
-            DER g a2 ty1 -> DER g (App a1 a2) ty2 \r
-  DAbs :: DER (g,(Var a,ty1)) e ty2 -> \r
-            DER g (Abs (Var a) e) (TyArr ty1 ty2) \r
-  DLit :: DER g Lit TyBase \r
-\r
--- G |- \x.x : a -> a \r
-test1 :: DER g (Abs (Var W) (Var W)) (TyArr ty ty) \r
-test1 = DAbs (DVar INOne)\r
-\r
--- G |- (\x.x) Lit : Lit \r
-test2 :: DER g (App (Abs (Var W) (Var W)) Lit) TyBase\r
-test2 = DApp (DAbs (DVar INOne)) DLit \r
-\r
--- G |- \x.\y. x y : (C -> C) -> C -> C \r
-test3 :: DER g (Abs (Var W) (Abs (Var (M W)) (App (Var W) (Var (M W))))) (TyArr (TyArr ty ty) (TyArr ty ty)) \r
-test3 = DAbs (DAbs (DApp (DVar (INShift INOne)) (DVar INOne))) \r
-\r
-data ISVAL e where \r
- ISVALAbs :: ISVAL (Abs (Var v) e)\r
- ISVALLit :: ISVAL Lit \r
-\r
-data React e1 e2 where \r
-  SUBSTReact :: React (Abs (Var y) e) v \r
-\r
--- evaluation \r
-data EDER e1 e2 where \r
- -- EVar    :: IN (a,val) -> ISVAL val -> EDER c a val \r
- EApp1   :: EDER e1 e1' -> EDER (App e1 e2) (App e1' e2) \r
- EApp2   :: ISVAL v1 -> EDER e2 e2' -> EDER (App v1 e2) (App v1 e2')\r
- EAppAbs :: ISVAL v2 -> React (Abs (Var v) e) v2 -> EDER (App (Abs (Var v) e) v2) e1\r
-\r
--- (\x.x) 3 -> 3 \r
--- test4 :: EDER (App (Abs (Var W) (Var W)) Lit) Lit \r
--- test4 = EAppAbs ISVALLit SUBSTEqVar \r
-\r
\r
--- existential \r
-data REDUCES e1 where \r
-   REDUCES :: EDER e1 e2 -> REDUCES e1 \r
-\r
--- data WFEnv x c g  where\r
---  WFOne ::  ISVAL v -> DER g v ty -> WFEnv (Var x) (c,(Var x,v)) (g,(Var x,ty))\r
---  WFShift :: WFEnv v c0 g0 -> WFEnv v (c0,(y,y1)) (g0,(z,z1))\r
-\r
--- data WFENVWRAP c g where \r
---    WFENVWRAP :: (forall v ty . IN g (v,ty) -> WFEnv v c g) -> WFENVWRAP c g  \r
-\r
-\r
--- data INEXVAL c x where \r
---   INEXVAL :: IN c (x,v) -> ISVAL v -> INEXVAL c x \r
-\r
--- -- the first cool theorem! \r
--- fromTEnvToEnv :: IN g (x,ty) -> WFEnv x c g ->  INEXVAL c x\r
--- fromTEnvToEnv INOne (WFOne isv _)  = INEXVAL INOne isv\r
--- fromTEnvToEnv (INShift ind1) (WFShift ind2) = \r
---           case (fromTEnvToEnv ind1 ind2) of \r
---              INEXVAL i isv -> INEXVAL (INShift i) isv\r
-\r
-\r
-data ISLAMBDA v where ISLAMBDA :: ISLAMBDA (Abs (Var x) e)\r
-data ISLIT v where ISLIT :: ISLIT Lit \r
-\r
-data EXISTAbs where \r
-  EXISTSAbs :: (Abs (Var x) e) -> EXISTAbs \r
-\r
-bot = bot \r
-\r
-canFormsLam :: ISVAL v -> DER g v (TyArr ty1 ty2) -> ISLAMBDA v \r
-canFormsLam ISVALAbs _ = ISLAMBDA \r
--- canFormsLam ISVALLit _ = bot         <== unfortunately I cannot catch this ... requires some exhaustiveness check :-( \r
-\r
-canFormsLit :: ISVAL v -> DER g v TyBase -> ISLIT v \r
-canFormsLit ISVALLit _ = ISLIT \r
-\r
-data NULL\r
-\r
-progress :: DER NULL e ty -> Either (ISVAL e) (REDUCES e) \r
-\r
-progress (DAbs prem)  = Left ISVALAbs \r
-progress (DLit)       = Left ISVALLit \r
--- progress (DVar iw)    = bot             <== here is the cool trick! I cannot even wite this down! \r
-progress (DApp e1 e2)  = \r
-     case (progress e1) of \r
-         Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))\r
-         Left  isv1         -> case (progress e2) of \r
-                                    Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2)) \r
-                                    Left isv2 -> case (canFormsLam isv1 e1) of \r
-                                                    ISLAMBDA -> Right (REDUCES (EAppAbs isv2 SUBSTReact))\r
-\r
-\r
---    case fromTEnvToEnv iw (f iw) of \r
---      INEXVAL i isv -> Right (REDUCES (EVar i isv)) \r
--- progress (WFENVWRAP f) (DApp e1 e2) = \r
---       case (progress (WFENVWRAP f) e1) of \r
---          Right (REDUCES r1) -> Right (REDUCES (EApp1 r1))\r
---          Left  isv1         -> case (progress (WFENVWRAP f) e2) of \r
---                                  Right (REDUCES r2) -> Right (REDUCES (EApp2 isv1 r2)) \r
---                                  Left isv2 -> case (canFormsLam isv1 e1) of \r
---                                                ISLAMBDA -> EAppAbs isv2 e1 \r
-                              \r
-\r
-                                  \r
+{-# 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
+
+
+
index bcd0a44..cea1c09 100644 (file)
@@ -1,18 +1,18 @@
-{-# LANGUAGE GADTs, ExistentialQuantification #-}\r
-{-# OPTIONS_GHC -O -fno-warn-overlapping-patterns #-}\r
-\r
--- Trac #2587\r
--- Actually this bug related to free variables and\r
--- type lets, but ostensibly it has a GADT flavour\r
--- Hence being in the GADT directory.\r
-\r
-module GadtBug(bug) where\r
-\r
-data Existential = forall a . Existential (Gadt a)\r
-\r
-data Gadt a where Value :: Gadt Double\r
-\r
-bug = [ match undefined | ps <- undefined, _ <- ps ]\r
-  where\r
-        match (Existential _) = undefined\r
-        match (Existential _) = undefined\r
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+{-# OPTIONS_GHC -O -fno-warn-overlapping-patterns #-}
+
+-- Trac #2587
+-- Actually this bug related to free variables and
+-- type lets, but ostensibly it has a GADT flavour
+-- Hence being in the GADT directory.
+
+module GadtBug(bug) where
+
+data Existential = forall a . Existential (Gadt a)
+
+data Gadt a where Value :: Gadt Double
+
+bug = [ match undefined | ps <- undefined, _ <- ps ]
+  where
+        match (Existential _) = undefined
+        match (Existential _) = undefined
index 9dac840..b9c6ffe 100644 (file)
@@ -1,17 +1,17 @@
-{-# LANGUAGE GADTs #-}\r
-\r
--- Trac #289\r
-\r
-module ShouldCompile where\r
-\r
-class C a where\r
-  f :: a -> Bool\r
-\r
-data T a where\r
-  MkT :: (C a) => a -> T a\r
-\r
-tf1 :: T Int -> Bool\r
-tf1 (MkT aa) = f aa\r
-\r
-tf2 :: T a -> Bool\r
-tf2 (MkT aa) = f aa\r
+{-# LANGUAGE GADTs #-}
+
+-- Trac #289
+
+module ShouldCompile where
+
+class C a where
+  f :: a -> Bool
+
+data T a where
+  MkT :: (C a) => a -> T a
+
+tf1 :: T Int -> Bool
+tf1 (MkT aa) = f aa
+
+tf2 :: T a -> Bool
+tf2 (MkT aa) = f aa
index 5b8a009..fcac058 100644 (file)
@@ -1,19 +1,19 @@
-{-# LANGUAGE GADTs, ExistentialQuantification #-}\r
-\r
--- Trac #289\r
-\r
-module ShouldCompile where\r
-\r
-class Foo a where \r
-  foo :: a -> Int \r
-\r
-data T = forall a. T (G a) \r
-data G a where\r
-  A :: G a\r
-  B :: Foo a => a -> G a\r
-\r
-doFoo :: T -> Int \r
-doFoo (T A) = 2 \r
-doFoo (T (B x)) = foo x \r
-\r
-\r
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+-- Trac #289
+
+module ShouldCompile where
+
+class Foo a where
+  foo :: a -> Int
+
+data T = forall a. T (G a)
+data G a where
+  A :: G a
+  B :: Foo a => a -> G a
+
+doFoo :: T -> Int
+doFoo (T A) = 2
+doFoo (T (B x)) = foo x
+
+
index 4db7b62..7efac22 100644 (file)
@@ -1,23 +1,23 @@
-{-# LANGUAGE GADTs #-}\r
-\r
--- Trac #345\r
-\r
-module ShouldCompile where\r
-\r
-data Succ n\r
-data Zero\r
-\r
-class Plus x y z | x y -> z\r
-instance Plus Zero x x\r
-instance Plus x y z => Plus (Succ x) y (Succ z)\r
-\r
-infixr 5 :::\r
-\r
-data List :: * -> * -> * where\r
-              Nil :: List a Zero\r
-              (:::) :: a -> List a n -> List a (Succ n)\r
-\r
-append :: Plus x y z => List a x -> List a y -> List a z\r
-append Nil ys = ys\r
-append (x ::: xs) ys = x ::: append xs ys\r
-\r
+{-# LANGUAGE GADTs #-}
+
+-- Trac #345
+
+module ShouldCompile where
+
+data Succ n
+data Zero
+
+class Plus x y z | x y -> z
+instance Plus Zero x x
+instance Plus x y z => Plus (Succ x) y (Succ z)
+
+infixr 5 :::
+
+data List :: * -> * -> * where
+              Nil :: List a Zero
+              (:::) :: a -> List a n -> List a (Succ n)
+
+append :: Plus x y z => List a x -> List a y -> List a z
+append Nil ys = ys
+append (x ::: xs) ys = x ::: append xs ys
+
index c5bdbcb..5f6e9fa 100644 (file)
@@ -1,8 +1,8 @@
-{-# LANGUAGE GADTs #-}\r
-\r
--- Check that trailing parens are ok in data con signatures\r
-\r
-module ShouldCompile where\r
\r
-data T where\r
-   MkT :: Int -> (Int -> T)\r
+{-# LANGUAGE GADTs #-}
+
+-- Check that trailing parens are ok in data con signatures
+
+module ShouldCompile where
+
+data T where
+   MkT :: Int -> (Int -> T)
index 4ac12ef..a7ae5a2 100644 (file)
@@ -1,18 +1,18 @@
-{-# LANGUAGE GADTs #-}\r
--- A simple GADT test from Roman\r
--- which nevertheless showed up a bug at one stage\r
-\r
-module ShouldCompile where\r
-\r
-data T a where\r
-  T1 :: () -> T ()\r
-  T2 :: T a -> T b -> T (a,b)\r
-\r
-class C a where\r
-  f :: T a -> a\r
-\r
-instance C () where\r
-  f (T1 x) = x\r
-\r
-instance (C a, C b) => C (a,b) where\r
-  f (T2 x y) = (f x, f y)\r
+{-# LANGUAGE GADTs #-}
+-- A simple GADT test from Roman
+-- which nevertheless showed up a bug at one stage
+
+module ShouldCompile where
+
+data T a where
+  T1 :: () -> T ()
+  T2 :: T a -> T b -> T (a,b)
+
+class C a where
+  f :: T a -> a
+
+instance C () where
+  f (T1 x) = x
+
+instance (C a, C b) => C (a,b) where
+  f (T2 x y) = (f x, f y)
index df9e0bc..ab8d70d 100644 (file)
@@ -1,15 +1,15 @@
-{-# LANGUAGE GADTs #-}\r
-\r
--- This one requires careful handling in \r
--- TcUnify.unifyTyConApp, to preserve rigidity.\r
-\r
-module ShouldCompile where\r
-\r
-data X a b where\r
-    X :: X a a\r
-\r
-data Y x a b where\r
-    Y :: x a b -> x b c -> Y x a c\r
-\r
-doy :: Y X a b -> Y X a b\r
-doy (Y X X) = Y X X\r
+{-# LANGUAGE GADTs #-}
+
+-- This one requires careful handling in
+-- TcUnify.unifyTyConApp, to preserve rigidity.
+
+module ShouldCompile where
+
+data X a b where
+    X :: X a a
+
+data Y x a b where
+    Y :: x a b -> x b c -> Y x a c
+
+doy :: Y X a b -> Y X a b
+doy (Y X X) = Y X X
index e3af7ad..b671db7 100644 (file)
@@ -1,79 +1,79 @@
-{-# LANGUAGE GADTs, KindSignatures #-}\r
-\r
--- See Trac #301\r
--- This particular one doesn't use GADTs per se, \r
--- but it does use dictionaries in constructors \r
-\r
-module Expr1 where\r
-\r
-data Expr :: * -> * where      -- Not a GADT at all\r
-  Const :: Show a => a -> Expr a\r
-               -- Note the Show constraint here\r
-  Var   :: Var a -> Expr a\r
-\r
-newtype Var a = V String\r
-\r
-instance Show (Var a) where show (V s) = s\r
-\r
---------------------------\r
-e1 :: Expr Int\r
-e1 = Const 42\r
-\r
-e2 :: Expr Bool\r
-e2 = Const True\r
-\r
-e3 :: Expr Integer\r
-e3 = Var (V "mersenne100")\r
-\r
---------------------------\r
-eval :: Expr a -> a\r
-eval (Const c) = c\r
-eval (Var v) = error ("free variable `" ++ shows v "'")\r
-\r
-{-\r
-    Up to here, everything works nicely:\r
-\r
-    \begin{verbatim}\r
-    *Expr0> eval e1\r
-    42\r
-    *Expr0> eval e2\r
-    True\r
-    *Expr1> eval e3\r
-    *** Exception: free variable `mersenne100'\r
-    \end{verbatim}\r
-\r
-    But let us now try to define a |shows| function.\r
-\r
-    In the following, without the type signature we get:\r
-    \begin{verbatim}\r
-    *Expr1> :t showsExpr\r
-    showsExpr :: forall a. (Show a) => Expr a -> String -> String\r
-    *Expr1> showsExpr e1 ""\r
-    "42"\r
-    *Expr1> showsExpr e2 ""\r
-    "True"\r
-    *Expr1> showsExpr e3 ""\r
-    "mersenne100"\r
-    \end{verbatim}\r
-\r
-    However, in the last case, the instance |Show Integer| was not used,\r
-    so should not have been required.\r
-    Therefore I would expect it to work as it is now, i.e.,\r
-    with the type signature:\r
--}\r
-\r
-showsExpr :: Expr a -> ShowS\r
-showsExpr (Const c) = shows c\r
-showsExpr (Var v) = shows v\r
-\r
-{- \r
-\r
-We used to get a complaint about the |Const| alternative (then line\r
-63) that documents that the constraint in the type of |Const| must\r
-have been ignored:\r
-\r
-    No instance for (Show a)\r
-      arising from use of `shows' at Expr1.lhs:63:22-26\r
-    Probable fix: add (Show a) to the type signature(s) for `showsExpr'\r
-    In the definition of `showsExpr': showsExpr (Const c) = shows c\r
--}\r
+{-# LANGUAGE GADTs, KindSignatures #-}
+
+-- See Trac #301
+-- This particular one doesn't use GADTs per se,
+-- but it does use dictionaries in constructors
+
+module Expr1 where
+
+data Expr :: * -> * where       -- Not a GADT at all
+  Const :: Show a => a -> Expr a
+                -- Note the Show constraint here
+  Var   :: Var a -> Expr a
+
+newtype Var a = V String
+
+instance Show (Var a) where show (V s) = s
+
+--------------------------
+e1 :: Expr Int
+e1 = Const 42
+
+e2 :: Expr Bool
+e2 = Const True
+
+e3 :: Expr Integer
+e3 = Var (V "mersenne100")
+
+--------------------------
+eval :: Expr a -> a
+eval (Const c) = c
+eval (Var v) = error ("free variable `" ++ shows v "'")
+
+{-
+    Up to here, everything works nicely:
+
+    \begin{verbatim}
+    *Expr0> eval e1
+    42
+    *Expr0> eval e2
+    True
+    *Expr1> eval e3
+    *** Exception: free variable `mersenne100'
+    \end{verbatim}
+
+    But let us now try to define a |shows| function.
+
+    In the following, without the type signature we get:
+    \begin{verbatim}
+    *Expr1> :t showsExpr
+    showsExpr :: forall a. (Show a) => Expr a -> String -> String
+    *Expr1> showsExpr e1 ""
+    "42"
+    *Expr1> showsExpr e2 ""
+    "True"
+    *Expr1> showsExpr e3 ""
+    "mersenne100"
+    \end{verbatim}
+
+    However, in the last case, the instance |Show Integer| was not used,
+    so should not have been required.
+    Therefore I would expect it to work as it is now, i.e.,
+    with the type signature:
+-}
+
+showsExpr :: Expr a -> ShowS
+showsExpr (Const c) = shows c
+showsExpr (Var v) = shows v
+
+{-
+
+We used to get a complaint about the |Const| alternative (then line
+63) that documents that the constraint in the type of |Const| must
+have been ignored:
+
+    No instance for (Show a)
+      arising from use of `shows' at Expr1.lhs:63:22-26
+    Probable fix: add (Show a) to the type signature(s) for `showsExpr'
+    In the definition of `showsExpr': showsExpr (Const c) = shows c
+-}
index a701400..aa96d68 100644 (file)
-{-# LANGUAGE GADTs, KindSignatures #-}\r
-\r
-module Expr0 where\r
-\r
--- See Trac #301\r
--- This one *does* use GADTs (Fct)\r
-\r
-data Expr :: * -> * where\r
-  Const :: Show a => a -> Expr a\r
-  Apply :: Fct a b -> Expr a -> Expr b\r
-\r
-data Fct :: * -> * -> * where\r
-  Succ :: Fct Int Int\r
-  EqZero :: Fct Int Bool\r
-  Add :: Fct Int (Int -> Int)\r
-\r
-------------------------------\r
-e1 :: Expr Int\r
-e1 = Apply Succ (Const 41)\r
-\r
-e2 :: Expr Bool\r
-e2 = Apply EqZero e1\r
-\r
-e3 :: Expr (Int -> Int)\r
-e3 = Apply Add e1\r
-\r
-------------------------------\r
-eval :: Expr a -> a\r
-eval (Const c) = c\r
-eval (Apply f a) = evalFct f $ eval a\r
-\r
-evalFct :: Fct a b -> a -> b\r
-evalFct Succ = succ\r
-evalFct EqZero = (0 ==)\r
-evalFct Add = (+)\r
-\r
-\r
-{-  Up to here, everything works nicely:\r
-\r
-    \begin{verbatim}\r
-    *Expr0> eval e1\r
-    42\r
-    *Expr0> eval e2\r
-    False\r
-    *Expr0> eval e3 5\r
-    47\r
-    \end{verbatim}\r
-\r
-    But let us now try to define a |Show| instance.\r
-    For |Fct|, this is not a problem:\r
--}\r
-\r
-instance Show (Fct a b) where\r
-  show Succ = "S"\r
-  show EqZero = "isZero"\r
-  show Add = "add"\r
-\r
-showsExpr :: Expr a -> ShowS\r
-showsExpr (Const c) = shows c\r
-showsExpr (Apply f a) =\r
-    ('(' :) . shows f . (' ' :) . showsExpr a . (')' :)\r
-\r
-instance Show (Expr a) where\r
-  showsPrec _ (Const c) = shows c\r
-  showsPrec _ (Apply f a) =\r
-    ('(' :) . shows f . (' ' :) . shows a . (')' :)\r
-\r
-{- But we used to get a complaint about the |Const| alternative (then\r
-   line 56) that documents that the constraint in the type of |Const|\r
-   must have been ignored:\r
-\r
-   \begin{verbatim}\r
-       No instance for (Show a)\r
-         arising from use of `shows' at Expr0.lhs:56:22-26\r
-       Probable fix: add (Show a) to the type signature(s) for `showsExpr'\r
-       In the definition of `showsExpr': showsExpr (Const c) = shows c\r
-   \end{verbatim}\r
-\r
-   But if we do that, the recursive call is of course still unsatisfied:\r
-   \begin{verbatim}\r
-       No instance for (Show a)\r
-         arising from use of `showsExpr' at Expr0.lhs:65:34-42\r
-       Probable fix: add (Show a) to the existential context for `Apply'\r
-       In the first argument of `(.)', namely `showsExpr a'\r
-       In the second argument of `(.)', namely `(showsExpr a) . ((')' :))'\r
-       In the second argument of `(.)', namely\r
-           `((' ' :)) . ((showsExpr a) . ((')' :)))'\r
-   \end{verbatim}\r
-\r
-   Following also the advice given in this last error message\r
-   actually makes GHC accept this, and then we can say:\r
-\r
-   \begin{verbatim}\r
-   *Expr0> showsExpr e1 ""\r
-   "(S 41)"\r
-   *Expr0> showsExpr e2 ""\r
-   "(isZero (S 41))"\r
-   \end{verbatim}\r
-\r
-   However, following this advice is counterintuitive\r
-   and should be unnecessary\r
-   since the |Show| instance for argument types\r
-   is only ever used in the const case.\r
-   We get:\r
-\r
-   \begin{verbatim}\r
-   *Expr0> showsExpr e3 ""\r
-\r
-   <interactive>:1:0:\r
-       No instance for (Show (Int -> Int))\r
-         arising from use of `showsExpr' at <interactive>:1:0-8\r
-       Probable fix: add an instance declaration for (Show (Int -> Int))\r
-       In the definition of `it': it = showsExpr e3 ""\r
-   \end{verbatim}\r
-\r
-   But of course we would expect the following:\r
-\r
-   \begin{verbatim}\r
-   *Expr0> showsExpr e3 ""\r
-   "(add (S 41))"\r
-   \end{verbatim}\r
-\r
-\r
-   \bigskip\r
-   The error messages are almost the same\r
-   if we define a |Show| instance directly\r
-   (line 90 was the |Const| alternative):\r
-\r
-   \begin{verbatim}\r
-       Could not deduce (Show a) from the context (Show (Expr a))\r
-         arising from use of `shows' at Expr0.lhs:90:26-30\r
-       Probable fix: add (Show a) to the class or instance method `showsPrec'\r
-   \end{verbatim}\r
--}\r
-\r
-\r
+{-# LANGUAGE GADTs, KindSignatures #-}
+
+module Expr0 where
+
+-- See Trac #301
+-- This one *does* use GADTs (Fct)
+
+data Expr :: * -> * where
+  Const :: Show a => a -> Expr a
+  Apply :: Fct a b -> Expr a -> Expr b
+
+data Fct :: * -> * -> * where
+  Succ :: Fct Int Int
+  EqZero :: Fct Int Bool
+  Add :: Fct Int (Int -> Int)
+
+------------------------------
+e1 :: Expr Int
+e1 = Apply Succ (Const 41)
+
+e2 :: Expr Bool
+e2 = Apply EqZero e1
+
+e3 :: Expr (Int -> Int)
+e3 = Apply Add e1
+
+------------------------------
+eval :: Expr a -> a
+eval (Const c) = c
+eval (Apply f a) = evalFct f $ eval a
+
+evalFct :: Fct a b -> a -> b
+evalFct Succ = succ
+evalFct EqZero = (0 ==)
+evalFct Add = (+)
+
+
+{-  Up to here, everything works nicely:
+
+    \begin{verbatim}
+    *Expr0> eval e1
+    42
+    *Expr0> eval e2
+    False
+    *Expr0> eval e3 5
+    47
+    \end{verbatim}
+
+    But let us now try to define a |Show| instance.
+    For |Fct|, this is not a problem:
+-}
+
+instance Show (Fct a b) where
+  show Succ = "S"
+  show EqZero = "isZero"
+  show Add = "add"
+
+showsExpr :: Expr a -> ShowS
+showsExpr (Const c) = shows c
+showsExpr (Apply f a) =
+    ('(' :) . shows f . (' ' :) . showsExpr a . (')' :)
+
+instance Show (Expr a) where
+  showsPrec _ (Const c) = shows c
+  showsPrec _ (Apply f a) =
+    ('(' :) . shows f . (' ' :) . shows a . (')' :)
+
+{- But we used to get a complaint about the |Const| alternative (then
+   line 56) that documents that the constraint in the type of |Const|
+   must have been ignored:
+
+   \begin{verbatim}
+       No instance for (Show a)
+         arising from use of `shows' at Expr0.lhs:56:22-26
+       Probable fix: add (Show a) to the type signature(s) for `showsExpr'
+       In the definition of `showsExpr': showsExpr (Const c) = shows c
+   \end{verbatim}
+
+   But if we do that, the recursive call is of course still unsatisfied:
+   \begin{verbatim}
+       No instance for (Show a)
+         arising from use of `showsExpr' at Expr0.lhs:65:34-42
+       Probable fix: add (Show a) to the existential context for `Apply'
+       In the first argument of `(.)', namely `showsExpr a'
+       In the second argument of `(.)', namely `(showsExpr a) . ((')' :))'
+       In the second argument of `(.)', namely
+           `((' ' :)) . ((showsExpr a) . ((')' :)))'
+   \end{verbatim}
+
+   Following also the advice given in this last error message
+   actually makes GHC accept this, and then we can say:
+
+   \begin{verbatim}
+   *Expr0> showsExpr e1 ""
+   "(S 41)"
+   *Expr0> showsExpr e2 ""
+   "(isZero (S 41))"
+   \end{verbatim}
+
+   However, following this advice is counterintuitive
+   and should be unnecessary
+   since the |Show| instance for argument types
+   is only ever used in the const case.
+   We get:
+
+   \begin{verbatim}
+   *Expr0> showsExpr e3 ""
+
+   <interactive>:1:0:
+       No instance for (Show (Int -> Int))
+         arising from use of `showsExpr' at <interactive>:1:0-8
+       Probable fix: add an instance declaration for (Show (Int -> Int))
+       In the definition of `it': it = showsExpr e3 ""
+   \end{verbatim}
+
+   But of course we would expect the following:
+
+   \begin{verbatim}
+   *Expr0> showsExpr e3 ""
+   "(add (S 41))"
+   \end{verbatim}
+
+
+   \bigskip
+   The error messages are almost the same
+   if we define a |Show| instance directly
+   (line 90 was the |Const| alternative):
+
+   \begin{verbatim}
+       Could not deduce (Show a) from the context (Show (Expr a))
+         arising from use of `shows' at Expr0.lhs:90:26-30
+       Probable fix: add (Show a) to the class or instance method `showsPrec'
+   \end{verbatim}
+-}
+
+
index f16da20..e05e3cb 100644 (file)
@@ -1,7 +1,7 @@
-{-# LANGUAGE GADTs, ExistentialQuantification #-}\r
-\r
-module ShouldFail where\r
-\r
-data T = forall a. T a (a->Int)\r
-\r
-f ~(T x f) = f x
\ No newline at end of file
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+module ShouldFail where
+
+data T = forall a. T a (a->Int)
+
+f ~(T x f) = f x
index 544705f..9903a66 100644 (file)
@@ -1,14 +1,14 @@
-{-# LANGUAGE GADTs #-}\r
-\r
--- It's not clear whether this one should succed or fail,\r
--- Arguably it should succeed because the type refinement on\r
+{-# LANGUAGE GADTs #-}
+
+-- It's not clear whether this one should succed or fail,
+-- Arguably it should succeed because the type refinement on
 -- T1 should make (y::Int).  Currently, though, it fails.
-\r
-module ShouldFail where\r
-\r
-data T a where\r
-  T1 :: Int -> T Int\r
-\r
-f :: (T a, a) -> Int\r
-f ~(T1 x, y) = x+y\r
-\r
+
+module ShouldFail where
+
+data T a where
+  T1 :: Int -> T Int
+
+f :: (T a, a) -> Int
+f ~(T1 x, y) = x+y
+
index 0d0018a..081dc36 100644 (file)
@@ -1,29 +1,29 @@
-{-# LANGUAGE GADTs #-}\r
-\r
-module Main where\r
-\r
-import Data.IORef\r
-\r
-data T a where\r
-  Li:: Int -> T Int\r
-  Lb:: Bool -> T Bool\r
-  La:: a -> T a\r
-\r
-writeInt:: T a -> IORef a -> IO ()\r
-writeInt v ref = case v of\r
-                  ~(Li x) -> writeIORef ref (1::Int)\r
-\r
-readBool:: T a -> IORef a -> IO ()\r
-readBool v ref = case v of\r
-                  ~(Lb x) -> \r
-                      readIORef ref >>= (print . not)\r
-\r
-tt::T a -> IO ()\r
-tt v = case v of\r
-         ~(Li x) ->  print "OK"\r
-\r
-main = do\r
-       tt (La undefined)\r
-       ref <- newIORef undefined\r
-       writeInt (La undefined) ref\r
-       readBool (La undefined) ref\r
+{-# LANGUAGE GADTs #-}
+
+module Main where
+
+import Data.IORef
+
+data T a where
+  Li:: Int -> T Int
+  Lb:: Bool -> T Bool
+  La:: a -> T a
+
+writeInt:: T a -> IORef a -> IO ()
+writeInt v ref = case v of
+                   ~(Li x) -> writeIORef ref (1::Int)
+
+readBool:: T a -> IORef a -> IO ()
+readBool v ref = case v of
+                   ~(Lb x) ->
+                       readIORef ref >>= (print . not)
+
+tt::T a -> IO ()
+tt v = case v of
+         ~(Li x) ->  print "OK"
+
+main = do
+        tt (La undefined)
+        ref <- newIORef undefined
+        writeInt (La undefined) ref
+        readBool (La undefined) ref
index 247b9eb..a476343 100644 (file)
-{-# LANGUAGE GADTs, ExistentialQuantification #-}\r
-\r
--- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)\r
--- demonstrates that it's possible to write functions of type\r
---     tc :: String -> Term a\r
--- where Term a is our strongly-typed GADT.  \r
--- That is, generate a typed term from an untyped source; Lennart \r
--- Augustsson set this as a challenge.\r
---\r
--- In fact the main function goes\r
---     tc :: UTerm -> exists ty. (Ty ty, Term ty)\r
--- so the type checker returns a pair of an expression and its type,\r
--- wrapped, of course, in an existential.\r
-\r
-module Main where\r
-\r
--- Untyped world --------------------------------------------\r
-data UTerm = UVar String\r
-          | ULam String UType UTerm\r
-          | UApp UTerm UTerm\r
-          | UConBool Bool\r
-          | UIf UTerm UTerm UTerm\r
-\r
-data UType = UBool | UArr UType UType\r
-\r
--- Typed world -----------------------------------------------\r
-data Ty t where\r
-  Bool :: Ty Bool\r
-  Arr  :: Ty a -> Ty b -> Ty (a -> b)\r
-\r
-data Term g t where\r
-  Var :: Var g t -> Term g t\r
-  Lam :: Ty a -> Term (g,a) b -> Term g (a->b) \r
-  App :: Term g (s -> t) -> Term g s -> Term g t\r
-  ConBool :: Bool -> Term g Bool\r
-  If :: Term g Bool -> Term g a -> Term g a -> Term g a\r
-\r
-data Var g t where\r
-  ZVar :: Var (h,t) t\r
-  SVar :: Var h t -> Var (h,s) t\r
-\r
-data Typed thing = forall ty. Typed (Ty ty) (thing ty)\r
-\r
--- Typechecking types\r
-data ExType = forall t. ExType (Ty t)\r
-\r
-tcType :: UType -> ExType\r
-tcType UBool = ExType Bool\r
-tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->\r
-                     case tcType t2 of { ExType t2' ->\r
-                     ExType (Arr t1' t2') }}\r
-\r
--- The type environment and lookup\r
-data TyEnv g where\r
-  Nil :: TyEnv g\r
-  Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)\r
-\r
-lookupVar :: String -> TyEnv g -> Typed (Var g)\r
-lookupVar _ Nil = error "Variable not found"\r
-lookupVar v (Cons s ty e) \r
-  | v==s      = Typed ty ZVar\r
-  | otherwise = case lookupVar v e of\r
-                  Typed ty v -> Typed ty (SVar v)\r
-\r
--- Comparing types\r
-newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }\r
-newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }\r
-\r
-cast2 :: Ty a -> Ty b -> (c a -> c b)\r
-cast2 Bool Bool x = x\r
-cast2 (Arr a1 a2) (Arr b1 b2) f\r
-  = let   C1 x = cast2 a1 b1 (C1 f)\r
-         C2 y = cast2 a2 b2 (C2 x)\r
-    in y\r
-\r
-data Equal a b where\r
-  Equal :: Equal c c\r
-\r
-cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)\r
-cmpTy Bool Bool = Just Equal\r
-cmpTy (Arr a1 a2) (Arr b1 b2)\r
-  = do { Equal <- cmpTy a1 b1\r
-       ; Equal <- cmpTy a2 b2\r
-       ; return Equal }\r
-\r
--- Typechecking terms\r
-tc :: UTerm -> TyEnv g -> Typed (Term g)\r
-tc (UVar v) env = case lookupVar v env of\r
-                   Typed ty v -> Typed ty (Var v)\r
-tc (UConBool b) env\r
-  = Typed Bool (ConBool b)\r
-tc (ULam s ty body) env \r
-  = case tcType ty of { ExType bndr_ty' ->\r
-    case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->\r
-    Typed (Arr bndr_ty' body_ty') \r
-         (Lam bndr_ty' body') }}\r
-tc (UApp e1 e2) env\r
-  = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->\r
-    case tc e2 env of { Typed arg_ty e2' ->\r
-    case cmpTy arg_ty bndr_ty of\r
-       Nothing -> error "Type error"\r
-       Just Equal -> Typed body_ty (App e1' e2') }}\r
-tc (UIf e1 e2 e3) env\r
-  = case tc e1 env of { Typed Bool e1' ->\r
-    case tc e2 env of { Typed t2   e2' ->\r
-    case tc e3 env of { Typed t3   e3' ->\r
-    case cmpTy t2 t3 of\r
-       Nothing -> error "Type error"\r
-       Just Equal -> Typed t2 (If e1' e2' e3') }}}\r
-\r
-showType :: Ty a -> String\r
-showType Bool = "Bool"\r
-showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"\r
-\r
-uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))\r
-\r
-test :: UTerm\r
-test = UApp uNot (UConBool True)\r
-\r
-main = putStrLn (case tc test Nil of\r
-                       Typed ty _ -> showType ty\r
-               )
\ No newline at end of file
+{-# LANGUAGE GADTs, ExistentialQuantification #-}
+
+-- This typechecker, written by Stephanie Weirich at Dagstuhl (Sept 04)
+-- demonstrates that it's possible to write functions of type
+--      tc :: String -> Term a
+-- where Term a is our strongly-typed GADT.
+-- That is, generate a typed term from an untyped source; Lennart
+-- Augustsson set this as a challenge.
+--
+-- In fact the main function goes
+--      tc :: UTerm -> exists ty. (Ty ty, Term ty)
+-- so the type checker returns a pair of an expression and its type,
+-- wrapped, of course, in an existential.
+
+module Main where
+
+-- Untyped world --------------------------------------------
+data UTerm = UVar String
+           | ULam String UType UTerm
+           | UApp UTerm UTerm
+           | UConBool Bool
+           | UIf UTerm UTerm UTerm
+
+data UType = UBool | UArr UType UType
+
+-- Typed world -----------------------------------------------
+data Ty t where
+  Bool :: Ty Bool
+  Arr  :: Ty a -> Ty b -> Ty (a -> b)
+
+data Term g t where
+  Var :: Var g t -> Term g t
+  Lam :: Ty a -> Term (g,a) b -> Term g (a->b)
+  App :: Term g (s -> t) -> Term g s -> Term g t
+  ConBool :: Bool -> Term g Bool
+  If :: Term g Bool -> Term g a -> Term g a -> Term g a
+
+data Var g t where
+  ZVar :: Var (h,t) t
+  SVar :: Var h t -> Var (h,s) t
+
+data Typed thing = forall ty. Typed (Ty ty) (thing ty)
+
+-- Typechecking types
+data ExType = forall t. ExType (Ty t)
+
+tcType :: UType -> ExType
+tcType UBool = ExType Bool
+tcType (UArr t1 t2) = case tcType t1 of { ExType t1' ->
+                      case tcType t2 of { ExType t2' ->
+                      ExType (Arr t1' t2') }}
+
+-- The type environment and lookup
+data TyEnv g where
+  Nil :: TyEnv g
+  Cons :: String -> Ty t -> TyEnv h -> TyEnv (h,t)
+
+lookupVar :: String -> TyEnv g -> Typed (Var g)
+lookupVar _ Nil = error "Variable not found"
+lookupVar v (Cons s ty e)
+  | v==s      = Typed ty ZVar
+  | otherwise = case lookupVar v e of
+                   Typed ty v -> Typed ty (SVar v)
+
+-- Comparing types
+newtype C1 c a2 d = C1 { unC1 :: c (d -> a2) }
+newtype C2 c b1 d = C2 { unC2 :: c (b1 -> d) }
+
+cast2 :: Ty a -> Ty b -> (c a -> c b)
+cast2 Bool Bool x = x
+cast2 (Arr a1 a2) (Arr b1 b2) f
+  = let   C1 x = cast2 a1 b1 (C1 f)
+          C2 y = cast2 a2 b2 (C2 x)
+    in y
+
+data Equal a b where
+  Equal :: Equal c c
+
+cmpTy :: Ty a -> Ty b -> Maybe (Equal a b)
+cmpTy Bool Bool = Just Equal
+cmpTy (Arr a1 a2) (Arr b1 b2)
+  = do  { Equal <- cmpTy a1 b1
+        ; Equal <- cmpTy a2 b2
+        ; return Equal }
+
+-- Typechecking terms
+tc :: UTerm -> TyEnv g -> Typed (Term g)
+tc (UVar v) env = case lookupVar v env of
+                    Typed ty v -> Typed ty (Var v)
+tc (UConBool b) env
+  = Typed Bool (ConBool b)
+tc (ULam s ty body) env
+  = case tcType ty of { ExType bndr_ty' ->
+    case tc body (Cons s bndr_ty' env) of { Typed body_ty' body' ->
+    Typed (Arr bndr_ty' body_ty')
+          (Lam bndr_ty' body') }}
+tc (UApp e1 e2) env
+  = case tc e1 env of { Typed (Arr bndr_ty body_ty) e1' ->
+    case tc e2 env of { Typed arg_ty e2' ->
+    case cmpTy arg_ty bndr_ty of
+        Nothing -> error "Type error"
+        Just Equal -> Typed body_ty (App e1' e2') }}
+tc (UIf e1 e2 e3) env
+  = case tc e1 env of { Typed Bool e1' ->
+    case tc e2 env of { Typed t2   e2' ->
+    case tc e3 env of { Typed t3   e3' ->
+    case cmpTy t2 t3 of
+        Nothing -> error "Type error"
+        Just Equal -> Typed t2 (If e1' e2' e3') }}}
+
+showType :: Ty a -> String
+showType Bool = "Bool"
+showType (Arr t1 t2) = "(" ++ showType t1 ++ ") -> (" ++ showType t2 ++ ")"
+
+uNot = ULam "x" UBool (UIf (UVar "x") (UConBool False) (UConBool True))
+
+test :: UTerm
+test = UApp uNot (UConBool True)
+
+main = putStrLn (case tc test Nil of
+                        Typed ty _ -> showType ty
+                )