yoko 0.2 → 0.3

raw patch · 47 files changed

+556/−2726 lines, 47 filesdep +template-haskelldep −taggedPVP ok

version bump matches the API change (PVP)

Dependencies added: template-haskell

Dependencies removed: tagged

API changes (from Hackage documentation)

Files

• CHANGES +8/−0
• Data/Yoko.hs +89/−15
• Data/Yoko/Cata.hs +0/−78
• Data/Yoko/Core.hs +0/−83
• Data/Yoko/CoreTypes.hs +0/−17
• Data/Yoko/Each.hs +38/−0
• Data/Yoko/Generic.hs +0/−156
• Data/Yoko/HCompos.hs +70/−0
• Data/Yoko/InDT.hs +0/−78
• Data/Yoko/MaybeKind.hs +20/−0
• Data/Yoko/Reduce.hs +0/−77
• Data/Yoko/Reflect.hs +0/−121
• Data/Yoko/ReflectBase.hs +0/−110
• Data/Yoko/Representation.hs +96/−0
• Data/Yoko/TypeBasics.hs +37/−0
• Data/Yoko/TypeSums.hs +115/−0
• Data/Yoko/TypeSumsAux.hs +12/−0
• Examples/Ex.hs +0/−6
• Examples/ExG.hs +0/−60
• Examples/InnerBase.hs +0/−8
• Examples/InnerGeneric.hs +0/−90
• Examples/LL.hs +0/−63
• Examples/LL0.hs +0/−57
• Examples/LLBase.hs +0/−13
• Examples/LLBasics.hs +0/−71
• Examples/LLDirect.hs +0/−81
• Examples/LLGeneric.hs +0/−89
• Examples/Main.hs +0/−25
• Examples/ReflectAux.hs +0/−19
• Examples/TermBase.hs +0/−24
• Examples/TermGeneric.hs +0/−190
• Examples/TermInner.hs +0/−60
• Examples/TermTest.hs +0/−93
• Examples/Test.hs +21/−0
• README +1/−1
• Type/Yoko.hs +0/−36
• Type/Yoko/BTree.hs +0/−194
• Type/Yoko/Fun.hs +0/−136
• Type/Yoko/FunA.hs +0/−36
• Type/Yoko/MFun.hs +0/−97
• Type/Yoko/Natural.hs +0/−82
• Type/Yoko/Sum.hs +0/−102
• Type/Yoko/TFunA.hs +0/−110
• Type/Yoko/TSTSS.hs +0/−29
• Type/Yoko/Type.hs +0/−84
• Type/Yoko/Universe.hs +0/−87
• yoko.cabal +49/−48

@@ -1,3 +1,11 @@+0.2 -> 0.4+===============++* drastic simplifications when writing the ICFP submission++* I'll eventually work those older features back in --- Though it is+  *extremely* unlikely, I apologize if you were using them.+ 0.1 -> 0.2 =============== 

@@ -1,19 +1,93 @@-{- |+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleContexts,+  MultiParamTypeClasses, FlexibleInstances, ConstraintKinds,+  ScopedTypeVariables, UndecidableInstances #-} -Module      :  Data.Yoko-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3+module Data.Yoko+  (derive, Equal, module Data.Yoko.Representation,+   module Data.Yoko.TypeSums, module Data.Yoko, encode) where -Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)+import Data.Yoko.TypeBasics+import Data.Yoko.Representation+import Data.Yoko.TypeSums (Embed, Partition, (:-:))+import qualified Data.Yoko.TypeSums as TypeSums+import Data.Yoko.Each --}-module Data.Yoko-  (module Type.Yoko, module Data.Yoko.Generic, module Data.Yoko.Reflect, module Data.Yoko.InDT-  ) where+import Control.Arrow (right, (+++)) -import Type.Yoko-import Data.Yoko.Generic-import Data.Yoko.Reflect-import Data.Yoko.InDT++++one :: (dc -> a) -> DCsOf (Range dc) (N dc) -> a+one = (. unDCsOf) . foldN++infixl 9 .|.   ;   f .|. g = one f ||| one g+infixr 8 .||   ;   f .|| g = one f ||| g+infixl 8 ||.   ;   f ||. g = f ||| one g++++type family Tag dc++type family Range dc+class (Generic dc, DT (Range dc)) => DC dc where rejoin :: dc -> Range dc++type family DCs t+type Disbanded t = DCsOf t (DCs t)+class Each IsDCOf (DCs t) => DT t where disband :: t -> Disbanded t++class (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),+       Embed (N dc) (DCs (Range dc))) => IsDCOf dc+instance (Partition (DCs (Range dc)) (N dc) (DCs (Range dc) :-: N dc),+          Embed (N dc) (DCs (Range dc))) => IsDCOf dc++++disbanded :: Embed (N dc) (DCs (Range dc)) => dc -> Disbanded (Range dc)+disbanded = DCsOf . TypeSums.inject++band :: forall t. Each (ConDCOf t) (DCs t) => Disbanded t -> t+band = each (Proxy :: Proxy (ConDCOf t)) rejoin++class (Range dc ~ t, DC dc) => ConDCOf t dc+instance (Range dc ~ t, DC dc) => ConDCOf t dc++++inject :: Embed (N dc) sum => dc -> sum+inject = TypeSums.inject++partition :: Partition sum sub (sum :-: sub) =>+             DCsOf t sum -> Either (DCsOf t sub) (DCsOf t (sum :-: sub))+partition = (DCsOf +++ DCsOf) . TypeSums.partition . unDCsOf++project :: Partition sum (N dc) (sum :-: N dc) =>+           DCsOf (Range dc) sum -> Either dc (DCsOf (Range dc) (sum :-: N dc))+project = right DCsOf . TypeSums.project . unDCsOf++++-- TODO need a MapSum just like MapRs, use a RPV for rep+reps :: EachGeneric sum => DCsOf t sum -> EachRep sum+reps = repEach . unDCsOf++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++++++exact_case :: (DT t, Partition (DCs t) dcs (DCs t :-: dcs)) =>+  (DCsOf t (DCs t :-: dcs) -> a) -> t -> (DCsOf t dcs -> a) -> a+exact_case g x f =+  either f g $ partition $ disband x++ig_from x = reps $ disband x

@@ -1,78 +0,0 @@-{-# LANGUAGE QuasiQuotes, TypeOperators, TypeFamilies, GADTs #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE MultiParamTypeClasses, FlexibleContexts, FlexibleInstances,-  UndecidableInstances #-}--{- |--Module      :  Data.Yoko.Algebra-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Catamorphism for mutually-recursive datatypes.---}-module Data.Yoko.Cata-  (Algebras, SiblingAlgs, algebras, CataU(..), catas, cata,-  module Data.Yoko.Reduce) where-    -import Type.Yoko--import Data.Yoko.Generic-import Data.Yoko.Reflect-import Data.Yoko.Reduce------type Algebras ts m = Each ts (Algebra m)-type SiblingAlgs t m = Algebras (Siblings t) m---- | Builds an 'Each' of algebras via 'AlgebraDT'.-algebras :: forall ts m. (ts ::: All (AlgebraU m)) => [qP|m|] -> Algebras ts m-algebras _ = each [qP|AlgebraU m :: *->*|] $ \AlgebraU -> algebraDT------- | @t@ inhabits @CataU ts m@ if------   1. @t@ is an instance of 'DT' and @ts ~ Siblings t@------   2. the recursive reduction can be mapped as a 'FromAt' function via---   'RMMap' across all constructors of @t@ and------   3. all of @t@'s siblings also inhabit the same universe.-data CataU ts m t where-  CataU :: (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),-            DCs t ::: All-              (YieldsArrowTSSU-               (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),-            ts ::: All (CataU ts m)-           ) => CataU ts m t-instance (DT t, ts ~ Siblings t, ts ::: Exists ((:=:) t),-          DCs t ::: All-            (YieldsArrowTSSU-             (AsComp (RMMap (SiblingsU t) (FromAt m) IdM :. N))),-          ts ::: All (CataU ts m)-         ) => t ::: CataU ts m where inhabits = CataU--catas :: forall m ts. (ts ::: All (CataU ts m)) =>-         Algebras ts m -> Each ts (FromAt m IdM)-catas fs = each [qP|CataU ts m :: *->*|] $ \d@CataU -> cataD d fs--cataD :: forall m t. CataU (Siblings t) m t -> SiblingAlgs t m -> t -> Med m t-cataD CataU fs =-  appNT fs (inhabits :: Uni (Siblings t) t) .-  appNTtoNP (eachArrow $ AsComp $ composeWith [qP|N :: *->*|] $-             RMMap $ catas fs) . disband---- | Uses the @m@-mediated algebras for @t@'s siblings to reduce a @t@ to @Med--- m t@.-cata :: (t ::: CataU (Siblings t) m) => SiblingAlgs t m -> t -> Med m t-cata = cataD inhabits

@@ -1,83 +0,0 @@-{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances, EmptyDataDecls #-}--{-# LANGUAGE TemplateHaskell #-}--{- |--Module      :  Data.Yoko.Core-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The core structural types; \"sum of products\" and such.---}--module Data.Yoko.Core where--import Type.Yoko.Type (derive)----import Polarity------ | Structural representations (e.g. "Data.Yoko.Generic"'s 'RM') of a @*@ type--- can be derived as a data family indexed by the core representation (@Rep@)--- of that type.-type family Rep a------ | void-data V--- | unit-data U = U--- | a dependency-newtype D a = D a--- | a recursive occurrence-newtype R t = R t--- | argument to a @* -> *@-newtype F f c = F (f c)--- | arguments to a @* -> * -> *@-newtype FF ff c d = FF (ff c d)--- | meta information-newtype M i c = M c---- | a named intermediate (user hook); crucially: @type instance Rep (N t) =--- Rep t@.-newtype N t = N t--type instance Rep (N t) = Rep t   -- this is the crucial meaning of N----concat `fmap` mapM derive [''V, ''U, ''D, ''R, ''F, ''FF, ''M, ''N]----infixr 6 :*-type (:*) = FF (,)------{--type instance Polarity ([qK|*->*->*|] M) (ki :* kt :* U) = Neutral-type instance Polarity ([qK|*->*|] (M i)) (kt :* U) = Pos--type instance Polarity ([qK|*->*|] R) (ka :* U) = Pos--type instance Polarity ([qK|(*->*)->*->*|] F) (kf :* kt :* U) = Pos-type instance Polarity ([qK|*->*|] (F f)) (kt :* U) =-  Polarity ([qK|*->*|] f) (kt :* U)--type instance Polarity ([qK|(*->*->*)->*->*->*|] FF) (kff :* kt :* ks :* U) = Pos-type instance Polarity ([qK|*->*->*|] (FF ff)) (kt :* ks :* U) =-  Polarity ([qK|*->*->*|] ff) (kt :* ks :* U)-type instance Polarity ([qK|*->*|] (FF ff t)) (ks :* U) =-  Polarity ([qK|*->*|] (ff t)) (ks :* U)--}

@@ -1,17 +0,0 @@-{- |--Module      :  Data.Yoko.CoreTypes-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Just the "Data.Yoko.Core" types -- doesn't export the constructors.---}--module Data.Yoko.CoreTypes (Rep, V, U, D, R, F, FF, M, N, (:*)) where--import Data.Yoko.Core

@@ -0,0 +1,38 @@+{-# LANGUAGE KindSignatures, ConstraintKinds, MultiParamTypeClasses,+  Rank2Types, FlexibleInstances, UndecidableInstances, TypeOperators #-}++module Data.Yoko.Each (Each, each) where++import Data.Yoko.TypeBasics+import Data.Yoko.Representation++++type Each = Each_+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)

@@ -1,156 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeFamilies, QuasiQuotes, StandaloneDeriving,-  FlexibleInstances, FlexibleContexts, UndecidableInstances, GADTs,-  MultiParamTypeClasses, TypeOperators, EmptyDataDecls  #-}--{- |--Module      :  Data.Yoko.Generic-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Representations of many Haskell types as compositions of "Data.Yoko.Core"-types.---}--module Data.Yoko.Generic-  (module Data.Yoko.Generic, module Data.Yoko.CoreTypes) where--import Data.Yoko.CoreTypes---import qualified Data.Yoko.Core as Core--import Type.Yoko.Type---import Type.Yoko.Universe ((:::)(..))----import qualified Control.Arrow as Arrow-                       --{- | @RM@ stands is for \"recursively mediated\", and @m@ is the \"mediator (of-recursive occurrences)\".--@-  data instance RM m V-  data instance RM m U = U-  newtype instance RM m (D a) = D a-  newtype instance RM m (R t) = R (Med m t)-  newtype instance RM m (F f c) = F (f (RM m c))-  newtype instance RM m (FF ff c d) = FF (ff (RM m c) (RM m d))-  newtype instance RM m (M i c) = M (RM m c)-@---}-data family RM m c-data instance RM m V-data instance RM m U = U-newtype instance RM m (D a) = D a-newtype instance RM m (R t) = R (Med m t)-newtype instance RM m (F f c) = F (f (RM m c))-newtype instance RM m (FF ff c d) =-  FF (ff (RM m c) (RM m d))-newtype instance RM m (M i c) = M (RM m c)---- | In @yoko@, the 'N' core type is used for a lightweight representation of--- constructor types -- each will define its own instance of @RM (N _)@.-type RMN m dc = RM m (N dc)--type RMI = RM IdM-type RMNI dc = RMN IdM dc------ | @Generic@ represents a recursion-mediated type @N a@ as a--- recursion-mediated @Rep a@. The opposite of \"representation\" is (the--- represented) \"object\".-class Generic a where-  rep :: RM m (N a) -> RM m (Rep a)-  obj :: RM m (Rep a) -> RM m (N a)--{-asRep :: (Generic a, Generic b) => (RM m (Rep a) -> RM m (Rep b)) -> RM m (N a) -> RM m (N b)-asRep f = obj . f . rep--asGist :: (Gist c, Gist d) => (Gst c m -> Gst d n) -> RM m c -> RM n d-asGist f = frip . f . gist--convertR :: (Gist c, Gst c m ~ Gst c n) => RM m c -> RM n c-convertR = asGist id-}---{---- @gist@ folds the mediator @m@ into the type and forgets all the frippery of--- the core representation. (The opposite of \"gist\" is \"frippery\".)-type family Gst c m-class Gist c where-  gist :: RM m c -> Gst c m-  frip :: Gst c m -> RM m c--data AsRep u t where AsRep :: u (Rep t) -> AsRep u t-instance (Rep t ::: u) => t ::: AsRep u where inhabits = AsRep inhabits--data GistD c where GistD :: Gist c => GistD c-instance Gist c => c ::: GistD where inhabits = GistD-gistD :: GistD c -> RM m c -> Gst c m; gistD GistD = gist-fripD :: GistD c -> Gst c m -> RM m c; fripD GistD = frip----type instance Gst (F f c) m = f (Gst c m)-instance (Functor f, Gist c) => Gist (F f c) where-  gist (F x) = fmap gist x-  frip = F . fmap frip-type instance Gst (FF Either c d) m = Either (Gst c m) (Gst d m)-instance (Gist c, Gist d) => Gist (FF Either c d) where-  gist = (gist Arrow.+++ gist) . unFF-  frip = FF . (frip Arrow.+++ frip)-type instance Gst (FF (,) c d) m = (,) (Gst c m) (Gst d m)-instance (Gist c, Gist d) => Gist (FF (,) c d) where-  gist = (gist Arrow.*** gist) . unFF-  frip = FF . (frip Arrow.*** frip)-type instance Gst (D a) m = a-instance Gist (D a) where gist (D x) = x; frip = D-type instance Gst (M i c) m = Gst c m-instance Gist c => Gist (M i c) where-  gist = gist . unM; frip = M . frip-type instance Gst (R t) m = Med m t-instance Gist (R t) where gist (R x) = x; frip = R-type instance Gst U m = ()-instance Gist U where gist _ = (); frip _ = U-type instance Gst V m = Core.V-instance Gist V where gist = absurd "gist[V]"; frip _ = void "gist[V]"-type instance Gst (N n) m = Gst (Rep n) m-instance (Generic t, Gist (Rep t)) => Gist (N t) where-  gist = gist . rep; frip = obj . frip--}---unD :: RM m (D a) -> a-unD (D x) = x--unM :: RM m (M i c) -> RM m c-unM (M x) = x--unR :: RM m (R t) -> Med m t-unR (R x) = x-deriving instance Eq (Med m t) => Eq (RM m (R t))-deriving instance Show (Med m t) => Show (RM m (R t))--instance Eq (RM m V) where _ == _ = True -- undefined?-instance Show (RM m V) where show _ = "<void>"-void :: String -> RM m V-void n = error $ "GenericR.void: " ++ n-absurd :: String -> RM m V -> a-absurd n = error $ "GenericR.absurd: " ++ n--unF (F x) = x-unFF (FF x) = x-deriving instance Eq (ff (RM m c) (RM m d)) => Eq (RM m (FF ff c d))-deriving instance Show (ff (RM m c) (RM m d)) => Show (RM m (FF ff c d))------concat `fmap` mapM derive [''RM]

@@ -0,0 +1,70 @@+{-# LANGUAGE TypeFamilies, TypeOperators, MultiParamTypeClasses,+  FlexibleContexts, FlexibleInstances, UndecidableInstances,+  ScopedTypeVariables  #-}++{-# OPTIONS_GHC -fcontext-stack=250 #-}++module Data.Yoko.HCompos (Idiom, HCompos(..)) where++import Data.Yoko.TypeBasics+import Data.Yoko++++import Control.Applicative++++++instance HCompos cnv sum t => HCompos cnv (DCsOf a sum) t where+  hcompos cnv = hcompos cnv . unDCsOf++++++type family Idiom cnv :: * -> *+class Applicative (Idiom cnv) => HCompos cnv a t where+  hcompos :: cnv -> a -> Idiom cnv t++++++instance (HCompos cnv a t, HCompos cnv b t+         ) => HCompos cnv (a :+: b) t where+  hcompos cnv = foldPlus (hcompos cnv) (hcompos cnv)++-- NB only works if there's exactly one matching constructor+instance (Generic dc, Just (N dc') ~ FindDCs (Tag dc) (DCs t),+          HComposRs cnv (Rep dc) (Rep dc'),+          DC dc', Range dc' ~ t, DT t+         ) => HCompos cnv (N dc) t where+  hcompos cnv = +    foldN $ liftA (rejoin . (id :: dc' -> dc') . obj) . mapRs cnv . rep++++type family FindDCs s sum+type instance FindDCs s (N dc) =+  If (Equal s (Tag dc)) (Just (N dc)) Nothing+type instance FindDCs s (a :+: b) = DistMaybePlus (FindDCs s a) (FindDCs s b)++++-- applies cnv to every Rec in a product; identity on other factors+class Applicative (Idiom cnv) => HComposRs cnv prod prod' where+  mapRs :: cnv -> prod -> Idiom cnv prod'++instance HCompos cnv a b => HComposRs cnv (Rec a) (Rec b) where+  mapRs cnv (Rec x) = Rec <$> hcompos cnv x++instance Applicative (Idiom cnv) => HComposRs cnv (Dep a) (Dep a) where+  mapRs _ = pure+instance Applicative (Idiom cnv) => HComposRs cnv U       U       where+  mapRs _ = pure++instance (HComposRs cnv a a', HComposRs cnv b b'+         ) => HComposRs cnv (a :*: b) (a' :*: b') where+  mapRs cnv (a :*: b) = (:*:) <$> mapRs cnv a <*> mapRs cnv b

@@ -1,78 +0,0 @@-{-# LANGUAGE TypeOperators, GADTs, FlexibleInstances, MultiParamTypeClasses,-  FlexibleContexts, UndecidableInstances, Rank2Types #-}--{- |--Module      :  Data.Yoko.InDT-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Various universes determined by a data constructor type's suitability to be-embedded in a data type.---}-module Data.Yoko.InDT where--import Type.Yoko--import Data.Yoko.Generic-import Data.Yoko.Reflect------ | A type @t@ inhabits @HasTagRepU tag c@ if @t@ is a 'DT' and there exists a @t@--- constructor satisfying @'TagRepIs' tag c@.-data HasTagRepU tag c t where-  HasTagRepU :: DT t => Exists (DCOf t :&& TagRepIs tag c) (DCs t) ->-                HasTagRepU tag c t-instance (DT t, DCs t ::: Exists (DCOf t :&& TagRepIs tag c)-         ) => t ::: HasTagRepU tag c where inhabits = HasTagRepU inhabits---- | Given @HasTagRepU tag c t@, a trivially-mediated @c@ value can be embedded into--- @t@.-hasTagRepU :: HasTagRepU tag c t -> RMI c -> t-hasTagRepU (HasTagRepU d) = w d where-  w :: Exists (DCOf t :&& TagRepIs tag c) dcs -> RMI c -> t-  w (Here (x@(DCOf _) :&& TagRepIs)) = fr_DCOf x . obj-  w (OnLeft u) = w u; w (OnRight u) = w u-------- | Often times, we're interested in the universe of types accomodating a data--- constructor's image under some type-function.-type HasTagRepImageU fn dc = HasTagRepU (Tag dc) (CApp fn (Rep dc))---- | A constructor type @dc@ inhabits @ImageHasTagRepU t fn@ if------ 1. @fn@ can be mapped across the recursive occurrences in @dc@, and------ 2. @t@ has a constructor isomorphic to the @fn@-image of @dc@ -data ImageInDTU t fn dc where-  ImageInDTU :: (Generic dc, Rep dc ::: Domain (CMap fn IdM)-                ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTU t fn dc-instance (Generic dc, Rep dc ::: Domain (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc-         ) => dc ::: ImageInDTU t fn where-  inhabits = ImageInDTU inhabits---- | Given @ImageInDTU t fn dc@, a trivially-mediated @dc@ value can be--- embedded into @t@.-imageInDTU :: (forall t. fn IdM t) -> ImageInDTU t fn dc -> RMNI dc -> t-imageInDTU fn (ImageInDTU d) = hasTagRepU d . apply (CMap fn) . rep---- | Same as @ImageInDTD@, but uses an implicitly applicative function.-data ImageInDTDA t fn dc where-  ImageInDTDA :: (Generic dc, Rep dc ::: DomainA (CMap fn IdM)-                 ) => HasTagRepImageU (fn IdM) dc t -> ImageInDTDA t fn dc-instance (Generic dc, Rep dc ::: DomainA (CMap fn IdM), t ::: HasTagRepImageU (fn IdM) dc-         ) => dc ::: ImageInDTDA t fn where-  inhabits = ImageInDTDA inhabits--imageInDTAU :: Functor (Idiom (fn IdM)) =>-               (forall t. fn IdM t) -> ImageInDTDA t fn dc -> RMNI dc -> Idiom (fn IdM) t-imageInDTAU fn (ImageInDTDA d) = fmap (hasTagRepU d) . applyA (CMap fn) . rep

@@ -0,0 +1,20 @@+{-# LANGUAGE TypeFamilies, EmptyDataDecls #-}++module Data.Yoko.MaybeKind where++import Type.Booleans++data Nothing+data Just (x :: *)++type family IsJust (x :: *) :: * -- returns Bool, ideally+type instance IsJust Nothing = False+type instance IsJust (Just x) = True++type family MaybePlus1 (x :: *) (y :: *) :: *+type instance MaybePlus1 Nothing y = y+type instance MaybePlus1 (Just x) Nothing = Just x++type family MaybeMap (f :: * -> *) (x :: *) :: *+type instance MaybeMap f (Just x) = Just (f x)+type instance MaybeMap f Nothing = Nothing

@@ -1,77 +0,0 @@-{-# LANGUAGE QuasiQuotes, ScopedTypeVariables, TypeOperators, GADTs,-  MultiParamTypeClasses, FlexibleContexts, TypeSynonymInstances,-  FlexibleInstances, UndecidableInstances, TypeFamilies #-}--{- |--Module      :  Data.Yoko.Reduce-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--A @t@-algebra reduces a disbanded @t@ into a mediation of @t@.---}-module Data.Yoko.Reduce-  (Alg, Algebra(..), AlgebraU(..),-   algebraFin, AlgebraDT(..), AlgebraUni, AlgebraDC(..)) where--import Type.Yoko--import Data.Yoko.Generic-import Data.Yoko.Reflect-------- | A @t@-algebra reduces a disbanded @t@ to the same mediation of @t@.-type Alg m t = Disbanded m t -> Med m t-newtype Algebra m t = Alg (Alg m t)-type instance Unwrap (Algebra m) t = Alg m t-instance Wrapper (Algebra m) where wrap = Alg; unwrap (Alg x) = x--data AlgebraU m t where-  AlgebraU :: (DT t, AlgebraDT m t) => AlgebraU m t-instance (DT t, AlgebraDT m t-         ) => t ::: AlgebraU m where inhabits = AlgebraU------algebraFin :: (AlgebraUni m (Inhabitants u), Finite u) =>-             AnRMN m u -> Med m (LeftmostRange (Inhabitants u))-algebraFin = algebraUni . finiteNP------ | @algebraDT@ determines the algebra from the type and mediator.-class DT t => AlgebraDT m t where algebraDT :: Disbanded m t -> Med m t----- | @algebraUni@ determines the \"algebra\" from the type-sum and mediator.-class AlgebraUni m dcs where-  algebraUni :: AnRMN m (Uni dcs) -> Med m (LeftmostRange dcs)--instance (Med m (LeftmostRange ts) ~ Med m (LeftmostRange us),-          AlgebraUni m ts, AlgebraUni m us) => AlgebraUni m (ts :+ us) where-  algebraUni = algebraUni `two` algebraUni-instance AlgebraDC m dc => AlgebraUni m (N dc) where-  algebraUni (NP (Uni (Here Refl)) x) = algebraDC x---- | @algebraDC@ determines the \"alegbra\" from the constructor type and--- mediator.-class DC dc => AlgebraDC m dc where algebraDC :: RMN m dc -> Med m (Range dc)----type OneOf ts = NP (Uni ts)--two :: (OneOf ts f -> a) -> (OneOf us f -> a) -> (OneOf (ts :+ us) f -> a)-two f g (NP (Uni tag) x) = case tag of-  OnLeft u -> f $ NP (Uni u) x-  OnRight v -> g $ NP (Uni v) x

@@ -1,121 +0,0 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances, GADTs,-  ScopedTypeVariables, FlexibleContexts, UndecidableInstances, QuasiQuotes,-  TypeOperators, TypeSynonymInstances, Rank2Types, ViewPatterns #-}--{- |--Module      :  Data.Yoko.Reflect-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Definitions on top of the basic @yoko@ reflection concepts "Data.Yoko.ReflectBase".---}--module Data.Yoko.Reflect-  (module Data.Yoko.Reflect, module Data.Yoko.ReflectBase) where--import Type.Yoko--import Data.Yoko.Generic-import Data.Yoko.ReflectBase hiding (DCU)----type instance Tag (N dc) = Tag dc----type instance Recurs (D a) = V-type instance Recurs (F f c) = Recurs c-type instance Recurs (FF ff c d) =-  NormW (Recurs c) (Recurs d) -- NormW avoiding duplication-type instance Recurs (M i c) = Recurs c-type instance Recurs (N t) = Recurs (Rep t)-type instance Recurs (R t) = N t-type instance Recurs U = V-type instance Recurs V = V--type SiblingsU t = Uni (Siblings t)----type OnlyDC t = UnN (DCs t)-type family UnN a-type instance UnN (N dc) = dc--uniqueDC :: (DT t, N (OnlyDC t) ~ DCs t, t ~ Range (OnlyDC t)) => t -> RMNI (OnlyDC t)-uniqueDC = uniqueRMN . disband--uniqueRMN :: (Finite u, N (UnN (Inhabitants u)) ~ Inhabitants u-             ) => AnRMN m u -> RMN m (UnN (Inhabitants u))-uniqueRMN x = case finiteNP x of NP (Uni (Here Refl)) x -> x--uniqueRMN' :: (Finite (DCOf (Range dc)), N dc ~ DCs (Range dc)-              ) => AnRMN m (DCOf (Range dc)) -> RMN m dc-uniqueRMN' = uniqueRMN------data IsDC dc where IsDC :: DC dc => IsDC dc-type instance Pred IsDC t = True-instance DC dc => dc ::: IsDC where inhabits = IsDC--newtype RMNTo m b dc = RMNTo {rmnTo :: RMN m dc -> b}-type instance Unwrap (RMNTo m b) dc = RMN m dc -> b-instance Wrapper (RMNTo m b) where wrap = RMNTo; unwrap = rmnTo------- | Just a specialization: @dcDispatch = (. disband) . dcDispatch'@.-dcDispatch :: DT t => NT (DCOf t) (RMNTo IdM b) -> t -> b-dcDispatch = (. disband) . dcDispatch'---- | Just a specialization: @dcDispatch' nt ('NP' ('DCOf' tag) fds) = 'appNT'--- nt tag fds@.-dcDispatch' :: DT t => NT (DCOf t) (RMNTo IdM b) -> Disbanded IdM t -> b-dcDispatch' nt (NP tag fds) = appNT nt tag fds-----{- | A fundamental notion of identity in @yoko@, the @TagRepIs tag c@ universe-contains all constructor types @dc@ where @(Tag dc ~ tag, c ~ Rep dc)@.--@-  type instance Pred (TagRepIs tag c) dc =-    And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))-@---}-data TagRepIs tag c dc where-  TagRepIs :: (Tag dc ~ tag, c ~ Rep dc) => TagRepIs tag c dc-instance (Tag dc ~ tag, c ~ Rep dc) => dc ::: TagRepIs tag c where-  inhabits = TagRepIs-type instance Pred (TagRepIs tag c) dc =-  And (IsEQ (Compare (Tag dc) tag)) (IsEQ (Compare (Rep dc) c))--{-data TagGistEQ tag gst m dc where-  TagGistEQ :: (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst-               ) => TagGistEQ tag gst m dc-instance (Tag dc ~ tag, Gist (N dc), Gst (N dc) m ~ gst-         ) => dc ::: TagGistEQ tag gst m where inhabits = TagGistEQ-type instance Pred (TagGistEQ tag gst m) dc =-  And (IsEQ (Compare (Tag dc) tag))-      (IsEQ (Compare (Gst (N dc) m) gst))-}-------- | Just a specialization: @bandDCs = band@.-bandDCs :: DT t => Disbanded IdM t -> t; bandDCs = band--fr_DCOf :: DCOf t dc -> RMNI dc -> t; fr_DCOf (DCOf _) = fr

@@ -1,110 +0,0 @@-{-# LANGUAGE TypeFamilies, GADTs, MultiParamTypeClasses, TypeOperators,-  FlexibleContexts, ScopedTypeVariables, ViewPatterns, FlexibleInstances,-  QuasiQuotes, UndecidableInstances, Rank2Types #-}--{- |--Module      :  Data.Yoko.ReflectBase-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The basic @yoko@ reflection concepts.---}-module Data.Yoko.ReflectBase where--import Type.Yoko-import Data.Yoko.Generic----- | The @Tag@ of a constructor type is a type-level reflection of its--- constructor name.-type family Tag dc---- | The @Recurs@ of a constructor type is the type-"Type.Yoko.Sum" of types--- that occur in this constructor. NB: @Recurs t `isSubsumedBy` Siblings (Range--- dc)@.-type family Recurs t---- | The \"Datatype Constructor\" class.-class (DT (Range dc), dc ::: DCU (Range dc), Generic dc) => DC dc where-  -- | The string name of this constructor.-  occName :: [qP|dc|] -> String --  -- | The range of this constructor.-  type Range dc--  -- | The evidence that this constructor inhabits the datatype constructor-  -- universe of its range.-  tag :: DCOf (Range dc) dc; tag = inhabits--  -- | Project this constructor from its range.-  to :: Range dc -> Maybe (RMNI dc)-  to (disband -> NP tg fds) = case eqT tg (tag :: DCOf (Range dc) dc) of-    Just Refl -> Just fds-    _ -> Nothing--  -- | Embed this constructor in its range.-  fr :: RMNI dc -> Range dc---- | Evidence that @t@ is the range of the constructor type @dc@.-data DCOf t dc where DCOf :: (DC dc, t ~ Range dc) => DCU t dc -> DCOf t dc-instance (DC dc, t ~ Range dc) => dc ::: DCOf t where inhabits = DCOf inhabits-type instance Inhabitants (DCOf t) = Inhabitants (DCU t)-instance Finite (DCU t) => Finite (DCOf t) where toUni (DCOf x) = toUni x-type instance Pred (DCOf t) dc = Elem dc (DCs t)-instance EqT (DCU t) => EqT (DCOf t) where eqT (DCOf x) (DCOf y) = eqT x y--data SiblingOf t s where SiblingOf :: (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => Uni (Siblings t) s -> SiblingOf t s-instance (s ::: Uni (Siblings t), Siblings s ~ Siblings t, DT s) => s ::: SiblingOf t where inhabits = SiblingOf inhabits-type instance Inhabitants (SiblingOf t) = Siblings t-instance Finite (SiblingOf t) where toUni (SiblingOf x) = x-type instance Pred (SiblingOf t) s = Elem s (Siblings t)-instance EqT (SiblingOf t) where eqT (SiblingOf x) (SiblingOf y) = eqT x y----type AnRMN m u = NP u (RM m :. N)-type Disbanded m t = AnRMN m (DCOf t)--disbanded :: DC dc => RMN m dc -> Disbanded m (Range dc)-disbanded fds = NP tag fds--band :: Disbanded IdM t -> t-band (NP (DCOf _) fds) = fr fds------ @LeftmostRange@ returns the @Range@ of the leftmost type in a type-sum.-type family LeftmostRange dcs-type instance LeftmostRange (N dc) = Range dc-type instance LeftmostRange (c :+ d) = LeftmostRange c--type DCs t = Inhabitants (DCOf t)---- | The "DataType" class.-class (Finite (DCU t), EqT (DCU t),-       DCs t ::: All (DCOf t), -- DCs t ::: All (AsRep GistU),-       Siblings t ::: All (SiblingOf t)-      ) => DT t where-  -- | The string name of this datatype's original package.-  packageName :: [qP|t|] -> String-  -- | The string name of this datatype's original module.-  moduleName :: [qP|t|] -> String--  -- | A type-sum of the types in this type's binding group, including-  -- itself. @Siblings t@ ought to be the same for every type @t@ in the-  -- binding group. (It also ought to be equivalent to the transitive closure-  -- of @Recurs . DCs@, by definition.)-  type Siblings t- -  -- | The data constructor universe. 'DCOf' is to be preferred as much as-  -- possible.-  data DCU t :: * -> * -- universe of constructor types--  -- | /Disband/ this type into one of its data constructors.-  disband :: t -> Disbanded IdM t

@@ -0,0 +1,96 @@+{-# LANGUAGE TypeFamilies, TypeOperators, TemplateHaskell,+  UndecidableInstances, EmptyDataDecls #-}++module Data.Yoko.Representation where++import Data.Yoko.TypeBasics++++data U = U+newtype F a = F a+infixr 6 :*:+data a :*: b = a :*: b++data Void+newtype N a = N a+infixl 6 :+:+data a :+: b = L a | R b deriving (Eq, Show, Ord, Read)++++newtype Par1 f a = Par1 (f a)++++newtype Dep a = Dep a+newtype Rec a = Rec a++++type family Rep a++++class Generic a where rep :: a -> Rep a; obj :: Rep a -> a+++unDep (Dep x) = x++unRec (Rec x) = x+mapRec f (Rec x) = Rec (f x)++unPar1 (Par1 x) = x++unN (N x) = x+foldN f = f . unN++mapN f = N . foldN f++foldPlus f g x = case x of+  L x -> f x   ;   R x -> g x++mapPlus f g = foldPlus (L . f) (R . g)++mapTimes f g (a :*: b) = f a :*: g b++foldTimes comb f g (a :*: b) = comb (f a) (g b)++++type family DistMaybePlus a b+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+type instance Add Z m = m+type instance Add (S n) m = S (Add n m)++type family CountRs rep+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)++++++-- carrying around the original type supplants many ascriptions+newtype DCsOf t sum = DCsOf sum   ;   unDCsOf (DCsOf x) = x+instance Functor (DCsOf t) where fmap f = DCsOf . f . unDCsOf++infixl 6 |||+(|||) :: (DCsOf t sumL -> a) -> (DCsOf t sumR -> a) ->+         DCsOf t (sumL :+: sumR) -> a+(|||) f g = foldPlus f g . mapPlus DCsOf DCsOf . unDCsOf++++++concat `fmap` mapM derive [''Dep, ''Rec, ''U, ''(:*:), ''N, ''(:+:)]

@@ -0,0 +1,37 @@+{-# LANGUAGE TypeFamilies, UndecidableInstances, DataKinds, PolyKinds #-}++module Data.Yoko.TypeBasics (+  module Data.Yoko.MaybeKind,+  module Type.Booleans,+  Proxy(..),+  Equal,+  IsPrefixOf,+  derive, encode+  ) where++import Type.Booleans+import Data.Yoko.MaybeKind++--import Data.Proxy.TH (Proxy(..))+import Type.Spine+import Type.Ord (IsEQ)+import Type.Serialize+import Type.Ord.SpineSerialize (Compare)++++data Proxy a = Proxy++++type Equal a b = IsEQ (Compare a b)++++type family IsPrefixOf (pre :: *) (s :: *) :: * -- emulated primitive++++derive n = do+  d <- spineType n+  (d ++) `fmap` serializeTypeAsHash n

@@ -0,0 +1,115 @@+{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, TypeOperators,+  NoPolyKinds, DataKinds #-}++{-# LANGUAGE FlexibleInstances, FlexibleContexts, UndecidableInstances,+  ScopedTypeVariables, EmptyDataDecls #-}++{-# OPTIONS_GHC -fcontext-stack=250 #-}++module Data.Yoko.TypeSums (DistMaybePlus, (:-:),+                           Embed, embed, inject,+                           Partition, project, partition) where++import Data.Yoko.TypeBasics+import Data.Yoko.Representation++import Control.Arrow (left)++import Data.Yoko.TypeSumsAux (Partition_N(..))++++++class Embed sub sup where embed_ :: sub -> sup++embed :: Embed sub sup => sub -> sup+embed = embed_++inject :: Embed (N a) sum => a -> sum+inject = embed . N++++class Partition sup subL subR where partition_ :: sup -> Either subL subR++partition :: Partition sup sub (sup :-: sub) =>+             sup -> Either sub (sup :-: sub)+partition = partition_++project :: Partition sum (N a) (sum :-: N a) => sum -> Either a (sum :-: N a)+project = left unN . partition_++++++data Here a+data TurnLeft path+data TurnRight path++type family Locate a sum+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 Elem a sum = IsJust (Locate a sum)++++++class InjectAt path a sum where injectAt :: Proxy path -> a -> sum+instance InjectAt (Here a) a (N a) where injectAt _ = N+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+  injectAt _ = R . injectAt (Proxy :: Proxy path)++++++instance (Locate x sup ~ Just path, InjectAt path x sup) => Embed (N x) sup where+  embed_ = injectAt (Proxy :: Proxy path) . unN+instance (Embed l sup, Embed r sup) => Embed (l :+: r) sup where+  embed_ = foldPlus embed embed++++++infixl 6 :-:+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 instance Combine Void x = x+type instance Combine (N x) Void = N x+type instance Combine (N x) (N y) = N x :+: N y +type instance Combine (N x) (l :+: r) = N x :+: (l :+: r)+type instance Combine (l :+: r) Void = l :+: r+type instance Combine (l :+: r) (N y) = (l :+: r) :+: N y+type instance Combine (ll :+: rl) (lr :+: rr) = (ll :+: rl) :+: (lr :+: rr)+++++instance (Partition_N (Elem x subL) x subL subR+         ) => Partition (N x) subL subR where+  partition_ = partition_N (Proxy :: Proxy (Elem x subL))++instance (Partition a subL subR, Partition b subL subR+         ) => Partition (a :+: b) subL subR where+  partition_ = foldPlus partition_ partition_++++instance Embed (N 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+  partition_N _ = Left  . embed

@@ -0,0 +1,12 @@+{-# LANGUAGE MultiParamTypeClasses, KindSignatures #-}++module Data.Yoko.TypeSumsAux where++import Data.Yoko.TypeBasics+import Data.Yoko.Representation++++-- this * is Bool, ideally+class Partition_N (bn :: *) x subL subR where+  partition_N :: Proxy bn -> N x -> Either subL subR

@@ -1,6 +0,0 @@-module Examples.Ex where--data Tree1 a = Leaf a | Branch (Tree1 a) (Tree1 a)--data Even a = Zero | Even a (Odd a)-data Odd  a = Odd a (Even a)

@@ -1,60 +0,0 @@-{-# LANGUAGE EmptyDataDecls, TypeFamilies, TemplateHaskell, FlexibleInstances, TypeOperators, MultiParamTypeClasses, GADTs, UndecidableInstances #-}--{-# OPTIONS_GHC -fcontext-stack=50 #-}--module Examples.ExG where--import qualified Examples.Ex as Ex-import Examples.ReflectAux----data Leaf a; data Branch a--data Zero a; data Even a; data Odd a--concat `fmap` mapM derive-  [''Ex.Tree1, ''Leaf, ''Branch,-   ''Ex.Even, ''Zero, ''Even,-   ''Ex.Odd, ''Odd]--type instance Tag (Leaf a) = $(return $ encode "Leaf")-newtype instance RM m (N (Leaf a)) = Leaf a-instance (True ~ IsEQ (Compare a a)) => DC (Leaf a) where-  occName _ = "Leaf"-  type Range (Leaf a) = Ex.Tree1 a-  fr ~(Leaf a) = Ex.Leaf a-type instance Rep (Leaf a) = D a-instance Generic (Leaf a) where-  rep ~(Leaf a) = D a-  obj ~(D a) = Leaf a--type instance Tag (Branch a) = $(return $ encode "Branch")-data instance RM m (N (Branch a)) =-  Branch (Med m (Ex.Tree1 a)) (Med m (Ex.Tree1 a))-instance (True ~ IsEQ (Compare a a)) => DC (Branch a) where-  occName _ = "Branch"-  type Range (Branch a) = Ex.Tree1 a-  fr ~(Branch a b) = Ex.Branch a b-type instance Rep (Branch a) = R (Ex.Tree1 a) :* R (Ex.Tree1 a)-instance Generic (Branch a) where-  rep ~(Branch a b) = FF (R a, R b)-  obj ~(FF (R a, R b)) = Branch a b--type instance Inhabitants (DCU (Ex.Tree1 a)) = N (Leaf a) :+ N (Branch a)-instance (True ~ IsEQ (Compare a a)) => DT (Ex.Tree1 a) where-  packageName _ = "yoko-0.1"-  moduleName _ = "Examples.ExG"-  type Siblings (Ex.Tree1 a) = N (Ex.Tree1 a)-  data DCU (Ex.Tree1 a) dc where-    Leaf_ :: DCU (Ex.Tree1 a) (Leaf a)-    Branch_ :: DCU (Ex.Tree1 a) (Branch a)-  disband (Ex.Leaf a) = disbanded $ Leaf a-  disband (Ex.Branch a b) = disbanded $ Branch a b-instance Finite (DCU (Ex.Tree1 a)) where-  toUni x = Uni $ case x of-    Leaf_ -> OnLeft $ Here Refl-    Branch_ -> OnRight $ Here Refl-instance (a ~ b) => (Leaf b) ::: DCU (Ex.Tree1 a) where inhabits = Leaf_-instance (a ~ b) => (Branch b) ::: DCU (Ex.Tree1 a) where inhabits = Branch_-instance EqT (DCU (Ex.Tree1 a)) where eqT = eqTFin

@@ -1,8 +0,0 @@-module Examples.InnerBase where--import Examples.TermBase (Type(..))--data Inner = Lam Type Inner-           | Var Int-           | App Inner Inner-  deriving Show

@@ -1,90 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, EmptyDataDecls #-}--{-# OPTIONS_GHC -fcontext-stack=250 #-}--{- |--Module      :  Examples.InnerGeneric-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The declaration that hook 'Examples.InnerBase.Inner' into @yoko@. This will-eventually be generated via Template Haskell.---}-module Examples.InnerGeneric where--import qualified Examples.TermBase as B-import Examples.InnerBase (Inner)-import qualified Examples.InnerBase as I--import Examples.ReflectAux--data Lam; data Var; data App--concat `fmap` mapM derive [''Inner, ''Lam, ''Var, ''App]--type instance Tag Lam = $(return $ encode "Lam")-type instance Recurs Lam = N Inner-instance DC Lam where-  occName _ = "Lam"-  type Range Lam = Inner-  fr ~(Lam ty tm) = I.Lam ty tm-data instance RM m (N Lam) = Lam B.Type (Med m Inner)-type instance Tag Var = $(return $ encode "Var")-type instance Recurs Var = V-instance DC Var where-  occName _ = "Var"-  type Range Var = Inner-  fr ~(Var i) = I.Var i-data instance RM m (N Var) = Var Int-type instance Tag App = $(return $ encode "App")-type instance Recurs App = N Inner-instance DC App where-  occName _ = "App"-  type Range App = Inner-  fr ~(App tm0 tm1) = I.App tm0 tm1-data instance RM m (N App) = App (Med m Inner) (Med m Inner)-instance DT Inner where-  packageName _ = "datatype-reflect"-  moduleName _ = "InnerBase"-  type Siblings Inner = N Inner-  data DCU Inner dc where-    Lam_ :: DCU Inner Lam; Var_ :: DCU Inner Var-    App_ :: DCU Inner App-  disband (I.Lam ty tm)   = disbanded $ Lam ty tm-  disband (I.Var i)       = disbanded $ Var i-  disband (I.App tm0 tm1) = disbanded $ App tm0 tm1-type instance Inhabitants (DCU Inner) = (N Lam :+ N Var) :+ N App-instance Finite (DCU Inner) where-  toUni Lam_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits-instance Etinif (DCU Inner) where-  frUni (Uni x) = case x of-    (OnLeft  (OnLeft  (Here Refl))) -> Lam_-    (OnLeft  (OnRight (Here Refl))) -> Var_-    (OnRight (Here Refl))  -> App_-instance (t ::: Uni (DCs Inner)) => t ::: DCU Inner where-  inhabits = frUni inhabits-instance EqT (DCU Inner) where eqT = eqTFin-----type instance Rep Var = D Int-instance Generic Var where-  rep ~(Var i) = D i-  obj ~(D i) = Var i-type instance Rep Lam = D B.Type :* R Inner-instance Generic Lam where-  rep ~(Lam ty tm) = FF (D ty, R tm)-  obj ~(FF (D ty, R tm)) = Lam ty tm-type instance Rep App = R Inner :* R Inner-instance Generic App where-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1

@@ -1,63 +0,0 @@-{-# LANGUAGE TypeOperators, TypeFamilies, MultiParamTypeClasses,-  FlexibleInstances, UndecidableInstances #-}--{-# OPTIONS_GHC -fcontext-stack=200 #-}--module Examples.LL where--import qualified Examples.InnerBase as I--import qualified Data.Set as Set-import qualified Data.IntMap as IM--import Examples.LLBasics--import qualified Examples.InnerGeneric as IG-import qualified Examples.LLGeneric ()--import Data.Yoko------lambdaLift :: Inner -> [Type] -> Prog-lambdaLift x e = Prog (reverse tlds) main where-  (main, tlds) = runMnd (ll x) (e, IM.empty, 0)--llLam (IG.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where-  updE (rho, rn) = (ty : rho, support `prepend` rn) where-    support =-      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm-llVar (IG.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i------------------------------------------ default-ll :: Inner -> Mnd Term; ll = applyA (LL :: LL IdM Inner)--data LL m t = LL; type instance Idiom (LL m) = Mnd-type instance Unwrap (LL m) t = LL m t-instance Wrapper (LL m) where wrap = id; unwrap = id--type instance Dom (LL m) t = Med m t-type instance Rng (LL m) t = Med m (TApp (LL m) t)-type instance TApp (LL m) Inner = Term -- instance for each type in binding group--instance (IdM ~ m) => Inner ::: DomainA (LL m) where-  inhabits = AppABy $ \_ -> dcDispatch $-    eachOrNT (oneF (RMNTo llLam) ||. llVar) $ NT $ imageInDTAU LL---  eachOrNT (one_ [qP|RMNTo m (Mnd Term) :: *->*|] llLam ||. llVar) $ NT $ imageInDTAU LL------env0 = [TBool, TBool, TArrow TInt TInt, TInt]-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0-ex1 = ex0 `I.App` I.Var 3-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`-      (I.Lam (TArrow TInt TInt) $ I.Var 0)---- *LL> lambdaLift ex1 env0--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))---      ] (App (App (DVar 0) (Var 2)) (Var 3))

@@ -1,57 +0,0 @@------module Examples.LL0 where--import qualified Examples.InnerBase as I--import qualified Data.Set as Set-import qualified Data.IntMap as IM--import Examples.LLBasics-----------lambdaLift :: Inner -> [Type] -> Prog-lambdaLift x e = Prog (reverse tlds) main where-  (main, tlds) = runMnd (ll x) (e, IM.empty, 0)--ll (I.Lam ty tm) = newTLD ty (fvs tm) $ local updE $ ll tm where-  updE (rho, rn) = (ty : rho, support `prepend` rn) where-    support =-      IM.fromDistinctAscList . flip zip [0..] . Set.toAscList . fvs $ tm-ll (I.Var i) = asks $ \(_, rn) -> Var $ lookupRN rn i------------------------------------------ default-ll (I.App tm1 tm2) = App <$> ll tm1 <*> ll tm2- ------------env0 = [TBool, TBool, TArrow TInt TInt, TInt]-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0-ex1 = ex0 `I.App` I.Var 3-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`-      (I.Lam (TArrow TInt TInt) $ I.Var 0)---- *LL> lambdaLift ex1 env0--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))---      ] (App (App (DVar 0) (Var 2)) (Var 3))

@@ -1,13 +0,0 @@-module Examples.LLBase where--import Examples.TermBase (Type(..))----data Term = DVar Int | Var Int | App Term Term-  deriving Show--type TLD = ([Type], Type, Term)--data Prog = Prog [TLD] Term-  deriving Show

@@ -1,71 +0,0 @@-{-# LANGUAGE FlexibleInstances, TypeOperators, MultiParamTypeClasses,-  TypeFamilies, UndecidableInstances #-}--module Examples.LLBasics-  (module Examples.LLBasics, module Examples.TermBase,-   module Examples.InnerBase, module Examples.LLBase,-   local, asks, (<$>), (<*>)) where--import Examples.TermBase (Type(..))-import Examples.InnerBase (Inner)-import qualified Examples.InnerBase as I-import Examples.LLBase--import qualified Control.Arrow as Arrow-import qualified Data.Set as Set; import Data.Set (Set)-import qualified Data.IntMap as IM; import Data.IntMap (IntMap)-import Data.Maybe (fromMaybe)--import Control.Monad.Reader.Class (MonadReader(..), asks)-import Control.Monad (ap)-import Control.Applicative (Applicative(pure, (<*>)), (<$>))----type Frees = Set Int; type Rename = IntMap Int--bump :: Frees -> Frees-bump = Set.map (subtract 1) . Set.filter (> 0)--lookupRN :: Rename -> Int -> Int-lookupRN rn i = fromMaybe i $ IM.lookup i rn--prepend :: Rename -> Rename -> Rename-prepend f = IM.unionWith const f .-            IM.fromDistinctAscList . map ((+ 1) Arrow.*** (+ 1)) . IM.toAscList----fvs :: Inner -> Frees-fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm-fvs (I.Var i) = Set.singleton i-fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2----newtype Mnd a = Mnd {runMnd :: ([Type], Rename, Int) -> (a, [TLD])}-instance Functor Mnd where fmap f = (>>= return . f)-instance Applicative Mnd where pure = return; (<*>) = ap-instance Monad Mnd where-  return a = Mnd $ \_ -> (a, [])-  m >>= k = Mnd $ \e@(tys, rn, sh) -> case runMnd m e of-    ~(a, w) -> Arrow.second (w ++) $ runMnd (k a) (tys, rn, sh + length w)-instance (e ~ ([Type], Rename)) => MonadReader e Mnd where-  ask = Mnd $ \ ~(x, y, _) -> ((x, y), []);-  local f (Mnd g) =-    Mnd $ \ ~(x, y, z) -> case f (x, y) of-      ~(x', y') -> g (x', y', z)--numEmissions :: Mnd Int-numEmissions = Mnd $ \ ~(_, _, z) -> (z, [])--emit :: [TLD] -> Mnd ()-emit w = Mnd $ \_ -> ((), w)--newTLD :: Type -> Frees -> Mnd Term -> Mnd Term--- NB could check if such a TLD already exists-newTLD ty fvs m = do-  (rho, rn) <- ask; sh <- numEmissions-  let fvs' = reverse $ Set.toAscList $ bump fvs-  m >>= \tm -> emit [(map (rho !!) fvs', ty, tm)]-  return $ foldl ((. Var . lookupRN rn) . App) (DVar sh) fvs'

@@ -1,81 +0,0 @@-{- |--Module      :  Examples.LLDirect-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Lambda-lifts 'Examples.InnerBase.Inner' to 'Examples.LLBase.LL' without using-@yoko@. Compare to "Examples.LL0" and "Examples.LL".---}-module Examples.LLDirect where--import Examples.TermBase (Type(..))-import Examples.InnerBase (Inner)-import qualified Examples.InnerBase as I-import Examples.LLBase--import qualified Data.Set as Set; import Data.Set (Set)-import qualified Data.IntMap as IM; import Data.IntMap (IntMap)----fvs :: Inner -> Set Int-fvs (I.Lam ty tm) = Set.map (subtract 1) $ Set.filter (> 0) $ fvs tm-fvs (I.Var i) = Set.singleton i-fvs (I.App tm1 tm2) = fvs tm1 `Set.union` fvs tm2--bump :: Set Int -> Set Int-bump = Set.map (subtract 1) . Set.filter (> 0)--renm :: IntMap Int -> Int -> Term -> Term-renm m dv tm@(Var i) = maybe tm Var $ IM.lookup i m-renm m dv (App tm1 tm2) = App (renm m dv tm1) (renm m dv tm2)-renm _ dv (DVar i) = DVar (i + dv)--renmP :: IntMap Int -> Int -> Prog -> Prog-renmP m dv (Prog tlds main) = Prog (map each tlds) (renm m dv main) where-  each (tys, ty, tm) = (tys, ty, renm m dv tm)-----type Env = [Type]--lambdaLift :: Inner -> Env -> Prog-lambdaLift (I.Lam ty tm) rho = newTLD ty rho (fvs tm) $ lambdaLift tm (ty : rho)-lambdaLift (I.Var i) rho = Prog [] $ Var i-lambdaLift (I.App tm1 tm2) rho = Prog (tlds1 ++ tlds2) $ App main1 main2 where-  Prog tlds1 main1 = lambdaLift tm1 rho-  Prog tlds2 main2 = renmP IM.empty (length tlds1) $ lambdaLift tm2 rho----newTLD :: Type -> Env -> Set Int -> Prog -> Prog--- NB could check if such a TLD already exists; lambdaLift@I.App would need to handle--- that too-newTLD ty rho fvs (Prog tlds main) =-  Prog ((map (rho !!) fvs', ty, renm rn 0 main) : tlds) $-  foldl ((. Var) . App) (DVar 0) fvs'-  where rn = IM.fromDistinctAscList $ zip (Set.toAscList fvs) [0..]-        fvs' = reverse $ Set.toAscList $ bump fvs------env0 = [TBool, TBool, TArrow TInt TInt, TInt]-ex0 = I.Lam TInt $ I.Lam TInt $ I.Var 4 `I.App` I.Var 1 `I.App` I.Var 0-ex1 = ex0 `I.App` I.Var 3-ex2 = (I.Lam (TArrow TInt TInt `TArrow` TArrow TInt TInt) $ I.Var 0) `I.App`-      (I.Lam (TArrow TInt TInt) $ I.Var 0)----- *LL> ll ex1 env0--- Prog [([TArrow TInt TInt],TInt,App (App (DVar 0) (Var 1)) (Var 0)),---       ([TArrow TInt TInt,TInt],TInt,App (App (Var 2) (Var 1)) (Var 0))---      ] (App (App (DVar 0) (Var 2)) (Var 3))

@@ -1,89 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, EmptyDataDecls #-}--{-# OPTIONS_GHC -fcontext-stack=250 #-}--{- |--Module      :  Examples.LLGeneric-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The declaration that hook 'Examples.LLBase.Term' into @yoko@. This will-eventually be generated via Template Haskell.---}-module Examples.LLGeneric where--import Examples.LLBase (Term)-import qualified Examples.LLBase as B--import Examples.ReflectAux--data DVar; data Var; data App--concat `fmap` mapM derive [''Term, ''DVar, ''Var, ''App]--type instance Tag DVar = $(return $ encode "DVar")-type instance Recurs DVar = V-instance DC DVar where-  occName _ = "DVar"-  type Range DVar = Term-  fr ~(DVar i) = B.DVar i-data instance RM m (N DVar) = DVar Int-type instance Tag Var = $(return $ encode "Var")-type instance Recurs Var = V-instance DC Var where-  occName _ = "Var"-  type Range Var = Term-  fr ~(Var i) = B.Var i-data instance RM m (N Var) = Var Int-type instance Tag App = $(return $ encode "App")-type instance Recurs App = N Term-instance DC App where-  occName _ = "App"-  type Range App = Term-  fr ~(App tm0 tm1) = B.App tm0 tm1-data instance RM m (N App) = App (Med m Term) (Med m Term)-instance DT Term where-  packageName _ = "datatype-reflect"-  moduleName _ = "TermBase"-  type Siblings Term = N Term-  data DCU Term dc where-    DVar_ :: DCU Term DVar; Var_ :: DCU Term Var-    App_ :: DCU Term App-  disband (B.DVar i)      = disbanded $ DVar i-  disband (B.Var i)       = disbanded $ Var i-  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1-type instance Inhabitants (DCU Term) = (N DVar :+ N Var) :+ N App-instance Finite (DCU Term) where-  toUni DVar_ = inhabits; toUni Var_ = inhabits; toUni App_ = inhabits-instance Etinif (DCU Term) where-  frUni (Uni x) = case x of-    (OnLeft  (OnLeft  (Here Refl))) -> DVar_-    (OnLeft  (OnRight (Here Refl))) -> Var_-    (OnRight (Here Refl))  -> App_-instance (t ::: Uni (DCs Term)) => t ::: DCU Term where-  inhabits = frUni inhabits-instance EqT (DCU Term) where eqT = eqTFin-----type instance Rep DVar = D Int-instance Generic DVar where-  rep ~(DVar i) = D i-  obj ~(D i) = DVar i-type instance Rep Var = D Int-instance Generic Var where-  rep ~(Var i) = D i-  obj ~(D i) = Var i-type instance Rep App = R Term :* R Term-instance Generic App where-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1

@@ -1,25 +0,0 @@-{- |--Module      :  Examples.Main-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Just bundles up the three examples.---}-module Main where--import Examples.TermTest-import Examples.TermInner-import Examples.LL----main = do-  print $ Examples.TermTest.ex1-  print $ Examples.TermInner.ex1-  print $ lambdaLift Examples.LL.ex1 env0

@@ -1,19 +0,0 @@-{- |--Module      :  Examples.ReflectAux-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Just bundles up some imports for the various @*Generic@ modules.---}-module Examples.ReflectAux (encode, module Data.Yoko, DCU) where--import Type.Serialize--import Data.Yoko hiding (qK)-import Data.Yoko.ReflectBase (DCU)

@@ -1,24 +0,0 @@-{- |--Module      :  Examples.TermBase-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)---}-module Examples.TermBase where--data Type = TBool | TInt | TArrow Type Type-  deriving Show--data Term = Lam Type Term-          | Var Int-          | App Term Term-          | Let [Decl] Term-  deriving Show--data Decl = Decl Type Term-  deriving Show

@@ -1,190 +0,0 @@-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators, GADTs,-  FlexibleInstances, MultiParamTypeClasses, FlexibleContexts, UndecidableInstances,-  TypeSynonymInstances, EmptyDataDecls #-}--{-# OPTIONS_GHC -fcontext-stack=250 #-}--{- |--Module      :  Examples.TermGeneric-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The declaration that hook 'Examples.TermBase.Type', 'Examples.TermBase.Term',-and 'Examples.TermBase.Decl' into @yoko@. This will eventually be generated via-Template Haskell.---}-module Examples.TermGeneric where--import qualified Examples.TermBase as B--import Examples.ReflectAux--data TBool; data TInt; data TArrow-data Lam; data Var; data App; data Let-data Decl--concat `fmap` mapM derive-  [''B.Type, ''TBool, ''TInt, ''TArrow,-   ''B.Term, ''Lam, ''Var, ''App, ''Let,-   ''B.Decl, ''Decl]--type instance Tag TBool = $(return $ encode "TBool")-type instance Recurs TBool = U-instance DC TBool where-  occName _ = "TBool"-  type Range TBool = B.Type-  fr _ = B.TBool-data instance RM m (N TBool) = TBool-type instance Tag TInt = $(return $ encode "TInt")-type instance Recurs TInt = U-instance DC TInt where-  occName _ = "TInt"-  type Range TInt = B.Type-  fr _ = B.TInt-data instance RM m (N TInt) = TInt-type instance Tag TArrow = $(return $ encode "TArrow")-type instance Recurs TArrow = N B.Type-instance DC TArrow where-  occName _ = "TArrow"-  type Range TArrow = B.Type-  fr ~(TArrow d r) = B.TArrow d r-data instance RM m (N TArrow) = TArrow (Med m B.Type) (Med m B.Type)-instance DT B.Type where-  packageName _ = "datatype-reflect"-  moduleName _ = "TermBase"-  type Siblings B.Type = N B.Type-  data DCU B.Type dc where-    TBool_ :: DCU B.Type TBool; TInt_ :: DCU B.Type TInt-    TArrow_ :: DCU B.Type TArrow-  disband B.TBool        = disbanded TBool-  disband B.TInt         = disbanded TInt-  disband (B.TArrow d r) = disbanded $ TArrow d r-type instance Inhabitants (DCU B.Type) = N TBool :+ N TInt :+ N TArrow-instance Finite (DCU B.Type) where-  toUni TBool_ = inhabits; toUni TInt_ = inhabits; toUni TArrow_ = inhabits-instance Etinif (DCU B.Type) where-  frUni (Uni x) = case x of-    (OnLeft          (Here Refl)) -> TBool_-    (OnRight (OnLeft  (Here Refl))) -> TInt_-    (OnRight (OnRight (Here Refl))) -> TArrow_-instance (t ::: Uni (DCs B.Type)) => t ::: DCU B.Type where-  inhabits = frUni inhabits-instance EqT (DCU B.Type) where eqT = eqTFin--type instance Tag Lam = $(return $ encode "Lam")-type instance Recurs Lam = N B.Term-instance DC Lam where-  occName _ = "Lam"-  type Range Lam = B.Term-  fr ~(Lam ty tm) = B.Lam ty tm-data instance RM m (N Lam) = Lam B.Type (Med m B.Term)-type instance Tag Var = $(return $ encode "Var")-type instance Recurs Var = U-instance DC Var where-  occName _ = "Var"-  type Range Var = B.Term-  fr ~(Var i) = B.Var i-data instance RM m (N Var) = Var Int-type instance Tag App = $(return $ encode "App")-type instance Recurs App = N B.Term-instance DC App where-  occName _ = "App"-  type Range App = B.Term-  fr ~(App tm0 tm1) = B.App tm0 tm1-data instance RM m (N App) = App (Med m B.Term) (Med m B.Term)-type instance Tag Let = $(return $ encode "Let")-type instance Recurs Let = N B.Decl :+ N B.Term-instance DC Let where-  occName _ = "Let"-  type Range Let = B.Term-  fr ~(Let ds tm) = B.Let ds tm-data instance RM m (N Let) = Let [Med m B.Decl] (Med m B.Term)-instance DT B.Term where-  packageName _ = "datatype-reflect"-  moduleName _ = "TermBase"-  type Siblings B.Term = N B.Term :+ N B.Decl-  data DCU B.Term dc where-    Lam_ :: DCU B.Term Lam; Var_ :: DCU B.Term Var-    App_ :: DCU B.Term App; Let_ :: DCU B.Term Let-  disband (B.Lam ty tm)   = disbanded $ Lam ty tm-  disband (B.Var i)       = disbanded $ Var i-  disband (B.App tm0 tm1) = disbanded $ App tm0 tm1-  disband (B.Let ds tm)   = disbanded $ Let ds tm-type instance Inhabitants (DCU B.Term) = (N Lam :+ N Var) :+ (N App :+ N Let)-instance Finite (DCU B.Term) where-  toUni Lam_ = inhabits; toUni Var_ = inhabits-  toUni App_ = inhabits; toUni Let_ = inhabits-instance Etinif (DCU B.Term) where-  frUni (Uni x) = case x of-    (OnLeft  (OnLeft (Here Refl))) -> Lam_-    (OnLeft  (OnRight (Here Refl))) -> Var_-    (OnRight (OnLeft (Here Refl))) -> App_-    (OnRight (OnRight (Here Refl))) -> Let_-instance (t ::: Uni (DCs B.Term)) => t ::: DCU B.Term where-  inhabits = frUni inhabits-instance EqT (DCU B.Term) where eqT = eqTFin--type instance Tag Decl = $(return $ encode "Decl")-type instance Recurs Decl = N B.Term-instance DC Decl where-  occName _ = "Decl"-  type Range Decl = B.Decl-  to = Just . uniqueDC; fr ~(Decl ds tm) = B.Decl ds tm-data instance RM m (N Decl) = Decl B.Type (Med m B.Term)-instance DT B.Decl where-  packageName _ = "datatype-reflect"-  moduleName _ = "DeclBase"-  type Siblings B.Decl = N B.Term :+ N B.Decl-  data DCU B.Decl dc where Decl_ :: DCU B.Decl Decl-  disband ~(B.Decl ty tm) = disbanded $ Decl ty tm-type instance Inhabitants (DCU B.Decl) = N Decl-instance Finite (DCU B.Decl) where-  toUni Decl_ = inhabits-instance Etinif (DCU B.Decl) where-  frUni (Uni (Here Refl)) = Decl_-instance (t ::: Uni (DCs B.Decl)) => t ::: DCU B.Decl where-  inhabits = frUni inhabits-instance EqT (DCU B.Decl) where eqT = eqTFin----type instance Rep TBool = V-instance Generic TBool where-  rep _ = void "rep[TBool]"-  obj _ = TBool-type instance Rep TInt = V-instance Generic TInt where-  rep _ = void "rep[TInt]"-  obj _ = TInt-type instance Rep TArrow = R B.Type :* R B.Type-instance Generic TArrow where-  rep ~(TArrow ty0 ty1) = FF (R ty0, R ty1)-  obj ~(FF (R ty0, R ty1)) = TArrow ty0 ty1--type instance Rep Var = D Int-instance Generic Var where-  rep ~(Var i) = D i-  obj ~(D i) = Var i-type instance Rep Lam = D B.Type :* R B.Term-instance Generic Lam where-  rep ~(Lam ty tm) = FF (D ty, R tm)-  obj ~(FF (D ty, R tm)) = Lam ty tm-type instance Rep App = R B.Term :* R B.Term-instance Generic App where-  rep ~(App tm0 tm1) = FF (R tm0, R tm1)-  obj ~(FF (R tm0, R tm1)) = App tm0 tm1-type instance Rep Let = F [] (R B.Decl) :* R B.Term-instance Generic Let where-  rep ~(Let ds tm) = FF (F (map R ds), R tm)-  obj ~(FF (F rds, R tm)) = Let (map unR rds) tm--type instance Rep Decl = D B.Type :* R B.Term-instance Generic Decl where-  rep ~(Decl ty tm) = FF (D ty, R tm)-  obj ~(FF (D ty, R tm)) = Decl ty tm

@@ -1,60 +0,0 @@-{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, FlexibleInstances,-  UndecidableInstances #-}--{-# OPTIONS_GHC -fcontext-stack=200 #-}--{- |--Module      :  Examples.TermInner-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--A let-elaboration via "Data.Yoko.InDT".---}-module Examples.TermInner where--import Examples.TermBase-import Examples.InnerBase (Inner)-import qualified Examples.InnerBase as I-import qualified Examples.TermGeneric as G-import Examples.InnerGeneric ()--import Type.Yoko--import Data.Yoko.InDT-import Data.Yoko.Reflect------elaborate :: Term -> Inner; elaborate = apply (Elab :: Elab IdM Term)--data Elab m t = Elab-type instance Unwrap (Elab m) t = Elab m t-instance Wrapper (Elab m) where wrap = id; unwrap = id--type instance Dom (Elab m) t = Med m t-type instance Rng (Elab m) t = Med m (TApp (Elab m) t)--type instance TApp (Elab m) Term = Inner--instance (IdM ~ m) => Term ::: Domain (Elab m) where-  inhabits = AppBy $ \_ -> dcDispatch $-    eachOrNT (oneF $ RMNTo elab_Let) $ NT $ imageInDTU Elab--elab_Let (G.Let ds tm) =-  foldr (\(Decl ty tm) x -> I.Lam ty x `I.App` elaborate tm) (elaborate tm) ds------ex0 = Let [Decl TInt (Var 111), Decl TBool (Var 222)] (Var 0)--ex1 = elaborate ex0

@@ -1,93 +0,0 @@-{-# LANGUAGE QuasiQuotes, TypeFamilies, FlexibleInstances,-  MultiParamTypeClasses, GADTs, PatternGuards #-}--{-# OPTIONS_GHC -fcontext-stack=200 #-}--{- |--Module      :  Examples.TermTest-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--A denotational semantics for the simple-typed lambda calculus via-"Data.Yoko.Cata".---}-module Examples.TermTest where--import Examples.TermBase-import qualified Examples.TermGeneric as G--import Type.Yoko-import Data.Yoko.Cata-import Data.Yoko----- | Since our family of abstract data types don't correspond to the--- object-language types, we need a tagged universal value space.-data Val = VBool Bool | VInt Int | VFun (Val -> Val)-instance Show Val where-  show (VBool b) = show b; show (VInt i) = show i; show (VFun _) = "<fun>"----eLam (G.Lam _ t) e = VFun $ t . (: e)-eVar (G.Var i) = (!! i)-eApp (G.App t1 t2) e-  | VFun f <- t1 e = f (t2 e)-  | otherwise = error "failed projection in reduce[App]"-eLet (G.Let ds t) = foldr cons t ds where cons (_, s) t e = t (s e : e)--eDecl (G.Decl ty t) = (ty, t)----- | The semantic domain of the reduction.-type Sem = [Val] -> Val---- | The recursion mediator for our denotation.-data SemM = SemM-type instance Med SemM Term = Sem-type instance Med SemM Decl = (Type, Sem)--instance AlgebraDT SemM Term where algebraDT = algebraFin-instance AlgebraDC SemM G.Lam where algebraDC = eLam-instance AlgebraDC SemM G.Var where algebraDC = eVar-instance AlgebraDC SemM G.App where algebraDC = eApp-instance AlgebraDC SemM G.Let where algebraDC = eLet--instance AlgebraDT SemM Decl where algebraDT = eDecl . uniqueRMN---- | 'eval' will work for any family of mutually recursive types that all have--- @'AlgebraDT' SemM@ instances.-eval x = ($ x) $ cata $ algebras [qP|SemM|]--eval'     x = ($ x) $ cata $ (algebraDT  .|. algebraDT :: SiblingAlgs Term SemM)-eval''    x = ($ x) $ cata $ (algebraDT  .|. algebraDT)-eval'''   x = ($ x) $ cata $ (algebraFin .|. algebraDT :: SiblingAlgs Term SemM)-eval''''  x = ($ x) $ cata $ (algebraFin .|. algebraDT)-eval''''' x = ($ x) $ cata $ (algebraDT  .|. (eDecl . uniqueRMN'))----instance AlgebraDT SemM Decl where algebraDT = algebraFin---instance AlgebraDC SemM G.Decl where algebraDC = eDecl---eval''''' x = ($ x) $ cata $ (algebraFin .|. algebraFin :: SiblingAlgs Term SemM)------vSucc = VFun $ \(VInt i) -> VInt $ i + 1---ex0 = eval (Var 0) [VBool True]-ex1 = eval (Let [Decl (TInt `TArrow` TInt) $ Lam TInt (Var 0) `App` Var 0 `App` Var 1]-                (Var 0)) [vSucc, VInt 9]-ex2' = eval (Decl TInt (Var 0))-ex2 = snd ex2' [VInt 3]-----ex1' = eval' (Let [Decl (TInt `TArrow` TInt) (Var 0 `App` Var 1)]---                (Var 0)) [vSucc, VInt 9]

@@ -0,0 +1,21 @@+{-# LANGUAGE TypeFamilies, TemplateHaskell #-}++{-# OPTIONS_GHC -ddump-splices #-}++module Test where++import Data.Yoko+import Type.Ord.SpineSerialize (Compare)+++data T a = T a++data X = X+++concat `fmap` mapM derive [''T, ''X]++++test :: (() ~ Compare a b) => a -> b -> ()+test _ _ = ()

@@ -1,1 +1,1 @@-See the documentation at http://code.google.com/p/yoko+Read the paper at http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf

@@ -1,36 +0,0 @@-{- |--Module      :  Type.Yoko-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)---}--module Type.Yoko (-  module Type.Yoko.Type,-  module Type.Yoko.Universe,-  module Type.Yoko.Natural,-  module Type.Yoko.BTree,-  module Type.Yoko.Sum,-  module Type.Yoko.TSTSS,-  module Type.Yoko.Fun,-  module Type.Yoko.FunA,-  module Type.Yoko.MFun,-  module Type.Yoko.TFunA-  ) where--import Type.Yoko.Type-import Type.Yoko.Universe-import Type.Yoko.Natural-import Type.Yoko.BTree-import Type.Yoko.Sum-import Type.Yoko.TSTSS--import Type.Yoko.Fun-import Type.Yoko.FunA-import Type.Yoko.MFun-import Type.Yoko.TFunA

@@ -1,194 +0,0 @@-{-# LANGUAGE TypeFamilies, ScopedTypeVariables, QuasiQuotes, Rank2Types,-  GADTs, MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,-  UndecidableInstances, EmptyDataDecls, TypeOperators #-}--{-# LANGUAGE TemplateHaskell #-}--{- |--Module      :  Type.Yoko.BTree-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Operators for the type-sums from "Type.Yoko.Sum".---}--module Type.Yoko.BTree where--import Type.Yoko.Type-import Type.Yoko.Universe-import Type.Yoko.Natural-import Data.Yoko.Core-import Type.Yoko.Sum-------- | @Inu t@ is a universe of type-sums containing @t@.-type Inu t = Exists ((:=:) t)---- | @Uni ts@ is a universe containing the types in the type-sum @ts@.-newtype Uni ts t = Uni (Inu t ts)--instance (ts ::: Inu t) => t ::: Uni ts where inhabits = Uni inhabits--type instance Pred (Uni ts) t = Elem t ts--instance EqT (Uni ts) where-  eqT (Uni u) (Uni v) = w u v where-    w :: forall ts a b. Inu a ts -> Inu b ts -> Maybe (a :=: b)-    w (Here Refl) (Here Refl) = Just Refl-    w (OnLeft u) (OnLeft v) = w u v-    w (OnRight u) (OnRight v) = w u v-    w _ _ = Nothing -------- | A @Uni ts t@ value can also be understood in terms of more primitive--- universes, 'VoidU', @':=:'@ and @':||'@ for 'V', 'N', and @':+'@,--- respectively.-type family PrimUni ts :: * -> *-type instance PrimUni V = VoidU-type instance PrimUni (N t) = (:=:) t-type instance PrimUni (ts :+ us) = PrimUni ts :|| PrimUni us--primUni :: Uni ts t -> PrimUni ts t-primUni (Uni u) = w u where-  w :: Inu t ts -> PrimUni ts t-  w (Here Refl) = Refl-  w (OnLeft u) = LeftU $ w u-  w (OnRight v) = RightU $ w v--primUni1 :: Uni (ts :+ us) t -> (Uni ts :|| Uni us) t-primUni1 (Uni (OnLeft u)) = LeftU $ Uni u-primUni1 (Uni (OnRight v)) = RightU $ Uni v------- | Finite universes can be represented as type-sums.-type family Inhabitants u-class Finite u where-  toUni :: u t -> Uni (Inhabitants u) t--finiteNP :: Finite u => NP u f -> NP (Uni (Inhabitants u)) f-finiteNP = firstNP toUni---- | @frUni@ sometimes requires a stronger context than does @toUni@, so we--- separate the two methods.-class Finite u => Etinif u where frUni :: Uni (Inhabitants u) t -> u t---- | Any finite universe can be used to determine type equality.-eqTFin :: (Inhabitants u ~ Inhabitants v, Finite u, Finite v-          ) => u a -> v b -> Maybe (a :=: b)-eqTFin x y = eqT (toUni x) (toUni y)--type instance Inhabitants (Uni ts) = ts-instance Finite (Uni ts) where toUni = id-instance Finite (Uni ts) => Etinif (Uni ts) where frUni = id--type instance Inhabitants VoidU = V--type instance Inhabitants ((:=:) t) = N t-instance Finite ((:=:) t) where toUni Refl = Uni (Here Refl)-instance Etinif ((:=:) t) where frUni (Uni (Here Refl)) = Refl--type instance Inhabitants (u :|| v) = Inhabitants u :+ Inhabitants v-instance (Finite u, Finite v) => Finite (u :|| v) where-  toUni (LeftU u) = case toUni u of-    Uni x -> Uni $ OnLeft $ x-  toUni (RightU v) = case toUni v of-    Uni x -> Uni $ OnRight $ x-instance (Etinif u, Etinif v) => Etinif (u :|| v) where-  frUni uv = case primUni1 uv of-    LeftU u -> LeftU $ frUni u-    RightU v -> RightU $ frUni v----- | @Norm@ uses @NormW@ to remove duplicates from (i.e. /normalize/) a--- type-sum.-type family Norm c-type instance Norm V = V-type instance Norm (N t) = N t-type instance Norm (ts :+ us) = NormW (ts :+ us) V---- | @NormW@ combines two type-sums into a right-associated type-sum containing--- no duplicates.-type family NormW c acc-type instance NormW V acc = acc-type instance NormW (N t) acc = If (Elem t acc) acc (N t :+ acc)-type instance NormW (ts :+ us) acc = NormW ts (NormW us acc)------- | @Each ts f@ provides a @'NT' t f@ for each @t@ in the type-sum @ts@.-type Each ts = NT (Uni ts)--none :: String -> Each V f-none s = NT $ error $ "TypeBTree.none: " ++ s--one_ :: [qP|f :: *->*|] -> Unwrap f t -> Each (N t) f-one_ p x = firstNT primUni $ constNT_ p x--one :: Unwrap f t -> Each (N t) f-one = one_ Proxy--oneF :: Wrapper f => f t -> Each (N t) f-oneF x = firstNT primUni $ constNTF x--infixr 6 |||, .|.-both, (|||) :: Each ts f -> Each us f -> Each (ts :+ us) f-both f g = firstNT primUni1 $ orNT f g; (|||) = both--infixl 5 ||.; infixr 5 .||-(.|.) :: Wrapper f => Unwrap f t -> Unwrap f s -> Each (N t :+ N s) f-(||.) :: Wrapper f => Each ts f -> Unwrap f t -> Each (ts :+ N t) f-(.||) :: Wrapper f => Unwrap f t -> Each ts f -> Each (N t :+ ts) f-f .|. g = one f ||| one g; f ||. g = f ||| one g; f .|| g = one f ||| g------ | @each@ is the principal means of defining an @Each@ value.-each :: forall u v f. (Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->-        (forall a. u a -> Unwrap f a) -> NT v f-each _ = \fs -> firstNT toUni $ w inhabits fs where-  w :: forall ts. All u ts ->-       (forall a. (a ::: u) => u a -> Unwrap f a) -> Each ts f-  w SumV _ = none "TypeBTree.each"-  w (SumN u) fns = one $ fns u-  w (SumS c d) fns = w c fns `both` w d fns-  -eachF :: forall u v f. (Wrapper f, Inhabitants v ::: All u, Finite v) => [qP|u :: *->*|] ->-         (forall a. u a -> f a) -> NT v f-eachF p f = each p (unwrap . f)--eachF_ :: forall f v. (Wrapper f, Inhabitants v ::: All NoneU, Finite v) => (forall a. f a) -> NT v f-eachF_ f = eachF Proxy ((\NoneU -> f) :: forall a. NoneU a -> f a)------ | Just a specialization: @prjEach x f = 'appNT' f x@.-prjEach :: Uni ts t -> Each ts f -> Unwrap f t-prjEach x f = appNT f x--prjEachF :: Wrapper f => Uni ts t -> Each ts f -> f t-prjEachF = (wrap .) . prjEach------- | @eachOrNT fs gs@ builds an 'NT' that uses @fs@ for as many types in the--- universe @v@ as possible, and uses @gs@ for the rest. It's an extension of--- 'orNT' to @Each@.-eachOrNT :: forall u v f w.-  (Inhabitants v ::: All (u :|| w), Finite v) => NT u f -> NT w f -> NT v f-eachOrNT fs dflt = firstNT toUni $ each Proxy $ appNT $ orNT fs dflt

@@ -1,136 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleContexts, Rank2Types, QuasiQuotes,-  TypeOperators, ScopedTypeVariables, GADTs, FlexibleInstances,-  MultiParamTypeClasses, UndecidableInstances #-}--{- |--Module      :  Type.Yoko.Fun-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--An explicit perspective on (both parametric and ad-hoc) polymorphic-functions. The datatype representing such a function must be of kind @* -> *@;-the parameter is the type at which the function is to be instantiated.---}--module Type.Yoko.Fun-  (Domain(..), Dom, Rng, applyU, apply,-   YieldsArrowTSSU, DomF, RngF, eachArrow,-   AsComp(..), WrapComp, WrapCompF-  ) where--import Type.Yoko.Type-import Type.Yoko.Universe-import Type.Yoko.Natural-import Type.Yoko.Sum-import Type.Yoko.BTree------- | @Domain fn@ is the universe of types at which @fn@ can be applied; it's--- the type-level domain of @fn@.-newtype Domain fn t = AppBy (fn t -> Dom fn t -> Rng fn t)---- | @Dom fn t@ is the domain of @fn@ at type @t@; it's the term-level domain--- of @fn@ at @t@.-type family Dom (fn :: * -> *) t--- | @Rng fn t@ is the range of @fn@ at type @t@; it's the term-level range of--- @fn@ at @t@.-type family Rng (fn :: * -> *) t---- | @applyD@ is analogous to '$'.-applyU :: Domain fn t -> fn t -> Dom fn t -> Rng fn t-applyU (AppBy f) = f---- | @apply = applyU inhabits@.-apply :: (t ::: Domain fn) => fn t -> Dom fn t -> Rng fn t-apply = applyU inhabits------ | @YieldsArrowTSSU fn@ also gaurantees that @fn@ at @t@ yields a type of the--- shape @(DomF fn) t -> (RngF fn) t@; i.e. it guarantees that @Dom fn t@ and--- @Rng fn t@ both don't depend on @t@ and also are an application of a @* ->--- *@ to @t@.-data YieldsArrowTSSU fn t where-  YieldsArrowTSSU ::-    (Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t-    ) => Domain fn t -> YieldsArrowTSSU fn t-instance (t ::: Domain fn, Dom fn t ~ DomF fn t, Rng fn t ~ RngF fn t-         ) => t ::: YieldsArrowTSSU fn where inhabits = YieldsArrowTSSU inhabits---- | Used by @YieldsArrowTSSU fn@ to structure the domain of @fn@.-type family DomF (fn :: * -> *) :: * -> *--- | Used by @YieldsArrowTSSU fn@ to structure the range of @fn@.-type family RngF (fn :: * -> *) :: * -> *---- | Just a specialization: @yieldsArrowTSSU (YieldsArrowTSSU domD) fn = applyU domU fn@.-yieldsArrowTSSU :: YieldsArrowTSSU fn t -> (forall t. fn t) -> DomF fn t -> RngF fn t-yieldsArrowTSSU (YieldsArrowTSSU domU) fn = applyU domU fn---- | Defines an @'NT' u@ from a suitably polymorphic type-function @fn@ if @u@--- is finite and the function yields an arrow at each type in @u@.-eachArrow :: forall fn u.-  (Finite u, Inhabitants u ::: All (YieldsArrowTSSU fn)-  ) => (forall t. fn t) -> NT u (ArrowTSS (DomF fn) (RngF fn))-eachArrow fn = each [qP|YieldsArrowTSSU fn :: *->*|] $-  \d -> yieldsArrowTSSU d fn------type instance Dom (fn :. f) a = Dom fn (f a)-type instance Rng (fn :. f) a = Rng fn (f a)-type instance DomF (fn :. f) = DomF fn-type instance RngF (fn :. f) = RngF fn-instance (f t ::: Domain fn) => t ::: Domain (fn :. f) where-  inhabits = AppBy $ \(Compose fn) -> apply fn-------- | Only instance: @type instance WrapComp_ (f (g a)) = (f :. g) a@.-type WrapComp a = WrapComp_ a-type family WrapComp_ a-type instance WrapComp_ (f (g a)) = (f :. g) a---- | Only instance: @type instance WrapCompF_ (f (g a)) = f :. g@.-type WrapCompF a = WrapCompF_ a-type family WrapCompF_ a :: * -> *-type instance WrapCompF_ (f (g a)) = f :. g------{- | Defining instances:--@-  type instance Dom (AsComp fn) t = WrapComp (Dom fn t)-  type instance Rng (AsComp fn) t = WrapComp (Rng fn t)-  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap-@---}-newtype AsComp (fn :: * -> *) t = AsComp (fn t)--type instance Unwrap (AsComp fn) t = fn t-instance Wrapper (AsComp fn) where wrap = AsComp; unwrap (AsComp x) = x--type instance Dom (AsComp fn) t = WrapComp (Dom fn t)-type instance Rng (AsComp fn) t = WrapComp (Rng fn t)--type instance DomF (AsComp fn) = WrapCompF (Dom fn ())-type instance RngF (AsComp fn) = WrapCompF (Rng fn ())--instance (t ::: Domain fn, Dom fn t ~ ex0 (ex1 ex2), Rng fn t ~ ex3 (ex4 ex5)-         ) => t ::: Domain (AsComp fn) where-  inhabits = AppBy $ \(AsComp fn) -> wrap . apply fn . unwrap

@@ -1,36 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleContexts #-}--{- |--Module      :  Type.Yoko.FunA-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--"Type.Yoko.Fun" functions that /implicitly/ return an applicative functor. The-implicitness means that the 'Rng' type instance is not expected to include the-applicative functor.---}--module Type.Yoko.FunA-  (Idiom, DomainA(..), applyA, applyAU) where--import Type.Yoko.Fun-import Type.Yoko.Universe------type family Idiom (fn :: * -> *) :: * -> *-newtype DomainA fn t = AppABy (fn t -> Dom fn t -> Idiom fn (Rng fn t))--applyA :: (t ::: DomainA fn) => fn t -> Dom fn t -> Idiom fn (Rng fn t)-applyA = applyAU inhabits--applyAU :: DomainA fn t -> fn t -> Dom fn t -> Idiom fn (Rng fn t)-applyAU (AppABy f) = f

@@ -1,97 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, FlexibleContexts,-  ScopedTypeVariables, UndecidableInstances, QuasiQuotes, TypeFamilies,-  GADTs, TypeOperators, Rank2Types #-}--{- |--Module      :  Type.Yoko.MFun-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--An enrichment of "Type.Yoko.Fun" where functions must be of kind @* -> * -> *@;-the first parameter is a mediator and the second is (as expected by-"Type.Yoko.Fun") the type at which the function is to be instantiated.---}--module Type.Yoko.MFun where--import Type.Yoko.TSTSS--import Type.Yoko.Type-import Type.Yoko.Universe-import Type.Yoko.Natural--import Type.Yoko.Fun--import Data.Yoko.Generic------- | mediator-functions can be mapped across an 'RM' type/value.-newtype RMMap u fn m c = RMMap (NT u (fn m))--{- | mediator-functions can also modify the mediator; e.g.--@-  type instance 'Dom' (RMMap u fn m) c = RM m c-  type instance 'Rng' (RMMap u fn m) c = RM (MApp fn m) c-@---}-type family MApp (fn :: * -> * -> *) m--type instance Dom (RMMap u fn m) c = RM m c-type instance Rng (RMMap u fn m) c = RM (MApp fn m) c--type instance MApp (RMMap u fn) m = MApp fn m--instance (t ::: u, t ::: Domain (fn m), Wrapper (fn m),-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med (MApp fn m) t-         ) => R t ::: Domain (RMMap u fn m) where-  inhabits = AppBy $ \(RMMap fns) ->-             R . apply (fns `appNTF` inhabitsFor [qP|t|]) . unR--instance (Rep t ::: Domain (RMMap u fn m), Generic t-         ) => N t ::: Domain (RMMap u fn m) where-  inhabits = AppBy $ \(RMMap fn) -> obj . apply (RMMap fn) . rep--instance D a ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ -> D . unD-instance U ::: Domain (RMMap u fn m) where inhabits = AppBy $ \_ _ -> U-instance (Functor f, c ::: Domain (RMMap u fn m)-         ) => F f c ::: Domain (RMMap u fn m) where-  inhabits = AppBy $ \(RMMap fn) -> F . fmap (apply (RMMap fn)) . unF-instance (c ::: Domain (RMMap u fn m), d ::: Domain (RMMap u fn m),-          FunctorTSTSS ff) => FF ff c d ::: Domain (RMMap u fn m) where-  inhabits = AppBy $ \(RMMap fn) -> FF .-             fmapTSTSS (apply (RMMap fn)) (apply (RMMap fn)) . unFF-instance (c ::: Domain (RMMap u fn m)) => M i c ::: Domain (RMMap u fn m) where-  inhabits = AppBy $ \(RMMap fn) -> M . apply (RMMap fn) . unM------type instance DomF (RMMap u fn m) = RM m-type instance RngF (RMMap u fn m) = RM (MApp fn m)------- | A @FromAt@ function is applicable only at the specified mediator and type;--- crucially @type instance MApp (FromAt m) n = m@.-newtype FromAt m n a = FromAt {toAt :: Med n a -> Med m a}--type instance Unwrap (FromAt m n) a = Med n a -> Med m a-instance Wrapper (FromAt m n) where wrap = FromAt; unwrap (FromAt x) = x--type instance Dom (FromAt m n) t = Med n t-type instance Rng (FromAt m n) t = Med m t-instance a ::: Domain (FromAt m n) where inhabits = AppBy toAt--type instance MApp (FromAt m) n = m

@@ -1,82 +0,0 @@-{-# LANGUAGE ExistentialQuantification, QuasiQuotes, TypeOperators,-  Rank2Types, GADTs, ScopedTypeVariables, TypeFamilies #-}--{- |--Module      :  Type.Yoko.Natural-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Natural transformations and pairs.---}--module Type.Yoko.Natural where--import Type.Yoko.Type-import Type.Yoko.Universe----type NT_ u f = forall t. u t -> f t---- | Natural transformations. We use 'Unwrap' to lighten the user interface at--- the value level, though it clutters the types a little.-newtype NT u f = NT (forall t. u t -> Unwrap f t)--nt_ :: [qP|f :: *->*|] -> (forall t. u t -> Unwrap f t) -> NT u f-nt_ p f = NT f---appNT :: NT u f -> u t -> Unwrap f t-appNT (NT f) x = f x--appNTF :: Wrapper f => NT u f -> NT_ u f-appNTF (NT f) x = wrap (f x)----- | Defining an @NT@ via type-level backtracking; ':||' uses 'Pred' to--- short-circuit, preferring inhabitation of @u@ over @v@.-orNT :: NT u f -> NT v f -> NT (u :|| v) f-orNT (NT f) (NT g) = NT $ \uv -> case uv of-  LeftU  u -> f u-  RightU v -> g v---constNT :: Unwrap f t -> NT ((:=:) t) f-constNT = constNT_ Proxy--constNT_ :: [qP|f :: *->*|] -> Unwrap f t -> NT ((:=:) t) f-constNT_ p x = nt_ p $ \Refl -> x--constNTF :: Wrapper f => f t -> NT ((:=:) t) f-constNTF x = NT $ \Refl -> unwrap x---firstNT :: NT_ u g -> NT g f -> NT u f-firstNT g (NT f) = NT $ f . g-------- | Natural pairs.-data NP u f = forall t. NP (u t) (Unwrap f t)---- | Analog to "Control.Arrow"@.first@.-firstNP :: NT_ u v -> NP u f -> NP v f-firstNP f (NP u x) = NP (f u) x----- | @ArrowTSS@ can be partially applied, and hence occur as the second--- argument of @NT@, where as @f _ -> g _@ cannot.-newtype ArrowTSS f g a = ArrowTSS (f a -> g a)-type instance Unwrap (ArrowTSS f g) a = f a -> g a-instance Wrapper (ArrowTSS f g) where wrap = ArrowTSS; unwrap (ArrowTSS f) = f--appNTtoNP :: (Wrapper f, Wrapper g) => NT u (ArrowTSS f g) -> NP u f -> NP u g-appNTtoNP (NT f) (NP u x) = NP u $ unwrap $ f u $ wrap x

@@ -1,102 +0,0 @@-{-# LANGUAGE TypeFamilies, GADTs, TypeOperators, EmptyDataDecls,-  QuasiQuotes, UndecidableInstances, ScopedTypeVariables,-  MultiParamTypeClasses, FlexibleInstances, TypeSynonymInstances,-  FlexibleContexts #-}--{-# LANGUAGE TemplateHaskell #-}--{- |--Module      :  Type.Yoko.Sum-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Finite sums of types.---}--module Type.Yoko.Sum ((:+), All(..), TSum, Exists(..), Elem) where--import Type.Yoko.Type-import Type.Yoko.Universe-import Data.Yoko.CoreTypes----infixr 5 :+--- | Type-sum union. We re-use 'N' as type-sum singleton and 'V' as the empty--- type-sum.-data t :+ s------ | The higher-order universe @All@. @c@ inhabits @All u@ if @c@ is a type-sum--- and all types in it inhabit @u@.-data All u c where-  SumV :: All u V-  SumN :: (t ::: u) => u t -> All u (N t)-  SumS :: All u c -> All u d -> All u (c :+ d)--instance V ::: All u where inhabits = SumV-instance (t ::: u) => N t ::: All u where inhabits = SumN inhabits-instance (c ::: All u, d ::: All u) => (c :+ d) ::: All u where-  inhabits = SumS inhabits inhabits---- | @All 'NoneU'@ is satisfied by any type-sum.-type TSum = All NoneU-------- | The higher-order universe @Exists@. @c@ inhabits @Exists p@ if there--- exists a type @t@ in the type-sum @c@ for which @'True' ~ 'Pred' p t@. NB--- that @c@ is not necessarily a type-sum; i.e. there is no well-typed total--- function from @Exists p c@ to @TSum c@.-data Exists p c where-  Here    :: p t        -> Exists p (N t)-  OnLeft  :: Exists p c -> Exists p (c :+ d)-  OnRight :: Exists p d -> Exists p (c :+ d)----data Nothing; data Just path--type family IsJust a-type instance IsJust Nothing = False-type instance IsJust (Just path) = True--type family Combine l r-type instance Combine Nothing Nothing = Nothing-type instance Combine Nothing (Just x) = Just (OnRight x)-type instance Combine (Just x) r = Just (OnLeft x)----data Here-data OnLeft x-data OnRight x---- | @Elem t ts@ is 'True' if @t@ occurs in the type sum @ts@.-type Elem t ts = IsJust (Find ((:=:) t) ts)--type family Find (pred :: * -> *) c-type instance Find p (N t) = If (Pred p t) (Just Here) Nothing-type instance Find p (c :+ d) = Combine (Find p c) (Find p d)-type instance Find p V = Nothing----instance (Just path ~ Find p c, c ::: Exists p :? path) => c ::: Exists p where-  inhabits = inhabits_ [qP|path|]--instance (t ::: p)                => N t      ::: Exists p :? Here where-  inhabits = Anno $ Here inhabits-instance (c ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnLeft  path where-  inhabits = Anno $ OnLeft  (inhabits_ [qP|path|])-instance (d ::: Exists p :? path) => (c :+ d) ::: Exists p :? OnRight path where-  inhabits = Anno $ OnRight (inhabits_ [qP|path|])

@@ -1,110 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleContexts, MultiParamTypeClasses,-  FlexibleInstances, UndecidableInstances, QuasiQuotes, ScopedTypeVariables,-  Rank2Types #-}--{- |--Module      :  Type.Yoko.TFunA-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--The type-level functionality of "Type.Yoko.FunA" functions.---}--module Type.Yoko.TFunA (TApp, CMap(..), CApp) where--import Type.Yoko.TSTSS--import Type.Yoko.Fun-import Type.Yoko.FunA--import Type.Yoko.Type-import Type.Yoko.Universe--import Data.Yoko.CoreTypes-import Data.Yoko.Generic--import Control.Applicative (Applicative(pure))-import Data.Traversable (Traversable(traverse))------- | The @TApp@ type family encodes the type-level functionality of--- "Type.Yoko.Fun" functions.-type family TApp (fn :: * -> *) t------- | @CMap fn m c@ applies @fn@ to all recursive occurrences (i.e. 'R') in a--- "Data.Yoko.Core" type @c@ that's mediated by @m@. The domain ('Dom') is @RM--- m c@ and the range ('Rng') is @RM m (CApp (fn m) c)@. The 'Idiom' is @Idiom--- (fn m)@.-newtype CMap fn m c = CMap (forall t. fn m t)--type instance Dom (CMap fn m) c = RM m c-type instance Rng (CMap fn m) c = RM m (CApp (fn m) c)-type instance Idiom (CMap fn m) = Idiom (fn m)---- | @CApp fn c@ applies the type-function @fn@ to all recursive occurrences--- (i.e. 'R') in the "Data.Yoko.Core" type @c@.-type family CApp (fn :: * -> *) c-type instance CApp fn (D a) = D a-type instance CApp fn (F f c) = F f (CApp fn c)-type instance CApp fn (FF ff c d) = FF ff (CApp fn c) (CApp fn d)-type instance CApp fn (M i c) = M i (CApp fn c)-type instance CApp fn (R t) = R (TApp fn t)-type instance CApp fn U = U-type instance CApp fn V = V--pureDomain :: (Dom fn t ~ Rng fn t) => Domain fn t-pureDomain = AppBy $ \_ -> id--instance D a ::: Domain (CMap fn m) where inhabits = pureDomain-instance (c ::: Domain (CMap fn m), Traversable f-         ) => F f c ::: Domain (CMap fn m) where-  inhabits = AppBy $ \(CMap fn) -> F . fmap (apply (CMap fn)) . unF-instance (c ::: Domain (CMap fn m), d ::: Domain (CMap fn m),-          FunctorTSTSS ff-         ) => FF ff c d ::: Domain (CMap fn m) where-  inhabits = AppBy $ \(CMap fn) -> FF .-               fmapTSTSS (apply (CMap fn)) (apply (CMap fn)) . unFF-instance (c ::: Domain (CMap fn m)) => M i c ::: Domain (CMap fn m) where-  inhabits = AppBy $ \(CMap fn) -> M . apply (CMap fn) . unM-instance (t ::: Domain (fn m), Wrapper (fn m),-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)-         ) => R t ::: Domain (CMap fn m) where-  inhabits = AppBy $ \(CMap fn) -> R . apply (fn :: fn m t) . unR-instance U ::: Domain (CMap fn m) where inhabits = pureDomain-instance V ::: Domain (CMap fn m) where inhabits = pureDomain--pureDomainA :: (Dom fn t ~ Rng fn t, Applicative (Idiom fn)) => DomainA fn t-pureDomainA = AppABy $ \_ -> pure--instance Applicative (Idiom (fn m)) => D a ::: DomainA (CMap fn m) where-  inhabits = pureDomainA-instance (c ::: DomainA (CMap fn m), Applicative (Idiom (fn m)),-          Traversable f) => F f c ::: DomainA (CMap fn m) where-  inhabits = AppABy $ \(CMap fn) -> fmap F . traverse (applyA (CMap fn)) . unF-instance (c ::: DomainA (CMap fn m), d ::: DomainA (CMap fn m),-          Applicative (Idiom (fn m)), TraversableTSTSS ff-         ) => FF ff c d ::: DomainA (CMap fn m) where-  inhabits = AppABy $ \(CMap fn) -> fmap FF .-               traverseTSTSS (applyA (CMap fn)) (applyA (CMap fn)) . unFF-instance (c ::: DomainA (CMap fn m), Functor (Idiom (fn m))-         ) => M i c ::: DomainA (CMap fn m) where-  inhabits = AppABy $ \(CMap fn) -> fmap M . applyA (CMap fn) . unM-instance (t ::: DomainA (fn m), Functor (Idiom (fn m)), Wrapper (fn m),-          Dom (fn m) t ~ Med m t, Rng (fn m) t ~ Med m (TApp (fn m) t)-         ) => R t ::: DomainA (CMap fn m) where-  inhabits = AppABy $ \(CMap fn) -> fmap R . applyA (fn :: fn m t) . unR-instance Applicative (Idiom (fn m)) => U ::: DomainA (CMap fn m) where-  inhabits = pureDomainA-instance Applicative (Idiom (fn m)) => V ::: DomainA (CMap fn m) where-  inhabits = pureDomainA

@@ -1,29 +0,0 @@-{- |--Module      :  Type.Yoko.TSTSS-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Classes for @* -> * -> *@ types.---}--module Type.Yoko.TSTSS where--import Control.Applicative----class FunctorTSTSS ff where-  fmapTSTSS :: (a -> c) -> (b -> d) -> ff a b -> ff c d-instance FunctorTSTSS Either where fmapTSTSS f g = (Left . f) `either` (Right . g)-instance FunctorTSTSS (,) where fmapTSTSS f g ~(x, y) = (f x, g y)--class TraversableTSTSS ff where-  traverseTSTSS :: Applicative i => (a -> i c) -> (b -> i d) -> ff a b -> i (ff c d)-instance TraversableTSTSS Either where traverseTSTSS f g = either (fmap Left . f) (fmap Right . g)-instance TraversableTSTSS (,) where traverseTSTSS f g ~(x, y) = (,) <$> f x <*> g y

@@ -1,84 +0,0 @@-{-# LANGUAGE TypeFamilies, FlexibleContexts, TypeOperators,-  ScopedTypeVariables, UndecidableInstances, FlexibleInstances #-}--{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, GADTs #-}--{- |--Module      :  Type.Yoko.Type-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Some fundamental types central to @yoko@.---}--module Type.Yoko.Type-  (qK, Proxy(Proxy), module Type.Yoko.Type, module Type.Spine.Stage0,-   module Type.Booleans, IsEQ, Compare, EqT(..), (:=:)(..)) where--import Data.Proxy (Proxy(..))--import Type.Spine-import Type.Spine.Stage0 (KS, KTSS)-import Type.Serialize--import Data.Proxy.TH (qProxy)-import Type.Booleans---import Polarity-import Type.Ord.SpineSerialize (IsEQ, Compare)--import Data.Type.Equality----qP = qProxy------ | The @Med@ type family encodes the behavior of recursion mediators.-type family Med m a--- | @type instance Med IdM a = a@.-data IdM = IdM; type instance Med IdM a = a------- | The @Wrapper@ class is used to make term-level programming newtypes a--- little more lightweight from the user perspective.-class Wrapper f where wrap :: Unwrap f a -> f a; unwrap :: f a -> Unwrap f a-type family Unwrap (f :: * -> *) a------ | The @Pred@ type family realizes type-level predicates (over types) that--- yield a type-level Boolean: either 'True' or 'False'. Predicates are often--- universes.-type family Pred (p :: * -> *) a--type instance Pred ((:=:) a) b = IsEQ (Compare a b)------derive n = do-  d <- spineType n-  (d ++) `fmap` serializeTypeAsHash n-------- | Composition of @* -> *@ types.-newtype (f :. g) a = Compose (f (g a))-type instance Unwrap (f :. g) a = f (g a)-instance Wrapper (f :. g) where wrap = Compose; unwrap (Compose x) = x---- | Explicitly takes the inner type as a proxy.-composeWith :: [qProxy|g :: *->*|] -> f (g a) -> (f :. g) a-composeWith _ = Compose

@@ -1,87 +0,0 @@-{-# LANGUAGE MultiParamTypeClasses, QuasiQuotes, TypeFamilies, TypeOperators,-  FlexibleContexts, ScopedTypeVariables, FlexibleInstances,-  UndecidableInstances, GADTs, Rank2Types, EmptyDataDecls #-}--{- |--Module      :  Type.Yoko.Universe-Copyright   :  (c) The University of Kansas 2011-License     :  BSD3--Maintainer  :  nicolas.frisby@gmail.com-Stability   :  experimental-Portability :  see LANGUAGE pragmas (... GHC)--Type universes.---}--module Type.Yoko.Universe where--import Type.Yoko.Type--infix 0 :::--- | A /universe/ determines a set of types; /open/ or /closed/. @(:::)@ is--- comparable to the @Sat@ class (e.g. from @SYB3@).-class a ::: u where inhabits :: u a------ | @(:?)@ helps us write /guarded/ @(:::)@ instances (see--- <http://hackage.haskell.org/trac/ghc/ticket/5590>)-infix 1 :?-data (u :? anno) a = Anno (u a)----- | For use with @(:::)@ instances that use @(:?)@.-inhabits_ :: forall a u anno. (a ::: u :? anno) => [qP|anno|] -> u a-inhabits_ _ = i where Anno i = inhabits :: (u :? anno) a---- | Sometimes it's helpful to specify which @t@ must be in the universe.-inhabitsFor :: (t ::: u) => [qP|t|] -> u t-inhabitsFor _ = inhabits------ | The universe of all types; it has /no/ contraints.-data NoneU a = NoneU-instance a ::: NoneU where inhabits = NoneU--type Both = (:&&)-infixr 3 :&&--- | Universe product.-data (u :&& v) a where (:&&) :: (a ::: u, a ::: v) => {fstU :: u a, sndU :: v a} -> (u :&& v) a-instance (a ::: u, a ::: v) => a ::: u :&& v where-  inhabits = inhabits :&& inhabits--type instance Pred (p :&& q) a = And (Pred p a) (Pred q a)----instance (a ~ b) => b ::: (:=:) a where inhabits = Refl---infixr 2 :||--- | Universe sum.-data (u :|| v) a where-  LeftU  :: u a -> (u :|| v) a-  RightU :: v a -> (u :|| v) a--instance (anno ~ Pred u a, a ::: u :|| v :? anno) => a ::: u :|| v where-  inhabits = inhabits_ [qP|anno|]-instance (True  ~ Pred u a, a ::: u) => a ::: u :|| v :? True where-  inhabits = Anno $ LeftU inhabits-instance (False ~ Pred u a, a ::: v) => a ::: u :|| v :? False where-  inhabits = Anno $ RightU inhabits---type instance Pred (u :|| v) t = Or (Pred u t) (Pred v t)------ | The empty universe.-data VoidU t -- the empty universe----instance (f t ::: u) => t ::: (u :. f) where inhabits = Compose inhabits

@@ -1,8 +1,11 @@ name: yoko-version: 0.2-synopsis: generic programming with disbanded constructors +version: 0.3+synopsis: Generic Programming with Disbanded Data Types -description: @yoko@ views a nominal datatype as a /band/ of constructors, each+description:+  Based off of the paper \"A Pattern for Almost Compositional Functions\" at <http://www.ittc.ku.edu/~nfrisby/papers/yoko.pdf>, submitted to ICFP 2012.+  .+  @yoko@ views a nominal datatype as a /band/ of constructors, each   a nominal type in its own right. Such datatypes can be disbanded via the   @disband@ function into an anonymous sum of nominal constructors, and vice   versa via the @band@ function. This library uses extensive type-level@@ -19,10 +22,10 @@   /constructor types/.   .   @-    data John = John ...-    data Paul = Paul ...+    data John   = John   ...+    data Paul   = Paul   ...     data George = George ...-    data Ringo = Ringo ...+    data Ringo  = Ringo  ...   @   .   @yoko@'s conceptual foundations start there. In particular, this allows a@@ -30,32 +33,37 @@   and sibling constructors.   .   As a generic programming library, @yoko@ extends @instant-generics@ with-  support for constructor-centric generic programming. The @Examples/LL.hs@+  support for constructor-centric generic programming. The @Examples/LambdaLift/@   file distributed with the @yoko@ source demonstrates defining a-  lambda-lifting conversion between the two types @Inner@, which has lambdas,+  lambda-lifting conversion between the two types @ULC@, which has lambdas,   and @Prog@, which has top-level function declarations instead.   .   @-    data Inner = Lam Type Inner | Var Int | App Inner Inner+    data ULC = Lam Type ULC | Var Int | Let [Decl] ULC | App ULC ULC   .-    data Term = Var Int | App Term Term | DVar Int-    data Prog = Prog ([Type], Type, Term) Term+    data Decl = Decl Type ULC+  .+  .+  .+    data Prog = Prog [FunDec] TLF+    type FunDec = ([Type], [Type], Type, TLF)+  .+    data TLF = Top Int [Occ] | Occ Occ | App TLF TLF+    data Occ = Par Int | Env Int   @   .   These types are defined in separate modules, since they have constructors   with the same name. Indeed, the fact that they having matching constructors-  named @App@ is crucial for @yoko@'s automatic conversion from @Inner@'s @App@-  to @Term@'s @App@. As written, the generic lambda-lifter would continue to-  work for any new @Inner@ constructors (e.g. syntax for tuples or mutable+  named @App@ is crucial for @yoko@'s automatic conversion from @ULC@'s @App@+  to @TLF@'s @App@. As written, the generic lambda-lifter would continue to+  work for any new @ULC@ constructors (e.g. syntax for tuples or mutable   references) as long as constructors with the same names and analogous fields-  were added to @Term@ and the semantics of those constructors doesn't involve+  were added to @TLF@ and the semantics of those constructors doesn't involve   binding. This default behavior of the lambda-lifter is specified in about ten   lines of user code.   .   Existing generic libraries don't use constructor names to the degree that-  @yoko@ does, and so cannot accomodate generic /conversions/ nearly as well.-  .-  See the wiki at <http://code.google.com/p/yoko> for more documentation.+  @yoko@ does, and so cannot accomodate generic /conversions/ as well.  category: Generics, Reflection @@ -73,37 +81,30 @@   library-  build-depends: base >= 4 && < 5-  build-depends: type-equality < 0.2, tagged >= 0.2 && < 0.3+  build-depends: base >= 4 && < 5, template-haskell+  build-depends: type-equality < 0.2 -  build-depends: type-booleans < 0.2, type-spine < 0.2, tagged-th < 0.2,-    type-digits < 0.2, type-cereal < 0.2, type-ord < 0.2, type-ord-spine-cereal-    < 0.2+  build-depends:+    type-booleans < 0.2,+    type-spine < 0.2,+    tagged-th < 0.2,+    type-digits < 0.2,+    type-cereal < 0.2,+    type-ord < 0.2,+    type-ord-spine-cereal < 0.2 -  exposed-modules: Type.Yoko,-                   Type.Yoko.Type,-                   Type.Yoko.Universe,-                   Type.Yoko.Natural,-                   Type.Yoko.Sum,-                   Type.Yoko.BTree,-                   Type.Yoko.TSTSS,-                   Type.Yoko.Fun,-                   Type.Yoko.FunA,-                   Type.Yoko.MFun,-                   Type.Yoko.TFunA,+  exposed-modules:+    Data.Yoko, Data.Yoko.HCompos, -                   Data.Yoko,-                   Data.Yoko.Core,-                   Data.Yoko.CoreTypes,-                   Data.Yoko.Generic,-                   Data.Yoko.ReflectBase,-                   Data.Yoko.Reflect,-                   Data.Yoko.InDT,-                   Data.Yoko.Reduce,-                   Data.Yoko.Cata+    Data.Yoko.TypeBasics, Data.Yoko.Each ---                   Examples.TermBase,---                   Examples.TermGeneric,---                   Examples.InnerBase,---                   Examples.InnerGeneric,---                   Examples.TermInner+  other-modules:+    Data.Yoko.MaybeKind,+    Data.Yoko.Representation,+    Data.Yoko.TypeSums,+    Data.Yoko.TypeSumsAux++    -- under development+--    Data.Yoko.Fold,+--    Data.Yoko.Map,+--    Data.Yoko.OnRs