yoko 0.9 → 2.0
raw patch · 27 files changed
+1832/−442 lines, 27 filesdep +semigroupsdep ~type-spine
Dependencies added: semigroups
Dependency ranges changed: type-spine
Files
- Data/Yoko.hs +5/−3
- Data/Yoko/Each.hs +0/−55
- Data/Yoko/HCompos.hs +42/−37
- Data/Yoko/Invariant.hs +62/−0
- Data/Yoko/MinCtors.hs +373/−0
- Data/Yoko/MinCtors/MMap.hs +46/−0
- Data/Yoko/MinCtors/Minima.hs +165/−0
- Data/Yoko/MinCtors/Prims0.hs +16/−0
- Data/Yoko/MinCtors/Prims1.hs +16/−0
- Data/Yoko/Prelude.hs +77/−0
- Data/Yoko/Representation.hs +93/−35
- Data/Yoko/SmartPreciseCase.hs +14/−14
- Data/Yoko/TH.hs +324/−147
- Data/Yoko/TH/Internal.hs +9/−2
- Data/Yoko/TypeBasics.hs +187/−2
- Data/Yoko/TypeSums.hs +38/−29
- Data/Yoko/View.hs +101/−18
- Data/Yoko/W.hs +67/−0
- Data/YokoRaw.hs +39/−43
- Examples/LambdaLift/Common.hs +8/−0
- Examples/LambdaLift/DeepSeq.hs +47/−24
- Examples/LambdaLift/FreeVars.hs +17/−15
- Examples/LambdaLift/LambdaLift.hs +11/−11
- Examples/LambdaLift/TLF.hs +2/−2
- Examples/LambdaLift/ULC.hs +1/−1
- Examples/MinCtors.hs +59/−0
- yoko.cabal +13/−4
Data/Yoko.hs view
@@ -36,8 +36,10 @@ -} module Data.Yoko- (module Data.YokoRaw, module Data.Yoko.SmartPreciseCase)- where+ (module Data.YokoRaw, module Data.Yoko.SmartPreciseCase, module Data.Yoko.TH) where -import Data.YokoRaw hiding (precise_case)+import Data.YokoRaw hiding (precise_case0) import Data.Yoko.SmartPreciseCase+import Data.Yoko.TH++import Data.Yoko.Prelude ()
− Data/Yoko/Each.hs
@@ -1,55 +0,0 @@-{-# LANGUAGE KindSignatures, ConstraintKinds, MultiParamTypeClasses,- Rank2Types, FlexibleInstances, UndecidableInstances, TypeOperators #-}--{- |--Module : Data.Yoko.Each-Copyright : (c) The University of Kansas 2012-License : BSD3--Maintainer : nicolas.frisby@gmail.com-Stability : experimental-Portability : see LANGUAGE pragmas (... GHC)--Basic support for folding through type-level sums.---}--module Data.Yoko.Each (Each, each) where--import Data.Yoko.TypeBasics-import Data.Yoko.Representation----- | The constraint @Each con sum@ corresponds to the constraing @forall dc in--- sum. con dc@.-type Each = Each_---- | Fold through a type-level sum.-each :: Each cxt sum => Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b-each = each_-------class Each_ cxt sum where- each_ :: Proxy cxt -> (forall a. cxt a => a -> b) -> sum -> b----instance cxt a => Each_ cxt (N a) where each_ _ f (N x) = f x--instance (Each_ cxt a, Each_ cxt b) => Each_ cxt (a :+: b) where- each_ c f = foldPlus (each c f) (each c f)----instance Each_ cxt sum => Each_ cxt (DCsOf t sum) where--- each_ c f = each c f . unDCsOf------_ex = putStrLn $ each (Proxy :: Proxy Show) show $- L (N 'n') `asTypeOf` R (N True)
Data/Yoko/HCompos.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses, FlexibleContexts, FlexibleInstances, UndecidableInstances,- ScopedTypeVariables, DataKinds #-}+ ScopedTypeVariables, DataKinds, PolyKinds #-} {-# OPTIONS_GHC -fcontext-stack=250 #-} @@ -23,6 +23,7 @@ module Data.Yoko.HCompos where import Data.Yoko.TypeBasics+import Data.Yoko.W import Data.Yoko import Control.Applicative@@ -36,15 +37,15 @@ -- | The applicative functor required by the conversion.-type family Idiom cnv :: * -> *+type family Idiom (cnv :: *) :: * -> * -- | Use the conversion @cnv@ to convert from @a@ to @b@.-class Applicative (Idiom cnv) => Convert cnv a b where- convert :: cnv -> a -> Idiom cnv b+class Applicative (Idiom cnv) => Convert0 cnv a b where+ convert0 :: cnv -> a -> Idiom cnv b -- | The generic version of @convert@; operates on /disbanded data types/.-class Applicative (Idiom cnv) => HCompos cnv a t where- hcompos :: cnv -> a -> Idiom cnv t+class Applicative (Idiom cnv) => HCompos0 cnv a t where+ hcompos0 :: cnv -> a p1 p0 -> Idiom cnv t @@ -52,45 +53,45 @@ -- these two instances make functions work directly for singly-recursive data -- types type instance Idiom (a -> i b) = i-instance (Applicative i, a ~ x, b ~ y) => Convert (a -> i b) x y where convert = ($)+instance (Applicative i, a ~ x, b ~ y) => Convert0 (a -> i b) x y where convert0 = ($) -data FoundDC star = NoCorrespondingConstructorFor_In_ star star | Match star+data FoundDC (k :: *) (l :: *) = NoCorrespondingConstructorFor_In_ k k | Match l -type family WithMessage (dcA :: *) (b :: *) (dcB :: Maybe *) :: FoundDC *+type family WithMessage (dcA :: k) (b :: k) (dcB :: Maybe l) :: FoundDC k l type instance WithMessage dcA b (Just x) = Match x type instance WithMessage dcA b Nothing = NoCorrespondingConstructorFor_In_ dcA b -- | @FindDCs dcA dcBs@ returns a type-level @Maybe@. @Just dcB@ is a fields -- type @dcB@ where @'Tag' dcA ~ dcB@.-type family FindDCs (s :: Digit) (dcBs :: *) :: Maybe *+type family FindDCs (s :: Digit) (dcBs :: * -> * -> *) :: Maybe (* -> * -> *) type instance FindDCs s (N dc) =- If (Equal s (Tag dc)) (Just dc) Nothing+ If (Equal s (Tag dc)) (Just (N dc)) Nothing type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b) -instance (HCompos cnv a t, HCompos cnv b t- ) => HCompos cnv (a :+: b) t where- hcompos cnv = foldPlus (hcompos cnv) (hcompos cnv)+instance (HCompos0 cnv a t, HCompos0 cnv b t+ ) => HCompos0 cnv (a :+: b) t where+ hcompos0 cnv = foldPlus (hcompos0 cnv) (hcompos0 cnv) -- NB only works if there's exactly one matching constructor-instance (Generic dcA, Match dcB ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),- MapRs cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB),+instance (Generic dcA, Match (N dcB) ~ WithMessage dcA b (FindDCs (Tag dcA) (DCs b)),+ MapRs0 cnv (ResultsInIncompatibleFields dcA dcB) dcA dcB (Rep dcA) (Rep dcB), DC dcB, Codomain dcB ~ b, DT b- ) => HCompos cnv (N dcA) b where- hcompos cnv =- foldN $ liftA (rejoin . (id :: dcB -> dcB) . obj) . mapRs cnv msgp p1 p2 . rep+ ) => HCompos0 cnv (N dcA) b where+ hcompos0 cnv =+ foldN0 $ liftA (unSym0 rejoin . (id :: dcB -> dcB) . unW'0 obj) . mapRs0 cnv msgp p1 p2 . unW0 rep where p1 :: Proxy dcA; p1 = Proxy; p2 :: Proxy dcB; p2 = Proxy msgp = ResultsInIncompatibleFields :: ResultsInIncompatibleFields dcA dcB -data ResultsInIncompatibleFields (dcA :: *) (dcB :: *) = ResultsInIncompatibleFields+data ResultsInIncompatibleFields (dcA :: k) (dcB :: k) = ResultsInIncompatibleFields @@ -100,25 +101,29 @@ -- | Same as @compos@ semantics, but with a generalized type and just for -- converting between product representations.-class Applicative (Idiom cnv) => MapRs cnv msg dc dc' prod prod' where- mapRs :: cnv -> msg -> Proxy dc -> Proxy dc' -> prod -> Idiom cnv prod'+class Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' prod prod' where+ mapRs0 :: cnv -> msg -> Proxy dc -> Proxy dc' -> prod p1 p0 -> Idiom cnv (prod' p1 p0) -instance Convert cnv a b => MapRs cnv msg dc dc' (Rec a) (Rec b) where- mapRs cnv _ _ _ (Rec x) = Rec <$> convert cnv x+instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' U U where+ mapRs0 _ _ _ _ = pure -instance Applicative (Idiom cnv) => MapRs cnv msg dc dc' (Dep a) (Dep a) where- mapRs _ _ _ _ = pure-instance Applicative (Idiom cnv) => MapRs cnv msg dc dc' U U where- mapRs _ _ _ _ = pure+instance (MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'+ ) => MapRs0 cnv msg dc dc' (a :*: b) (a' :*: b') where+ mapRs0 cnv msgp p1 p2 (a :*: b) = (:*:) <$> mapRs0 cnv msgp p1 p2 a <*> mapRs0 cnv msgp p1 p2 b -instance (MapRs cnv msg dc dc' a a', MapRs cnv msg dc dc' b b'- ) => MapRs cnv msg dc dc' (a :*: b) (a' :*: b') where- mapRs cnv msgp p1 p2 (a :*: b) = (:*:) <$> mapRs cnv msgp p1 p2 a <*> mapRs cnv msgp p1 p2 b+instance MapRs0 cnv msg dc dc' a a' => MapRs0 cnv msg dc dc' (C dcA a) (C dcB a') where+ mapRs0 cnv msgp p1 p2 (C x) = C <$> mapRs0 cnv msgp p1 p2 x -instance (Traversable f, MapRs cnv msg dc dc' a a'- ) => MapRs cnv msg dc dc' (Par1 f a) (Par1 f a') where- mapRs cnv msgp p1 p2 (Par1 x) = Par1 <$> traverse (mapRs cnv msgp p1 p2) x+instance Convert0 cnv a b => MapRs0 cnv msg dc dc' (T0 (Rec lbl) a) (T0 (Rec lbl') b) where+ mapRs0 cnv _ _ _ (T0 x) = T0 <$> convert0 cnv x -instance (Bitraversable f, MapRs cnv msg dc dc' a a', MapRs cnv msg dc dc' b b'- ) => MapRs cnv msg dc dc' (Par2 f a b) (Par2 f a' b') where- mapRs cnv msgp p1 p2 (Par2 x) = Par2 <$> bitraverse (mapRs cnv msgp p1 p2) (mapRs cnv msgp p1 p2) x+instance Applicative (Idiom cnv) => MapRs0 cnv msg dc dc' (T0 Dep a) (T0 Dep a) where+ mapRs0 _ _ _ _ = pure++instance (Traversable f, MapRs0 cnv msg dc dc' a a'+ ) => MapRs0 cnv msg dc dc' (T1 Dep f a) (T1 Dep f a') where+ mapRs0 cnv msgp p1 p2 (T1 x) = T1 <$> traverse (mapRs0 cnv msgp p1 p2) x++instance (Bitraversable f, MapRs0 cnv msg dc dc' a a', MapRs0 cnv msg dc dc' b b'+ ) => MapRs0 cnv msg dc dc' (T2 Dep f a b) (T2 Dep f a' b') where+ mapRs0 cnv msgp p1 p2 (T2 x) = T2 <$> bitraverse (mapRs0 cnv msgp p1 p2) (mapRs0 cnv msgp p1 p2) x
+ Data/Yoko/Invariant.hs view
@@ -0,0 +1,62 @@+{-# LANGUAGE TypeOperators, LambdaCase, FlexibleContexts, UndecidableInstances, PolyKinds #-}++module Data.Yoko.Invariant+ (module Data.Yoko.Invariant, module Data.Functor.Invariant) where++import Data.Yoko.W+import Data.YokoRaw++import Data.Functor.Invariant++++++gen_invmap :: (Invariant2 (DCs t), DT t, AreDCsOf t (DCs t)) =>+ (a -> b) -> (b -> a) -> t a -> t b+gen_invmap f f' = unW'1 band . invmap2 id id f f' . unW1 disband++gen_invmap2 :: (Invariant2 (DCs t), DT t, AreDCsOf t (DCs t)) =>+ (a -> c) -> (c -> a) -> (b -> d) -> (d -> b) -> t a b -> t c d+gen_invmap2 f f' g g' = unW'2 band . invmap2 f f' g g' . unW2 disband++++++instance Invariant2 U where+ invmap2 _ _ _ _ _ = U++instance (Invariant2 l, Invariant2 r) => Invariant2 (l :*: r) where+ invmap2 f f' g g' (l :*: r) = invmap2 f f' g g' l :*: invmap2 f f' g g' r++instance (Invariant2 r) => Invariant2 (C dc r) where+ invmap2 f f' g g' (C x) = C $ invmap2 f f' g g' x+++-- can optimize for * and * -> *, but I'm favoring terseness+instance (WN dc, Invariant2 (Rep dc), Generic dc) => Invariant2 (N dc) where+ invmap2 f f' g g' = unSym nN obj . invmap2 f f' g g' . unSym rep unN++instance (Invariant2 l, Invariant2 r) => Invariant2 (l :+: r) where+ invmap2 f f' g g' = \case+ L x -> L $ invmap2 f f' g g' x+ R x -> R $ invmap2 f f' g g' x++instance Invariant2 Void where invmap2 = error "invmap2 @Void"++++instance Invariant2 (T0 v t) where+ invmap2 _ _ _ _ (T0 x) = T0 x++instance (Invariant t, Invariant2 r) => Invariant2 (T1 v t r) where+ invmap2 f f' g g' (T1 x) = T1 $ invmap (invmap2 f f' g g') (invmap2 f' f g' g) x++instance (Invariant2 t, Invariant2 r, Invariant2 s) => Invariant2 (T2 v t r s) where+ invmap2 f f' g g' (T2 x) = T2 $ invmap2 (invmap2 f f' g g') (invmap2 f' f g' g) (invmap2 f f' g g') (invmap2 f' f g' g) x++++instance Invariant2 Par1 where invmap2 f _ _ _ (Par1 x) = Par1 (f x)+instance Invariant2 Par0 where invmap2 _ _ g _ (Par0 x) = Par0 (g x)
+ Data/Yoko/MinCtors.hs view
@@ -0,0 +1,373 @@+{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, UndecidableInstances,+ DefaultSignatures, ViewPatterns, FlexibleContexts, FlexibleInstances,+ PolyKinds, MultiParamTypeClasses, Rank2Types #-}++module Data.Yoko.MinCtors (MinCtors(..), gen_minCtors, nCtors) where++import Data.Yoko++import Data.Semigroup (Min(..))+import qualified Data.Yoko.MinCtors.MMap as MMap+import Data.Yoko.MinCtors.Minima++import Data.Monoid (mappend)++import qualified GHC.Real++--------------------+-- miscellaneous++pDisband :: Proxy t -> Proxy (DCs t)+pDisband _ = Proxy++pRep :: Proxy t -> Proxy (Rep t)+pRep _ = Proxy+++++++++++++++--------------------+-- the internal classes++class MinInfoRec (t :: k) (ts :: [k1]) where+ minInfoRec :: Proxy t -> Proxy ts -> SiblingInT ts++class MinInfoNonRec (t :: k) where minInfoNonRec :: Proxy t -> Minima2++minima1ToSiblingInT :: VRepeat ts => Minima2 -> SiblingInT ts+minima1ToSiblingInT =+ MMap.mapWithMonoKeys (\(np1, np0) -> (cvRepeat 0, np1, np0)) id++void :: Minima2+void = MMap.singleton (0, 0) $ Min 0++nCtors :: MinCtorsTrim t => Int -> Proxy t -> MinCtorsT t+nCtors n p = minCtorsTrim p $ nCtors' n p++nCtors' :: Int -> Proxy t -> Minima2+nCtors' n _ = MMap.singleton (0, 0) $ Min n++++++++deApp :: Proxy (T1 v f r) -> (Proxy f, Proxy r)+deApp _ = (Proxy, Proxy)++instance (Ord (CVec ts NRec), MinCtors f, MinInfoRec r ts) => MinInfoRec (T1 Dep f r) ts where+ minInfoRec (deApp -> (pf, pr)) pts = minCtors pf `plug0` minInfoRec pr pts++instance (MinCtors f, MinInfoNonRec r) => MinInfoNonRec (T1 Dep f r) where+ minInfoNonRec (deApp -> (pf, pr)) = minCtors pf `plug0'` minInfoNonRec pr++deApp2 :: Proxy (T2 v ff r1 r0) -> (Proxy ff, Proxy r1, Proxy r0)+deApp2 _ = (Proxy, Proxy, Proxy)++instance (Ord (CVec ts NRec), MinCtors ff, MinInfoRec rB ts, MinInfoRec rA ts) => MinInfoRec (T2 Dep ff rB rA) ts where+ minInfoRec (deApp2 -> (ff, rB, rA)) pts =+ plug10 (minCtors ff) (minInfoRec rB pts) (minInfoRec rA pts)++instance (MinCtors ff, MinInfoNonRec rB, MinInfoNonRec rA) => MinInfoNonRec (T2 Dep ff rB rA) where+ minInfoNonRec (deApp2 -> (ff, rB, rA)) = plug10' (minCtors ff) (minInfoNonRec rB) (minInfoNonRec rA)++++instance (VRepeat ts) => MinInfoRec (Void t) ts where minInfoRec _ _ = minima1ToSiblingInT void+instance MinInfoNonRec (Void t) where minInfoNonRec = nCtors' 0++++deN :: Proxy (N dc) -> Proxy dc+deN _ = Proxy++instance MinInfoRec (Rep dc) ts => MinInfoRec (N dc) ts where+ minInfoRec = minInfoRec . pRep . deN+instance MinInfoNonRec (Rep dc) => MinInfoNonRec (N dc) where+ minInfoNonRec = minInfoNonRec . pRep . deN++++++deC :: Proxy (C t r) -> Proxy r+deC _ = Proxy++instance MinInfoRec r ts => MinInfoRec (C dc r) ts where+ minInfoRec = (MMap.map (fmap succ) .) . minInfoRec . deC+instance MinInfoNonRec r => MinInfoNonRec (C dc r) where+ minInfoNonRec = MMap.map (fmap succ) . minInfoNonRec . deC++++dePlus :: Proxy (l :+: r) -> (Proxy l, Proxy r)+dePlus _ = (Proxy, Proxy)++instance (Ord (CVec ts NRec), MinInfoRec l ts, MinInfoRec r ts) => MinInfoRec (l :+: r) ts where+ minInfoRec (dePlus -> (l, r)) pts = minInfoRec l pts `mappend` minInfoRec r pts+instance (MinInfoNonRec l, MinInfoNonRec r) => MinInfoNonRec (l :+: r) where+ minInfoNonRec (dePlus -> (l, r)) = minInfoNonRec l `mappend` minInfoNonRec r++++instance MinInfoNonRec U where minInfoNonRec = nCtors' 0+instance (VRepeat ts) => MinInfoRec U ts where minInfoRec _ _ = minima1ToSiblingInT void++deTimes :: Proxy (l :*: r) -> (Proxy l, Proxy r)+deTimes _ = (Proxy, Proxy)++instance (Ord (CVec ts NRec), VRepeat ts, MinInfoRec l ts, MinInfoRec r ts) => MinInfoRec (l :*: r) ts where+ minInfoRec (deTimes -> (l, r)) pts =+ addSiblingInTs (minInfoRec l pts) (minInfoRec r pts)+instance (MinInfoNonRec l, MinInfoNonRec r) => MinInfoNonRec (l :*: r) where+ minInfoNonRec (deTimes -> (l, r)) = addMinima2 (minInfoNonRec l) (minInfoNonRec r)++++instance MinInfoNonRec Par1 where minInfoNonRec _ = MMap.singleton (1, 0) $ Min 0+instance MinInfoNonRec Par0 where minInfoNonRec _ = MMap.singleton (0, 1) $ Min 0+instance (VRepeat ts, MinInfoNonRec Par1) => MinInfoRec Par1 ts where+ minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p+instance (VRepeat ts, MinInfoNonRec Par0) => MinInfoRec Par0 ts where+ minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p++++deRec0 :: Proxy (T0 (Rec lbl) t) -> Proxy lbl+deRec0 _ = Proxy++instance (IndexInto lbl ts, VRepeat ts) => MinInfoRec (T0 (Rec lbl) t) ts where+ minInfoRec (deRec0 -> plbl) pts =+ MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0++deRec1 :: Proxy (T1 (Rec lbl) t r) -> Proxy lbl+deRec1 _ = Proxy++-- TODO: how to support non-regular data types?++-- NB only supports regular data types for now+instance (IndexInto lbl ts, VRepeat ts) => MinInfoRec (T1 (Rec lbl) t Par0) ts where+ minInfoRec (deRec1 -> plbl) pts =+ MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0++deRec2 :: Proxy (T2 (Rec lbl) t r s) -> Proxy lbl+deRec2 _ = Proxy++class Regularish r s where+ regularish :: ((r ~ Par1, s ~ Par0) => a) -> ((r ~ Par0, s ~ Par1) => a) -> a+instance Regularish Par1 Par0 where regularish x _ = x+instance Regularish Par0 Par1 where regularish _ y = y+-- NB no other instances!++-- NB only supports regularish data types for now+instance (Regularish r s, IndexInto lbl ts, VRepeat ts) => MinInfoRec (T2 (Rec lbl) t r s) ts where+ minInfoRec (deRec2 -> plbl) pts =+ MMap.singleton (cvUpd (cvRepeat 0) (indexInto plbl pts) $ \_ -> 1, 0, 0) $ Min 0++++deDep0 :: Proxy (T0 v t) -> Proxy t+deDep0 _ = Proxy++instance (VRepeat ts, MinInfoNonRec (T0 Dep t)) => MinInfoRec (T0 Dep t) ts where+ minInfoRec p _ = minima1ToSiblingInT $ minInfoNonRec p++instance MinCtors t => MinInfoNonRec (T0 Dep t) where+ minInfoNonRec = maybe MMap.empty (MMap.singleton (0, 0) . Min) . minCtors . deDep0++++++pDTs :: Proxy t -> Proxy (DTs t)+pDTs _ = Proxy++class MinCtorsTrim t where minCtorsTrim :: Proxy t -> Minima2 -> MinCtorsT t+instance MinCtorsTrim (t :: *) where+ minCtorsTrim _ m = getMin `fmap` MMap.lookup (0, 0) m+instance MinCtorsTrim (t :: * -> *) where+ minCtorsTrim _ = MMap.mapWithMonoKeys (\(_, nP0) -> nP0) id+instance MinCtorsTrim (t :: * -> * -> *) where minCtorsTrim _ = id++gen_minCtors :: (MinCtorsTrim t, MinCtorsWorker t (DTs t)) => Proxy t -> MinCtorsT t+gen_minCtors p = minCtorsTrim p $ method p (pDTs p)++type family MinCtorsT (t :: k) :: *+type instance MinCtorsT (t :: *) = Maybe Int+type instance MinCtorsT (t :: * -> *) = Minima1+type instance MinCtorsT (t :: * -> * -> *) = Minima2++class MinCtors t where+ minCtors :: Proxy t -> MinCtorsT t+ default minCtors :: (MinCtorsTrim t, MinCtorsWorker t (DTs t)) => Proxy t -> MinCtorsT t+ minCtors = gen_minCtors++class MinCtorsWorker t dpos where method :: Proxy t -> Proxy dpos -> Minima2++pSiblingDTs :: Proxy t -> Proxy (SiblingDTs t)+pSiblingDTs _ = Proxy++instance MinInfoNonRec (DCs t) => MinCtorsWorker t NonRecDT where method pt _ = minInfoNonRec (pDisband pt)++pIndex :: Proxy (RecDT l r) -> Proxy (Length l)+pIndex _ = Proxy++instance (IndexInto (Length l) (SiblingDTs t),+ VInitialize (MinInfo__ (SiblingDTs t)) (SiblingDTs t),+ VFunctor (SiblingInC (SiblingDTs t)) (SiblingDTs t),+ VRepeat (SiblingDTs t),+ VEnum (SiblingDTs t),+ Eq (CVec (SiblingDTs t) Minima2),+ MinInfoRec (DCs t) (SiblingDTs t)) => MinCtorsWorker t (RecDT l r) where+ method pt pdpos = (`cvAt` indexInto (pIndex pdpos) psibs) $ solve_sibling_set' $+ cvInitialize (pcon psibs) minInfo__+ where psibs = pSiblingDTs pt+ pcon :: Proxy ts -> Proxy (MinInfo__ ts)+ pcon _ = Proxy++class (MinInfoRec (DCs t) ts, ts ~ SiblingDTs t) => MinInfo__ ts t+instance (MinInfoRec (DCs t) ts, ts ~ SiblingDTs t) => MinInfo__ ts t++minInfo__ :: MinInfo__ ts t => Proxy t -> SiblingInT ts+minInfo__ p = minInfoRec (pDisband p) (pSiblingDTs p)++++++++++{-++-- T tests support for interesting structures as well as avoiding the recursive+-- branch+data T a = One a | Branch (T a, [T a]) Int++yokoTH ''T++++++-- S tests one interesting way that the final answer depends on the parameter+data S a = OneS a | BranchS Int Int++yokoTH ''S++++-- M1 and M2 exercise the erroneous definition for Recs+data M1 = M1C Int Int Int Int | M1D M2+data M2 = M2C M1++yokoTH ''M1+yokoTH ''M2+++++yokoTH ''Nat++++data Inf = Inf Inf++yokoTH ''Inf++++++data X a = X a a a a++yokoTH ''X++data Y a = Y (X (X a))++yokoTH ''Y++++data Stream a = SCons a (Stream a)+type instance DTs Stream = RecDT '[] '[]++yokoTH ''Stream++data Even a = ENil | ECons a (Odd a)+data Odd a = OCons a (Even a)++yokoTH ''Even+yokoTH ''Odd+++++instance MinCtors X+instance MinCtors a => MinCtors (X a)++instance MinCtors Y+instance MinCtors a => MinCtors (Y a)++instance MinCtors Stream+instance MinCtors a => MinCtors (Stream a)++instance MinCtors T+instance MinCtors a => MinCtors (T a)+instance MinCtors S+instance MinCtors a => MinCtors (S a)+instance MinCtors M1+instance MinCtors M2+instance MinCtors Inf++instance MinCtors Nat+++instance MinCtors Even+instance MinCtors Odd+instance MinCtors a => MinCtors (Even a)+instance MinCtors a => MinCtors (Odd a)++-}++++++--------------------+-- usages+instance MinCtors Bool+instance MinCtors ()++instance MinCtors (,)+instance MinCtors a => MinCtors ((,) a)+instance (MinCtors a, MinCtors b) => MinCtors ((,) a b)++instance MinCtors a => MinCtors ((,,) a)+instance (MinCtors a, MinCtors b) => MinCtors ((,,) a b)+instance (MinCtors a, MinCtors b, MinCtors c) => MinCtors ((,,) a b c)++instance MinCtors Maybe+instance MinCtors a => MinCtors (Maybe a)++instance MinCtors []+instance MinCtors a => MinCtors [a]++instance MinCtors Either+instance MinCtors a => MinCtors (Either a)+instance (MinCtors a, MinCtors b) => MinCtors (Either a b)++instance MinCtors GHC.Real.Ratio+instance MinCtors a => MinCtors (GHC.Real.Ratio a)
+ Data/Yoko/MinCtors/MMap.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE StandaloneDeriving, FlexibleContexts, UndecidableInstances #-}++-- | Like 'Map' but with a 'Monoid' instance that respects the value type's+-- 'Semigroup' instance.++module Data.Yoko.MinCtors.MMap where++import Data.Monoid++import Data.Semigroup (Semigroup)+import qualified Data.Semigroup as Semigroup++import Data.Map (Map)+import qualified Data.Map as Map++import qualified Data.Foldable as F++++newtype MMap k f v = MMap {unMMap :: Map k (f v)}++deriving instance Eq (Map k (f v)) => Eq (MMap k f v)+deriving instance Show (Map k (f v)) => Show (MMap k f v)++map f (MMap m) = MMap $ Map.map f m++singleton k v = MMap $ Map.singleton k v++null (MMap m) = Map.null m++empty :: MMap k f v+empty = MMap Map.empty++instance (Ord k, Semigroup (f v)) => Monoid (MMap k f v) where+ mempty = MMap Map.empty+ MMap x `mappend` MMap y = MMap $ Map.unionWith (Semigroup.<>) x y++foldMap :: Monoid m => (k -> f v -> m) -> MMap k f v -> m+foldMap f (MMap m) = F.foldMap (uncurry f) $ Map.toList m++mapWithMonoKeys :: (k -> k1) -> (f v -> g v1) -> MMap k f v -> MMap k1 g v1+mapWithMonoKeys fk fv (MMap m) =+ MMap $ Map.mapKeysMonotonic fk $ Map.map fv m++lookup :: Ord k => k -> MMap k f v -> Maybe (f v)+lookup k (MMap m) = Map.lookup k m
+ Data/Yoko/MinCtors/Minima.hs view
@@ -0,0 +1,165 @@+{-# LANGUAGE ScopedTypeVariables, PolyKinds, DataKinds, MultiParamTypeClasses,+ TypeFamilies, UndecidableInstances, FlexibleInstances, FlexibleContexts #-}++module Data.Yoko.MinCtors.Minima+ (NCtor, NRec, NP1, NP0, Minima2, Minima1, Minimum,+ DTsCVec, SumInfo, SC_SumInfo,+ SiblingInT, SiblingInC, addMinima2, addSiblingInTs,+ solve_sibling_set, solve_sibling_set',+ plug10, plug0, plug10', plug0') where++import Data.Yoko.TypeBasics++import Data.Yoko.View++import Data.Yoko.MinCtors.MMap (MMap)+import qualified Data.Yoko.MinCtors.MMap as MMap++import qualified Data.Foldable as F++import Data.Semigroup (Min(..))++import Data.Traversable (traverse)+import Data.Maybe (catMaybes)++++instance Functor Min where fmap f (Min a) = Min (f a)++++--------------------+-- an appropriate abstraction for the MinCtors question+type NCtor = Int+type NRec = Int+type NP1 = Int+type NP0 = Int++type Minima2 = MMap (NP1, NP0) Min NCtor+type Minima1 = MMap NP0 Min NCtor+type Minimum = MMap () Min NCtor++-- scale each coordinate+scale :: Int -> Minima2 -> Minima2+scale i = MMap.mapWithMonoKeys (\(np1, np0) -> (i * np1, i * np0)) (fmap (i *))++-- take Cartesian product, add coordinates point-wise, and re\"normalize\"+addMinima2 :: Minima2 -> Minima2 -> Minima2+addMinima2 m m' = flip MMap.foldMap m $ \(np1, np0) (Min k) ->+ flip MMap.foldMap m' $ \(np1', np0') (Min k') ->+ MMap.singleton (np1 + np1', np0 + np0') (Min $ k + k')++-- product and sum info+type DTsCVec t = CVec (SiblingDTs t)++type SumInfo t = MMap (DTsCVec t NRec, NP1, NP0) Min NCtor++scaleSiblingInTs :: Int -> SiblingInT ts -> SiblingInT ts+scaleSiblingInTs i = MMap.mapWithMonoKeys (\(r, np1, np0) -> (fmap (i *) r, i * np1, i * np0)) (fmap (i *))++addSiblingInTs :: Ord (CVec ts NRec) => SiblingInT ts -> SiblingInT ts -> SiblingInT ts+addSiblingInTs m m' = flip MMap.foldMap m $ \(rs, np1, np0) (Min k) ->+ flip MMap.foldMap m' $ \(rs', np1', np0') (Min k') ->+ MMap.singleton (cvZipWith (+) rs rs', np1 + np1', np0 + np0') (Min $ k + k')++++++--------------------+-- solve a sibling set++-- let cnv x = ($ x) $ MMap . Map.fromList . map (\(recs, np1, np0, k) -> ((recs, np1, np0), k))++-- TODO Put an interface around 'solve' so it can also be applied to+-- non-recursive data types -- this might involve a token type representing the+-- entire "sibling set", even for non-recursive types++-- TODO how to memoize the sibling set analysis as a CAF with all siblings'+-- MinCtors dictionaries sharing the CAF's elements?++-- | @type instance 'App' SC_SumInfo t = 'SumInfo' t@+data SC_SumInfo t = SC_SumInfo+type instance App SC_SumInfo t = SumInfo t++solve_sibling_set ::+ (Eq (CVec ts Minima2), VRepeat ts,+ VFunctor (SiblingInC ts) ts, VEnum ts) => Vec ts SC_SumInfo -> Work ts+solve_sibling_set = solve_sibling_set' . homogenize++solve_sibling_set' ::+ (Eq (CVec ts Minima2), VRepeat ts, VEnum ts) => CVec ts (SiblingInT ts) -> Work ts+solve_sibling_set' table = chaotic (step table) $ initialize table++-- 1) start with the smallest non-recursive ctors++-- 2) build up only from those, so we're maintaining a correct answer the+-- entire time++-- 3) codata siblings end up as MMap.empty.++-- the work set holds the sofar determined answers -- only the ones that are+-- gauranteed to be minimal. Codata siblings never get changed from MMap.empty.+type Work ts = CVec ts Minima2++-- like SC_SumInfo except parameterized over the sibling set instead of just a+-- single sibling+type SiblingInT ts = MMap (CVec ts NRec, NP1, NP0) Min NCtor++-- switch to a 'CVec', since all of the 'DTs' instances are compatible...+homogenize :: forall ts. VFunctor (SiblingInC ts) ts =>+ Vec ts SC_SumInfo -> CVec ts (SiblingInT ts)+homogenize = (CVec .) $ vMap (Proxy :: Proxy (SiblingInC ts)) $ \_ -> id++-- ...in this way+class (ts ~ SiblingDTs t) => SiblingInC (ts :: [k]) (t :: k)+instance (ts ~ SiblingDTs t) => SiblingInC ts t++-- the initial work set is the siblings' smallest non-recursive constructors+initialize :: CVec ts (SiblingInT ts) -> Work ts+initialize = fmap $ \ctors -> flip MMap.foldMap ctors $ \(recs, np1, np0) k ->+ if F.all (0 ==) recs -- non-recursive ctor iff no recursive occurrences+ then MMap.singleton (np1, np0) k+ else MMap.empty++-- extend the working set with the unsolved siblings that are now soluble+step :: VEnum ts => CVec ts (SiblingInT ts) -> Work ts -> Work ts+step table sofar = cvZipWith leftbias sofar $ flip fmap table $+ MMap.foldMap $ \(recs, np1, np0) k -> -- fold over products in this sibling+ -- if all of its non-zero NRecs are solved...+ let all_answered = flip traverse (cvAddIndexes recs) $ \(idx, times) ->+ if times <= 0 then Just Nothing -- omit without failing+ else let answer = sofar `cvAt` idx+ in if MMap.null answer then Nothing -- fail+ else Just $ Just $ scale times answer -- emit+ in ($ all_answered) $ maybe MMap.empty $+ foldl addMinima2 (MMap.singleton (np1, np0) k) . catMaybes . cvec2list++leftbias m1 m2 = if MMap.null m1 then m2 else m1++-- rinse and repeat until clean+chaotic :: Eq a => (a -> a) -> a -> a+chaotic f = w where w x = let x' = f x in if x == x' then x else w x'++++++--------------------+-- combining minima++plug0 :: Ord (CVec ts NRec) => Minima1 -> SiblingInT ts -> SiblingInT ts+plug0 f s0 = flip MMap.foldMap f $ \np0 (Min k) ->+ MMap.map (fmap (+k)) $ scaleSiblingInTs np0 s0++plug10 :: Ord (CVec ts NRec) => Minima2 -> SiblingInT ts -> SiblingInT ts -> SiblingInT ts+plug10 f s1 s0 = flip MMap.foldMap f $ \(np1, np0) (Min k) ->+ MMap.map (fmap (+k)) $ scaleSiblingInTs np1 s1 `addSiblingInTs` scaleSiblingInTs np0 s0++plug0' :: Minima1 -> Minima2 -> Minima2+plug0' f s0 = flip MMap.foldMap f $ \np0 (Min k) ->+ MMap.map (fmap (+k)) $ scale np0 s0++plug10' :: Minima2 -> Minima2 -> Minima2 -> Minima2+plug10' f s1 s0 = flip MMap.foldMap f $ \(np1, np0) (Min k) ->+ MMap.map (fmap (+k)) $ scale np1 s1 `addMinima2` scale np0 s0
+ Data/Yoko/MinCtors/Prims0.hs view
@@ -0,0 +1,16 @@+module Data.Yoko.MinCtors.Prims0 where++import qualified GHC.Word+import qualified GHC.ForeignPtr++import Data.Yoko.MinCtors++++instance MinCtors Int where minCtors = nCtors 0+instance MinCtors Integer where minCtors = nCtors 0+instance MinCtors Char where minCtors = nCtors 0+instance MinCtors Float where minCtors = nCtors 0+instance MinCtors Double where minCtors = nCtors 0+instance MinCtors GHC.Word.Word8 where minCtors = nCtors 0+instance MinCtors GHC.ForeignPtr.ForeignPtr where minCtors = nCtors 0
+ Data/Yoko/MinCtors/Prims1.hs view
@@ -0,0 +1,16 @@+module Data.Yoko.MinCtors.Prims1 where++import qualified GHC.Word+import qualified GHC.ForeignPtr++import Data.Yoko.MinCtors++++instance MinCtors Int where minCtors = nCtors 1+instance MinCtors Integer where minCtors = nCtors 1+instance MinCtors Char where minCtors = nCtors 1+instance MinCtors Float where minCtors = nCtors 1+instance MinCtors Double where minCtors = nCtors 1+instance MinCtors GHC.Word.Word8 where minCtors = nCtors 1+instance MinCtors GHC.ForeignPtr.ForeignPtr where minCtors = nCtors 1
+ Data/Yoko/Prelude.hs view
@@ -0,0 +1,77 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators,+ UndecidableInstances, DataKinds, LambdaCase #-}++module Data.Yoko.Prelude where++import qualified GHC.Real++import Data.Yoko.TH+import Data.Yoko.W+import Data.YokoRaw++import Type.Spine (spineType_d)+import Type.Serialize (serializeTypeAsHash_data)+++yokoTH ''Bool+++yokoTH ''()++type instance DTs (,,) = NonRecDT++yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''GHC.Real.Ratio+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''(,)+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''(,,)+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''Maybe+yokoTH_with (yokoDefaults {invInsts = \_ -> False}) ''Either++data Nil_ (p0 :: *) = Nil_+data Cons_ (p0 :: *) = Cons_ p0 [p0]++spineType_d ''Nil_+spineType_d ''Cons_++serializeTypeAsHash_data ''Nil_+serializeTypeAsHash_data ''Cons_++type instance Codomain Nil_ = []+type instance Codomain Cons_ = []++type instance Codomain (Nil_ a) = [a]+type instance Codomain (Cons_ a) = [a]++type instance Rep (Nil_ a) = Subst0 Nil_ a+instance Generic (Nil_ a) where+ rep = W0 $ \_ -> C U+ obj = W'0 $ \_ -> Nil_++type instance Rep Nil_ = C Nil_ U+instance Generic Nil_ where+ rep = W1 $ \_ -> C U+ obj = W'1 $ \_ -> Nil_++type instance Rep (Cons_ a) = Subst0 Cons_ a+instance Generic (Cons_ a) where+ rep = W0 $ \(Cons_ a as) -> C (T0 a :*: T0 as)+ obj = W'0 $ \(C (T0 a :*: T0 as)) -> Cons_ a as++type instance Rep Cons_ = C Cons_ (Par0 :*: T1 (Rec 'Z) [] Par0)+instance Generic Cons_ where+ rep = W1 $ \(Cons_ a as) -> C (Par0 a :*: T1 (map Par0 as))+ obj = W'1 $ \(C (Par0 a :*: T1 as)) -> Cons_ a (map unPar0 as)++type instance DTs [] = RecDT '[] '[]+type instance DCs [] = N Nil_ :+: N Cons_+type instance DTs [a] = RecDT '[] '[]+type instance DCs [a] = N (Nil_ a) :+: N (Cons_ a)++instance (EQ ~ SpineCompare a a) => DT [a] where+ disband = W0 $ \case+ [] -> L $ N0 $ Nil_+ a : as -> R $ N0 $ Cons_ a as++instance DT [] where+ disband = W1 $ \case+ [] -> L $ N1 $ Nil_+ a : as -> R $ N1 $ Cons_ a as
Data/Yoko/Representation.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies, TypeOperators, TemplateHaskell,- UndecidableInstances, EmptyDataDecls, DataKinds #-}+ UndecidableInstances, EmptyDataDecls, DataKinds, PolyKinds,+ MultiParamTypeClasses, FlexibleInstances #-} {- | @@ -19,88 +20,143 @@ (-- * Representation -- ** Sums Void(..), N(..), (:+:)(..),+ C(..), -- ** Products U(..), (:*:)(..), -- ** Fields- Rec(..), Dep(..), Par1(..), Par2(..),+ T0(..), T1(..), T2(..), Variety(..),+ Par1(..), Par0(..), -- ** Conversions to and from fields-of-products structure Rep, Generic(..), -- ** Auxilliaries- unN, foldN, mapN,- foldPlus, mapPlus,+ unC, foldC, mapC,+ WN(..),+ unN0, foldN0, mapN0,+ unN1, foldN1, mapN1,+ unN2, foldN2, mapN2,+ foldPlus, FoldPlusW'(..), mapPlus, foldTimes, mapTimes,- unRec, mapRec, unDep, unPar1, unPar2,+ unT0, mapT0,+ unT1, mapT1,+ unT2, mapT2,+ unPar0, mapPar0,+ unPar1, mapPar1, DistMaybePlus ) where +import Data.Yoko.W import Data.Yoko.TypeBasics +data Variety = Rec Nat | Dep++++-- | Wrapper around productus+newtype C dc r (p1 :: *) (p0 :: *) = C (r p1 p0)+ -- | The empty product.-data U = U+data U (p1 :: *) (p0 :: *) = U infixr 6 :*: -- | Product union.-data a :*: b = a :*: b+data (:*:) a b (p1 :: *) (p0 :: *) = a p1 p0 :*: b p1 p0 -- | The empty sum. Used as an error type instead of a represention type, since -- data types with no constructors are uninteresting from a generic programming -- perspective -- there's just not much to be done generically.-data Void+data Void (p1 :: *) (p0 :: *) -- | The singleton sum.-newtype N a = N a+data family N (dc :: k) :: * -> * -> *+newtype instance N dc (p1 :: *) (p0 :: *) = N0 dc+newtype instance N dc (p1 :: *) (p0 :: *) = N1 (dc p0)+newtype instance N dc (p1 :: *) (p0 :: *) = N2 (dc p1 p0) infixl 6 :+: -- | Sum union.-data a :+: b = L a | R b deriving (Eq, Show, Ord, Read)+data (:+:) a b (p1 :: *) (p0 :: *) = L (a p1 p0) | R (b p1 p0) deriving (Eq, Show, Ord, Read) --- | Representation of unary type application. @f@ is a genuine @*->*@ type,--- not a representation. @a@ is a representation.-newtype Par1 f a = Par1 (f a) --- | Representation of binary type application. @f@ is a genuine @*->*->*@--- type, not a representation. @a@ and @b@ are representations.-newtype Par2 f a b = Par2 (f a b)+-- | An occurrence of the 1st parameter.+newtype Par1 (p1 :: *) (p0 :: *) = Par1 p1 +-- | An occurrence of the zeroth parameter.+newtype Par0 (p1 :: *) (p0 :: *) = Par0 p0 --- | A non-recursive occurrence.-newtype Dep a = Dep a --- | A recursive occurrence.-newtype Rec a = Rec a +newtype T0 (v :: Variety) t (p1 :: *) (p0 :: *) = T0 t+newtype T1 (v :: Variety) (t :: * -> *) a (p1 :: *) (p0 :: *) = T1 (t (a p1 p0))+newtype T2 (v :: Variety) (t :: * -> * -> *) b a (p1 :: *) (p0 :: *) = T2 (t (b p1 p0) (a p1 p0)) + -- | A mapping to the structural representation of a fields type: just products -- of fields, no sums -- fields types have just one constructor.-type family Rep a+type family Rep (t :: k) :: * -> * -> * -- | Converts between a fields type and its product-of-fields structure.-class Generic a where rep :: a -> Rep a; obj :: Rep a -> a+class Generic dc where+ rep :: W dc (Rep dc) p1 p0; obj :: W' dc (Rep dc) p1 p0 -unDep (Dep x) = x -unRec (Rec x) = x-mapRec f (Rec x) = Rec (f x)+class ComposeW dc => WN dc where+ nN :: W dc (N dc) p1 p0+ unN :: W' dc (N dc) p1 p0+instance WN (dc :: *) where nN = W0 N0; unN = W'0 unN0+instance WN (dc :: * -> *) where nN = W1 N1; unN = W'1 unN1+instance WN (dc :: * -> * -> *) where nN = W2 N2; unN = W'2 unN2 +unT0 (T0 x) = x+mapT0 f (T0 x) = T0 (f x)++unT1 (T1 x) = x+mapT1 f (T1 x) = T1 (f x)++unT2 (T2 x) = x+mapT2 f (T2 x) = T2 (f x)++unPar0 (Par0 x) = x+mapPar0 f (Par0 x) = Par0 (f x)+ unPar1 (Par1 x) = x-unPar2 (Par2 x) = x+mapPar1 f (Par1 x) = Par1 (f x) -unN (N x) = x-foldN f = f . unN -mapN f = N . foldN f +unC (C x) = x+foldC f = f . unC+mapC f = foldC (C . f)++unN0 (N0 x) = x+foldN0 f = f . unN0++unN1 (N1 x) = x+foldN1 f = f . unN1++unN2 (N2 x) = x+foldN2 f = f . unN2++mapN0 f = N0 . foldN0 f+mapN1 f = N1 . foldN1 f+mapN2 f = N2 . foldN2 f+ foldPlus f g x = case x of L x -> f x ; R x -> g x +class FoldPlusW' (s :: k) where+ foldPlusW' :: W' s l p1 p0 -> W' s r p1 p0 -> W' s (l :+: r) p1 p0+instance FoldPlusW' (s :: *) where foldPlusW' (W'0 f) (W'0 g) = W'0 $ foldPlus f g+instance FoldPlusW' (s :: * -> *) where foldPlusW' (W'1 f) (W'1 g) = W'1 $ foldPlus f g+instance FoldPlusW' (s :: * -> * -> *) where foldPlusW' (W'2 f) (W'2 g) = W'2 $ foldPlus f g+ mapPlus f g = foldPlus (L . f) (R . g) mapTimes f g (a :*: b) = f a :*: g b@@ -112,26 +168,28 @@ -- | We avoid empty sums with a type-level @Maybe@. @DistMaybePlus@ performs -- sum union on lifted sums, only introducing @:+:@ when both arguments are -- @Just@s.-type family DistMaybePlus (a :: Maybe *) (b :: Maybe *) :: Maybe *+type family DistMaybePlus (a :: Maybe (* -> * -> *)) (b :: Maybe (* -> * -> *)) :: Maybe (* -> * -> *) type instance DistMaybePlus Nothing b = b type instance DistMaybePlus (Just a) Nothing = Just a type instance DistMaybePlus (Just a) (Just b) = Just (a :+: b) --data Z; data S n-type family Add n m+{-+data Nat = Z | S Nat+type family Add (n :: Nat) (m :: Nat) :: Nat type instance Add Z m = m type instance Add (S n) m = S (Add n m) -type family CountRs rep+type family CountRs (rep :: * -> * -> *) :: Nat type instance CountRs (Dep a) = Z type instance CountRs (Rec a) = S Z type instance CountRs U = Z type instance CountRs (a :*: b) = Add (CountRs a) (CountRs b)+-} -concat `fmap` mapM derive_data [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]+concat `fmap` mapM derive_data [''Variety, ''T0, ''T1, ''T2, ''Par1, ''Par0, ''C, ''U, ''(:*:), ''N, ''(:+:)]+concat `fmap` mapM derive_pro ['Rec, 'Dep, 'Z, 'S]
Data/Yoko/SmartPreciseCase.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances #-}+{-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts, TypeFamilies, UndecidableInstances, Rank2Types #-} {- | @@ -25,16 +25,16 @@ -} -module Data.Yoko.SmartPreciseCase where+module Data.Yoko.SmartPreciseCase (precise_case0, Default(..)) where -import Data.YokoRaw hiding (precise_case)+import Data.YokoRaw hiding (precise_case0) import qualified Data.YokoRaw as Raw class Error_precise_case_requires_at_least_1_special_case a -data AdHoc dcs dt r = AdHoc dt (dcs -> r)-newtype Default a = Default a+data AdHoc dcs dt r = AdHoc dt (forall p1 p0. dcs p1 p0 -> r)+newtype Default a r = Default (forall p1 p0. a p1 p0 -> r) @@ -43,7 +43,7 @@ class Builder adhoc bldr where precise_case_ :: adhoc -> bldr -instance Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a -> b) where+instance Error_precise_case_requires_at_least_1_special_case () => Builder (Start dt) (Default a final -> b) where precise_case_ = error "precise_case_ requires at least 1 special case" newtype Start dt = Start dt@@ -53,20 +53,20 @@ Builder (Start dt) ((dc -> r) -> bldr) where precise_case_ (Start dt) f = precise_case_ $ AdHoc dt $ one f -instance (dt ~ Codomain dc, dt ~ Codomain dcs, r ~ r', -- False ~ Elem dc dcs,+instance (dt ~ Codomain dc, dt ~ Codomain0 dcs, r ~ r', -- False ~ Elem dc dcs, Builder (AdHoc (dcs :+: N dc) dt r) bldr) => Builder (AdHoc dcs dt r) ((dc -> r') -> bldr) where precise_case_ (AdHoc dt adhoc) f = precise_case_ $ AdHoc dt $ adhoc ||. f -instance (DT dt, dt ~ Codomain dcs, dt ~ Codomain (DCs dt),+instance (DT dt, dt ~ Codomain0 dcs, dt ~ Codomain0 (DCs dt), Partition (DCs dt) dcs (DCs dt :-: dcs),- x ~ (DCs dt :-: dcs -> r),- final ~ r) =>- Builder (AdHoc dcs dt r) (Default x -> final) where- precise_case_ (AdHoc dt adhoc) (Default dflt) = Raw.precise_case dflt dt adhoc+ x ~ (DCs dt :-: dcs),+ final ~ r, final' ~ r) =>+ Builder (AdHoc dcs dt r) (Default x final -> final') where+ precise_case_ (AdHoc dt adhoc) (Default dflt) = Raw.precise_case0 dflt dt adhoc -precise_case :: Builder (Start dt) bldr => dt -> bldr-precise_case = precise_case_ . Start+precise_case0 :: Builder (Start dt) bldr => dt -> bldr+precise_case0 = precise_case_ . Start
Data/Yoko/TH.hs view
@@ -1,4 +1,5 @@-{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards, DataKinds #-}+{-# LANGUAGE TypeOperators, ViewPatterns, TemplateHaskell, PatternGuards,+ DataKinds, LambdaCase #-} {- | @@ -21,7 +22,7 @@ Each 'Mapping' specifies a representation type, its constructor, and a structure-preserving mapping function. The default options handle applications-of @*->*@ and @*->*->*@ types with the 'Par1' and 'Par2' types from+of @*->*@ and @*->*->*@ types with the 'T1' and 'T2' types from "Data.Yoko.Representation" and uses the 'invmap' and 'invmap2' mapping functions from the @invariant@ package. @@ -29,7 +30,7 @@ is applied at kind @*->*->*@. It can, however handle @data U = C0 | C1 (Int, U, U)@, since @(,,) Int@ is applied at kind @*->*->*@ -- the kind of the application is determined by the leftmost argument with a recursive-occurrence. In this case, @yokoTH@ uses the default @Mapping ''Par2 'Par2+occurrence. In this case, @yokoTH@ uses the default @Mapping ''T2 'T2 'invmap2@. The following invocation of @yokoTH_with@ can handle @T@, since it provides an@@ -66,10 +67,13 @@ import Type.Serialize (serializeTypeAsHash_data) import qualified Type.Ord as Ord -import Data.Yoko.TypeBasics (encode)+import Data.Yoko.TypeBasics (encode, Nat(..))+import Data.Yoko.W import Data.Yoko.Representation import Data.Yoko.View +import Data.Yoko.Invariant+ import Language.Haskell.TH as TH hiding (Codomain) import Language.Haskell.TH.Syntax as TH hiding (Codomain) import qualified Language.Haskell.TH.SCCs as SCCs@@ -77,17 +81,20 @@ import qualified Data.Yoko.TH.Internal as Int import Data.Yoko.TH.Internal (tvbName, peelApp, peelAppAcc, expandSyn) -import Data.Functor.Invariant (invmap, invmap2)- import qualified Control.Monad.Writer as Writer import qualified Control.Monad.Trans as Trans+import Control.Monad (liftM, when, foldM) import qualified Control.Arrow as Arrow import Data.Set (Set) import qualified Data.Set as Set+import Data.Map (Map)+import qualified Data.Map as Map import qualified Data.List as List +import Data.Maybe (catMaybes)+ import Data.Kind (KindStar(..)) import Data.TypeFun import Data.Record hiding (convert, Name)@@ -98,32 +105,50 @@ +w0' :: (t p1 p0 -> s ) -> W' s t p1 p0; w0' = W'0+w1' :: (t p1 p0 -> s p0) -> W' s t p1 p0; w1' = W'1+w2' :: (t p1 p0 -> s p1 p0) -> W' s t p1 p0; w2' = W'2 ++++ convert r = R.convert $ R.withStyle r (Id KindStar) -data Target = Target deriving Show-data Renamer = Renamer deriving Show+data Target = Target deriving Show+data Renamer = Renamer deriving Show data Mappings = Mappings deriving Show+data InvInsts = InvInsts deriving Show+data DCInsts = DCInsts deriving Show data BindingGroup = BindingGroup deriving Show-data TargetData = TargetData deriving Show-data TargetType = TargetType deriving Show-data TargetKind = TargetKind deriving Show-instance R.Name Target where name = Target-instance R.Name Renamer where name = Renamer+data TargetData = TargetData deriving Show+data TargetType = TargetType deriving Show+data TargetCxt = TargetCxt deriving Show+data TargetTVBs = TargetTVBs deriving Show+data TargetPars = TargetPars deriving Show+data ConName = ConName deriving Show+data ConFields = ConFields deriving Show+instance R.Name Target where name = Target+instance R.Name Renamer where name = Renamer instance R.Name Mappings where name = Mappings+instance R.Name InvInsts where name = InvInsts+instance R.Name DCInsts where name = DCInsts instance R.Name BindingGroup where name = BindingGroup-instance R.Name TargetData where name = TargetData-instance R.Name TargetType where name = TargetType-instance R.Name TargetKind where name = TargetKind+instance R.Name TargetData where name = TargetData+instance R.Name TargetType where name = TargetType+instance R.Name TargetCxt where name = TargetCxt+instance R.Name TargetTVBs where name = TargetTVBs+instance R.Name TargetPars where name = TargetPars+instance R.Name ConName where name = ConName+instance R.Name ConFields where name = ConFields -- | A 'Mapping' identifies the representation type, its constructor, and the--- associated mapping function. For example, 'Par1' is represented with--- @Mapping ''Par1 'Par1 'invmap@.+-- associated mapping function. For example, 'T1' is represented with @Mapping+-- ''T1 'T1 'invmap@. data Mapping = Mapping- {containerTypeName :: Name, containerCtor :: Name,- methodName :: Name}+ {containerTypeName :: Name, containerCtor :: Name, methodName :: Name} -- | The default @yoko@ derivations can be customised. data YokoOptions = YokoOptions@@ -131,12 +156,19 @@ -- @(++ \"_\")@. renamer :: (String -> String) -> (String -> String), -- | How applications of higher-rank data types are represented. Defaults- -- to @[(1, 'Mapping' ''Par1 'Par1 'invmap), (2, 'Mapping' ''Par2 'Par2 'invmap2)]@.- mappings :: [(Int, Mapping)] -> [(Int, Mapping)]}+ -- to @[(1, 'Mapping' ''T1 'T1 'invmap), (2, 'Mapping' ''T2 'T2+ -- 'invmap2)]@.+ mappings :: [(Int, Mapping)] -> [(Int, Mapping)],+ -- | Should instances of 'Invariant' also be automatically derived for this+ -- type? Defaults to @True@.+ invInsts :: Bool -> Bool,+ -- | For which constructors should instances of 'Rep' and 'Generic' be+ -- automatically derived? Defaults to the set of all constructors.+ dcInsts :: [Name] -> [Name]} --- | The default options. @yokoDefaults = YokoOptions id id@.+-- | The default options. @yokoDefaults = YokoOptions id id id@. yokoDefaults :: YokoOptions-yokoDefaults = YokoOptions id id+yokoDefaults = YokoOptions id id id id type M r = Writer.WriterT [Dec] Q @@ -151,6 +183,11 @@ +concatMapM :: Monad m => (a -> m [b]) -> [a] -> m [b]+concatMapM f = liftM concat . mapM f+++ -- | Derive fields types and all @yoko@ instances for a given data type. yokoTH :: Name -> Q [Dec] yokoTH n = yokoTH_with yokoDefaults n@@ -159,36 +196,34 @@ yokoTH_with :: YokoOptions -> Name -> Q [Dec] yokoTH_with options n = runM $ yoko0 $ X :& Target := n :& Renamer := (mkName . renamer options (++ "_") . TH.nameBase)- :& Mappings := mappings options [(1, Mapping ''Par1 'Par1 'invmap),- (2, Mapping ''Par2 'Par2 'invmap2)]+ :& Mappings := mappings options [(1, Mapping ''T1 'T1 'invmap),+ (2, Mapping ''T2 'T2 'invmap2)]+ :& InvInsts := invInsts options True+ :& DCInsts := dcInsts options -- gather reflective information about the target type yoko0 r@(convert -> X :& Target := n) = do- names <- liftQ $ SCCs.binding_group n- datatype@(Int.DataType tvbs _) <- liftQ $ Int.dataType n-- let ty = applyConT2TVBs n tvbs+ datatype <- liftQ $ Int.dataType n - -- get the kind of the target type; each fields type has the same kind- cxt <- flip mapM tvbs $ \tvb -> liftQ $- EqualP (PromotedT 'EQ) `fmap` do- let tv = [t| Spine $(return $ tvbType tvb) |]- [t| Ord.Compare $tv $tv |]+ scc <- do+ scc <- liftQ $ SCCs.scc n+ case scc of+ Left n -> return $ Left n+ Right ns -> fmap (Right . fst) $ foldM snoc (Map.empty, 0) $ Set.toAscList ns+ where snoc (m, acc) n = liftQ (reify n) >>= return . \case+ TyConI TySynD{} -> (Map.insert n Nothing m, acc)+ _ -> (Map.insert n (Just acc) m, acc + 1) - yoko1 $ r :&- BindingGroup := names :&- TargetData := datatype :&- TargetType := ty :&- TargetKind := (map tvbKind tvbs, cxt)+ yoko1 $ r :& TargetData := datatype :& BindingGroup := scc -- generate fields types conName :: Con -> Name-conName (NormalC n _) = n-conName (RecC n _) = n-conName (InfixC _ n _) = n+conName (NormalC n _) = n+conName (RecC n _) = n+conName (InfixC _ n _) = n conName (ForallC _ _ c) = conName c renameCon :: (Name -> Name) -> Con -> Con@@ -204,6 +239,12 @@ tvbType :: TyVarBndr -> Type tvbType = VarT . tvbName +compose :: Exp -> Exp -> Exp+compose l r = VarE '(.) `AppE` l `AppE` r++postConE :: Name -> Exp -> Exp+postConE n inj = compose (ConE n) inj+ applyConT2TVBs :: Name -> [TyVarBndr] -> Type applyConT2TVBs n tvbs = foldl ((. tvbType) . AppT) (ConT n) tvbs @@ -218,145 +259,263 @@ foldl ((. VarE) . AppE) (ConE ne) ns) where ns = [ mkName $ "x" ++ show i | i <- [0..k - 1] ] -simpleClause pats exp = Clause pats (NormalB exp) []+simpleVal n exp = ValD (VarP n) (NormalB exp) [] halves :: [a] -> b -> (b -> b -> b) -> (a -> b) -> b-halves as nil app each = w (length as) as where+halves as nil appnd single = w (length as) as where w _ [] = nil- w _ [a] = each a- w k as = w lk l `app` w rk r+ w _ [a] = single a+ w k as = w lk l `appnd` w rk r where lk = k `div` 2 ; rk = k - lk (l, r) = List.splitAt lk as +toNat 0 = PromotedT 'Z+toNat n = PromotedT 'S `AppT` toNat (n - 1)+ data FieldRO = FieldRO {repF :: Exp, objF :: Exp} -fieldRO :: [(Int, Mapping)] -> Set Name -> Type -> Q (Type, FieldRO)-fieldRO maps bg = w' where+namesIn :: Type -> Set Name+namesIn (ForallT tvbs _ ty) = namesIn ty `Set.difference` Set.fromList (map tvbName tvbs)+namesIn (AppT ty1 ty2) = namesIn ty1 `Set.union` namesIn ty2+namesIn (SigT ty _) = namesIn ty+namesIn (VarT n) = Set.singleton n+namesIn (ConT n) = Set.singleton n+namesIn _ = Set.empty++fieldRO :: [(Int, Mapping)] -> Either Name (Map Name (Maybe Int)) ->+ [Name] -> -- just the represented parameters (ie Par1 and Par0)+ Type -> Q (Type, FieldRO)+fieldRO maps bg parNs = w' where w' = uncurry w . peelApp - isRec n = Set.member n bg+ isRec = case bg of+ Left _ -> const False+ Right bg -> \n -> Map.member n bg+ isPar n = n `elem` parNs+ isImportant n = isRec n || isPar n - simple b ty tys = return $ (ConT tyn `AppT` foldl AppT ty tys,- if b then FieldRO (ConE 'Rec) (VarE 'unRec)- else FieldRO (ConE 'Dep) (VarE 'unDep))- where tyn = if b then ''Rec else ''Dep+ (nRecTy, nRecCtor) = case length parNs of+ 0 -> (''T0, 'T0)+ 1 -> (''T1, 'T1)+ 2 -> (''T2, 'T2) w ty tys = case ty of- AppT{} -> Int.thFail $ "impossible: AppT is guarded by peelApp."- SigT ty _ -> uncurry w $ peelAppAcc tys ty- ForallT{} -> Int.thFail $ "no support for ForallT."- ConT n | isRec n -> do- rhs <- expandSyn ty tys- case rhs of+ PromotedT{} -> Int.thFail $ "no support for promoted types."+ PromotedTupleT{} -> Int.thFail $ "no support for promoted types."+ PromotedNilT{} -> Int.thFail $ "no support for promoted types."+ PromotedConsT{} -> Int.thFail $ "no support for promoted types."+ StarT{} -> Int.thFail $ "no support for kinds."+ ConstraintT{} -> Int.thFail $ "no support for constraint kinds."+ LitT{} -> Int.thFail $ "no support for type literals."+ AppT{} -> Int.thFail $ "impossible: AppT is guarded by peelApp."+ ForallT{} -> Int.thFail $ "no support for ForallT."+ UnboxedTupleT{} -> Int.thFail $ "no support for unboxed tuples."++ SigT ty _ -> uncurry w $ peelAppAcc tys ty++ VarT n | Just k <- List.findIndex (== n) $ reverse parNs ->+ if null tys then return $+ let (tyn, ctor, dtor) = case k of+ 0 -> (''Par0, 'Par0, 'unPar0)+ 1 -> (''Par1, 'Par1, 'unPar1)+ in (ConT tyn, FieldRO (ConE ctor) (VarE dtor))+ else Int.thFail $ "no support for poly- or higher-kinded parameters."++ ConT n | Just lbl <- case bg of Left _ -> Nothing; Right bg -> Map.lookup n bg -> case lbl of+ Nothing -> expandSyn ty tys >>= \case Just (ty, tys) -> w ty tys- Nothing ->- if not (null recs) then Int.thFail "no support for nested recursion."- else simple True ty tys- _- | not (null recs) -> case lookup (length recs) maps of- Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length recs) ++ " arguments."- Just (Mapping {containerTypeName = tyn, containerCtor = ctor,- methodName = mn}) -> do- recs <- mapM w' recs- let snoc (tyL, fROL) (tyR, fROR) =- (tyL `AppT` tyR, fROL `appRO` fROR)- appRO l r = FieldRO {repF = repF l `AppE` repF r `AppE` objF r,- objF = objF l `AppE` objF r `AppE` repF r}- post fRO = FieldRO {repF = ConE ctor `compose` repF fRO,- objF = objF fRO `compose` dtor}- return $ Arrow.second post $ foldl snoc- (ConT tyn `AppT` container,- FieldRO {repF = VarE mn, objF = VarE mn}) recs- where dtor = LamE [ConP ctor [VarP x]] (VarE x)- where x = mkName "x"- | otherwise -> simple False ty tys- where (foldl AppT ty -> container, recs) =- List.break (any isRec . Set.toList . SCCs.type_dependencies) tys+ Nothing -> Int.thFail "impossible: expandSyn is guarded by yoko0."+ Just lbl -> appliedRec lbl container tys'+ where (foldl AppT ty -> container, tys') =+ List.splitAt (length tys - length parNs) tys + -- NB cannot be recursive ... TODO unless we're operating on []+ _ -> appliedDep container importants+ where (foldl AppT ty -> container, importants) =+ List.break (any isImportant . Set.toList . namesIn) tys++ appliedRec lbl container tys = case null tys of+ True -> return (ConT ''T0 `AppT` (PromotedT 'Rec `AppT` toNat lbl) `AppT` container, FieldRO (ConE 'T0) (VarE 'unT0))+ False -> case lookup (length tys) maps of+ Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length tys) ++ " arguments."+ Just (Mapping {methodName = mn}) -> appliedType (ConT nRecTy `AppT` (PromotedT 'Rec `AppT` toNat lbl), nRecCtor, mn) container tys++ appliedDep container tys = case null tys of+ True -> return (ConT ''T0 `AppT` PromotedT 'Dep `AppT` container, FieldRO (ConE 'T0) (VarE 'unT0))+ False -> case lookup (length tys) maps of+ Nothing -> Int.thFail $ "no case in the given YokoOptions for type constructors with " ++ show (length tys) ++ " arguments."+ Just (Mapping {containerTypeName = tyn, containerCtor = ctor, methodName = mn}) ->+ appliedType (ConT tyn `AppT` PromotedT 'Dep, ctor, mn) container tys++ appliedType (rTy, nCtor, nMap) ty tys = do+ tys <- mapM w' tys+ let snoc (tyL, fROL) (tyR, fROR) = (tyL `AppT` tyR, fROL `appRO` fROR)+ appRO l r = FieldRO {repF = repF l `AppE` repF r `AppE` objF r,+ objF = objF l `AppE` objF r `AppE` repF r}+ post fRO = FieldRO {repF = ConE nCtor `compose` repF fRO,+ objF = objF fRO `compose` dtor}+ where dtor = let x = mkName "x" in LamE [ConP nCtor [VarP x]] (VarE x)+ return $ Arrow.second post $ foldl snoc+ (rTy `AppT` ty,+ FieldRO {repF = VarE nMap, objF = VarE nMap}) tys+ data ConRO = ConRO {repP :: [Pat], repE :: Exp, objP :: Pat, objE :: [Exp]} yoko1 r@(convert -> X :&- Renamer := rn :&- Mappings := maps :&- BindingGroup := bg :&- TargetData := Int.DataType tvbs cons :&- TargetType := ty :&- TargetKind := (ks, cxt)+ Target := tyn :&+ Renamer := rn :&+ Mappings := maps :&+ TargetData := Int.DataType tvbs cons :&+ DCInsts := dcInsts ) = do- loc <- liftQ TH.location+ let activated = dcInsts $ either ((:[]) . conName) (map conName) cons -- make a name into a NameG for a type in the current module; NB the fields -- types need not be declared in the same module as the target type+ loc <- liftQ TH.location let mkG n = Name (mkOccName $ nameBase n) $ NameG TcClsName (mkPkgName $ loc_package loc) (mkModName $ loc_module loc) - liftQ (sequence [do+ -- extract the ctors' fields and declare the fields types+ nAndFieldss <- flip mapM (either (:[]) id cons) $ \con -> do let n = conName con n' = rn n- fd = applyConT2TVBs n' tvbs+ generate [Int.dataType2Dec n' $ Int.DataType tvbs $ Right [renameCon rn con]]+ (>>= generate) $ liftQ $ serializeTypeAsHash_data (mkG n')+ fmap ((,) n) $ liftQ $ conFields con - fields <- conFields con+ let tvbSplits = [ List.splitAt k tvbs+ | k <- [length (drop 2 tvbs)..length tvbs] ]+ -- eg tvbs = [a,b,c]: [ ([a,b,c], []), ([a,b], [c]), ([a], [b,c]) ]+ -- eg tvbs = [a,b]: [ ([a,b] , []), ([a] , [b]), ([] , [a,b]) ]+ -- eg tvbs = [a]: [ ([a] , []), ([] , [a]) ]+ -- eg tvbs = []: [ ([] , []) ] - -- declare the fields type and its Codomain/Tag/DC instances- let yokoD = - [Int.dataType2Dec n' (Int.DataType tvbs (Right [renameCon rn con])),- TySynInstD ''Codomain [fd] ty,- TySynInstD ''Tag [fd] $ encode $ TH.nameBase n,- InstanceD cxt (ConT ''DC `AppT` fd)- [let (pat, exp) = pat_exp n' n $ length fields- in FunD 'rejoin [simpleClause [pat] exp]]- ]+ (>>= generate) $ liftQ $ spineType_d_ tyn $ map tvbKind tvbs+ (>>= generate) $ liftQ $ serializeTypeAsHash_data tyn - -- declare the Rep and Generic instances- (repTy, (conRO, _)) <- Arrow.second ($ 0) `fmap` halves fields- (return (ConT ''U, \s ->- (ConRO {repP = [], repE = ConE 'U,- objP = WildP, objE = []}, s)))- (\l r -> l >>= \(tyL, roL) -> r >>= \(tyR, roR) -> return $- (ConT ''(:*:) `AppT` tyL `AppT` tyR,- \s -> case roL s of- (roL, s) -> case roR s of- (roR, s) ->- (ConRO {repP = repP roL ++ repP roR,- repE = ConE '(:*:) `AppE` repE roL `AppE` repE roR,- objP = ConP '(:*:) [objP roL, objP roR],- objE = objE roL ++ objE roR}, s)))- (\(_, ty) ->- let post fRO s =- (ConRO {repP = [VarP n], repE = repF fRO `AppE` VarE n,- objP = VarP n, objE = [objF fRO `AppE` VarE n]},- s + 1)- where n = mkName $ "x" ++ show s- in Arrow.second post `fmap` fieldRO maps bg ty)+ flip mapM_ tvbSplits $ \(tvbs, pars) ->+ (flip mapM (either (:[]) id cons) $ \con -> do+ let n = conName con+ n' = rn n+ ((>>= generate) $ liftQ $ spineType_d_ (mkG n') $ map tvbKind tvbs)) >> - let genD = [TySynInstD ''Rep [fd] repTy,- InstanceD cxt (ConT ''Generic `AppT` fd)- [FunD 'rep [simpleClause [ConP n' (repP conRO)] $ repE conRO],- FunD 'obj [simpleClause [objP conRO] $- foldl AppE (ConE n') $ objE conRO]]]+ case filter ((/= StarT) . tvbKind) pars of+ offenders@(_:_) -> liftQ $ Int.thWarn $ "not representing " ++ nameBase tyn ++ " with " ++ msg (length pars) ++ " because [" ++ List.intercalate "," (map (nameBase . tvbName) offenders) ++ "] involves poly- or higher-kinds."+ where msg 1 = "1 parameter"+ msg n = show n ++ " parameters"+ [] -> do+ -- the pervasive context of the reflective Compare constraints+ cxt <- liftQ $ flip mapM tvbs $ \tvb ->+ EqualP (PromotedT 'EQ) `fmap` do+ let tv = [t| Spine $(return $ tvbType tvb) |]+ [t| Ord.Compare $tv $tv |] - -- integrate with type-spine and type-cereal- spineD <- spineType_d_ (mkG n') ks- cerealD <- serializeTypeAsHash_data (mkG n')+ -- for every fields type, generate the fields types instances+ flip mapM_ nAndFieldss $ \(n, fields) -> do+ yoko2 (n `elem` activated) $ r :&+ TargetTVBs := tvbs :&+ TargetPars := pars :&+ TargetType := applyConT2TVBs tyn tvbs :&+ TargetCxt := cxt :&+ ConName := n :&+ ConFields := fields - return $ yokoD ++ spineD ++ cerealD ++ genD- | con <- either (:[]) id cons ]) >>= generate . concat+ -- generate the DCs, DTs, DT instances+ yoko3 $ r :&+ TargetTVBs := tvbs :&+ TargetPars := pars :&+ TargetType := applyConT2TVBs tyn tvbs :&+ TargetCxt := cxt - yoko2 r --- generate DCs/DT instances-compose l r = VarE '(.) `AppE` l `AppE` r+yoko2 activated (convert -> X :&+ Renamer := rn :&+ Mappings := maps :&+ BindingGroup := bg :&+ TargetType := ty :&+ TargetPars := pars :&+ TargetTVBs := tvbs :&+ TargetCxt := cxt :&+ ConName := n :&+ ConFields := fields+ ) = do+ let nW_rejoin = case length pars of+ 0 -> 'Sym0+ 1 -> 'Sym1+ 2 -> 'Sym2 -postConE :: Name -> Exp -> Exp-postConE n inj = compose (ConE n) inj+ let (nW_rep, nW_obj) = case length pars of+ 0 -> ('W0, 'w0')+ 1 -> ('W1, 'w1')+ 2 -> ('W2, 'w2') -yoko2 r@(convert -> X :&- Renamer := rn :&- TargetData := Int.DataType tvbs cons :&- TargetType := ty :&- TargetKind := (_, cxt)+ let n' = rn n ; fd = applyConT2TVBs n' tvbs++ -- declare the fields type's Codomain/Tag/DC instances+ generate+ [TySynInstD ''Codomain [fd] ty,+ TySynInstD ''Tag [fd] $ encode $ TH.nameBase n,+ InstanceD cxt (ConT ''DC `AppT` fd)+ [let (pat, exp) = pat_exp n' n $ length fields+ in simpleVal 'rejoin $ ConE nW_rejoin `AppE` LamE [pat] exp]+ ]++ -- declare the Rep and Generic RHSs+ when activated $ (>>= generate) $ do+ (repTy, (conRO, _)) <- liftQ $ Arrow.second ($ 0) `fmap` halves fields+ (return (ConT ''U, \s ->+ (ConRO {repP = [], repE = ConE 'U,+ objP = WildP, objE = []}, s)))++ (\l r -> l >>= \(tyL, roL) -> r >>= \(tyR, roR) -> return $+ (ConT ''(:*:) `AppT` tyL `AppT` tyR,+ \s -> case roL s of+ (roL, s) -> case roR s of+ (roR, s) ->+ (ConRO {repP = repP roL ++ repP roR,+ repE = ConE '(:*:) `AppE` repE roL `AppE` repE roR,+ objP = ConP '(:*:) [objP roL, objP roR],+ objE = objE roL ++ objE roR}, s)))++ (\(_, ty) ->+ let post fRO s =+ (ConRO {repP = [VarP n], repE = repF fRO `AppE` VarE n,+ objP = VarP n, objE = [objF fRO `AppE` VarE n]},+ s + 1)+ where n = mkName $ "x" ++ show s+ in Arrow.second post `fmap`+ fieldRO maps bg (map tvbName pars) ty)++ return+ [ TySynInstD ''Rep [fd] (ConT ''C `AppT` fd `AppT` repTy),+ InstanceD cxt (ConT ''Generic `AppT` fd)+ [simpleVal 'rep $ (ConE nW_rep `AppE`) $ LamE [ConP n' (repP conRO)] $ ConE 'C `AppE` repE conRO,+ simpleVal 'obj $ (VarE nW_obj `AppE`) $ LamE [ConP 'C [objP conRO]] $ foldl AppE (ConE n') $ objE conRO]]++-- generate DCs/DT instances+yoko3 r@(convert -> X :&+ Target := tyn :&+ Renamer := rn :&+ InvInsts := invInsts :&+ TargetData := Int.DataType _ cons :&+ BindingGroup := bg :&+ TargetType := ty :&+ TargetPars := pars :&+ TargetTVBs := tvbs :&+ TargetCxt := cxt ) = do+ let (nW_disband, nNCtor) = case length pars of+ 0 -> ('W0, 'N0)+ 1 -> ('W1, 'N1)+ 2 -> ('W2, 'N2)++ let invInst = case length pars of+ 0 -> Nothing+ 1 -> Just (''Invariant, 'invmap, 'gen_invmap)+ 2 -> Just (''Invariant2, 'invmap2, 'gen_invmap2)+ (dcs, cases) <- liftQ $ halves (either (:[]) id cons) (Int.thFail $ "`" ++ show (r !!! Target :: Name) ++ "' must have constructors.") (\l r -> do@@ -369,10 +528,28 @@ fields <- length `fmap` conFields con return $ let n = conName con in (ConT ''N `AppT` applyConT2TVBs (rn n) tvbs,- [(ConE 'N, (n, fields))]))+ [(ConE nNCtor, (n, fields))])) - cases <- return $ flip map cases $ \(inj, (n, fds)) ->+ matches <- return $ flip map cases $ \(inj, (n, fds)) -> let (pat, exp) = pat_exp n (rn n) fds- in simpleClause [pat] $ inj `AppE` exp+ in Match pat (NormalB $ inj `AppE` exp) [] generate $ [TySynInstD ''DCs [ty] dcs,- InstanceD cxt (ConT ''DT `AppT` ty) [FunD 'disband cases]]+ InstanceD cxt (ConT ''DT `AppT` ty)+ [simpleVal 'disband $ (ConE nW_disband `AppE`) $ LamCaseE matches]]++ when invInsts $ flip (maybe (return ())) invInst $ \(cls, method, rhs) ->+ generate [InstanceD cxt (ConT cls `AppT` ty) [ValD (VarP method) (NormalB (VarE rhs)) []]]++ (>>= generate) $ do+ rhs <- case fmap (Set.toAscList . Map.keysSet) bg of+ Left _ -> return $ PromotedT 'NonRecDT+ Right ns -> do+ -- filter out the type synonyms+ ns <- fmap catMaybes $ flip mapM ns $ \n -> liftQ (reify n) >>= \case+ TyConI TySynD{} -> return Nothing+ _ -> return $ Just n+ let (l, _:r) = List.break (== tyn) ns+ promo = foldr cons PromotedNilT where+ cons n sofar = PromotedConsT `AppT` foldl AppT (ConT n) (map (VarT . tvbName) tvbs) `AppT` sofar+ return $ PromotedT 'RecDT `AppT` promo l `AppT` promo r+ return [TySynInstD ''DTs [ty] rhs]
Data/Yoko/TH/Internal.hs view
@@ -27,7 +27,11 @@ thFail s = fail $ "yokoTH: " ++ s +thWarn :: String -> Q ()+thWarn s = reportWarning $ "yokoTH: " ++ s ++ data DataType = DataType [TyVarBndr] (Either Con [Con]) @@ -35,10 +39,13 @@ dataType :: Name -> Q DataType dataType n = do i <- reify n+ let refine = map $ \tvb -> case tvb of+ PlainTV n -> KindedTV n StarT+ _ -> tvb case i of TyConI d -> case d of- DataD _ _ tvbs cons _ -> return $ DataType tvbs $ Right cons- NewtypeD _ _ tvbs con _ -> return $ DataType tvbs $ Left con+ DataD _ _ tvbs cons _ -> return $ DataType (refine tvbs) $ Right cons+ NewtypeD _ _ tvbs con _ -> return $ DataType (refine tvbs) $ Left con _ -> thFail $ "expecting name of newtype or data type, not: " ++ show d _ -> thFail $ "expecting name of newtype or data type, not: " ++ show i
Data/Yoko/TypeBasics.hs view
@@ -1,4 +1,6 @@-{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds #-}+{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds, GADTs,+ FlexibleInstances, TypeOperators, Rank2Types, ScopedTypeVariables,+ InstanceSigs, ConstraintKinds, MultiParamTypeClasses #-} {- | @@ -16,10 +18,24 @@ module Data.Yoko.TypeBasics ( Proxy(..), Equal, derive_data, derive_pro,+ Nat(..), SingNat(..),+ Length, Length', Append,+ App, Constant(..),+ Vec(..), vCarrying,+ VFunctor(..), TrivCon, trivCon,+ VInitialize(..),+ CVec(..), cvec2list,+ VRepeat(..), Diag_(..), VZip(..), cvZipWith,+ Idx(..), IndexInto(..), cvAt, cvUpd, VEnum(..), cvAddIndexes, -- ** Re-exports- module Data.Yoko.MaybeKind, encode+ module Data.Yoko.MaybeKind, encode, SpineCompare ) where +import Data.Monoid+import qualified Data.Foldable as F+import qualified Data.Traversable as T+import qualified Control.Applicative as I+ import Data.Yoko.MaybeKind import Type.Spine@@ -49,3 +65,172 @@ derive_pro n = do d <- spineType_pro n (d ++) `fmap` serializeTypeAsHash_pro n++++-- naturals+data Nat = Z | S Nat++data SingNat :: Nat -> * where+ SZ :: SingNat 'Z+ SN :: SingNat n -> SingNat ('S n)++-- lists+type family Append (x :: [k]) (y :: [k]) :: [k]+type instance Append '[] y = y+type instance Append (t ': ts) y = t ': Append ts y+++type Length list = Length' Z list++type family Length' (acc :: Nat) (list :: [k]) :: Nat+type instance Length' acc '[] = acc+type instance Length' acc (t ': list) = Length' (S acc) list++-- indexed vectors+type family App (fn :: k -> *) (t :: k) :: *++newtype Constant a (t :: k) = Constant a+type instance App (Constant a) k = a++data Vec :: [k] -> (k -> *) -> * where+ VNil :: Vec '[] f+ VCons :: App f t -> Vec ts f -> Vec (t ': ts) f++instance Eq (Vec '[] f) where _ == _ = True+instance (Eq (App f t), Eq (Vec ts f)) => Eq (Vec (t ': ts) f) where+ VCons a as == VCons b bs = a == b && as == bs++instance Ord (Vec '[] f) where compare _ _ = EQ+instance (Ord (App f t), Ord (Vec ts f)) => Ord (Vec (t ': ts) f) where+ VCons a as `compare` VCons b bs = compare (a, as) (b, bs)++vCarrying :: Proxy f -> Vec ts f -> Vec ts f+vCarrying _ = id++class VFunctor c ts where+ vMap :: Proxy c -> (forall t. c t => Proxy t -> App f t -> App g t) -> Vec ts f -> Vec ts g++instance VFunctor c '[] where+ vMap _ _ VNil = VNil+instance (c t, VFunctor c ts) => VFunctor c (t ': ts) where+ vMap c f (VCons x xs) = VCons (f (Proxy :: Proxy t) x) $ vMap c f xs++class TrivCon a; instance TrivCon a+trivCon :: Proxy TrivCon+trivCon = Proxy++instance Monoid (Vec '[] f) where+ mempty = VNil; mappend _ _ = VNil+instance (Monoid (App f t), Monoid (Vec ts f)) => Monoid (Vec (t ': ts) f) where+ mempty = VCons mempty mempty+ VCons x xs `mappend` VCons y ys = mappend x y `VCons` mappend xs ys++++newtype CVec ts a = CVec {unCVec :: Vec ts (Constant a)}++instance Eq (Vec ts (Constant a)) => Eq (CVec ts a) where CVec x == CVec y = x == y+instance Ord (Vec ts (Constant a)) => Ord (CVec ts a) where CVec x `compare` CVec y = compare x y++instance Monoid (Vec ts (Constant a)) => Monoid (CVec ts a) where+ mempty = CVec mempty+ CVec x `mappend` CVec y = CVec $ mappend x y++instance Functor (CVec ts) where fmap = T.fmapDefault+instance F.Foldable (CVec ts) where foldMap = T.foldMapDefault++instance T.Traversable (CVec ts) where+ traverse :: forall a i b. I.Applicative i => (a -> i b) -> CVec ts a -> i (CVec ts b)+ traverse f (CVec v) = CVec I.<$> w v where+ w :: forall ts. Vec ts (Constant a) -> i (Vec ts (Constant b))+ w x = case x of+ VNil -> I.pure VNil+ VCons a as -> VCons I.<$> f a I.<*> w as++cvec2list :: CVec ts a -> [a]+cvec2list = F.toList++class VRepeat ts where cvRepeat :: a -> CVec ts a++instance VRepeat '[] where cvRepeat _ = CVec VNil+instance VRepeat ts => VRepeat (t ': ts) where+ cvRepeat a = CVec $ VCons a $ unCVec $ cvRepeat a++data Diag_ (f :: k -> *) (g :: k -> *) (t :: k) = Diag_+type instance App (Diag_ f g) t = (App f t, App g t)++class VZip ts where vZip :: Vec ts f -> Vec ts g -> Vec ts (Diag_ f g)++instance VZip '[] where vZip _ _ = VNil+instance VZip ts => VZip (t ': ts) where+ vZip (VCons a as) (VCons b bs) = VCons (a, b) $ vZip as bs++cvZipWith :: forall a b c ts. (a -> b -> c) -> CVec ts a -> CVec ts b -> CVec ts c+cvZipWith f (CVec x) (CVec y) = CVec $ w x y where+ w :: forall ts. Vec ts (Constant a) -> Vec ts (Constant b) -> Vec ts (Constant c)+ w VNil VNil = VNil+ w (VCons a as) (VCons b bs) = VCons (f a b) $ w as bs++data Idx :: [k] -> * where+ ZIdx :: Idx (t ': ts)+ SIdx :: Idx ts -> Idx (t ': ts)+type instance App Idx ts = Idx ts++class IndexInto (n :: Nat) (ts :: [k]) where+ indexInto :: Proxy n -> Proxy ts -> Idx ts++instance IndexInto Z (t ': ts) where indexInto _ _ = ZIdx+instance IndexInto n ts => IndexInto (S n) (t ': ts) where+ indexInto _ _ = SIdx $ indexInto (Proxy :: Proxy n) (Proxy :: Proxy ts)++instance Show (Idx ts) where+ showsPrec _ ZIdx = showString "ZIdx"+ showsPrec p (SIdx x) = showParen (p > 10) $+ showString "SIdx" . showChar ' ' . showsPrec 11 x++instance Eq (Idx ts) where+ ZIdx == ZIdx = True+ SIdx a == SIdx b = a == b+ _ == _ = False++instance Ord (Idx ts) where+ ZIdx `compare` ZIdx = EQ+ ZIdx `compare` _ = LT+ SIdx _ `compare` ZIdx = GT+ SIdx a `compare` SIdx b = compare a b++cvAt :: forall ts a. CVec ts a -> Idx ts -> a+cvAt (CVec v) = flip w v where+ w :: forall ts. Idx ts -> Vec ts (Constant a) -> a+ w ZIdx (VCons a _ ) = a+ w (SIdx idx) (VCons _ as) = w idx as++cvUpd :: forall ts a. CVec ts a -> Idx ts -> (a -> a) -> CVec ts a+cvUpd (CVec v) idx f = CVec $ w idx v where+ w :: forall ts. Idx ts -> Vec ts (Constant a) -> Vec ts (Constant a)+ w ZIdx (VCons a as) = VCons (f a) as+ w (SIdx idx) (VCons a as) = VCons a $ w idx as++class VEnum ts where cvEnum :: CVec ts (Idx ts)+instance VEnum '[] where cvEnum = CVec VNil+instance VEnum ts => VEnum (t ': ts) where+ cvEnum = CVec $ VCons ZIdx $ unCVec $ fmap SIdx cvEnum++cvAddIndexes :: VEnum ts => CVec ts a -> CVec ts (Idx ts, a)+cvAddIndexes = cvZipWith (,) cvEnum++++type instance App Proxy t = Proxy t++class VInitialize c ts where+ vInitialize :: Proxy c -> Proxy f -> (forall t. c t => Proxy t -> App f t) -> Vec ts f+ cvInitialize :: Proxy c -> (forall t. c t => Proxy t -> a) -> CVec ts a+instance VInitialize c '[] where+ vInitialize _ _ _ = VNil+ cvInitialize _ _ = CVec VNil+instance (c t, VInitialize c ts) => VInitialize c (t ': ts) where+ vInitialize pc pf x = VCons (x (Proxy :: Proxy t)) (vInitialize pc pf x)+ cvInitialize pc x = CVec $+ VCons (x (Proxy :: Proxy t)) (unCVec $ cvInitialize pc x)
Data/Yoko/TypeSums.hs view
@@ -1,5 +1,4 @@-{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators,- NoPolyKinds, DataKinds #-}+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators, PolyKinds, DataKinds #-} {-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances, ScopedTypeVariables, EmptyDataDecls #-}@@ -21,8 +20,8 @@ -} module Data.Yoko.TypeSums (DistMaybePlus, (:-:),- Embed, embed, inject,- Partition, project, partition) where+ Embed, embed, inject0, inject1, inject2,+ Partition, project0, project1, project2, partition) where import Data.Yoko.TypeBasics import Data.Yoko.Representation@@ -34,39 +33,49 @@ -class Embed sub sup where embed_ :: sub -> sup+class Embed sub sup where embed_ :: sub (p1 :: *) (p0 :: *) -> sup p1 p0 -embed :: Embed sub sup => sub -> sup+embed :: Embed sub sup => sub p1 p0 -> sup p1 p0 embed = embed_ -inject :: Embed (N a) sum => a -> sum-inject = embed . N+inject0 :: Embed (N a) sum => a -> sum p1 p0+inject0 = embed . N0 +inject1 :: Embed (N a) sum => a p0 -> sum p1 p0+inject1 = embed . N1 +inject2 :: Embed (N a) sum => a p1 p0 -> sum p1 p0+inject2 = embed . N2 -class Partition sup subL subR where partition_ :: sup -> Either subL subR ++class Partition sup subL subR where partition_ :: sup (p1 :: *) (p0 :: *) -> Either (subL p1 p0) (subR p1 p0)+ partition :: Partition sup sub (sup :-: sub) =>- sup -> Either sub (sup :-: sub)+ sup p1 p0 -> Either (sub p1 p0) ((sup :-: sub) p1 p0) partition = partition_ -project :: Partition sum (N a) (sum :-: N a) => sum -> Either a (sum :-: N a)-project = left unN . partition_+project0 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either a ((sum :-: N a) p1 p0)+project0 = left unN0 . partition_ +project1 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either (a p0) ((sum :-: N a) p1 p0)+project1 = left unN1 . partition_ +project2 :: Partition sum (N a) (sum :-: N a) => sum p1 p0 -> Either (a p1 p0) ((sum :-: N a) p1 p0)+project2 = left unN2 . partition_ -data Here a-data TurnLeft path-data TurnRight path -type family Locate a sum :: Maybe *-type instance Locate a (N x) = If (Equal x a) (Just (Here a)) Nothing++data Path k = Here k | TurnLeft (Path k) | TurnRight (Path k)++type family Locate (a :: k) (sum :: * -> * -> *) :: Maybe (Path k)+type instance Locate a (N x) = If (Equal x a) (Just (Here a)) Nothing type instance Locate a (l :+: r) = MaybeMap TurnLeft (Locate a l) `MaybePlus1` MaybeMap TurnRight (Locate a r)-type instance Locate a Void = Nothing+type instance Locate a Void = Nothing type Elem a sum = IsJust (Locate a sum) @@ -74,8 +83,8 @@ -class InjectAt path a sum where injectAt :: Proxy path -> a -> sum-instance InjectAt (Here a) a (N a) where injectAt _ = N+class InjectAt path n sum where injectAt :: Proxy path -> n (p1 :: *) (p0 :: *) -> sum p1 p0+instance InjectAt (Here a) (N a) (N a) where injectAt _ = id instance InjectAt path a l => InjectAt (TurnLeft path) a (l :+: r) where injectAt _ = L . injectAt (Proxy :: Proxy path) instance InjectAt path a r => InjectAt (TurnRight path) a (l :+: r) where@@ -85,8 +94,8 @@ -instance (Locate x sup ~ Just path, InjectAt path x sup) => Embed (N x) sup where- embed_ = injectAt (Proxy :: Proxy path) . unN+instance (Locate x sup ~ Just path, InjectAt path (N x) sup) => Embed (N x) sup where+ embed_ = injectAt (Proxy :: Proxy path) instance (Embed l sup, Embed r sup) => Embed (l :+: r) sup where embed_ = foldPlus embed embed @@ -95,12 +104,12 @@ infixl 6 :-:-type family (:-:) sum sum2-type instance (:-:) (N x) sum2 = If (Elem x sum2) Void (N x)+type family (:-:) (sum :: * -> * -> *) (sum2 :: * -> * -> *) :: * -> * -> *+type instance (:-:) (N x) sum2 = If (Elem x sum2) Void (N x) type instance (:-:) (l :+: r) sum2 = Combine (l :-: sum2) (r :-: sum2) -type family Combine sum sum2+type family Combine (sum :: * -> * -> *) (sum2 :: * -> * -> *) :: * -> * -> * type instance Combine Void x = x type instance Combine (N x) Void = N x type instance Combine (N x) (N y) = N x :+: N y@@ -112,9 +121,9 @@ class Partition_N (bn :: Bool) x subL subR where- partition_N :: Proxy bn -> N x -> Either subL subR+ partition_N :: Proxy bn -> x (p1 :: *) (p0 :: *) -> Either (subL p1 p0) (subR p1 p0) -instance (Partition_N (Elem x subL) x subL subR+instance (Partition_N (Elem x subL) (N x) subL subR ) => Partition (N x) subL subR where partition_ = partition_N (Proxy :: Proxy (Elem x subL)) @@ -124,7 +133,7 @@ -instance Embed (N x) subR => Partition_N False x subL subR where+instance Embed x subR => Partition_N False x subL subR where partition_N _ = Right . embed-instance Embed (N x) subL => Partition_N True x subL subR where+instance Embed x subL => Partition_N True x subL subR where partition_N _ = Left . embed
Data/Yoko/View.hs view
@@ -1,5 +1,6 @@ {-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,- MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds #-}+ MultiParamTypeClasses, FlexibleInstances, UndecidableInstances, DataKinds,+ PolyKinds, GADTs #-} {- | @@ -16,42 +17,124 @@ -} module Data.Yoko.View- (-- * Reflection+{- (-- * Reflection -- ** Fields types- Tag, Codomain, DC(..),+ Tag, Codomain0, Codi, DC(..),+ -- ** Substitution+ Subst, Subst0, Subst1, -- ** Disbanded data types DCs, DT(..)- ) where+ ) -} where +import Data.Yoko.W+import Data.Yoko.TypeBasics import Data.Yoko.Representation-import Data.Yoko.TypeSums (Embed, Partition, (:-:))-import Data.Yoko.Each+--import Data.Yoko.TypeSums (Embed, Partition, (:-:))+--import Data.Yoko.Each import Type.Digits (Digit) ++ -- | @Tag@ returns a simulated type-level string that is the name of the -- constructor that the @dc@ fields type represents.-type family Tag dc :: Digit+type family Tag (dc :: k) :: Digit -- | @Codomain@ is the data type that contains the constructor that the fields -- type @dc@ represents. It can also be applied to sums of fields types, in -- which case it just uses the left-most.-type family Codomain dc-type instance Codomain (N dc) = Codomain dc-type instance Codomain (l :+: r) = Codomain l+type family Codomain (dc :: k) :: k +type family Codomain0 (dcs :: * -> * -> *) :: *+type family Codomain1 (dcs :: * -> * -> *) :: * -> *+type family Codomain2 (dcs :: * -> * -> *) :: * -> * -> *+type instance Codomain0 (N dc) = Codomain dc+type instance Codomain1 (N dc) = Codomain dc+type instance Codomain2 (N dc) = Codomain dc+type instance Codomain0 (l :+: r) = Codomain0 l+type instance Codomain1 (l :+: r) = Codomain1 l+type instance Codomain2 (l :+: r) = Codomain2 l++++data DTPos k = NonRecDT | RecDT [k] [k]++-- | Maps a type to its mutually recursive siblings.+type family DTs (t :: k) :: DTPos k+++type NumDTs t = NumDTs' (DTs t)+type family NumDTs' (t :: DTPos k) :: Nat+type instance NumDTs' NonRecDT = Z+type instance NumDTs' (RecDT l r) = S (Length' (Length r) l)++type SiblingDTs t = SiblingDTs' t (DTs t)+type family SiblingDTs' (t :: k) (dpos :: DTPos k) :: [k]+type instance SiblingDTs' t NonRecDT = '[]+type instance SiblingDTs' t (RecDT l r) = Append l (t ': r)+++ -- | Any fields type can be further represented as a product-of-fields and can -- be injected back into the original data type.-class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: dc -> Codomain dc+class (Generic dc, DT (Codomain dc)) => DC dc where rejoin :: Sym dc (Codomain dc) p1 p0 -- | The @DCs@ of a data type is sum of all of its fields types.-type family DCs t--- | @DT@ disbands a data type if all of its fields types have @DC@ instances.-class Each IsDCOf (DCs t) => DT t where disband :: t -> DCs t+type family DCs (t :: k) :: * -> * -> *+-- | @DT@ disbands a data type.@+class DT t where disband :: W t (DCs t) p1 p0 -class (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),- Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc-instance (Partition (DCs (Codomain dc)) (N dc) (DCs (Codomain dc) :-: N dc),- Embed (N dc) (DCs (Codomain dc))) => IsDCOf dc+++-- take a representation, C or above and excluding Recs/Pars, to an actual *+-- type+type family Eval (r :: * -> * -> *) :: *+type instance Eval (T0 Dep t) = t+--type instance Eval Void = ???+type instance Eval (l :+: r) = Eval l -- equivalently, Eval r+type instance Eval (C (dc :: *) r) = Codomain dc+type instance Eval (N dc) = Codomain dc++++data SubstSpec star = Sub0 star | Sub1 star | Sub10 star star++++type family Subst (spec :: SubstSpec *) (r :: * -> * -> *) :: * -> * -> *+--type instance Subst spec Void = ???+type instance Subst spec (N dc) = N dc+type instance Subst spec (l :+: r) = Subst spec l :+: Subst spec r++type instance Subst spec (C dc r) = C dc (Subst spec r)+type instance Subst spec U = U+type instance Subst spec (l :*: r) = Subst spec l :*: Subst spec r++type instance Subst (Sub0 par0 ) Par0 = T0 Dep par0+type instance Subst (Sub1 par1 ) Par0 = Par0+type instance Subst (Sub10 par1 par0) Par0 = T0 Dep par0+type instance Subst (Sub1 par1 ) Par1 = T0 Dep par1+type instance Subst (Sub10 par1 par0) Par1 = T0 Dep par1++type instance Subst (Sub0 par0) (T1 (Rec lbl) t a) = T0 (Rec lbl) (t (Eval (Subst (Sub0 par0) a)))+--type instance Subst (Sub1 par1) (Rec0 lbl t) = undefined+--type instance Subst (Sub10 par1 par0) (Rec1 lbl t a) = undefined++--type instance Subst (Sub0 par0 (Rec2 lbl t b a) = undefined+type instance Subst (Sub1 par1) (T2 (Rec lbl) t b a) =+ T1 (Rec lbl) (t (Eval (Subst (Sub1 par1) b))) (Subst (Sub1 par1) a)+type instance Subst (Sub10 par1 par0) (T2 (Rec lbl) t b a) =+ T0 (Rec lbl) (t (Eval (Subst (Sub10 par1 par0) b)) (Eval (Subst (Sub10 par1 par0) a)))++type instance Subst spec (T0 Dep t) = T0 Dep t++type instance Subst spec (T1 Dep f x ) = T1 Dep f (Subst spec x)+type instance Subst spec (T2 Dep f x y) = T2 Dep f (Subst spec x) (Subst spec y)++++type Subst0 t p0 = Subst (Sub0 p0) (Rep t)+type Subst1 t p1 = Subst (Sub1 p1) (Rep t)+type Subst10 t p1 p0 = Subst (Sub10 p1 p0) (Rep t)
+ Data/Yoko/W.hs view
@@ -0,0 +1,67 @@+{-# LANGUAGE TypeFamilies, PolyKinds, RankNTypes, ConstraintKinds #-}++{-# LANGUAGE FlexibleInstances #-}++module Data.Yoko.W where++++data family W (t :: k) :: (* -> * -> *) -> * -> * -> *++newtype instance W (t :: *) s p1 p0 = W0 (t -> s p1 p0)+newtype instance W (t :: * -> *) s p1 p0 = W1 (t p0 -> s p1 p0)+newtype instance W (t :: * -> * -> *) s p1 p0 = W2 (t p1 p0 -> s p1 p0)++unW0 (W0 f) = f+unW1 (W1 f) = f+unW2 (W2 f) = f++data family W' (s :: k) :: (* -> * -> *) -> * -> * -> *++newtype instance W' (s :: *) t p1 p0 = W'0 (t p1 p0 -> s )+newtype instance W' (s :: * -> *) t p1 p0 = W'1 (t p1 p0 -> s p0)+newtype instance W' (s :: * -> * -> *) t p1 p0 = W'2 (t p1 p0 -> s p1 p0)++unW'0 (W'0 f) = f+unW'1 (W'1 f) = f+unW'2 (W'2 f) = f++data family Sym (t :: k) :: k -> * -> * -> *++newtype instance Sym (t :: *) s p1 p0 = Sym0 (t -> s )+newtype instance Sym (t :: * -> *) s p1 p0 = Sym1 (t p0 -> s p0)+newtype instance Sym (t :: * -> * -> *) s p1 p0 = Sym2 (t p1 p0 -> s p1 p0)++unSym0 (Sym0 f) = f+unSym1 (Sym1 f) = f+unSym2 (Sym2 f) = f+++class ComposeW (t :: k) where+ composeW :: (s p1 p0 -> s' p1 p0) -> W t s p1 p0 -> W t s' p1 p0+ composeW' :: W' t s' p1 p0 -> (s p1 p0 -> s' p1 p0) -> W' t s p1 p0+ sym :: W' t' s p1 p0 -> W t s p1 p0 -> Sym t t' p1 p0+ unSym :: W t s' p1 p0 -> W' t s p1 p0 -> s p1 p0 -> s' p1 p0+ composeSymW' :: Sym t t' p1 p0 -> W' t s p1 p0 -> W' t' s p1 p0+ composeWSym :: W t' s p1 p0 -> Sym t t' p1 p0 -> W t s p1 p0+instance ComposeW (t :: *) where+ composeW f (W0 g) = W0 (f . g)+ composeW' (W'0 f) g = W'0 (f . g)+ sym (W'0 f) (W0 g) = Sym0 (f . g)+ unSym (W0 f) (W'0 g) = f . g+ composeSymW' (Sym0 f) (W'0 g) = W'0 (f . g)+ composeWSym (W0 f) (Sym0 g) = W0 (f . g)+instance ComposeW (t :: * -> *) where+ composeW f (W1 g) = W1 (f . g)+ composeW' (W'1 f) g = W'1 (f . g)+ sym (W'1 f) (W1 g) = Sym1 (f . g)+ unSym (W1 f) (W'1 g) = f . g+ composeSymW' (Sym1 f) (W'1 g) = W'1 (f . g)+ composeWSym (W1 f) (Sym1 g) = W1 (f . g)+instance ComposeW (t :: * -> * -> *) where+ composeW f (W2 g) = W2 (f . g)+ composeW' (W'2 f) g = W'2 (f . g)+ sym (W'2 f) (W2 g) = Sym2 (f . g)+ unSym (W2 f) (W'2 g) = f . g+ composeSymW' (Sym2 f) (W'2 g) = W'2 (f . g)+ composeWSym (W2 f) (Sym2 g) = W2 (f . g)
Data/YokoRaw.hs view
@@ -1,6 +1,6 @@ {-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts, MultiParamTypeClasses, FlexibleInstances, ScopedTypeVariables,- UndecidableInstances #-}+ UndecidableInstances, PolyKinds #-} {- | @@ -20,39 +20,37 @@ module Data.YokoRaw (module Data.Yoko.Representation, module Data.Yoko.View,+ module Data.Yoko.TypeBasics,+ module Data.Yoko.W, -- * Building fields type consumers one, (|||), (||.), (.||), (.|.), -- * Operations on disbanded data types- disbanded, band, ConDCOf, precise_case,+ disbanded, AreDCsOf, band, precise_case0, -- * Operations on sums of fields types (:-:), Embed, Partition, embed, inject, partition, project, -- * Forgetting @yoko@'s extra structure- reps, EachGeneric, EachRep, ig_from,- Equal,- -- * Bundled Template Haskell- module Data.Yoko.TH) where+ reps, EachGeneric, EachRep, ig_from) where +import Data.Yoko.W import Data.Yoko.TypeBasics import Data.Yoko.Representation import Data.Yoko.View import Data.Yoko.TypeSums (Embed, Partition, (:-:)) import qualified Data.Yoko.TypeSums as TypeSums-import Data.Yoko.Each--import Data.Yoko.TH+--import Data.Yoko.Each -- | @one@ extends a function that consumes a fields type to a function that -- consumes a disbanded data type containing just that fields type.-one :: (dc -> a) -> N dc -> a-one = foldN+one :: (dc -> a) -> N dc p1 p0 -> a+one = foldN0 infixl 6 ||| -- | Combines two functions that consume disbanded data types into a function -- that consumes their union. All fields types must be from the same data type.-(|||) :: (Codomain sumL ~ Codomain sumR) => (sumL -> a) -> (sumR -> a) -> sumL :+: sumR -> a+(|||) :: (Codomain0 sumL ~ Codomain0 sumR) => (sumL p1 p0 -> a) -> (sumR p1 p0 -> a) -> (sumL :+: sumR) p1 p0 -> a (|||) = foldPlus infixl 9 .|.@@ -69,56 +67,54 @@ -- | @disbanded@ injects a fields type into its disbanded range-disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc)-disbanded = TypeSums.inject+disbanded :: Embed (N dc) (DCs (Codomain dc)) => dc -> DCs (Codomain dc) p1 p0+disbanded = TypeSums.inject0 -- | @band@s a disbanded data type back into its normal data type. ----- Since 'Disbanded' is a type family, the range of @band@ determines the @t@--- type variable.-band :: forall t. Each (ConDCOf t) (DCs t) => DCs t -> t-band = each (Proxy :: Proxy (ConDCOf t)) rejoin+-- Since 'DCs' is a type family, it's the range of @band@ that determines the+-- @t@ type variable.+class AreDCsOf (t :: k) (dcs :: * -> * -> *) where band_ :: W' t dcs p1 p0+instance (WN dc, Codomain dc ~ t, DC dc) => AreDCsOf t (N dc) where+ band_ = composeSymW' rejoin unN+instance (FoldPlusW' t, AreDCsOf t l, AreDCsOf t r) => AreDCsOf t (l :+: r) where band_ = foldPlusW' band_ band_ -class (Codomain dc ~ t, DC dc) => ConDCOf t dc-instance (Codomain dc ~ t, DC dc) => ConDCOf t dc+band :: (AreDCsOf (t :: k) (DCs t)) => W' t (DCs t) p1 p0+band = band_ -embed :: (Codomain sub ~ Codomain sup, Embed sub sup) => sub -> sup+embed :: (Codomain0 sub ~ Codomain0 sup, Embed sub sup) => sub p1 p0 -> sup p1 p0 embed = TypeSums.embed -- | @inject@s a fields type into a sum of fields types.-inject :: Embed (N dc) sum => dc -> sum-inject = TypeSums.inject+inject :: Embed (N dc) sum => dc -> sum p1 p0+inject = TypeSums.inject0 -- | @partition@s a sum of fields type into a specified sum of fields types and -- the remaining sum.-partition :: (Codomain sum ~ Codomain sub, Partition sum sub (sum :-: sub)) =>- sum -> Either sub (sum :-: sub)+partition :: (Codomain0 sum ~ Codomain0 sub, Partition sum sub (sum :-: sub)) =>+ sum p1 p0 -> Either (sub p1 p0) ((sum :-: sub) p1 p0) partition = TypeSums.partition -- | @project@s a single fields type out of a disbanded data type.-project :: (Codomain sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>- sum -> Either dc (sum :-: N dc)-project = TypeSums.project+project :: (Codomain0 sum ~ Codomain dc, Partition sum (N dc) (sum :-: N dc)) =>+ sum p1 p0 -> Either dc ((sum :-: N dc) p1 p0)+project = TypeSums.project0 -- TODO need a MapSum just like MapRs, use a RPV for rep -- | @reps@ maps a disbanded data type to its sum-of-products representation.-reps :: EachGeneric sum => sum -> EachRep sum+reps :: EachGeneric sum => sum p1 p0 -> EachRep sum p1 p0 reps = repEach -type family EachRep sum+type family EachRep (sum :: * -> * -> *) :: * -> * -> * type instance EachRep (N a) = Rep a type instance EachRep (a :+: b) = EachRep a :+: EachRep b-class EachGeneric sum where- repEach :: sum -> EachRep sum ; objEach :: EachRep sum -> sum-instance Generic a => EachGeneric (N a) where- repEach (N x) = rep x ; objEach = N . obj-instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where- repEach = mapPlus repEach repEach- objEach = mapPlus objEach objEach+class EachGeneric sum where repEach :: sum p1 p0 -> EachRep sum p1 p0+instance (WN dc, Generic dc) => EachGeneric (N dc) where repEach = unSym rep unN+instance (EachGeneric a, EachGeneric b) => EachGeneric (a :+: b) where repEach = mapPlus repEach repEach @@ -136,12 +132,12 @@ -- -- In this example, @C0_@, @C1_@, and @C2_@ are fields types. The other fields -- types for the same data type are handled with the @default@ function.-precise_case :: (Codomain dcs ~ t, Codomain (DCs t) ~ t, DT t,- Partition (DCs t) dcs (DCs t :-: dcs)) =>- (DCs t :-: dcs -> a) -> t -> (dcs -> a) -> a-precise_case g x f = either f g $ partition $ disband x+precise_case0 :: (Codomain0 dcs ~ t, Codomain0 (DCs t) ~ t, DT t,+ Partition (DCs t) dcs (DCs t :-: dcs)) =>+ ((DCs t :-: dcs) p1 p0 -> a) -> t -> (dcs p1 p0 -> a) -> a+precise_case0 g x f = either f g $ partition $ unW0 disband x -- | @ig_from x =@ 'reps $ disband' @x@ is a convenience. It approximates the -- @instant-generics@ view, less the @CEq@ annotations.-ig_from :: (DT t, EachGeneric (DCs t)) => t -> EachRep (DCs t)-ig_from x = reps $ disband x+ig_from :: (ComposeW t, DT t, EachGeneric (DCs t)) => W t (EachRep (DCs t)) p1 p0+ig_from = reps `composeW` disband
Examples/LambdaLift/Common.hs view
@@ -1,3 +1,5 @@+{-# LANGUAGE TemplateHaskell, DataKinds, TypeFamilies #-}+ {- | Module : LambdaLift.Common@@ -14,4 +16,10 @@ module LambdaLift.Common where +import Data.Yoko+++ data Type = TyUnit | TyInt | TyFun Type Type deriving Show++yokoTH ''Type
Examples/LambdaLift/DeepSeq.hs view
@@ -1,5 +1,5 @@ {-# LANGUAGE TypeOperators, FlexibleInstances, FlexibleContexts,- UndecidableInstances #-}+ UndecidableInstances, DefaultSignatures, PolyKinds, DataKinds, TypeFamilies #-} {- | @@ -18,31 +18,54 @@ module LambdaLift.DeepSeq where import Data.Yoko+import Data.Bifunctor -class DeepSeq a where rnf :: a -> ()-instance DeepSeq a => DeepSeq [a] where- rnf [] = ()- rnf (x : xs) = rnf x `seq` rnf xs-instance DeepSeq a => DeepSeq (N a) where rnf = rnf . unN-instance (DeepSeq a, DeepSeq b) => DeepSeq (a :+: b) where- rnf = foldPlus rnf rnf---instance DeepSeq sum => DeepSeq (DCsOf a sum) where rnf = rnf . unDCsOf-instance (DeepSeq a, DeepSeq b) => DeepSeq (a :*: b) where- rnf = foldTimes seq rnf rnf-instance DeepSeq a => DeepSeq (Rec a) where rnf = rnf . unRec-instance DeepSeq a => DeepSeq (Dep a) where rnf = rnf . unDep-instance DeepSeq (f a) => DeepSeq (Par1 f a) where rnf = rnf . unPar1-instance DeepSeq U where rnf U = ()+class DeepSeq0 a where+ rnf0 :: a -> ()+ default rnf0 :: (DeepSeq2 (DCs a), DT a) => a -> ()+ rnf0 = rnf2 . unW0 disband+class DeepSeq1 a where+ rnf1 :: a () -> ()+ default rnf1 :: (DeepSeq2 (DCs a), DT a) => a () -> ()+ rnf1 = rnf2 . unW1 disband+class DeepSeq2 a where+ rnf2 :: a () () -> ()+ default rnf2 :: (DeepSeq2 (DCs a), DT a) => a () () -> ()+ rnf2 = rnf2 . unW2 disband -instance DeepSeq Int where rnf = (`seq` ())-instance (DeepSeq a, DeepSeq b) => DeepSeq (Either a b) where- rnf = either rnf rnf+instance (WN a, DeepSeq2 (Rep a), Generic a) => DeepSeq2 (N a) where+ rnf2 = rnf2 . unSym rep unN+instance (DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (a :+: b) where+ rnf2 = foldPlus rnf2 rnf2 -instance (DeepSeq a, DeepSeq b, DeepSeq c) =>- DeepSeq (a, b, c) where- rnf (a, b, c) = rnf a `seq` rnf b `seq` rnf c-instance (DeepSeq a, DeepSeq b, DeepSeq c, DeepSeq d) =>- DeepSeq (a, b, c, d) where- rnf (a, b, c, d) = rnf a `seq` rnf b `seq` rnf c `seq` rnf d+instance DeepSeq2 U where rnf2 U = ()+instance (DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (a :*: b) where+ rnf2 = foldTimes seq rnf2 rnf2+instance DeepSeq2 a => DeepSeq2 (C dc a) where rnf2 = rnf2 . unC++instance DeepSeq0 a => DeepSeq2 (T0 v a) where rnf2 = rnf0 . unT0+instance (Functor f, DeepSeq1 f, DeepSeq2 a) => DeepSeq2 (T1 v f a) where+ rnf2 = rnf1 . fmap rnf2 . unT1+instance (Bifunctor f, DeepSeq2 f, DeepSeq2 a, DeepSeq2 b) => DeepSeq2 (T2 (Rec lbl) f a b) where+ rnf2 = rnf2 . bimap rnf2 rnf2 . unT2++instance DeepSeq2 Par0 where rnf2 (Par0 ()) = ()+instance DeepSeq2 Par1 where rnf2 (Par1 ()) = ()++++instance (EQ ~ SpineCompare a a, DeepSeq0 a) => DeepSeq0 [a]+instance DeepSeq1 []++instance DeepSeq0 Int where rnf0 = (`seq` ())+instance (DeepSeq0 a, DeepSeq0 b) => DeepSeq0 (Either a b) where+ rnf0 = either rnf0 rnf0++instance (DeepSeq0 a, DeepSeq0 b, DeepSeq0 c) =>+ DeepSeq0 (a, b, c) where+ rnf0 (a, b, c) = rnf0 a `seq` rnf0 b `seq` rnf0 c+instance (DeepSeq0 a, DeepSeq0 b, DeepSeq0 c, DeepSeq0 d) =>+ DeepSeq0 (a, b, c, d) where+ rnf0 (a, b, c, d) = rnf0 a `seq` rnf0 b `seq` rnf0 c `seq` rnf0 d
Examples/LambdaLift/FreeVars.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances #-}+{-# LANGUAGE TypeOperators, FlexibleContexts, UndecidableInstances, KindSignatures, DataKinds, FlexibleInstances #-} {- | @@ -42,33 +42,35 @@ class FreeVars a where freeVars :: a -> Frees+class FreeVars2 a where freeVars2 :: a (p1 :: *) (p0 :: *) -> Frees instance FreeVars ULC where freeVars = w where- w tm = case partition $ disband tm of+ w tm = case partition $ unW0 disband tm of Left x -> ($ x) $ (\(Lam_ _ty tm) -> bump 1 $ w tm) .|| (\(Var_ i) -> IS.singleton i) .|. (\(Let_ ds tm) -> foldr (\(Decl _ tm) -> IS.union (w tm) . bump 1) (w tm) ds)- Right x -> freeVars x+ Right x -> freeVars2 x -- through sums --instance FreeVars sum => FreeVars (DCsOf t sum) where -- freeVars = freeVars . unDCsOf-instance (FreeVars a, FreeVars b) => FreeVars (a :+: b) where- freeVars = foldPlus freeVars freeVars-instance (Generic a, FreeVars (Rep a)) => FreeVars (N a) where- freeVars = freeVars . rep . unN+instance (FreeVars2 a, FreeVars2 b) => FreeVars2 (a :+: b) where+ freeVars2 = foldPlus freeVars2 freeVars2+instance (WN dc, Generic dc, FreeVars2 (Rep dc)) => FreeVars2 (N dc) where+ freeVars2 = freeVars2 . unSym rep unN -- through products-instance FreeVars U where freeVars = const IS.empty-instance (FreeVars a, FreeVars b) => FreeVars (a :*: b) where- freeVars = foldTimes IS.union freeVars freeVars+instance FreeVars2 U where freeVars2 = const IS.empty+instance (FreeVars2 a, FreeVars2 b) => FreeVars2 (a :*: b) where+ freeVars2 = foldTimes IS.union freeVars2 freeVars2+instance FreeVars2 a => FreeVars2 (C dc a) where freeVars2 = freeVars2 . unC -- through fields-instance FreeVars a => FreeVars (Rec a) where- freeVars = freeVars . unRec-instance FreeVars (Dep a) where freeVars = const IS.empty-instance (Foldable f, FreeVars a) => FreeVars (Par1 f a) where- freeVars = foldMap freeVars . unPar1+instance FreeVars a => FreeVars2 (T0 (Rec lbl) a) where+ freeVars2 = freeVars . unT0+instance FreeVars2 (T0 Dep a) where freeVars2 = const IS.empty+instance (Foldable f, FreeVars2 a) => FreeVars2 (T1 v f a) where+ freeVars2 = foldMap freeVars2 . unT1
Examples/LambdaLift/LambdaLift.hs view
@@ -28,7 +28,7 @@ import LambdaLift.LLBasics import LambdaLift.FreeVars (freeVars)-import LambdaLift.DeepSeq (DeepSeq(..))+import LambdaLift.DeepSeq (DeepSeq0(..), rnf2) @@ -42,12 +42,12 @@ data Cnv = Cnv type instance Idiom Cnv = M-instance Convert Cnv ULC TLF where convert Cnv = ll+instance Convert0 Cnv ULC TLF where convert0 Cnv = ll ll :: ULC -> M TLF-ll tm = precise_case tm llLam llVar llLet (Default $ hcompos Cnv)+ll tm = precise_case0 tm llLam llVar llLet (Default $ hcompos0 Cnv) llLam lams@(Lam_ tyTop tmTop) = do -- get the body; count formals; determine captives@@ -55,7 +55,7 @@ peel (acc, ty') (Lam ty tm) = peel (ty' : acc, ty) tm peel acc tm = (acc, tm) let nLocals = 1 + length tys -- NB "1 +" is for ty- let captives = IS.toAscList $ freeVars $ rejoin lams+ let captives = IS.toAscList $ freeVars $ unSym0 rejoin lams captives' = reverse captives (rho, rn) <- ask@@ -117,12 +117,12 @@ -instance DeepSeq Type where rnf = (`seq` ())-instance DeepSeq Occ where- rnf (Par x) = rnf x- rnf (Env x) = rnf x-instance DeepSeq Prog where rnf (Prog decs tm) = rnf decs `seq` rnf tm-instance DeepSeq TLF where rnf = rnf . reps . disband+instance DeepSeq0 Type where rnf0 = (`seq` ())+instance DeepSeq0 Occ where+ rnf0 (Par x) = rnf0 x+ rnf0 (Env x) = rnf0 x+instance DeepSeq0 Prog where rnf0 (Prog decs tm) = rnf0 decs `seq` rnf0 tm+instance DeepSeq0 TLF where rnf0 = rnf2 . unW0 ig_from @@ -130,4 +130,4 @@ -- this should evaluate without an exception if things are working; NB doesn't -- actually test correctness -- currently asking you to do that by -- investigating the value of each lambda-lifted term-all_exs = rnf [ex0', ex1', ex2', ex3', ex4', ex5']+all_exs = rnf0 [ex0', ex1', ex2', ex3', ex4', ex5']
Examples/LambdaLift/TLF.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators, DataKinds #-} {- | @@ -34,7 +34,7 @@ -concat `fmap` mapM yokoTH [''TLF]+concat `fmap` mapM yokoTH [''Occ, ''TLF, ''Prog] {- data Top_ = Top_ Int [Occ]
Examples/LambdaLift/ULC.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators #-}+{-# LANGUAGE TypeFamilies, TemplateHaskell, TypeOperators, DataKinds #-} {- |
+ Examples/MinCtors.hs view
@@ -0,0 +1,59 @@+{-# LANGUAGE TemplateHaskell, TypeFamilies, DataKinds #-}++module Examples.MinCtors where++import Data.Yoko+import Data.Yoko.MinCtors+import Data.Yoko.MinCtors.Prims0 ()++data I = I Int++data H = H I++data D = D0 H+ | D1 D+ | D2 D D++concat `fmap` mapM yokoTH [''I, ''H, ''D]++instance MinCtors I+instance MinCtors H+instance MinCtors D++{-++ *MinCtorsExample> minCtors (Proxy :: Proxy D)+ Just 3++This means that the minimal value uses three constructors.++@* -> *@ and @* -> * -> *@ kinded types have different result types. Consider+the minimal @(forall p1 p0. (p1, p0))@ value: it uses both of its parameters+once, and has its own single constructor.++ *MinCtorsExample> minCtors (Proxy :: Proxy (,))+ MMap {unMMap = fromList [((1,1),Min {getMin = 1})]}++Accordingly, the minimal @[]@ value uses its single parameter zero times.++ *MinCtorsExample> minCtors (Proxy :: Proxy [])+ MMap {unMMap = fromList [(0,Min {getMin = 1})]}++And there are two minimal @Either@ values, each which uses one of the+parameters. We track both because which one is ultimately minimal depends on+the instantiation of @Either@'s parameters, and their minimal counts.++ *MinCtorsExample> minCtors (Proxy :: Proxy Either)+ MMap {unMMap = fromList [((0,1),Min {getMin = 1}),((1,0),Min {getMin = 1})]}++These might not be necessary for your uses, but they are used by my generic+definitions in order to handle types like @T@ below that have internal+applications.++-}++data T = T (Either D ((Int, Int), (Bool, Bool)))++yokoTH ''T++instance MinCtors T
yoko.cabal view
@@ -1,5 +1,5 @@ name: yoko-version: 0.9+version: 2.0 synopsis: Generic Programming with Disbanded Data Types description:@@ -97,12 +97,12 @@ build-depends: th-sccs, invariant - build-depends: type-equality, bifunctors+ build-depends: type-equality, bifunctors, semigroups build-depends: kinds >= 0.0.1.5, type-functions >= 0.2.0.3, records >= 0.1.1.6 build-depends:- type-spine >= 0.2, type-digits >= 0.2, type-cereal >= 0.2, type-ord >= 0.2, type-ord-spine-cereal >= 0.2+ type-spine >= 0.2.0.20120924, type-digits >= 0.2, type-cereal >= 0.2, type-ord >= 0.2, type-ord-spine-cereal >= 0.2 exposed-modules: Data.Yoko,@@ -111,7 +111,16 @@ Data.YokoRaw, Data.Yoko.HCompos, Data.Yoko.TH, - Data.Yoko.TypeBasics, Data.Yoko.Each+ Data.Yoko.Invariant,++ Data.Yoko.TypeBasics, Data.Yoko.W,++ Data.Yoko.Prelude,++ Data.Yoko.MinCtors,+ Data.Yoko.MinCtors.Prims0, Data.Yoko.MinCtors.Prims1,+ Data.Yoko.MinCtors.Minima,+ Data.Yoko.MinCtors.MMap other-modules: Data.Yoko.View,