mirror of
https://github.com/github/semantic.git
synced 2024-12-01 00:33:59 +03:00
Rename our Union type to Sum.
This commit is contained in:
Rob Rix
parent
171d349eee
commit
50a3fecfe3
@ -91,6 +91,8 @@ library
|
||||
, Data.Span
|
||||
, Data.SplitDiff
|
||||
-- À la carte syntax types
|
||||
, Data.Sum
|
||||
, Data.Sum.Templates
|
||||
, Data.Syntax
|
||||
, Data.Syntax.Comment
|
||||
, Data.Syntax.Declaration
|
||||
@ -99,8 +101,6 @@ library
|
||||
, Data.Syntax.Literal
|
||||
, Data.Syntax.Statement
|
||||
, Data.Syntax.Type
|
||||
, Data.Syntax.Union
|
||||
, Data.Syntax.Union.Templates
|
||||
, Data.Term
|
||||
-- Diffing algorithms & interpretation thereof
|
||||
, Diffing.Algorithm
|
||||
|
||||
@ -10,7 +10,7 @@
|
||||
{-# LANGUAGE UndecidableInstances #-}
|
||||
|
||||
{-|
|
||||
Module : Data.Union
|
||||
Module : Data.Sum
|
||||
Description : Open unions (type-indexed co-products) for extensible effects.
|
||||
Copyright : Allele Dev 2015
|
||||
License : BSD-3
|
||||
@ -33,11 +33,11 @@ Our list r of open union components is a small Universe.
|
||||
Therefore, we can use the Typeable-like evidence in that
|
||||
universe.
|
||||
|
||||
The data constructors of Union are not exported.
|
||||
The data constructors of Sum are not exported.
|
||||
-}
|
||||
|
||||
module Data.Syntax.Union (
|
||||
Union,
|
||||
module Data.Sum (
|
||||
Sum,
|
||||
decompose,
|
||||
weaken,
|
||||
inj,
|
||||
@ -55,11 +55,11 @@ module Data.Syntax.Union (
|
||||
import Data.Functor.Classes (Eq1(..), eq1, Ord1(..), compare1, Show1(..), showsPrec1)
|
||||
import Data.Maybe (fromMaybe)
|
||||
import Data.Proxy
|
||||
import Data.Syntax.Union.Templates
|
||||
import Unsafe.Coerce(unsafeCoerce)
|
||||
import Data.Sum.Templates
|
||||
import GHC.Exts (Constraint)
|
||||
import GHC.Prim (Proxy#, proxy#)
|
||||
import GHC.TypeLits
|
||||
import Unsafe.Coerce(unsafeCoerce)
|
||||
|
||||
pure [mkElemIndexTypeFamily 150]
|
||||
|
||||
@ -69,16 +69,16 @@ infixr 5 :<
|
||||
-- t is can be a GADT and hence not necessarily a Functor.
|
||||
-- Int is the index of t in the list r; that is, the index of t in the
|
||||
-- universe r.
|
||||
data Union (r :: [ * -> * ]) (v :: *) where
|
||||
Union :: {-# UNPACK #-} !Int -> t v -> Union r v
|
||||
data Sum (r :: [ * -> * ]) (v :: *) where
|
||||
Sum :: {-# UNPACK #-} !Int -> t v -> Sum r v
|
||||
|
||||
{-# INLINE prj' #-}
|
||||
{-# INLINE inj' #-}
|
||||
inj' :: Int -> t v -> Union r v
|
||||
inj' = Union
|
||||
inj' :: Int -> t v -> Sum r v
|
||||
inj' = Sum
|
||||
|
||||
prj' :: Int -> Union r v -> Maybe (t v)
|
||||
prj' n (Union n' x) | n == n' = Just (unsafeCoerce x)
|
||||
prj' :: Int -> Sum r v -> Maybe (t v)
|
||||
prj' n (Sum n' x) | n == n' = Just (unsafeCoerce x)
|
||||
| otherwise = Nothing
|
||||
|
||||
newtype P (t :: * -> *) (r :: [* -> *]) = P { unP :: Int }
|
||||
@ -92,31 +92,31 @@ type family Members ms r :: Constraint where
|
||||
type (ts :<: r) = Members ts r
|
||||
|
||||
-- | Inject a functor into a type-aligned union.
|
||||
inj :: forall e r v. (e :< r) => e v -> Union r v
|
||||
inj :: forall e r v. (e :< r) => e v -> Sum r v
|
||||
inj = inj' (unP (elemNo :: P e r))
|
||||
{-# INLINE inj #-}
|
||||
|
||||
-- | Maybe project a functor out of a type-aligned union.
|
||||
prj :: forall e r v. (e :< r) => Union r v -> Maybe (e v)
|
||||
prj :: forall e r v. (e :< r) => Sum r v -> Maybe (e v)
|
||||
prj = prj' (unP (elemNo :: P e r))
|
||||
{-# INLINE prj #-}
|
||||
|
||||
|
||||
decompose :: Union (t ': r) v -> Either (Union r v) (t v)
|
||||
decompose (Union 0 v) = Right $ unsafeCoerce v
|
||||
decompose (Union n v) = Left $ Union (n-1) v
|
||||
decompose :: Sum (t ': r) v -> Either (Sum r v) (t v)
|
||||
decompose (Sum 0 v) = Right $ unsafeCoerce v
|
||||
decompose (Sum n v) = Left $ Sum (n-1) v
|
||||
{-# INLINE [2] decompose #-}
|
||||
|
||||
|
||||
-- | Specialized version of 'decompose'.
|
||||
decompose0 :: Union '[t] v -> Either (Union '[] v) (t v)
|
||||
decompose0 (Union _ v) = Right $ unsafeCoerce v
|
||||
decompose0 :: Sum '[t] v -> Either (Sum '[] v) (t v)
|
||||
decompose0 (Sum _ v) = Right $ unsafeCoerce v
|
||||
-- No other case is possible
|
||||
{-# RULES "decompose/singleton" decompose = decompose0 #-}
|
||||
{-# INLINE decompose0 #-}
|
||||
|
||||
weaken :: Union r w -> Union (any ': r) w
|
||||
weaken (Union n v) = Union (n+1) v
|
||||
weaken :: Sum r w -> Sum (any ': r) w
|
||||
weaken (Sum n v) = Sum (n+1) v
|
||||
|
||||
type (Member t r) = KnownNat (ElemIndex t r)
|
||||
type (t :< r) = Member t r
|
||||
@ -128,20 +128,20 @@ elemNo = P (fromIntegral (natVal' (proxy# :: Proxy# (ElemIndex t r))))
|
||||
|
||||
-- | Helper to apply a function to a functor of the nth type in a type list.
|
||||
class Apply (c :: (* -> *) -> Constraint) (fs :: [* -> *]) where
|
||||
apply :: proxy c -> (forall g . c g => g a -> b) -> Union fs a -> b
|
||||
apply :: proxy c -> (forall g . c g => g a -> b) -> Sum fs a -> b
|
||||
|
||||
apply' :: Apply c fs => proxy c -> (forall g . c g => (forall x. g x -> Union fs x) -> g a -> b) -> Union fs a -> b
|
||||
apply' proxy f u@(Union n _) = apply proxy (f (Union n)) u
|
||||
apply' :: Apply c fs => proxy c -> (forall g . c g => (forall x. g x -> Sum fs x) -> g a -> b) -> Sum fs a -> b
|
||||
apply' proxy f u@(Sum n _) = apply proxy (f (Sum n)) u
|
||||
{-# INLINABLE apply' #-}
|
||||
|
||||
apply2 :: Apply c fs => proxy c -> (forall g . c g => g a -> g b -> d) -> Union fs a -> Union fs b -> Maybe d
|
||||
apply2 proxy f u@(Union n1 _) (Union n2 r2)
|
||||
apply2 :: Apply c fs => proxy c -> (forall g . c g => g a -> g b -> d) -> Sum fs a -> Sum fs b -> Maybe d
|
||||
apply2 proxy f u@(Sum n1 _) (Sum n2 r2)
|
||||
| n1 == n2 = Just (apply proxy (\ r1 -> f r1 (unsafeCoerce r2)) u)
|
||||
| otherwise = Nothing
|
||||
{-# INLINABLE apply2 #-}
|
||||
|
||||
apply2' :: Apply c fs => proxy c -> (forall g . c g => (forall x. g x -> Union fs x) -> g a -> g b -> d) -> Union fs a -> Union fs b -> Maybe d
|
||||
apply2' proxy f u@(Union n1 _) (Union n2 r2)
|
||||
apply2' :: Apply c fs => proxy c -> (forall g . c g => (forall x. g x -> Sum fs x) -> g a -> g b -> d) -> Sum fs a -> Sum fs b -> Maybe d
|
||||
apply2' proxy f u@(Sum n1 _) (Sum n2 r2)
|
||||
| n1 == n2 = Just (apply' proxy (\ reinj r1 -> f reinj r1 (unsafeCoerce r2)) u)
|
||||
| otherwise = Nothing
|
||||
{-# INLINABLE apply2' #-}
|
||||
@ -149,7 +149,7 @@ apply2' proxy f u@(Union n1 _) (Union n2 r2)
|
||||
pure (mkApplyInstance <$> [1..150])
|
||||
|
||||
|
||||
instance Apply Foldable fs => Foldable (Union fs) where
|
||||
instance Apply Foldable fs => Foldable (Sum fs) where
|
||||
foldMap f = apply (Proxy :: Proxy Foldable) (foldMap f)
|
||||
{-# INLINABLE foldMap #-}
|
||||
|
||||
@ -165,14 +165,14 @@ instance Apply Foldable fs => Foldable (Union fs) where
|
||||
length = apply (Proxy :: Proxy Foldable) length
|
||||
{-# INLINABLE length #-}
|
||||
|
||||
instance Apply Functor fs => Functor (Union fs) where
|
||||
instance Apply Functor fs => Functor (Sum fs) where
|
||||
fmap f = apply' (Proxy :: Proxy Functor) (\ reinj a -> reinj (fmap f a))
|
||||
{-# INLINABLE fmap #-}
|
||||
|
||||
(<$) v = apply' (Proxy :: Proxy Functor) (\ reinj a -> reinj (v <$ a))
|
||||
{-# INLINABLE (<$) #-}
|
||||
|
||||
instance (Apply Foldable fs, Apply Functor fs, Apply Traversable fs) => Traversable (Union fs) where
|
||||
instance (Apply Foldable fs, Apply Functor fs, Apply Traversable fs) => Traversable (Sum fs) where
|
||||
traverse f = apply' (Proxy :: Proxy Traversable) (\ reinj a -> reinj <$> traverse f a)
|
||||
{-# INLINABLE traverse #-}
|
||||
|
||||
@ -180,28 +180,28 @@ instance (Apply Foldable fs, Apply Functor fs, Apply Traversable fs) => Traversa
|
||||
{-# INLINABLE sequenceA #-}
|
||||
|
||||
|
||||
instance Apply Eq1 fs => Eq1 (Union fs) where
|
||||
instance Apply Eq1 fs => Eq1 (Sum fs) where
|
||||
liftEq eq u1 u2 = fromMaybe False (apply2 (Proxy :: Proxy Eq1) (liftEq eq) u1 u2)
|
||||
{-# INLINABLE liftEq #-}
|
||||
|
||||
instance (Apply Eq1 fs, Eq a) => Eq (Union fs a) where
|
||||
instance (Apply Eq1 fs, Eq a) => Eq (Sum fs a) where
|
||||
(==) = eq1
|
||||
{-# INLINABLE (==) #-}
|
||||
|
||||
|
||||
instance (Apply Eq1 fs, Apply Ord1 fs) => Ord1 (Union fs) where
|
||||
liftCompare compareA u1@(Union n1 _) u2@(Union n2 _) = fromMaybe (compare n1 n2) (apply2 (Proxy :: Proxy Ord1) (liftCompare compareA) u1 u2)
|
||||
instance (Apply Eq1 fs, Apply Ord1 fs) => Ord1 (Sum fs) where
|
||||
liftCompare compareA u1@(Sum n1 _) u2@(Sum n2 _) = fromMaybe (compare n1 n2) (apply2 (Proxy :: Proxy Ord1) (liftCompare compareA) u1 u2)
|
||||
{-# INLINABLE liftCompare #-}
|
||||
|
||||
instance (Apply Eq1 fs, Apply Ord1 fs, Ord a) => Ord (Union fs a) where
|
||||
instance (Apply Eq1 fs, Apply Ord1 fs, Ord a) => Ord (Sum fs a) where
|
||||
compare = compare1
|
||||
{-# INLINABLE compare #-}
|
||||
|
||||
|
||||
instance Apply Show1 fs => Show1 (Union fs) where
|
||||
instance Apply Show1 fs => Show1 (Sum fs) where
|
||||
liftShowsPrec sp sl d = apply (Proxy :: Proxy Show1) (liftShowsPrec sp sl d)
|
||||
{-# INLINABLE liftShowsPrec #-}
|
||||
|
||||
instance (Apply Show1 fs, Show a) => Show (Union fs a) where
|
||||
instance (Apply Show1 fs, Show a) => Show (Sum fs a) where
|
||||
showsPrec = showsPrec1
|
||||
{-# INLINABLE showsPrec #-}
|
||||
@ -1,5 +1,5 @@
|
||||
{-# LANGUAGE TemplateHaskell #-}
|
||||
module Data.Syntax.Union.Templates
|
||||
module Data.Sum.Templates
|
||||
( mkElemIndexTypeFamily
|
||||
, mkApplyInstance
|
||||
) where
|
||||
@ -42,7 +42,7 @@ mkApplyInstance paramN =
|
||||
, PragmaD (InlineP apply Inlinable FunLike AllPhases)
|
||||
]
|
||||
where typeParams = VarT . mkName . ('f' :) . show <$> [0..pred paramN]
|
||||
[applyC, apply, f, r, union] = mkName <$> ["Apply", "apply", "f", "r", "Union"]
|
||||
[applyC, apply, f, r, union] = mkName <$> ["Apply", "apply", "f", "r", "Sum"]
|
||||
[constraint, a] = VarT . mkName <$> ["constraint", "a"]
|
||||
mkClause i nthType = Clause
|
||||
[ WildP, VarP f, ConP union [ LitP (IntegerL i), VarP r ] ]
|
||||
Loading…
Reference in New Issue
Block a user