packages feed

ghc-typelits-extra 0.1.1 → 0.1.2

raw patch · 9 files changed

+244/−97 lines, 9 filesdep +transformersdep ~ghc-typelits-natnormalise

Dependencies added: transformers

Dependency ranges changed: ghc-typelits-natnormalise

Files

CHANGELOG.md view
@@ -1,6 +1,9 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package -## 0.1.1 *January 20th 2015*+## 0.1.2 *July 8th 2016*+* Solve KnownNat constraints over CLog and GCD, i.e., KnownNat (CLog 2 4)++## 0.1.1 *January 20th 2016* * Compile on GHC 8.0+  ## 0.1 *October 21st 2015*
LICENSE view
@@ -1,4 +1,4 @@-Copyright (c) 2015, Christiaan Baaij+Copyright (c) 2015-2016, University of Twente All rights reserved.  Redistribution and use in source and binary forms, with or without
ghc-typelits-extra.cabal view
@@ -1,5 +1,5 @@ name:                ghc-typelits-extra-version:             0.1.1+version:             0.1.2 synopsis:            Additional type-level operations on GHC.TypeLits.Nat description:   Additional type-level operations on @GHC.TypeLits.Nat@:@@ -24,7 +24,7 @@ license-file:        LICENSE author:              Christiaan Baaij maintainer:          christiaan.baaij@gmail.com-copyright:           Copyright © 2015 University of Twente+copyright:           Copyright © 2015-2016 University of Twente category:            Type System build-type:          Simple extra-source-files:  README.md@@ -48,7 +48,8 @@                        GHC.TypeLits.Extra.Solver.Operations   build-depends:       base                >= 4.8  && <5,                        ghc                 >= 7.10 && <8.2,-                       ghc-tcplugins-extra >= 0.2+                       ghc-tcplugins-extra >= 0.2,+                       transformers        >= 0.4.2.0 && < 0.6   hs-source-dirs:      src   default-language:    Haskell2010   other-extensions:    CPP@@ -66,7 +67,7 @@   Other-Modules:       ErrorTests   build-depends:       base                      >= 4.8 && <5,                        ghc-typelits-extra        >= 0.1.1,-                       ghc-typelits-natnormalise >= 0.4,+                       ghc-typelits-natnormalise >= 0.4.1,                        tasty                     >= 0.10,                        tasty-hunit               >= 0.9   hs-source-dirs:      tests
src/GHC/TypeLits/Extra.hs view
@@ -1,12 +1,5 @@-{-# LANGUAGE DataKinds    #-}-{-# LANGUAGE TypeFamilies #-}--{-# OPTIONS_HADDOCK show-extensions #-}--{-# LANGUAGE Safe #-}- {-|-Copyright  :  (C) 2015, University of Twente+Copyright  :  (C) 2015-2016, University of Twente License    :  BSD2 (see the file LICENSE) Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com> @@ -27,6 +20,14 @@  pragma to the header of your file. -}++{-# LANGUAGE DataKinds    #-}+{-# LANGUAGE TypeFamilies #-}++{-# OPTIONS_HADDOCK show-extensions #-}++{-# LANGUAGE Safe #-}+ module GHC.TypeLits.Extra where  import GHC.TypeLits (Nat)
src/GHC/TypeLits/Extra/Solver.hs view
@@ -1,3 +1,18 @@+{-|+Copyright  :  (C) 2015-2016, University of Twente+License    :  BSD2 (see the file LICENSE)+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>++To use the plugin, add the++@+{\-\# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver \#-\}+@++pragma to the header of your file++-}+ {-# LANGUAGE CPP           #-} {-# LANGUAGE TupleSections #-} @@ -7,36 +22,37 @@ {-# OPTIONS_GHC -fno-warn-deprecations #-} #endif -{-|-Copyright  :  (C) 2015, Christiaan Baaij-License    :  BSD2 (see the file LICENSE)-Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>---} module GHC.TypeLits.Extra.Solver   ( plugin ) where  -- external-import Data.Maybe          (catMaybes, mapMaybe)-import GHC.TcPluginM.Extra (evByFiat, lookupModule, lookupName, tracePlugin)+import Control.Monad             ((<=<))+import Control.Monad.Trans.Maybe (MaybeT (..))+import Data.Maybe                (catMaybes)+import GHC.TcPluginM.Extra       (evByFiat, lookupModule, lookupName,+                                  tracePlugin) #if __GLASGOW_HASKELL__ < 711-import GHC.TcPluginM.Extra (failWithProvenace)+import GHC.TcPluginM.Extra       (failWithProvenace) #endif  -- GHC API+import Class      (Class, classMethods, className, classTyCon)+import FamInst    (tcInstNewTyCon_maybe) import FastString (fsLit)+import Id         (idType) import Module     (mkModuleName) import OccName    (mkTcOcc) import Outputable (Outputable (..), (<+>), ($$), text) import Plugins    (Plugin (..), defaultPlugin)-import TcEvidence (EvTerm)+import PrelNames  (knownNatClassName)+import TcEvidence (EvTerm (EvLit), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM  (TcPluginM, tcLookupTyCon, tcPluginTrace, zonkCt) import TcRnTypes  (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvPred,                    isWanted) import TcType      (typeKind)-import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,-                   eqType)+import Type       (EqRel (NomEq), Kind, PredTree (EqPred, ClassPred), Type, classifyPredType,+                   dropForAlls, eqType, funResultTy, tyConAppTyCon_maybe) import TysWiredIn (typeNatKind)  -- internal@@ -72,11 +88,11 @@ decideEqualSOP defs givens  _deriveds wanteds = do   -- GHC 7.10.1 puts deriveds with the wanteds, so filter them out   let wanteds' = filter (isWanted . ctEvidence) wanteds-  let unit_wanteds = mapMaybe (toNatEquality defs) wanteds'+  unit_wanteds <- catMaybes <$> mapM (runMaybeT . toNatEquality defs) wanteds'   case unit_wanteds of     [] -> return (TcPluginOk [] [])     _  -> do-      unit_givens <- mapMaybe (toNatEquality defs) <$> mapM zonkCt givens+      unit_givens <- catMaybes <$> mapM ((runMaybeT . toNatEquality defs) <=< zonkCt) givens       sr <- simplifyExtra (unit_givens ++ unit_wanteds)       tcPluginTrace "normalised" (ppr sr)       case sr of@@ -87,7 +103,8 @@         Impossible eq -> failWithProvenace (fromNatEquality eq) #endif -type NatEquality = (Ct,ExtraOp,ExtraOp)+type NatEquality  = (Ct,ExtraOp,ExtraOp)+type KnConstraint = (Ct,Class,Type,ExtraOp)  data SimplifyResult   = Simplified [(EvTerm,Ct)]@@ -97,26 +114,34 @@   ppr (Simplified evs) = text "Simplified" $$ ppr evs   ppr (Impossible eq)  = text "Impossible" <+> ppr eq -simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult+simplifyExtra :: [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs   where-    simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult+    simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality KnConstraint] -> TcPluginM SimplifyResult     simples evs [] = return (Simplified (catMaybes evs))-    simples evs (eq@(ct,u,v):eqs') = do+    simples evs (Left eq@((ct,u,v)):eqs') = do       ur <- unifyExtra ct u v       tcPluginTrace "unifyExtra result" (ppr ur)       case ur of         Win  -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'         Lose -> return  (Impossible eq)         Draw -> simples evs eqs'+    simples evs (Right (ct,cls,ty,u):eqs') = do+      tcPluginTrace "unifyExtra KnownNat result" (ppr u)+      case u of+        (I i) -> simples (((,) <$> makeLitDict cls ty (EvNum i) <*> pure ct):evs) eqs'+        _ -> simples evs eqs'  -- Extract the Nat equality constraints-toNatEquality :: ExtraDefs -> Ct -> Maybe NatEquality+toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality KnConstraint) toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq t1 t2       | isNatKind (typeKind t1) || isNatKind (typeKind t1)-      -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2-    _ -> Nothing+      -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)+    ClassPred cls [ty]+      | className cls == knownNatClassName+      -> Right <$> ((ct,cls,ty,) <$> normaliseNat defs ty)+    _ -> fail "Nothing"   where     isNatKind :: Kind -> Bool     isNatKind = (`eqType` typeNatKind)@@ -140,3 +165,32 @@ evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq t1 t2 -> Just (evByFiat "ghc-typelits-extra" t1 t2)     _                  -> Nothing++makeLitDict :: Class -> Type -> EvLit -> Maybe EvTerm+-- THIS CODE IS COPIED FROM:+-- https://github.com/ghc/ghc/blob/8035d1a5dc7290e8d3d61446ee4861e0b460214e/compiler/typecheck/TcInteract.hs#L1973+--+-- makeLitDict adds a coercion that will convert the literal into a dictionary+-- of the appropriate type.  See Note [KnownNat & KnownSymbol and EvLit]+-- in TcEvidence.  The coercion happens in 2 steps:+--+--     Integer -> SNat n     -- representation of literal to singleton+--     SNat n  -> KnownNat n -- singleton to dictionary+--+--     The process is mirrored for Symbols:+--     String    -> SSymbol n+--     SSymbol n -> KnownSymbol n -}+makeLitDict clas ty evLit+  | Just (_, co_dict) <- tcInstNewTyCon_maybe (classTyCon clas) [ty]+    -- co_dict :: KnownNat n ~ SNat n+  , [ meth ]   <- classMethods clas+  , Just tcRep <- tyConAppTyCon_maybe -- SNat+                    $ funResultTy     -- SNat n+                    $ dropForAlls     -- KnownNat n => SNat n+                    $ idType meth     -- forall n. KnownNat n => SNat n+  , Just (_, co_rep) <- tcInstNewTyCon_maybe tcRep [ty]+        -- SNat n ~ Integer+  , let ev_tm = mkEvCast (EvLit evLit) (mkTcSymCo (mkTcTransCo co_dict co_rep))+  = Just ev_tm+  | otherwise+  = Nothing
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -1,12 +1,46 @@-module GHC.TypeLits.Extra.Solver.Operations where+{-|+Copyright  :  (C) 2015-2016, University of Twente+License    :  BSD2 (see the file LICENSE)+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>+-} +{-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}+#if __GLASGOW_HASKELL__ < 711+{-# LANGUAGE StandaloneDeriving #-}+#endif++module GHC.TypeLits.Extra.Solver.Operations+  ( ExtraOp (..)+  , EType (..)+  , mergeGCD+  , mergeCLog+  , mergeExp+  , mergeAdd+  , mergeSub+  , mergeMul+  )+where+ -- GHC API import Outputable (Outputable (..), (<+>), integer, text)-import Type       (TyVar)+import Type       (Type, TyVar)+#if __GLASGOW_HASKELL__ >= 711+import Type (eqType)+#endif +newtype EType = EType Type+  deriving Outputable+#if __GLASGOW_HASKELL__ < 711+deriving instance Eq EType+#else+instance Eq EType where+  (EType t1) == (EType t2) = eqType t1 t2+#endif+ data ExtraOp   = I    Integer   | V    TyVar+  | C    EType   | GCD  ExtraOp ExtraOp   | CLog ExtraOp ExtraOp   | Exp  ExtraOp ExtraOp@@ -15,6 +49,7 @@ instance Outputable ExtraOp where   ppr (I i)      = integer i   ppr (V v)      = ppr v+  ppr (C c)      = ppr c   ppr (GCD x y)  = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (CLog x y) = text "CLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (Exp x y)  = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"@@ -35,3 +70,17 @@ mergeExp :: ExtraOp -> ExtraOp -> ExtraOp mergeExp (I i) (I j) = I (i^j) mergeExp x     y     = Exp x y++mergeAdd :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeAdd (I i) (I j) = Just (I (i + j))+mergeAdd _     _     = Nothing++mergeSub :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeSub (I i) (I j)+  | let s = i - j+  , s >= 0 = Just (I s)+mergeSub _     _     = Nothing++mergeMul :: ExtraOp -> ExtraOp -> Maybe ExtraOp+mergeMul (I i) (I j) = Just (I (i * j))+mergeMul _     _     = Nothing
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -1,20 +1,35 @@+{-|+Copyright  :  (C) 2015-2016, University of Twente+License    :  BSD2 (see the file LICENSE)+Maintainer :  Christiaan Baaij <christiaan.baaij@gmail.com>+-}+ {-# LANGUAGE CPP #-}-module GHC.TypeLits.Extra.Solver.Unify where +module GHC.TypeLits.Extra.Solver.Unify+  ( ExtraDefs (..)+  , UnifyResult (..)+  , normaliseNat+  , unifyExtra+  )+where+ -- external-import Data.Function (on)+import Control.Monad.Trans.Class (lift)+import Control.Monad.Trans.Maybe (MaybeT (..))+import Data.Function             (on)  -- GHC API-import Outputable (Outputable (..), (<+>), ($$), text)-import TcPluginM  (TcPluginM, tcPluginTrace)+import Outputable (Outputable (..), ($$), text)+import TcPluginM  (TcPluginM, matchFam, tcPluginTrace) import TcRnMonad  (Ct) import TcTypeNats (typeNatExpTyCon) import Type       (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy) import TyCon      (TyCon) #if __GLASGOW_HASKELL__ >= 711-import TyCoRep       (Type (..), TyLit (..))+import TyCoRep    (Type (..), TyLit (..)) #else-import TypeRep       (Type (..), TyLit (..))+import TypeRep    (Type (..), TyLit (..)) #endif import UniqSet    (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet) @@ -26,7 +41,7 @@   , clogTyCon :: TyCon   } -normaliseNat :: ExtraDefs -> Type -> Maybe ExtraOp+normaliseNat :: ExtraDefs -> Type -> MaybeT TcPluginM ExtraOp normaliseNat defs ty | Just ty1 <- coreView ty = normaliseNat defs ty1 normaliseNat _ (TyVarTy v)          = pure (V v) normaliseNat _ (LitTy (NumTyLit i)) = pure (I i)@@ -35,61 +50,18 @@                                    <*> normaliseNat defs y   | tc == clogTyCon defs = do x' <- normaliseNat defs x                               y' <- normaliseNat defs y-                              mergeCLog x' y'+                              MaybeT (return (mergeCLog x' y'))   | tc == typeNatExpTyCon = mergeExp <$> normaliseNat defs x                                      <*> normaliseNat defs y-  | otherwise = Nothing-normaliseNat _ _ = Nothing -reifyExtraOp :: ExtraDefs -> ExtraOp -> Type-reifyExtraOp _    (I i)     = mkNumLitTy i-reifyExtraOp _    (V v)     = mkTyVarTy v-reifyExtraOp defs (GCD x y) = mkTyConApp (gcdTyCon defs)-                                         [reifyExtraOp defs x-                                         ,reifyExtraOp defs y-                                         ]-reifyExtraOp defs (CLog x y) = mkTyConApp (clogTyCon defs)-                                          [reifyExtraOp defs x-                                          ,reifyExtraOp defs y-                                          ]-reifyExtraOp defs (Exp x y) = mkTyConApp typeNatExpTyCon-                                         [reifyExtraOp defs x-                                         ,reifyExtraOp defs y-                                         ]---type ExtraSubst = [SubstItem]--data SubstItem-  = SubstItem-  { siVar  :: TyVar-  , siOP   :: ExtraOp-  , siNote :: Ct-  }--instance Outputable SubstItem where-  ppr si = ppr (siVar si) <+> text " := " <+> ppr (siOP si)--substsExtra :: ExtraSubst -> ExtraOp -> ExtraOp-substsExtra []     u = u-substsExtra (si:s) u = substsExtra s (substExtra (siVar si) (siOP si) u)--substExtra :: TyVar -> ExtraOp -> ExtraOp -> ExtraOp-substExtra _  _ i@(I _)    = i-substExtra tv e v@(V tv')-  | tv == tv'              = e-  | otherwise              = v-substExtra tv e (GCD x y)  = mergeGCD (substExtra tv e x) (substExtra tv e y)-substExtra tv e (CLog x y) = case mergeCLog x' y' of-    Just k  -> k-    Nothing -> CLog x' y'-  where-    x' = substExtra tv e x-    y' = substExtra tv e y-substExtra tv e (Exp x y) = mergeExp (substExtra tv e x) (substExtra tv e y)+normaliseNat defs (TyConApp tc tys) = do+  tys'   <- mapM (fmap (reifyEOP defs) . normaliseNat defs) tys+  tyM    <- lift (matchFam tc tys')+  case tyM of+    Just (_,ty) -> normaliseNat defs ty+    _ -> return (C (EType (TyConApp tc tys))) -substsSubst :: ExtraSubst -> ExtraSubst -> ExtraSubst-substsSubst s = map (\si -> si {siOP = substsExtra s (siOP si)})+normaliseNat _ t = return (C (EType t))  -- | Result of comparing two 'SOP' terms, returning a potential substitution -- list under which the two terms are equal.@@ -110,15 +82,38 @@  unifyExtra' :: Ct -> ExtraOp -> ExtraOp -> UnifyResult unifyExtra' _ u v-  | eqFV u v  = if u == v then Win else Lose+  | eqFV u v  = if u == v then Win+                          else if containsConstants u || containsConstants v+                                  then Draw+                                  else Lose   | otherwise = Draw  fvOP :: ExtraOp -> UniqSet TyVar fvOP (I _)      = emptyUniqSet fvOP (V v)      = unitUniqSet v+fvOP (C _)      = emptyUniqSet fvOP (GCD x y)  = fvOP x `unionUniqSets` fvOP y fvOP (CLog x y) = fvOP x `unionUniqSets` fvOP y fvOP (Exp x y)  = fvOP x `unionUniqSets` fvOP y  eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP++reifyEOP :: ExtraDefs -> ExtraOp -> Type+reifyEOP _ (I i) = mkNumLitTy i+reifyEOP _ (V v) = mkTyVarTy v+reifyEOP _ (C (EType c)) = c+reifyEOP defs (GCD x y) = mkTyConApp (gcdTyCon defs) [reifyEOP defs x+                                                     ,reifyEOP defs y]+reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Exp x y) = mkTyConApp typeNatExpTyCon [reifyEOP defs x+                                                     ,reifyEOP defs y]++containsConstants :: ExtraOp -> Bool+containsConstants (I _) = False+containsConstants (V _) = False+containsConstants (C _) = True+containsConstants (GCD x y)  = containsConstants x || containsConstants y+containsConstants (CLog x y) = containsConstants x || containsConstants y+containsConstants (Exp x y)  = containsConstants x || containsConstants y
tests/ErrorTests.hs view
@@ -37,6 +37,12 @@ testFail9 :: Proxy (CLog 0 (0^y)) -> Proxy y testFail9 = id +testFail10 :: Integer+testFail10 = natVal (Proxy :: Proxy (CLog 1 4))++testFail11 :: Integer+testFail11 = natVal (Proxy :: Proxy ((CLog 4 4) - (CLog 2 4)))+ testFail1Errors =   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"   ,"Actual type: Proxy 4 -> Proxy 4"@@ -81,3 +87,9 @@   ["Expected type: Proxy (CLog 0 (0 ^ y)) -> Proxy y"   ,"Actual type: Proxy y -> Proxy y"   ]++testFail10Errors =+  ["No instance for (KnownNat (CLog 1 4))"]++testFail11Errors =+  ["No instance for (KnownNat (CLog 4 4 - CLog 2 4))"]
tests/Main.hs view
@@ -1,10 +1,12 @@-{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables #-}+{-# LANGUAGE CPP, DataKinds, TypeOperators, ScopedTypeVariables, KindSignatures,+             TypeFamilies, UndecidableInstances #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver #-}  import Data.List (isInfixOf) import Data.Proxy+import Data.Type.Bool import Control.Exception import Test.Tasty import Test.Tasty.HUnit@@ -29,6 +31,22 @@ test5 :: Proxy (CLog x (x^y)) -> Proxy y test5 = id +test6 :: Integer+test6 = natVal (Proxy :: Proxy (CLog 6 8))++test7 :: Integer+test7 = natVal (Proxy :: Proxy (CLog 3 10))++test8 :: Integer+test8 = natVal (Proxy :: Proxy ((CLog 2 4) * (3 ^ (CLog 2 4))))++type family Max (x :: Nat) (y :: Nat) :: Nat+  where+    Max x y = If (x <=? y) y x++test9 :: Integer+test9 = natVal (Proxy :: Proxy (Max (CLog 2 4) (CLog 4 20)))+ main :: IO () main = defaultMain tests @@ -50,6 +68,18 @@     , testCase "forall x>1 . CLog x (x^y) ~ y" $       show (test4 Proxy) @?=       "Proxy"+    , testCase "KnownNat (CLog 6 8) ~ 2" $+      show test6 @?=+      "2"+    , testCase "KnownNat (CLog 3 10) ~ 3" $+      show test7 @?=+      "3"+    , testCase "KnownNat ((CLog 2 4) * (3 ^ (CLog 2 4)))) ~ 18" $+      show test8 @?=+      "18"+    , testCase "KnownNat (Max (CLog 2 4) (CLog 4 20)) ~ 3" $+      show test9 @?=+      "3"     ]   , testGroup "errors"     [ testCase "GCD 6 8 ~ 4" $ testFail1 `throws` testFail1Errors@@ -61,6 +91,8 @@     , testCase "CLog 4 0 ~ 0" $ testFail7 `throws` testFail7Errors     , testCase "CLog 1 (1^y) ~ y" $ testFail8 `throws` testFail8Errors     , testCase "CLog 0 (0^y) ~ y" $ testFail9 `throws` testFail9Errors+    , testCase "No instance (KnownNat (CLog 1 4))" $ testFail10 `throws` testFail10Errors+    , testCase "No instance (KnownNat (CLog 4 4 - CLog 2 4))" $ testFail11 `throws` testFail11Errors     ]   ]