f0f5253 · patch · git.iko.soy

git.iko.soy/patch

on develop help sign in

Factor out the use of the experimental dependent-sum classes

f0f5253Ryan Trinkle9 years ago

reflex.cabal+9−1

compare with develop

unifiedsplit

@@ -34,7 +34,12 @@ flag expose-all-unfoldings

34 manual: True

36flag debug-trace-events

37− description: add instrumentation that outputs the stack trace of the definition of an event whenever it is subscribed to. Warning: It is very slow!

37+ description: Add instrumentation that outputs the stack trace of the definition of an event whenever it is subscribed to. Warning: It is very slow!

38+ default: False

39+ manual: True

40+

41+flag experimental-dependent-sum-instances

42+ description: Use experimental incoherent instances for certain forked dependent-sum typeclasses

38 default: False

43 default: False

39 manual: True

44 manual: True

@@ -125,6 +130,9 @@ library

125 if flag(expose-all-unfoldings)

130 if flag(expose-all-unfoldings)

126 ghc-options: -fexpose-all-unfoldings

131 ghc-options: -fexpose-all-unfoldings

127

132

133+ if flag(experimental-dependent-sum-instances)

134+ ghc-options: -DEXPERIMENTAL_DEPENDENT_SUM_INSTANCES

135+

128test-suite semantics

136test-suite semantics

129 type: exitcode-stdio-1.0

137 type: exitcode-stdio-1.0

130 main-is: semantics.hs

138 main-is: semantics.hs

src/Data/Functor/Misc.hs+54−5

@@ -78,24 +78,48 @@ deriving instance Show k => Show (Const2 k v v')

78deriving instance Read k => Read (Const2 k v v)

80instance Show k => GShow (Const2 k v) where

81+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

81 gshowToShow (Const2 _) = id

82 gshowToShow (Const2 _) = id

83+#else

84+ gshowsPrec n x@(Const2 _) = showsPrec n x

85+#endif

83instance (Show k, Show (f v)) => ShowTag (Const2 k v) f where

87instance (Show k, Show (f v)) => ShowTag (Const2 k v) f where

88+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

84 showTagToShow (Const2 _) _ = id

89 showTagToShow (Const2 _) _ = id

90+#else

91+ showTaggedPrec (Const2 _) = showsPrec

92+#endif

86instance Eq k => GEq (Const2 k v) where

94instance Eq k => GEq (Const2 k v) where

95+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

87 geqToEq _ = id

96 geqToEq _ = id

88 geqUnify (Const2 _) (Const2 _) _ = id

97 geqUnify (Const2 _) (Const2 _) _ = id

98+#else

99+ geq (Const2 a) (Const2 b) =

100+ if a == b

101+ then Just Refl

102+ else Nothing

103+#endif

104

90instance Ord k => GCompare (Const2 k v) where

105instance Ord k => GCompare (Const2 k v) where

106+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

91 gcompareToOrd (Const2 _) = id

107 gcompareToOrd (Const2 _) = id

92 gcompare (Const2 a) (Const2 b) = strengthenOrdering $ compare a b

108 gcompare (Const2 a) (Const2 b) = strengthenOrdering $ compare a b

109+#else

110+ gcompare (Const2 a) (Const2 b) = case compare a b of

111+ LT -> GLT

112+ EQ -> GEQ

113+ GT -> GGT

114+#endif

115

116+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

94instance {-# INCOHERENT #-} (Eq k, Eq v) => EqTag (Const2 k v) Identity where

117instance {-# INCOHERENT #-} (Eq k, Eq v) => EqTag (Const2 k v) Identity where

95 eqTagToEq (Const2 _) _ = id

118 eqTagToEq (Const2 _) _ = id

119

97instance {-# INCOHERENT #-} Eq k => EqTag (Const2 k v) (Const2 k v) where

120instance {-# INCOHERENT #-} Eq k => EqTag (Const2 k v) (Const2 k v) where

98 eqTagToEq (Const2 _) _ = id

121 eqTagToEq (Const2 _) _ = id

122+#endif

123

100-- | Convert a 'DMap' to a regular 'Map'

124-- | Convert a 'DMap' to a regular 'Map'

101dmapToMap :: DMap (Const2 k v) Identity -> Map k v

125dmapToMap :: DMap (Const2 k v) Identity -> Map k v

@@ -132,11 +156,17 @@ deriving instance Show (f a) => Show (WrapArg g f (g' a))

132deriving instance Read (f a) => Read (WrapArg g f (g a))

156deriving instance Read (f a) => Read (WrapArg g f (g a))

133

157

134instance GEq f => GEq (WrapArg g f) where

158instance GEq f => GEq (WrapArg g f) where

159+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

135 geqToEq (WrapArg f) = geqToEq f

160 geqToEq (WrapArg f) = geqToEq f

136 geqUnify (WrapArg a) (WrapArg b) = geqUnify a b

161 geqUnify (WrapArg a) (WrapArg b) = geqUnify a b

162+#else

163+ geq (WrapArg a) (WrapArg b) = (\Refl -> Refl) <$> geq a b

164+#endif

137

165

138instance GCompare f => GCompare (WrapArg g f) where

166instance GCompare f => GCompare (WrapArg g f) where

167+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

139 gcompareToOrd (WrapArg f) = gcompareToOrd f

168 gcompareToOrd (WrapArg f) = gcompareToOrd f

169+#endif

140 gcompare (WrapArg a) (WrapArg b) = case gcompare a b of

170 gcompare (WrapArg a) (WrapArg b) = case gcompare a b of

141 GLT -> GLT

171 GLT -> GLT

142 GEQ -> GEQ

172 GEQ -> GEQ

@@ -188,6 +218,7 @@ deriving instance Show (EitherTag l r a)

188deriving instance Eq (EitherTag l r a)

218deriving instance Eq (EitherTag l r a)

189deriving instance Ord (EitherTag l r a)

219deriving instance Ord (EitherTag l r a)

190

220

221+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

191instance {-# INCOHERENT #-} (Show (f l), Show (f r)) => ShowTag (EitherTag l r) f where

222instance {-# INCOHERENT #-} (Show (f l), Show (f r)) => ShowTag (EitherTag l r) f where

192 showTagToShow e _ = case e of

223 showTagToShow e _ = case e of

193 LeftTag -> id

224 LeftTag -> id

@@ -197,32 +228,49 @@ instance {-# INCOHERENT #-} (Eq (f l), Eq (f r)) => EqTag (EitherTag l r) f wher

197 eqTagToEq e _ = case e of

228 eqTagToEq e _ = case e of

198 LeftTag -> id

229 LeftTag -> id

199 RightTag -> id

230 RightTag -> id

231+#endif

200

232

201instance GEq (EitherTag l r) where

233instance GEq (EitherTag l r) where

234+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

202 geqToEq _ = id

235 geqToEq _ = id

203 geqUnify LeftTag LeftTag _ same = same

236 geqUnify LeftTag LeftTag _ same = same

204 geqUnify RightTag RightTag _ same = same

237 geqUnify RightTag RightTag _ same = same

205 geqUnify _ _ unknown _ = unknown

238 geqUnify _ _ unknown _ = unknown

239+#endif

206 geq a b = case (a, b) of

240 geq a b = case (a, b) of

207 (LeftTag, LeftTag) -> Just Refl

241 (LeftTag, LeftTag) -> Just Refl

208 (RightTag, RightTag) -> Just Refl

242 (RightTag, RightTag) -> Just Refl

209 _ -> Nothing

243 _ -> Nothing

210

244

211instance GCompare (EitherTag l r) where

245instance GCompare (EitherTag l r) where

246+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

212 gcompareToOrd _ = id

247 gcompareToOrd _ = id

248+#endif

213 gcompare a b = case (a, b) of

249 gcompare a b = case (a, b) of

214 (LeftTag, LeftTag) -> GEQ

250 (LeftTag, LeftTag) -> GEQ

215 (LeftTag, RightTag) -> GLT

251 (LeftTag, RightTag) -> GLT

216 (RightTag, LeftTag) -> GGT

252 (RightTag, LeftTag) -> GGT

217 (RightTag, RightTag) -> GEQ

253 (RightTag, RightTag) -> GEQ

218

254

219−instance {-# INCOHERENT #-} GShow (EitherTag l r) where

255+instance GShow (EitherTag l r) where

256+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

220 gshowToShow _ = id

257 gshowToShow _ = id

258+#else

259+ gshowsPrec _ a = case a of

260+ LeftTag -> showString "LeftTag"

261+ RightTag -> showString "RightTag"

262+#endif

221

263

222instance (Show l, Show r) => ShowTag (EitherTag l r) Identity where

264instance (Show l, Show r) => ShowTag (EitherTag l r) Identity where

265+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

223 showTagToShow t _ = case t of

266 showTagToShow t _ = case t of

224 LeftTag -> id

267 LeftTag -> id

225 RightTag -> id

268 RightTag -> id

269+#else

270+ showTaggedPrec t n (Identity a) = case t of

271+ LeftTag -> showsPrec n a

272+ RightTag -> showsPrec n a

273+#endif

226

274

227-- | Convert 'Either' to a 'DSum'. Inverse of 'dsumToEither'.

275-- | Convert 'Either' to a 'DSum'. Inverse of 'dsumToEither'.

228eitherToDSum :: Either a b -> DSum (EitherTag a b) Identity

276eitherToDSum :: Either a b -> DSum (EitherTag a b) Identity

@@ -245,14 +293,15 @@ dsumToEither = \case

245-- representational so that we can use safe 'coerce'.

293-- representational so that we can use safe 'coerce'.

246newtype ComposeMaybe f a = ComposeMaybe { getComposeMaybe :: Maybe (f a) } deriving (Show, Eq, Ord)

294newtype ComposeMaybe f a = ComposeMaybe { getComposeMaybe :: Maybe (f a) } deriving (Show, Eq, Ord)

247

295

248−instance EqTag f g => EqTag f (ComposeMaybe g) where

249− eqTagToEq f _ = eqTagToEq f (Proxy :: Proxy g)

250−

251deriving instance Functor f => Functor (ComposeMaybe f)

296deriving instance Functor f => Functor (ComposeMaybe f)

252

297

298+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

299+instance {-# INCOHERENT #-} EqTag f g => EqTag f (ComposeMaybe g) where

300+ eqTagToEq f _ = eqTagToEq f (Proxy :: Proxy g)

301+

253instance {-# INCOHERENT #-} GShow k => ShowTag k (ComposeMaybe k) where

302instance {-# INCOHERENT #-} GShow k => ShowTag k (ComposeMaybe k) where

254 showTagToShow k _ r = gshowToShow k (showTagToShow k (Proxy :: Proxy k) r)

303 showTagToShow k _ r = gshowToShow k (showTagToShow k (Proxy :: Proxy k) r)

255−

304+#endif

256--------------------------------------------------------------------------------

305--------------------------------------------------------------------------------

257-- Deprecated functions

306-- Deprecated functions

258--------------------------------------------------------------------------------

307--------------------------------------------------------------------------------

src/Reflex/Dynamic.hs+4

@@ -334,17 +334,21 @@ data FHList f l where

334 FHCons :: f e -> FHList f l -> FHList f (e ': l)

335

336instance GEq (HListPtr l) where

337+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

337 geqToEq _ = id

338 geqToEq _ = id

338 geqUnify HHeadPtr HHeadPtr _ same = same

339 geqUnify HHeadPtr HHeadPtr _ same = same

339 geqUnify (HTailPtr a) (HTailPtr b) different same = geqUnify a b different same

340 geqUnify (HTailPtr a) (HTailPtr b) different same = geqUnify a b different same

340 geqUnify _ _ different _ = different

341 geqUnify _ _ different _ = different

342+#endif

341 HHeadPtr `geq` HHeadPtr = Just Refl

343 HHeadPtr `geq` HHeadPtr = Just Refl

342 HHeadPtr `geq` HTailPtr _ = Nothing

344 HHeadPtr `geq` HTailPtr _ = Nothing

343 HTailPtr _ `geq` HHeadPtr = Nothing

345 HTailPtr _ `geq` HHeadPtr = Nothing

344 HTailPtr a `geq` HTailPtr b = a `geq` b

346 HTailPtr a `geq` HTailPtr b = a `geq` b

345

347

346instance GCompare (HListPtr l) where -- Warning: This ordering can't change, dmapTo*HList will break

348instance GCompare (HListPtr l) where -- Warning: This ordering can't change, dmapTo*HList will break

349+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

347 gcompareToOrd _ = id

350 gcompareToOrd _ = id

351+#endif

348 HHeadPtr `gcompare` HHeadPtr = GEQ

352 HHeadPtr `gcompare` HHeadPtr = GEQ

349 HHeadPtr `gcompare` HTailPtr _ = GLT

353 HHeadPtr `gcompare` HTailPtr _ = GLT

350 HTailPtr _ `gcompare` HHeadPtr = GGT

354 HTailPtr _ `gcompare` HHeadPtr = GGT

src/Reflex/Patch/DMapWithMove.hs+11−4

@@ -1,5 +1,4 @@

1−-- | This module defines the 'Patch' class, which is used by Reflex to manage

1+{-# LANGUAGE CPP #-}

2−-- changes to 'Reflex.Class.Incremental' values.

3{-# LANGUAGE FlexibleContexts #-}

2{-# LANGUAGE FlexibleContexts #-}

4{-# LANGUAGE FlexibleInstances #-}

3{-# LANGUAGE FlexibleInstances #-}

5{-# LANGUAGE GADTs #-}

4{-# LANGUAGE GADTs #-}

@@ -19,23 +18,29 @@ import qualified Reflex.Patch.MapWithMove as MapWithMove

20import Data.Dependent.Map (DMap, DSum (..), GCompare (..))

19import Data.Dependent.Map (DMap, DSum (..), GCompare (..))

21import qualified Data.Dependent.Map as DMap

20import qualified Data.Dependent.Map as DMap

22−import Data.Dependent.Sum (ShowTag (..), EqTag (..))

21+import Data.Dependent.Sum (EqTag (..))

23import Data.Functor.Constant

22import Data.Functor.Constant

24import Data.Functor.Misc

23import Data.Functor.Misc

25import Data.Functor.Product

24import Data.Functor.Product

26import Data.GADT.Compare (GEq (..))

25import Data.GADT.Compare (GEq (..))

27−import Data.GADT.Show (GShow (..))

28import qualified Data.Map as Map

26import qualified Data.Map as Map

29import Data.Maybe

27import Data.Maybe

30import Data.Semigroup (Semigroup (..), (<>))

28import Data.Semigroup (Semigroup (..), (<>))

31import Data.Some (Some)

29import Data.Some (Some)

32import qualified Data.Some as Some

30import qualified Data.Some as Some

33import Data.These

31import Data.These

32+

33+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

34+import Data.Dependent.Sum (ShowTag (..))

35+import Data.GADT.Show (GShow (..))

34import Data.Typeable (Proxy (..))

36import Data.Typeable (Proxy (..))

37+#endif

36-- | Like 'PatchMapWithMove', but for 'DMap'.

39-- | Like 'PatchMapWithMove', but for 'DMap'.

37data PatchDMapWithMove k v = PatchDMapWithMove (DMap k (NodeInfo k v))

40data PatchDMapWithMove k v = PatchDMapWithMove (DMap k (NodeInfo k v))

41+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

38 deriving (Show)

42 deriving (Show)

43+#endif

40data NodeInfo k v a = NodeInfo

45data NodeInfo k v a = NodeInfo

41 { _nodeInfo_from :: !(From k v a)

46 { _nodeInfo_from :: !(From k v a)

@@ -43,11 +48,13 @@ data NodeInfo k v a = NodeInfo

43 }

48 }

44 deriving (Show)

49 deriving (Show)

51+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

46instance {-# INCOHERENT #-} (GShow k, ShowTag k v) => ShowTag k (NodeInfo k v) where

52instance {-# INCOHERENT #-} (GShow k, ShowTag k v) => ShowTag k (NodeInfo k v) where

47 showTagToShow k _ r = gshowToShow k $ showTagToShow k (Proxy :: Proxy v) r

53 showTagToShow k _ r = gshowToShow k $ showTagToShow k (Proxy :: Proxy v) r

49instance {-# INCOHERENT #-} (GEq k, EqTag k v) => EqTag k (From k v) where

55instance {-# INCOHERENT #-} (GEq k, EqTag k v) => EqTag k (From k v) where

50 eqTagToEq k _ r = eqTagToEq k (Proxy :: Proxy v) (geqToEq k r)

56 eqTagToEq k _ r = eqTagToEq k (Proxy :: Proxy v) (geqToEq k r)

57+#endif

52data From (k :: a -> *) (v :: a -> *) :: a -> * where

59data From (k :: a -> *) (v :: a -> *) :: a -> * where

53 From_Insert :: v a -> From k v a

60 From_Insert :: v a -> From k v a

src/Reflex/Spider/Internal.hs+6

@@ -730,11 +730,17 @@ instance Eq (SpiderTimelineEnv x) where

730 _ == _ = True -- Since only one exists of each type

731

732instance GEq SpiderTimelineEnv where

733+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

733 geqToEq _ = id

734 geqToEq _ = id

734 geqUnify (a :: SpiderTimelineEnv a) (b :: SpiderTimelineEnv b) different same = if _spiderTimeline_lock a == _spiderTimeline_lock b

735 geqUnify (a :: SpiderTimelineEnv a) (b :: SpiderTimelineEnv b) different same = if _spiderTimeline_lock a == _spiderTimeline_lock b

735 then case unsafeCoerce Refl :: a :~: b of

736 then case unsafeCoerce Refl :: a :~: b of

736 Refl -> same -- This unsafeCoerce is safe because the same SpiderTimelineEnv can't have two different 'x' arguments

737 Refl -> same -- This unsafeCoerce is safe because the same SpiderTimelineEnv can't have two different 'x' arguments

737 else different

738 else different

739+#else

740+ a `geq` b = if _spiderTimeline_lock a == _spiderTimeline_lock b

741+ then Just $ unsafeCoerce Refl -- This unsafeCoerce is safe because the same SpiderTimelineEnv can't have two different 'x' arguments

742+ else Nothing

743+#endif

738

744

739data EventEnv x

745data EventEnv x

740 = EventEnv { eventEnvAssignments :: !(IORef [SomeAssignment x]) -- Needed for Subscribe

746 = EventEnv { eventEnvAssignments :: !(IORef [SomeAssignment x]) -- Needed for Subscribe