ghc-typelits-natnormalise 0.1 → 0.1.1

raw patch · 4 files changed

+45/−11 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +3/−0
• README.md +2/−0
• ghc-typelits-natnormalise.cabal +7/−7
• src/GHC/TypeLits/Normalise.hs +33/−4

@@ -1,4 +1,7 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.1.1 *April 17th 2015*+* Add workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+ ## 0.1 *March 30th 2015* * Initial release

@@ -1,5 +1,7 @@ # ghc-tynat-normalise +[![Build Status](https://secure.travis-ci.org/christiaanb/ghc-typelits-natnormalise.png?branch=master)](http://travis-ci.org/christiaanb/ghc-typelits-natnormalise)+ A type checker plugin for GHC that can solve _equalities_  of types of kind `Nat`, where these types are either: 

@@ -1,17 +1,18 @@ name:                ghc-typelits-natnormalise-version:             0.1+version:             0.1.1 synopsis:            GHC typechecker plugin for types of kind GHC.TypeLits.Nat description:   A type checker plugin for GHC that can solve /equalities/ of types of kind-  'GHC.TypeLits.Nat', where these types are either:+  @Nat@, where these types are either:   .   * Type-level naturals+  .   * Type variables+  .   * Applications of the arithmetic expressions @(+,-,*,^)@.   .-  It solves these equalities by normalising them to /sort-of/-  'GHC.TypeLits.Normalise.SOP.SOP' (Sum-of-Products) form, and then perform a-  simple syntactic equality.+  It solves these equalities by normalising them to /sort-of/ @SOP@+  (Sum-of-Products) form, and then perform a simple syntactic equality.   .   For example, this solver can prove the equality between:   .@@ -25,8 +26,7 @@   4*x*(2 + x)^y + 4*(2 + x)^y + (2 + x)^y*x^2   @   .-  Because the latter is actually the 'GHC.TypeLits.Normalise.SOP.SOP' normal-  form of the former.+  Because the latter is actually the @SOP@ normal form of the former.   .   To use the plugin, add the   .

@@ -1,4 +1,5 @@ {-# LANGUAGE TupleSections #-}+{-# LANGUAGE CPP           #-}  {-# OPTIONS_HADDOCK show-extensions #-} @@ -55,10 +56,15 @@ import Plugins    (Plugin (..), defaultPlugin) import TcEvidence (EvTerm (EvCoercion), TcCoercion (..)) import TcPluginM  (TcPluginM, tcPluginTrace, unsafeTcPluginTcM, zonkCt)+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711+import qualified  Inst+#else import qualified  TcMType-import TcRnTypes  (Ct, CtEvidence (..), CtOrigin, TcPlugin(..),+#endif+import TcRnTypes  (Ct, CtLoc, CtOrigin, TcPlugin(..),                    TcPluginResult(..), ctEvidence, ctEvPred,                    ctLoc, ctLocOrigin, isGiven, isWanted, mkNonCanonical)+import TcSMonad   (runTcS,newGivenEvVar) import TcType     (mkEqPred, typeKind) import Type       (EqRel (NomEq), Kind, PredTree (EqPred), PredType, Type,                    TyVar, classifyPredType, mkTyVarTy)@@ -67,6 +73,12 @@ -- internal import GHC.TypeLits.Normalise.Unify +-- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+import Control.Monad (unless)+import Data.IORef    (readIORef)+import StaticFlags   (initStaticOpts, v_opt_C_ready)+import TcPluginM     (tcPluginIO)+ -- | To use the plugin, add -- -- @@@ -87,6 +99,8 @@ decideEqualSOP :: () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult decideEqualSOP _ _givens _deriveds []      = return (TcPluginOk [] []) decideEqualSOP _ givens  _deriveds wanteds = do+    -- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+    initializeStaticFlags     let unit_wanteds = mapMaybe toNatEquality wanteds     case unit_wanteds of       [] -> return (TcPluginOk [] [])@@ -102,9 +116,7 @@  substItemToCt :: SubstItem TyVar Type Ct -> TcPluginM Ct substItemToCt si-  | isGiven (ctEvidence ct) = return $ mkNonCanonical-                                     $ CtGiven predicate-                                               (evByFiat "units" (ty1, ty2)) loc+  | isGiven (ctEvidence ct) = newSimpleGiven loc predicate (ty1,ty2)   | otherwise               = newSimpleWanted (ctLocOrigin loc) predicate   where     predicate = mkEqPred ty1 ty2@@ -156,8 +168,19 @@  -- Utils newSimpleWanted :: CtOrigin -> PredType -> TcPluginM Ct+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 711+newSimpleWanted orig = fmap mkNonCanonical . unsafeTcPluginTcM . Inst.newWanted orig+#else newSimpleWanted orig = unsafeTcPluginTcM . TcMType.newSimpleWanted orig+#endif +newSimpleGiven :: CtLoc -> PredType -> (Type,Type) -> TcPluginM Ct+newSimpleGiven loc predicate (ty1,ty2)= do+  (ev,_) <- unsafeTcPluginTcM $ runTcS+                              $ newGivenEvVar loc+                                  (predicate, evByFiat "units" (ty1, ty2))+  return (mkNonCanonical ev)+ evMagic :: Ct -> Maybe EvTerm evMagic ct = case classifyPredType $ ctEvPred $ ctEvidence ct of     EqPred NomEq t1 t2 -> Just (evByFiat "tylits_magic" (t1, t2))@@ -166,3 +189,9 @@ evByFiat :: String -> (Type, Type) -> EvTerm evByFiat name (t1,t2) = EvCoercion $ TcCoercion                       $ mkUnivCo (fsLit name) Nominal t1 t2++-- workaround for https://ghc.haskell.org/trac/ghc/ticket/10301+initializeStaticFlags :: TcPluginM ()+initializeStaticFlags = tcPluginIO $ do+  r <- readIORef v_opt_C_ready+  unless r initStaticOpts