simplistic-generics 0.1.0.0 → 2.0.0

raw patch · 11 files changed

+1870/−227 lines, 11 filesdep +containersdep +deepseqdep +mtldep −comonadPVP ok

version bump matches the API change (PVP)

Dependencies added: containers, deepseq, mtl, template-haskell

Dependencies removed: comonad

API changes (from Hackage documentation)

Files

• simplistic-generics.cabal +46/−30
• src/Data/Constraints.hs +0/−16
• src/Generics/Simplistic.hs +339/−115
• src/Generics/Simplistic/Deep.hs +390/−0
• src/Generics/Simplistic/Deep/TH.hs +315/−0
• src/Generics/Simplistic/Derive/Eq.hs +16/−18
• src/Generics/Simplistic/Derive/Functor.hs +23/−17
• src/Generics/Simplistic/Derive/Show.hs +30/−31
• src/Generics/Simplistic/Unify.hs +289/−0
• src/Generics/Simplistic/Util.hs +249/−0
• src/Generics/Simplistic/Zipper.hs +173/−0

@@ -1,33 +1,49 @@-cabal-version:       >=1.10-name:                simplistic-generics-version:             0.1.0.0-synopsis:            Generic programming without too many type classes-description:         This library provides a representation build on top of -                     `GHC.Generics`, which can be used to describe generic-                     operations on a single function, instead of having-                     each case defined in an instance of a type class.--- bug-reports:-license:             BSD3-license-file:        LICENSE-author:              Alejandro Serrano-maintainer:          trupill@gmail.com--- copyright:-category:            Data-build-type:          Simple-extra-source-files:  README.md+cabal-version: 1.12 -library-  exposed-modules:     Generics.Simplistic,-                       Generics.Simplistic.Derive.Eq,-                       Generics.Simplistic.Derive.Functor,-                       Generics.Simplistic.Derive.Show-                       Data.Constraints-  -- other-modules:-  -- other-extensions:-  build-depends:       base >=4.12 && <5, kind-apply, comonad-  hs-source-dirs:      src-  default-language:    Haskell2010+-- This file has been generated from package.yaml by hpack version 0.31.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 1b90926eead859c5af167c81f38f7e1fc252fdba35adaaad6ee34ae33b85009b +name:           simplistic-generics+version:        2.0.0+synopsis:       Generic programming without too many type classes+description:    This library provides a representation build on top of `GHC.Generics`, which can be used to describe generic operations on a single function, instead of having each case defined in an instance of a type class.+category:       Data+author:         Alejandro Serrano and Victor Miraldo+maintainer:     trupill@gmail.com and v.cacciarimiraldo@gmail.com+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+ source-repository head-  type:                git-  location:            https://gitlab.com/trupill/simplistic-generics+  type: git+  location: https://gitlab.com/trupill/simplistic-generics++library+  exposed-modules:+      Generics.Simplistic+      Generics.Simplistic.Deep+      Generics.Simplistic.Deep.TH+      Generics.Simplistic.Derive.Eq+      Generics.Simplistic.Derive.Functor+      Generics.Simplistic.Derive.Show+      Generics.Simplistic.Unify+      Generics.Simplistic.Util+      Generics.Simplistic.Zipper+  other-modules:+      Paths_simplistic_generics+  hs-source-dirs:+      src/+  ghc-options: -O2 -Wall+  build-depends:+      base >=4.12 && <5+    , containers+    , deepseq+    , kind-apply+    , mtl+    , template-haskell+  default-language: Haskell2010

@@ -1,16 +0,0 @@-{-# language MultiParamTypeClasses,-             UndecidableInstances,-             QuantifiedConstraints,-             ConstraintKinds,-             FlexibleInstances,-             KindSignatures,-             PolyKinds #-}-module Data.Constraints where--import GHC.Exts (Constraint)--class    (c => d) => Implies c d-instance (c => d) => Implies c d--class    Trivial c-instance Trivial c

@@ -1,63 +1,123 @@-{-# language GADTs,-             DataKinds,-             PolyKinds,-             TypeOperators,-             ConstraintKinds,-             MultiParamTypeClasses,-             FlexibleContexts,-             FlexibleInstances,-             QuantifiedConstraints,-             UndecidableInstances,-             KindSignatures,-             TypeFamilies #-}-module Generics.Simplistic (-  -- * From `GHC.Generics.Extra` module-  Generic, Rep, Generic1, Rep1,-  V1, U1, (:+:), (:*:), K1, M1, (:=>:),-  -- * Simplistic representation on `*` types -  SMeta(..), SRep(..), GenericSy, fromS, toS, fromI, toI,-  -- ** Constraints over the leaves of a data type-  OnLeaves,-  -- * Simplistic representation on `* -> *` types -  SRep1(..), GenericSy1, fromS1, toS1,+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE DefaultSignatures       #-}+{-# LANGUAGE DeriveGeneric           #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE KindSignatures          #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE QuantifiedConstraints   #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# LANGUAGE StandaloneDeriving      #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE UndecidableInstances    #-}+-- |Introduces closed representations functor+-- for "GHC.Generics" style generics.+module Generics.Simplistic+  ( -- ** Re-exports from "GHC.Generics.Extra" module+    Generic, Rep, Rep1, Par1, Rec1, (:.:)(..), V1, U1(..), (:+:)(..)+  , (:*:)(..), K1(..), M1(..), (:=>:)(..), R+  -- * Simplistic representation on @*@ types+  , GMeta(..), SMeta(..), SMetaI(..), SRep(..) , I(..) , Simplistic   -- ** Constraints over the leaves of a data type-  OnLeaves1,+  , OnLeaves+  -- ** Combinators+  -- *** Maps , zips and folds+  , repMap , repMapM , repMapCM+  , zipSRep , repLeaves , repLeavesC , repLeavesList+  -- *** Metadata+  , getDatatypeName , getConstructorName+  , repDatatypeName , repConstructorName+  -- ** Shallow Conversion+  , fromS , toS , GShallow(..)+  -- * Simplistic representation on @* -> *@ types+  , SRep1(..) , OnLeaves1 , fromS1 , toS1 , GShallow1(..) , Simplistic1   -- * Auxiliary constraints-  Implies, Trivial-) where+  , Implies, Trivial+  ) where -import Control.Comonad-import Data.Functor.Identity-import Data.Constraints+import Data.Proxy+import Control.Monad.Identity+import Control.DeepSeq++import GHC.Generics import GHC.Generics.Extra import GHC.Exts (Constraint) +import Generics.Simplistic.Util ++---------------------+-- Representations --+---------------------+ data SMeta i t where   SM_D :: Datatype    d => SMeta D d   SM_C :: Constructor c => SMeta C c   SM_S :: Selector    s => SMeta S s+deriving instance Show (SMeta i t)+deriving instance Eq   (SMeta i t) +-- Dirty trick to access the dictionaries I need+data SMetaI d f x = SMetaI++smetaI :: SMeta i t -> SMetaI t Proxy ()+smetaI _ = SMetaI++getDatatypeName :: SMeta D d -> String+getDatatypeName x@SM_D = datatypeName (smetaI x)++getConstructorName :: SMeta C c -> String+getConstructorName x@SM_C = conName (smetaI x)++-- |Singletons for metainformation+class GMeta i c where+  smeta :: SMeta i c++instance Constructor c => GMeta C c where+  smeta = SM_C++instance Datatype d => GMeta D d where+  smeta = SM_D++instance Selector s => GMeta S s where+  smeta = SM_S++-- |Given some @a@, a value of type @SRep w (Rep a)@ is+-- a closed representation of a generic value of type @a@. infixr 5 :**: data SRep w f where   S_U1   ::                          SRep w U1   S_L1   ::              SRep w f -> SRep w (f :+: g)   S_R1   ::              SRep w g -> SRep w (f :+: g)-  (:**:) ::  SRep w f -> SRep w g -> SRep w (f :*: g)+  (:**:) :: SRep w f  -> SRep w g -> SRep w (f :*: g)   S_K1   ::              w a      -> SRep w (K1 i a)   S_M1   :: SMeta i t -> SRep w f -> SRep w (M1 i t f)   S_ST   ::         c => SRep w f -> SRep w (c :=>: f)--type GenericSy a = (Generic a, Sy (Rep a))+deriving instance (forall a. Show (w a)) => Show (SRep w f)+deriving instance (forall a. Eq   (w a)) => Eq   (SRep w f)+instance (forall x . NFData (w x)) => NFData (SRep w f) where+  rnf S_U1       = ()+  rnf (S_K1 w)   = rnf w+  rnf (S_M1 _ x) = rnf x+  rnf (S_L1 x)   = rnf x+  rnf (S_R1 x)   = rnf x+  rnf (x :**: y) = rnf x `seq` rnf y+  rnf (S_ST x)   = rnf x  -fromS :: (GenericSy a, Applicative w) => a -> SRep w (Rep a)-fromS = fromS' . from-fromI :: (GenericSy a) => a -> SRep Identity (Rep a)-fromI = fromS-toS :: (GenericSy a, Comonad w) => SRep w (Rep a) -> a-toS = to . toS'-toI :: (GenericSy a) => SRep Identity (Rep a) -> a-toI = toS+-- |All types supported by "GHC.Generics" are /simplistic/, this+-- constraint just couples their necessary together.+type Simplistic a = (Generic a , GShallow (Rep a)) +-- |Computes the constraint that corresponds to ensuring all+-- leaves of a representation satisfy a given constraint.+-- For example,+--+-- > OnLeaves Eq (Rep (Either a b)) = (Eq a , Eq b)+-- type family OnLeaves (c :: * -> Constraint) (f :: * -> *) :: Constraint where   OnLeaves c V1        = ()   OnLeaves c U1        = ()@@ -67,7 +127,202 @@   OnLeaves c (M1 i p f) = OnLeaves c f   OnLeaves c (d :=>: f) = Implies d (OnLeaves c f) +-- |Retrieves the datatype name for a representation.+-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of+-- a type constructed with "GHC.Generics" builtin mechanisms.+repDatatypeName :: SRep w f -> String+repDatatypeName (S_M1 x@SM_D _)+  = getDatatypeName x+repDatatypeName (S_M1 _ x)+  = repDatatypeName x+repDatatypeName (S_L1 x)+  = repDatatypeName x+repDatatypeName (S_R1 x)+  = repDatatypeName x+repDatatypeName _+  = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"++-- |Retrieves the constructor name for a representation.+-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of+-- a type constructed with "GHC.Generics" builtin mechanisms.+repConstructorName :: SRep w f -> String+repConstructorName (S_M1 x@SM_C _)+  = getConstructorName x+repConstructorName (S_M1 _ x)+  = repConstructorName x+repConstructorName (S_L1 x)+  = repConstructorName x+repConstructorName (S_R1 x)+  = repConstructorName x+repConstructorName _+  = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"++-- |Zips two representations together if they are made up of+-- the same constructor. For example,+--+-- > zipSRep (fromS (: 1 [])) (fromS (: 2 (: 3 [])))+-- >  == Just (fromS (: (1 , 2) ([] , [3])))+-- >+-- > zipSRep (fromS (: 1 [])) (fromS [])+-- >  == Nothing+zipSRep :: SRep w f -> SRep z f -> Maybe (SRep (w :*: z) f)+zipSRep S_U1         S_U1         = return S_U1+zipSRep (S_L1 x)     (S_L1 y)     = S_L1 <$> zipSRep x y+zipSRep (S_R1 x)     (S_R1 y)     = S_R1 <$> zipSRep x y+zipSRep (S_M1 m x)   (S_M1 _ y)   = S_M1 m <$> zipSRep x y+zipSRep (x1 :**: x2) (y1 :**: y2) = (:**:) <$> (zipSRep x1 y1) <*> (zipSRep x2 y2)+zipSRep (S_K1 x)     (S_K1 y)     = return $ S_K1 (x :*: y)+zipSRep _            _            = Nothing++-- |Performs a /crush/ over the leaves of a 'SRep' carrying a constraint+-- around.+repLeavesC :: (OnLeaves c rep)+           => Proxy c+           -> (forall x . c x => w x -> r) -- ^ leaf extraction+           -> (r -> r -> r)         -- ^ join product+           -> r                     -- ^ empty+           -> SRep w rep -> r+repLeavesC _ _ _ e S_U1       = e+repLeavesC p l j e (S_L1 x)   = repLeavesC p l j e x+repLeavesC p l j e (S_R1 x)   = repLeavesC p l j e x+repLeavesC p l j e (S_M1 _ x) = repLeavesC p l j e x+repLeavesC p l j e (x :**: y) = j (repLeavesC p l j e x) (repLeavesC p l j e y)+repLeavesC _ l _ _ (S_K1 x)   = l x+repLeavesC p l j e (S_ST x)   = repLeavesC p l j e x+++-- |Performs a /crush/ over the leaves of a 'SRep'+repLeaves :: (forall x . w x -> r) -- ^ leaf extraction+          -> (r -> r -> r)         -- ^ join product+          -> r                     -- ^ empty+          -> SRep w rep -> r+repLeaves _ _ e S_U1       = e+repLeaves l j e (S_L1 x)   = repLeaves l j e x+repLeaves l j e (S_R1 x)   = repLeaves l j e x+repLeaves l j e (S_M1 _ x) = repLeaves l j e x+repLeaves l j e (x :**: y) = j (repLeaves l j e x) (repLeaves l j e y)+repLeaves l _ _ (S_K1 x)   = l x+repLeaves l j e (S_ST x)   = repLeaves l j e x++-- |Example of 'repLeaves' that places the values of @w@ inside+-- a list.+repLeavesList :: SRep w rep -> [Exists w]+repLeavesList = repLeaves ((:[]) . Exists) (++) []++-- |Maps a function over a representation taking into+-- account that the leaves of the representation satisfy+-- a given constraint.+repMapCM :: (Monad m , OnLeaves c rep)+         => Proxy c -- ^ Which constraint shall be threaded through+         -> (forall y . c y => f y -> m (g y))+         -> SRep f rep -> m (SRep g rep)+repMapCM _p _f (S_U1)     = return S_U1+repMapCM _p f  (S_K1 x)   = S_K1   <$> f x+repMapCM p  f  (S_M1 m x) = S_M1 m <$> repMapCM p f x+repMapCM p  f  (S_L1 x)   = S_L1   <$> repMapCM p f x+repMapCM p  f  (S_R1 x)   = S_R1   <$> repMapCM p f x+repMapCM p  f  (x :**: y) = (:**:) <$> repMapCM p f x <*> repMapCM p f y+repMapCM p  f  (S_ST x)   = S_ST   <$> repMapCM p f x ++-- |Maps a monadic function over the representation+repMapM :: (Monad m)+        => (forall y . f y -> m (g y))+        -> SRep f rep -> m (SRep g rep)+repMapM _f (S_U1)    = return S_U1+repMapM f (S_K1 x)   = S_K1 <$> f x+repMapM f (S_M1 m x) = S_M1 m <$> repMapM f x+repMapM f (S_L1 x)   = S_L1 <$> repMapM f x+repMapM f (S_R1 x)   = S_R1 <$> repMapM f x+repMapM f (S_ST x)   = S_ST <$> repMapM f x+repMapM f (x :**: y)+  = (:**:) <$> repMapM f x <*> repMapM f y++-- |Maps a simple functino over the representation+repMap :: (forall y . f y -> g y)+       -> SRep f rep -> SRep g rep+repMap f = runIdentity . repMapM (return . f)++--------------------------------++-- |Identity functor+newtype I x = I { unI :: x }+  deriving Eq++instance Show x => Show (I x) where+  showsPrec p (I x) = showParen (p > 10) $ showString "I " . showsPrec 11 x+instance Functor I where+  fmap f (I x) = I (f x)+instance Applicative I where+  pure        = I+  I f <*> I x = I (f x)+instance Monad I where+  I x >>= f = f x++-- |Shallow conversion between "GHC.Generics" representation+-- and 'SRep'; The 'fromS' and 'toS' functions provide the+-- toplevel api.+class GShallow f where+  sfrom :: f x -> SRep I f+  sto   :: SRep I f -> f x++instance GShallow U1 where+  sfrom U1 = S_U1+  sto S_U1 = U1++instance (GShallow f , GShallow g) => GShallow (f :+: g) where+  sfrom (L1 x) = S_L1 (sfrom x)+  sfrom (R1 x) = S_R1 (sfrom x)+  sto (S_L1 x) = L1 (sto x)+  sto (S_R1 x) = R1 (sto x)++instance (GShallow f , GShallow g) => GShallow (f :*: g) where+  sfrom (x :*:  y) = sfrom x :**: sfrom y+  sto   (x :**: y) = sto x   :*:  sto y++instance (GShallow f , GMeta i c) => GShallow (M1 i c f) where+  sfrom (M1 x)   = S_M1 smeta (sfrom x)+  sto (S_M1 _ x) = M1 (sto x)++instance GShallow (K1 R x) where+  sfrom (K1 x) = S_K1 (I x)+  sto (S_K1 (I x)) = K1 x++-- |Converts a value of a generic type directly to its+-- (shallow) simplistic representation.+fromS :: (Simplistic a) => a -> SRep I (Rep a)+fromS = sfrom . from++-- |Converts a simplistic representation back to its corresponding+-- value of type @a@.+toS :: (Simplistic a) => SRep I (Rep a) -> a+toS = to . sto++-- TODO: Study whether it makes sense to add rules+--       and inline pragmas for performance.+-- {-# RULES "sfrom/sto" forall x.  sfrom (sto x) = x #-}+-- {-# RULES "sto/sfrom" forall x.  sto (sfrom x) = x #-}++---------------------------------------+---------------------------------------+-- Representation of `* -> *` types  --+---------------------------------------+---------------------------------------++-- $simplistic1+--+-- "GHC.Generics" provides 'Rep' for types of kind @*@+-- and 'Rep1' for types of kind @* -> *@. Similarly,+-- we also provide 'SRep1' for a closed-universe interpretation+-- of 'Rep1'. It is worth noting the support is limitted and+-- we have not yet written combinators for 'SRep1' like we+-- did for 'SRep'. An example usage of 'SRep1' can be found+-- in "Generics.Simplistic.Derive.Functor".+ infixr 5 :***:++-- |Similar to 'SRep', but is indexed over the functors that+-- make up a 'Rep1', used to explicitely encode types with+-- one parameter.  data SRep1 f x where   S1_U1   ::                           SRep1 U1         x   S1_L1   ::              SRep1 f x -> SRep1 (f :+: g)  x@@ -80,12 +335,7 @@   S1_Rec  ::          f x           -> SRep1 (Rec1 f)   x   S1_Comp ::          f (SRep1 g x) -> SRep1 (f :.: g)  x -type GenericSy1 f = (Generic1 f, Sy1 (Rep1 f))--fromS1 :: (GenericSy1 f) => f a -> SRep1 (Rep1 f) a-fromS1 = fromS1' . from1-toS1 :: (GenericSy1 f) => SRep1 (Rep1 f) a -> f a-toS1 = to1 . toS1'+type Simplistic1 f = (Generic1 f, GShallow1 (Rep1 f))  type family OnLeaves1 (c :: * -> Constraint) (r :: (* -> *) -> Constraint)                       (f :: * -> *) :: Constraint where@@ -100,74 +350,48 @@   OnLeaves1 c r (Rec1 f)   = r f   OnLeaves1 c r (f :.: g)  = (r f, OnLeaves1 c r g) --- Internal instances-class SMety i t where-  smeta :: SMeta i t-instance Datatype d => SMety D d where-  smeta = SM_D-instance Constructor c => SMety C c where-  smeta = SM_C-instance Selector s => SMety S s where-  smeta = SM_S-class Sy f where-  fromS' :: Applicative w => f a -> SRep w f-  toS'   :: Comonad     w => SRep w f -> f a-instance Sy V1 where-  fromS' = undefined-  toS'   = undefined-instance Sy U1 where-  fromS' U1 = S_U1-  toS'   S_U1 = U1-instance (Sy f, Sy g) => Sy (f :+: g) where-  fromS' (L1 x) = S_L1 (fromS' x)-  fromS' (R1 y) = S_R1 (fromS' y)-  toS'   (S_L1 x) = L1 (toS' x)-  toS'   (S_R1 y) = R1 (toS' y)-instance (Sy f, Sy g) => Sy (f :*: g) where-  fromS' (x :*: y) = fromS' x :**: fromS' y-  toS'   (x :**: y) = toS' x :*: toS' y-instance Sy (K1 i a) where-  fromS' (K1 x) = S_K1 (pure x)-  toS'   (S_K1 x) = K1 (extract x)-instance (SMety i t, Sy f) => Sy (M1 i t f) where-  fromS' (M1 x) = S_M1 smeta (fromS' x)-  toS'   (S_M1 _ x) = M1 (toS' x)-instance (c => Sy f) => Sy (c :=>: f) where-  fromS' (SuchThat x) = S_ST (fromS' x)-  toS'   (S_ST x) = SuchThat (toS' x)+-- |Converts a value of a generic type directly to its+-- (shallow) simplistic1 representation with a parameter.+fromS1 :: (Simplistic1 f) => f x -> SRep1 (Rep1 f) x+fromS1 = sfrom1 . from1 -class Sy1 f where-  fromS1' :: f a -> SRep1 f a-  toS1'   :: SRep1 f a -> f a-instance Sy1 V1 where-  fromS1' = undefined-  toS1'   = undefined-instance Sy1 U1 where-  fromS1' U1 = S1_U1-  toS1'   S1_U1 = U1-instance (Sy1 f, Sy1 g) => Sy1 (f :+: g) where-  fromS1' (L1 x) = S1_L1 (fromS1' x)-  fromS1' (R1 y) = S1_R1 (fromS1' y)-  toS1'   (S1_L1 x) = L1 (toS1' x)-  toS1'   (S1_R1 y) = R1 (toS1' y)-instance (Sy1 f, Sy1 g) => Sy1 (f :*: g) where-  fromS1' (x :*: y) = fromS1' x :***: fromS1' y-  toS1'   (x :***: y) = toS1' x :*: toS1' y-instance Sy1 (K1 i a) where-  fromS1' (K1 x) = S1_K1 x-  toS1'   (S1_K1 x) = K1 x-instance (SMety i t, Sy1 f) => Sy1 (M1 i t f) where-  fromS1' (M1 x) = S1_M1 smeta (fromS1' x)-  toS1'   (S1_M1 _ x) = M1 (toS1' x)-instance (c => Sy1 f) => Sy1 (c :=>: f) where-  fromS1' (SuchThat x) = S1_ST (fromS1' x)-  toS1'   (S1_ST x) = SuchThat (toS1' x)-instance Sy1 Par1 where-  fromS1' (Par1 x) = S1_Par x-  toS1'   (S1_Par x) = Par1 x-instance Sy1 (Rec1 f) where-  fromS1' (Rec1 x) = S1_Rec x-  toS1'   (S1_Rec x) = Rec1 x-instance (Functor f, Sy1 g) => Sy1 (f :.: g) where-  fromS1' (Comp1 x) = S1_Comp (fmap fromS1' x)-  toS1'   (S1_Comp x) = Comp1 (fmap toS1' x)+-- |Converts a simplistic1 representation back to its corresponding+-- value of type @a@.+toS1 :: (Simplistic1 f) => SRep1 (Rep1 f) x -> f x+toS1 = to1 . sto1++class GShallow1 f where+  sfrom1 :: f a -> SRep1 f a+  sto1   :: SRep1 f a -> f a+instance GShallow1 V1 where+  sfrom1 = undefined+  sto1   = undefined+instance GShallow1 U1 where+  sfrom1 U1 = S1_U1+  sto1   S1_U1 = U1+instance (GShallow1 f, GShallow1 g) => GShallow1 (f :+: g) where+  sfrom1 (L1 x) = S1_L1 (sfrom1 x)+  sfrom1 (R1 y) = S1_R1 (sfrom1 y)+  sto1   (S1_L1 x) = L1 (sto1 x)+  sto1   (S1_R1 y) = R1 (sto1 y)+instance (GShallow1 f, GShallow1 g) => GShallow1 (f :*: g) where+  sfrom1 (x :*: y) = sfrom1 x :***: sfrom1 y+  sto1   (x :***: y) = sto1 x :*: sto1 y+instance GShallow1 (K1 i a) where+  sfrom1 (K1 x) = S1_K1 x+  sto1   (S1_K1 x) = K1 x+instance (GMeta i t, GShallow1 f) => GShallow1 (M1 i t f) where+  sfrom1 (M1 x) = S1_M1 smeta (sfrom1 x)+  sto1   (S1_M1 _ x) = M1 (sto1 x)+instance (c => GShallow1 f) => GShallow1 (c :=>: f) where+  sfrom1 (SuchThat x) = S1_ST (sfrom1 x)+  sto1   (S1_ST x) = SuchThat (sto1 x)+instance GShallow1 Par1 where+  sfrom1 (Par1 x) = S1_Par x+  sto1   (S1_Par x) = Par1 x+instance GShallow1 (Rec1 f) where+  sfrom1 (Rec1 x) = S1_Rec x+  sto1   (S1_Rec x) = Rec1 x+instance (Functor f, GShallow1 g) => GShallow1 (f :.: g) where+  sfrom1 (Comp1 x) = S1_Comp (fmap sfrom1 x)+  sto1   (S1_Comp x) = Comp1 (fmap sto1 x)

@@ -0,0 +1,390 @@+{-# LANGUAGE DeriveGeneric           #-}+{-# LANGUAGE QuantifiedConstraints   #-}+{-# LANGUAGE UndecidableInstances    #-}+{-# LANGUAGE UndecidableSuperClasses #-}+{-# LANGUAGE FlexibleContexts        #-}+{-# LANGUAGE FlexibleInstances       #-}+{-# LANGUAGE ConstraintKinds         #-}+{-# LANGUAGE DefaultSignatures       #-}+{-# LANGUAGE StandaloneDeriving      #-}+{-# LANGUAGE TypeOperators           #-}+{-# LANGUAGE DataKinds               #-}+{-# LANGUAGE PolyKinds               #-}+{-# LANGUAGE GADTs                   #-}+{-# LANGUAGE KindSignatures          #-}+{-# LANGUAGE PatternSynonyms         #-}+{-# LANGUAGE RankNTypes              #-}+{-# LANGUAGE TypeFamilies            #-}+{-# LANGUAGE MultiParamTypeClasses   #-}+{-# LANGUAGE ScopedTypeVariables     #-}+{-# OPTIONS_GHC -Wno-orphans         #-}+-- |Deep representation for 'SRep'+module Generics.Simplistic.Deep+  ( -- * (Co)Free (Co)Monad and its cousins+    HolesAnn(..)+  , SFix    , pattern SFix    , pattern Prim+  , SFixAnn , pattern SFixAnn , pattern PrimAnn+  , Holes   , pattern Roll    , pattern Hole+  -- ** Constraints+  , CompoundCnstr , PrimCnstr+  -- ** Coercions+  , holesToSFix , sfixToHoles+  -- ** Maps, zips and folds+  , holesMapAnn , holesMap , holesMapM , holesMapAnnM , getAnn+  , holesJoin , holesSize, holesHolesList+  , holesRefineM , holesRefineHoles , holesRefineHolesM+  , synthesize , synthesizeM , cataM+  -- ** Anti-Unification+  , lgg+  -- ** Conversion+  , Deep(..) , GDeep(..)+  ) where++import Data.Proxy+-- import qualified Data.Set as S (Set, fromList)+import Control.Monad.Identity+import Control.DeepSeq+import GHC.Generics (from , to)+import Unsafe.Coerce++import Generics.Simplistic+import Generics.Simplistic.Util++-- Useful constraints++type PrimCnstr kappa fam b+  = (Elem b kappa , NotElem b fam)++type CompoundCnstr kappa fam a+  = (Elem a fam , NotElem a kappa , Generic a)++-- |The cofree comonad and free monad on the same type;+-- this allows us to use the same recursion operator+-- for everything.+data HolesAnn kappa fam ann h a where+  Hole' :: ann a -- ^ Annotation+        -> h a -> HolesAnn kappa fam ann h a+  Prim' :: (PrimCnstr kappa fam a)+        => ann a -- ^ Annotation+        -> a -> HolesAnn kappa fam ann h a+  Roll' :: (CompoundCnstr kappa fam a)+        => ann a -- ^ Annotation+        -> SRep (HolesAnn kappa fam ann h) (Rep a)+        -> HolesAnn kappa fam ann h a++instance (All Eq kappa , EqHO h) => EqHO (Holes kappa fam h) where+  eqHO x y = all (exElim $ uncurry' go) $ holesHolesList (lgg x y)+    where+      go :: Holes kappa fam h a -> Holes kappa fam h a -> Bool+      go (Hole h1) (Hole h2) = eqHO h1 h2+      go _         _         = False++instance (All Eq kappa , EqHO h) => Eq (Holes kappa fam h t) where+   (==) = eqHO++-- |Deep representations are easily achieved by forbiding+-- the 'Hole'' constructor and providing unit annotations.+type SFix kappa fam = HolesAnn kappa fam U1 V1++pattern SFix :: () => (CompoundCnstr kappa fam a)+             => SRep (SFix kappa fam) (Rep a)+             -> SFix kappa fam a+pattern SFix x = Roll x+{-# COMPLETE SFix , Prim #-}++-- |A tree with holes has unit annotations+type Holes kappa fam = HolesAnn kappa fam U1++pattern Hole :: h a -> Holes kappa fam h a+pattern Hole x = Hole' U1 x++pattern Prim :: () => (PrimCnstr kappa fam a)+             => a -> Holes kappa fam h a+pattern Prim a = Prim' U1 a++pattern Roll :: () => (CompoundCnstr kappa fam a)+             => SRep (Holes kappa fam h) (Rep a)+             -> Holes kappa fam h a+pattern Roll x = Roll' U1 x+{-# COMPLETE Hole , Prim , Roll #-}++-- |Annotated fixpoints are also easy; forbid the 'Hole''+-- constructor but add something to every 'Roll' of+-- the representation.+type SFixAnn kappa fam ann = HolesAnn kappa fam ann V1++pattern PrimAnn :: () => (PrimCnstr kappa fam a)+                => ann a -> a -> SFixAnn kappa fam ann a+pattern PrimAnn ann a = Prim' ann a++pattern SFixAnn :: () => (CompoundCnstr kappa fam a)+                => ann a+                -> SRep (SFixAnn kappa fam ann) (Rep a)+                -> SFixAnn kappa fam ann a+pattern SFixAnn ann x = Roll' ann x+{-# COMPLETE SFixAnn , PrimAnn #-}++---------------+-- Coercions --+---------------++sfixToHoles :: SFix kappa fam at -> Holes kappa fam h at+sfixToHoles = unsafeCoerce++holesToSFix :: Holes kappa fam V1 at -> SFix kappa fam at+holesToSFix = id++------------+-- NFData --+------------++-- VCM: QUESTION: DDoes it make sense to have this here?+-- I need it in /hdiff/, and I can see how it can be useful.+-- @trupill, do you prefer to keep this or trash this?++instance (forall x . NFData (ann x) , forall x . NFData (h x))+    => NFData (HolesAnn kappa fam ann h f) where+  rnf (Prim' ann _) = rnf ann+  rnf (Hole' ann h) = rnf ann `seq` rnf h+  rnf (Roll' ann x) = rnf ann `seq` rnf x++instance NFData (V1 x) where+  rnf _ = ()++instance NFData (U1 x) where+  rnf U1 = ()++----------------------+-- Useful Functions --+----------------------++-- |Retrieves the annotation inside a 'HolesAnn';+-- this is the counit of the comonad.+getAnn :: HolesAnn kappa fam ann h a -> ann a+getAnn (Hole' ann _) = ann+getAnn (Prim' ann _) = ann+getAnn (Roll' ann _) = ann++-- TODO: swap parameters+-- |Maps over a 'HolesAnn' treating annotations and holes+-- independently.+holesMapAnnM :: (Monad m)+             => (forall x . f x   -> m (g x)) -- ^ Function to transform holes+             -> (forall x . ann x -> m (psi x)) -- ^ Function to transform annotations+             -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam psi g a)+holesMapAnnM f g (Hole' a x)   = Hole' <$> g a <*> f x+holesMapAnnM _ g (Prim' a x)   = flip Prim' x <$> g a+holesMapAnnM f g (Roll' a x) = Roll' <$> g a <*> repMapM (holesMapAnnM f g) x++-- |Maps over 'HolesAnn' maintaining annotations intact.+holesMapM :: (Monad m)+          => (forall x . f x -> m (g x))+          -> HolesAnn kappa fam ann f a -> m (HolesAnn kappa fam ann g a)+holesMapM f = holesMapAnnM f return++-- |Maps over the holes in a 'HolesAnn'+holesMap :: (forall x . f x -> g x)+         -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam ann g a+holesMap f = runIdentity . holesMapM (return . f)++-- |Maps over holes and annotations in a 'HolesAnn'+holesMapAnn :: (forall x . f   x -> g x)+            -> (forall x . ann x -> phi x)+            -> HolesAnn kappa fam ann f a -> HolesAnn kappa fam phi g a+holesMapAnn f g = runIdentity . holesMapAnnM (return . f) (return . g)++-- |Monadic multiplication+holesJoin :: HolesAnn kappa fam ann (HolesAnn kappa fam ann f) a+          -> HolesAnn kappa fam ann f a+holesJoin (Hole' _ x) = x+holesJoin (Prim' a x) = Prim' a x+holesJoin (Roll' a x) = Roll' a (repMap holesJoin x)++-- |Computes the list of holes in a 'HolesAnn'+holesHolesList :: HolesAnn kappa fam ann f a -> [Exists f]+holesHolesList (Hole' _ x) = [Exists x]+holesHolesList (Prim' _ _) = []+holesHolesList (Roll' _ x) = concatMap (exElim holesHolesList) $ repLeavesList x++{-+holesHolesSet :: (Ord (Exists f)) => Holes kappa fam f a -> S.Set (Exists f)+holesHolesSet = S.fromList . holesHolesList+-}++-- TODO: Implement holesMap in terms of refine; its much better!++-- |Refines holes using a monadic action+holesRefineHolesM :: (Monad m)+                  => (forall b . f b -> m (Holes kappa fam g b))+                  -> Holes kappa fam f a+                  -> m (Holes kappa fam g a)+holesRefineHolesM f = fmap holesJoin . holesMapM f++-- |Refine holes with a simple action+holesRefineHoles :: (forall b . f b -> Holes kappa fam g b)+                 -> Holes kappa fam f a+                 -> Holes kappa fam g a+holesRefineHoles f = holesJoin . runIdentity . holesMapM (return . f)++-- |Refine holes and primitives+holesRefineM :: (Monad m)+             => (forall b . f b -> m (Holes kappa fam g b))+             -> (forall b . (PrimCnstr kappa fam b)+                  => b -> m (Holes kappa fam g b))+             -> Holes kappa fam f a+             -> m (Holes kappa fam g a)+holesRefineM f _ (Hole x) = f x+holesRefineM _ g (Prim x) = g x+holesRefineM f g (Roll x) = Roll <$> repMapM (holesRefineM f g) x++-- |Counts how many 'Prim's and 'Roll's are inside a 'HolesAnn'.+holesSize :: HolesAnn kappa fam ann h a -> Int+holesSize (Hole' _ _) = 0+holesSize (Prim' _ _) = 1+holesSize (Roll' _ x) = 1 + sum (map (exElim holesSize) $ repLeavesList x)++-- |Catamorphism over 'HolesAnn'+cataM :: (Monad m)+      => (forall b . (CompoundCnstr kappa fam b)+            => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion+      -> (forall b . (PrimCnstr kappa fam b)+            => ann b -> b -> m (phi b)) -- ^ How to handle primitivies+      -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes+      -> HolesAnn kappa fam ann h a+      -> m (phi a)+cataM f g h (Roll' ann x) = repMapM (cataM f g h) x >>= f ann+cataM _ g _ (Prim' ann x) = g ann x+cataM _ _ h (Hole' ann x) = h ann x++-- |Synthetization of attributes+synthesizeM :: (Monad m)+            => (forall b . (CompoundCnstr kappa fam b)+                  => ann b -> SRep phi (Rep b) -> m (phi b)) -- ^ How to handle recursion+            -> (forall b . (PrimCnstr kappa fam b)+                  => ann b -> b -> m (phi b)) -- ^ How to handle primitives+           -> (forall b . ann b -> h b -> m (phi b)) -- ^ How to handle holes+            -> HolesAnn kappa fam ann h a+            -> m (HolesAnn kappa fam phi h a)+synthesizeM f g h = cataM (\ann r -> flip Roll' r+                                <$> f ann (repMap getAnn r))+                          (\ann b -> flip Prim' b <$> g ann b)+                          (\ann r -> flip Hole' r <$> h ann r)++-- |Simpler version of 'synthesizeM' working over the /Identity/ monad.+synthesize :: (forall b . (CompoundCnstr kappa fam b)+                 => ann b -> SRep phi (Rep b) -> phi b)+           -> (forall b . (PrimCnstr kappa fam b)+                 => ann b -> b -> phi b)+           -> (forall b . ann b -> h b -> phi b)+           -> HolesAnn kappa fam ann h a+           -> HolesAnn kappa fam phi h a+synthesize f g h = runIdentity+                 . synthesizeM (\ann -> return . f ann)+                               (\ann -> return . g ann)+                               (\ann -> return . h ann)++-- Anti unification is so simple it doesn't+-- deserve its own module++-- |Computes the /least general generalization/ of two+-- trees.+lgg :: forall kappa fam h i a+     . (All Eq kappa)+    => Holes kappa fam h a -> Holes kappa fam i a+    -> Holes kappa fam (Holes kappa fam h :*: Holes kappa fam i) a+lgg (Prim x) (Prim y)+  | weq (Proxy :: Proxy kappa) x y = Prim x+  | otherwise                      = Hole (Prim x :*: Prim y)+lgg x@(Roll rx) y@(Roll ry) =+  case zipSRep rx ry of+    Nothing -> Hole (x :*: y)+    Just r  -> Roll (repMap (uncurry' lgg) r)+lgg x y = Hole (x :*: y)++----------------------+-- Deep translation --+----------------------++{- It is possible to have a simler GDeep; relying on+-- GShallow. I'll test performance later.++class GDeep' fam prim isPrim a where+  gdfrom'  :: Proxy isPrim -> a -> SFix fam prim a+  gdto'    :: Proxy isPrim -> SFix fam prim a -> a++instance (CompoundCnstr fam prim a , GDeep fam prim a)+     => GDeep' fam prim 'False a where+  gdfrom' _ a = gdfrom $ a+  gdto' _   x = gdto x++instance (PrimCnstr fam prim a) => GDeep' fam prim 'True a where+  gdfrom' _ a = Prim a+  gdto'   _ (Prim a) = a++class GDeep fam prim a where+  gdfrom :: a -> SFix fam prim a+  gdto   :: SFix fam prim a -> a++instance GDeep' fam prim (IsElem a prim) a => GDeep fam prim a where+  gdfrom = gdfrom' (Proxy :: Proxy (IsElem a prim))+  gdto   = gdto'   (Proxy :: Proxy (IsElem a prim))++dfrom :: forall fam prim a+       . (CompoundCnstr fam prim a)+      => a -> SFix fam prim a+dfrom = SFix+      . runIdentity+      . repMapCM (Proxy :: Proxy (GDeep fam prim))+         (\(I x) -> return $ gdfrom x)+      . fromS++-}++class (CompoundCnstr kappa fam a) => Deep kappa fam a where+  dfrom :: a -> SFix kappa fam a+  default dfrom :: (GDeep kappa fam (Rep a)) => a -> SFix kappa fam a+  dfrom = SFix . gdfrom . from++  dto :: SFix kappa fam a -> a+  default dto :: (GDeep kappa fam (Rep a)) => SFix kappa fam a -> a+  dto (SFix x) = to . gdto $ x++class GDeep kappa fam f where+  gdfrom :: f x -> SRep (SFix kappa fam) f+  gdto   :: SRep (SFix kappa fam) f -> f x++class GDeepAtom kappa fam (isPrim :: Bool) a where+  gdfromAtom  :: Proxy isPrim -> a -> SFix kappa fam a+  gdtoAtom    :: Proxy isPrim -> SFix kappa fam a -> a++instance (CompoundCnstr kappa fam a , Deep kappa fam a)+     => GDeepAtom kappa fam 'False a where+  gdfromAtom _ a = dfrom $ a+  gdtoAtom _   x = dto x++instance (PrimCnstr kappa fam a) => GDeepAtom kappa fam 'True a where+  gdfromAtom _ a = Prim a+  gdtoAtom   _ (Prim a) = a++instance (GDeepAtom kappa fam (IsElem a kappa) a) => GDeep kappa fam (K1 R a) where+  gdfrom (K1 a)   = S_K1 (gdfromAtom (Proxy :: Proxy (IsElem a kappa)) a)+  gdto   (S_K1 a) = K1 (gdtoAtom (Proxy :: Proxy (IsElem a kappa)) a)++instance GDeep kappa fam U1 where+  gdfrom U1  = S_U1+  gdto S_U1 = U1++instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :*: g) where+  gdfrom (x :*: y) = (gdfrom x) :**: (gdfrom y)+  gdto (x :**: y) = (gdto x) :*: (gdto y)++instance (GDeep kappa fam f , GDeep kappa fam g) => GDeep kappa fam (f :+: g) where+  gdfrom (L1 x) = S_L1 (gdfrom x)+  gdfrom (R1 x) = S_R1 (gdfrom x)++  gdto (S_L1 x) = L1 (gdto x)+  gdto (S_R1 x) = R1 (gdto x)++instance (GMeta i c , GDeep kappa fam f) => GDeep kappa fam (M1 i c f) where+  gdfrom (M1 x)   = S_M1 smeta (gdfrom x)+  gdto (S_M1 _ x) = M1 (gdto x)

@@ -0,0 +1,315 @@+{-# LANGUAGE TypeOperators      #-}+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE DeriveFunctor      #-}+{-# LANGUAGE TupleSections      #-}+{-# LANGUAGE TemplateHaskell    #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE CPP                #-}+-- |This module provides some Template Haskell functionality to+-- help out the declaration of 'Deep' instances.+--+-- Note that we chose to not automate the whole process on purpose.+-- Sometimes the user will need to define standalone 'Generic'+-- instances for some select types in the family, some other times+-- the user might want better control over naming, for example.+-- Consequently, the most adaptable option is to provide+-- two TH utilities:+--+-- 1. Unfolding a family into a list of types until a fixpoint is reached,+-- given in 'unfoldFamilyInto'+-- 2. Declaring 'Deep' for a list of types, given in 'declareDeepFor'+--+-- The stepts in between unfolding the family and declaring 'Deep' vary+-- too much from case to case and hence, must be manually executed.+-- Let us run through  a simple example, which involves mutual+-- recursion and type synonyms in the AST of a pseudo-language.+--+-- > data Stmt var+-- >   = SAssign var (Exp var)+-- >   | SIf     (Exp var) (Stmt var) (Stmt var)+-- >   | SSeq    (Stmt var) (Stmt var)+-- >   | SReturn (Exp var)+-- >   | SDecl (Decl var)+-- >   | SSkip+-- >   deriving (Show, Generic)+-- >+-- > data ODecl var+-- >   = DVar var+-- >   | DFun var var (Stmt var)+-- >   deriving (Show, Generic)+-- >+-- > type Decl x = TDecl x+-- > type TDecl x = ODecl x+-- >+-- > data Exp var+-- >   = EVar  var+-- >   | ECall var (Exp var)+-- >   | EAdd (Exp var) (Exp var)+-- >   | ESub (Exp var) (Exp var)+-- >   | ELit Int+-- >   deriving (Show, Generic)+--+-- Now say we want to use some code written with /generics-simplistic/+-- over these datatypes above. We must declare the 'Deep'+-- instances for the types in the family and "GHC.Generics"+-- takes care of the rest.+--+-- The first step is in defining @Prim@ and @Fam@, which+-- will be type-level lists with the primitive types and the non-primitive,+-- or compound, types.+--+-- An easy way to gather /all/ types involved in the family is with+-- 'unfoldFamilyInto', like:+--+-- > unfoldFamilyInto "stmtFam" [t| Stmt Int |]+--+-- The call above will be expanded into:+--+-- > stmtFam :: [String]+-- > stmtFam = ["Generics.Simplistic.Example.Exp Int"+-- >           ,"Generics.Simplistic.Example.ODecl Int"+-- >           ,"Generics.Simplistic.Example.Stmt Int"+-- >           ,"Int"+-- >           ]+--+-- Which can then be inspected with GHCi and, with+-- some elbow-grease (or test-editting macros!) we can+-- easily generate the necessary type-level lists:+--+-- > type Fam = '[Generics.Simplistic.Example.Exp Int+-- >             ,Generics.Simplistic.Example.ODecl Int+-- >             ,Generics.Simplistic.Example.Stmt Int+-- >             ]+-- >+-- > type Prim = '[Int]+--+-- Finally, we are ready to call 'deriveDeepFor' and get+-- the instances declared.+--+-- > deriveDeepFor ''Prim ''Fam+--+-- The TH code above expands to:+--+-- > instance Deep Prim Fam (Exp Int)+-- > instance Deep Prim Fam (ODecl Int)+-- > instance Deep Prim Fam (Stmt Int)+--+-- This workflow is crucial to be able to work+-- with large mutually recursive families, and it becomes+-- especially easy if coupled with+-- a text editor with good macro support (read emacs and vim).+--+module Generics.Simplistic.Deep.TH+  ( unfoldFamilyInto+  , deriveDeepFor+  , deriveInstancesWith+  ) where++import Control.Monad.State+import Control.Arrow ((***))++import Language.Haskell.TH hiding (match)+import Language.Haskell.TH.Syntax hiding (lift)++import qualified Data.Set as S++import Generics.Simplistic.Deep++-- |Lists all the necessary types that should+-- have 'Generic' and 'Deep' instances. For example,+--+-- > data Rose2 a b = Fork (Either a b) [Rose2 a b]+-- > unfoldFamilyInto 'rose2tys [t| Rose2 Int Char |]+--+-- Will yield the following code:+--+-- > rose2tys :: String+-- > rose2tys = [ "Rose2 Int Char"+-- >            , "Either Int Char"+-- >            , "[Rose2 Int Char]"+-- >            , "Int"+-- >            , "Char"+-- >            ]+--+-- You should then use some elbow grease or your favorite text editor+-- and its provided macro functionality to produce:+--+-- > type Rose2Prim = '[Int , Char]+-- > type Rose2Fam  = '[Rose2 Int Char , Either Int Char , [Rose2 Int Char]]+-- > deriving instance Generic (Rose2 Int Char)+-- > deriving instance Generic (Either Int Char)+-- > instance Deep Rose2Prim Rose2Fam (Rose2 Int Char)+-- > instance Deep Rose2Prim Rose2Fam (Either Int Char)+-- > instance Deep Rose2Prim Rose2Fam [Rose2 Int Char]+--+-- Note that types like @Int@ will appear fully qualified,+-- this will need some renaming.+unfoldFamilyInto :: String -> Q Type -> Q [Dec]+unfoldFamilyInto n first = do+  ty <- first >>= convertType+  allTys <- S.toList <$> execStateT (process ty) S.empty+  listStr <- [t| [String] |]+  return [ SigD (mkName n) listStr+         , FunD (mkName n) [Clause [] (NormalB $ mkExp allTys) []]+         ]+ where+   mkExp :: [STy] -> Exp+   mkExp = ListE . map (LitE . StringL . show . ppr . trevnocType)++-- |Given two type-level lists @Prims@ and @Fam@, will generate+-- @instance Deep Prim Fam f@ for every @f@ in @Fam@.+deriveDeepFor :: Name -> Name -> Q [Dec]+deriveDeepFor pr fam =+  let qprim = return $ ConT pr+      qfam  = return $ ConT fam+   in deriveInstancesWith (\t -> [t| Deep $(qprim) $(qfam) $(return t) |]) fam++-- |Given a function @f@ and a type level stored in @fam@,+-- 'deriveInstacesWith' will generate:+--+-- > instance f x+--+-- for each @x@ in @fam@. This function is mostly internal,+-- please check 'deriveDeepFor' and 'deriveGenericFor'.+deriveInstancesWith :: (Type -> Q Type) -- ^ Instance to derive+                    -> Name -- ^ fam+                    -> Q [Dec]+deriveInstancesWith f fam = do+  tys <- getTypeLevelList fam+  forM tys $ \ty -> do+    instTy <- f ty+    return $ InstanceD Nothing [] instTy []+++getTypeLevelList :: Name -> Q [Type]+getTypeLevelList x = do+  mtyDecl <- reifyDec x+  case mtyDecl of+    Nothing              -> fail ("Not a type declaration: " ++ show (ppr x))+    Just (TySynD _ _ ty) -> getTyLL ty+    Just d -> fail ("Not a type-level list: " ++ show (ppr x) ++ show (ppr d))+ where+   getTyLL :: Type -> Q [Type]+   getTyLL (SigT t _) = getTyLL t+   getTyLL PromotedNilT = return []+   getTyLL (AppT (AppT PromotedConsT a) as) = (a:) <$> getTyLL as+   getTyLL t = fail ("Not a type-level list: " ++ show (ppr x) ++ "; " ++ show t)++process :: STy -> StateT (S.Set STy) Q ()+process ty = do+  tys <- get+  if ty `S.member` tys+  then return ()+  else do+    let (tyHd , args) = styFlatten ty+    case tyHd of+      ConST tyName -> do+        tyDecl <- lift (reifyDec tyName)+        case tyDecl of+          Just dec -> processDecl dec args+          Nothing  -> return ()+      _ -> fail "Invalid type"++processDecl :: Dec -> [STy] -> StateT (S.Set STy) Q ()+processDecl (DataD _ tyName vars _ cons _) args = do+  modify (S.insert (styApp tyName args))+  let argVal = zip (map tyvarName vars) args+  mapM_ (processCon argVal) cons+processDecl (NewtypeD _ tyName vars _ con _) args = do+  modify (S.insert (styApp tyName args))+  let argVal = zip (map tyvarName vars) args+  processCon argVal con+processDecl (TySynD _ vars ty) args = do+  sty <- convertType ty+  let argVal = zip (map tyvarName vars) args+  process (styReduce argVal sty)+processDecl _ _+  = fail "unknown decl"++processCon :: [(Name , STy)] -> Con -> StateT (S.Set STy) Q ()+processCon argVal con = do+  fields <- mapM (fmap (styReduce argVal) . convertType) (conType con)+  mapM_ process fields++tyvarName :: TyVarBndr -> Name+tyvarName (PlainTV n) = n+tyvarName (KindedTV n _) = n++vbtyTy :: VarBangType -> Type+vbtyTy (_ , _ , t) = t++btyTy :: BangType -> Type+btyTy (_ , t) = t++conType :: Con -> [Type]+conType (NormalC _ btys)     = map btyTy btys+conType (RecC _ vbtys)       = map vbtyTy vbtys+conType (InfixC tyl _ tyr)   = map btyTy [tyl , tyr]+conType (ForallC _ _ c)      = conType c+conType (GadtC _ btys _)     = map btyTy btys+conType (RecGadtC _ vbtys _) = map vbtyTy vbtys++----------------------++data STy+  = AppST STy STy+  | VarST Name+  | ConST Name+  deriving (Eq , Show, Ord)++#if __GLASGOW_HASKELL__ >= 808+convertType :: (MonadFail m) => Type -> m STy+#else+convertType :: (Monad m) => Type -> m STy+#endif+convertType (AppT a b)  = AppST <$> convertType a <*> convertType b+convertType (SigT t _)  = convertType t+convertType (VarT n)    = return (VarST n)+convertType (ConT n)    = return (ConST n)+convertType (ParensT t) = convertType t+convertType ListT       = return (ConST (mkName "[]"))+convertType (TupleT n)  = return (ConST (mkName $ '(':replicate (n-1) ',' ++ ")"))+convertType t           = fail ("convertType: Unsupported Type: " ++ show t)++trevnocType :: STy -> Type+trevnocType (AppST a b) = AppT (trevnocType a) (trevnocType b)+trevnocType (VarST n)   = VarT n+trevnocType (ConST n)+  | n == mkName "[]" = ListT+  | isTupleN n       = TupleT $ length (show n) - 1+  | otherwise        = ConT n+  where isTupleN n0 = take 2 (show n0) == "(,"++-- |Handy substitution function.+--+--  @stySubst t m n@ substitutes m for n within t, that is: t[m/n]+stySubst :: STy -> Name -> STy -> STy+stySubst (AppST a b) m n = AppST (stySubst a m n) (stySubst b m n)+stySubst (ConST a)   _ _ = ConST a+stySubst (VarST x)   m n+  | x == m    = n+  | otherwise = VarST x++-- |Just like subst, but applies a list of substitutions+styReduce :: [(Name , STy)] -> STy -> STy+styReduce parms t = foldr (\(n , m) ty -> stySubst ty n m) t parms++-- |Flattens an application into a list of arguments;+--+--  @styFlatten (AppST (AppST Tree A) B) == (Tree , [A , B])@+styFlatten :: STy -> (STy , [STy])+styFlatten (AppST a b) = id *** (++ [b]) $ styFlatten a+styFlatten sty         = (sty , [])++styApp :: Name -> [STy] -> STy+styApp name args = go (ConST name) (reverse args)+  where go t [] = t+        go t (x:xs) = AppST (go t xs) x++-- * Parsing Haskell's AST++reifyDec :: Name -> Q (Maybe Dec)+reifyDec name =+  do info <- reify name+     case info of TyConI dec -> return (Just dec)+                  _          -> return Nothing

@@ -1,23 +1,21 @@-{-# language GADTs,-             TypeFamilies,-             ConstraintKinds,-             TypeOperators,-             FlexibleContexts #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE TypeFamilies     #-}+{-# LANGUAGE ConstraintKinds  #-}+{-# LANGUAGE TypeOperators    #-}+{-# LANGUAGE FlexibleContexts #-} module Generics.Simplistic.Derive.Eq where -import Data.Functor.Identity+import Data.Proxy+ import Generics.Simplistic+import Generics.Simplistic.Util -geq :: (Applicative w, OnLeaves Eq f)-    => SRep w f -> SRep w f -> w Bool-geq S_U1       S_U1       = pure True-geq (S_L1 x)   (S_L1 y)   = geq x y-geq (S_R1 x)   (S_R1 y)   = geq x y-geq (x :**: y) (u :**: v) = (&&) <$> geq x u <*> geq y v-geq (S_K1 x)   (S_K1 y)   = (==) <$> x <*> y-geq (S_M1 _ x) (S_M1 _ y) = geq x y-geq (S_ST x)   (S_ST y)   = geq x y-geq _          _          = pure False+geq' :: (OnLeaves Eq f) => SRep I f -> SRep I f -> Bool+geq' x y = maybe False sameLeaves $ zipSRep x y+  where+    sameLeaves :: (OnLeaves Eq f) => SRep (I :*: I) f -> Bool+    sameLeaves = repLeavesC (Proxy :: Proxy Eq) (uncurry' (==)) (&&) True -geq' :: (GenericSy a, OnLeaves Eq (Rep a)) => a -> a -> Bool-geq' x y = runIdentity $ geq (fromS x) (fromS y)+geq :: (Generic a, GShallow (Rep a), OnLeaves Eq (Rep a))+    => a -> a -> Bool+geq x y = geq' (fromS x) (fromS y)

@@ -1,23 +1,29 @@-{-# language GADTs,-             TypeOperators,-             FlexibleContexts #-}+{-# LANGUAGE GADTs            #-}+{-# LANGUAGE TypeOperators    #-}+{-# LANGUAGE FlexibleContexts #-} module Generics.Simplistic.Derive.Functor where  import Generics.Simplistic -gfmap :: OnLeaves1 Trivial Functor f+-- TODO: Abstract this away as a repMap1++-- |'SRep1' is a functor+gfmap' :: OnLeaves1 Trivial Functor f       => (a -> b) -> SRep1 f a -> SRep1 f b-gfmap _ S1_U1       = S1_U1-gfmap f (S1_L1 x)   = S1_L1 (gfmap f x)-gfmap f (S1_R1 x)   = S1_R1 (gfmap f x)-gfmap f (x :***: y) = gfmap f x :***: gfmap f y-gfmap f (S1_K1 x)   = S1_K1 x-gfmap f (S1_M1 i x) = S1_M1 i (gfmap f x)-gfmap f (S1_ST x)   = S1_ST (gfmap f x)-gfmap f (S1_Par  x) = S1_Par (f x)-gfmap f (S1_Rec  x) = S1_Rec (fmap f x)-gfmap f (S1_Comp x) = S1_Comp (fmap (gfmap f) x)+gfmap' _ S1_U1       = S1_U1+gfmap' f (S1_L1 x)   = S1_L1 (gfmap' f x)+gfmap' f (S1_R1 x)   = S1_R1 (gfmap' f x)+gfmap' f (x :***: y) = gfmap' f x :***: gfmap' f y+gfmap' _ (S1_K1 x)   = S1_K1 x+gfmap' f (S1_M1 i x) = S1_M1 i (gfmap' f x)+gfmap' f (S1_ST x)   = S1_ST (gfmap' f x)+gfmap' f (S1_Par  x) = S1_Par (f x)+gfmap' f (S1_Rec  x) = S1_Rec (fmap f x)+gfmap' f (S1_Comp x) = S1_Comp (fmap (gfmap' f) x) -gfmap' :: (GenericSy1 f, OnLeaves1 Trivial Functor (Rep1 f))-       => (a -> b) -> f a -> f b-gfmap' f x = toS1 $ gfmap f $ fromS1 x+-- |The action of f over arrows can be obtained by translating+-- into the generic representation, using the generic+-- 'gfmap'' and translating back to regular representation.+gfmap :: (Simplistic1 f, OnLeaves1 Trivial Functor (Rep1 f))+      => (a -> b) -> f a -> f b+gfmap f = toS1 . gfmap' f . fromS1

@@ -1,43 +1,42 @@-{-# language GADTs,-             TypeFamilies,-             ConstraintKinds,-             TypeOperators,-             FlexibleContexts,-             ScopedTypeVariables,-             DeriveGeneric #-}-module Generics.Simplistic.Derive.Show where+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE TypeFamilies        #-}+{-# LANGUAGE ConstraintKinds     #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveGeneric       #-}+-- |Derives a generic show, for example+--+-- > data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic+-- > +-- > myListValue :: MyList Integer+-- > myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil))+-- > +-- > instance Show a => Show (MyList a) where+-- >   show = gshow+--+-- The code here was adapted from `generic-deriving`+-- https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs+module Generics.Simplistic.Derive.Show (gshow , gshowsPrec) where -import Data.Functor.Identity import Generics.Simplistic import GHC.Generics --- An example-data MyList a = MyNil | MyCons { hd :: a, tl :: MyList a } deriving Generic--myListValue :: MyList Integer-myListValue = MyCons 1 (MyCons 2 (MyCons 3 MyNil))--instance Show a => Show (MyList a) where-  show = gshow---- Translated from `generic-deriving`--- https://github.com/dreixel/generic-deriving/blob/master/src/Generics/Deriving/Show.hs- appPrec :: Int appPrec = 2  data Type = Rec | Tup | Pref | Inf String -gshow :: (GenericSy t, OnLeaves Show (Rep t))+gshow :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t))       => t -> String gshow v = gshowsPrec Pref 0 v "" -gshowsPrec :: (GenericSy t, OnLeaves Show (Rep t))+gshowsPrec :: (Generic t, GShallow (Rep t), OnLeaves Show (Rep t))            => Type -> Int -> t -> ShowS gshowsPrec t n v = gshowsPrec' t n (fromS v)  gshowsPrec' :: (OnLeaves Show f)-            => Type -> Int -> SRep Identity f -> ShowS+            => Type -> Int -> SRep I f -> ShowS -- "Simple" cases gshowsPrec' _ _ S_U1       = id gshowsPrec' t n (S_L1 x)   = gshowsPrec' t n x@@ -54,7 +53,7 @@ gshowsPrec' t@Pref    n (a :**: b) =   gshowsPrec' t (n+1) a . showChar ' '    . gshowsPrec' t (n+1) b -- The case of metadata-gshowsPrec' t n (S_M1 (SM_C :: SMeta i c) (x :: SRep Identity f)) = +gshowsPrec' _ n (S_M1 (SM_C :: SMeta i c) (x :: SRep I f)) =    case fixity of     Prefix    -> showParen (n > appPrec && not (isNullary x))                   ( showString (conName c)@@ -78,7 +77,7 @@           conIsTuple y = tupleName (conName y) where             tupleName ('(':',':_) = True             tupleName _ = False-gshowsPrec' t n (S_M1 (SM_S :: SMeta i c) (x :: SRep Identity f)) +gshowsPrec' t n (S_M1 (SM_S :: SMeta i c) (x :: SRep I f))    | selName s == "" = --showParen (n > appPrec)                       (gshowsPrec' t n x)   | otherwise       =   showString (selName s)@@ -87,12 +86,12 @@     where s :: M1 S c f () = undefined gshowsPrec' t n (S_M1 _ x) = gshowsPrec' t n x -isNullary :: SRep Identity a -> Bool+isNullary :: SRep I a -> Bool isNullary S_U1       = True-isNullary (S_L1 x)   = error "unnecessary case"-isNullary (S_R1 x)   = error "unnecessary case"-isNullary (x :**: y) = False-isNullary (S_K1 x)   = False+isNullary (S_L1 _)   = error "unnecessary case"+isNullary (S_R1 _)   = error "unnecessary case"+isNullary (_ :**: _) = False+isNullary (S_K1 _)   = False isNullary (S_M1 t x) = case t of                          SM_S -> isNullary x                          _    -> error "unnecessary case"

@@ -0,0 +1,289 @@+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE TupleSections         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+-- |Constraint-based unification algorithm for 'Holes'+module Generics.Simplistic.Unify+  ( -- * Substitution+    Subst , substEmpty , substInsert , substLkup , substApply+    -- * Unification+  , UnifyErr(..) , unify , unify_ , unifyWith , minimize+  ) where++import           Data.List (sort)+import qualified Data.Map as M+import           Control.Monad.Except+import           Control.Monad.State+import           Control.Monad.Writer hiding (All)+import           Control.Monad.Cont+import           Unsafe.Coerce++import Generics.Simplistic.Deep+import Generics.Simplistic.Util++-- |Unification can return succesfully or find either+-- a 'OccursCheck' failure or a 'SymbolClash' failure.+data UnifyErr kappa fam phi :: * where+  -- |The occurs-check fails when the variable in question+  -- occurs within the term its supposed to be unified with.+  OccursCheck :: [Exists phi]+              -> UnifyErr kappa fam phi+  -- |A symbol-clash is thrown when the head of the+  -- two terms is different and neither is a variabe.+  SymbolClash :: Holes    kappa fam phi at+              -> Holes    kappa fam phi at+              -> UnifyErr kappa fam phi++-- |A substitution is but a map; the existential quantifiers are+-- necessary to ensure we can reuse from "Data.Map"+--+-- Note that we must be able to compare @Exists phi@. This+-- comparison needs to work heterogeneously and it must+-- return 'EQ' only when the contents are in fact equal.+-- Even though we only need this instance for "Data.Map"+--+-- A typical example for @phi@ is @Const Int at@, representing+-- a variable. The @Ord@ instance would then be:+--+-- > instance Ord (Exists (Const Int)) where+-- >   compare (Exists (Const x)) (Exists (Const y))+-- >     = compare x y+--+type Subst kappa fam phi+  = M.Map (Exists phi) (Exists (Holes kappa fam phi))++-- |Empty substitution+substEmpty :: Subst kappa fam phi+substEmpty = M.empty++-- |Looks a value up in a substitution, see 'substInsert'+substLkup :: (Ord (Exists phi))+          => Subst kappa fam phi -- ^+          -> phi at+          -> Maybe (Holes kappa fam phi at)+substLkup sigma var =+  case M.lookup (Exists var) sigma of+    Nothing         -> Nothing+    -- In case we found something, it must be of the same+    -- type as what we got because we only insert+    -- well-typed things.+    -- TODO: Use our sameTy method to remove the unsafeCoerce+    Just (Exists t) -> Just $ unsafeCoerce t++-- |Applies a substitution to a term once; Variables not in the+-- support of the substitution are left untouched.+substApply :: (Ord (Exists phi))+           => Subst kappa fam phi -- ^+           -> Holes kappa fam phi at+           -> Holes kappa fam phi at+substApply sigma = holesJoin+                 . holesMap (\v -> maybe (Hole v) id $ substLkup sigma v)++-- |Inserts a point in a substitution. Note how the index of+-- @phi@ /must/ match the index of the term being inserted.+-- This is important when looking up terms because we must+-- 'unsafeCoerce' the existential type variables to return.+--+-- Please, always use this insertion function; or, if you insert+-- by hand, ensure thetype indices match.+substInsert :: (Ord (Exists phi))+            => Subst kappa fam phi -- ^+            -> phi at+            -> Holes kappa fam phi at+            -> Subst kappa fam phi+substInsert sigma v x = M.insert (Exists v) (Exists x) sigma++-- |Unification is done in a monad.+type UnifyM kappa fam phi+  = StateT (Subst kappa fam phi) (Except (UnifyErr kappa fam phi))++-- |Attempts to unify two 'Holes', but ignores+-- which error happened when they could not be unified.+unify_ :: (All Eq kappa , Ord (Exists phi) , EqHO phi)+       => Holes kappa fam phi at -- ^+       -> Holes kappa fam phi at+       -> Maybe (Subst kappa fam phi)+unify_ a = either (const Nothing) Just+         . runExcept . unify a++-- |Attempts to unify two 'Holes'+unify :: (All Eq kappa , Ord (Exists phi) , EqHO phi)+      => Holes kappa fam phi at -- ^+      -> Holes kappa fam phi at+      -> Except (UnifyErr kappa fam phi)+                (Subst kappa fam phi)+unify = unifyWith substEmpty++-- |Attempts to unify two 'Holes' with an already existing+-- substitution+unifyWith :: (All Eq kappa , Ord (Exists phi) , EqHO phi)+          => Subst kappa fam phi -- ^ Starting subst+          -> Holes kappa fam phi at+          -> Holes kappa fam phi at+          -> Except (UnifyErr kappa fam phi)+                    (Subst kappa fam phi)+unifyWith sigma x y = execStateT (unifyM x y) sigma++-- Actual unification algorithm; In order to improve efficiency,+-- we first register all equivalences we need to satisfy,+-- then on 'mininize' we do the occurs-check.+unifyM :: forall kappa fam phi at+        . (All Eq kappa , EqHO phi , Ord (Exists phi)) +       => Holes kappa fam phi at+       -> Holes kappa fam phi at+       -> UnifyM kappa fam phi ()+unifyM x y = do+  _ <- getEquivs x y+  s <- get+  case minimize s of+    Left vs  -> throwError (OccursCheck vs)+    Right s' -> put s'+  where+    getEquivs :: Holes kappa fam phi b+              -> Holes kappa fam phi b+              -> UnifyM kappa fam phi ()+    getEquivs p q = void $ holesMapM (uncurry' getEq) (lgg p q)+    +    getEq :: Holes kappa fam phi b+          -> Holes kappa fam phi b+          -> UnifyM kappa fam phi (Holes kappa fam phi b)+    getEq p (Hole var)   = record_eq var p >> return p+    getEq p@(Hole var) q = record_eq var q >> return p+    getEq p q | eqHO p q   = return p+              | otherwise  = throwError (SymbolClash p q)+           +    -- Whenever we see a variable being matched against a term+    -- we record the equivalence. First we make sure we did not+    -- record such equivalence yet, otherwise, we recursively thin+    record_eq :: phi b -> Holes kappa fam phi b -> UnifyM kappa fam phi ()+    record_eq var q = do+      sigma <- get+      case substLkup sigma var of+        -- First time we see 'var', we instantiate it and get going.+        Nothing -> when (not $ eqHO q (Hole var))+                 $ modify (\s -> substInsert s var q)+        -- It's not the first time we thin 'var'; previously, we had+        -- that 'var' was supposed to be p'. We will check whether it+        -- is the same as q, if not, we will have to thin p' with q.+        Just q' -> unless (eqHO q' q)+                 $ void $ getEquivs q q'+          ++-- |The minimization step performs the /occurs check/ and removes+--  unecessary steps, returning an idempodent substitution when+--  successful. For example;+--+--  > sigma = fromList+--  >           [ (0 , bin 1 2)+--  >           , (1 , bin 4 4) ]+--+-- Then, @minimize sigma@ will return @fromList [(0 , bin (bin 4 4) 2) , (1 , bin 4 4)]@+-- This returns @Left vs@ if occurs-check fail for variables @vs@.+--+minimize :: forall kappa fam phi . (Ord (Exists phi))+         => Subst kappa fam phi -- ^+         -> Either [Exists phi] (Subst kappa fam phi)+minimize sigma =+  let sigma' = breakCycles inj proj $ removeIds proj sigma+   in whileM sigma' [] $ \s _+    -> M.fromList <$> (mapM (secondF (exMapM (go sigma'))) (M.toList s))+  where+    inj :: Exists phi -> Exists (Holes kappa fam phi)+    inj = exMap Hole++    proj :: Exists (Holes kappa fam phi) -> Maybe (Exists phi)+    proj (Exists (Hole phi)) = Just $ Exists phi+    proj _                   = Nothing+    +    secondF :: (Functor m) => (a -> m b) -> (x , a) -> m (x , b)+    secondF f (x , a) = (x,) <$> f a++    -- The actual engine of the 'minimize' function is thinning the+    -- variables that appear in the image of the substitution under production.+    -- We use the writer monad solely to let us know whether some variables have+    -- been substituted in this current term. After one iteration+    -- of the map where no variable is further refined, we are done.+    go :: Subst kappa fam phi+       -> Holes kappa fam phi at+       -> Writer [Exists phi] (Holes kappa fam phi at)+    go ss = holesRefineHolesM $ \var -> do+           case substLkup ss var of+             Nothing       -> return (Hole var)+             Just r        -> tell [Exists var]+                           >> return r++    -- | Just like nub; but works on a sorted list+    mnub :: (Ord a) => [a] -> [a]+    mnub [] = []+    mnub [x] = [x]+    mnub (x:y:ys)+      | x == y    = mnub (y:ys)+      | otherwise = x : mnub (y:ys)++    -- We loop while there is work to be done or no progress+    -- was done.+    whileM :: (Ord (Exists phi))+           => a -> [Exists phi] -> (a -> [Exists phi] -> Writer [Exists phi] a)+           -> Either [Exists phi] a+    whileM a xs f = do+      let (x' , xs') = runWriter (f a xs)+      if null xs'+      then return x'+      else if (mnub (sort xs') == mnub (sort xs))+           then Left xs'+           else whileM x' xs' f++-- |Removes the keys that project to themselves according to+-- the provided projection.+--+-- > removeIds id $ M.fromList [(0,0), (1,2) , (3,4)]+-- >   = M.fromList [(1,2),(3,4)]+--+removeIds :: forall a b+           . (Ord a) => (b -> Maybe a) -> M.Map a b -> M.Map a b+removeIds proj = M.filterWithKey (\a b -> not $ Just a == proj b)+++-- |Will make sure there are no cycles in the map as per the+-- provided function. For example,+--+-- > breakCycles id Just $ M.fromList [(0,1) , (1,2) , (2,0)]+-- >  = M.fromList [(1,0),(2,0)]+--+-- Usefull when the maps represent some sort of equivalence; the function+-- essentially collapses the equivalence class.+breakCycles :: forall a b+             . (Ord a) => (a -> b) -> (b -> Maybe a) -> M.Map a b -> M.Map a b+breakCycles inj proj m0+  = let (flattenedCycles , m') = runState (dropCycles m0) M.empty+     in M.union flattenedCycles m'+  where+    dropCycles :: M.Map a b -> State (M.Map a b) (M.Map a b)+    dropCycles m = case findCycle m of+                     Nothing        -> return m+                     Just (a , cyc) -> do+                       modify (M.union cyc)+                       dropCycles (M.delete a (m M.\\ cyc))++    cycleFor :: a -> M.Map a b -> Maybe (M.Map a b)+    cycleFor a0 m = M.lookup a0 m >>= proj >>= go M.empty+      where+        go :: M.Map a b -> a -> Maybe (M.Map a b)+        go aux a'+          | a' == a0 || a' `M.member` aux = return aux+          | otherwise = M.lookup a' m >>= proj >>= go (M.insert a' (inj a0) aux) ++    findCycle :: M.Map a b -> Maybe (a , M.Map a b)+    findCycle m = (`runCont` id) $ callCC $+      \exit -> (>> return Nothing) . flip mapM_ (M.keys m) $+        \a -> case cycleFor a m of+                Nothing -> return ()+                Just r  -> exit $ Just (a , r)

@@ -0,0 +1,249 @@+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE TypeSynonymInstances  #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE PatternSynonyms       #-}+module Generics.Simplistic.Util+  ( -- * Utility Functions and Types+    (&&&) , (***) , (:->) , (<.>)+    -- * Poly-kind indexed product functionality+  , (:*:)(..) , Delta , curry' , uncurry' , delta , deltaMap+    -- * Poly-kind indexed sums+  , Sum(..) , either' , either''+    -- * Constraints+  , Implies , Trivial+    -- * Higher-order Eq and Show+  , EqHO(..) , ShowHO(..)+    -- * Existential Wrapper+  , Exists(..) , exMap , exMapM , exElim+    -- * Elem functionality+  , Elem , NotElem , HasElem(..) , ElemPrf(..) , IsElem, sameTy+    -- * Witnessing and All constraints+  , All , Witness(..) , witness , witnessPrf+  , weq , wshow+  ) where++import Data.Kind  (Constraint)+import Data.Proxy (Proxy(..))+import Data.Functor.Sum+import Data.Functor.Const+import Data.Type.Equality+import Control.Arrow ((***) , (&&&))+import GHC.Generics ((:*:)(..), V1 , U1(..))++-- |Lifted curry+curry' :: ((f :*: g) x -> a) -> f x -> g x -> a+curry' f fx gx = f (fx :*: gx)++-- |Lifted uncurry+uncurry' :: (f x -> g x -> a) -> (f :*: g) x -> a+uncurry' f (fx :*: gx) = f fx gx++-- |Natural transformations+type f :-> g = forall n . f n -> g n++-- |Diagonal indexed functor+type Delta f = f :*: f++-- |Duplicates its argument+delta :: f :-> Delta f+delta fx = fx :*: fx++-- |Applies the same function to both components of the pair+deltaMap :: (f :-> g) -> Delta f :-> Delta g+deltaMap f (x :*: y) = f x :*: f y++-- |Higher-order sum eliminator+either' :: (f :-> r) -> (g :-> r) -> Sum f g :-> r+either' f _ (InL x) = f x+either' _ g (InR x) = g x++-- |Just like 'either'', but the result type is of kind Star+either'' :: (forall x . f x -> a) -> (forall y . g y -> a) -> Sum f g r -> a+either'' f g = getConst . either' (Const . f) (Const . g)++infixr 8 <.>+-- |Kleisli Composition+(<.>) :: (Monad m) => (b -> m c) -> (a -> m b) -> a -> m c+f <.> g = (>>= f) . g++-- |Constraint implication+class    (c => d) => Implies c d+instance (c => d) => Implies c d++-- |Trivial constraint+class    Trivial c+instance Trivial c++-- |Higher order , poly kinded, version of 'Eq'+class EqHO (f :: ki -> *) where+  eqHO :: forall k . f k -> f k -> Bool++instance Eq a => EqHO (Const a) where+  eqHO (Const a) (Const b) = a == b++instance (EqHO f, EqHO g) => EqHO (f :*: g) where+  eqHO (fx :*: gx) (fy :*: gy) = eqHO fx fy && eqHO gx gy++instance (EqHO f, EqHO g) => EqHO (Sum f g) where+  eqHO (InL fx) (InL fy) = eqHO fx fy+  eqHO (InR gx) (InR gy) = eqHO gx gy+  eqHO _        _        = False++instance EqHO V1 where+  eqHO _ _ = True++instance EqHO U1 where+  eqHO _ _ = True++++-- |Higher order, poly kinded, version of 'Show'; We provide+-- the same 'showsPrec' mechanism. The documentation of "Text.Show"+-- has a good example of the correct usage of 'showsPrec':+--+-- > +-- > infixr 5 :^:+-- > data Tree a =  Leaf a  |  Tree a :^: Tree a+-- >+-- > instance (Show a) => Show (Tree a) where+-- >   showsPrec d (Leaf m) = showParen (d > app_prec) $+-- >        showString "Leaf " . showsPrec (app_prec+1) m+-- >     where app_prec = 10+-- > +-- >   showsPrec d (u :^: v) = showParen (d > up_prec) $+-- >        showsPrec (up_prec+1) u .+-- >        showString " :^: "      .+-- >        showsPrec (up_prec+1) v+-- >     where up_prec = 5+--+class ShowHO (f :: ki -> *) where+  showHO      :: forall k . f k -> String+  showsPrecHO :: forall k . Int -> f k -> ShowS+  {-# MINIMAL showHO | showsPrecHO #-}++  showHO fx          = showsPrecHO 0 fx ""+  showsPrecHO _ fx s = showHO fx ++ s++instance Show a => ShowHO (Const a) where+  showsPrecHO d (Const a) = showParen (d > app_prec) $+      showString "Const " . showsPrec (app_prec + 1) a+    where app_prec = 10++instance (ShowHO f , ShowHO g) => ShowHO (f :*: g) where+  showsPrecHO d (x :*: y) = showParen (d > app_prec) $+                            showsPrecHO (app_prec+1) x+                          . showString " :*: "+                          . showsPrecHO (app_prec+1) y+    where app_prec = 10++instance (ShowHO f , ShowHO g) => ShowHO (Sum f g) where+  showsPrecHO d (InL fx) = showParen (d > app_prec) $+      showString "InL " . showsPrecHO (app_prec + 1) fx+    where app_prec = 10+  showsPrecHO d (InR gx) = showParen (d > app_prec) $+      showString "InR " . showsPrecHO (app_prec + 1) gx+    where app_prec = 10++-- |Existential type wrapper. This comesin particularly+-- handy when we want to add mrsop terms to+-- some container. See "Generics.MRSOP.Holes.Unify" for example.+data Exists (f :: k -> *) :: * where+  Exists :: f x -> Exists f++-- |Maps over 'Exists'+exMap :: (forall x . f x -> g x) -> Exists f -> Exists g+exMap f (Exists x) = Exists (f x)++-- |Maps a monadic actino over 'Exists'+exMapM :: (Monad m) => (forall x . f x -> m (g x)) -> Exists f -> m (Exists g)+exMapM f (Exists x) = Exists <$> f x++-- |eliminates an 'Exists'+exElim :: (forall x . f x -> a) -> Exists f -> a+exElim f (Exists x) = f x++instance ShowHO f => Show (Exists f) where+  show = exElim showHO++-- Boolean predicate about being element of a list+type family IsElem (a :: k) (as :: [ k ]) :: Bool where+  IsElem a (a ': as) = 'True+  IsElem a (b ': as) = IsElem a as+  IsElem a '[]       = 'False++-- An actual proof that something is an element+data ElemPrf a as where+  Here  :: ElemPrf a (a ': as)+  There :: ElemPrf a as -> ElemPrf a (b ': as)++-- Constructing these proofs+class HasElem a as where+  hasElem :: ElemPrf a as+instance {-# OVERLAPPING #-} HasElem a (a ': as) where+  hasElem = Here+instance {-# OVERLAPPABLE #-}+    (HasElem a as) => HasElem a (b ': as) where+  hasElem = There hasElem++-- |We will carry constructive information on the+-- constraint. Forcing 'IsElem' to true +type Elem    a as = (IsElem a as ~ 'True , HasElem a as)++-- |Negation of 'Elem'+type NotElem a as = IsElem a as ~ 'False++-- |Returns whether two types are the same, given that+-- both belong to the same list.+sameTy :: forall fam x y . (Elem x fam , Elem y fam) +      => Proxy fam -> Proxy x -> Proxy y -> Maybe (x :~: y)+sameTy _ _ _ = go (hasElem :: ElemPrf x fam) (hasElem :: ElemPrf y fam)+ where+   go :: ElemPrf x fam' -> ElemPrf b fam' -> Maybe (x :~: b)+   go Here       Here      = Just Refl+   go (There rr) (There y) = go rr y+   go _          _         = Nothing++type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where+  All c '[]       = ()+  All c (x ': xs) = (c x , All c xs)++-- |Carries information about @x@ being an instance of @c@+data Witness c x where+  Witness :: (c x) => Witness c x++-- |Provides the witness that @x@ is an instance of @c@+witness :: forall x xs c+         . (HasElem x xs , All c xs)+        => Proxy xs -> Witness c x+witness _ = witnessPrf (hasElem :: ElemPrf x xs)++-- |Fetches the 'Eq' instance for an element of a list+weq :: forall x xs+     . (All Eq xs , Elem x xs)+    => Proxy xs -> x -> x -> Bool+weq p = case witness p :: Witness Eq x of+            Witness -> (==)++-- |Fetches the 'Eq' instance for an element of a list+wshow :: forall x xs+       . (All Show xs , Elem x xs)+      => Proxy xs -> x -> String+wshow p = case witness p :: Witness Show x of+            Witness -> show++-- |Provides the witness that @x@ is an instance of @c@+witnessPrf :: (All c xs) => ElemPrf x xs -> Witness c x+witnessPrf Here      = Witness+witnessPrf (There p) = witnessPrf p+

@@ -0,0 +1,173 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE StandaloneDeriving    #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE KindSignatures        #-}+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+-- |Provides bare-bones /zipper/ functionality+-- to 'SRep' and 'Holes'.+module Generics.Simplistic.Zipper where++import Data.Proxy+import Data.Type.Equality+import GHC.Generics+import Data.Functor.Sum+import Control.Arrow (first)++import Generics.Simplistic+import Generics.Simplistic.Deep+import Generics.Simplistic.Util++-- |A value of type 'SZip ty w f' corresponds to a value of type+-- 'SRep w f' with one of its leaves of type @w ty@ absent.+-- This is essentially a zipper for 'SRep'.+data SZip ty w f where+  Z_KH    :: SZip ty w (K1 i ty)++  Z_L1    ::                SZip ty w f -> SZip ty w (f :+: g)+  Z_R1    ::                SZip ty w g -> SZip ty w (f :+: g)+  Z_PairL :: SZip ty w f -> SRep    w g -> SZip ty w (f :*: g)+  Z_PairR :: SRep   w f  -> SZip ty w g -> SZip ty w (f :*: g)+  Z_M1    :: SMeta i t   -> SZip ty w f -> SZip ty w (M1 i t f)+deriving instance (forall a. Show (w a)) => Show (SZip h w f)+deriving instance (forall a. Eq (w a)) => Eq   (SZip h w f)++-- |We can transform a 'SZip' into a 'SRep' given+-- we are provided with a value to /plug/ into the identified position.+plug :: SZip ty phi f -> phi ty -> SRep phi f+plug Z_KH          k = S_K1 k+plug (Z_L1 x)      k = S_L1 $ plug x k+plug (Z_R1 x)      k = S_R1 $ plug x k+plug (Z_M1 c x)    k = S_M1 c $ plug x k+plug (Z_PairL x y) k = (plug x k) :**: y+plug (Z_PairR x y) k = x :**: (plug y k)++-- |Maps over a 'SZip'+zipperMap :: (forall x . h x -> g x)+          -> SZip ty h f -> SZip ty g f+zipperMap f (Z_L1 x)      = Z_L1 (zipperMap f x)+zipperMap f (Z_R1 x)      = Z_R1 (zipperMap f x)+zipperMap f (Z_M1 c x)    = Z_M1 c (zipperMap f x)+zipperMap f (Z_PairL x y) = Z_PairL (zipperMap f x) (repMap f y)+zipperMap f (Z_PairR x y) = Z_PairR (repMap f x) (zipperMap f y)+zipperMap _ Z_KH          = Z_KH++inr1 :: (x :*: y) t -> (Sum z x :*: y) t+inr1 (x :*: y) = (InR x :*: y)++-- |Given a @z :: SZip ty h f@ and a @r :: Rep w f@, if @z@ and @r@+-- are made with the same constuctor we return a representation+-- that contains both @h@s and @w@s in its leaves, except in one leaf+-- of type @ty@. This is analogous to 'zipSRep'.+zipperRepZip :: SZip ty h f -> SRep w f -> Maybe (SRep ((Sum ((:~:) ty) h) :*: w) f)+zipperRepZip Z_KH          (S_K1 y)   = return $ S_K1 (InL Refl :*: y)+zipperRepZip (Z_L1 x)      (S_L1 y)   = S_L1 <$> zipperRepZip x y+zipperRepZip (Z_R1 x)      (S_R1 y)   = S_R1 <$> zipperRepZip x y+zipperRepZip (Z_M1 c x)    (S_M1 _ y) = S_M1 c <$> zipperRepZip x y+zipperRepZip (Z_PairL x y) (y1 :**: y2)+  = (:**:) <$> zipperRepZip x y1 <*> (repMap inr1 <$> zipSRep y y2)+zipperRepZip (Z_PairR x y) (y1 :**: y2)+  = (:**:) <$> (repMap inr1 <$> zipSRep x y1) <*> zipperRepZip y y2+zipperRepZip _ _ = Nothing++-- |Overlaps two zippers together; only succeeds if both zippers+-- have the same constructor AND hole.+zipSZip :: SZip ty h f -> SZip ty w f -> Maybe (SZip ty (h :*: w) f)+zipSZip Z_KH          Z_KH       = Just Z_KH+zipSZip (Z_L1 x)      (Z_L1 y)   = Z_L1 <$> zipSZip x y+zipSZip (Z_R1 x)      (Z_R1 y)   = Z_R1 <$> zipSZip x y+zipSZip (Z_M1 c x)    (Z_M1 _ y) = Z_M1 c <$> zipSZip x y+zipSZip (Z_PairL x y) (Z_PairL w z)+  = Z_PairL <$> zipSZip x w <*> zipSRep y z+zipSZip (Z_PairR x y) (Z_PairR w z)+  = Z_PairR <$> zipSRep x w <*> zipSZip y z+zipSZip _ _ = Nothing++-- |Analogous to 'repLeavesList'+zipLeavesList :: SZip ty w f -> [Maybe (Exists w)]+zipLeavesList (Z_L1 x)      = zipLeavesList x+zipLeavesList (Z_R1 x)      = zipLeavesList x+zipLeavesList (Z_M1 _ x)    = zipLeavesList x+zipLeavesList (Z_PairL l x) = zipLeavesList l ++ map Just (repLeavesList x)+zipLeavesList (Z_PairR x l) = map Just (repLeavesList x) ++ zipLeavesList l+zipLeavesList (Z_KH )       = [Nothing]++-- |The 'Zipper' datatype packages a 'SZip' in a more standard+-- presentation. A value of type @Zipper c f g t@ represents+-- a value of type @SRep f t@, where exactly one recursive leaf (of type @t@)+-- carries a value of type @g t@, moreover, we also carry a proof that+-- the constraint @c@ holds.+data Zipper c f g t where+  Zipper :: c+         => { zipper :: SZip t f (Rep t)+            , sel    :: g t+            }+         -> Zipper c f g t++-- |Auxiliar type synonym for annotated fixpoints.+type Zipper' kappa fam ann phi t+  = Zipper (CompoundCnstr kappa fam t)+           (HolesAnn kappa fam ann phi)+           (HolesAnn kappa fam ann phi) t++-- |Given a function that checks wheter an arbitrary position+-- is recursive and a value of @t@, returns all possible zippers ove+-- @t@. +zippers :: forall kappa fam ann phi t+         . (forall a . (Elem t fam) => phi a -> Maybe (a :~: t)) +        -> HolesAnn kappa fam ann phi t+        -> [Zipper' kappa fam ann phi t] +zippers _   (Prim' _ _) = []+zippers _   (Hole' _ _) = []+zippers aux (Roll' _ r) = map (uncurry Zipper) (go r)+  where+    pf :: Proxy fam+    pf = Proxy++    pa :: HolesAnn kappa fam ann phi a -> Proxy a+    pa _ = Proxy++    go :: SRep (HolesAnn kappa fam ann phi) f+       -> [(SZip t (HolesAnn kappa fam ann phi) f+          , HolesAnn kappa fam ann phi t)]+    go S_U1       = []+    go (S_L1 x)   = first Z_L1 <$> go x+    go (S_R1 x)   = first Z_R1 <$> go x+    go (S_M1 c x) = first (Z_M1 c) <$> go x+    go (x :**: y) = (first (flip Z_PairL y) <$> go x)+                 ++ (first (Z_PairR x)      <$> go y)+    go (S_K1 x@(Roll' _ _)) =+      case sameTy pf (Proxy :: Proxy t) (pa x) of+        Just Refl -> return $ (Z_KH , x)+        Nothing   -> []+    go (S_K1 x@(Hole' _ xh)) = +      case aux xh of+        Just Refl -> return $ (Z_KH , x)+        Nothing   -> []+    go _ = []+      +-- |Retrieves the constructor name for a representation.+-- /WARNING; UNSAFE/ this function only works if @f@ is the representation of+-- a type constructed with "GHC.Generics" builtin mechanisms.+zipConstructorName :: SZip h w f -> String+zipConstructorName (Z_M1 x@SM_C _)+  = getConstructorName x+zipConstructorName (Z_M1 _ x)+  = zipConstructorName x+zipConstructorName (Z_L1 x)+  = zipConstructorName x+zipConstructorName (Z_R1 x)+  = zipConstructorName x+zipConstructorName _+  = error "Please; use GHC's deriving mechanism. This keeps M1's at the top of the Rep"+