ghc-typelits-natnormalise 0.5.7 → 0.5.8
raw patch · 5 files changed
+111/−43 lines, 5 filesdep ~ghcPVP ok
version bump matches the API change (PVP)
Dependency ranges changed: ghc
API changes (from Hackage documentation)
Files
- CHANGELOG.md +3/−0
- LICENSE +2/−1
- ghc-typelits-natnormalise.cabal +4/−3
- src/GHC/TypeLits/Normalise.hs +100/−38
- src/GHC/TypeLits/Normalise/Unify.hs +2/−1
CHANGELOG.md view
@@ -1,5 +1,8 @@ # Changelog for the [`ghc-typelits-natnormalise`](http://hackage.haskell.org/package/ghc-typelits-natnormalise) package +## 0.5.8 *January 4th 2018*+* Add support for GHC 8.4.1-alpha1+ ## 0.5.7 *November 7th 2017* * Solve inequalities such as: `1 <= a + 3`
LICENSE view
@@ -1,4 +1,5 @@-Copyright (c) 2015-2016, University of Twente+Copyright (c) 2015-2016, University of Twente,+ 2017-2018, QBayLogic B.V. All rights reserved. Redistribution and use in source and binary forms, with or without
ghc-typelits-natnormalise.cabal view
@@ -1,5 +1,5 @@ name: ghc-typelits-natnormalise-version: 0.5.7+version: 0.5.8 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@@ -42,12 +42,13 @@ author: Christiaan Baaij maintainer: christiaan.baaij@gmail.com copyright: Copyright © 2015-2016, University of Twente,- 2017 , QBayLogic B.V.+ 2017-2018, QBayLogic B.V. category: Type System build-type: Simple extra-source-files: README.md CHANGELOG.md cabal-version: >=1.10+tested-with: GHC == 8.0.2, GHC == 8.2.2, GHC == 8.4.1 source-repository head type: git@@ -64,7 +65,7 @@ GHC.TypeLits.Normalise.SOP, GHC.TypeLits.Normalise.Unify build-depends: base >=4.9 && <5,- ghc >=8.0.1 && <8.4,+ ghc >=8.0.1 && <8.6, ghc-tcplugins-extra >=0.2, integer-gmp >=1.0 && <1.1 hs-source-dirs: src
src/GHC/TypeLits/Normalise.hs view
@@ -1,5 +1,6 @@ {-|-Copyright : (C) 2015-2016, University of Twente+Copyright : (C) 2015-2016, University of Twente,+ 2017 , QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> @@ -53,8 +54,8 @@ import Control.Arrow (second) import Control.Monad (replicateM) import Data.Either (rights)-import Data.List (intersect)-import Data.Maybe (mapMaybe)+import Data.List (intersect, mapAccumR)+import Data.Maybe (catMaybes) import GHC.TcPluginM.Extra (tracePlugin) -- GHC API@@ -112,11 +113,11 @@ decideEqualSOP 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 wanteds'+ let unit_wanteds = catMaybes . snd $ mapAccumR toNatEquality [] wanteds' case unit_wanteds of [] -> return (TcPluginOk [] []) _ -> do- unit_givens <- mapMaybe toNatEquality <$> mapM zonkCt givens+ unit_givens <- catMaybes . snd . mapAccumR toNatEquality [] <$> mapM zonkCt givens sr <- simplifyNats unit_givens unit_wanteds tcPluginTrace "normalised" (ppr sr) case sr of@@ -147,56 +148,90 @@ -> [Either NatEquality NatInEquality] -- ^ Wanted constraints -> TcPluginM SimplifyResult-simplifyNats eqsG eqsW =- let eqs = eqsG ++ eqsW- in tcPluginTrace "simplifyNats" (ppr eqs) >> simples [] [] [] eqs+simplifyNats givens wanteds =+ let eqs = givens ++ wanteds+ in tcPluginTrace "simplifyNats" (ppr eqs) >>+ simples [] [] [] [] givens wanteds where- simples :: [CoreUnify]- -> [((EvTerm, Ct), [Ct])]- -> [Either NatEquality NatInEquality]- -> [Either NatEquality NatInEquality]- -> TcPluginM SimplifyResult- simples _subst evs _xs [] = return (Simplified evs)- simples subst evs xs (eq@(Left (ct,u,v)):eqs') = do+ simples+ :: [CoreUnify]+ -- Substitutions+ -> [((EvTerm, Ct), [Ct])]+ -- Evidence+ -> [Either NatEquality NatInEquality]+ -- Processed given constraints+ -> [Either NatEquality NatInEquality]+ -- Unsolved wanted constraints+ -> [Either NatEquality NatInEquality]+ -- Given constraints+ -> [Either NatEquality NatInEquality]+ -- Wanted constraints+ -> TcPluginM SimplifyResult+ -- Finished+ simples _subst evs _eqGS _xs _eqG [] = return (Simplified evs)+ -- Process all the givens (create substitutions)+ simples subst evs eqGS xs (eq:eqs') ws+ | Left (ct,u,v) <- eq = do ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)- tcPluginTrace "unifyNats result" (ppr ur) case ur of+ Lose -> return (Impossible eq)+ Draw subst'@(_:_) -> do+ evM <- evMagic ct (map unifyItemToPredType subst')+ case evM of+ Nothing -> simples subst evs eqGS xs eqs' ws+ Just ev ->+ simples (substsSubst subst' subst ++ subst')+ (ev:evs) eqGS xs eqs' ws+ _ -> simples subst evs eqGS xs eqs' ws+ | Right (ct,u) <- eq = do+ let u' = substsSOP subst u+ case isNatural u' of+ Just False -> return (Impossible eq)+ -- Add a processed given with substitution applied+ _ -> simples subst evs (Right (ct,u'):eqGS) xs eqs' ws+ -- Process all the wanteds (actually solve constraints)+ simples subst evs eqGS xs [] (eq:eqs')+ | Left (ct,u,v) <- eq = do+ ur <- unifyNats ct (substsSOP subst u) (substsSOP subst v)+ case ur of Win -> do evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' [] (xs ++ eqs')+ simples subst evs' eqGS [] [] (xs ++ eqs') Lose -> return (Impossible eq)- Draw [] -> simples subst evs (eq:xs) eqs'+ Draw [] -> simples subst evs eqGS (eq:xs) [] eqs' Draw subst' -> do evM <- evMagic ct (map unifyItemToPredType subst') case evM of- Nothing -> simples subst evs xs eqs'+ Nothing -> simples subst evs eqGS xs [] eqs' Just ev -> simples (substsSubst subst' subst ++ subst')- (ev:evs) [] (xs ++ eqs')- simples subst evs xs (eq@(Right (ct,u)):eqs') = do+ (ev:evs) eqGS [] [] (xs ++ eqs')+ | Right (ct,u) <- eq = do let u' = substsSOP subst u- tcPluginTrace "unifyNats(ineq) results" (ppr (ct,u')) case isNatural u' of Just True -> do evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' xs eqs'+ simples subst evs' eqGS xs [] eqs' Just False -> return (Impossible eq) Nothing -> -- This inequality is either a given constraint, or it is a wanted -- constraint, which in normal form is equal to another given -- constraint, hence it can be solved.- if u `elem` (map snd (rights eqsG))+ if u' `elem` (map snd (rights eqGS)) then do evs' <- maybe evs (:evs) <$> evMagic ct []- simples subst evs' xs eqs'- else simples subst evs (eq:xs) eqs'+ simples subst evs' eqGS xs [] eqs'+ else simples subst evs eqGS (eq:xs) [] eqs' -- Extract the Nat equality constraints-toNatEquality :: Ct -> Maybe (Either NatEquality NatInEquality)-toNatEquality ct = case classifyPredType $ ctEvPred $ ctEvidence ct of+toNatEquality+ :: [(CType,Bool)]+ -> Ct+ -> ([(CType,Bool)],Maybe (Either NatEquality NatInEquality))+toNatEquality a ct = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> go t1 t2- _ -> Nothing+ _ -> (a,Nothing) where go (TyConApp tc xs) (TyConApp tc' ys) | tc == tc'@@ -204,21 +239,40 @@ ,typeNatMulTyCon,typeNatExpTyCon]) = case filter (not . uncurry eqType) (zip xs ys) of [(x,y)] | isNatKind (typeKind x) && isNatKind (typeKind y)- -> Just (Left (ct, normaliseNat x, normaliseNat y))- _ -> Nothing+ -> (a,Just (Left (ct, normaliseNat x, normaliseNat y)))+ _ -> (a,Nothing)++ go (TyConApp tc xs) t2 | tc == typeNatLeqTyCon , [x,y] <- xs- = if tc' == promotedTrueDataCon- then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [y,x])))- else if tc' == promotedFalseDataCon- then Just (Right (ct,normaliseNat (mkTyConApp typeNatSubTyCon [x,mkTyConApp typeNatAddTyCon [y,mkNumLitTy 1]])))- else Nothing+ = let trueLEq = (a,Just (Right (ct,normaliseNat+ (mkTyConApp typeNatSubTyCon [y,x]))))+ falseLEq = (a,Just (Right (ct,normaliseNat+ (mkTyConApp typeNatSubTyCon+ [x,mkTyConApp typeNatAddTyCon+ [y,mkNumLitTy 1]]))))+ in case t2 of+ TyConApp tc' _+ | tc' == promotedTrueDataCon+ -> trueLEq+ | tc' == promotedFalseDataCon+ -> falseLEq+ _ | Just b <- lookup (CType t2) a+ -> if b then trueLEq else falseLEq+ | otherwise+ -> (a,Nothing) + go x (TyConApp tc _)+ | tc == promotedTrueDataCon+ = ((CType x,True):a,Nothing)+ | tc == promotedFalseDataCon+ = ((CType x,False):a,Nothing)+ go x y | isNatKind (typeKind x) && isNatKind (typeKind y)- = Just (Left (ct,normaliseNat x,normaliseNat y))+ = (a,Just (Left (ct,normaliseNat x,normaliseNat y))) | otherwise- = Nothing+ = (a,Nothing) isNatKind :: Kind -> Bool isNatKind = (`eqType` typeNatKind)@@ -237,10 +291,18 @@ evMagic :: Ct -> [PredType] -> TcPluginM (Maybe ((EvTerm, Ct), [Ct])) evMagic ct preds = case classifyPredType $ ctEvPred $ ctEvidence ct of EqPred NomEq t1 t2 -> do+#if MIN_VERSION_ghc(8,5,0)+ holes <- mapM (newCoercionHole . uncurry mkPrimEqPred . getEqPredTys) preds+#else holes <- replicateM (length preds) newCoercionHole+#endif let newWanted = zipWith (unifyItemToCt (ctLoc ct)) preds holes ctEv = mkUnivCo (PluginProv "ghc-typelits-natnormalise") Nominal t1 t2+#if MIN_VERSION_ghc(8,5,0)+ holeEvs = map mkHoleCo holes+#else holeEvs = zipWith (\h p -> uncurry (mkHoleCo h Nominal) (getEqPredTys p)) holes preds+#endif natReflCo = mkNomReflCo typeNatKind natCoBndr = (,natReflCo) <$> (newFlexiTyVar typeNatKind) forallEv <- mkForAllCos <$> (replicateM (length preds) natCoBndr) <*> pure ctEv
src/GHC/TypeLits/Normalise/Unify.hs view
@@ -1,5 +1,6 @@ {-|-Copyright : (C) 2015-2016, University of Twente+Copyright : (C) 2015-2016, University of Twente,+ 2017 , QBayLogic B.V. License : BSD2 (see the file LICENSE) Maintainer : Christiaan Baaij <christiaan.baaij@gmail.com> -}