ghc-typelits-knownnat 0.2.2 → 0.2.3
raw patch · 5 files changed
+56/−6 lines, 5 filesdep ~ghc-typelits-natnormalise
Dependency ranges changed: ghc-typelits-natnormalise
Files
- CHANGELOG.md +4/−0
- LICENSE +2/−1
- ghc-typelits-knownnat.cabal +3/−3
- src/GHC/TypeLits/KnownNat/Solver.hs +35/−2
- tests/Main.hs +12/−0
CHANGELOG.md view
@@ -1,5 +1,9 @@ # Changelog for the [`ghc-typelits-knownnat`](http://hackage.haskell.org/package/ghc-typelits-knownnat) package +## 0.2.3 *January 15th 2017*+* Solve normalised literal constraints, i.e.:+ * `KnownNat (((addrSize + 1) - (addrSize - 1))) ~ KnownNat 2`+ ## 0.2.2 *September 29th 2016* * New features: * Derive smaller constraints from larger constraints when they differ by a single variable, i.e. `KnownNat (a + b), KnownNat b` implies `KnownNat a`.
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-knownnat.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-knownnat-version: 0.2.2+version: 0.2.3 synopsis: Derive KnownNat constraints from other KnownNat constraints description: A type checker plugin for GHC that can derive \"complex\" @KnownNat@@@ -45,7 +45,7 @@ license-file: LICENSE author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com-copyright: Copyright © 2016 University of Twente+copyright: Copyright © 2016, University of Twente, 2017 QBayLogic category: Type System build-type: Simple extra-source-files: README.md@@ -84,7 +84,7 @@ build-depends: base >= 4.9 && <4.10, ghc >= 8.0.1 && <8.2, ghc-tcplugins-extra >= 0.2,- ghc-typelits-natnormalise >= 0.5 && <0.6,+ ghc-typelits-natnormalise >= 0.5.2 && <0.6, singletons >= 2.2 && <3.0, transformers >= 0.5.2.0 && <0.6, template-haskell >= 2.11.0.0 && <2.13
src/GHC/TypeLits/KnownNat/Solver.hs view
@@ -115,7 +115,7 @@ import OccName (mkTcOcc, occNameString) import Plugins (Plugin (..), defaultPlugin) import PrelNames (knownNatClassName)-import TcEvidence (EvTerm (..), mkEvCast, mkTcSymCo, mkTcTransCo)+import TcEvidence (EvTerm (..), EvLit (EvNum), mkEvCast, mkTcSymCo, mkTcTransCo) import TcPluginM (TcPluginM, tcLookupClass, getInstEnvs, zonkCt) import TcRnTypes (Ct, TcPlugin(..), TcPluginResult (..), ctEvidence, ctEvLoc, ctEvPred, ctEvTerm, ctLoc, ctLocSpan, isWanted,@@ -125,7 +125,7 @@ funResultTy, mkNumLitTy, mkStrLitTy, mkTyConApp, piResultTys, splitFunTys, splitTyConApp_maybe, tyConAppTyCon_maybe) import TyCon (tyConName)-import TyCoRep (Type (..))+import TyCoRep (Type (..), TyLit (..)) import Var (DFunId) -- | Classes and instances from "GHC.TypeLits.KnownNat"@@ -327,6 +327,14 @@ (evs,new) <- unzip <$> mapM go_arg df_args return ((,concat new) <$> makeOpDict df cls args' op evs) _ -> return ((,[]) <$> go_other ty)+ go (LitTy (NumTyLit i))+ -- Let GHC solve simple Literal constraints+ | LitTy _ <- op+ = return Nothing+ -- This plugin only solves Literal KnownNat's that needed to be normalised+ -- first+ | otherwise+ = return ((,[]) <$> makeLitDict cls op i) go _ = return Nothing -- Get EvTerm arguments for type-level operations. If they do not exist@@ -474,3 +482,28 @@ -- SNat x ~ KnownNat x = Just . mkEvCast xEv $ (kn_co_dict_x `mkTcTransCo` kn_co_rep_x) `mkTcTransCo` mkTcSymCo (kn_co_dict_z `mkTcTransCo` kn_co_rep_z) | otherwise = Nothing++-- | 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+makeLitDict :: Class -> Type -> Integer -> Maybe EvTerm+makeLitDict clas ty i+ | 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 (EvNum i)) (mkTcSymCo (mkTcTransCo co_dict co_rep))+ = Just ev_tm+ | otherwise+ = Nothing
tests/Main.hs view
@@ -100,6 +100,12 @@ test21 :: forall m n . (KnownNat (m+n), KnownNat m) => Proxy (m+n) -> Proxy m -> Integer test21 _ _ = natVal (Proxy :: Proxy n) +test22 :: forall x y . (KnownNat x, KnownNat y) => Proxy x -> Proxy y -> Integer+test22 _ _ = natVal (Proxy :: Proxy (y*x*y))++test23 :: SNat addrSize -> SNat ((addrSize + 1) - (addrSize - 1))+test23 SNat = SNat+ tests :: TestTree tests = testGroup "ghc-typelits-natnormalise" [ testGroup "Basic functionality"@@ -133,6 +139,9 @@ , testCase "KnownNat (7 - 5) ~ 2" $ show (test9 (Proxy @ 7) (Proxy @ 5)) @?= "2"+ , testCase "KnownNat (y*x*y), x=3 y=4 ~ 48" $+ show (test22 (Proxy @3) (Proxy @4))@?=+ "48" ], testGroup "Implications" [ testCase "KnownNat m => KnownNat (m*m); @ 5" $@@ -179,6 +188,9 @@ , testCase "SNat (a+b) - SNat b = SNat a" $ show (test19 (SNat @ 16) (SNat @10)) @?= "6"+ , testCase "SNat ((addrSize + 1) - (addrSize - 1)) = SNat 2" $+ show (test23 (SNat @ 8)) @?=+ "2" ] ]