{-# 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 (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 a b. TcPluginM (a -> b) -> TcPluginM a -> TcPluginM b
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 (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
singNatLeq :: SingletonCons -> TyCon
singNatGeq :: SingletonCons -> TyCon
singNatLt :: SingletonCons -> TyCon
singNatGt :: SingletonCons -> TyCon
singNatPlus :: SingletonCons -> TyCon
singNatMinus :: SingletonCons -> TyCon
singNatTimes :: SingletonCons -> TyCon
singNatCompare :: SingletonCons -> TyCon
singTrueSym0 :: SingletonCons -> TyCon
singFalseSym0 :: SingletonCons -> TyCon
caseNameForSingLeq :: SingletonCons -> TyCon
caseNameForSingGeq :: SingletonCons -> TyCon
caseNameForSingLt :: SingletonCons -> TyCon
caseNameForSingGt :: SingletonCons -> TyCon
singMin :: SingletonCons -> TyCon
singMax :: SingletonCons -> TyCon
caseNameForMin :: SingletonCons -> TyCon
caseNameForMax :: SingletonCons -> TyCon
singNatLeq :: TyCon
singNatGeq :: TyCon
singNatLt :: TyCon
singNatGt :: TyCon
singNatPlus :: TyCon
singNatMinus :: TyCon
singNatTimes :: TyCon
singNatCompare :: TyCon
singTrueSym0 :: TyCon
singFalseSym0 :: TyCon
caseNameForSingLeq :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingGt :: TyCon
singMin :: TyCon
singMax :: TyCon
caseNameForMin :: TyCon
caseNameForMax :: 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 = [singNatLeq]
      , natGeqBool = [singNatGeq]
      , natLtBool = [singNatLt]
      , natGtBool = [singNatGt]
      , natCompare = [singNatCompare]
      , natPlus = [singNatPlus]
      , natMinus = [singNatMinus]
      , natTimes = [singNatTimes]
      , parsePred = parseSingPred
      , parseExpr = parseSingExpr
      , trueData = [singTrueSym0]
      , natMin = [singMin]
      , natMax = [singMax]
      , falseData = [singFalseSym0]
      }

singPackage :: FastString
singPackage :: FastString
singPackage = FastString
"singletons-base"

ordModName, numModName, prelInstName :: ModuleName
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"

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 = ModuleUnit -> ModuleName -> Module
forall u. u -> ModuleName -> GenModule u
mkModule ModuleUnit
singUnit ModuleName
prelInstName
      singletonsNum :: Module
singletonsNum = ModuleUnit -> ModuleName -> Module
forall u. u -> ModuleName -> GenModule u
mkModule ModuleUnit
singUnit ModuleName
numModName
  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")
  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
"-")
  TyCon
singMin <- 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
"Min")
  TyCon
singMax <- 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
"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 (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")
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: minMaxes" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$
    (TyCon, TyCon, TyCon, TyCon) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TyCon
singMin, TyCon
singMax, TyCon
caseNameForMin, TyCon
caseNameForMax)
  SingletonCons -> TcPluginM SingletonCons
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return SingletonCons {TyCon
singNatLeq :: TyCon
singNatGeq :: TyCon
singNatLt :: TyCon
singNatGt :: TyCon
singNatPlus :: TyCon
singNatMinus :: TyCon
singNatTimes :: TyCon
singNatCompare :: TyCon
singTrueSym0 :: TyCon
singFalseSym0 :: TyCon
caseNameForSingLeq :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingGt :: TyCon
singMin :: TyCon
singMax :: TyCon
caseNameForMin :: TyCon
caseNameForMax :: TyCon
singTrueSym0 :: TyCon
singFalseSym0 :: TyCon
singNatLeq :: TyCon
singNatLt :: TyCon
singNatGeq :: TyCon
singNatGt :: TyCon
singNatPlus :: TyCon
singNatTimes :: TyCon
singNatMinus :: TyCon
singMin :: TyCon
singMax :: TyCon
caseNameForSingLeq :: TyCon
caseNameForSingLt :: TyCon
caseNameForSingGeq :: TyCon
caseNameForSingGt :: TyCon
caseNameForMin :: TyCon
caseNameForMax :: TyCon
singNatCompare :: 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 " (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
con)
  Just (TyCon
appTy0, [Type
n, Type
b, Type
bdy, Type
r]) <- (Type -> (TyCon, [Type])) -> Maybe Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> (TyCon, [Type])
splitTyConApp (Maybe Type -> Maybe (TyCon, [Type]))
-> TcPluginM (Maybe Type) -> TcPluginM (Maybe (TyCon, [Type]))
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' <- (TyCon -> [Type] -> TcPluginM (Maybe Type))
-> (TyCon, [Type]) -> TcPluginM (Maybe Type)
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]
_) = (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
dat'
  TyCon -> TcPluginM TyCon
forall a. a -> TcPluginM a
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 " (TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr TyCon
con)
  Just (TyCon
appTy0, [Type
n, Type
b, Type
bdy, Type
r]) <- (Type -> (TyCon, [Type])) -> Maybe Type -> Maybe (TyCon, [Type])
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Type -> (TyCon, [Type])
splitTyConApp (Maybe Type -> Maybe (TyCon, [Type]))
-> TcPluginM (Maybe Type) -> TcPluginM (Maybe (TyCon, [Type]))
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' <- (TyCon -> [Type] -> TcPluginM (Maybe Type))
-> (TyCon, [Type]) -> TcPluginM (Maybe Type)
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) = " ((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 a. a -> TcPluginM a
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 :: forall a. [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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([a] -> [a] -> [a]) -> ([a] -> [a]) -> [a] -> [a]
forall a b. ([a] -> a -> b) -> ([a] -> a) -> [a] -> b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [a] -> [a]
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
_]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
  , Just Expr -> Expr -> Expr
bin <- TyCon
-> [(TyCon, Expr -> Expr -> Expr)] -> Maybe (Expr -> Expr -> Expr)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Expr)]
Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]
minLikeCaseDic = do
      StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM ()
 -> MaybeT (StateT ParseEnv TcPluginM) ())
-> StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TcPluginM () -> StateT ParseEnv TcPluginM ()
forall (m :: * -> *) a. Monad m => m a -> StateT ParseEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM () -> StateT ParseEnv TcPluginM ())
-> TcPluginM () -> StateT ParseEnv TcPluginM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"hit!" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ (Type, TyCon) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type
ty, TyCon
con)
      Expr -> Expr -> Expr
bin (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
toE Type
l MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toE Type
r
  | Bool
otherwise = do
      StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM ()
 -> MaybeT (StateT ParseEnv TcPluginM) ())
-> StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TcPluginM () -> StateT ParseEnv TcPluginM ()
forall (m :: * -> *) a. Monad m => m a -> StateT ParseEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM () -> StateT ParseEnv TcPluginM ())
-> TcPluginM () -> StateT ParseEnv TcPluginM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"I don't know how to read:" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ (Type, Maybe (TyCon, [Type])) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type
ty, (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty)
      Machine Expr
forall a. MaybeT (StateT ParseEnv TcPluginM) a
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 SingletonCons
forall a. Given a => a
given, Expr -> Expr -> Expr
Min)
  , (SingletonCons -> TyCon
caseNameForMax SingletonCons
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
(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]) <- (() :: Constraint) => 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]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
toExp Type
r
  | Bool
otherwise = do
      StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM ()
 -> MaybeT (StateT ParseEnv TcPluginM) ())
-> StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TcPluginM () -> StateT ParseEnv TcPluginM ()
forall (m :: * -> *) a. Monad m => m a -> StateT ParseEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM () -> StateT ParseEnv TcPluginM ())
-> TcPluginM () -> StateT ParseEnv TcPluginM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: Miokuring" (Type -> SDoc
forall a. Outputable a => a -> SDoc
ppr Type
ty)
      Machine Prop
forall a. MaybeT (StateT ParseEnv TcPluginM) a
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 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 :: Given SingletonCons =>
(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]) <- (() :: Constraint) => 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]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
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]) <- (() :: Constraint) => 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]) <- (() :: Constraint) => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
cmpTy
  , TyCon
cmp TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a b. (a -> b) -> (Expr -> a) -> Expr -> b
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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
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 a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero