{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
module Data.Singletons.TypeNats.Presburger
( plugin,
singletonTranslation,
)
where
import Control.Monad
import Control.Monad.Trans (MonadTrans (lift))
import Data.Reflection (Given, give, given)
import GHC.TypeLits.Presburger.Compat
import GHC.TypeLits.Presburger.Types
plugin :: Plugin
plugin :: Plugin
plugin =
TcPluginM Translation -> Plugin
pluginWith forall a b. (a -> b) -> a -> b
$
forall a. Semigroup a => a -> a -> a
(<>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM Translation
defaultTranslation forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPluginM Translation
singletonTranslation
data SingletonCons = SingletonCons
{ SingletonCons -> TyCon
singNatLeq :: TyCon
, SingletonCons -> TyCon
singNatGeq :: TyCon
, SingletonCons -> TyCon
singNatLt :: TyCon
, SingletonCons -> TyCon
singNatGt :: TyCon
, SingletonCons -> TyCon
singNatPlus :: TyCon
, SingletonCons -> TyCon
singNatMinus :: TyCon
, SingletonCons -> TyCon
singNatTimes :: TyCon
, SingletonCons -> TyCon
singNatCompare :: TyCon
, SingletonCons -> TyCon
singTrueSym0 :: TyCon
, SingletonCons -> TyCon
singFalseSym0 :: TyCon
, SingletonCons -> TyCon
caseNameForSingLeq :: TyCon
, SingletonCons -> TyCon
caseNameForSingGeq :: TyCon
, SingletonCons -> TyCon
caseNameForSingLt :: TyCon
, SingletonCons -> TyCon
caseNameForSingGt :: TyCon
, SingletonCons -> TyCon
singMin :: TyCon
, SingletonCons -> TyCon
singMax :: TyCon
, SingletonCons -> TyCon
caseNameForMin :: TyCon
, SingletonCons -> TyCon
caseNameForMax :: TyCon
}
singletonTranslation ::
TcPluginM Translation
singletonTranslation :: TcPluginM Translation
singletonTranslation = SingletonCons -> Translation
toTranslation forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM SingletonCons
genSingletonCons
toTranslation ::
SingletonCons -> Translation
toTranslation :: SingletonCons -> Translation
toTranslation scs :: SingletonCons
scs@SingletonCons {TyCon
caseNameForMax :: TyCon
caseNameForMin :: TyCon
singMax :: TyCon
singMin :: TyCon
caseNameForSingGt :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLeq :: TyCon
singFalseSym0 :: TyCon
singTrueSym0 :: TyCon
singNatCompare :: TyCon
singNatTimes :: TyCon
singNatMinus :: TyCon
singNatPlus :: TyCon
singNatGt :: TyCon
singNatLt :: TyCon
singNatGeq :: TyCon
singNatLeq :: TyCon
caseNameForMax :: SingletonCons -> TyCon
caseNameForMin :: SingletonCons -> TyCon
singMax :: SingletonCons -> TyCon
singMin :: SingletonCons -> TyCon
caseNameForSingGt :: SingletonCons -> TyCon
caseNameForSingLt :: SingletonCons -> TyCon
caseNameForSingGeq :: SingletonCons -> TyCon
caseNameForSingLeq :: SingletonCons -> TyCon
singFalseSym0 :: SingletonCons -> TyCon
singTrueSym0 :: SingletonCons -> TyCon
singNatCompare :: SingletonCons -> TyCon
singNatTimes :: SingletonCons -> TyCon
singNatMinus :: SingletonCons -> TyCon
singNatPlus :: SingletonCons -> TyCon
singNatGt :: SingletonCons -> TyCon
singNatLt :: SingletonCons -> TyCon
singNatGeq :: SingletonCons -> TyCon
singNatLeq :: SingletonCons -> TyCon
..} =
forall a r. a -> (Given a => r) -> r
give SingletonCons
scs forall a b. (a -> b) -> a -> b
$
forall a. Monoid a => a
mempty
{ natLeqBool :: [TyCon]
natLeqBool = [TyCon
singNatLeq]
, natGeqBool :: [TyCon]
natGeqBool = [TyCon
singNatGeq]
, natLtBool :: [TyCon]
natLtBool = [TyCon
singNatLt]
, natGtBool :: [TyCon]
natGtBool = [TyCon
singNatGt]
, natCompare :: [TyCon]
natCompare = [TyCon
singNatCompare]
, natPlus :: [TyCon]
natPlus = [TyCon
singNatPlus]
, natMinus :: [TyCon]
natMinus = [TyCon
singNatMinus]
, natTimes :: [TyCon]
natTimes = [TyCon
singNatTimes]
, parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
parsePred = Given SingletonCons =>
(Type -> Machine Expr) -> Type -> Machine Prop
parseSingPred
, parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr
parseExpr = Given SingletonCons =>
(Type -> Machine Expr) -> Type -> Machine Expr
parseSingExpr
, trueData :: [TyCon]
trueData = [TyCon
singTrueSym0]
, natMin :: [TyCon]
natMin = [TyCon
singMin]
, natMax :: [TyCon]
natMax = [TyCon
singMax]
, falseData :: [TyCon]
falseData = [TyCon
singFalseSym0]
}
singPackage :: FastString
#if defined(MIN_VERISION_singletons_base)
singPackage = "singletons-base"
#else
singPackage :: FastString
singPackage = FastString
"singletons"
#endif
ordModName, numModName, prelInstName :: ModuleName
#if defined(SINGLETONS_BASE)
ordModName :: ModuleName
ordModName = String -> ModuleName
mkModuleName String
"Data.Ord.Singletons"
numModName :: ModuleName
numModName = String -> ModuleName
mkModuleName String
"GHC.Num.Singletons"
prelInstName :: ModuleName
prelInstName = String -> ModuleName
mkModuleName String
"Data.Singletons.Base.Instances"
#else
ordModName = mkModuleName "Data.Singletons.Prelude.Ord"
numModName = mkModuleName "Data.Singletons.Prelude.Num"
prelInstName = mkModuleName "Data.Singletons.Prelude.Instances"
#endif
genSingletonCons :: TcPluginM SingletonCons
genSingletonCons :: TcPluginM SingletonCons
genSingletonCons = do
Module
singletonOrd <- ModuleName -> FastString -> TcPluginM Module
lookupModule ModuleName
ordModName FastString
singPackage
let singUnit :: ModuleUnit
singUnit = Module -> ModuleUnit
moduleUnit' Module
singletonOrd
prel :: Module
prel = forall u. u -> ModuleName -> GenModule u
mkModule ModuleUnit
singUnit ModuleName
prelInstName
singletonsNum :: Module
singletonsNum = forall u. u -> ModuleName -> GenModule u
mkModule ModuleUnit
singUnit ModuleName
numModName
TyCon
singTrueSym0 <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
prel (String -> OccName
mkTcOcc String
"TrueSym0")
TyCon
singFalseSym0 <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
prel (String -> OccName
mkTcOcc String
"FalseSym0")
#if MIN_VERSION_singletons(2,4,1)
TyCon
singNatLeq <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
"<=")
TyCon
singNatLt <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
"<")
TyCon
singNatGeq <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
">=")
TyCon
singNatGt <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
">")
TyCon
singNatPlus <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonsNum (String -> OccName
mkTcOcc String
"+")
TyCon
singNatTimes <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonsNum (String -> OccName
mkTcOcc String
"*")
TyCon
singNatMinus <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonsNum (String -> OccName
mkTcOcc String
"-")
#else
singNatLeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<=")
singNatLt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":<")
singNatGeq <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>=")
singNatGt <- tcLookupTyCon =<< lookupOrig singletonOrd (mkTcOcc ":>")
singNatPlus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":+")
singNatTimes <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":*")
singNatMinus <- tcLookupTyCon =<< lookupOrig singletonsNum (mkTcOcc ":-")
#endif
TyCon
singMin <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
"Min")
TyCon
singMax <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
"Max")
TyCon
caseNameForSingLeq <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel TyCon
singNatLeq
TyCon
caseNameForSingLt <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel TyCon
singNatLt
TyCon
caseNameForSingGeq <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel TyCon
singNatGeq
TyCon
caseNameForSingGt <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel TyCon
singNatGt
TyCon
caseNameForMin <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinOp TyCon
singMin
TyCon
caseNameForMax <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinOp TyCon
singMax
TyCon
singNatCompare <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
singletonOrd (String -> OccName
mkTcOcc String
"Compare")
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: minMaxes" forall a b. (a -> b) -> a -> b
$
forall a. Outputable a => a -> SDoc
ppr (TyCon
singMin, TyCon
singMax, TyCon
caseNameForMin, TyCon
caseNameForMax)
forall (m :: * -> *) a. Monad m => a -> m a
return SingletonCons {TyCon
singNatCompare :: TyCon
caseNameForMax :: TyCon
caseNameForMin :: TyCon
caseNameForSingGt :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingLeq :: TyCon
singMax :: TyCon
singMin :: TyCon
singNatMinus :: TyCon
singNatTimes :: TyCon
singNatPlus :: TyCon
singNatGt :: TyCon
singNatGeq :: TyCon
singNatLt :: TyCon
singNatLeq :: TyCon
singFalseSym0 :: TyCon
singTrueSym0 :: TyCon
caseNameForMax :: TyCon
caseNameForMin :: TyCon
singMax :: TyCon
singMin :: TyCon
caseNameForSingGt :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLeq :: TyCon
singFalseSym0 :: TyCon
singTrueSym0 :: TyCon
singNatCompare :: TyCon
singNatTimes :: TyCon
singNatMinus :: TyCon
singNatPlus :: TyCon
singNatGt :: TyCon
singNatLt :: TyCon
singNatGeq :: TyCon
singNatLeq :: TyCon
..}
getCaseNameForSingletonBinOp :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinOp :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinOp TyCon
con = do
let vars :: [Type]
vars = [Type
typeNatKind, TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit Integer
0), TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit Integer
0)]
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"matching... for " (forall a. Outputable a => a -> SDoc
ppr TyCon
con)
Just (TyCon
appTy0, [Type
n, Type
b, Type
bdy, Type
r]) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> (TyCon, [Type])
splitTyConApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
con [Type]
vars
let (TyCon
appTy, [Type]
args) = Type -> (TyCon, [Type])
splitTyConApp Type
bdy
Just Type
innermost <- TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
appTy [Type]
args
Just Type
dat <- TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
appTy0 [Type
n, Type
b, Type
innermost, Type
r]
Just Type
dat' <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' (Type -> (TyCon, [Type])
splitTyConApp Type
dat)
let Just (TyCon
con', [Type]
_) = HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
dat'
forall (m :: * -> *) a. Monad m => a -> m a
return TyCon
con'
getCaseNameForSingletonBinRel :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonBinRel TyCon
con = do
let vars :: [Type]
vars = [Type
typeNatKind, TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit Integer
0), TyLit -> Type
LitTy (Integer -> TyLit
NumTyLit Integer
0)]
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"matching... for " (forall a. Outputable a => a -> SDoc
ppr TyCon
con)
Just (TyCon
appTy0, [Type
n, Type
b, Type
bdy, Type
r]) <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> (TyCon, [Type])
splitTyConApp forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
con [Type]
vars
let (TyCon
appTy, [Type]
args) = Type -> (TyCon, [Type])
splitTyConApp Type
bdy
Just Type
innermost <- TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
appTy [Type]
args
Just Type
dat <- TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' TyCon
appTy0 [Type
n, Type
b, Type
innermost, Type
r]
Just Type
dat' <- forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyCon -> [Type] -> TcPluginM (Maybe Type)
matchFam' (Type -> (TyCon, [Type])
splitTyConApp Type
dat)
String -> SDoc -> TcPluginM ()
tcPluginTrace String
"matched. (orig, inner) = " (forall a. Outputable a => a -> SDoc
ppr (TyCon
con, forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (TyCon, [Type])
splitTyConApp Type
dat'))
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ Type -> (TyCon, [Type])
splitTyConApp Type
dat'
lastTwo :: [a] -> [a]
lastTwo :: forall a. [a] -> [a]
lastTwo = forall a. Int -> [a] -> [a]
drop forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Num a => a -> a -> a
subtract Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Int
length forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall a. a -> a
id
parseSingExpr ::
(Given SingletonCons) =>
(Type -> Machine Expr) ->
Type ->
Machine Expr
parseSingExpr :: Given SingletonCons =>
(Type -> Machine Expr) -> Type -> Machine Expr
parseSingExpr Type -> Machine Expr
toE Type
ty
| Just (TyCon
con, [Type
_, Type
l, Type
r, Type
_]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
, Just Expr -> Expr -> Expr
bin <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]
minLikeCaseDic = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"hit!" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr (Type
ty, TyCon
con)
Expr -> Expr -> Expr
bin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toE Type
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toE Type
r
| Bool
otherwise = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"I don't know how to read:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr (Type
ty, HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
minLikeCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]
minLikeCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]
minLikeCaseDic =
[ (SingletonCons -> TyCon
caseNameForMin forall a. Given a => a
given, Expr -> Expr -> Expr
Min)
, (SingletonCons -> TyCon
caseNameForMax forall a. Given a => a
given, Expr -> Expr -> Expr
Max)
]
parseSingPred ::
(Given SingletonCons) =>
(Type -> Machine Expr) ->
Type ->
Machine Prop
parseSingPred :: Given SingletonCons =>
(Type -> Machine Expr) -> Type -> Machine Prop
parseSingPred Type -> Machine Expr
toExp Type
ty
| Type -> Bool
isEqPred Type
ty = Given SingletonCons =>
(Type -> Machine Expr) -> PredTree -> Machine Prop
parseSingPredTree Type -> Machine Expr
toExp forall a b. (a -> b) -> a -> b
$ Type -> PredTree
classifyPredType Type
ty
| Just (TyCon
con, [Type
_, Type
_, Type
_, Type
_, Type
cmpTy]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
, Just Expr -> Expr -> Prop
bin <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
, Just (TyCon
cmp, forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
, TyCon
cmp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
Expr -> Expr -> Prop
bin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
| Bool
otherwise = do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: Miokuring" (forall a. Outputable a => a -> SDoc
ppr Type
ty)
forall (m :: * -> *) a. MonadPlus m => m a
mzero
compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic =
[ (SingletonCons -> TyCon
caseNameForSingLeq forall a. Given a => a
given, Expr -> Expr -> Prop
(:<=))
, (SingletonCons -> TyCon
caseNameForSingLt forall a. Given a => a
given, Expr -> Expr -> Prop
(:<))
, (SingletonCons -> TyCon
caseNameForSingGeq forall a. Given a => a
given, Expr -> Expr -> Prop
(:>=))
, (SingletonCons -> TyCon
caseNameForSingGt forall a. Given a => a
given, Expr -> Expr -> Prop
(:>))
]
parseSingPredTree ::
Given SingletonCons =>
(Type -> Machine Expr) ->
PredTree ->
Machine Prop
parseSingPredTree :: Given SingletonCons =>
(Type -> Machine Expr) -> PredTree -> Machine Prop
parseSingPredTree Type -> Machine Expr
toExp (EqPred EqRel
NomEq Type
p Type
b)
| forall a. a -> Maybe a
Just TyCon
promotedTrueDataCon forall a. Eq a => a -> a -> Bool
== Type -> Maybe TyCon
tyConAppTyCon_maybe Type
b
, Just (TyCon
con, [Type
_, Type
_, Type
_, Type
_, Type
cmpTy]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
p
, Just Expr -> Expr -> Prop
bin <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
, Just (TyCon
cmp, forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
, TyCon
cmp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
Expr -> Expr -> Prop
bin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
| forall a. a -> Maybe a
Just TyCon
promotedFalseDataCon forall a. Eq a => a -> a -> Bool
== Type -> Maybe TyCon
tyConAppTyCon_maybe Type
b
, Just (TyCon
con, [Type
_, Type
_, Type
_, Type
_, Type
cmpTy]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
p
, Just Expr -> Expr -> Prop
bin <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
, Just (TyCon
cmp, forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
, TyCon
cmp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Prop
Not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> Prop
bin forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
parseSingPredTree Type -> Machine Expr
_ PredTree
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero