{-# 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) -- (n :<=? m) ~ 'True
  | forall a. a -> Maybe a
Just TyCon
promotedTrueDataCon 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])
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 -- Singleton's <=...
    , 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