ghc-typelits-presburger 0.1.0.0 → 0.1.1.0
raw patch · 4 files changed
+90/−31 lines, 4 filesPVP ok
version bump matches the API change (PVP)
API changes (from Hackage documentation)
Files
- examples/simple-arith.hs +39/−15
- ghc-typelits-presburger.cabal +8/−3
- src/GHC/Compat.hs +1/−3
- src/GHC/TypeLits/Presburger.hs +42/−10
examples/simple-arith.hs view
@@ -2,34 +2,58 @@ {-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} module Main where import Data.Type.Equality-import GHC.TypeLits (type (<=), type (*), type (+), type (<=?))+import GHC.TypeLits (Nat, type (<=), type (*), type (+), type (<=?), CmpNat) import Proof.Propositional (Empty(..)) import Proof.Propositional (IsTrue(Witness))+import Data.Singletons.Prelude type n <=! m = IsTrue (n <=? m) infix 4 <=! -natLeqZero :: (n <= 0) => proxy n -> n :~: 0-natLeqZero _ = Refl+-- natLeqZero :: (n <= 0) => proxy n -> n :~: 0+-- natLeqZero _ = Refl +-- (%:<=?) :: Sing n -> Sing m -> Sing (n <=? m)+-- n %:<=? m = case sCompare n m of+-- SLT -> STrue+-- SEQ -> STrue+-- SGT -> SFalse -hoge :: ((n + 1 <=? n) ~ 'False) => ()-hoge = ()+-- natLeqZero :: IsTrue (n <=? 0) -> Sing n -> n :~: 0+-- natLeqZero Witness Zero = Refl -fuga :: ((n + 1 <=? 0) ~ 'False) => ()-fuga = () -bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => ()-bar = ()+-- hoge :: ((n + 1 <=? n) ~ 'False) => ()+-- hoge = () -trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)-trans _ _ Witness = Witness+-- fuga :: ((n + 1 <=? 0) ~ 'False) => ()+-- fuga = () -eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))-eqv _ _ = Refl+-- bar :: ((2 * (n + 1)) ~ ((2 * n) + 2)) => proxy n -> ()+-- bar _ = () -predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)-predSucc _ = Witness+-- trans :: proxy n -> proxy m -> n <=! m -> (n + 1) <=! (m + 1)+-- trans _ _ Witness = Witness +-- eqv :: proxy n -> proxy m -> (n <=? m) :~: ((n + 1) <=? (m + 1))+-- eqv _ _ = Refl++-- leqSucc :: proxy n -> proxy m -> IsTrue ((n + 1) :<= m) -> CmpNat n m :~: 'LT+-- leqSucc _ _ Witness = Refl+++-- predSucc :: forall proxy n. Empty (n <=! 0) => proxy n -> IsTrue (n + 1 <=? 2 * n)+-- predSucc _ = Witness+ main :: IO () main = putStrLn "finished"++-- succLEqLTSucc :: Sing m -> Compare 0 (m + 1) :~: 'LT+-- succLEqLTSucc _ = Refl+++-- succCompare :: Sing (n :: Nat) -> Sing m -> CmpNat n m :~: CmpNat (n + 1) (m + 1)+-- succCompare _ _ = Refl++eqToRefl :: Sing (n :: Nat) -> Sing (m :: Nat) -> CmpNat n m :~: 'EQ -> n :~: m+eqToRefl _n _m Refl = Refl
ghc-typelits-presburger.cabal view
@@ -1,7 +1,12 @@ name: ghc-typelits-presburger-version: 0.1.0.0-synopsis: Initial project template from stack-description: Please see README.md+version: 0.1.1.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.+ You can use by adding this package to @build-depends@ and add the following pragma to the head of .hs files:+ .+ > OPTIONS_GHC -fplugin GHC.TypeLits.Presburger+ homepage: https://github.com/konn/ghc-typelits-presburger#readme license: BSD3 license-file: LICENSE
src/GHC/Compat.hs view
@@ -17,9 +17,7 @@ tcPluginTrace) import TcRnMonad as GHC.Compat (Ct, TcPluginResult (..), isWanted) import TcRnTypes as GHC.Compat (TcPlugin (..), ctEvPred, ctEvidence)-import TcTypeNats as GHC.Compat (typeNatAddTyCon, typeNatExpTyCon)-import TcTypeNats as GHC.Compat (typeNatLeqTyCon, typeNatMulTyCon)-import TcTypeNats as GHC.Compat (typeNatSubTyCon)+import TcTypeNats as GHC.Compat #if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800 import GhcPlugins (InScopeSet, Outputable, emptyUFM) import qualified PrelNames as Old
src/GHC/TypeLits/Presburger.hs view
@@ -15,6 +15,8 @@ import Data.Reflection (give) import TcPluginM (tcLookupClass) import TcPluginM (lookupOrig)+import TysWiredIn (promotedEQDataCon, promotedGTDataCon,+ promotedLTDataCon) assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos)@@ -103,7 +105,7 @@ let subst = foldr unionTvSubst emptyTvSubst $ map genSubst (gs ++ ds) tcPluginTrace "Current subst" (ppr subst) tcPluginTrace "wanteds" $ ppr $ map (deconsPred) ws- tcPluginTrace "givens" $ ppr $ map (deconsPred) gs+ tcPluginTrace "givens" $ ppr $ map (substTy subst . deconsPred) gs tcPluginTrace "deriveds" $ ppr $ map deconsPred ds let wants = mapMaybe (\ct -> (,) ct <$> toPresburgerPred subst (substTy subst $ deconsPred ct)) $ filter (isWanted . ctEvidence) ws@@ -159,15 +161,15 @@ | con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 toPresburgerPred subst ty | isEqPred ty = toPresburgerPredTree subst $ classifyPredType ty- | Just (con, [l, r]) <- splitTyConApp_maybe ty+ | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r , con == eqTyCon = toPresburgerPredTree subst $ EqPred NomEq l r- | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty+ | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r , con == eqWitnessTyCon = toPresburgerPredTree subst $ EqPred NomEq l r- | Just (con, [l]) <- splitTyConApp_maybe ty+ | Just (con, [l]) <- splitTyConApp_maybe ty -- Empty l => ... , con == emptyTyCon = Not <$> toPresburgerPred subst l- | Just (con, [l]) <- splitTyConApp_maybe ty+ | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => , con == isTrueTyCon = toPresburgerPred subst l- | ts <- decompFunTy ty+ | ts <- decompFunTy ty -- v -> v' -> ... -> Void , (args , [vd]) <- splitAt (length ts - 1) ts , isVoidTy vd = do preds <- mapM (toPresburgerPred subst) args@@ -180,15 +182,43 @@ Not <$> toPresburgerPredTree subst (EqPred NomEq p (mkTyConTy promotedTrueDataCon)) toPresburgerPredTree subst (EqPred NomEq p b) -- (n :<=? m) ~ 'True | Just promotedTrueDataCon == tyConAppTyCon_maybe (substTy subst b)- , TyConApp con [t1, t2] <- substTy subst p+ , Just (con, [t1, t2]) <- splitTyConApp_maybe (substTy subst p) , con == typeNatLeqTyCon = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 toPresburgerPredTree subst (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) | typeKind p `eqType` mkTyConTy promotedBoolTyCon = (<=>) <$> toPresburgerPred subst p <*> toPresburgerPred subst q-toPresburgerPredTree subst (EqPred NomEq t1 t2) -- (n :: Nat) ~ (m :: Nat)- | typeKind t1 `eqType` typeNatKind = (:==) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2-toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) ~ (m :: Nat)+toPresburgerPredTree subst (EqPred NomEq n m) -- (n :: Nat) ~ (m :: Nat)+ | typeKind n `eqType` typeNatKind =+ (:==) <$> toPresburgerExp subst n+ <*> toPresburgerExp subst m+toPresburgerPredTree subst (EqPred _ t1 t2) -- CmpNat a b ~ CmpNat c d+ | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)+ , Just (con', [c, d]) <- splitTyConApp_maybe (substTy subst t2)+ , con == typeNatCmpTyCon, con' == typeNatCmpTyCon+ = (<=>) <$> ((:<) <$> toPresburgerExp subst a <*> toPresburgerExp subst b)+ <*> ((:<) <$> toPresburgerExp subst c <*> toPresburgerExp subst d)+toPresburgerPredTree subst (EqPred NomEq t1 t2) -- CmpNat a b ~ x+ | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t1)+ , con == typeNatCmpTyCon+ , Just cmp <- tyConAppTyCon_maybe (substTy subst t2) =+ let dic = [(promotedLTDataCon, (:<))+ ,(promotedEQDataCon, (:==))+ ,(promotedGTDataCon, (:>))+ ]+ in lookup cmp dic <*> toPresburgerExp subst a+ <*> toPresburgerExp subst b+toPresburgerPredTree subst (EqPred NomEq t1 t2) -- x ~ CmpNat a b+ | Just (con, [a, b]) <- splitTyConApp_maybe (substTy subst t2)+ , con == typeNatCmpTyCon+ , Just cmp <- tyConAppTyCon_maybe (substTy subst t1) =+ let dic = [(promotedLTDataCon, (:<))+ ,(promotedEQDataCon, (:==))+ ,(promotedGTDataCon, (:>))+ ]+ in lookup cmp dic <*> toPresburgerExp subst a+ <*> toPresburgerExp subst b+toPresburgerPredTree subst (ClassPred con [t1, t2]) -- (n :: Nat) <= (m :: Nat) | typeNatLeqTyCon == classTyCon con , typeKind t1 `eqType` typeNatKind = (:<=) <$> toPresburgerExp subst t1 <*> toPresburgerExp subst t2 toPresburgerPredTree _ _ = Nothing@@ -212,6 +242,8 @@ | (con, op) <- [(typeNatAddTyCon, (:+)), (typeNatSubTyCon, (:-))]] LitTy (NumTyLit n) -> Just (K n) _ -> Nothing++-- simplTypeCmp :: Type -> Type simpleExp :: Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)