packages feed

ghc-typelits-extra 0.2.1 → 0.2.2

raw patch · 9 files changed

+205/−53 lines, 9 files

Files

CHANGELOG.md view
@@ -1,5 +1,12 @@ # Changelog for the [`ghc-typelits-extra`](http://hackage.haskell.org/package/ghc-typelits-extra) package +# 0.2.2 *January 15th 2017*+* Reduce `Min n (n+1)` to `n`+* Reduce `Max n (n+1)` to `n+1`+* Reduce cases like `1 <=? Div 18 6` to `True`+* Add a type-level division that rounds up: `type DivRU n d = Div (n + (d - 1)) d`+* Add a type-level `divMod` : `DivMod :: Nat -> Nat -> '(Nat, Nat)`+ # 0.2.1 *September 29th 2016* * Reduce `Max n n` to `n` * Reduce `Min n n` to `n`
LICENSE view
@@ -1,4 +1,5 @@-Copyright (c) 2015-2016, University of Twente+Copyright (c) 2015-2016, University of Twente,+              2017, QBayLogic 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.2.1+version:             0.2.2 synopsis:            Additional type-level operations on GHC.TypeLits.Nat description:   Additional type-level operations on @GHC.TypeLits.Nat@:@@ -40,7 +40,7 @@ license-file:        LICENSE author:              Christiaan Baaij maintainer:          christiaan.baaij@gmail.com-copyright:           Copyright © 2015-2016 University of Twente+copyright:           Copyright © 2015-2016, University of Twente, 2017, QBayLogic category:            Type System build-type:          Simple extra-source-files:  README.md
src/GHC/TypeLits/Extra.hs view
@@ -62,6 +62,9 @@     -- ** Integral   , Div   , Mod+  , DivMod+    -- *** Variants+  , DivRU     -- ** Logarithm   , FLog   , CLog@@ -79,7 +82,8 @@ import GHC.Base               (isTrue#,(==#),(+#)) import GHC.Integer            (smallInteger) import GHC.Integer.Logarithms (integerLogBase#)-import GHC.TypeLits           (KnownNat, Nat, type (<=), type (<=?), natVal)+import GHC.TypeLits+  (KnownNat, Nat, type (+), type (-), type (<=), type (<=?), natVal) import GHC.TypeLits.KnownNat  (KnownNat2 (..), SNatKn (..), nameToSymbol)  -- | Type-level 'max'@@ -115,6 +119,9 @@ type family Div (x :: Nat) (y :: Nat) :: Nat where   Div x 1 = x +-- | A variant of 'Div' that rounds up instead of down+type DivRU n d = Div (n + (d - 1)) d+ genDefunSymbols [''Div]  instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Div) x y where@@ -133,6 +140,9 @@ instance (KnownNat x, KnownNat y, 1 <= y) => KnownNat2 $(nameToSymbol ''Mod) x y where   type KnownNatF2 $(nameToSymbol ''Mod) = ModSym0   natSing2 = SNatKn (rem (natVal (Proxy @x)) (natVal (Proxy @y)))++-- | Type-level `divMod`+type DivMod n d = '(Div n d, Mod n d)  -- | Type-level equivalent of <https://hackage.haskell.org/package/integer-gmp/docs/GHC-Integer-Logarithms.html#v:integerLogBase-35- integerLogBase#> -- .i.e. the exact integer equivalent to "@'floor' ('logBase' x y)@"
src/GHC/TypeLits/Extra/Solver.hs view
@@ -41,7 +41,9 @@ import TcType      (typeKind) import Type       (EqRel (NomEq), Kind, PredTree (EqPred), classifyPredType,                    eqType)-import TysWiredIn (typeNatKind)+import TyCoRep    (Type (..))+import TysWiredIn (typeNatKind, promotedTrueDataCon, promotedFalseDataCon)+import TcTypeNats (typeNatLeqTyCon)  -- internal import GHC.TypeLits.Extra.Solver.Operations@@ -99,47 +101,67 @@         Simplified evs -> return (TcPluginOk (filter (isWanted . ctEvidence . snd) evs) [])         Impossible eq  -> return (TcPluginContradiction [fromNatEquality eq]) -type NatEquality = (Ct,ExtraOp,ExtraOp)+type NatEquality   = (Ct,ExtraOp,ExtraOp)+type NatInEquality = (Ct,ExtraOp,ExtraOp,Bool)  data SimplifyResult   = Simplified [(EvTerm,Ct)]-  | Impossible NatEquality+  | Impossible (Either NatEquality NatInEquality)  instance Outputable SimplifyResult where   ppr (Simplified evs) = text "Simplified" $$ ppr evs   ppr (Impossible eq)  = text "Impossible" <+> ppr eq -simplifyExtra :: [NatEquality] -> TcPluginM SimplifyResult+simplifyExtra :: [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult simplifyExtra eqs = tcPluginTrace "simplifyExtra" (ppr eqs) >> simples [] eqs   where-    simples :: [Maybe (EvTerm, Ct)] -> [NatEquality] -> TcPluginM SimplifyResult+    simples :: [Maybe (EvTerm, Ct)] -> [Either NatEquality NatInEquality] -> TcPluginM SimplifyResult     simples evs [] = return (Simplified (catMaybes evs))-    simples evs (eq@((ct,u,v)):eqs') = do+    simples evs (eq@(Left (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 (eq@(Right (ct,u,v,b)):eqs') = do+      tcPluginTrace "unifyExtra leq result" (ppr (u,v,b))+      case (u,v) of+        (I i,I j)+          | (i <= j) == b -> simples (((,) <$> evMagic ct <*> pure ct):evs) eqs'+          | otherwise     -> return  (Impossible eq)+        _ -> simples evs eqs' + -- Extract the Nat equality constraints-toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM NatEquality+toNatEquality :: ExtraDefs -> Ct -> MaybeT TcPluginM (Either NatEquality NatInEquality) toNatEquality defs ct = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq t1 t2       | isNatKind (typeKind t1) || isNatKind (typeKind t2)-      -> (ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2+      -> Left <$> ((ct,,) <$> normaliseNat defs t1 <*> normaliseNat defs t2)+      | TyConApp tc [x,y] <- t1+      , tc == typeNatLeqTyCon+      , TyConApp tc' [] <- t2+      -> if tc' == promotedTrueDataCon+            then Right <$> ((ct,,,True) <$> normaliseNat defs x <*> normaliseNat defs y)+            else if tc' == promotedFalseDataCon+                 then Right <$> ((ct,,,False) <$> normaliseNat defs x <*> normaliseNat defs y)+                 else fail "Nothing"     _ -> fail "Nothing"   where     isNatKind :: Kind -> Bool     isNatKind = (`eqType` typeNatKind) -fromNatEquality :: NatEquality -> Ct-fromNatEquality (ct, _, _) = ct+fromNatEquality :: Either NatEquality NatInEquality -> Ct+fromNatEquality (Left (ct, _, _))  = ct+fromNatEquality (Right (ct,_,_,_)) = ct  lookupExtraDefs :: TcPluginM ExtraDefs lookupExtraDefs = do     md <- lookupModule myModule myPackage-    ExtraDefs <$> look md "Div"+    ExtraDefs <$> look md "Max"+              <*> look md "Min"+              <*> look md "Div"               <*> look md "Mod"               <*> look md "FLog"               <*> look md "CLog"
src/GHC/TypeLits/Extra/Solver/Operations.hs view
@@ -8,6 +8,10 @@  module GHC.TypeLits.Extra.Solver.Operations   ( ExtraOp (..)+  , ExtraDefs (..)+  , reifyEOP+  , mergeMax+  , mergeMin   , mergeDiv   , mergeMod   , mergeFLog@@ -23,16 +27,20 @@ import GHC.Base                     (isTrue#,(==#),(+#)) import GHC.Integer                  (smallInteger) import GHC.Integer.Logarithms       (integerLogBase#)-import GHC.TypeLits.Normalise.Unify (CType (..))+import GHC.TypeLits.Normalise.Unify (CType (..), normaliseNat, isNatural)  -- GHC API import Outputable (Outputable (..), (<+>), integer, text)-import Type       (TyVar)+import TcTypeNats (typeNatExpTyCon, typeNatSubTyCon)+import TyCon      (TyCon)+import Type       (Type, TyVar, mkNumLitTy, mkTyConApp, mkTyVarTy)  data ExtraOp   = I    Integer   | V    TyVar   | C    CType+  | Max  ExtraOp ExtraOp+  | Min  ExtraOp ExtraOp   | Div  ExtraOp ExtraOp   | Mod  ExtraOp ExtraOp   | FLog ExtraOp ExtraOp@@ -47,6 +55,8 @@   ppr (I i)      = integer i   ppr (V v)      = ppr v   ppr (C c)      = ppr c+  ppr (Max x y)  = text "Max (" <+> ppr x <+> text "," <+> ppr y <+> text ")"+  ppr (Min x y)  = text "Min (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (Div x y)  = text "Div (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (Mod x y)  = text "Mod (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (FLog x y) = text "FLog (" <+> ppr x <+> text "," <+> ppr y <+> text ")"@@ -55,6 +65,63 @@   ppr (GCD x y)  = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (LCM x y)  = text "GCD (" <+> ppr x <+> text "," <+> ppr y <+> text ")"   ppr (Exp x y)  = text "Exp (" <+> ppr x <+> text "," <+> ppr y <+> text ")"++data ExtraDefs = ExtraDefs+  { maxTyCon  :: TyCon+  , minTyCon  :: TyCon+  , divTyCon  :: TyCon+  , modTyCon  :: TyCon+  , flogTyCon :: TyCon+  , clogTyCon :: TyCon+  , logTyCon  :: TyCon+  , gcdTyCon  :: TyCon+  , lcmTyCon  :: TyCon+  }++reifyEOP :: ExtraDefs -> ExtraOp -> Type+reifyEOP _ (I i) = mkNumLitTy i+reifyEOP _ (V v) = mkTyVarTy v+reifyEOP _ (C (CType c)) = c+reifyEOP defs (Max x y)  = mkTyConApp (maxTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Min x y)  = mkTyConApp (minTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Div x y)  = mkTyConApp (divTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Mod x y)  = mkTyConApp (modTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Log x y)  = mkTyConApp (logTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (GCD x y)  = mkTyConApp (gcdTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (LCM x y)  = mkTyConApp (lcmTyCon defs)  [reifyEOP defs x+                                                       ,reifyEOP defs y]+reifyEOP defs (Exp x y)  = mkTyConApp typeNatExpTyCon  [reifyEOP defs x+                                                       ,reifyEOP defs y]++mergeMax :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp+mergeMax defs x y =+  let x' = reifyEOP defs x+      y' = reifyEOP defs y+      z  = normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])+  in  case isNatural z of+        Just True  -> y+        Just False -> x+        _ -> Max x y++mergeMin :: ExtraDefs -> ExtraOp -> ExtraOp -> ExtraOp+mergeMin defs x y =+  let x' = reifyEOP defs x+      y' = reifyEOP defs y+      z  = normaliseNat (mkTyConApp typeNatSubTyCon [y',x'])+  in  case isNatural z of+        Just True  -> x+        Just False -> y+        _ -> Max x y  mergeDiv :: ExtraOp -> ExtraOp -> Maybe ExtraOp mergeDiv _     (I 0)      = Nothing
src/GHC/TypeLits/Extra/Solver/Unify.hs view
@@ -23,29 +23,22 @@ import TcPluginM  (TcPluginM, matchFam, tcPluginTrace) import TcRnMonad  (Ct) import TcTypeNats (typeNatExpTyCon)-import Type       (TyVar, coreView, mkNumLitTy, mkTyConApp, mkTyVarTy)-import TyCon      (TyCon)+import Type       (TyVar, coreView) import TyCoRep    (Type (..), TyLit (..)) import UniqSet    (UniqSet, emptyUniqSet, unionUniqSets, unitUniqSet)  -- internal import GHC.TypeLits.Extra.Solver.Operations -data ExtraDefs = ExtraDefs-  { divTyCon  :: TyCon-  , modTyCon  :: TyCon-  , flogTyCon :: TyCon-  , clogTyCon :: TyCon-  , logTyCon  :: TyCon-  , gcdTyCon  :: TyCon-  , lcmTyCon  :: TyCon-  }- 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) normaliseNat defs (TyConApp tc [x,y])+  | tc == maxTyCon defs = mergeMax defs <$> normaliseNat defs x+                                        <*> normaliseNat defs y+  | tc == minTyCon defs = mergeMin defs <$> normaliseNat defs x+                                        <*> normaliseNat defs y   | tc == divTyCon defs = do x' <- normaliseNat defs x                              y' <- normaliseNat defs y                              MaybeT (return (mergeDiv x' y'))@@ -106,6 +99,8 @@ fvOP (I _)      = emptyUniqSet fvOP (V v)      = unitUniqSet v fvOP (C _)      = emptyUniqSet+fvOP (Max x y)  = fvOP x `unionUniqSets` fvOP y+fvOP (Min x y)  = fvOP x `unionUniqSets` fvOP y fvOP (Div x y)  = fvOP x `unionUniqSets` fvOP y fvOP (Mod x y)  = fvOP x `unionUniqSets` fvOP y fvOP (FLog x y) = fvOP x `unionUniqSets` fvOP y@@ -118,32 +113,12 @@ eqFV :: ExtraOp -> ExtraOp -> Bool eqFV = (==) `on` fvOP -reifyEOP :: ExtraDefs -> ExtraOp -> Type-reifyEOP _ (I i) = mkNumLitTy i-reifyEOP _ (V v) = mkTyVarTy v-reifyEOP _ (C (CType c)) = c-reifyEOP defs (Div x y)  = mkTyConApp (divTyCon defs)  [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (Mod x y)  = mkTyConApp (modTyCon defs)  [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (CLog x y) = mkTyConApp (clogTyCon defs) [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (FLog x y) = mkTyConApp (flogTyCon defs) [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (Log x y)  = mkTyConApp (logTyCon defs)  [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (GCD x y)  = mkTyConApp (gcdTyCon defs)  [reifyEOP defs x-                                                       ,reifyEOP defs y]-reifyEOP defs (LCM x y)  = mkTyConApp (lcmTyCon 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 (Max x y)  = containsConstants x || containsConstants y+containsConstants (Min x y)  = containsConstants x || containsConstants y containsConstants (Div x y)  = containsConstants x || containsConstants y containsConstants (Mod x y)  = containsConstants x || containsConstants y containsConstants (FLog x y) = containsConstants x || containsConstants y
tests/ErrorTests.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, TypeOperators, TemplateHaskell #-}+{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies, TemplateHaskell #-}  {-# OPTIONS_GHC -fdefer-type-errors #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}@@ -75,6 +75,19 @@ testFail20 :: Integer testFail20 = natVal (Proxy :: Proxy (Log 3 10)) +testFail21 :: Proxy a -> Proxy b -> Proxy (Min a (a*b)) -> Proxy a+testFail21 _ _ = id++testFail22 :: Proxy a -> Proxy b -> Proxy (Max a (a*b)) -> Proxy (a*b)+testFail22 _ _ = id++testFail23' :: ((1 <=? Div l r) ~ False) => Proxy l -> Proxy r -> ()+testFail23' _ _ = ()++testFail23 :: ()+testFail23 = testFail23' (Proxy @18) (Proxy @3)++ testFail1Errors =   ["Expected type: Proxy (GCD 6 8) -> Proxy 4"   ,"Actual type: Proxy 4 -> Proxy 4"@@ -182,3 +195,15 @@           then litE $ stringL "Couldn't match type ‘FLog 3 10’ with ‘CLog 3 10’"           else litE $ stringL "Couldn't match type `FLog 3 10' with `CLog 3 10'"     )]++testFail21Errors =+  ["Expected type: Proxy (Min a (a * b)) -> Proxy a"+  ,"Actual type: Proxy a -> Proxy a"+  ]++testFail22Errors =+  ["Expected type: Proxy (Max a (a * b)) -> Proxy (a * b)"+  ,"Actual type: Proxy (a * b) -> Proxy (a * b)"]++testFail23Errors =+  ["Couldn't match type ‘1 <=? Div 18 3’ with ‘'False’"]
tests/Main.hs view
@@ -1,4 +1,4 @@-{-# LANGUAGE DataKinds, TypeOperators #-}+{-# LANGUAGE DataKinds, TypeOperators, TypeApplications, TypeFamilies #-}  {-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}@@ -106,6 +106,27 @@ test30 :: Proxy n -> Proxy (1 + Max n n) -> Proxy (Min n n + 1) test30 _ = id +test31 :: Proxy (Min n (n + 1)) -> Proxy n+test31 = id++test32 :: Proxy (Min (n + 1) n) -> Proxy n+test32 = id++test33 :: Proxy (Max n (n + 1)) -> Proxy (n+1)+test33 = id++test34 :: Proxy (Max (n + 1) n) -> Proxy (n+1)+test34 = id++test35 :: Proxy n -> Proxy (1 + Max n (1 + n)) -> Proxy (n + 2)+test35 _ = id++test36 :: Proxy n -> Proxy (1 + Min n (1 + n)) -> Proxy (n + 1)+test36 _ = id++test37 :: (1 <= Div l r) => Proxy l -> Proxy r -> ()+test37 _ _ = ()+ main :: IO () main = defaultMain tests @@ -202,6 +223,27 @@     , testCase "forall x . (Min x x + 1) ~ (1 + Max x x)" $       show (test30 Proxy Proxy) @?=       "Proxy"+    , testCase "forall x . Min x (x+1) ~ x" $+      show (test31 Proxy) @?=+      "Proxy"+    , testCase "forall x . Min (x+1) x ~ x" $+      show (test32 Proxy) @?=+      "Proxy"+    , testCase "forall x . Max x (x+1) ~ (x+1)" $+      show (test33 Proxy) @?=+      "Proxy"+    , testCase "forall x . Max (x+1) x ~ (x+1)" $+      show (test34 Proxy) @?=+      "Proxy"+    , testCase "forall x . (1 + Max n (1+n)) ~ (2 + x)" $+      show (test35 Proxy Proxy) @?=+      "Proxy"+    , testCase "forall x . (1 + Min n (1+n)) ~ (1 + x)" $+      show (test36 Proxy Proxy) @?=+      "Proxy"+    , testCase "1 <= Div 18 3" $+      show (test37 (Proxy @18) (Proxy @3)) @?=+      "()"     ]   , testGroup "errors"     [ testCase "GCD 6 8 /~ 4" $ testFail1 `throws` testFail1Errors@@ -224,6 +266,9 @@     , testCase "GCD 6 8 + x /~ x + GCD 9 6" $ testFail18 `throws` testFail18Errors     , testCase "No instance (KnownNat (Log 3 0))" $ testFail19 `throws` testFail19Errors     , testCase "No instance (KnownNat (Log 3 10))" $ testFail20 `throws` testFail20Errors+    , testCase "Min a (a*b) /~ a" $ testFail21 `throws` testFail21Errors+    , testCase "Max a (a*b) /~ (a*b)" $ testFail22 `throws` testFail22Errors+    , testCase "(1 <=? Div 18 6) ~ False" $ testFail23 `throws` testFail23Errors     ]   ]