{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances      #-}
{-# LANGUAGE MultiWayIf, OverloadedStrings, PatternGuards, RankNTypes #-}
{-# LANGUAGE RecordWildCards, TypeOperators, ViewPatterns             #-}
module Data.Singletons.TypeNats.Presburger
  (plugin, singletonTranslation
  ) where
import GHC.TypeLits.Presburger.Compat
import GHC.TypeLits.Presburger.Types

import Control.Monad
import Data.Reflection (Given, give, given)
import GHC             (mkModule, moduleUnitId)
import TcPluginM       (lookupOrig, matchFam)
import Type            (splitTyConApp)

plugin :: Plugin
plugin :: Plugin
plugin = TcPluginM Translation -> Plugin
pluginWith (TcPluginM Translation -> Plugin)
-> TcPluginM Translation -> Plugin
forall a b. (a -> b) -> a -> b
$
  Translation -> Translation -> Translation
forall a. Semigroup a => a -> a -> a
(<>) (Translation -> Translation -> Translation)
-> TcPluginM Translation -> TcPluginM (Translation -> Translation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM Translation
defaultTranslation TcPluginM (Translation -> Translation)
-> TcPluginM Translation -> TcPluginM Translation
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
      }

singletonTranslation
  :: TcPluginM Translation
singletonTranslation :: TcPluginM Translation
singletonTranslation = SingletonCons -> Translation
toTranslation (SingletonCons -> Translation)
-> TcPluginM SingletonCons -> TcPluginM Translation
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
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
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
..} =
  SingletonCons
-> (Given SingletonCons => Translation) -> Translation
forall a r. a -> (Given a => r) -> r
give SingletonCons
scs ((Given SingletonCons => Translation) -> Translation)
-> (Given SingletonCons => Translation) -> Translation
forall a b. (a -> b) -> a -> b
$
    Translation
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
(Type -> Machine Expr) -> Type -> Machine Prop
parseSingPred
    , trueData :: [TyCon]
trueData = [TyCon
singTrueSym0]
    , falseData :: [TyCon]
falseData = [TyCon
singFalseSym0]
    }

genSingletonCons :: TcPluginM SingletonCons
genSingletonCons :: TcPluginM SingletonCons
genSingletonCons = do
  Module
singletonOrd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Data.Singletons.Prelude.Ord") (String -> FastString
fsLit String
"singletons")
  Module
singletonsNum <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Data.Singletons.Prelude.Num") (String -> FastString
fsLit String
"singletons")
  let prel :: Module
prel = UnitId -> ModuleName -> Module
mkModule (Module -> UnitId
moduleUnitId Module
singletonsNum) (String -> ModuleName
mkModuleName String
"Data.Singletons.Prelude.Instances")
  TyCon
singTrueSym0 <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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 (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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
caseNameForSingLeq <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp TyCon
singNatLeq
  TyCon
caseNameForSingLt <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp TyCon
singNatLt
  TyCon
caseNameForSingGeq <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp TyCon
singNatGeq
  TyCon
caseNameForSingGt <- TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp TyCon
singNatGt
  TyCon
singNatCompare <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
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")
  SingletonCons -> TcPluginM SingletonCons
forall (m :: * -> *) a. Monad m => a -> m a
return SingletonCons :: TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> SingletonCons
SingletonCons{TyCon
singNatCompare :: TyCon
caseNameForSingGt :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingLeq :: TyCon
singNatMinus :: TyCon
singNatTimes :: TyCon
singNatPlus :: TyCon
singNatGt :: TyCon
singNatGeq :: TyCon
singNatLt :: TyCon
singNatLeq :: TyCon
singFalseSym0 :: TyCon
singTrueSym0 :: 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
..}

getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp :: TyCon -> TcPluginM TyCon
getCaseNameForSingletonOp 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 " (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
con)
  Just (TyCon
appTy0, [Type
n,Type
b,Type
bdy,Type
r]) <- ((TcCoercion, Type) -> (TyCon, [Type]))
-> Maybe (TcCoercion, Type) -> Maybe (TyCon, [Type])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type -> (TyCon, [Type])
splitTyConApp (Type -> (TyCon, [Type]))
-> ((TcCoercion, Type) -> Type)
-> (TcCoercion, Type)
-> (TyCon, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TcCoercion, Type) -> Type
forall a b. (a, b) -> b
snd) (Maybe (TcCoercion, Type) -> Maybe (TyCon, [Type]))
-> TcPluginM (Maybe (TcCoercion, Type))
-> TcPluginM (Maybe (TyCon, [Type]))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type))
matchFam  TyCon
con [Type]
vars
  let (TyCon
appTy, [Type]
args) = Type -> (TyCon, [Type])
splitTyConApp Type
bdy
  Just Type
innermost <- ((TcCoercion, Type) -> Type)
-> Maybe (TcCoercion, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TcCoercion, Type) -> Type
forall a b. (a, b) -> b
snd (Maybe (TcCoercion, Type) -> Maybe Type)
-> TcPluginM (Maybe (TcCoercion, Type)) -> TcPluginM (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type))
matchFam TyCon
appTy [Type]
args
  Just (TcCoercion
_, Type
dat) <- TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type))
matchFam TyCon
appTy0 [Type
n,Type
b,Type
innermost,Type
r]
  Just Type
dat' <- ((TcCoercion, Type) -> Type)
-> Maybe (TcCoercion, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (TcCoercion, Type) -> Type
forall a b. (a, b) -> b
snd (Maybe (TcCoercion, Type) -> Maybe Type)
-> TcPluginM (Maybe (TcCoercion, Type)) -> TcPluginM (Maybe Type)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type)))
-> (TyCon, [Type]) -> TcPluginM (Maybe (TcCoercion, Type))
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry TyCon -> [Type] -> TcPluginM (Maybe (TcCoercion, Type))
matchFam (Type -> (TyCon, [Type])
splitTyConApp Type
dat)
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"matched. (orig, inner) = " ((TyCon, TyCon) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon
con, (TyCon, [Type]) -> TyCon
forall a b. (a, b) -> a
fst ((TyCon, [Type]) -> TyCon) -> (TyCon, [Type]) -> TyCon
forall a b. (a -> b) -> a -> b
$ Type -> (TyCon, [Type])
splitTyConApp Type
dat'))
  TyCon -> TcPluginM TyCon
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon -> TcPluginM TyCon) -> TyCon -> TcPluginM TyCon
forall a b. (a -> b) -> a -> b
$ (TyCon, [Type]) -> TyCon
forall a b. (a, b) -> a
fst ((TyCon, [Type]) -> TyCon) -> (TyCon, [Type]) -> TyCon
forall a b. (a -> b) -> a -> b
$ Type -> (TyCon, [Type])
splitTyConApp Type
dat'

lastTwo :: [a] -> [a]
lastTwo :: [a] -> [a]
lastTwo = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Int -> [a] -> [a]) -> ([a] -> Int) -> [a] -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
2 (Int -> Int) -> ([a] -> Int) -> [a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> [a]
forall a. a -> a
id

parseSingPred
  :: (Given SingletonCons)
  => (Type -> Machine Expr) -> Type -> Machine Prop
parseSingPred :: (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
(Type -> Machine Expr) -> PredTree -> Machine Prop
parseSingPredTree Type -> Machine Expr
toExp (PredTree -> Machine Prop) -> PredTree -> Machine Prop
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])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  , Just Expr -> Expr -> Prop
bin <- TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Prop)]
Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
  , Just (TyCon
cmp, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare SingletonCons
forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
      Expr -> Expr -> Prop
bin (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
  | Bool
otherwise = Machine Prop
forall (m :: * -> *) a. MonadPlus m => m a
mzero

compCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic :: [(TyCon, Expr -> Expr -> Prop)]
compCaseDic =
  [ (SingletonCons -> TyCon
caseNameForSingLeq SingletonCons
forall a. Given a => a
given, Expr -> Expr -> Prop
(:<=))
  , (SingletonCons -> TyCon
caseNameForSingLt SingletonCons
forall a. Given a => a
given, Expr -> Expr -> Prop
(:<))
  , (SingletonCons -> TyCon
caseNameForSingGeq SingletonCons
forall a. Given a => a
given, Expr -> Expr -> Prop
(:>=))
  , (SingletonCons -> TyCon
caseNameForSingGt SingletonCons
forall a. Given a => a
given, Expr -> Expr -> Prop
(:>))
  ]


parseSingPredTree
  :: Given SingletonCons
  => (Type -> Machine Expr)
  -> PredTree -> Machine Prop
parseSingPredTree :: (Type -> Machine Expr) -> PredTree -> Machine Prop
parseSingPredTree Type -> Machine Expr
toExp (EqPred EqRel
NomEq Type
p Type
b)  -- (n :<=? m) ~ 'True
  | TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
promotedTrueDataCon  Maybe TyCon -> Maybe TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Maybe TyCon
tyConAppTyCon_maybe Type
b -- Singleton's <=...
  , Just (TyCon
con, [Type
_,Type
_,Type
_,Type
_,Type
cmpTy]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
p
  , Just Expr -> Expr -> Prop
bin <- TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Prop)]
Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
  , Just (TyCon
cmp, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare SingletonCons
forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
    Expr -> Expr -> Prop
bin (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
  | TyCon -> Maybe TyCon
forall a. a -> Maybe a
Just TyCon
promotedFalseDataCon  Maybe TyCon -> Maybe TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== Type -> Maybe TyCon
tyConAppTyCon_maybe Type
b -- Singleton's <=...
  , Just (TyCon
con, [Type
_,Type
_,Type
_,Type
_,Type
cmpTy]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
p
  , Just Expr -> Expr -> Prop
bin <- TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Prop)]
Given SingletonCons => [(TyCon, Expr -> Expr -> Prop)]
compCaseDic
  , Just (TyCon
cmp, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [SingletonCons -> TyCon
singNatCompare SingletonCons
forall a. Given a => a
given, TyCon
typeNatCmpTyCon] =
    (Prop -> Prop) -> (Expr -> Prop) -> Expr -> Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Prop -> Prop
Not ((Expr -> Prop) -> Expr -> Prop)
-> (Expr -> Expr -> Prop) -> Expr -> Expr -> Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr -> Prop
bin (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toExp Type
l MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
parseSingPredTree Type -> Machine Expr
_ PredTree
_ = Machine Prop
forall (m :: * -> *) a. MonadPlus m => m a
mzero