packages feed

compdata 0.9 → 0.10

raw patch · 24 files changed

+298/−92 lines, 24 filesdep ~QuickCheckdep ~basedep ~containers

Dependency ranges changed: QuickCheck, base, containers, deepseq, derive, mtl, template-haskell, test-framework-quickcheck2, th-expand-syns, transformers, tree-view

Files

compdata.cabal view
@@ -1,5 +1,5 @@ Name:			compdata-Version:		0.9+Version:		0.10 Synopsis:            	Compositional Data Types Description: @@ -145,6 +145,7 @@                         Data.Comp.Mapping                         Data.Comp.Thunk                         Data.Comp.Ops+                        Data.Comp.Projection                          Data.Comp.Multi                         Data.Comp.Multi.Term@@ -163,6 +164,7 @@                         Data.Comp.Multi.Derive                         Data.Comp.Multi.Generic                         Data.Comp.Multi.Desugar+                        Data.Comp.Multi.Projection    Other-Modules:        Data.Comp.SubsumeCommon                         Data.Comp.Derive.Equality@@ -185,8 +187,9 @@                         Data.Comp.Multi.Derive.SmartConstructors                         Data.Comp.Multi.Derive.SmartAConstructors -  Build-Depends:	base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive,+  Build-Depends:	base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, derive,                         deepseq, th-expand-syns, transformers, tree-view+  Extensions:           FlexibleContexts   hs-source-dirs:	src   ghc-options:          -W @@ -195,8 +198,8 @@   Type:                 exitcode-stdio-1.0   Main-is:		Data_Test.hs   hs-source-dirs:	testsuite/tests examples src-  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, -                        HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2, derive,+  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, +                        HUnit, test-framework, test-framework-hunit, test-framework-quickcheck2 >= 0.3, derive,                         th-expand-syns, deepseq, transformers  Benchmark algebra@@ -206,7 +209,7 @@   ghc-options:          -W -O2   -- Disable short-cut fusion rules in order to compare optimised and unoptimised code.   cpp-options:          -DNO_RULES-  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers+  Build-Depends:        base >= 4.7, base < 5, template-haskell, containers, mtl >= 2.2.1, QuickCheck >= 2 && < 2.8, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers   source-repository head
examples/Examples/Common.hs view
@@ -1,4 +1,5 @@ {-# LANGUAGE TemplateHaskell, TypeOperators #-}+{-# LANGUAGE FlexibleContexts #-} -------------------------------------------------------------------------------- -- | -- Module      :  Examples.Common
src/Data/Comp/Derive/Arbitrary.hs view
@@ -49,7 +49,7 @@   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify dt   let argNames = map (VarT . tyVarBndrName) (tail args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Arbitrary . (: [])) argNames+      preCond = map (mkClassP ''Arbitrary . (: [])) argNames       classType = AppT (ConT ''ArbitraryF) complType   arbitraryDecl <- generateArbitraryFDecl constrs   shrinkDecl <- generateShrinkFDecl constrs
src/Data/Comp/Derive/DeepSeq.hs view
@@ -35,7 +35,7 @@   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''NFData . (: [])) argNames+      preCond = map (mkClassP ''NFData . (: [])) argNames       classType = AppT (ConT ''NFDataF) complType   constrs' <- mapM normalConExp constrs   rnfFDecl <- funD 'rnfF (rnfFClauses constrs')
src/Data/Comp/Derive/Equality.hs view
@@ -34,7 +34,7 @@   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Eq . (: [])) argNames+      preCond = map (mkClassP ''Eq . (: [])) argNames       classType = AppT (ConT ''EqF) complType   eqFDecl <- funD 'eqF  (eqFClauses constrs)   return [InstanceD preCond classType [eqFDecl]]
src/Data/Comp/Derive/Ordering.hs view
@@ -40,7 +40,7 @@   TyConI (DataD _cxt name args constrs _deriving) <- abstractNewtypeQ $ reify fname   let argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Ord . (: [])) argNames+      preCond = map (mkClassP ''Ord . (: [])) argNames       classType = AppT (ConT ''OrdF) complType   eqAlgDecl <- funD 'compareF  (compareFClauses constrs)   return [InstanceD preCond classType [eqAlgDecl]]
src/Data/Comp/Derive/Show.hs view
@@ -40,7 +40,7 @@   let fArg = VarT . tyVarBndrName $ last args       argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Show . (: [])) argNames+      preCond = map (mkClassP ''Show . (: [])) argNames       classType = AppT (ConT ''ShowF) complType   constrs' <- mapM normalConExp constrs   showFDecl <- funD 'showF (showFClauses fArg constrs')@@ -76,7 +76,7 @@   let fArg = VarT . tyVarBndrName $ last args       argNames = map (VarT . tyVarBndrName) (init args)       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Show . (: [])) argNames+      preCond = map (mkClassP ''Show . (: [])) argNames       classType = AppT (ConT ''ShowConstr) complType   constrs' <- mapM normalConExp constrs   showConstrDecl <- funD 'showConstr (showConstrClauses fArg constrs')
src/Data/Comp/Derive/Utils.hs view
@@ -27,7 +27,7 @@ #endif  {-|-  This is the @Q@-lifted version of 'abstractNewtypeQ.+  This is the @Q@-lifted version of 'abstractNewtype. -} abstractNewtypeQ :: Q Info -> Q Info abstractNewtypeQ = liftM abstractNewtype@@ -125,6 +125,33 @@ derive :: [Name -> Q [Dec]] -> [Name] -> Q [Dec] derive ders names = liftM concat $ sequence [der name | der <- ders, name <- names] +{-| Apply a class name to type arguments to construct a type class+    constraint.+-}++#if __GLASGOW_HASKELL__ < 710+mkClassP :: Name -> [Type] -> Pred+mkClassP = ClassP+#else+mkClassP :: Name -> [Type] -> Type+mkClassP name = foldl AppT (ConT name)+#endif++{-| This function checks whether the given type constraint is an+equality constraint. If so, the types of the equality constraint are+returned. -}++#if __GLASGOW_HASKELL__ < 710+isEqualP :: Pred -> Maybe (Type, Type)+isEqualP (EqualP x y) = Just (x, y)+isEqualP _ = Nothing+#else+isEqualP :: Type -> Maybe (Type, Type)+isEqualP (AppT (AppT EqualityT x) y) = Just (x, y)+isEqualP _ = Nothing+#endif++ -- | This function lifts type class instances over sums -- ofsignatures. To this end it assumes that it contains only methods -- with types of the form @f t1 .. tn -> t@ where @f@ is the signature@@ -154,8 +181,8 @@       let g = VarT $ mkName "g"       let ts1 = map VarT ts1_       let ts2 = map VarT ts2_-      let cxt = [ClassP name (ts1 ++ f : ts2),-                 ClassP name (ts1 ++ g : ts2)]+      let cxt = [mkClassP name (ts1 ++ f : ts2),+                 mkClassP name (ts1 ++ g : ts2)]       let tp = ((ConT sumName `AppT` f) `AppT` g)       let complType = foldl AppT (foldl AppT (ConT name) ts1 `AppT` tp) ts2       decs' <- sequence $ concatMap decl decs
src/Data/Comp/Mapping.hs view
@@ -2,6 +2,9 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE DeriveFoldable #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.Mapping@@ -22,11 +25,15 @@     , number     , Traversable ()     , Mapping (..)-    , lookupNumMap) where+    , prodMap+    , lookupNumMap+    , lookupNumMap'+    , NumMap) where  import Data.IntMap (IntMap) import qualified Data.IntMap as IntMap import Data.Traversable+import Data.Foldable  import Control.Monad.State hiding (mapM) import Prelude hiding (mapM)@@ -64,19 +71,25 @@      -- | This function constructs the pointwise product of two maps each     -- with a default value.-    prodMap :: v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)+    prodMapWith :: (v1 -> v2 -> v) -> v1 -> v2 -> m v1 -> m v2 -> m v      -- | Returns the value at the given key or returns the given     -- default when the key is not an element of the map.     findWithDefault :: a -> k -> m a -> a -+-- | This function constructs the pointwise product of two maps each+-- with a default value.+prodMap :: Mapping m k => v1 -> v2 -> m v1 -> m v2 -> m (v1, v2)+prodMap = prodMapWith (,) -newtype NumMap k v = NumMap (IntMap v) deriving Functor+newtype NumMap k v = NumMap (IntMap v) deriving (Functor,Foldable,Traversable)  lookupNumMap :: a -> Int -> NumMap t a -> a lookupNumMap d k (NumMap m) = IntMap.findWithDefault d k m +lookupNumMap' :: Int -> NumMap t a -> Maybe a+lookupNumMap' k (NumMap m) = IntMap.lookup k m+ instance Mapping (NumMap k) (Numbered k) where     NumMap m1 & NumMap m2 = NumMap (IntMap.union m1 m2)     Numbered k _ |-> v = NumMap $ IntMap.singleton k v@@ -84,6 +97,6 @@      findWithDefault d (Numbered i _) m = lookupNumMap d i m -    prodMap p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge -                                          (IntMap.map (,q)) (IntMap.map (p,)) mp mq-      where merge _ p q = Just (p,q)+    prodMapWith f p q (NumMap mp) (NumMap mq) = NumMap $ IntMap.mergeWithKey merge +                                          (IntMap.map (`f` q)) (IntMap.map (p `f`)) mp mq+      where merge _ p q = Just (p `f` q)
src/Data/Comp/Multi/Derive/Equality.hs view
@@ -32,7 +32,7 @@       argNames = map (VarT . tyVarBndrName) (init args')       ftyp = VarT . tyVarBndrName $ last args'       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Eq . (: [])) argNames+      preCond = map (mkClassP ''Eq . (: [])) argNames       classType = AppT (ConT ''EqHF) complType   constrs' <- mapM normalConExp constrs   eqFDecl <- funD 'eqHF  (eqFClauses ftyp constrs constrs')
src/Data/Comp/Multi/Derive/Show.hs view
@@ -49,7 +49,7 @@       fArg = VarT . tyVarBndrName $ last args'       argNames = map (VarT . tyVarBndrName) (init args')       complType = foldl AppT (ConT name) argNames-      preCond = map (ClassP ''Show . (: [])) argNames+      preCond = map (mkClassP ''Show . (: [])) argNames       classType = AppT (ConT ''ShowHF) complType   constrs' <- mapM normalConExp constrs   showFDecl <- funD 'showHF (showFClauses fArg constrs')
src/Data/Comp/Multi/Derive/SmartConstructors.hs view
@@ -35,7 +35,7 @@     liftM concat $ mapM (genSmartConstr (map tyVarBndrName targs) tname) cons         where iTp iVar (ForallC _ cxt _) =                   -- Check if the GADT phantom type is constrained-                  case [y | EqualP x y <- cxt, x == VarT iVar] of+                  case [y | Just (x, y) <- map isEqualP cxt, x == VarT iVar] of                     [] -> Nothing                     tp:_ -> Just tp               iTp _ _ = Nothing
src/Data/Comp/Multi/HFunctor.hs view
@@ -1,3 +1,7 @@+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE DeriveTraversable         #-}+{-# LANGUAGE DeriveFoldable            #-}+{-# LANGUAGE DeriveFunctor             #-} {-# LANGUAGE ExistentialQuantification #-} {-# LANGUAGE FlexibleInstances         #-} {-# LANGUAGE MultiParamTypeClasses     #-}@@ -5,6 +9,7 @@ {-# LANGUAGE ScopedTypeVariables       #-} {-# LANGUAGE TypeOperators             #-} {-# LANGUAGE UndecidableInstances      #-}+{-# LANGUAGE IncoherentInstances       #-}  -------------------------------------------------------------------------------- -- |@@ -34,17 +39,16 @@      (:.:)(..)      ) where +import Data.Traversable+import Data.Foldable+import Data.Functor.Compose+ -- | The identity Functor.-newtype I a = I {unI :: a}+newtype I a = I {unI :: a} deriving (Functor, Foldable, Traversable) -instance Functor I where-    fmap f (I x) = I (f x)  -- | The parametrised constant functor.-newtype K a i = K {unK :: a}--instance Functor (K a) where-    fmap _ (K x) = K x+newtype K a i = K {unK :: a} deriving (Functor, Foldable, Traversable)  data E f = forall i. E {unE :: f i} @@ -95,7 +99,9 @@     -- @g :-> h@ to a natural transformation @f g :-> f h@     hfmap :: (f :-> g) -> h f :-> h g +instance (Functor f) => HFunctor (Compose f) where hfmap f (Compose xs) = Compose (fmap f xs)+ infixl 5 :.:  -- | This data type denotes the composition of two functor families.-data  (f :.: g) e t = Comp f (g e) t+data (:.:) f (g :: (* -> *) -> (* -> *)) (e :: * -> *) t = Comp (f (g e) t)
src/Data/Comp/Multi/HTraversable.hs view
@@ -36,7 +36,10 @@     -- Alternative type in terms of natural transformations using     -- functor composition @:.:@:     ---    -- @hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)@+    -- @+    -- hmapM :: Monad m => (a :-> m :.: b) -> t a :-> m :.: (t b)+    -- @+    --      hmapM :: (Monad m) => NatM m a b -> NatM m (t a) (t b)      htraverse :: (Applicative f) => NatM f a b -> NatM f (t a) (t b)
src/Data/Comp/Multi/Mapping.hs view
@@ -4,6 +4,7 @@ {-# LANGUAGE TupleSections #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-}+{-# LANGUAGE FlexibleContexts #-} -------------------------------------------------------------------------------- -- | -- Module      :  Data.Comp.Multi.Mapping
src/Data/Comp/Multi/Ops.hs view
@@ -28,7 +28,12 @@ -- -------------------------------------------------------------------------------- -module Data.Comp.Multi.Ops where+module Data.Comp.Multi.Ops +    ( module Data.Comp.Multi.Ops+    , (O.:*:)(..)+    , O.ffst+    , O.fsnd+    ) where  import Control.Applicative import Control.Monad@@ -90,25 +95,6 @@     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)     Elem f g = NotFound --type family Choose (e1 :: Emb) (r :: Emb) :: Emb where-    Choose (Found x) (Found y) = Ambiguous-    Choose Ambiguous y = Ambiguous-    Choose x Ambiguous = Ambiguous-    Choose (Found x) y = Found (Le x)-    Choose x (Found y) = Found (Ri y)-    Choose x y = NotFound---type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where-    Sum' (Found x) (Found y) = Found (Sum x y)-    Sum' Ambiguous y = Ambiguous-    Sum' x Ambiguous = Ambiguous-    Sum' NotFound y = NotFound-    Sum' x NotFound = NotFound--data Proxy a = P- class Subsume (e :: Emb) (f :: (* -> *) -> * -> *)                          (g :: (* -> *) -> * -> *) where   inj'  :: Proxy e -> f a :-> g a@@ -164,19 +150,6 @@             Inl y -> f1 y             Inr y -> f2 y --- Products--infixr 8 :*:--data (f :*: g) a = f a :*: g a---fst :: (f :*: g) a -> f a-fst (x :*: _) = x--snd :: (f :*: g) a -> g a-snd (_ :*: x) = x- -- Constant Products  infixr 7 :&:@@ -184,7 +157,9 @@ -- | This data type adds a constant product to a -- signature. Alternatively, this could have also been defined as ----- @data (f :&: a) (g ::  * -> *) e = f g e :&: a e@+-- @+-- data (f :&: a) (g ::  * -> *) e = f g e :&: a e+-- @ -- -- This is too general, however, for example for 'productHHom'.
+ src/Data/Comp/Multi/Projection.hs view
@@ -0,0 +1,75 @@+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Multi.Projection+-- Copyright   :  (c) 2014 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides a generic projection function 'pr' for+-- arbitrary nested binary products.+--+--------------------------------------------------------------------------------+++module Data.Comp.Multi.Projection (pr, (:<), (:*:)(..), ffst, fsnd) where++import Data.Comp.SubsumeCommon+import Data.Comp.Multi.Ops hiding (Elem)++type family Elem (f :: * -> *)+                 (g :: * -> *) :: Emb where+    Elem f f = Found Here+    Elem (f1 :*: f2) g =  Sum' (Elem f1 g) (Elem f2 g)+    Elem f (g1 :*: g2) = Choose (Elem f g1) (Elem f g2)+    Elem f g = NotFound++class Proj (e :: Emb) (p :: * -> *)+                      (q :: * -> *) where+    pr'  :: Proxy e -> q a -> p a++instance Proj (Found Here) f f where+    pr' _ = id++instance Proj (Found p) f g => Proj (Found (Le p)) f (g :*: g') where+    pr' _ = pr' (P :: Proxy (Found p)) . ffst+++instance Proj (Found p) f g => Proj (Found (Ri p)) f (g' :*: g) where+    pr' _ = pr' (P :: Proxy (Found p)) . fsnd+++instance (Proj (Found p1) f1 g, Proj (Found p2) f2 g)+    => Proj (Found (Sum p1 p2)) (f1 :*: f2) g where+    pr' _ x = (pr' (P :: Proxy (Found p1)) x :*: pr' (P :: Proxy (Found p2)) x)+++infixl 5 :<++-- | The constraint @e :< p@ expresses that @e@ is a component of the+-- type @p@. That is, @p@ is formed by binary products using the type+-- @e@. The occurrence of @e@ must be unique. For example we have @Int+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.++type f :< g = (Proj (ComprEmb (Elem f g)) f g)+++-- | This function projects the component of type @e@ out or the+-- compound value of type @p@.++pr :: forall p q a . (p :< q) => q a -> p a+pr = pr' (P :: Proxy (ComprEmb (Elem p q)))
src/Data/Comp/Multi/Variables.hs view
@@ -81,17 +81,21 @@     -- | Indicates the set of variables bound by the @f@ constructor     -- for each argument of the constructor. For example for a     -- non-recursive let binding:+    --      -- @     -- data Let i e = Let Var (e i) (e i)     -- instance HasVars Let Var where     --   bindsVars (Let v x y) = y |-> Set.singleton v     -- @+    --      -- If, instead, the let binding is recursive, the methods has to     -- be implemented like this:+    --      -- @     --   bindsVars (Let v x y) = x |-> Set.singleton v &     --                           y |-> Set.singleton v     -- @+    --      -- This indicates that the scope of the bound variable also     -- extends to the right-hand side of the variable binding.     --
src/Data/Comp/Ops.hs view
@@ -98,25 +98,6 @@     Elem f (g1 :+: g2) = Choose (Elem f g1) (Elem f g2)     Elem f g = NotFound --type family Choose (e1 :: Emb) (r :: Emb) :: Emb where-    Choose (Found x) (Found y) = Ambiguous-    Choose Ambiguous y = Ambiguous-    Choose x Ambiguous = Ambiguous-    Choose (Found x) y = Found (Le x)-    Choose x (Found y) = Found (Ri y)-    Choose x y = NotFound---type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where-    Sum' (Found x) (Found y) = Found (Sum x y)-    Sum' Ambiguous y = Ambiguous-    Sum' x Ambiguous = Ambiguous-    Sum' NotFound y = NotFound-    Sum' x NotFound = NotFound--data Proxy a = P- class Subsume (e :: Emb) (f :: * -> *) (g :: * -> *) where   inj'  :: Proxy e -> f a -> g a   prj'  :: Proxy e -> g a -> Maybe (f a)@@ -185,6 +166,21 @@  fsnd :: (f :*: g) a -> g a fsnd (_ :*: x) = x++instance (Functor f, Functor g) => Functor (f :*: g) where+    fmap h (f :*: g) = (fmap h f :*: fmap h g)+++instance (Foldable f, Foldable g) => Foldable (f :*: g) where+    foldr f e (x :*: y) = foldr f (foldr f e y) x+    foldl f e (x :*: y) = foldl f (foldl f e x) y+++instance (Traversable f, Traversable g) => Traversable (f :*: g) where+    traverse f (x :*: y) = liftA2 (:*:) (traverse f x) (traverse f y)+    sequenceA (x :*: y) = liftA2 (:*:)(sequenceA x) (sequenceA y)+    mapM f (x :*: y) = liftM2 (:*:) (mapM f x) (mapM f y)+    sequence (x :*: y) = liftM2 (:*:) (sequence x) (sequence y)  -- Constant Products
+ src/Data/Comp/Projection.hs view
@@ -0,0 +1,74 @@+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-}++++--------------------------------------------------------------------------------+-- |+-- Module      :  Data.Comp.Projection+-- Copyright   :  (c) 2014 Patrick Bahr+-- License     :  BSD3+-- Maintainer  :  Patrick Bahr <paba@di.ku.dk>+-- Stability   :  experimental+-- Portability :  non-portable (GHC Extensions)+--+-- This module provides a generic projection function 'pr' for+-- arbitrary nested binary products.+--+--------------------------------------------------------------------------------+++module Data.Comp.Projection (pr, (:<)) where++import Data.Comp.SubsumeCommon++type family Elem (f :: *)+                 (g :: *) :: Emb where+    Elem f f = Found Here+    Elem (f1, f2) g =  Sum' (Elem f1 g) (Elem f2 g)+    Elem f (g1, g2) = Choose (Elem f g1) (Elem f g2)+    Elem f g = NotFound++class Proj (e :: Emb) (p :: *)+                      (q :: *) where+    pr'  :: Proxy e -> q -> p++instance Proj (Found Here) f f where+    pr' _ = id++instance Proj (Found p) f g => Proj (Found (Le p)) f (g, g') where+    pr' _ = pr' (P :: Proxy (Found p)) . fst+++instance Proj (Found p) f g => Proj (Found (Ri p)) f (g', g) where+    pr' _ = pr' (P :: Proxy (Found p)) . snd+++instance (Proj (Found p1) f1 g, Proj (Found p2) f2 g)+    => Proj (Found (Sum p1 p2)) (f1, f2) g where+    pr' _ x = (pr' (P :: Proxy (Found p1)) x, pr' (P :: Proxy (Found p2)) x)+++infixl 5 :<++-- | The constraint @e :< p@ expresses that @e@ is a component of the+-- type @p@. That is, @p@ is formed by binary products using the type+-- @e@. The occurrence of @e@ must be unique. For example we have @Int+-- :< (Bool,(Int,Bool))@ but not @Bool :< (Bool,(Int,Bool))@.++type f :< g = (Proj (ComprEmb (Elem f g)) f g)+++-- | This function projects the component of type @e@ out or the+-- compound value of type @p@.++pr :: forall p q . (p :< q) => q -> p+pr = pr' (P :: Proxy (ComprEmb (Elem p q)))
src/Data/Comp/SubsumeCommon.hs view
@@ -2,6 +2,7 @@ {-# LANGUAGE TypeFamilies         #-} {-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE PolyKinds            #-}  -------------------------------------------------------------------------------- -- |@@ -21,6 +22,9 @@     ( ComprEmb     , Pos (..)     , Emb (..)+    , Choose+    , Sum'+    , Proxy (..)     ) where  -- | This type is used in its promoted form only. It represents@@ -34,6 +38,26 @@ -- found. 'Ambiguous' indicates that there are duplicates on the left- -- or the right-hand side. data Emb = Found Pos | NotFound | Ambiguous++data Proxy a = P+++type family Choose (e1 :: Emb) (r :: Emb) :: Emb where+    Choose (Found x) (Found y) = Ambiguous+    Choose Ambiguous y = Ambiguous+    Choose x Ambiguous = Ambiguous+    Choose (Found x) y = Found (Le x)+    Choose x (Found y) = Found (Ri y)+    Choose x y = NotFound+++type family Sum' (e1 :: Emb) (r :: Emb) :: Emb where+    Sum' (Found x) (Found y) = Found (Sum x y)+    Sum' Ambiguous y = Ambiguous+    Sum' x Ambiguous = Ambiguous+    Sum' NotFound y = NotFound+    Sum' x NotFound = NotFound+  -- | This type family takes a position type and compresses it. That -- means it replaces each nested occurrence of
src/Data/Comp/Sum.hs view
@@ -26,7 +26,6 @@      (:=:),      (:+:),      caseF,-     Proxy (..),       -- * Projections for Signatures and Terms      proj,
src/Data/Comp/Unification.hs view
@@ -20,7 +20,7 @@ import Data.Comp.Term import Data.Comp.Variables -import Control.Monad.Error+import Control.Monad.Except import Control.Monad.State  import Data.Traversable@@ -42,10 +42,6 @@ data UnifError f v = FailedOccursCheck v (Term f)                    | HeadSymbolMismatch (Term f) (Term f)                    | UnifError String--instance Error (UnifError f v) where-    strMsg = UnifError-  -- | This is used in order to signal a failed occurs check during -- unification.
src/Data/Comp/Variables.hs view
@@ -43,6 +43,7 @@ import Data.Comp.Derive import Data.Comp.Mapping import Data.Comp.Term+import Data.Comp.Ops import Data.Foldable hiding (elem, notElem) import Data.Map (Map) import qualified Data.Map as Map@@ -71,17 +72,21 @@     -- | Indicates the set of variables bound by the @f@ constructor     -- for each argument of the constructor. For example for a     -- non-recursive let binding:+    --      -- @     -- data Let e = Let Var e e     -- instance HasVars Let Var where     --   bindsVars (Let v x y) = y |-> Set.singleton v     -- @+    --      -- If, instead, the let binding is recursive, the methods has to     -- be implemented like this:+    --      -- @     --   bindsVars (Let v x y) = x |-> Set.singleton v &     --                           y |-> Set.singleton v     -- @+    --      -- This indicates that the scope of the bound variable also     -- extends to the right-hand side of the variable binding.     --@@ -91,6 +96,10 @@   $(derive [liftSum] [''HasVars])++instance HasVars f v => HasVars (f :&: a) v where+  isVar (f :&: _)     = isVar f+  bindsVars (f :&: _) = bindsVars f  -- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if -- @v@ is contained in the given set of variables.