diff --git a/examples/simple-arith-core.hs b/examples/simple-arith-core.hs --- a/examples/simple-arith-core.hs +++ b/examples/simple-arith-core.hs @@ -23,7 +23,13 @@ import Data.Type.Equality import GHC.TypeLits import Proof.Propositional (Empty (..), IsTrue (Witness), withEmpty) +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 +import qualified Data.Type.Ord as DTO +#endif +main :: IO () +main = putStrLn "finished" + type n <=! m = IsTrue (n <=? m) infix 4 <=! @@ -86,9 +92,6 @@ eqToRefl :: pxy n -> pxy m -> CmpNat n m :~: 'EQ -> n :~: m eqToRefl _n _m Refl = Refl -main :: IO () -main = putStrLn "finished" - rangeEql :: ((n == 0) ~ 'False) => pxy n -> @@ -100,3 +103,25 @@ pxy n -> (n <=? 2) :~: 'True rangeEqlLeq _ = Refl + +-- GHC >= 9.2 only Tests +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 902 +data NProxy (n :: Nat) = NProxy + +ghc92NLeqToGt :: (n DTO.<=? m) ~ 'False + => NProxy n -> NProxy m -> (n DTO.>? m) :~: 'True +ghc92NLeqToGt _ _ = Refl + +ghc92GtToGeq :: (n DTO.> m) + => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'True +ghc92GtToGeq _ _ = Refl + +ghc92GeqEquivNLt :: NProxy n -> NProxy m -> (n DTO.>=? m) :~: ((n DTO. NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False +ghc92NLtToGeq _ _ = Refl +#endif diff --git a/ghc-typelits-presburger.cabal b/ghc-typelits-presburger.cabal --- a/ghc-typelits-presburger.cabal +++ b/ghc-typelits-presburger.cabal @@ -1,13 +1,13 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0. +-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack -- --- hash: f5d043e0588502295fbbf222a24c404b5415e14c21786d9e5e7bacc06e2088af +-- hash: ebd8f606caa0d36b4fa5c701546d739968ed42ceeba4e62275620799c4e295dc name: ghc-typelits-presburger -version: 0.6.0.0 +version: 0.6.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. @@ -29,7 +29,8 @@ copyright: 2015 (c) Hiromi ISHII license: BSD3 license-file: LICENSE -tested-with: GHC==8.6.5 GHC==8.8.4 GHC==8.10.4 GHC==9.0.1 +tested-with: + GHC==8.6.5 GHC==8.8.4 GHC==8.10.7 GHC==9.0.1 GHC==9.2.1 build-type: Simple source-repository head @@ -55,7 +56,7 @@ build-depends: base >=4.7 && <5 , containers - , ghc <9.1 + , ghc <9.3 , ghc-tcplugins-extra >=0.2 && <0.5 , mtl , pretty diff --git a/src/GHC/TypeLits/Presburger/Compat.hs b/src/GHC/TypeLits/Presburger/Compat.hs --- a/src/GHC/TypeLits/Presburger/Compat.hs +++ b/src/GHC/TypeLits/Presburger/Compat.hs @@ -1,4 +1,5 @@ {-# LANGUAGE CPP, FlexibleInstances, PatternGuards, PatternSynonyms #-} +{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE TypeSynonymInstances, ViewPatterns #-} {-# LANGUAGE PatternSynonyms #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -34,13 +35,29 @@ import GHC.Unit.Types (Module, UnitId, toUnitId) import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (mkModule) import GHC.Data.FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Driver.Env.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) +#else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) import GHC.Driver.Session (unitState) -import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit) +#endif +import GHC.Plugins (InScopeSet, Outputable, emptyUFM, moduleUnit, Unit, Name) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Hs as GHC.TypeLits.Presburger.Compat (HsParsedModule(..)) +import GHC.Types.TyThing as GHC.TypeLits.Presburger.Compat (lookupTyCon) +import GHC.Builtin.Types (naturalTy) +#else +import GHC.Plugins as GHC.TypeLits.Presburger.Compat + ( HsParsedModule(..), + lookupTyCon, + typeNatKind + ) +#endif + import GHC.Plugins as GHC.TypeLits.Presburger.Compat ( PackageName (..),isStrLitTy, isNumLitTy, nilDataCon, consDataCon, - Hsc, HsParsedModule(..), + Hsc, Plugin (..), TCvSubst (..), TvSubstEnv, @@ -48,7 +65,6 @@ defaultPlugin, emptyTCvSubst, eqType, - lookupTyCon, mkTcOcc, mkTyConTy, mkTyVarTy, @@ -61,12 +77,19 @@ text, tyConAppTyCon_maybe, typeKind, - typeNatKind, unionTCvSubst, ) import GHC.Tc.Plugin (lookupOrig) import GHC.Core.InstEnv as GHC.TypeLits.Presburger.Compat (classInstances) +#if MIN_VERSION_ghc(9,2,0) +import GHC.Tc.Plugin (unsafeTcPluginTcM) +import GHC.Utils.Logger (getLogger) +import Data.Functor ((<&>)) +import GHC.Unit.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) +#else import GHC.Driver.Types as GHC.TypeLits.Presburger.Compat (IsBootInterface(..)) +#endif + import GHC.Tc.Plugin as GHC.TypeLits.Presburger.Compat ( TcPluginM, getInstEnvs, @@ -84,6 +107,7 @@ import GHC.Tc.Types as GHC.TypeLits.Presburger.Compat (TcPlugin (..), TcPluginResult (..)) import GHC.Tc.Types.Constraint as GHC.TypeLits.Presburger.Compat ( Ct, + CtEvidence, ctEvPred, ctEvidence, isWanted, @@ -103,7 +127,7 @@ #else import Class as GHC.TypeLits.Presburger.Compat (classTyCon, className) import FastString as GHC.TypeLits.Presburger.Compat (FastString, fsLit, unpackFS) -import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages) +import GhcPlugins (InScopeSet, Outputable, emptyUFM, InstalledUnitId(..), initPackages, Name) import GhcPlugins as GHC.TypeLits.Presburger.Compat (PackageName (..), fsToUnitId, lookupPackageName, lookupTyCon, mkTcOcc, mkTyConTy, ppr, promotedFalseDataCon, promotedTrueDataCon, text, tyConAppTyCon_maybe, typeKind, typeNatKind) import HscTypes as GHC.TypeLits.Presburger.Compat (HscEnv (hsc_dflags)) import Module as GHC.TypeLits.Presburger.Compat (ModuleName, mkModuleName, mkModule) @@ -173,7 +197,7 @@ import qualified Predicate as Old (classifyPredType) import Predicate as GHC.TypeLits.Presburger.Compat (mkPrimEqPredRole) import Constraint as GHC.TypeLits.Presburger.Compat - (Ct, ctEvidence, ctEvPred, isWanted) + (Ct, ctEvidence, CtEvidence, ctEvPred, isWanted) #else import GHC (NoExt(..)) import GhcPlugins as GHC.TypeLits.Presburger.Compat (EqRel (..), PredTree (..)) @@ -316,7 +340,7 @@ mkSubstitution :: [Ct] -> Substitution mkSubstitution = #if MIN_VERSION_ghc(8,4,1) - fst . unzip . Extra.mkSubst' + map fst . Extra.mkSubst' #else foldr (unionTvSubst . genSubst) emptyTvSubst #endif @@ -344,9 +368,18 @@ type RawUnitId = FastString preloadedUnitsM :: TcPluginM [FastString] -#if MIN_VERSION_ghc(9,0,0) +#if MIN_VERSION_ghc(9,2,0) preloadedUnitsM = do + logger <- unsafeTcPluginTcM getLogger dflags <- hsc_dflags <$> getTopEnv + packs <- tcPluginIO $ initUnits logger dflags Nothing <&> + \(_, us, _, _ ) -> preloadUnits us + let packNames = map (\(UnitId p) -> p) packs + tcPluginTrace "pres: packs" $ ppr packNames + pure packNames +#elif MIN_VERSION_ghc(9,0,0) +preloadedUnitsM = do + dflags <- hsc_dflags <$> getTopEnv packs <- tcPluginIO $ preloadUnits . unitState <$> initUnits dflags let packNames = map (\(UnitId p) -> p) packs tcPluginTrace "pres: packs" $ ppr packNames @@ -397,5 +430,110 @@ pattern IsBoot = True {-# COMPLETE NotBoot, IsBoot #-} + #endif +#if MIN_VERSION_ghc(9,2,0) +typeNatKind :: TcType +typeNatKind = naturalTy +#endif +mtypeNatLeqTyCon :: Maybe TyCon +#if MIN_VERSION_ghc(9,2,0) +mtypeNatLeqTyCon = Nothing +#else +mtypeNatLeqTyCon = Just typeNatLeqTyCon +#endif + +lookupTyNatPredLeq :: TcPluginM Name +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatPredLeq = do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + lookupOrig tyOrd (mkTcOcc "<=") +#else +lookupTyNatPredLeq = + lookupOrig gHC_TYPENATS (mkTcOcc "<=") +#endif + +lookupTyNatBoolLeq :: TcPluginM TyCon +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatBoolLeq = do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "<=?") +#else +lookupTyNatBoolLeq = + pure typeNatLeqTyCon +#endif + +lookupTyNatPredLt :: TcPluginM (Maybe TyCon) +-- Note: base library shipepd with 9.2.1 has a wrong implementation; +-- hence we MUST NOT desugar it with <= 9.2.1 +#if MIN_VERSION_ghc(9,2,2) +lookupTyNatPredLt = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "<") +#else +lookupTyNatPredLt = pure Nothing +#endif + +lookupTyNatBoolLt :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatBoolLt = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc " do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc ">") +#else +lookupTyNatPredGt = pure Nothing +#endif + +lookupTyNatBoolGt :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatBoolGt = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc ">?") +#else +lookupTyNatBoolGt = pure Nothing +#endif + +lookupTyNatPredGeq :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatPredGeq = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc ">=") +#else +lookupTyNatPredGeq = pure Nothing +#endif + +lookupTyNatBoolGeq :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +lookupTyNatBoolGeq = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc ">=?") +#else +lookupTyNatBoolGeq = pure Nothing +#endif + +mOrdCondTyCon :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +mOrdCondTyCon = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "OrdCond") +#else +mOrdCondTyCon = pure Nothing +#endif + +lookupTyGenericCompare :: TcPluginM (Maybe TyCon) +#if MIN_VERSION_ghc(9,2,0) +lookupTyGenericCompare = Just <$> do + tyOrd <- lookupModule (mkModuleName "Data.Type.Ord") "base" + tcLookupTyCon =<< lookupOrig tyOrd (mkTcOcc "Compare") +#else +lookupTyGenericCompare = pure Nothing +#endif diff --git a/src/GHC/TypeLits/Presburger/Types.hs b/src/GHC/TypeLits/Presburger/Types.hs --- a/src/GHC/TypeLits/Presburger/Types.hs +++ b/src/GHC/TypeLits/Presburger/Types.hs @@ -11,7 +11,10 @@ {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE ViewPatterns #-} - +{-# LANGUAGE RecordWildCards #-} +{-# LANGUAGE DerivingStrategies #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE DerivingVia #-} -- | Since 0.3.0.0 module GHC.TypeLits.Presburger.Types ( pluginWith, @@ -25,7 +28,7 @@ import Control.Applicative ((<|>)) import Control.Arrow (second) -import Control.Monad (forM, forM_, guard, mzero, unless) +import Control.Monad (forM_, guard, mzero, unless) import Control.Monad.State.Class import Control.Monad.Trans.Class import Control.Monad.Trans.Maybe (MaybeT (..)) @@ -48,6 +51,7 @@ import Data.Reflection (Given, give, given) import qualified Data.Set as Set import GHC.TypeLits.Presburger.Compat +import qualified Data.Foldable as F assert' :: Prop -> PropSet -> PropSet assert' p ps = foldr assert ps (p : varPos) @@ -132,7 +136,7 @@ loop (Not q) = Not <$> loop q loop (l :<= r) = (:<=) <$> loopExp l <*> loopExp r loop (l :< r) = (:<) <$> loopExp l <*> loopExp r - loop (l :>= r) = (:<=) <$> loopExp l <*> loopExp r + loop (l :>= r) = (:>=) <$> loopExp l <*> loopExp r loop (l :> r) = (:>) <$> loopExp l <*> loopExp r loop (l :== r) = (:==) <$> loopExp l <*> loopExp r loop (l :/= r) = (:/=) <$> loopExp l <*> loopExp r @@ -156,10 +160,13 @@ loopExp (Min l r) = Min <$> loopExp l <*> loopExp r loopExp (Max l r) = Max <$> loopExp l <*> loopExp r loopExp (If p l r) = If <$> loop p <*> loopExp l <*> loopExp r + loopExp (Mod l n) = Mod <$> loopExp l <*> pure n + loopExp (Div l n) = Div <$> loopExp l <*> pure n loopExp e@(K _) = return e data Translation = Translation { isEmpty :: [TyCon] + , ordCond :: [TyCon] , isTrue :: [TyCon] , trueData :: [TyCon] , falseData :: [TyCon] @@ -222,6 +229,7 @@ , parseExpr = \toE -> (<|>) <$> parseExpr l toE <*> parseExpr r toE , natMin = natMin l <> natMin r , natMax = natMax l <> natMax r + , ordCond = ordCond l <> ordCond r } instance Monoid Translation where @@ -256,6 +264,7 @@ , parseExpr = const $ const mzero , natMin = mempty , natMax = mempty + , ordCond = mempty } decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult @@ -348,28 +357,46 @@ eqWitCon_ <- getEqWitnessTyCon vmd <- lookupModule (mkModuleName "Data.Void") (fsLit "base") voidTyCon <- tcLookupTyCon =<< lookupOrig vmd (mkTcOcc "Void") - nLeq <- tcLookupTyCon =<< lookupOrig gHC_TYPENATS (mkTcOcc "<=") - return - mempty - { isEmpty = isEmpties - , tyEq = [eqTyCon_] - , tyEqWitness = [eqWitCon_] - , tyEqBool = [eqBoolTyCon] - , isTrue = isTrues - , voids = [voidTyCon] - , natMinus = [typeNatSubTyCon] - , natPlus = [typeNatAddTyCon] - , natTimes = [typeNatMulTyCon] - , natExp = [typeNatExpTyCon] - , falseData = [promotedFalseDataCon] - , trueData = [promotedTrueDataCon] - , natLeqBool = [typeNatLeqTyCon] - , natLeq = [nLeq] - , natCompare = [typeNatCmpTyCon] - , orderingEQ = [promotedEQDataCon] - , orderingLT = [promotedLTDataCon] - , orderingGT = [promotedGTDataCon] - } + nLeq <- tcLookupTyCon =<< lookupTyNatPredLeq + tyLeqB <- lookupTyNatBoolLeq + mTyLtP <- lookupTyNatPredLt + mTyLtB <- lookupTyNatBoolLt + mTyGeqP <- lookupTyNatPredGeq + mTyGeqB <- lookupTyNatBoolGeq + mTyGtP <- lookupTyNatPredGt + mTyGtB <- lookupTyNatBoolGt + mOrdCond <- mOrdCondTyCon + mtyGenericCompare <- lookupTyGenericCompare + let trans = + mempty + { isEmpty = isEmpties + , tyEq = [eqTyCon_] + , ordCond = F.toList mOrdCond + , tyEqWitness = [eqWitCon_] + , tyEqBool = [eqBoolTyCon] + , isTrue = isTrues + , voids = [voidTyCon] + , natMinus = [typeNatSubTyCon] + , natPlus = [typeNatAddTyCon] + , natTimes = [typeNatMulTyCon] + , natExp = [typeNatExpTyCon] + , falseData = [promotedFalseDataCon] + , trueData = [promotedTrueDataCon] + , natLeqBool = [tyLeqB] + , natLeq = [nLeq] + , natGeqBool = F.toList mTyGeqB + , natGeq = F.toList mTyGeqP + , natGtBool = F.toList mTyGtB + , natGt = F.toList mTyGtP + , natLtBool = F.toList mTyLtB + , natLt = F.toList mTyLtP + , natCompare = typeNatCmpTyCon : F.toList mtyGenericCompare + , orderingEQ = [promotedEQDataCon] + , orderingLT = [promotedLTDataCon] + , orderingGT = [promotedGTDataCon] + } + tcPluginTrace "Final translation: " (ppr mTyGeqB) + pure trans (<=>) :: Prop -> Prop -> Prop p <=> q = (p :&& q) :|| (Not p :&& Not q) @@ -390,7 +417,7 @@ deconsPred = ctEvPred . ctEvidence toPresburgerPred :: Given Translation => Type -> Machine Prop -toPresburgerPred (TyConApp con [t1, t2]) +toPresburgerPred (TyConApp con (lastN 2 -> [t1, t2])) | con `elem` (natLeq given ++ natLeqBool given) = (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 toPresburgerPred ty @@ -403,7 +430,7 @@ | cls@(EqPred NomEq _ _) <- classifyPredType ty = toPresburgerPredTree cls | isEqPred ty = toPresburgerPredTree $ classifyPredType ty - | Just (con, [l, r]) <- splitTyConApp_maybe ty -- l ~ r + | Just (con, [l, r]) <- splitTyConAppLastBin ty -- l ~ r , con `elem` (tyEq given ++ tyEqBool given) = toPresburgerPredTree $ EqPred NomEq l r | Just (con, [_k, l, r]) <- splitTyConApp_maybe ty -- l (:~: {k}) r @@ -415,14 +442,15 @@ | Just (con, [l]) <- splitTyConApp_maybe ty -- IsTrue l => , con `elem` isTrue given = toPresburgerPred l - | Just (con, ts) <- splitTyConApp_maybe ty - , let n = length ts - , n >= 2 - , [t1, t2] <- drop (n - 2) ts + | Just (con, [t1, t2]) <- splitTyConAppLastBin ty , typeKind t1 `eqType` typeNatKind - , typeKind t2 `eqType` typeNatKind = - let p = lookup con binPropDic - in MaybeT (return p) <*> toPresburgerExp t1 <*> toPresburgerExp t2 + , typeKind t2 `eqType` typeNatKind + , Just p <- lookup con binPropDic = + p <$> toPresburgerExp t1 <*> toPresburgerExp t2 + | Just DataCond{..} <- parseOrdCond ty = do -- OrdCond + fromCondCases condCases + <$> toPresburgerExp lhs + <*> toPresburgerExp rhs | otherwise = parsePred given toPresburgerExp ty splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type]) @@ -432,19 +460,76 @@ guard $ n >= 2 return (con, drop (n - 2) ts) +data DataCond = DataCond { lhs, rhs :: Type, condCases :: CondCases } + +data CondCases = CondCases { ltCase, eqCase, gtCase :: Bool } + deriving (Show, Eq, Ord) + +fromCondCases :: CondCases -> Expr -> Expr -> Prop +fromCondCases (CondCases True False False) = (:<) +fromCondCases (CondCases False True False) = (:==) +fromCondCases (CondCases False False True) = (:>) +fromCondCases (CondCases True True False) = (:<=) +fromCondCases (CondCases True False True) = (:/=) +fromCondCases (CondCases True True True) = const $ const PTrue +fromCondCases (CondCases False True True) = (:>=) +fromCondCases (CondCases False False False) = const $ const PFalse + +parseOrdCond :: Given Translation => Type -> Maybe DataCond +parseOrdCond ty = do + (con, lastN 4 -> [cmp, ltTy, eqTy, gtTy]) <- splitTyConApp_maybe ty + guard $ con `elem` ordCond given + (cmpCon, lastN 2 -> [lhs, rhs]) <- splitTyConApp_maybe cmp + guard $ cmpCon `elem` natCompare given + ltCase <- decodeTyBool ltTy + eqCase <- decodeTyBool eqTy + gtCase <- decodeTyBool gtTy + let condCases = CondCases{..} + pure DataCond{..} + +decodeTyBool :: Type -> Maybe Bool +decodeTyBool ty = do + con <- tyConAppTyCon_maybe ty + (True <$ guard (con == promotedTrueDataCon)) + <|> (False <$ guard (con == promotedFalseDataCon)) + + toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop toPresburgerPredTree (EqPred NomEq p false) -- P ~ 'False <=> Not P ~ 'True | maybe False (`elem` falseData given) $ tyConAppTyCon_maybe false = - Not <$> toPresburgerPredTree (EqPred NomEq p (mkTyConTy promotedTrueDataCon)) -toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True - | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b + Not <$> toPresburgerPred p +toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'b + | Just isTrue <- decodeTyBool b , Just (con, [t1, t2]) <- splitTyConAppLastBin p , con `elem` natLeqBool given = - (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 -toPresburgerPredTree (EqPred NomEq p b) -- (n :<=? m) ~ 'True + if isTrue + then (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 + else (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p b) -- (n : toPresburgerExp t1 <*> toPresburgerExp t2 + else (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p b) -- (n :>? m) ~ b + | Just isTrue <- decodeTyBool b + , Just (con, [t1, t2]) <- splitTyConAppLastBin p + , con `elem` natGtBool given = + if isTrue + then (:>) <$> toPresburgerExp t1 <*> toPresburgerExp t2 + else (:<=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p b) -- (n :>=? m) ~ b + | Just isTrue <- decodeTyBool b + , Just (con, [t1, t2]) <- splitTyConAppLastBin p + , con `elem` natGeqBool given = + if isTrue + then (:>=) <$> toPresburgerExp t1 <*> toPresburgerExp t2 + else (:<) <$> toPresburgerExp t1 <*> toPresburgerExp t2 +toPresburgerPredTree (EqPred NomEq p b) | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b = toPresburgerPred p -toPresburgerPredTree (EqPred NomEq b p) -- 'True ~ (n :<=? m) +toPresburgerPredTree (EqPred NomEq b p) | maybe False (`elem` trueData given) $ tyConAppTyCon_maybe b = toPresburgerPred p toPresburgerPredTree (EqPred NomEq p q) -- (p :: Bool) ~ (q :: Bool) @@ -477,11 +562,26 @@ MaybeT (return $ lookup cmp orderingDic) <*> toPresburgerExp a <*> toPresburgerExp b +toPresburgerPredTree (EqPred NomEq cond p) + -- OrdCond (CmpNat _ _) lt eq gt ~ ? (for GHC >= 9.2) + | Just DataCond{..} <- parseOrdCond cond = do + body <- fromCondCases condCases + <$> toPresburgerExp lhs + <*> toPresburgerExp rhs + maybe ((body <=>) <$> toPresburgerPred p) + (\q -> if q then pure body else pure $ Not body) + $ decodeTyBool p + -- ? ~ OrdCond (CmpNat _ _) lt eq gt (for GHC >= 9.2) + | Just DataCond{..} <- parseOrdCond p = do + body <- fromCondCases condCases + <$> toPresburgerExp lhs + <*> toPresburgerExp rhs + maybe ((body <=>) <$> toPresburgerPred cond) + (\q -> if q then pure body else pure $ Not body) + $ decodeTyBool cond toPresburgerPredTree (ClassPred con ts) -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat) - | let n = length ts - , n >= 2 - , [t1, t2] <- drop (n - 2) ts + | [t1, t2] <- lastN 2 ts , typeKind t1 `eqType` typeNatKind , typeKind t2 `eqType` typeNatKind = let p = lookup (classTyCon con) binPropDic @@ -543,6 +643,8 @@ lastTwo :: [a] -> [a] lastTwo = drop <$> subtract 2 . length <*> id +lastN :: Int -> [a] -> [a] +lastN n = drop <$> subtract n . length <*> id simpleExp :: Given Translation => Type -> Type simpleExp (AppTy t1 t2) = AppTy (simpleExp t1) (simpleExp t2)