Browse files

Added Read instance for DSum and an example file wherein it is tested

  • Loading branch information...
1 parent 3719026 commit f250a32604a80de509f02ebe0b8ce9727071cc71 @mokus0 committed Mar 17, 2011
Showing with 126 additions and 4 deletions.
  1. +107 −0 examples/FooGADT.hs
  2. +15 −0 src/Data/Dependent/Sum.hs
  3. +4 −4 src/Data/GADT/Compare.hs
View
107 examples/FooGADT.hs
@@ -0,0 +1,107 @@
+{-# LANGUAGE GADTs #-}
+module FooGADT where
+
+import Data.Dependent.Sum
+import Data.GADT.Show
+import Data.GADT.Compare
+
+data Foo a where
+ Foo :: Foo Double
+ Bar :: Foo Int
+ Baz :: Foo String
+ Qux :: Foo Double
+
+instance Eq (Foo a) where
+ Foo == Foo = True
+ Bar == Bar = True
+ Baz == Baz = True
+ Qux == Qux = True
+ _ == _ = False
+
+instance GEq Foo where
+ geq Foo Foo = Just Refl
+ geq Bar Bar = Just Refl
+ geq Baz Baz = Just Refl
+ geq Qux Qux = Just Refl
+ geq _ _ = Nothing
+
+ maybeEq Foo Foo y n = y
+ maybeEq Bar Bar y n = y
+ maybeEq Baz Baz y n = y
+ maybeEq Qux Qux y n = y
+ maybeEq _ _ y n = n
+
+
+instance EqTag Foo where
+ eqTagged Foo Foo = (==)
+ eqTagged Bar Bar = (==)
+ eqTagged Baz Baz = (==)
+ eqTagged Qux Qux = (==)
+ eqTagged _ _ = const (const False)
+
+instance GCompare Foo where
+ gcompare Foo Foo = GEQ
+ gcompare Foo _ = GLT
+
+ gcompare Bar Foo = GGT
+ gcompare Bar Bar = GEQ
+ gcompare Bar _ = GLT
+
+ gcompare Baz Foo = GGT
+ gcompare Baz Bar = GGT
+ gcompare Baz Baz = GEQ
+ gcompare Baz _ = GLT
+
+ gcompare Qux Foo = GGT
+ gcompare Qux Bar = GGT
+ gcompare Qux Baz = GGT
+ gcompare Qux Qux = GEQ
+
+instance OrdTag Foo where
+ compareTagged Foo Foo = compare
+ compareTagged Bar Bar = compare
+ compareTagged Baz Baz = compare
+ compareTagged Qux Qux = compare
+
+ compareTagged _ _ = error "OrdTag: bad case"
+
+instance Show (Foo a) where
+ showsPrec _ Foo = showString "Foo"
+ showsPrec _ Bar = showString "Bar"
+ showsPrec _ Baz = showString "Baz"
+ showsPrec _ Qux = showString "Qux"
+
+instance GShow Foo where
+ gshowsPrec = showsPrec
+
+instance ShowTag Foo where
+ showTaggedPrec Foo = showsPrec
+ showTaggedPrec Bar = showsPrec
+ showTaggedPrec Baz = showsPrec
+ showTaggedPrec Qux = showsPrec
+
+
+instance GRead Foo where
+ greadsPrec _ str = case tag of
+ "Foo" -> [(\k -> k Foo, rest)]
+ "Bar" -> [(\k -> k Bar, rest)]
+ "Baz" -> [(\k -> k Baz, rest)]
+ "Qux" -> [(\k -> k Qux, rest)]
+ _ -> []
+ where (tag, rest) = splitAt 3 str
+
+instance ReadTag Foo where
+ readTaggedPrec Foo = readsPrec
+ readTaggedPrec Bar = readsPrec
+ readTaggedPrec Baz = readsPrec
+ readTaggedPrec Qux = readsPrec
+
+
+foo x = Foo :=> x
+bar x = Bar :=> x
+baz x = Baz :=> x
+qux x = Qux :=> x
+
+
+xs = [foo pi, bar 100, baz "hello world", qux (exp 1)]
+xs' = read (show xs) `asTypeOf` xs
View
15 src/Data/Dependent/Sum.hs
@@ -66,6 +66,21 @@ instance ShowTag tag => Show (DSum tag) where
. showTaggedPrec tag 1 value
)
+class GRead tag => ReadTag tag where
+ readTaggedPrec :: tag a -> Int -> ReadS a
+
+instance ReadTag tag => Read (DSum tag) where
+ readsPrec p = readParen (p > 1) $ \s ->
+ concat
+ [ withTag $ \tag ->
+ [ (tag :=> val, rest'')
+ | (val, rest'') <- readTaggedPrec tag 1 rest'
+ ]
+ | (withTag, rest) <- greadsPrec p s
+ , let (con, rest') = splitAt 5 rest
+ , con == " :=> "
+ ]
+
-- |In order to test @DSum tag@ for equality, @tag@ must know how to test
-- both itself and its tagged values for equality. 'EqTag' defines
-- the interface by which they are expected to do so.
View
8 src/Data/GADT/Compare.hs
@@ -35,17 +35,17 @@ class GEq f where
--
-- (Making use of the 'DSum' type from "Data.Dependent.Sum" in both examples)
geq :: f a -> f b -> Maybe (a := b)
- geq = maybeEq (Just Refl) Nothing
+ geq x y = maybeEq x y (Just Refl) Nothing
- -- An interesting alternative formulation:
+ -- |An interesting alternative formulation:
-- This one is nice because it's purely type-level, which means
-- that in some cases the type checker can statically prove
-- that the 'f' case is unreachable.
--
-- Sometimes, though, it can be hard to get the 'Refl' case's type to unify
-- with the assumptions properly.
- maybeEq :: ((a ~ b) => c) -> c -> f a -> f b -> c
- maybeEq f z x y = case geq x y of
+ maybeEq :: f a -> f b -> ((a ~ b) => c) -> c -> c
+ maybeEq x y f z = case geq x y of
Just Refl -> f
Nothing -> z

0 comments on commit f250a32

Please sign in to comment.