th-kinds 0.0.1 → 0.1.0
raw patch · 3 files changed
+46/−58 lines, 3 filesdep ~template-haskellPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: template-haskell
API changes (from Hackage documentation)
Files
- Language/Haskell/TH/KindInference.hs +31/−45
- Language/Haskell/TH/Unification.hs +13/−11
- th-kinds.cabal +2/−2
Language/Haskell/TH/KindInference.hs view
@@ -11,7 +11,7 @@ import Debug.Trace import Data.Map((!)) import Data.Set-import Control.Monad.State+import Control.Monad.State.Strict import Text.ParserCombinators.ReadP hiding (get) import Language.Haskell.TH hiding (AppE)@@ -54,11 +54,11 @@ fK <- infer f xK <- infer x let var = Var (AppT f x)- lift $ unify fK (xK `kindArrow` var)+ unify fK (xK ->- var) return var infer (SigT t k) = do tK <- infer t- lift $ unify tK (kToTerm k)+ unify tK (kToTerm k) return tK infer (ForallT bdrs cxt t) = do mapM_ handleBdr bdrs@@ -80,26 +80,24 @@ return k)) examine :: Maybe Name -> Name -> LoopKillerT (KindUT Q) ()-examine name0 name = case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of- (n:_) -> do lift $ unify (tyVar name) (tupleKind n star)- mUnify name0 (tyVar name)+examine name0 name = do+ mUnify name0 (tyVar name)+ case [n | (n, "") <- readP_to_S matchUnboxedTuple (nameBase name)] of+ (n:_) -> unify (tyVar name) (tupleKind n star) _ -> do inf <- lift $ lift $ reify name case inf of ClassI dec -> examineDec name0 dec TyConI dec -> examineDec name0 dec- PrimTyConI name n _ -> do- lift $ unify (tyVar name) (tupleKind n star)- mUnify name0 (tyVar name)- TyVarI name typ -> do- kind <- infer typ- lift $ unify (tyVar name) kind- mUnify name0 (tyVar name)- _ -> return ()+ PrimTyConI name n _ -> unify (tyVar name) (tupleKind n star)+ TyVarI name typ -> do+ kind <- infer typ+ unify (tyVar name) kind+ _ -> return () mUnify :: Maybe Name -> KindUTerm -> LoopKillerT (KindUT Q) () mUnify name0 k = case name0 of - Just name0 -> lift $ unify (tyCon name0) k+ Just name0 -> unify (tyCon name0) k _ -> return () examineDec :: Maybe Name -> Dec -> LoopKillerT (KindUT Q) ()@@ -109,7 +107,7 @@ modify (insert name) mapM_ handleCxt cxt args <- mapM handleBdr bdrs- lift $ unify (tyCon name) (foldr kindArrow star args)+ unify (tyCon name) (foldr (->-) star args) mUnify name0 (tyCon name) mapM_ handleCon cons examineDec name0 (NewtypeD cxt name bdrs con _) = do@@ -118,7 +116,7 @@ modify (insert name) mapM_ handleCxt cxt args <- mapM handleBdr bdrs- lift $ unify (tyCon name) (foldr kindArrow star args)+ unify (tyCon name) (foldr (->-) star args) mUnify name0 (tyCon name) handleCon con examineDec name0 (ClassD cxt name bdrs _ _) = do@@ -127,14 +125,14 @@ modify (insert name) mapM_ handleCxt cxt args <- mapM handleBdr bdrs- lift $ unify (tyCon name) (foldr kindArrow star args)+ unify (tyCon name) (foldr (->-) star args) mUnify name0 (tyCon name) examineDec name0 (FamilyD _ name bdrs mK) = do visited <- get unless (name `member` visited) $ do modify (insert name)- args <- mapM handleBdr bdrs- lift $ unify (tyCon name) (maybe star kToTerm mK)+ mapM_ handleBdr bdrs+ unify (tyCon name) (maybe star kToTerm mK) mUnify name0 (tyCon name) examineDec name0 (TySynD name bdrs typ) = do visited <- get@@ -142,22 +140,16 @@ modify (insert name) args <- mapM handleBdr bdrs kind <- infer typ- lift $ unify (tyCon name) (foldr kindArrow kind args)+ unify (tyCon name) (foldr (->-) kind args) mUnify name0 (tyCon name) examineDec _ _ = return () handleCon :: Con -> LoopKillerT (KindUT Q) ()-handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> do- k <- infer t- lift $ unify k star) ts-handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> do- k <- infer t- lift $ unify k star) ts+handleCon (NormalC _ ts) = mapM_ (\ (_, t) -> infer t >>= unify star) ts+handleCon (RecC _ ts) = mapM_ (\ (_, _, t) -> infer t >>= unify star) ts handleCon (InfixC (_, t1) _ (_, t2)) = do- k1 <- infer t1- k2 <- infer t2- lift $ unify k1 star- lift $ unify k2 star+ infer t1 >>= unify star+ infer t2 >>= unify star handleCon (ForallC bdrs cxt con) = do mapM_ handleBdr bdrs mapM_ handleCxt cxt@@ -172,37 +164,31 @@ handleBdr :: TyVarBndr -> LoopKillerT (KindUT Q) KindUTerm handleBdr (PlainTV n) = return (tyVar n) handleBdr (KindedTV n k) = do- lift $ unify (tyVar n) (kToTerm k)+ unify (tyVar n) (kToTerm k) return (tyVar n) handleCxt :: Pred -> LoopKillerT (KindUT Q) () handleCxt (ClassP name args) = do kinds <- mapM infer args- lift $ unify (Var (ConT name)) (foldr kindArrow star kinds)+ unify (Var (ConT name)) (foldr (->-) star kinds) examine (Just name) name handleCxt (EqualP t1 t2) = do k1 <- infer t1 k2 <- infer t2- lift $ unify k1 k2+ unify k1 k2 kToTerm :: Kind -> KindUTerm-kToTerm = kToTerm' . fixKind where- kToTerm' (ArrowK a b) = kToTerm' a `kindArrow` kToTerm' b- kToTerm' StarK = star--fixKind :: Kind -> Kind-fixKind k = loop k StarK where- loop StarK k = k- loop (ArrowK k1 k2) k = loop k1 (loop k2 StarK `ArrowK` k)+kToTerm (ArrowK a b) = kToTerm a ->- kToTerm b+kToTerm StarK = star -kindArrow :: KindUTerm -> KindUTerm -> KindUTerm-kindArrow = App KindArrow+(->-) :: KindUTerm -> KindUTerm -> KindUTerm+(->-) = App KindArrow star :: KindUTerm star = Atom Star tupleKind :: Int -> KindUTerm -> KindUTerm-tupleKind n k = foldr kindArrow k (replicate n star)+tupleKind n k = foldr (->-) k (replicate n star) instance (Ppr a, Ppr b) => Ppr (Either a b) where ppr (Left x) = text "Left" <+> parens (ppr x)
Language/Haskell/TH/Unification.hs view
@@ -1,6 +1,6 @@-{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-}+{-# LANGUAGE UndecidableInstances, FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies, TypeSynonymInstances, StandaloneDeriving, GeneralizedNewtypeDeriving #-} -module Language.Haskell.TH.Unification (subTerm, Term(..), UnifT, Explicit(..), unify, solveUnification) where+module Language.Haskell.TH.Unification (subTerm, Term(..), MonadUnify(..), UnifT, Explicit(..), solveUnification) where import Control.Monad import Data.Map hiding (map)@@ -18,12 +18,18 @@ deriving instance (Monad m) => Monad (UnifT f v a m) deriving instance (Monad m) => MonadState (Constraints f v a) (UnifT f v a m) +class Monad m => MonadUnify u m | m -> u where+ unify :: u -> u -> m ()++instance Monad m => MonadUnify (Term f v a) (UnifT f v a m) where+ a `unify` b = modify ((a :==: b):)++instance MonadUnify u m => MonadUnify u (StateT s m) where+ a `unify` b = lift (a `unify` b)+ instance MonadTrans (UnifT f v a) where lift = UnifT . lift . lift -unify :: (Monad m) => Term f v a -> Term f v a -> UnifT f v a m ()-a `unify` b = modify ((a :==: b):)- runUnification :: (Ord v, Eq f, Eq a, Monad m) => UnifT f v a m x -> m (Either String (Constraints f v a)) runUnification (UnifT m) = runErrorT (execStateT m []) @@ -45,8 +51,8 @@ | a == b -> solve def constrs | otherwise -> fail "Mismatched atoms" App f1 x1 y1 :==: App f2 x2 y2- | f1 /= f2 -> fail "Mismatched functions"- | otherwise -> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)+ | f1 == f2 -> solve def ([x1 :==: x2, y1 :==: y2] ++ constrs)+ | otherwise -> fail "Mismatched functions" _ -> fail "Function matched to atom" solve _ [] = return empty @@ -64,7 +70,3 @@ subSol :: (Ord v, Eq f, Eq a) => Explicit f a -> v -> Term f v a -> Solution f v a -> Solution f v a subSol def v t sol = insert v (subTerm def sol t) sol- --- test :: UnifT Char String String IO ()--- test = do App 'f' (App 'g' (Var "A") (Var "A")) (Var "A") `unify`--- App 'f' (Var "B") (Atom "xyz")
th-kinds.cabal view
@@ -1,5 +1,5 @@ Name: th-kinds-Version: 0.0.1+Version: 0.1.0 Category: Template Haskell Author: Louis Wasserman License: BSD3@@ -9,7 +9,7 @@ Description: Given the name of a Haskell type, typeclass, type family, or any of the above, determines its kind. Maintainer: Louis Wasserman <wasserman.louis@gmail.com> Build-type: Simple-build-depends: template-haskell >= 2.4.0.0 , base >= 4 && < 5, containers >= 0.3, mtl+build-depends: template-haskell == 2.4.0.1 , base >= 4 && < 5, containers >= 0.3, mtl exposed-modules: Language.Haskell.TH.KindInference