ghc-typelits-presburger 0.6.0.0 → 0.6.1.0

raw patch · 4 files changed

+325/−59 lines, 4 filesdep ~ghcPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: ghc

API changes (from Hackage documentation)

Files

• examples/simple-arith-core.hs +28/−3
• ghc-typelits-presburger.cabal +6/−5
• src/GHC/TypeLits/Presburger/Compat.hs +146/−8
• src/GHC/TypeLits/Presburger/Types.hs +145/−43

@@ -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.<? m) == 'False)+ghc92GeqEquivNLt _ _ = Refl++-- N.B. We can't replace with predicate style with GHC 9.2.1+-- by the bug in base-4.16.0.0+ghc92NLtToGeq :: (n DTO.<? m) ~ 'True+  => NProxy n -> NProxy m -> (n DTO.>=? m) :~: 'False+ghc92NLtToGeq _ _ = Refl+#endif

@@ -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

@@ -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 "<?")+#else+lookupTyNatBoolLt = pure Nothing+#endif++lookupTyNatPredGt :: TcPluginM (Maybe TyCon)+#if MIN_VERSION_ghc(9,2,0)+lookupTyNatPredGt = Just <$> 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

@@ -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 :<? m) ~ b+  | Just isTrue <- decodeTyBool b+    , Just (con, [t1, t2]) <- splitTyConAppLastBin p+    , con `elem` natLtBool 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` 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)