packages feed

th-context 0.23 → 0.24

raw patch · 7 files changed

+480/−105 lines, 7 filesdep +atp-haskelldep +prettydep −th-typegraph

Dependencies added: atp-haskell, pretty

Dependencies removed: th-typegraph

Files

+ Data/Logic/ATP/TH.hs view
@@ -0,0 +1,180 @@+-- | ATP instances for the template haskell type 'Type', and the+-- conjunction of such types, @[Type]@.  In these instances, almost+-- every role is played by 'Type'.  It might a case where the tagged+-- package could be used to advantage.  A list represents conjunction,+-- but there is no disjunction operation, nor any derived from it like+-- implication or equivalence.++{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TypeFamilies, UndecidableInstances #-}+module Data.Logic.ATP.TH+    ( unfoldApply+    , expandBindings+    ) where++import Control.Monad.State (modify)+import Data.Generics (everywhere, mkT)+import Data.List (intersperse)+import Data.Logic.ATP (IsAtom, IsVariable(..), IsFunction, IsPredicate, HasEquate(..))+import Data.Logic.ATP.Apply (HasApply(PredOf, TermOf, applyPredicate, foldApply', overterms, onterms))+import Data.Logic.ATP.Formulas (IsFormula(..))+import Data.Logic.ATP.Lit (IsLiteral(..), JustLiteral)+import Data.Logic.ATP.Pretty (hcat, HasFixity(..), Pretty(pPrint), text)+import Data.Logic.ATP.Prop (IsPropositional(..))+import Data.Logic.ATP.Term (IsTerm(..))+import Data.Logic.ATP.Unif (Unify(UTermOf, unify'), unify_literals)+import Data.Map as Map (insertWithKey, lookup, Map)+import Data.Maybe (fromMaybe)+import Data.Monoid ((<>))+import Data.String (IsString(fromString))+import Language.Haskell.TH+import Language.Haskell.TH.PprLib (to_HPJ_Doc)+import Language.Haskell.TH.Expand (pprint1)++newtype Context = Context [Type] deriving (Eq, Ord, Show)++-- | Helper function to interpret a type application:+--     @unfoldApply (AppT (AppT (AppT (VarT (mkName "a")) StarT) ListT) ArrowT) -> (VarT (mkName "a"), [StarT, ListT, ArrowT])@+-- The inverse is @uncurry . foldl AppT@.+unfoldApply :: Type -> [Type] -> (Type, [Type])+unfoldApply (AppT t1 t2) ts = unfoldApply t1 (t2 : ts)+unfoldApply t ts = (t, ts)++instance HasFixity Type where+    precedence _ = undefined+    associativity _ = undefined++instance Pretty Type where+    pPrint = to_HPJ_Doc . ppr++instance Pretty Context where+    pPrint (Context ts) = text "(" <> hcat (intersperse (text ", ") (map pPrint ts)) <> text ")"++instance IsAtom Type++instance IsAtom Context++instance IsString Type where+    fromString = VarT . mkName++instance IsString Context where+    fromString = Context . (: []) . fromString++instance IsVariable Type where+    variant _v _vs = error "variant" -- Maybe we should use newName here?  That means using the Q monad everywhere.+    prefix p (VarT name) = VarT (mkName (p ++ nameBase name))+    prefix _p typ = error $ "IsVariable " ++ pprint typ++instance IsFunction Type++-- For type Type, the domain elements are concrete types, while+-- predicates are either EqualityT or class names applied to a+-- suitable number of class type parameters.+instance IsPredicate Type++instance IsTerm Type where+    type (TVarOf Type) = Type+    type (FunOf Type) = Type+    vt = id+    fApp _fn _ts = error "fApp"+    foldTerm vf _af x@(VarT _) = vf x+    foldTerm _vf af x@(ConT _) = af x []+    foldTerm _vf af x = af x []+    -- foldTerm _vf _af t = error $ "foldTerm: " ++ show t++instance HasApply Type where+    type (PredOf Type) = Type+    type (TermOf Type) = Type+    applyPredicate p ts = foldl AppT p ts+    foldApply' _atomf applyf x = uncurry applyf (unfoldApply x []) -- Not yet clear what values comprise the atom type+    overterms _f _r0 _x = error "overterms"+    onterms _f _x = error "onterms"++-- EqualityT is the only predicate I am aware of.+instance HasEquate Type where+    equate a b = AppT (AppT EqualityT a) b+    foldEquate eq _ap (AppT (AppT EqualityT a) b) = eq a b+    foldEquate _eq ap t = uncurry ap (unfoldApply t [])++instance IsFormula Type where+    type (AtomOf Type) = Type+    true = error "true"+    false = error "false"+    asBool = error "asBool"+    atomic = id+    overatoms _f _fm _r0 = error "overatoms"+    onatoms _f _fm = error "onatoms"++instance IsLiteral Type where+    naiveNegate x = error $ "naiveNegate " ++ show x+    foldNegation _f _ne x = error $ "foldNegation " ++ show x+    foldLiteral' _ho _ne _tf at x = at x -- I don't yet know what types are true, false, or negation.  They may not exist.+    -- foldLiteral' _ho _ne _tf _at x = error $ "foldLiteral' " ++ show x++instance JustLiteral Type++instance HasFixity Context where+    precedence _ = undefined+    associativity _ = undefined++instance IsFormula Context where+    type (AtomOf Context) = Type+    true = error "true"+    false = error "false"+    asBool = error "asBool"+    atomic = Context . (: [])+    overatoms _f _fm _r0 = error "overatoms"+    onatoms _f _fm = error "onatoms"++-- A list of types are considered to be AND-ed, as in the 'Cxt' type.+instance IsLiteral Context where+    naiveNegate (Context [x]) = Context [naiveNegate x]+    naiveNegate _lits = error "Invalid Literal"+    foldNegation _f _ne x = error $ "foldNegation " ++ show x+    foldLiteral' _ho _ne _tf at (Context [x]) = at x -- I don't yet know what types are true, false, or negation.  They may not exist.+    foldLiteral' _ho _ne _tf _at x = error $ "foldLiteral' " ++ show x++instance IsPropositional Context where+    Context a .&. Context b = Context (a <> b)+    (.|.) = error "IsPropositional Type: Disjunction not supported"+    (.<=>.) = error "IsPropositional Type: IFF not supported"+    (.=>.) = error "IsPropositional Type: Imp not supported"+    foldPropositional' = error "foldPropositional'"+    foldCombination = error "foldCombination"++instance Monad m => Unify m Type where+    type UTermOf Type = TermOf Type+    unify' (AppT (AppT EqualityT a@(VarT _)) b) = modify (bind a b)+    unify' (AppT (AppT EqualityT a) b@(VarT _)) = modify (bind b a)+    unify' (AppT (AppT EqualityT (AppT a b)) (AppT c d)) =+        -- I'm told this is incorrect in the presence of type functions+        unify' (AppT (AppT EqualityT a) c) >> unify' (AppT (AppT EqualityT b) d)+    unify' (AppT (AppT EqualityT a) b) | a == b = return ()+    unify' (AppT (AppT EqualityT a) b) = fail $ "Cannot unify: (" ++ pprint1 a ++ ", " ++ pprint1 b ++ ")"+    unify' _ = return ()++instance Monad m => Unify m [Type] where+    type UTermOf [Type] = TermOf Type+    unify' = mapM_ unify'++-- | Create a new variable binding, making sure all bound variables in+-- are expanded in the resulting map.+bind :: Pred -> Pred -> Map Pred Pred -> Map Pred Pred+bind v@(VarT _) a mp =+    -- First, expand all occurrences of the new variable in existing bindings+    let mp' = everywhere (mkT (expandBinding v a)) mp in+    -- Next, expand all bound variables in the new binding+    let a' = everywhere (mkT (expandBindings mp')) a in+    -- Does this introduce any recursive bindings?+    let a'' = everywhere (mkT (expandBinding v (error $ "Recursive binding of " ++ show v))) a' in+    -- If the value is already bound, make sure the binding is identical+    Map.insertWithKey (\v' a1 a2 ->+                           if a1 == a2+                           then a1+                           else error ("Conflicting definitions of " ++ show v' ++ ":\n  " ++ show a1 ++ "\n  " ++ show a2)) v a'' mp'++expandBindings :: Map Pred Pred -> Pred -> Pred+expandBindings mp x@(VarT _) = fromMaybe x (Map.lookup x mp)+expandBindings _ x = x++expandBinding :: Pred -> Pred -> Pred -> Pred+expandBinding v a x = if x == v then a else x
Language/Haskell/TH/Context.hs view
@@ -17,26 +17,32 @@ {-# OPTIONS_GHC -Wall -fno-warn-orphans #-} module Language.Haskell.TH.Context     ( InstMap+    , ContextM     , DecStatus(Declared, Undeclared, instanceDec)     , reifyInstancesWithContext     , tellInstance     , tellUndeclared+    , noInstance     ) where -import Data.Maybe (isJust)+import Control.Lens (view) import Control.Monad (filterM)+import Control.Monad.Reader (ReaderT)+import Control.Monad.State (execStateT) import Control.Monad.States (MonadStates, getPoly, modifyPoly)-import Control.Monad.Writer (MonadWriter, tell)+import Control.Monad.Writer (MonadWriter, tell, WriterT) import Data.Generics (everywhere, mkT) import Data.List (intercalate)+import Data.Logic.ATP.TH (expandBindings {-instance Unify [Type]-})+import Data.Logic.ATP.Unif (Unify(unify'), unify) import Data.Map as Map (elems, insert, lookup, Map) import Data.Maybe (mapMaybe)--- import Debug.Trace (trace)+import Debug.Trace (trace) import Language.Haskell.TH import Language.Haskell.TH.Desugar as DS (DsMonad) import Language.Haskell.TH.PprLib (cat, ptext) import Language.Haskell.TH.Syntax hiding (lift)-import Language.Haskell.TH.TypeGraph.Expand (ExpandMap, expandType, E(unE))+import Language.Haskell.TH.Expand (ExpandMap, expandType, E, unE) import Language.Haskell.TH.Instances ({- Ord instances from th-orphans -})  -- FIXME: Should actually be Map (E Pred) (Maybe (DecStatus@@ -44,6 +50,14 @@ -- compile error. type InstMap = Map (E Pred) [DecStatus InstanceDec] +-- | Combine the DsMonad (desugaring), which includes the Q monad, and+-- state to record declared instances, type expansions, and a string+-- for debugging messages.+class (DsMonad m, MonadStates InstMap m, MonadStates ExpandMap m, MonadStates String m) => ContextM m++instance ContextM m => ContextM (ReaderT r m)+instance (ContextM m, Monoid w) => ContextM (WriterT w m)+ -- | Did we get this instance from the Q monad or does it still need to be spliced? data DecStatus a     = Declared {instanceDec :: a}@@ -65,15 +79,15 @@ -- monad 'InstMap', associated with an empty list of predicates, and the -- empty list is returned.  Later the caller can use 'tellInstance' to -- associate instances with the predicate.-reifyInstancesWithContext :: forall m. (DsMonad m, MonadStates InstMap m, MonadStates ExpandMap m) =>-                             Name -> [Type] -> m [InstanceDec]+reifyInstancesWithContext :: forall m. ContextM m => Name -> [Type] -> m [InstanceDec] reifyInstancesWithContext className typeParameters = do   p <- expandType $ foldInstance className typeParameters   mp <- getPoly :: m InstMap   case Map.lookup p mp of     Just x -> return $ map instanceDec x     Nothing -> do-      -- trace ("        -> reifyInstancesWithContext " ++ pprint (foldInstance className typeParameters) ++ "...") (return ())+      modifyPoly ("  " ++)+      pre <- getPoly :: m String       -- Add an entry with a bogus value to limit recursion on       -- the predicate we are currently testing       modifyPoly (Map.insert p [] :: InstMap -> InstMap)@@ -81,89 +95,76 @@       insts <- qReifyInstances className typeParameters       -- Filter out the ones that conflict with the instance context       r <- filterM (testInstance className typeParameters) insts+#ifdef DEBUG+      trace (intercalate ("\n" ++ pre ++ "    ")+                         ((pre ++ "reifyInstancesWithContext " ++ pprint1 (foldInstance className typeParameters) ++ " -> [") :+                          map (\(InstanceD _ typ _) -> pprint1 typ) r) +++                         "]") (return ())+#endif       -- Now insert the correct value into the map and return it.  Because       -- this instance was discovered in the Q monad it is marked Declared.       modifyPoly (Map.insert p (map Declared r))       -- trace ("        <- reifyInstancesWithContext " ++ pprint (foldInstance className typeParameters) ++ " -> " ++ pprint r) (return ())+      modifyPoly (drop 2 :: String -> String)       return r  -- | Test one of the instances returned by qReifyInstances against the -- context we have computed so far.  We have already added a ClassP predicate -- for the class and argument types, we now need to unify those with the -- type returned by the instance and generate some EqualP predicates.-testInstance :: (DsMonad m, MonadStates InstMap m, MonadStates ExpandMap m) => Name -> [Type] -> InstanceDec -> m Bool-testInstance className typeParameters (InstanceD instanceContext instanceType _) = do+testInstance :: ContextM m => Name -> [Type] -> InstanceDec -> m Bool+testInstance className typeParameters+#if MIN_VERSION_template_haskell(2,11,0)+                 (InstanceD Nothing instanceContext instanceType _)+#else+                 (InstanceD instanceContext instanceType _)+#endif+                     = do   -- The new context consists of predicates derived by unifying the   -- type parameters with the instance type, plus the prediates in the   -- instance context field.-  mapM expandType (instancePredicates (reverse typeParameters) instanceType ++ instanceContext) >>= testContext . map unE+  mapM expandType (instancePredicates ++ instanceContext) >>= testContext . map (view unE)     where-      instancePredicates :: [Type] -> Type -> [Pred]-      instancePredicates (x : xs) (AppT l r) = AppT (AppT EqualityT x) r : instancePredicates xs l-      instancePredicates [] (ConT className') | className == className' = []-      instancePredicates _ _ =-          error $ (unlines ["testInstance: Failure unifying instance with arguments.  This should never",-                            "happen because qReifyInstance returned this instance for these exact arguments:",-                            " typeParameters=[" ++ intercalate ", " (map show typeParameters) ++ "]",-                            " instanceType=" ++ show instanceType])+      instancePredicates :: [Pred]+      instancePredicates = maybe (error $ "Invalid instance type: " ++ show instanceType) instanceEqualities (unfoldInstance instanceType)+      instanceEqualities (_, instanceArgs)+          | length instanceArgs /= length typeParameters =+              error $ "type class arity error:" +++                      "\n  class name = " ++ show className +++                      "\n  type parameters = " ++ show typeParameters +++                      "\n  instance args = " ++ show instanceArgs+      instanceEqualities (_, instanceArgs) = map (\(a, b) ->  AppT (AppT EqualityT a) b) (zip typeParameters instanceArgs) testInstance _ _ x = error $ "qReifyInstances returned something that doesn't appear to be an instance declaration: " ++ show x  -- | Now we have predicates representing the unification of the type--- parameters with the instance type.  Are they consistent?  Find out--- using type synonym expansion, variable substitution, elimination of--- vacuous predicates, and unification.-testContext :: (DsMonad m, MonadStates InstMap m, MonadStates ExpandMap m) => [Pred] -> m Bool-testContext context =-    and <$> (simplifyContext context >>= mapM consistent)---- | Perform type expansion on the predicates, then simplify using--- variable substitution and eliminate vacuous equivalences.-simplifyContext :: (DsMonad m, MonadStates InstMap m) => [Pred] -> m [Pred]-simplifyContext context =-    do let context' = concat $ map unify context-       let context'' = foldl simplifyPredicate context' context'-       if (context'' == context) then return context'' else simplifyContext context''---- | Try to simplify the context by eliminating of one of the predicates.--- If we succeed start again with the new context.-simplifyPredicate :: [Pred] -> Pred -> [Pred]-simplifyPredicate context (AppT (AppT EqualityT v@(VarT _)) b) = everywhere (mkT (\ x -> if x == v then b else x)) context-simplifyPredicate context (AppT (AppT EqualityT a) v@(VarT _)) = everywhere (mkT (\ x -> if x == v then a else x)) context-simplifyPredicate context p@(AppT (AppT EqualityT a) b) | a == b = filter (/= p) context-simplifyPredicate context _ = context---- | Unify the two arguments of an EqualP predicate, return a list of--- simpler predicates associating types with a variables.-unify :: Pred -> [Pred]-unify (AppT (AppT EqualityT (AppT a b)) (AppT c d)) = unify (AppT (AppT EqualityT a) c) ++ unify (AppT (AppT EqualityT b) d)-unify (AppT (AppT EqualityT (ConT a)) (ConT b)) | a == b = []-unify (AppT (AppT EqualityT a@(VarT _)) b) = [AppT (AppT EqualityT a) b]-unify (AppT (AppT EqualityT a) b@(VarT _)) = [AppT (AppT EqualityT a) b]-unify x = [x]+-- parameters with the instance type, along with the instance+-- superclasses.  Are they consistent?  Find out using type synonym+-- expansion, variable substitution, elimination of vacuous+-- predicates, and unification.+testContext :: ContextM m => [Pred] -> m Bool+testContext context = and <$> (unify context mempty >>= \mp -> mapM consistent (everywhere (mkT (expandBindings mp)) context)) --- | Decide whether a predicate is consistent with the accumulated--- context.  Use recursive calls to reifyInstancesWithContext when--- we encounter a class name applied to a list of type parameters.-consistent :: (DsMonad m, MonadStates InstMap m, MonadStates ExpandMap m) => Pred -> m Bool-consistent typ-    | isJust (unfoldInstance typ) =-        let Just (className, typeParameters) = unfoldInstance typ in-        (not . null) <$> reifyInstancesWithContext className typeParameters-consistent (AppT (AppT EqualityT (AppT a b)) (AppT c d)) =-    -- I'm told this is incorrect in the presence of type functions-    (&&) <$> consistent (AppT (AppT EqualityT a) c) <*> consistent (AppT (AppT EqualityT b) d)-consistent (AppT (AppT EqualityT (VarT _)) _) = return True-consistent (AppT (AppT EqualityT _) (VarT _)) = return True+-- | Decide whether a predicate returned by 'unify' is+-- consistent with the accumulated context.  Use recursive calls to+-- reifyInstancesWithContext when we encounter a class name applied to+-- a list of type parameters.+consistent :: ContextM m => Pred -> m Bool consistent (AppT (AppT EqualityT a) b) | a == b = return True-consistent (AppT (AppT EqualityT _) _) = return False-consistent typ = error $ "Unexpected Pred: " ++ pprint typ+consistent typ =+    maybe (error $ "Unexpected Pred: " ++ pprint typ)+          (\(className, typeParameters) -> (not . null) <$> reifyInstancesWithContext className typeParameters)+          (unfoldInstance typ)  -- | Declare an instance in the state monad, marked Undeclared.  After -- this, the instance predicate (constructed from class name and type -- parameters) will be considered part of the context for subsequent -- calls to reifyInstancesWithContext.-tellInstance :: (DsMonad m, MonadStates InstMap m, Quasi m, MonadStates ExpandMap m) => Dec -> m ()+tellInstance :: ContextM m => Dec -> m ()+#if MIN_VERSION_template_haskell(2,11,0)+tellInstance inst@(InstanceD _ _ instanceType _) =+#else tellInstance inst@(InstanceD _ instanceType _) =+#endif     do let Just (className, typeParameters) = unfoldInstance instanceType        p <- expandType $ foldInstance className typeParameters        (mp :: InstMap) <- getPoly@@ -200,3 +201,35 @@ unfoldInstance (ConT name) = Just (name, []) unfoldInstance (AppT t1 t2) = maybe Nothing (\ (name, types) -> Just (name, types ++ [t2])) (unfoldInstance t1) unfoldInstance _ = Nothing++noInstance :: forall m. ContextM m => Name -> Name -> m Bool+noInstance className typeName =+    null <$> reifyInstancesWithContext className [ConT typeName]+#if 0+    qReify typeName >>= doInfo >>= \typ -> null <$> reifyInstancesWithContext className [typ]+    where+      doInfo :: Info -> m Type+      doInfo (TyConI dec) = doDec dec+      doDec :: Dec -> m Type+      doDec (NewtypeD cxt name tvbs con decs) = doDec (DataD cxt name tvbs [con] decs)+      doDec (DataD _cxt name tvbs _cons _decs) = return $ foldl AppT (ConT name) (map (VarT . toName) tvbs)+      doDec (TySynD name tvbs typ) = return $ foldl AppT (ConT name) (map (VarT . toName) tvbs)+      toName (PlainTV x) = x+      toName (KindedTV x _) = x+#endif+#if 0+noInstance className typeName = do+  i <- qReify typeName+  typ <- case i of+           TyConI (TySynD _name _tvbs typ) ->+               +           TyConI (DataD _cxt _name tvbs _fundeps _decs) ->+               do vs <- mapM (\c -> VarT <$> runQ (newName [c])) (take (length tvbs) ['a'..'z'])+                  return $ foldl AppT (ConT typeName) vs+           _ -> error $ "noInstance - " ++ show typeName ++ " has an invalid type: " ++ show i+  r <- null <$> reifyInstancesWithContext className [typ]+#ifdef DEBUG+  trace ("noInstance " ++ show className ++ " " ++ show typeName ++ " -> " ++ show r) (return ())+#endif+  return r+#endif
+ Language/Haskell/TH/Expand.hs view
@@ -0,0 +1,90 @@+-- | The 'Expanded' class helps keep track of which 'Type' values have+-- been fully expanded to a canonical form.  This lets us use the 'Eq'+-- and 'Ord' relationships on 'Type' and 'Pred' values when reasoning+-- about instance context.  What the 'expandType' function does is use+-- the function from @th-desugar@ to replace occurrences of @ConT name@+-- with the associated 'Type' if @name@ is a declared type synonym+-- @TySynD name _ typ@.  For convenience, a wrapper type 'E' is+-- provided, along with the 'Expanded' instances @E Type@ and @E+-- Pred@.  Now the 'expandType' and 'expandPred' functions can be used+-- to return values of type @E Type@ and @E Pred@ respectively.+--+-- Instances @Expanded Type Type@ and @Expanded Pred Pred@ are+-- provided in "Language.Haskell.TH.Context.Unsafe", for when less+-- type safety is required.++{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}++module Language.Haskell.TH.Expand+    ( E(E, _unE), unE+    , ExpandMap+    , expandType+    , expandPred+    , expandClassP+    , pprint1+    ) where++import Control.Lens (makeLenses)+import Control.Monad.States (MonadStates(getPoly), modifyPoly)+import Data.Data (Data)+import Data.Generics (Data, everywhere, mkT)+import Data.Map as Map (Map, lookup, insert)+import Language.Haskell.Exts.Syntax ()+import Language.Haskell.TH+import Language.Haskell.TH.Desugar as DS (DsMonad, dsType, expand, typeToTH)+import Language.Haskell.TH.Instances ()+import Language.Haskell.TH.PprLib (to_HPJ_Doc)+import Language.Haskell.TH.Syntax -- (Lift(lift))+import Prelude hiding (pred)+import qualified Text.PrettyPrint as HPJ++-- | A concrete type used to mark type which have been expanded+newtype E a = E {_unE :: a} deriving (Eq, Ord, Show, Data)++instance Ppr a => Ppr (E a) where+    ppr (E x) = ppr x++instance Lift (E Type) where+    lift etype = [|E $(lift (_unE etype))|]++$(makeLenses ''E)++-- | The state type used to memoize expansions.+type ExpandMap = Map Type (E Type)++-- | Apply the th-desugar expand function to a 'Type' and mark it as expanded.+expandType :: (DsMonad m, MonadStates ExpandMap m)  => Type -> m (E Type)+expandType typ = do+  getPoly >>= maybe expandType' return . Map.lookup typ+    where+      expandType' =+          do e <- E <$> DS.typeToTH <$> (DS.dsType typ >>= DS.expand)+             modifyPoly (Map.insert typ e)+             return e++-- | Apply the th-desugar expand function to a 'Pred' and mark it as expanded.+-- Note that the definition of 'Pred' changed in template-haskell-2.10.0.0.+expandPred :: (DsMonad m, MonadStates ExpandMap m)  => Type -> m (E Type)+expandPred = expandType++-- | Expand a list of 'Type' and build an expanded 'ClassP' 'Pred'.+expandClassP :: forall m. (DsMonad m, MonadStates ExpandMap m)  => Name -> [Type] -> m (E Type)+expandClassP className typeParameters = (expandType $ foldl AppT (ConT className) typeParameters) :: m (E Type)++pprint1 :: (Ppr a, Data a) => a -> [Char]+pprint1 = pprintStyle (HPJ.style {HPJ.mode = HPJ.OneLineMode}) . friendlyNames++pprintStyle :: (Ppr a, Data a) => HPJ.Style -> a -> String+pprintStyle style = HPJ.renderStyle style . to_HPJ_Doc . ppr++friendlyNames :: Data a => a -> a+friendlyNames =+    everywhere (mkT friendlyName)+    where+      friendlyName (Name x _) = Name x NameS -- Remove all module qualifiers
test/Common.hs view
@@ -1,19 +1,21 @@-{-# LANGUAGE FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TemplateHaskell #-}+{-# LANGUAGE CPP, FlexibleContexts, FlexibleInstances, MultiParamTypeClasses, TemplateHaskell #-} module Common where  import Control.Lens (makeLenses, use, (.=)) import Control.Monad.State (evalStateT, StateT) import Control.Monad.States (MonadStates(getPoly, putPoly))+import Data.Default (Default(def)) import Data.List as List (map) import Data.Map as Map (toList) import Data.Set as Set (Set, difference, empty, toList) import Data.Generics (Data, everywhere, mkT) import Language.Haskell.TH-import Language.Haskell.TH.Context (DecStatus(Declared, Undeclared), InstMap)-import Language.Haskell.TH.TypeGraph.Edges (GraphEdges)-import Language.Haskell.TH.TypeGraph.Expand (ExpandMap)-import Language.Haskell.TH.TypeGraph.Prelude (pprint')-import Language.Haskell.TH.TypeGraph.Vertex (TypeGraphVertex(..), TGV)+import Language.Haskell.TH.Context (ContextM, DecStatus(Declared, Undeclared), InstMap)+import Language.Haskell.TH.Desugar (DsMonad)+import Language.Haskell.TH.Expand (ExpandMap, pprint1)+--import Language.Haskell.TH.TypeGraph.Edges (GraphEdges)+--import Language.Haskell.TH.TypeGraph.Expand (ExpandMap)+--import Language.Haskell.TH.TypeGraph.Vertex (TypeGraphVertex(..), TGV)  data SetDifferences a = SetDifferences {unexpected :: Set a, missing :: Set a} deriving (Eq, Ord, Show) @@ -31,33 +33,43 @@ -- Some very nasty bug is triggered here in ghc-7.8 if we try to implement -- a generic function that unReifies the symbols.  Ghc-7.10 works fine --- pprint'' :: (Data a, Ppr a) => a -> String--- pprint'' = pprint' . unReify+-- pprint' :: (Data a, Ppr a) => a -> String+-- pprint' = pprint1 . unReify  pprintDec :: Dec -> String-pprintDec = pprint' . unReify+pprintDec = pprint1 . unReify  pprintDec' :: DecStatus Dec -> String-pprintDec' (Undeclared x) = "Undeclared (" ++ pprint' (unReify x) ++ ")"-pprintDec' (Declared x) = "Declared (" ++ pprint' (unReify x) ++ ")"+pprintDec' (Undeclared x) = "Undeclared (" ++ pprint1 (unReify x) ++ ")"+pprintDec' (Declared x) = "Declared (" ++ pprint1 (unReify x) ++ ")"  pprintType :: Type -> String-pprintType = pprint' . unReify+pprintType = pprint1 . unReify -pprintVertex :: (Ppr v, TypeGraphVertex v) => v -> String-pprintVertex = pprint'+#if 0+pprintVertex :: (Ppr v, Data v, TypeGraphVertex v) => v -> String+pprintVertex = pprint1+#endif  pprintPred :: Pred -> String-pprintPred = pprint' . unReify+pprintPred = pprint1 . unReify -edgesToStrings :: Ppr key => GraphEdges key -> [(String, [String])]-edgesToStrings mp = List.map (\ (t, ts) -> (pprint' t, map pprint' (Set.toList ts))) (Map.toList mp)+#if 0+edgesToStrings :: (Ppr key, Data key) => GraphEdges key -> [(String, [String])]+edgesToStrings mp = List.map (\ (t, ts) -> (pprint1 t, map pprint1 (Set.toList ts))) (Map.toList mp)+#endif  data S     = S { _instMap :: InstMap-        , _visited :: Set TGV-        , _expanded :: ExpandMap }+        -- , _visited :: Set TGV+        , _expanded :: ExpandMap+        , _prefix :: String } +instance Default S where+    def = S mempty mempty ""++instance DsMonad m => ContextM (StateT S m)+ $(makeLenses ''S)  instance Monad m => MonadStates InstMap (StateT S m) where@@ -68,9 +80,15 @@     getPoly = use expanded     putPoly s = expanded .= s +#if 0 instance Monad m => MonadStates (Set TGV) (StateT S m) where     getPoly = use visited     putPoly s = visited .= s+#endif +instance Monad m => MonadStates String (StateT S m) where+    getPoly = use prefix+    putPoly s = prefix .= s+ evalS :: Monad m => StateT S m a -> m a-evalS action = evalStateT action (S mempty mempty mempty)+evalS action = evalStateT action def
test/Context.hs view
@@ -10,7 +10,10 @@ import Data.Array.IArray import Data.Array.Unboxed import Data.Bits+import Data.Default (def) import Data.List as List (map)+import Data.Logic.ATP (Failing(..), unify)+import Data.Logic.ATP.TH ({- Unify instance for template haskell -}) import Data.Map as Map (Map, empty, map, mapKeys, toList, fromList) import Data.Set as Set (fromList, map, Set) import Language.Haskell.TH@@ -19,8 +22,7 @@ -- import Language.Haskell.TH.Context.Simple (missingInstances, simpleMissingInstanceTest) import Language.Haskell.TH.Desugar (withLocalDeclarations) import Language.Haskell.TH.Syntax (Lift(lift), Quasi(qReifyInstances))-import Language.Haskell.TH.TypeGraph.Expand (E(unE), ExpandMap, expandType)-import Language.Haskell.TH.TypeGraph.Prelude (pprint')+import Language.Haskell.TH.Expand (E(_unE), unE, ExpandMap, expandType, pprint1) import System.Exit (ExitCode) import Test.Hspec hiding (runIO) import Test.Hspec.Core.Spec (SpecM)@@ -38,18 +40,18 @@   it "expands types as expected" $ do      (expected :: [Type]) <- runQ (sequence [ [t| [Char] |], [t|Maybe [Char] |], [t|Maybe (Maybe [Char])|] ])      let actual = $(withLocalDeclarations [] $ flip evalStateT (Map.empty :: ExpandMap) $-                    do (types :: [Type]) <- runQ (sequence [ [t|String|], [t|Maybe String|], [t|Maybe (Maybe String)|] ]) >>= mapM expandType >>= return . List.map unE+                    do (types :: [Type]) <- runQ (sequence [ [t|String|], [t|Maybe String|], [t|Maybe (Maybe String)|] ]) >>= mapM expandType >>= return . List.map (view unE)                        runQ . lift $ types)      actual `shouldBe` expected    -- Test the behavior of th-reify-many   it "can tell that there is an instance NFData Char" $      $(do insts <- qReifyInstances ''NFData [ConT ''Char]-          lift $ List.map pprint' insts) `shouldBe` (["instance Control.DeepSeq.NFData GHC.Types.Char"] :: [String])+          lift $ List.map pprint1 insts) `shouldBe` (["instance NFData Char"] :: [String])    it "can tell that there is no instance NFData ExitCode" $      $(do insts <- qReifyInstances ''NFData [ConT ''ExitCode]-          lift $ List.map pprint' insts) `shouldBe` ([] :: [String])+          lift $ List.map pprint1 insts) `shouldBe` ([] :: [String]) {-   it "can tell that an instance hasn't been declared" $      $(missingInstances simpleMissingInstanceTest [d|instance NFData ExitCode|] >>= lift . List.null)@@ -83,27 +85,40 @@                   lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec) (Map.mapKeys pprintPred mp))))           `shouldBe` noDifferences -}++  it "knows variables with different names unify" $ do+     let a = mkName "a"+         b = mkName "b"+     unify (AppT (AppT EqualityT (VarT a)) (VarT b)) mempty `shouldBe` Success (Map.fromList [(VarT a, VarT b)])+{-+  it "knows variables are not Eq with other types" $ do+     (E (VarT (mkName "a")) == E (AppT (VarT (mkName "b")) (VarT (mkName "c")))) `shouldBe` False++  it "knows different types are not Eq" $ do+     (E (ConT (mkName "a")) == E (ConT (mkName "b"))) `shouldBe` False+-}+   it "can handle multi param class IArray" $ do      (\ (insts, pairs) -> (setDifferences (Set.fromList insts) arrayInstances,                            Map.map Set.fromList (Map.fromList pairs)))              -- Unquote the template haskell Q monad expression              $(do -- Run instances and save the result and the state monad result-                  (insts, s) <- runStateT (reifyInstancesWithContext ''IArray [ConT ''UArray, VarT (mkName "a")]) (S mempty mempty mempty)+                  (insts, s) <- runStateT (reifyInstancesWithContext ''IArray [ConT ''UArray, VarT (mkName "a")]) def                   -- Convert to lists of text so we can lift out of Q-                  lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . unE) (view instMap s)))))+                  lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . _unE) (view instMap s)))))           `shouldBe` (noDifferences,                       -- I don't think this is right                       Map.fromList [("IArray UArray a", Set.map (\ x -> "Declared (" ++ x ++ ")") arrayInstances)] :: Map String (Set String))    it "handles a wrapper instance" $-     $(do (insts, s) <- runStateT (reifyInstancesWithContext ''MyClass [AppT (ConT ''Wrapper) (ConT ''Int)]) (S mempty mempty mempty)-          lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . unE) (view instMap s)))))+     $(do (insts, s) <- runStateT (reifyInstancesWithContext ''MyClass [AppT (ConT ''Wrapper) (ConT ''Int)]) def+          lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . _unE) (view instMap s)))))           `shouldBe` (["instance MyClass a => MyClass (Wrapper a)"],                       [("MyClass (Wrapper Int)",["Declared (instance MyClass a => MyClass (Wrapper a))"]),                        ("MyClass Int",["Declared (instance MyClass Int)"])])   it "handles a multi param wrapper instance" $-     $(do (insts, s) <- runStateT (reifyInstancesWithContext ''MyMPClass [VarT (mkName "a"), AppT (ConT ''Wrapper) (ConT ''Int)]) (S mempty mempty mempty)-          lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . unE) (view instMap s)))))+     $(do (insts, s) <- runStateT (reifyInstancesWithContext ''MyMPClass [VarT (mkName "a"), AppT (ConT ''Wrapper) (ConT ''Int)]) def+          lift (List.map pprintDec insts, Map.toList (Map.map (List.map pprintDec') (Map.mapKeys (pprintPred . _unE) (view instMap s)))))           `shouldBe` (["instance MyMPClass a b => MyMPClass a (Wrapper b)"],                       [("MyMPClass a (Wrapper Int)",["Declared (instance MyMPClass a b => MyMPClass a (Wrapper b))"]),                        ("MyMPClass a Int",["Declared (instance MyMPClass a Int)"])])
test/Values.hs view
@@ -10,10 +10,43 @@ bitsInstances =   Set.fromList     [-      "instance Bits CChar","instance Bits CInt","instance Bits CIntMax","instance Bits CIntPtr","instance Bits CLLong","instance Bits CLong","instance Bits CPtrdiff","instance Bits CSChar","instance Bits CShort","instance Bits CSigAtomic","instance Bits CSize","instance Bits CUChar","instance Bits CUInt","instance Bits CUIntMax","instance Bits CUIntPtr","instance Bits CULLong","instance Bits CULong","instance Bits CUShort","instance Bits CWchar",-      "instance Bits Bool","instance Bits Int","instance Bits Integer","instance Bits Word","instance Bits Word16","instance Bits Word32","instance Bits Word64","instance Bits Word8",+      "instance Bits CChar",+      "instance Bits CInt",+      "instance Bits CIntMax",+      "instance Bits CIntPtr",+      "instance Bits CLLong",+      "instance Bits CLong",+      "instance Bits CPtrdiff",+      "instance Bits CSChar",+      "instance Bits CShort",+      "instance Bits CSigAtomic",+      "instance Bits CSize",+      "instance Bits CUChar",+      "instance Bits CUInt",+      "instance Bits CUIntMax",+      "instance Bits CUIntPtr",+      "instance Bits CULLong",+      "instance Bits CULong",+      "instance Bits CUShort",+      "instance Bits CWchar",+      "instance Bits Bool",+      "instance Bits Int",+      "instance Bits Integer",+      "instance Bits Word",+      "instance Bits Word16",+      "instance Bits Word32",+      "instance Bits Word64",+      "instance Bits Word8",       -- These come and go depending on the version of something.-      "instance Bits Int16","instance Bits Int32","instance Bits Int64","instance Bits Int8","instance Bits Natural"+      "instance Bits Int16",+      "instance Bits Int32",+      "instance Bits Int64",+      "instance Bits Int8",+      "instance Bits Natural",+      -- These are new(?)+      "instance Bits a => Bits (Const a b)",+      "instance Bits a => Bits (Identity a)",+      "instance Bits a => Bits (Tagged s a)"     ]  enumInstances :: Set String
th-context.cabal view
@@ -1,5 +1,5 @@ name:               th-context-version:            0.23+version:            0.24 cabal-version:      >= 1.10 build-type:         Simple license:            BSD3@@ -18,13 +18,18 @@                     the instances inserted into the InstMap are not fully recognized                     when computing the context. extra-source-files: test/Common.hs test/Context.hs test/Tests.hs test/Values.hs+tested-with:        GHC == 7.10.3, GHC == 7.11.*  Library   default-language: Haskell2010   ghc-options:      -Wall -O2   hs-source-dirs: .-  exposed-modules:  Language.Haskell.TH.Context+  exposed-modules:+    Data.Logic.ATP.TH+    Language.Haskell.TH.Context+    Language.Haskell.TH.Expand   build-depends:+    atp-haskell >= 1.14,     base >= 4.8 && < 5,     containers,     data-default,@@ -32,11 +37,11 @@     lens,     mtl,     mtl-unleashed >= 0.5,+    pretty,     syb,     template-haskell >= 2.10,     th-desugar,-    th-orphans >= 0.10.0,-    th-typegraph >= 0.31+    th-orphans >= 0.10.0  test-suite th-context-tests   type:             exitcode-stdio-1.0@@ -45,9 +50,11 @@   main-is:          Tests.hs   build-depends:     array,+    atp-haskell,     base,     bytestring,     containers,+    data-default,     deepseq,     ghc-prim,     hspec,@@ -61,8 +68,7 @@     th-context,     th-desugar,     th-orphans,-    th-reify-many,-    th-typegraph+    th-reify-many   default-language: Haskell2010  source-repository head