{-# 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 (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
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
..} =
  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
      , parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr
parseExpr = Given SingletonCons =>
(Type -> Machine Expr) -> Type -> Machine Expr
(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 = mkModuleName "Data.Ord.Singletons"
numModName = mkModuleName "GHC.Num.Singletons"
prelInstName = mkModuleName "Data.Singletons.Base.Instances"
#else
ordModName :: ModuleName
ordModName = String -> ModuleName
mkModuleName String
"Data.Singletons.Prelude.Ord"
numModName :: ModuleName
numModName = String -> ModuleName
mkModuleName String
"Data.Singletons.Prelude.Num"
prelInstName :: ModuleName
prelInstName = String -> ModuleName
mkModuleName String
"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 = ModuleUnit -> ModuleName -> Module
mkModule ModuleUnit
singUnit ModuleName
prelInstName
      singletonsNum :: Module
singletonsNum = ModuleUnit -> ModuleName -> Module
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")
#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
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 (m :: * -> *) a. Monad m => a -> m a
return SingletonCons :: TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> TyCon
-> SingletonCons
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 " (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)
  let Just (TyCon
con', [Type]
_) = HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
dat'
  TyCon -> TcPluginM TyCon
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]) <- ((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

parseSingExpr ::
  (Given SingletonCons) =>
  (Type -> Machine Expr) ->
  Type ->
  Machine Expr
parseSingExpr :: (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])
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 (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 (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 (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 (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 (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, HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty)
    Machine Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero

minLikeCaseDic :: Given SingletonCons => [(TyCon, Expr -> Expr -> Expr)]
minLikeCaseDic :: [(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 :: (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 = do
    StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
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 (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 (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