ghc-typelits-presburger 0.6.1.0 → 0.6.2.0

raw patch · 3 files changed

+28/−3 lines, 3 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +8/−1
• ghc-typelits-presburger.cabal +2/−2
• src/GHC/TypeLits/Presburger/Types.hs +18/−0

@@ -10,6 +10,7 @@ {-# LANGUAGE TypeInType #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE NoStarIsType #-} {-# OPTIONS_GHC -dcore-lint #-} {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} @@ -61,7 +62,7 @@ minusLeq _ _ = Witness  absurdTrueFalse :: ( 'True :~: 'False) -> a-absurdTrueFalse = \case+absurdTrueFalse = \case {}  #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ > 802 hoge :: proxy n -> IsTrue (n + 1 <=? n) -> a@@ -124,4 +125,10 @@ ghc92NLtToGeq :: (n DTO.<? m) ~ 'True   => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False ghc92NLtToGeq _ _ = Refl++minLeq :: n <= m => NProxy n -> NProxy m -> DTO.Min n m :~: n+minLeq _ _ = Refl++maxLeq :: n <= m => NProxy n -> NProxy m -> DTO.Max n m :~: m+maxLeq _ _ = Refl #endif

@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: ebd8f606caa0d36b4fa5c701546d739968ed42ceeba4e62275620799c4e295dc+-- hash: 321c5fb49fa1a616b17e9d7403d059fae66cceb781b4b2a12f547a6be9636e5d  name:           ghc-typelits-presburger-version:        0.6.1.0+version:        0.6.2.0 synopsis:       Presburger Arithmetic Solver for GHC Type-level natural numbers. description:    @ghc-typelits-presburger@ augments GHC type-system with Presburger                 Arithmetic Solver for Type-level natural numbers.

@@ -601,6 +601,12 @@ toPresburgerExp :: Given Translation => Type -> Machine Expr toPresburgerExp ty = case ty of   TyVarTy t -> return $ Var $ toName $ getKey $ getUnique t+  TyConApp tc (lastN 4 -> [cmpNM, l, e, g])+    | tc `elem` ordCond given+    , TyConApp cmp (lastN 2 -> [n, m]) <- cmpNM+    , cmp `elem` natCompare given+    , all ((`elem` [TypeEq n, TypeEq m]) . TypeEq) [l,e,g]+    -> decodeMinMax n m l e g   t@(TyConApp tc ts) ->     parseExpr given toPresburgerExp ty       <|> body tc ts@@ -638,6 +644,18 @@                   ++ [ step con Max                      | con <- natMin given                      ]++decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr+decodeMinMax n m lt eq gt +  | lt `eqType`  n && eq `eqType`  n && gt `eqType` m = +    Min <$> toPresburgerExp n <*> toPresburgerExp m+  | lt `eqType`  n && eq `eqType`  m && gt `eqType` m = +    Min <$> toPresburgerExp n <*> toPresburgerExp m+  | lt `eqType` m && eq `eqType`  m && gt `eqType` n = +    Max <$> toPresburgerExp n <*> toPresburgerExp m+  | lt `eqType` m && eq `eqType`  n && gt `eqType` n = +    Max <$> toPresburgerExp n <*> toPresburgerExp m+  | otherwise = mzero  -- simplTypeCmp :: Type -> Type