f0f5253 · reflex · git.iko.soy

git.iko.soy/reflex

Factor out the use of the experimental dependent-sum classes

commitf0f5253c3dcfe324913873a4466232fc51e41602 authorRyan Trinkle <ryan.trinkle@gmail.com> dateTue 18 Apr 2017, 21:32 (9 years ago) parent1647b9c

5 files changed+84−10

compare with develop

unifiedsplit

reflex.cabal+9−1 src/Data/Functor/Misc.hs+54−5 src/Reflex/Dynamic.hs+4 src/Reflex/Patch/DMapWithMove.hs+11−4 src/Reflex/Spider/Internal.hs+6

reflex.cabal+9−1

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

3434 manual: True

3535

3636flag 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

3843 default: False

3944 manual: True

4045

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

125130 if flag(expose-all-unfoldings)

126131 ghc-options: -fexpose-all-unfoldings

127132

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

134+ ghc-options: -DEXPERIMENTAL_DEPENDENT_SUM_INSTANCES

135+

128136test-suite semantics

129137 type: exitcode-stdio-1.0

130138 main-is: semantics.hs

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

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

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

7979

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

81+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

8182 gshowToShow (Const2 _) = id

83+#else

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

85+#endif

8286

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

88+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

8489 showTagToShow (Const2 _) _ = id

90+#else

91+ showTaggedPrec (Const2 _) = showsPrec

92+#endif

8593

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

95+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

8796 geqToEq _ = id

8897 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

89104

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

106+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

91107 gcompareToOrd (Const2 _) = id

92108 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

93115

116+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

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

95118 eqTagToEq (Const2 _) _ = id

96119

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

98121 eqTagToEq (Const2 _) _ = id

122+#endif

99123

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

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

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

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

133157

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

159+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

135160 geqToEq (WrapArg f) = geqToEq f

136161 geqUnify (WrapArg a) (WrapArg b) = geqUnify a b

162+#else

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

164+#endif

137165

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

167+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

139168 gcompareToOrd (WrapArg f) = gcompareToOrd f

169+#endif

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

141171 GLT -> GLT

142172 GEQ -> GEQ

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

188218deriving instance Eq (EitherTag l r a)

189219deriving instance Ord (EitherTag l r a)

190220

221+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

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

192223 showTagToShow e _ = case e of

193224 LeftTag -> id

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

197228 eqTagToEq e _ = case e of

198229 LeftTag -> id

199230 RightTag -> id

231+#endif

200232

201233instance GEq (EitherTag l r) where

234+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

202235 geqToEq _ = id

203236 geqUnify LeftTag LeftTag _ same = same

204237 geqUnify RightTag RightTag _ same = same

205238 geqUnify _ _ unknown _ = unknown

239+#endif

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

207241 (LeftTag, LeftTag) -> Just Refl

208242 (RightTag, RightTag) -> Just Refl

209243 _ -> Nothing

210244

211245instance GCompare (EitherTag l r) where

246+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

212247 gcompareToOrd _ = id

248+#endif

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

214250 (LeftTag, LeftTag) -> GEQ

215251 (LeftTag, RightTag) -> GLT

216252 (RightTag, LeftTag) -> GGT

217253 (RightTag, RightTag) -> GEQ

218254

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

255+instance GShow (EitherTag l r) where

256+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

220257 gshowToShow _ = id

258+#else

259+ gshowsPrec _ a = case a of

260+ LeftTag -> showString "LeftTag"

261+ RightTag -> showString "RightTag"

262+#endif

221263

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

265+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

223266 showTagToShow t _ = case t of

224267 LeftTag -> id

225268 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

226274

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

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

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

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

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

247295

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

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

250−

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

252297

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+

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

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

255−

304+#endif

256305--------------------------------------------------------------------------------

257306-- Deprecated functions

258307--------------------------------------------------------------------------------

src/Reflex/Dynamic.hs+4

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

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

335335

336336instance GEq (HListPtr l) where

337+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

337338 geqToEq _ = id

338339 geqUnify HHeadPtr HHeadPtr _ same = same

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

340341 geqUnify _ _ different _ = different

342+#endif

341343 HHeadPtr `geq` HHeadPtr = Just Refl

342344 HHeadPtr `geq` HTailPtr _ = Nothing

343345 HTailPtr _ `geq` HHeadPtr = Nothing

344346 HTailPtr a `geq` HTailPtr b = a `geq` b

345347

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

349+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

347350 gcompareToOrd _ = id

351+#endif

348352 HHeadPtr `gcompare` HHeadPtr = GEQ

349353 HHeadPtr `gcompare` HTailPtr _ = GLT

350354 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

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

1+{-# LANGUAGE CPP #-}

32{-# LANGUAGE FlexibleContexts #-}

43{-# LANGUAGE FlexibleInstances #-}

54{-# LANGUAGE GADTs #-}

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

1918

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

2120import qualified Data.Dependent.Map as DMap

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

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

2322import Data.Functor.Constant

2423import Data.Functor.Misc

2524import Data.Functor.Product

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

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

2826import qualified Data.Map as Map

2927import Data.Maybe

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

3129import Data.Some (Some)

3230import qualified Data.Some as Some

3331import Data.These

32+

33+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

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

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

3436import Data.Typeable (Proxy (..))

37+#endif

3538

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

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

41+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

3842 deriving (Show)

43+#endif

3944

4045data NodeInfo k v a = NodeInfo

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

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

4348 }

4449 deriving (Show)

4550

51+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

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

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

4854

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

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

57+#endif

5158

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

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

src/Reflex/Spider/Internal.hs+6

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

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

731731

732732instance GEq SpiderTimelineEnv where

733+#ifdef EXPERIMENTAL_DEPENDENT_SUM_INSTANCES

733734 geqToEq _ = id

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

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

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

737738 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

738744

739745data EventEnv x

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