packages feed

model (empty) → 0.2

raw patch · 16 files changed

+1180/−0 lines, 16 filesdep +ListLikedep +basedep +containerssetup-changed

Dependencies added: ListLike, base, containers, deepseq, ghc-prim, model, pretty, tasty, tasty-hunit, tasty-quickcheck, transformers

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Pasqualino `Titto` Assini (c) 2016++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Pasqualino `Titto` Assini nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ model.cabal view
@@ -0,0 +1,40 @@+name:                model+version:             0.2+synopsis:            Derive a model of a data type using Generics+description:         See the tutorial at: https://github.com/tittoassini/model+homepage:            http://github.com/tittoassini/model+license:             BSD3+license-file:        LICENSE+author:              Pasqualino `Titto` Assini+maintainer:          tittoassini@gmail.com+copyright:           Copyright: (c) 2016 Pasqualino `Titto` Assini+category:            Data,Reflection,Generics+build-type:          Simple+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Data.Model,Data.Model.Class,Data.Model.Env,Data.Model.Instances,Data.Model.Pretty,Data.Model.Types,Type.ANat,Type.Analyse+  build-depends:       base >= 4.7 && < 5, containers >= 0.5.6.2, deepseq >= 1.4, pretty >= 1.1.2.0, transformers >= 0.4 ,ListLike >= 4.2.1+  default-language:    Haskell2010++test-suite model-test+  type:                exitcode-stdio-1.0+  hs-source-dirs:      test+  main-is:             Spec.hs+  other-modules: Test.Data,Test.Data2,Test.Data3,Test.Data.Model+  build-depends:       base+                     , ghc-prim >= 0.4.0.0+                     , tasty >= 0.11.0.2+                     , tasty-hunit+                     , tasty-hunit >= 0.9.2+                     , tasty-quickcheck+                     , tasty-quickcheck >= 0.8.4+                     , pretty+                     , containers+                     , model+  default-language:    Haskell2010++source-repository head+  type:     git+  location: https://github.com/tittoassini/model
+ src/Data/Model.hs view
@@ -0,0 +1,9 @@+module Data.Model (+  -- |Check the <https://github.com/tittoassini/model tutorial and github repo>+  module X+  ) where++import Data.Model.Class as X+import Data.Model.Types as X+import Data.Model.Instances as X+import Data.Model.Pretty as X
+ src/Data/Model/Class.hs view
@@ -0,0 +1,171 @@+{-# LANGUAGE DefaultSignatures         #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE TypeOperators             #-}++module Data.Model.Class(+  typeModel+  ,Model(..)+  ,AsType(..)++  -- *Utilities+  ,useCT++  -- *Re-exports+  ,Ana+  --,Typ+  )+  where++import           Control.Monad+import           Control.Monad.Trans.State.Lazy+import           Data.Either+import           Data.Model.Env+import           Data.Model.Types+import           Data.Typeable+import qualified GHC.Generics                   as G+import           Type.Analyse++-- | Return the model for the given type+typeModel :: AsType (Ana a) => Proxy a -> HTypeModel+typeModel p = withEnv (asTypeP p)++-- We feed to the analyser the abstract version of the type+-- in order to distinguish between variable and non variable positions+asTypeP :: forall a. AsType (Ana a) => Proxy a -> State Env HType+asTypeP _ = asType (undefined :: Ana a)++-- |Helper class used to capture the type parameters+class AsType a where+  asType :: a -> State Env HType++instance {-# OVERLAPPABLE #-} Model a => AsType (Typ a) where asType _ = envType (Proxy::Proxy a)++instance (AsType f,AsType a) => AsType (App f a) where+  asType _ = TypeApp <$> asType (undefined::f) <*> asType (undefined::a)++--instance (KnownNat t,Typeable t) => AsType (Typ (ANat t)) where asType _ = envType (Proxy::Proxy a)++-- |TypeLits are used to represent data type's parameters.+instance (KnownNat t,Typeable t) => Model (ANat t) where+  envType _ = return . TypeCon . TypVar . fromIntegral . anatVal $ (undefined :: ANat t)+++-- | Class of types whose model can be calculated+-- Instances are derived automatically, provided that the data type has an instance for `GHC.Generics`+class (Typeable a,AsType (Ana a)) => Model a where+-- class (Typeable a) => Model a where+-- class Model a where++  -- |Given a type proxy, update the environment with the ADTs referred by it and return the corresponding `HType`+  envType :: Proxy a -> State Env HType++  -- |Default, Generics based implementation+  default envType :: (Generic a, GModel (Rep a)) => Proxy a -> State Env HType+  envType p = addCT_ False p $ gcons (from (undefined :: a))++-- |Use the given constructors tree as model for the given type, returns the build type+--+-- Exported so that it can be used to overwrite default definitions+useCT :: Typeable a => Maybe (ConTree String HTypeRef) -> proxy a -> State Env (Type (TypeRef QualName))+useCT ct p = addCT_ True p (return ct)++addCT_ useLocalString p mct =+  let tr = typeRep p+      (tc,ts) = splitTyConApp tr+      nm hname = if useLocalString then "" else hname+      -- nm hname = hname+      uname = tyConName tc+      qname = QualName (nm $ tyConPackage tc) (nm $ tyConModule tc) uname+  in do+    inCtx <- enterCtx qname+    unless inCtx $ do+      ct <- mct+      addDef qname $ ADT uname (fromIntegral $ length ts) $ ct+    closeCtx+    return . TypeCon . TypRef $ qname++-- |Helper class, uses Generics to capture the model of a data type+-- Adapted from the Beamable package+class GModel f where+    gcons :: f a -> State Env (Maybe (ConTree String HTypeRef))+    gcontree :: f a -> State Env (ConTree String HTypeRef)+    gtype :: f a -> State Env HType+    gtypeN :: f a -> State Env [Either HType (String,HType)]++instance GModel (M1 D d V1) where+    gcons _ = return Nothing+    gcontree = notThere+    gtype = notThere+    gtypeN = notThere++-- |Datatypes with single constructor only+instance (GModel a, Datatype d, Constructor c) => GModel (M1 D d (M1 C c a)) where+    gcons x = Just <$> gcontree (unM1 x)+    gcontree = notThere+    gtype = notThere+    gtypeN = notThere++-- | Needed to avoid overlapping instances with (M1 D d (M1 C c a))+instance (Datatype d, GModel a, GModel b) => GModel (M1 D d (a :+: b) ) where+    gcons x = Just <$> gcontree x+    gcontree x = ConTree <$> gcontree (unL . unM1 $ x) <*> gcontree (unR . unM1 $ x)+    gtype = notThere+    gtypeN = notThere++-- |Datatypes with multiple constructors+instance (GModel a, Constructor c) => GModel (M1 C c a) where+  gcons = notThere++  gcontree x = Con (conName x) . toE . partitionEithers  <$> gtypeN (unM1 x)+    where+      toE (ls,[]) = Left ls+      toE ([],rs) = Right rs++  gtype = notThere+  gtypeN = notThere++-- |Constructors+instance (GModel a, GModel b) => GModel (a :+: b) where+  gcons = notThere+  gcontree x = ConTree <$> gcontree (unL x) <*> gcontree (unR x)+  gtype = notThere+  gtypeN = notThere++instance (Selector c,GModel a) => GModel (M1 G.S c a) where+  gcons = notThere+  gcontree = notThere+  gtype = notThere+  gtypeN ~s@(M1 x) = (\t -> [let n = selName s+                               in if null n+                                  then Left t+                                  else Right (n,t)+                              ]) <$> gtype x++instance (GModel a, GModel b) => GModel (a :*: b) where+  gcons = notThere+  gcontree = notThere+  gtype = notThere+  gtypeN ~(x :*: y) = (++) <$> gtypeN x <*> gtypeN y++instance GModel U1 where+  gcons = notThere+  gcontree = notThere+  gtype = notThere+  gtypeN _ = return []++instance (AsType (Ana a),Model a) => GModel (K1 i a) where+  gcons = notThere+  gcontree = notThere+  gtype _ = asTypeP (undefined::Proxy a)+  gtypeN _ = return []++unL :: (l :+: r) a -> l a+unL = error "unL should be used only for type recovery operations"++unR :: (l :+: r) a -> r a+unR = error "unR should be used only for type recovery operations"++notThere = error "never called"
+ src/Data/Model/Env.hs view
@@ -0,0 +1,43 @@+{-# LANGUAGE TypeOperators #-}+-- |Environment used while capturing model+module Data.Model.Env(State,Env,withEnv,enterCtx,addDef,closeCtx) where++import           Control.Monad.Trans.State.Lazy+import           Data.Bifunctor+import qualified Data.Map                       as M+import           Data.Model.Types++-- |Environment used while capturing model+data Env = Env {ctx::[QualName]  -- ^The stack of entered types+               ,env::HTypeEnv    -- ^The environment+               } deriving Show++-- |Run the model capturing computation+withEnv :: State Env HType -> HTypeModel+withEnv m = (\(t,e) -> TypeModel (unVar <$> t) e) . second env $ runState m (Env [] M.empty)++-- |Enter a type+enterCtx :: QualName -> State Env Bool+enterCtx name = do+   f <- inCtx name+   modify (\e -> e {ctx = name : ctx e})+   return f++-- |Returns True if we have already seen this data type and do not need to analyse it further+inCtx :: QualName -> State Env Bool+inCtx name = (name `elem`) <$> gets (\e -> ctx e ++ M.keys (env e))++-- |Add a new data type model to the environment+addDef :: QualName -> HADT -> State Env ()+addDef ref adt  = modify (\e -> e {env = M.insert ref adt (env e)})++-- |Leave current type+closeCtx :: State Env ()+closeCtx = modify (\e -> e {ctx = drop 1 (ctx e)})++-- pretty print environment+-- showEnv e = unlines [""+--                   ,show $ map locName $ seen e+--                   ,show $ map (first locName) $ ctx e+--                   ,show $ map (\(d,deps) -> (locName $ declName d,map locName deps)) $ defs e+--                   ]
+ src/Data/Model/Instances.hs view
@@ -0,0 +1,11 @@+-- |Instances of `Model` for common types (Bool,Maybe,Either)+module Data.Model.Instances where++import           Data.Model.Class++instance Model Bool++instance Model a => Model (Maybe a)++instance (Model a,Model b) => Model (Either a b)+
+ src/Data/Model/Pretty.hs view
@@ -0,0 +1,80 @@+{-# LANGUAGE FlexibleInstances         #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE OverloadedStrings         #-}+{-# LANGUAGE TupleSections             #-}+-- |Pretty instances for the model types+module Data.Model.Pretty(+  -- *Utilities+  dotted,spacedP,vspacedP,varP+  -- *Re-exports+  ,Pretty(..),prettyShow+  ) where++import           Data.Char+import           Data.List+import qualified Data.ListLike.String           as S+import qualified Data.Map                       as M+import           Data.Model.Types+import           Text.PrettyPrint.HughesPJClass++instance( Pretty exRef,Ord exRef,Show exRef,S.StringLike adtName,S.StringLike consName,S.StringLike ref) => Pretty (TypeModel adtName consName (TypeRef ref) exRef) where+  pPrint (TypeModel t e) = vcat $ [+     text "Type:"+    ,pPrint t <+> text "->" <+> pPrint (localName . declName <$> solveAll e t)+    ,text ""+    ,text "Environment:"]+     ++ map (\(ref,adt) -> pPrint ref <+> text "->" <+> pPrint (stringADT e adt)) (M.assocs e)++stringADT env adt = ADT (localName . declName $ adt) (declNumParameters adt) (((localName <$>) <$>) . conTreeNameMap localName <$> declCons adt)++localName = Name . S.toString++instance (Pretty n,Pretty cn,Pretty r) => Pretty (ADT n cn r) where pPrint = prettyADT "" '≡'++prettyADT pre eq adt = text pre <+> pPrint (declName adt) <+> vars adt <+> maybe (text "") (\c -> char eq <+> pPrint c) (declCons adt)++vars adt = sep . map varP . map (\x -> x-1) $ [1 .. declNumParameters adt]++varP n = char $ chr ( (ord 'a') + (fromIntegral n))++instance (Pretty name,Pretty ref) => Pretty (ConTree name ref) where+  pPrint (Con n (Left fs)) = pPrint n <+> sep (map (printPrettyType True) fs)+  pPrint (Con n (Right nfs)) = pPrint n <+> "{" <> sep (punctuate "," (map (\(n,t) -> pPrint n <+> "::" <+> pPrint t) nfs)) <> "}"+  -- pPrint (ConTree l r) = pPrint l <+> char '|' <+> pPrint r+  pPrint tr@(ConTree l r) = let (h:t) = constructors tr+                            in vcat (char ' ' <+> pPrint h : map (\c -> (char '|') <+> pPrint c) t)++instance Pretty n => Pretty (TypeRef n) where+   pPrint (TypVar v)   = varP v+   pPrint (TypRef s)   = pPrint s++instance Pretty r => Pretty (Type r) where pPrint = printPrettyType False++data PrettyType r = PrettyType Bool (TypeN r)+printPrettyType n = pPrint . PrettyType n . typeN++instance Pretty r => Pretty (PrettyType r) where+  pPrint (PrettyType _ (TypeN f [])) = pPrint f+  pPrint (PrettyType n (TypeN f as)) = maybeParens n (pPrint f <+> spacedP (map (PrettyType True) as))++instance Pretty r => Pretty (TypeN r) where+  pPrint (TypeN f []) = pPrint f+  pPrint (TypeN f as) = parens (pPrint f <+> spacedP as)++instance Pretty QualName where pPrint (QualName p m l) = dotted [p,m,l]++instance Pretty Name where pPrint (Name n) = text n++instance Pretty Doc where pPrint d = d++-- |Separate with a space+spacedP :: Pretty a => [a] -> Doc+spacedP = sep . map pPrint++-- |Separate with a new line+vspacedP :: Pretty a => [a] -> Doc+vspacedP = sep . intersperse (text "") . map pPrint++-- |Intercalate with '.'+dotted :: [String] -> Doc+dotted = text . intercalate "."
+ src/Data/Model/Types.hs view
@@ -0,0 +1,259 @@+{- |A model for simple algebraic data types.+-}+{-# LANGUAGE DeriveAnyClass    #-}+{-# LANGUAGE DeriveFoldable    #-}+{-# LANGUAGE DeriveFunctor     #-}+{-# LANGUAGE DeriveGeneric     #-}+{-# LANGUAGE DeriveTraversable ,FlexibleInstances #-}+module Data.Model.Types(+  -- *Model+  TypeModel(..),TypeEnv+  ,ADT(..)+  ,ConTree(..)+  ,Type(..),TypeN(..),TypeRef(..)++  -- *Names+  ,Name(..),QualName(..),qualName++  -- *Model Utilities+  ,adtNamesMap+  --,typeADTs+  ,typeN,typeA+  ,constructors,conTreeNameMap,conTreeTypeMap,conTreeTypeList,conTreeTypeFoldMap,fieldsTypes,fieldsNames++  -- *Handy aliases+  ,HTypeEnv,HTypeModel,HADT,HType,HTypeRef+  -- ,HEnv++  -- *Utilities+  ,solve,solveAll,unVar++  -- *Re-exports+  ,module GHC.Generics,Proxy(..)+  -- ,S.StringLike(),S.toString,S.fromString+  ) where++import           Control.DeepSeq+import           Data.Bifunctor  (first,second)+import           Data.Proxy+import           Data.Word       (Word8)+import           GHC.Generics+import qualified Data.Map as M+import qualified Data.ListLike.String           as S+import Data.List++-- |Haskell Environment+type HTypeEnv = TypeEnv String String (TypeRef QualName) QualName++-- |Haskell TypeModel+type HTypeModel = TypeModel String String (TypeRef QualName) QualName++-- |Haskell ADT+type HADT = ADT String String HTypeRef++-- |Haskell Type+type HType = Type HTypeRef++-- |Reference to an Haskell Type+type HTypeRef = TypeRef QualName++{- |+The complete model of a type, a reference to the type plus its environment:++* adtName:  type used to represent the name of a data type+* consName: type used to represent the name of a constructor+* inRef:    type used to represent a reference to a type or a type variable inside the data type definition (for example `HTypeRef`)+* exRef:    type used to represent a reference to a type in the type name (for example `QualName`)+-}+data TypeModel adtName consName inRef exRef = TypeModel {+  -- |The type application corresponding to the type+  typeName::Type exRef++  -- |The environment in which the type is defined+  ,typeEnv::TypeEnv adtName consName inRef exRef+  }+  deriving (Eq, Ord, Show, NFData, Generic)++--typeADTs = M.elems . typeEnv++-- |A map of all the ADTs that are directly or indirectly referred by a type, indexed by a type reference+type TypeEnv adtName consName inRef exRef = M.Map exRef (ADT adtName consName inRef)++{- |+Simple algebraic data type (not a GADT):++* declName: type used to represent the name of the data type+* consName: type used to represent the name of a constructor+* ref:      type used to represent a reference to a type or a type variable inside the data type definition (for example `HTypeRef`)+-}+data ADT name consName ref =+       ADT+         { declName          :: name   -- ^The name of the data type (for example @Bool@ for @data Bool@)+         , declNumParameters :: Word8  -- ^The number of type parameters/variable (up to a maximum of 255)+         , declCons          :: Maybe (ConTree consName ref) -- ^The constructors, if present+         }+       deriving (Eq, Ord, Show, NFData, Generic, Functor, Foldable, Traversable)++-- |Constructors are assembled in a binary tree+data ConTree name ref =+  Con {+  -- | The constructor name, unique in the data type+  constrName    :: name++  -- | Constructor fields, they can be either unnamed (Left case) or named (Right case)+  -- If they are named, they must all be named+  ,constrFields :: Either+                   [Type ref]+                   [(name,Type ref)]+  }++  {- |+  Constructor tree.++  Constructors are disposed in an optimally balanced, right heavier tree:++  For example, the data type:++  @data N = One | Two | Three | Four | Five@++  Would have its contructors ordered in the following tree:++>          |+>     |            |+>  One Two   Three   |+>                Four Five++  To get a list of constructor in declaration order, use `constructors`+  -}+  | ConTree (ConTree name ref) (ConTree name ref)++  deriving (Eq, Ord, Show, NFData, Generic)++-- |Return the list of constructors in definition order+constructors c@(Con _ _) = [c]+constructors (ConTree l r) = constructors l ++ constructors r++-- |Return just the field types+fieldsTypes :: Either [b] [(a, b)] -> [b]+fieldsTypes (Left ts)   = ts+fieldsTypes (Right nts) = map snd nts++-- |Return just the field names (or an empty list if unspecified)+fieldsNames (Left _)   = []+fieldsNames (Right nts) = map snd nts++-- GHC won't derive these instances automatically+instance Functor (ConTree name) where+  fmap f (ConTree l r) = ConTree (fmap f l) (fmap f r)+  fmap f (Con n (Left ts)) = Con n (Left $ (fmap . fmap) f ts)+  fmap f (Con n (Right ts)) = Con n (Right $ (fmap . fmap . fmap) f ts)++instance Foldable (ConTree name) where+   foldMap f (ConTree l r) = foldMap f l `mappend` foldMap f r+   foldMap f (Con _ (Left ts)) = mconcat . map (foldMap f) $ ts+   foldMap f (Con _ (Right nts)) = mconcat . map (foldMap f . snd) $ nts++instance Traversable (ConTree name) where+  traverse f (ConTree l r) = ConTree <$> traverse f l <*> traverse f r+  traverse f (Con n (Left ts)) = Con n . Left <$> sequenceA (map (traverse f) ts)+  -- TODO: simplify this+  traverse f (Con n (Right nts)) = Con n . Right . zip (map fst nts) <$> sequenceA (map (traverse f . snd) nts)++-- CHECK: easier to use lens?+-- |Map on the constructor types (used for example when eliminating variables)+conTreeTypeMap :: (Type t -> Type ref) -> ConTree name t -> ConTree name ref+conTreeTypeMap f (ConTree l r) = ConTree (conTreeTypeMap f l) (conTreeTypeMap f r)+conTreeTypeMap f (Con n (Left ts)) = Con n (Left $ map f ts)+conTreeTypeMap f (Con n (Right nts)) = Con n (Right $ map (second f) nts)++-- |Map over a constructor tree names+conTreeNameMap :: (name -> name2) -> ConTree name t -> ConTree name2 t+conTreeNameMap f (ConTree l r) = ConTree (conTreeNameMap f l) (conTreeNameMap f r)+conTreeNameMap f (Con n (Left ts)) = Con (f n) (Left ts)+conTreeNameMap f (Con n (Right nts)) = Con (f n) (Right $ map (first f) nts)++-- |Extract list of types in a constructor tree+conTreeTypeList :: ConTree name t -> [Type t]+conTreeTypeList = conTreeTypeFoldMap (:[])++-- |Fold over the types in a constructor tree+conTreeTypeFoldMap :: Monoid a => (Type t -> a) -> ConTree name t -> a+conTreeTypeFoldMap f (ConTree l r) = conTreeTypeFoldMap f l `mappend` conTreeTypeFoldMap f r+conTreeTypeFoldMap f (Con _ (Left ts)) = mconcat . map f $ ts+conTreeTypeFoldMap f (Con _ (Right nts)) = mconcat . map (f . snd) $ nts++-- |Map over the names of an ADT and of its constructors+adtNamesMap+  :: (adtName1 -> adtName2)+     -> (consName1 -> consName2)+     -> ADT adtName1 consName1 ref+     -> ADT adtName2 consName2 ref+adtNamesMap f g adt = adt {declName = f (declName adt),declCons = conTreeNameMap g <$> declCons adt}++-- |A type+data Type ref = TypeCon ref                    -- ^Type constructor ("Bool","Maybe",..)+              | TypeApp (Type ref) (Type ref)  -- ^Type application+  deriving (Eq, Ord, Show, NFData, Generic, Functor, Foldable, Traversable)++-- |Another representation of a type, sometime easier to work with+data TypeN r = TypeN r [TypeN r]+             deriving (Eq,Ord,Read,Show,NFData ,Generic,Functor,Foldable,Traversable)++-- |Convert from Type to TypeN+typeN :: Type r -> TypeN r+typeN (TypeApp f a) = let TypeN h ts = typeN f+                       in TypeN h (ts ++ [typeN a])+typeN (TypeCon r) = TypeN r []++-- |Convert from TypeN to Type+typeA :: TypeN ref -> Type ref+typeA (TypeN t ts) = app (TypeCon t) (map typeA ts)+  where app t [] = t+        app t (x:xs) = app (TypeApp t x) xs++-- |A reference to a type+data TypeRef name = TypVar Word8  -- ^Type variable+                  | TypRef name   -- ^Type reference+  deriving (Eq, Ord, Show, NFData, Generic, Functor, Foldable, Traversable)++-- |A fully qualified Haskell name+data QualName = QualName {pkgName,mdlName,locName :: String}+              deriving (Eq, Ord, Show, NFData, Generic)++-- |Return the qualified name, minus the package name.+qualName :: QualName -> String+qualName n = concat [mdlName n,".",locName n]++instance S.StringLike QualName where+  toString n = intercalate "." [pkgName n,mdlName n,locName n]+  fromString n = let (p,r) = span (/= '.') n+                     (m,r2) = span (/= '.') $ tail r+                     l = tail r2+                 in QualName p m l++instance S.StringLike String where+  toString = id+  fromString = id++-- |Simple name+data Name = Name String deriving (Eq, Ord, Show, NFData, Generic)++instance S.StringLike Name where+  toString (Name n)= n+  fromString n = Name n++-- Utilities++-- |Remove variable references (for example if we know that a type is fully saturated and cannot contain variables)+unVar (TypVar _) = error "Unexpected variable"+unVar (TypRef n) = n++-- |Solve all references in a data structure, using the given environment+solveAll :: (Functor f, Show k, Ord k) => M.Map k b -> f k -> f b+solveAll env t = (\r -> solve r env) <$> t++-- |Solve a key in an environment, returns an error if the key is missing+solve :: (Ord k, Show k) => k -> M.Map k a -> a+solve k e = case M.lookup k e of+     Nothing -> error $ unwords ["Unknown reference to",show k]+     Just v -> v
+ src/Type/ANat.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE DataKinds ,ScopedTypeVariables #-}+-- |Nats with * kind+module Type.ANat(ANat,anatVal,A0,A1,A2,A3,A4,A5,A6,A7,A8,A9,module GHC.TypeLits) where++import GHC.TypeLits++-- |Envelope to get Nats with * kind+data ANat (n :: Nat)++-- |Convert a Nat to the corresponding Integer+--+-- >>> anatVal (undefined::A5)+-- 5+anatVal :: KnownNat n => ANat n -> Integer+anatVal = natVal++type A0 = ANat 0+type A1 = ANat 1+type A2 = ANat 2+type A3 = ANat 3+type A4 = ANat 4+type A5 = ANat 5+type A6 = ANat 6+type A7 = ANat 7+type A8 = ANat 8+type A9 = ANat 9+++++
+ src/Type/Analyse.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE DataKinds            #-}+{-# LANGUAGE PolyKinds            #-}+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE UndecidableInstances #-}+-- |Utility to abstract parametric types+module Type.Analyse(Ana,App,Typ,module Type.ANat) where++import Type.ANat++{- |+Abstract a concrete type to a type applied to variables.++More precisely: to a meta-representation where type application is represented by `App`, data types are marked by `Typ` and variables are represented by `ANat` types.++BUG: Silently fails for types with more than 9 parameters (should be defined recursively, if you know how let me know)++Examples:++>>> undefined :: Ana (Maybe Char)+undefined :: Ana (Maybe Char) :: App (Typ (Maybe A0)) (Typ Char)++>>> undefined :: Ana (Either Int Char)+undefined :: Ana (Either Int Char)+  :: App (App (Typ (Either A0 A1)) (Typ Int)) (Typ Char)++>>> undefined :: Ana ([(Bool,())])+undefined :: Ana ([(Bool,())])+  :: App (Typ [A0]) (App (App (Typ (A0, A1)) (Typ Bool)) (Typ ()))+-}+type family Ana t where+    Ana (f a0 a1 a2 a3 a4 a5 a6 a7 a8) = App (App (App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 A7 A8 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)) (Ana a7)) (Ana a8)+    Ana (f a0 a1 a2 a3 a4 a5 a6 a7) = App (App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 A7 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)) (Ana a7)+    Ana (f a0 a1 a2 a3 a4 a5 a6) = App (App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 A6 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)) (Ana a6)+    Ana (f a0 a1 a2 a3 a4 a5) = App (App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 A5 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)) (Ana a5)+    Ana (f a0 a1 a2 a3 a4) = App (App (App (App (App (Typ (f A0 A1 A2 A3 A4 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)) (Ana a4)+    Ana (f a0 a1 a2 a3) = App (App (App (App (Typ (f A0 A1 A2 A3 )) (Ana a0)) (Ana a1)) (Ana a2)) (Ana a3)+    Ana (f a0 a1 a2) = App (App (App (Typ (f A0 A1 A2 )) (Ana a0)) (Ana a1)) (Ana a2)+    Ana (f a0 a1) = App (App (Typ (f A0 A1 )) (Ana a0)) (Ana a1)+    Ana (f a0) = App (Typ (f A0 )) (Ana a0)+    Ana a = Typ a++-- Problem: in Ana (Either Char Int) -> Ana (f a) f==Either Char a=Int++-- |Type application+data App f a++-- |A data type+data Typ a++
+ test/Spec.hs view
@@ -0,0 +1,166 @@+{-# LANGUAGE DeriveAnyClass            #-}+{-# LANGUAGE DeriveGeneric             #-}+{-# LANGUAGE FlexibleContexts          #-}+{-# LANGUAGE NoMonomorphismRestriction #-}+{-# LANGUAGE OverloadedStrings         #-}+{-# LANGUAGE ScopedTypeVariables       #-}+{-# LANGUAGE StandaloneDeriving        #-}+import           Data.Bifunctor+import qualified Data.Either+import           Data.List+import qualified Data.Map              as M+import           Data.Model+import           Data.Traversable+import           Data.Typeable+import           Data.Word+import qualified GHC.Base+import qualified GHC.Types+import           Test.Data+import           Test.Data.Model+import qualified Test.Data2+import qualified Test.Data3+import           Test.Tasty+import           Test.Tasty.HUnit+import           Test.Tasty.QuickCheck as QC++-- main = makeTests+main = mainTest++mainTest = defaultMain tests++tests :: TestTree+tests = testGroup "Tests" [properties,  unitTests]++properties = testGroup "Properties" []++models = [typeModel (Proxy :: Proxy Void)+       ,typeModel (Proxy :: Proxy Unit)+       ,typeModel (Proxy :: Proxy Bool)+       ,typeModel (Proxy :: Proxy Char)+       ,typeModel (Proxy :: Proxy String)+       ,typeModel (Proxy :: Proxy [Bool])+       ,typeModel (Proxy :: Proxy N)+       ,typeModel (Proxy :: Proxy Un)+       ,typeModel (Proxy :: Proxy D2)+       ,typeModel (Proxy :: Proxy D4)+       ,typeModel (Proxy :: Proxy A0)+       ,typeModel (Proxy :: Proxy B0)+       -- ,typeModel (Proxy :: Proxy Various)+       -- ghc chokes on these heavily mutually dependent types+       -- ,typeModel (Proxy :: Proxy MM1)+       -- ,typeModel (Proxy :: Proxy MM2)+       -- ,typeModel (Proxy :: Proxy MM3)+       ,typeModel (Proxy :: Proxy (Phantom Unit))+       ,typeModel (Proxy :: Proxy (List Bool))+       ,typeModel (Proxy :: Proxy (Test.Data2.List Bool))+       ,typeModel (Proxy :: Proxy (Test.Data3.List Bool))+       ,typeModel (Proxy :: Proxy (List (Test.Data2.List (Test.Data3.List Bool))))+       ,typeModel (Proxy :: Proxy (Maybe Void))+       ,typeModel (Proxy :: Proxy (Either Bool Unit))+       ,typeModel (Proxy :: Proxy (RR Un Unit N))+       ,typeModel (Proxy :: Proxy (Either Bool (List Unit)))+       ,typeModel (Proxy :: Proxy (Tr (Maybe Unit)))+       ,typeModel (Proxy :: Proxy (Perfect Bool))++        -- Unsupported: higher kind+        --,typeModel (Proxy :: Proxy (PerfectF Maybe Bool))+        --,typeModel (Proxy :: Proxy (Free Maybe Bool))+       ]++tst p e = let tm = typeModel p+              s = prettyShow . simpleType $ typeName tm+          in testCase (unwords ["typeModel of",s]) $ simpleHTypeEnv tm @?= e++----- Pretty printing+-- Simplify type for test+simpleHTypeEnv tm = (simpleType $ typeName tm+                    ,sort . map simpleADT $ M.assocs $ typeEnv tm)++simpleType = (TypRef . asName <$>)+simpleADT (qname,adt) = ADT (qualName qname) (declNumParameters adt) ((mdlRef <$>) <$> declCons adt)++mdlRef :: HTypeRef -> TypeRef Name+mdlRef (TypVar v)   = TypVar v+mdlRef (TypRef n)   = TypRef (asName n)++asName = Name . qualName++pr = print+pp = putStrLn . prettyShow++-- THIS STOPPED WORKING (ghc 8.01?), Char not instance of Generic+-- instance Model Char++-- Some fake instance declaration for primitive types+instance Model Char where envType _ = envType (Proxy::Proxy CharSI)+data CharSI deriving Generic+instance Model CharSI++-- Provide models for Word8 .. using stand-in classes+instance Model Word8 where envType _ = envType (Proxy::Proxy Word8SI)+data Word8SI deriving Generic+instance Model Word8SI++-- TODO: Fix problems with types using symbolic constructors+instance Model a => Model [a] where envType _ = envType (Proxy::Proxy (ListSI a))++data ListSI a deriving Generic+instance Model a => Model (ListSI a)++instance Model ()++----- Create tests+makeTests = makeTest models+-- unitTests = undefined++thisFile = "test/Spec.hs"++makeTest ts = appendFile thisFile $ ("\n-- Appended by makeTest\nunitTests = testGroup \"Unit tests\" [" ++ (intercalate "\n\n  ," $ map (\tm -> unwords ["tst (Proxy :: Proxy (",prettyShow . simpleType . typeName $ tm,")) (",show . simpleHTypeEnv $ tm,")"]) ts)) ++ " ]"+++-- Appended by makeTest+unitTests = testGroup "Unit tests" [tst (Proxy :: Proxy ( Test.Data.Void )) ( (TypeCon (TypRef (Name "Test.Data.Void")),[ADT {declName = "Test.Data.Void", declNumParameters = 0, declCons = Nothing}]) )++  ,tst (Proxy :: Proxy ( Test.Data.Unit )) ( (TypeCon (TypRef (Name "Test.Data.Unit")),[ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( GHC.Types.Bool )) ( (TypeCon (TypRef (Name "GHC.Types.Bool")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Main.CharSI )) ( (TypeCon (TypRef (Name "Main.CharSI")),[ADT {declName = "Main.CharSI", declNumParameters = 0, declCons = Nothing}]) )++  ,tst (Proxy :: Proxy ( Main.ListSI Main.CharSI )) ( (TypeApp (TypeCon (TypRef (Name "Main.ListSI"))) (TypeCon (TypRef (Name "Main.CharSI"))),[ADT {declName = "Main.CharSI", declNumParameters = 0, declCons = Nothing},ADT {declName = "Main.ListSI", declNumParameters = 1, declCons = Nothing}]) )++  ,tst (Proxy :: Proxy ( Main.ListSI GHC.Types.Bool )) ( (TypeApp (TypeCon (TypRef (Name "Main.ListSI"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Main.ListSI", declNumParameters = 1, declCons = Nothing}]) )++  ,tst (Proxy :: Proxy ( Test.Data.N )) ( (TypeCon (TypRef (Name "Test.Data.N")),[ADT {declName = "Test.Data.N", declNumParameters = 0, declCons = Just (ConTree (ConTree (Con {constrName = "One", constrFields = Left []}) (Con {constrName = "Two", constrFields = Left []})) (ConTree (Con {constrName = "Three", constrFields = Left []}) (ConTree (Con {constrName = "Four", constrFields = Left []}) (Con {constrName = "Five", constrFields = Left []}))))}]) )++  ,tst (Proxy :: Proxy ( Test.Data.Un )) ( (TypeCon (TypRef (Name "Test.Data.Un")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.Un", declNumParameters = 0, declCons = Just (Con {constrName = "Un", constrFields = Right [("un",TypeCon (TypRef (Name "GHC.Types.Bool")))]})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.D2 )) ( (TypeCon (TypRef (Name "Test.Data.D2")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.D2", declNumParameters = 0, declCons = Just (Con {constrName = "D2", constrFields = Left [TypeCon (TypRef (Name "GHC.Types.Bool")),TypeCon (TypRef (Name "Test.Data.N"))]})},ADT {declName = "Test.Data.N", declNumParameters = 0, declCons = Just (ConTree (ConTree (Con {constrName = "One", constrFields = Left []}) (Con {constrName = "Two", constrFields = Left []})) (ConTree (Con {constrName = "Three", constrFields = Left []}) (ConTree (Con {constrName = "Four", constrFields = Left []}) (Con {constrName = "Five", constrFields = Left []}))))}]) )++  ,tst (Proxy :: Proxy ( Test.Data.D4 )) ( (TypeCon (TypRef (Name "Test.Data.D4")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.D4", declNumParameters = 0, declCons = Just (Con {constrName = "D4", constrFields = Left [TypeCon (TypRef (Name "GHC.Types.Bool")),TypeCon (TypRef (Name "Test.Data.N")),TypeCon (TypRef (Name "Test.Data.Unit")),TypeCon (TypRef (Name "Test.Data.N3"))]})},ADT {declName = "Test.Data.N", declNumParameters = 0, declCons = Just (ConTree (ConTree (Con {constrName = "One", constrFields = Left []}) (Con {constrName = "Two", constrFields = Left []})) (ConTree (Con {constrName = "Three", constrFields = Left []}) (ConTree (Con {constrName = "Four", constrFields = Left []}) (Con {constrName = "Five", constrFields = Left []}))))},ADT {declName = "Test.Data.N3", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "N1", constrFields = Left []}) (ConTree (Con {constrName = "N2", constrFields = Left []}) (Con {constrName = "N3", constrFields = Left []})))},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.A0 )) ( (TypeCon (TypRef (Name "Test.Data.A0")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.A0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "A0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.B0")),TypeCon (TypRef (Name "Test.Data.B0")),TypeCon (TypRef (Name "Test.Data.D0")),TypeCon (TypRef (Name "GHC.Types.Bool"))]}) (Con {constrName = "A1", constrFields = Left [TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "Test.Data.Unit"))),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool")))]}))},ADT {declName = "Test.Data.B0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "B0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.C0"))]}) (Con {constrName = "B1", constrFields = Left []}))},ADT {declName = "Test.Data.C0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "C0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.A0"))]}) (Con {constrName = "C1", constrFields = Left []}))},ADT {declName = "Test.Data.D0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "D0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.E0"))]}) (Con {constrName = "D1", constrFields = Left []}))},ADT {declName = "Test.Data.E0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "E0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.D0"))]}) (Con {constrName = "E1", constrFields = Left []}))},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})},ADT {declName = "Test.Data2.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Cons2", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "Nil2", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Test.Data.B0 )) ( (TypeCon (TypRef (Name "Test.Data.B0")),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.A0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "A0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.B0")),TypeCon (TypRef (Name "Test.Data.B0")),TypeCon (TypRef (Name "Test.Data.D0")),TypeCon (TypRef (Name "GHC.Types.Bool"))]}) (Con {constrName = "A1", constrFields = Left [TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "Test.Data.Unit"))),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool")))]}))},ADT {declName = "Test.Data.B0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "B0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.C0"))]}) (Con {constrName = "B1", constrFields = Left []}))},ADT {declName = "Test.Data.C0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "C0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.A0"))]}) (Con {constrName = "C1", constrFields = Left []}))},ADT {declName = "Test.Data.D0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "D0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.E0"))]}) (Con {constrName = "D1", constrFields = Left []}))},ADT {declName = "Test.Data.E0", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "E0", constrFields = Left [TypeCon (TypRef (Name "Test.Data.D0"))]}) (Con {constrName = "E1", constrFields = Left []}))},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})},ADT {declName = "Test.Data2.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Cons2", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "Nil2", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Test.Data.Phantom Test.Data.Unit )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data.Phantom"))) (TypeCon (TypRef (Name "Test.Data.Unit"))),[ADT {declName = "Test.Data.Phantom", declNumParameters = 1, declCons = Just (Con {constrName = "Phantom", constrFields = Left []})},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.List GHC.Types.Bool )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Test.Data2.List GHC.Types.Bool )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data2.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Cons2", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "Nil2", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Test.Data3.List GHC.Types.Bool )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data3.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data3.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data3.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( Test.Data.List (Test.Data2.List (Test.Data3.List GHC.Types.Bool)) )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeApp (TypeCon (TypRef (Name "Test.Data3.List"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))},ADT {declName = "Test.Data2.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Cons2", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data2.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "Nil2", constrFields = Left []}))},ADT {declName = "Test.Data3.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data3.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))}]) )++  ,tst (Proxy :: Proxy ( GHC.Base.Maybe Test.Data.Void )) ( (TypeApp (TypeCon (TypRef (Name "GHC.Base.Maybe"))) (TypeCon (TypRef (Name "Test.Data.Void"))),[ADT {declName = "GHC.Base.Maybe", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Nothing", constrFields = Left []}) (Con {constrName = "Just", constrFields = Left [TypeCon (TypVar 0)]}))},ADT {declName = "Test.Data.Void", declNumParameters = 0, declCons = Nothing}]) )++  ,tst (Proxy :: Proxy ( Data.Either.Either GHC.Types.Bool Test.Data.Unit )) ( (TypeApp (TypeApp (TypeCon (TypRef (Name "Data.Either.Either"))) (TypeCon (TypRef (Name "GHC.Types.Bool")))) (TypeCon (TypRef (Name "Test.Data.Unit"))),[ADT {declName = "Data.Either.Either", declNumParameters = 2, declCons = Just (ConTree (Con {constrName = "Left", constrFields = Left [TypeCon (TypVar 0)]}) (Con {constrName = "Right", constrFields = Left [TypeCon (TypVar 1)]}))},ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.RR Test.Data.Un Test.Data.Unit Test.Data.N )) ( (TypeApp (TypeApp (TypeApp (TypeCon (TypRef (Name "Test.Data.RR"))) (TypeCon (TypRef (Name "Test.Data.Un")))) (TypeCon (TypRef (Name "Test.Data.Unit")))) (TypeCon (TypRef (Name "Test.Data.N"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.N", declNumParameters = 0, declCons = Just (ConTree (ConTree (Con {constrName = "One", constrFields = Left []}) (Con {constrName = "Two", constrFields = Left []})) (ConTree (Con {constrName = "Three", constrFields = Left []}) (ConTree (Con {constrName = "Four", constrFields = Left []}) (Con {constrName = "Five", constrFields = Left []}))))},ADT {declName = "Test.Data.RR", declNumParameters = 3, declCons = Just (ConTree (Con {constrName = "RN", constrFields = Right [("rna",TypeCon (TypVar 0)),("rnb",TypeCon (TypVar 1)),("rnc",TypeCon (TypVar 2))]}) (ConTree (Con {constrName = "RA", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeApp (TypeApp (TypeCon (TypRef (Name "Test.Data.RR"))) (TypeCon (TypVar 0))) (TypeCon (TypVar 0))) (TypeCon (TypVar 2)),TypeCon (TypVar 1)]}) (Con {constrName = "RAB", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeApp (TypeApp (TypeCon (TypRef (Name "Test.Data.RR"))) (TypeCon (TypVar 2))) (TypeCon (TypVar 1))) (TypeCon (TypVar 0)),TypeCon (TypVar 1)]})))},ADT {declName = "Test.Data.Un", declNumParameters = 0, declCons = Just (Con {constrName = "Un", constrFields = Right [("un",TypeCon (TypRef (Name "GHC.Types.Bool")))]})},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Data.Either.Either GHC.Types.Bool (Test.Data.List Test.Data.Unit) )) ( (TypeApp (TypeApp (TypeCon (TypRef (Name "Data.Either.Either"))) (TypeCon (TypRef (Name "GHC.Types.Bool")))) (TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypRef (Name "Test.Data.Unit")))),[ADT {declName = "Data.Either.Either", declNumParameters = 2, declCons = Just (ConTree (Con {constrName = "Left", constrFields = Left [TypeCon (TypVar 0)]}) (Con {constrName = "Right", constrFields = Left [TypeCon (TypVar 1)]}))},ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.Tr (GHC.Base.Maybe Test.Data.Unit) )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data.Tr"))) (TypeApp (TypeCon (TypRef (Name "GHC.Base.Maybe"))) (TypeCon (TypRef (Name "Test.Data.Unit")))),[ADT {declName = "GHC.Base.Maybe", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "Nothing", constrFields = Left []}) (Con {constrName = "Just", constrFields = Left [TypeCon (TypVar 0)]}))},ADT {declName = "Test.Data.Forest", declNumParameters = 1, declCons = Just (Con {constrName = "Forest", constrFields = Left [TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeApp (TypeCon (TypRef (Name "Test.Data.Tr"))) (TypeCon (TypVar 0)))]})},ADT {declName = "Test.Data.List", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "C", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.List"))) (TypeCon (TypVar 0))]}) (Con {constrName = "N", constrFields = Left []}))},ADT {declName = "Test.Data.Tr", declNumParameters = 1, declCons = Just (Con {constrName = "Tr", constrFields = Left [TypeCon (TypVar 0),TypeApp (TypeCon (TypRef (Name "Test.Data.Forest"))) (TypeCon (TypVar 0))]})},ADT {declName = "Test.Data.Unit", declNumParameters = 0, declCons = Just (Con {constrName = "Unit", constrFields = Left []})}]) )++  ,tst (Proxy :: Proxy ( Test.Data.Perfect GHC.Types.Bool )) ( (TypeApp (TypeCon (TypRef (Name "Test.Data.Perfect"))) (TypeCon (TypRef (Name "GHC.Types.Bool"))),[ADT {declName = "GHC.Types.Bool", declNumParameters = 0, declCons = Just (ConTree (Con {constrName = "False", constrFields = Left []}) (Con {constrName = "True", constrFields = Left []}))},ADT {declName = "Test.Data.Fork", declNumParameters = 1, declCons = Just (Con {constrName = "Fork", constrFields = Left [TypeCon (TypVar 0),TypeCon (TypVar 0)]})},ADT {declName = "Test.Data.Perfect", declNumParameters = 1, declCons = Just (ConTree (Con {constrName = "ZeroP", constrFields = Left [TypeCon (TypVar 0)]}) (Con {constrName = "SuccP", constrFields = Left [TypeApp (TypeCon (TypRef (Name "Test.Data.Perfect"))) (TypeApp (TypeCon (TypRef (Name "Test.Data.Fork"))) (TypeCon (TypVar 0)))]}))}]) ) ]
+ test/Test/Data.hs view
@@ -0,0 +1,199 @@+{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE DeriveTraversable #-}+{-# LANGUAGE MultiParamTypeClasses ,DeriveGeneric ,DeriveDataTypeable ,ScopedTypeVariables ,GADTs ,NoMonomorphismRestriction ,DeriveGeneric ,DefaultSignatures ,TemplateHaskell ,TypeFamilies ,FlexibleContexts ,FlexibleInstances ,EmptyDataDecls #-}+{-+ A collection of data types used for testing.+-}+module Test.Data where++import Control.Exception+import           Data.Char+import           Data.Int+import           Data.Word++import           Data.Typeable+import           Data.Data+import           GHC.Generics+import           Data.Data+import qualified Test.Data2 as D2+import Data.Foldable+import GHC.Exts hiding (toList)++data Void deriving Generic++data X = X X deriving Generic++data Unit = Unit deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Un = Un {un::Bool} deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data D2 = D2 Bool N deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data D4 = D4 Bool N Unit N3 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- Enumeration+data N3 = N1 | N2 | N3+            deriving (Eq, Ord, Read, Show, Typeable, Data, Generic,Enum)++data N = One+       | Two+       | Three+       | Four+       | Five+  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic, Enum)++-- toForestD :: Forest a -> ForestD (Tr2 a)+ -- toForestD (Forest lt) = undefined -- Forest2 (ForestD (map (\t -> let Tr2 tt = treeConv t in tt) . toList $ lt))++-- toForestD (Forest lt) = undefined -- Forest2 (ForestD (map (\t -> let Tr2 tt = treeConv t in tt) . toList $ lt))++toForest2 :: Forest a -> Forest2 a+toForest2 (Forest f) = Forest2 (ForestD $ fmap toTr f)++toTr :: Tr a -> TrD (Forest2 a) a+toTr (Tr a f) = TrD a (toForest2 f)++toTr2 :: Tr a -> Tr2 a+toTr2 (Tr a (Forest f)) = Tr2 (TrD a (ForestD $ fmap toTr2 f))++-- tying the recursive knot, equivalent to Forest/Tree+data Forest2 a = Forest2 (ForestD (TrD (Forest2 a) a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data Tr2 a = Tr2 (TrD (ForestD (Tr2 a)) a) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- First-order non mutually recursive+data ForestD t = ForestD (List t) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data TrD f a = TrD a f deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- Explicit mutually recursive+data Forest a = Forest (List (Tr a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data Tr a = Tr a (Forest a) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Words = Words Word8 Word16 Word32 Word64+            deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Ints = Ints Int8 Int16 Int32 Int64+            deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- non-recursive data type+data Various = V1 (Maybe Bool) | V2 Bool (Either Bool (Maybe Bool))+              deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- Phantom type+data Phantom a = Phantom deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+++-- Recursive data types++data RR a b c = RN {rna::a, rnb::b ,rnc::c}+              | RA a (RR a a c) b+              | RAB a (RR c b a) b+  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Expr = ValB Bool | Or Expr Expr | If Expr Expr Expr  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data List a = C a (List a)+            | N+  deriving (Eq, Ord, Read, Show, Typeable, Traversable, Data, Generic ,Generic1,Functor,Foldable)++data ListS a = Nil | Cons a (ListS a)+  deriving (Eq, Ord, Read, Show, Typeable, Functor, Foldable, Traversable, Data, Generic ,Generic1)++-- non-regular Haskell datatypes like:+-- Binary instances but no Model+data Nest a = NilN | ConsN (a, Nest (a, a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data TN a = LeafT a | BranchT (TN (a,a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Bush a = NilB | ConsB (a, Bush (Bush a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- Perfectly balanced binary tree+data Perfect a = ZeroP a | SuccP (Perfect (Fork a)) deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data Fork a = Fork a a deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- non regular with higher-order kind parameters+-- no Binary/Model instances+data PerfectF f α = NilP | ConsP α (PerfectF f (f α)) deriving (Typeable,Generic) -- No Data++data Pr f g a = Pr (f a (g a))++data Higher f a = Higher (f a) deriving (Typeable,Generic,Data)++-- data Pr2 (f :: * -> *) a = Pr2 (f )++data Free f a = Pure a | Roll (f (Free f a)) deriving (Typeable,Generic)++-- mutual references+data A = A B | AA Int deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data B = B A | BB Char deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- recursive sets:+-- Prob: ghc will just explode on this+-- data MM1 = MM1 MM2 MM4 MM0 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- data MM0 = MM0 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic) +-- data MM2 = MM2 MM3 Bool deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- data MM3 = MM3 MM4 Bool deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- data MM4 = MM4 MM4 MM2 MM5 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- data MM5 = MM5 Unit MM6 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+-- data MM6 = MM6 MM5 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data A0 = A0 B0 B0 D0 Bool+        | A1 (List Bool) (List Unit) (D2.List Bool) (D2.List Bool)+        deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data B0 = B0 C0 | B1 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data C0 = C0 A0 | C1 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data D0 = D0 E0 | D1 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+data E0 = E0 D0 | E1 deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Even = Zero | SuccE Odd+data Odd = SuccO Even++-- Existential types+-- data Fold a b = forall x. Fold (x -> a -> x) x (x -> b)++-- data Some :: (* -> *) -> * where+--   Some :: f a -> Some f++-- data Dict (c :: Constraint) where+--   Dict :: c => Dict c+data Direction = North | South | Center | East | West+               deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Stream a = Stream a (Stream a)+            deriving (Eq, Ord, Read, Show, Typeable, Data, Generic,Functor,Foldable,Traversable)++data Tree a = Node (Tree a) (Tree a) | Leaf a+            deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++-- Example schema from: http://mechanical-sympathy.blogspot.co.uk/2014/05/simple-binary-encoding.html+data Car = Car {+  serialNumber::Word64+  ,modelYear::Word16+  ,available::Bool+  ,code::CarModel+  ,someNumbers::[Int32]+  ,vehicleCode::String+  ,extras::[OptionalExtra]+  ,engine::Engine+  ,fuelFigures::[Consumption]+  ,performanceFigures :: [(OctaneRating,[Acceleration])]+  ,make::String+  ,carModel::String+  } deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Acceleration = Acceleration {mph::Word16,seconds::Float} deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++type OctaneRating = Word8 -- minValue="90" maxValue="110"++data Consumption = Consumption {cSpeed::Word16,cMpg::Float} deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data CarModel = ModelA | ModelB | ModelC  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data OptionalExtra = SunRoof | SportsPack | CruiseControl deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)++data Engine = Engine {+  capacity :: Word16+  ,numCylinders:: Word8+  ,maxRpm:: Word16 -- constant 9000+  ,manufacturerCode :: String+  ,fuel::String -- constant Petrol+  } deriving (Eq, Ord, Read, Show, Typeable, Data, Generic)+
+ test/Test/Data/Model.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE StandaloneDeriving ,DeriveGeneric ,ScopedTypeVariables ,FlexibleContexts ,DeriveAnyClass #-}+module Test.Data.Model where++import           Data.Model+import           Test.Data+import qualified Test.Data2 as Data2+import qualified Test.Data3 as Data3+import Data.Word+import GHC.Generics+import Data.Proxy+import Data.Typeable++-- instance Model Word8+-- instance Model Words+-- instance Model Ints++-- instance Model ADT+-- instance Model MM0+-- instance Model MM1+-- instance Model MM2+-- instance Model MM3+-- instance Model MM4+-- instance Model MM5+-- instance Model MM6++instance Model Void+instance Model Unit++instance Model N3+instance Model N+instance Model Un+instance Model D2+instance Model D4+instance Model A0+instance Model B0+instance Model C0+instance Model D0+instance Model E0++instance Model Various+instance Model a => Model (Phantom a)+instance Model a => Model (Data2.List a)+instance Model a => Model (Data3.List a)+instance Model a => Model (List a)+instance Model a => Model (Tree a)+instance (Model a, Model b, Model c) => Model (RR a b c)+instance Model Expr+instance Model a => Model (Perfect a)+instance Model a => Model (Fork a)+instance Model a => Model (Forest a)+instance Model a => Model (Tr a)+instance Model t => Model (ForestD t)+instance (Model f,Model a) => Model (TrD f a)+instance Model a => Model (Forest2 a)+instance Model a => Model (Tr2 a)++-- Higher kind+-- instance (Model a,Model f) => Model (Higher f a)+-- instance (Model (f a),Typeable f,Model a) => Model (PerfectF f a)+-- instance (Model v,Model (f v),Model a) => Model (Free f a)+
+ test/Test/Data2.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE MultiParamTypeClasses ,DeriveGeneric ,DeriveDataTypeable ,ScopedTypeVariables ,GADTs ,NoMonomorphismRestriction ,DeriveGeneric ,DefaultSignatures ,TemplateHaskell ,TypeFamilies ,FlexibleContexts ,FlexibleInstances ,EmptyDataDecls #-}+module Test.Data2 where++import           Data.Typeable+import           Data.Data+import           GHC.Generics++-- A definition with the same name of a definition in Test.Data, used to test for name clashes.a+data List a = Cons2 a (List a)+            | Nil2+  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic ,Generic1)+
+ test/Test/Data3.hs view
@@ -0,0 +1,12 @@+{-# LANGUAGE MultiParamTypeClasses ,DeriveGeneric ,DeriveDataTypeable ,ScopedTypeVariables ,GADTs ,NoMonomorphismRestriction ,DeriveGeneric ,DefaultSignatures ,TemplateHaskell ,TypeFamilies ,FlexibleContexts ,FlexibleInstances ,EmptyDataDecls #-}+module Test.Data3 where++import           Data.Typeable+import           Data.Data+import           GHC.Generics++-- A definition identical to the one in Test.Data, used to test for name clashes.+data List a = C a (List a)+            | N+  deriving (Eq, Ord, Read, Show, Typeable, Data, Generic ,Generic1)+