{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PartialTypeSignatures #-}
{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
-- | Since 0.3.0.0
module GHC.TypeLits.Presburger.Types
  ( pluginWith,
    defaultTranslation,
    Translation (..),
    ParseEnv,
    Machine,
    module Data.Integer.SAT,
  )
where

import Control.Applicative ((<|>))
import Control.Arrow (second)
import Control.Monad (forM_, guard, mzero, unless)
import Control.Monad.State.Class
import Control.Monad.Trans.Class
import Control.Monad.Trans.Maybe (MaybeT (..))
import Control.Monad.Trans.RWS.Strict (runRWS, tell)
import Control.Monad.Trans.State (StateT, runStateT)
import Data.Char (isDigit)
import Data.Foldable (asum)
import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName)
import qualified Data.Integer.SAT as SAT
import Data.List (nub)
#if MIN_VERSION_ghc(9,4,0)
import qualified GHC.Core as GHC (Expr(..))
#endif
import qualified Data.List as L
import qualified Data.Map.Strict as M
import Data.Maybe
  ( catMaybes,
    fromMaybe,
    isNothing,
    listToMaybe,
    maybeToList,
  )
import Data.Reflection (Given, give, given)
import qualified Data.Set as Set
import GHC.TypeLits.Presburger.Compat as Compat
import qualified Data.Foldable as F

assert' :: Prop -> PropSet -> PropSet
assert' :: Prop -> PropSet -> PropSet
assert' Prop
p PropSet
ps = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert PropSet
ps (Prop
p forall a. a -> [a] -> [a]
: [Prop]
varPos)
  where
    varPos :: [Prop]
varPos = [Integer -> Expr
K Integer
0 Expr -> Expr -> Prop
:<= Name -> Expr
Var Name
i | Name
i <- Prop -> [Name]
varsProp Prop
p]

data Proof = Proved | Disproved [(Int, Integer)]
  deriving (ReadPrec [Proof]
ReadPrec Proof
Int -> ReadS Proof
ReadS [Proof]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Proof]
$creadListPrec :: ReadPrec [Proof]
readPrec :: ReadPrec Proof
$creadPrec :: ReadPrec Proof
readList :: ReadS [Proof]
$creadList :: ReadS [Proof]
readsPrec :: Int -> ReadS Proof
$creadsPrec :: Int -> ReadS Proof
Read, Int -> Proof -> ShowS
[Proof] -> ShowS
Proof -> CommandLineOption
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
showList :: [Proof] -> ShowS
$cshowList :: [Proof] -> ShowS
show :: Proof -> CommandLineOption
$cshow :: Proof -> CommandLineOption
showsPrec :: Int -> Proof -> ShowS
$cshowsPrec :: Int -> Proof -> ShowS
Show, Proof -> Proof -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Proof -> Proof -> Bool
$c/= :: Proof -> Proof -> Bool
== :: Proof -> Proof -> Bool
$c== :: Proof -> Proof -> Bool
Eq, Eq Proof
Proof -> Proof -> Bool
Proof -> Proof -> Ordering
Proof -> Proof -> Proof
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Proof -> Proof -> Proof
$cmin :: Proof -> Proof -> Proof
max :: Proof -> Proof -> Proof
$cmax :: Proof -> Proof -> Proof
>= :: Proof -> Proof -> Bool
$c>= :: Proof -> Proof -> Bool
> :: Proof -> Proof -> Bool
$c> :: Proof -> Proof -> Bool
<= :: Proof -> Proof -> Bool
$c<= :: Proof -> Proof -> Bool
< :: Proof -> Proof -> Bool
$c< :: Proof -> Proof -> Bool
compare :: Proof -> Proof -> Ordering
$ccompare :: Proof -> Proof -> Ordering
Ord)

isProved :: Proof -> Bool
isProved :: Proof -> Bool
isProved Proof
Proved = Bool
True
isProved Proof
_ = Bool
False

varsProp :: Prop -> [SAT.Name]
varsProp :: Prop -> [Name]
varsProp (Prop
p :|| Prop
q) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p forall a. [a] -> [a] -> [a]
++ Prop -> [Name]
varsProp Prop
q
varsProp (Prop
p :&& Prop
q) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p forall a. [a] -> [a] -> [a]
++ Prop -> [Name]
varsProp Prop
q
varsProp (Not Prop
p) = Prop -> [Name]
varsProp Prop
p
varsProp (Expr
e :== Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :/= Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :< Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :> Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :<= Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :>= Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp Prop
_ = []

varsExpr :: Expr -> [SAT.Name]
varsExpr :: Expr -> [Name]
varsExpr (Expr
e :+ Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Expr
e :- Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Integer
_ :* Expr
v) = Expr -> [Name]
varsExpr Expr
v
varsExpr (Negate Expr
e) = Expr -> [Name]
varsExpr Expr
e
varsExpr (Min Expr
l Expr
r) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
l forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
r
varsExpr (Max Expr
l Expr
r) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
l forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
r
varsExpr (Var Name
i) = [Name
i]
varsExpr (K Integer
_) = []
varsExpr (If Prop
p Expr
e Expr
v) = forall a. Eq a => [a] -> [a]
nub forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
e forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Div Expr
e Integer
_) = Expr -> [Name]
varsExpr Expr
e
varsExpr (Mod Expr
e Integer
_) = Expr -> [Name]
varsExpr Expr
e

data PluginMode
  = DisallowNegatives
  | AllowNegatives
  deriving (ReadPrec [PluginMode]
ReadPrec PluginMode
Int -> ReadS PluginMode
ReadS [PluginMode]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [PluginMode]
$creadListPrec :: ReadPrec [PluginMode]
readPrec :: ReadPrec PluginMode
$creadPrec :: ReadPrec PluginMode
readList :: ReadS [PluginMode]
$creadList :: ReadS [PluginMode]
readsPrec :: Int -> ReadS PluginMode
$creadsPrec :: Int -> ReadS PluginMode
Read, Int -> PluginMode -> ShowS
[PluginMode] -> ShowS
PluginMode -> CommandLineOption
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
showList :: [PluginMode] -> ShowS
$cshowList :: [PluginMode] -> ShowS
show :: PluginMode -> CommandLineOption
$cshow :: PluginMode -> CommandLineOption
showsPrec :: Int -> PluginMode -> ShowS
$cshowsPrec :: Int -> PluginMode -> ShowS
Show, PluginMode -> PluginMode -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PluginMode -> PluginMode -> Bool
$c/= :: PluginMode -> PluginMode -> Bool
== :: PluginMode -> PluginMode -> Bool
$c== :: PluginMode -> PluginMode -> Bool
Eq, Eq PluginMode
PluginMode -> PluginMode -> Bool
PluginMode -> PluginMode -> Ordering
PluginMode -> PluginMode -> PluginMode
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PluginMode -> PluginMode -> PluginMode
$cmin :: PluginMode -> PluginMode -> PluginMode
max :: PluginMode -> PluginMode -> PluginMode
$cmax :: PluginMode -> PluginMode -> PluginMode
>= :: PluginMode -> PluginMode -> Bool
$c>= :: PluginMode -> PluginMode -> Bool
> :: PluginMode -> PluginMode -> Bool
$c> :: PluginMode -> PluginMode -> Bool
<= :: PluginMode -> PluginMode -> Bool
$c<= :: PluginMode -> PluginMode -> Bool
< :: PluginMode -> PluginMode -> Bool
$c< :: PluginMode -> PluginMode -> Bool
compare :: PluginMode -> PluginMode -> Ordering
$ccompare :: PluginMode -> PluginMode -> Ordering
Ord)

pluginWith :: TcPluginM Translation -> Plugin
pluginWith :: TcPluginM Translation -> Plugin
pluginWith TcPluginM Translation
trans =
  Plugin
defaultPlugin
    { tcPlugin :: TcPlugin
tcPlugin = forall a. a -> Maybe a
Just forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin TcPluginM Translation
trans forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {t :: * -> *} {a}.
(Foldable t, Eq a, IsString a) =>
t a -> PluginMode
procOpts
#if MIN_VERSION_ghc(8,6,0)
    , pluginRecompile :: [CommandLineOption] -> IO PluginRecompile
pluginRecompile = [CommandLineOption] -> IO PluginRecompile
purePlugin
#endif
    }
  where
    procOpts :: t a -> PluginMode
procOpts t a
opts
      | a
"allow-negated-numbers" forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
opts = PluginMode
AllowNegatives
      | Bool
otherwise = PluginMode
DisallowNegatives

presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin TcPluginM Translation
trans PluginMode
mode =
  CommandLineOption -> TcPlugin -> TcPlugin
tracePlugin
    CommandLineOption
"typelits-presburger"
    TcPlugin
      { tcPluginInit :: TcPluginM ()
tcPluginInit = forall (m :: * -> *) a. Monad m => a -> m a
return ()
      , tcPluginStop :: () -> TcPluginM ()
tcPluginStop = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
#if MIN_VERSION_ghc(9,4,1)
      , tcPluginSolve = const $ \_ gs ws -> decidePresburger mode trans () gs [] ws
#else
      , tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = PluginMode -> TcPluginM Translation -> () -> TcPluginSolver
decidePresburger PluginMode
mode TcPluginM Translation
trans
#endif

#if MIN_VERSION_ghc(9,4,1)
      , tcPluginRewrite = mempty
#endif
      }

testIf :: PropSet -> Prop -> Proof
testIf :: PropSet -> Prop -> Proof
testIf PropSet
ps Prop
q = forall b a. b -> (a -> b) -> Maybe a -> b
maybe Proof
Proved [(Int, Integer)] -> Proof
Disproved forall a b. (a -> b) -> a -> b
$ PropSet -> Maybe [(Int, Integer)]
checkSat (Prop -> Prop
Not Prop
q Prop -> PropSet -> PropSet
`assert'` PropSet
ps)

-- Replaces every subtraction with new constant,
-- adding order constraint.
handleSubtraction :: PluginMode -> Prop -> Prop
handleSubtraction :: PluginMode -> Prop -> Prop
handleSubtraction PluginMode
AllowNegatives Prop
p = Prop
p
handleSubtraction PluginMode
DisallowNegatives Prop
p0 =
  let (Prop
p, Set Expr
_, Set Prop
w) = forall r w s a. RWS r w s a -> r -> s -> (a, s, w)
runRWS (forall {m :: * -> *} {r}.
Monad m =>
Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
p0) () forall a. Set a
Set.empty
   in forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> Prop -> Prop
(:&&) Prop
p Set Prop
w
  where
    loop :: Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
PTrue = forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
    loop Prop
PFalse = forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PFalse
    loop (Prop
q :|| Prop
r) = Prop -> Prop -> Prop
(:||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
q forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
r
    loop (Prop
q :&& Prop
r) = Prop -> Prop -> Prop
(:&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
q forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
r
    loop (Not Prop
q) = Prop -> Prop
Not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
q
    loop (Expr
l :<= Expr
r) = Expr -> Expr -> Prop
(:<=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :< Expr
r) = Expr -> Expr -> Prop
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :>= Expr
r) = Expr -> Expr -> Prop
(:>=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :> Expr
r) = Expr -> Expr -> Prop
(:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :== Expr
r) = Expr -> Expr -> Prop
(:==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :/= Expr
r) = Expr -> Expr -> Prop
(:/=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r

    withPositive :: Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive Expr
pos = do
      Set Expr
dic <- forall s (m :: * -> *). MonadState s m => m s
get
      forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (forall a. Ord a => a -> Set a -> Bool
Set.member Expr
pos Set Expr
dic) forall a b. (a -> b) -> a -> b
$ do
        forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> Set a
Set.insert Expr
pos
        forall (m :: * -> *) w r s. Monad m => w -> RWST r w s m ()
tell forall a b. (a -> b) -> a -> b
$ forall a. Ord a => [a] -> Set a
Set.fromList [Expr
pos Expr -> Expr -> Prop
:>= Integer -> Expr
K Integer
0]
      forall (m :: * -> *) a. Monad m => a -> m a
return Expr
pos

    loopExp :: Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp e :: Expr
e@(Negate Expr
_) = forall {m :: * -> *} {r}.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
Negate forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
e
    loopExp (Expr
l :- Expr
r) = do
      Expr
e <- Expr -> Expr -> Expr
(:-) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
      forall {m :: * -> *} {r}.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive Expr
e
    loopExp (Expr
l :+ Expr
r) = Expr -> Expr -> Expr
(:+) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loopExp v :: Expr
v@Var {} = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
    loopExp (Integer
c :* Expr
e)
      | Integer
c forall a. Ord a => a -> a -> Bool
> Integer
0 = (Integer
c Integer -> Expr -> Expr
:*) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
e
      | Bool
otherwise = (forall a. Num a => a -> a
negate Integer
c Integer -> Expr -> Expr
:*) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp (Expr -> Expr
Negate Expr
e)
    loopExp (Min Expr
l Expr
r) = Expr -> Expr -> Expr
Min forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loopExp (Max Expr
l Expr
r) = Expr -> Expr -> Expr
Max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loopExp (If Prop
p Expr
l Expr
r) = Prop -> Expr -> Expr -> Expr
If forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loopExp (Mod Expr
l Integer
n) = Expr -> Integer -> Expr
Mod forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp (Div Expr
l Integer
n) = Expr -> Integer -> Expr
Div forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp e :: Expr
e@(K Integer
_) = forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

data Translation = Translation
  { Translation -> [TyCon]
isEmpty :: [TyCon]
  , Translation -> [TyCon]
ordCond :: [TyCon]
  , Translation -> [TyCon]
assertTy :: [TyCon]
  , Translation -> [TyCon]
isTrue :: [TyCon]
  , Translation -> [TyCon]
trueData :: [TyCon]
  , Translation -> [TyCon]
falseData :: [TyCon]
  , Translation -> [TyCon]
voids :: [TyCon]
  , Translation -> [TyCon]
tyEq :: [TyCon]
  , Translation -> [TyCon]
tyEqBool :: [TyCon]
  , Translation -> [TyCon]
tyEqWitness :: [TyCon]
  , Translation -> [TyCon]
tyNot :: [TyCon]
  , Translation -> [TyCon]
tyAnd :: [TyCon]
  , Translation -> [TyCon]
tyOr :: [TyCon]
  , Translation -> [TyCon]
tyIf :: [TyCon]
  , Translation -> [TyCon]
tyNeqBool :: [TyCon]
  , Translation -> [TyCon]
natPlus :: [TyCon]
  , Translation -> [TyCon]
natMinus :: [TyCon]
  , Translation -> [TyCon]
natExp :: [TyCon]
  , Translation -> [TyCon]
natTimes :: [TyCon]
  , Translation -> [TyCon]
natLeq :: [TyCon]
  , Translation -> [TyCon]
natLeqBool :: [TyCon]
  , Translation -> [TyCon]
natGeq :: [TyCon]
  , Translation -> [TyCon]
natGeqBool :: [TyCon]
  , Translation -> [TyCon]
natLt :: [TyCon]
  , Translation -> [TyCon]
natLtBool :: [TyCon]
  , Translation -> [TyCon]
natGt :: [TyCon]
  , Translation -> [TyCon]
natGtBool :: [TyCon]
  , Translation -> [TyCon]
natMin :: [TyCon]
  , Translation -> [TyCon]
natMax :: [TyCon]
  , Translation -> [TyCon]
orderingLT :: [TyCon]
  , Translation -> [TyCon]
orderingGT :: [TyCon]
  , Translation -> [TyCon]
orderingEQ :: [TyCon]
  , Translation -> [TyCon]
natCompare :: [TyCon]
  , Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
  , Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr :: (Type -> Machine Expr) -> Type -> Machine Expr
  }

instance Semigroup Translation where
  Translation
l <> :: Translation -> Translation -> Translation
<> Translation
r =
    Translation
      { isEmpty :: [TyCon]
isEmpty = Translation -> [TyCon]
isEmpty Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
isEmpty Translation
r
      , isTrue :: [TyCon]
isTrue = Translation -> [TyCon]
isTrue Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
isTrue Translation
r
      , assertTy :: [TyCon]
assertTy = Translation -> [TyCon]
assertTy Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
assertTy Translation
r
      , voids :: [TyCon]
voids = Translation -> [TyCon]
voids Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
voids Translation
r
      , tyEq :: [TyCon]
tyEq = Translation -> [TyCon]
tyEq Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyEq Translation
r
      , tyNot :: [TyCon]
tyNot = Translation -> [TyCon]
tyNot Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyNot Translation
r
      , tyAnd :: [TyCon]
tyAnd = Translation -> [TyCon]
tyAnd Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyAnd Translation
r
      , tyOr :: [TyCon]
tyOr = Translation -> [TyCon]
tyOr Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyOr Translation
r
      , tyIf :: [TyCon]
tyIf = Translation -> [TyCon]
tyIf Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyIf Translation
r
      , tyEqBool :: [TyCon]
tyEqBool = Translation -> [TyCon]
tyEqBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyEqBool Translation
r
      , tyEqWitness :: [TyCon]
tyEqWitness = Translation -> [TyCon]
tyEqWitness Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyEqWitness Translation
r
      , tyNeqBool :: [TyCon]
tyNeqBool = Translation -> [TyCon]
tyNeqBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyNeqBool Translation
r
      , natPlus :: [TyCon]
natPlus = Translation -> [TyCon]
natPlus Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natPlus Translation
r
      , natMinus :: [TyCon]
natMinus = Translation -> [TyCon]
natMinus Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natMinus Translation
r
      , natTimes :: [TyCon]
natTimes = Translation -> [TyCon]
natTimes Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natTimes Translation
r
      , natExp :: [TyCon]
natExp = Translation -> [TyCon]
natExp Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natExp Translation
r
      , natLeq :: [TyCon]
natLeq = Translation -> [TyCon]
natLeq Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natLeq Translation
r
      , natGeq :: [TyCon]
natGeq = Translation -> [TyCon]
natGeq Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natGeq Translation
r
      , natLt :: [TyCon]
natLt = Translation -> [TyCon]
natLt Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natLt Translation
r
      , natGt :: [TyCon]
natGt = Translation -> [TyCon]
natGt Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natGt Translation
r
      , natLeqBool :: [TyCon]
natLeqBool = Translation -> [TyCon]
natLeqBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natLeqBool Translation
r
      , natGeqBool :: [TyCon]
natGeqBool = Translation -> [TyCon]
natGeqBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natGeqBool Translation
r
      , natLtBool :: [TyCon]
natLtBool = Translation -> [TyCon]
natLtBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natLtBool Translation
r
      , natGtBool :: [TyCon]
natGtBool = Translation -> [TyCon]
natGtBool Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natGtBool Translation
r
      , orderingLT :: [TyCon]
orderingLT = Translation -> [TyCon]
orderingLT Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
orderingLT Translation
r
      , orderingGT :: [TyCon]
orderingGT = Translation -> [TyCon]
orderingGT Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
orderingGT Translation
r
      , orderingEQ :: [TyCon]
orderingEQ = Translation -> [TyCon]
orderingEQ Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
orderingEQ Translation
r
      , natCompare :: [TyCon]
natCompare = Translation -> [TyCon]
natCompare Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natCompare Translation
r
      , trueData :: [TyCon]
trueData = Translation -> [TyCon]
trueData Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
trueData Translation
r
      , falseData :: [TyCon]
falseData = Translation -> [TyCon]
falseData Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
falseData Translation
r
      , parsePred :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred = \TcPredType -> Machine Expr
f TcPredType
ty -> Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred Translation
l TcPredType -> Machine Expr
f TcPredType
ty forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred Translation
r TcPredType -> Machine Expr
f TcPredType
ty
      , parseExpr :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr = \TcPredType -> Machine Expr
toE -> forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr Translation
l TcPredType -> Machine Expr
toE forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr Translation
r TcPredType -> Machine Expr
toE
      , natMin :: [TyCon]
natMin = Translation -> [TyCon]
natMin Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natMin Translation
r
      , natMax :: [TyCon]
natMax = Translation -> [TyCon]
natMax Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natMax Translation
r
      , ordCond :: [TyCon]
ordCond = Translation -> [TyCon]
ordCond Translation
l forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
ordCond Translation
r
      }

instance Monoid Translation where
  mempty :: Translation
mempty =
    Translation
      { isEmpty :: [TyCon]
isEmpty = forall a. Monoid a => a
mempty
      , isTrue :: [TyCon]
isTrue = forall a. Monoid a => a
mempty
      , assertTy :: [TyCon]
assertTy = forall a. Monoid a => a
mempty
      , tyEq :: [TyCon]
tyEq = forall a. Monoid a => a
mempty
      , tyEqBool :: [TyCon]
tyEqBool = forall a. Monoid a => a
mempty
      , tyEqWitness :: [TyCon]
tyEqWitness = forall a. Monoid a => a
mempty
      , tyNeqBool :: [TyCon]
tyNeqBool = forall a. Monoid a => a
mempty
      , tyNot :: [TyCon]
tyNot = forall a. Monoid a => a
mempty
      , tyAnd :: [TyCon]
tyAnd = forall a. Monoid a => a
mempty
      , tyOr :: [TyCon]
tyOr = forall a. Monoid a => a
mempty
      , tyIf :: [TyCon]
tyIf = forall a. Monoid a => a
mempty
      , voids :: [TyCon]
voids = forall a. Monoid a => a
mempty
      , natPlus :: [TyCon]
natPlus = forall a. Monoid a => a
mempty
      , natMinus :: [TyCon]
natMinus = forall a. Monoid a => a
mempty
      , natTimes :: [TyCon]
natTimes = forall a. Monoid a => a
mempty
      , natExp :: [TyCon]
natExp = forall a. Monoid a => a
mempty
      , natLeq :: [TyCon]
natLeq = forall a. Monoid a => a
mempty
      , natGeq :: [TyCon]
natGeq = forall a. Monoid a => a
mempty
      , natLt :: [TyCon]
natLt = forall a. Monoid a => a
mempty
      , natGt :: [TyCon]
natGt = forall a. Monoid a => a
mempty
      , natLeqBool :: [TyCon]
natLeqBool = forall a. Monoid a => a
mempty
      , natGeqBool :: [TyCon]
natGeqBool = forall a. Monoid a => a
mempty
      , natLtBool :: [TyCon]
natLtBool = forall a. Monoid a => a
mempty
      , natGtBool :: [TyCon]
natGtBool = forall a. Monoid a => a
mempty
      , orderingLT :: [TyCon]
orderingLT = forall a. Monoid a => a
mempty
      , orderingGT :: [TyCon]
orderingGT = forall a. Monoid a => a
mempty
      , orderingEQ :: [TyCon]
orderingEQ = forall a. Monoid a => a
mempty
      , natCompare :: [TyCon]
natCompare = forall a. Monoid a => a
mempty
      , trueData :: [TyCon]
trueData = []
      , falseData :: [TyCon]
falseData = []
      , parsePred :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero
      , parseExpr :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const forall (m :: * -> *) a. MonadPlus m => m a
mzero
      , natMin :: [TyCon]
natMin = forall a. Monoid a => a
mempty
      , natMax :: [TyCon]
natMax = forall a. Monoid a => a
mempty
      , ordCond :: [TyCon]
ordCond = forall a. Monoid a => a
mempty
      }

decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
decidePresburger :: PluginMode -> TcPluginM Translation -> () -> TcPluginSolver
decidePresburger PluginMode
_ TcPluginM Translation
genTrans ()
_ [Ct]
gs [] [] = do
  CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Started givens with: " (forall a. Outputable a => a -> SDoc
ppr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (CtEvidence -> TcPredType
ctEvPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
gs)
  Translation
trans <- TcPluginM Translation
genTrans
  forall a r. a -> (Given a => r) -> r
give Translation
trans forall a b. (a -> b) -> a -> b
$ do
    [Maybe (Ct, Prop)]
ngs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Ct
a -> forall a. Machine a -> TcPluginM (Maybe a)
runMachine forall a b. (a -> b) -> a -> b
$ (,) Ct
a forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred (Ct -> TcPredType
deconsPred Ct
a)) [Ct]
gs
    let givens :: [(Ct, Prop)]
givens = forall a. [Maybe a] -> [a]
catMaybes [Maybe (Ct, Prop)]
ngs
        prems0 :: [Prop]
prems0 = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Ct, Prop)]
givens
        prems :: PropSet
prems = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert' PropSet
noProps [Prop]
prems0
    if forall a. Maybe a -> Bool
isNothing (PropSet -> Maybe [(Int, Integer)]
checkSat PropSet
prems)
      then forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginSolveResult
TcPluginContradiction [Ct]
gs
      else forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [] []
decidePresburger PluginMode
mode TcPluginM Translation
genTrans ()
_ [Ct]
gs [Ct]
_ds [Ct]
ws = do
  Translation
trans <- TcPluginM Translation
genTrans
  forall a r. a -> (Given a => r) -> r
give Translation
trans forall a b. (a -> b) -> a -> b
$ do
    [Ct]
gs' <- [Ct] -> TcPluginM [Ct]
normaliseGivens [Ct]
gs
    let subst :: Substitution
subst = [Ct] -> Substitution
mkSubstitution [Ct]
gs'
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Current subst" (forall a. Outputable a => a -> SDoc
ppr Substitution
subst)
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: wanteds" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TcPredType -> TcPredType
subsType Substitution
subst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPredType
deconsPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> Ct -> Ct
subsCt Substitution
subst) [Ct]
ws
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: givens" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TcPredType -> TcPredType
subsType Substitution
subst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPredType
deconsPred) [Ct]
gs
    (PropSet
prems, [(Ct, Prop)]
wants, [Prop]
prems0) <- do
      [(Ct, Prop)]
wants <-
        forall a. [Maybe a] -> [a]
catMaybes
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
            ( \Ct
ct ->
                forall a. Machine a -> TcPluginM (Maybe a)
runMachine forall a b. (a -> b) -> a -> b
$
                  (,) Ct
ct
                    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred
                      ( Substitution -> TcPredType -> TcPredType
subsType Substitution
subst forall a b. (a -> b) -> a -> b
$
                          Ct -> TcPredType
deconsPred forall a b. (a -> b) -> a -> b
$ Substitution -> Ct -> Ct
subsCt Substitution
subst Ct
ct
                      )
            )
            (forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
ws)

      [Maybe Prop]
resls <-
        forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
          (forall a. Machine a -> TcPluginM (Maybe a)
runMachine forall b c a. (b -> c) -> (a -> b) -> a -> c
. Given Translation => TcPredType -> Machine Prop
toPresburgerPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> TcPredType -> TcPredType
subsType Substitution
subst forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPredType
deconsPred)
          [Ct]
gs
      let prems :: PropSet
prems = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert' PropSet
noProps forall a b. (a -> b) -> a -> b
$ forall a. [Maybe a] -> [a]
catMaybes [Maybe Prop]
resls
      forall (m :: * -> *) a. Monad m => a -> m a
return (PropSet
prems, forall a b. (a -> b) -> [a] -> [b]
map (forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second forall a b. (a -> b) -> a -> b
$ PluginMode -> Prop -> Prop
handleSubtraction PluginMode
mode) [(Ct, Prop)]
wants, forall a. [Maybe a] -> [a]
catMaybes [Maybe Prop]
resls)
    let solved :: [Ct]
solved = forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall a. (a -> Bool) -> [a] -> [a]
filter (Proof -> Bool
isProved forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSet -> Prop -> Proof
testIf PropSet
prems forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Ct, Prop)]
wants
        coerced :: [(EvTerm, Ct)]
coerced =
          [ (EvTerm
evProof, Ct
ct)
          | Ct
ct <- [Ct]
solved
          , Just EvTerm
evProof <- forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Given Translation => PredTree -> Maybe EvTerm
extractProof forall a b. (a -> b) -> a -> b
$ TcPredType -> PredTree
classifyPredType forall a b. (a -> b) -> a -> b
$ Ct -> TcPredType
deconsPred Ct
ct
          ]
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: final premises" (CommandLineOption -> SDoc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> CommandLineOption
show [Prop]
prems0)
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: final goals" (CommandLineOption -> SDoc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> CommandLineOption
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Ct, Prop)]
wants)
    case PropSet -> Prop -> Proof
testIf PropSet
prems (forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Prop -> Prop -> Prop
(:&&) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Prop
PTrue [(Ct, Prop)]
wants) of
      Proof
Proved -> do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Proved" (CommandLineOption -> SDoc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> CommandLineOption
show forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Ct, Prop)]
wants)
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: ... with coercions" (forall a. Outputable a => a -> SDoc
ppr [(EvTerm, Ct)]
coerced)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginSolveResult
TcPluginOk [(EvTerm, Ct)]
coerced []
      Disproved [(Int, Integer)]
wit -> do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Failed! " (CommandLineOption -> SDoc
text forall a b. (a -> b) -> a -> b
$ forall a. Show a => a -> CommandLineOption
show [(Int, Integer)]
wit)
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginSolveResult
TcPluginContradiction forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Ct, Prop)]
wants


extractProof :: Given Translation => PredTree -> Maybe EvTerm
extractProof :: Given Translation => PredTree -> Maybe EvTerm
extractProof (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) = 
    forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ CommandLineOption -> TcPredType -> TcPredType -> EvTerm
evByFiat CommandLineOption
"ghc-typelits-presburger" TcPredType
t1 TcPredType
t2
#if MIN_VERSION_base(4,17,0)
extractProof (IrredPred prd)
  | Just (con, lastN 2 -> [_, _]) <- splitTyConApp_maybe prd
  , con `elem` assertTy given = 
    Just $ GHC.Var (dataConWrapId $ cTupleDataCon 0) `evCast`
      mkUnivCo
      (PluginProv $ "ghc-typelits-presburger: extractProof")
      Representational
      (mkTyConTy (cTupleTyCon 0))
      prd
#endif
extractProof PredTree
_ = forall a. Maybe a
Nothing

eqReasoning :: FastString
eqReasoning :: FastString
eqReasoning = CommandLineOption -> FastString
fsLit CommandLineOption
"equational-reasoning"

defaultTranslation :: TcPluginM Translation
defaultTranslation :: TcPluginM Translation
defaultTranslation = do
  [FastString]
packs <- TcPluginM [FastString]
preloadedUnitsM
  let eqThere :: Bool
eqThere = forall a. a -> Maybe a -> a
fromMaybe Bool
False forall a b. (a -> b) -> a -> b
$
        forall a. [a] -> Maybe a
listToMaybe forall a b. (a -> b) -> a -> b
$ do
          FastString
pname <- [FastString]
packs
          CommandLineOption
rest <-
            forall a. Maybe a -> [a]
maybeToList forall a b. (a -> b) -> a -> b
$
              forall a. Eq a => [a] -> [a] -> Maybe [a]
L.stripPrefix CommandLineOption
"equational-reasoning-" forall a b. (a -> b) -> a -> b
$ FastString -> CommandLineOption
unpackFS FastString
pname
          forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> Bool
null CommandLineOption
rest Bool -> Bool -> Bool
|| Char -> Bool
isDigit (forall a. [a] -> a
head CommandLineOption
rest)
  ([TyCon]
isEmpties, [TyCon]
isTrues) <-
    if Bool
eqThere
      then do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: equational-reasoning activated!" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr ()
        Module
emd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"Proof.Propositional.Empty") FastString
eqReasoning
        Module
pmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"Proof.Propositional") FastString
eqReasoning

        TyCon
emptyClsTyCon <- Class -> TyCon
classTyCon forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> TcPluginM Class
tcLookupClass forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
emd (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"Empty"))
        TyCon
isTrueCon_ <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
pmd (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"IsTrue")
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TyCon
emptyClsTyCon], [TyCon
isTrueCon_])
      else do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: No equational-reasoning found." forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr ()
        forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])

  TyCon
eqTyCon_ <- TcPluginM TyCon
getEqTyCon
  TyCon
eqBoolTyCon <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
dATA_TYPE_EQUALITY (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"==")
  TyCon
eqWitCon_ <- TcPluginM TyCon
getEqWitnessTyCon
  Maybe TyCon
assertTy <- TcPluginM (Maybe TyCon)
lookupAssertTyCon
  Module
vmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (CommandLineOption -> ModuleName
mkModuleName CommandLineOption
"Data.Void") (CommandLineOption -> FastString
fsLit CommandLineOption
"base")
  TyCon
voidTyCon <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
vmd (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"Void")
  TyCon
nLeq <- Name -> TcPluginM TyCon
tcLookupTyCon forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TcPluginM Name
lookupTyNatPredLeq
  TyCon
tyLeqB <- TcPluginM TyCon
lookupTyNatBoolLeq
  Maybe TyCon
mTyLtP <- TcPluginM (Maybe TyCon)
lookupTyNatPredLt
  Maybe TyCon
mTyLtB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolLt
  Maybe TyCon
mTyGeqP <- TcPluginM (Maybe TyCon)
lookupTyNatPredGeq
  Maybe TyCon
mTyGeqB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolGeq
  Maybe TyCon
mTyGtP <- TcPluginM (Maybe TyCon)
lookupTyNatPredGt
  Maybe TyCon
mTyGtB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolGt
  Maybe TyCon
mOrdCond <- TcPluginM (Maybe TyCon)
mOrdCondTyCon
  Maybe TyCon
mtyGenericCompare <- TcPluginM (Maybe TyCon)
lookupTyGenericCompare
  [TyCon]
tyNot <- forall a. Maybe a -> [a]
maybeToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyNot
  [TyCon]
tyAnd <- forall a. Maybe a -> [a]
maybeToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyAnd
  [TyCon]
tyOr <- forall a. Maybe a -> [a]
maybeToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyOr
  [TyCon]
tyIf <- forall a. Maybe a -> [a]
maybeToList forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyIf
  let trans :: Translation
trans =
        forall a. Monoid a => a
mempty
          { isEmpty :: [TyCon]
isEmpty = [TyCon]
isEmpties
          , assertTy :: [TyCon]
assertTy = forall a. Maybe a -> [a]
maybeToList Maybe TyCon
assertTy
          , tyEq :: [TyCon]
tyEq = [TyCon
eqTyCon_]
          , [TyCon]
tyNot :: [TyCon]
tyNot :: [TyCon]
tyNot
          , [TyCon]
tyAnd :: [TyCon]
tyAnd :: [TyCon]
tyAnd
          , [TyCon]
tyOr :: [TyCon]
tyOr :: [TyCon]
tyOr
          , [TyCon]
tyIf :: [TyCon]
tyIf :: [TyCon]
tyIf
          , ordCond :: [TyCon]
ordCond = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mOrdCond
          , tyEqWitness :: [TyCon]
tyEqWitness = [TyCon
eqWitCon_]
          , tyEqBool :: [TyCon]
tyEqBool = [TyCon
eqBoolTyCon]
          , isTrue :: [TyCon]
isTrue = [TyCon]
isTrues
          , voids :: [TyCon]
voids = [TyCon
voidTyCon]
          , natMinus :: [TyCon]
natMinus = [TyCon
typeNatSubTyCon]
          , natPlus :: [TyCon]
natPlus = [TyCon
typeNatAddTyCon]
          , natTimes :: [TyCon]
natTimes = [TyCon
typeNatMulTyCon]
          , natExp :: [TyCon]
natExp = [TyCon
typeNatExpTyCon]
          , falseData :: [TyCon]
falseData = [TyCon
promotedFalseDataCon]
          , trueData :: [TyCon]
trueData = [TyCon
promotedTrueDataCon]
          , natLeqBool :: [TyCon]
natLeqBool = [TyCon
tyLeqB]
          , natLeq :: [TyCon]
natLeq = [TyCon
nLeq]
          , natGeqBool :: [TyCon]
natGeqBool = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGeqB
          , natGeq :: [TyCon]
natGeq = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGeqP
          , natGtBool :: [TyCon]
natGtBool = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGtB
          , natGt :: [TyCon]
natGt = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGtP
          , natLtBool :: [TyCon]
natLtBool = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyLtB
          , natLt :: [TyCon]
natLt = forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyLtP
          , natCompare :: [TyCon]
natCompare = TyCon
typeNatCmpTyCon forall a. a -> [a] -> [a]
: forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mtyGenericCompare
          , orderingEQ :: [TyCon]
orderingEQ = [TyCon
promotedEQDataCon]
          , orderingLT :: [TyCon]
orderingLT = [TyCon
promotedLTDataCon]
          , orderingGT :: [TyCon]
orderingGT = [TyCon
promotedGTDataCon]
          }
  CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"Final translation: " (forall a. Outputable a => a -> SDoc
ppr Maybe TyCon
mTyGeqB)
  forall (f :: * -> *) a. Applicative f => a -> f a
pure Translation
trans

(<=>) :: Prop -> Prop -> Prop
Prop
p <=> :: Prop -> Prop -> Prop
<=> Prop
q = (Prop
p Prop -> Prop -> Prop
:&& Prop
q) Prop -> Prop -> Prop
:|| (Prop -> Prop
Not Prop
p Prop -> Prop -> Prop
:&& Prop -> Prop
Not Prop
q)

orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic =
  [(TyCon
lt, Expr -> Expr -> Prop
(:<)) | TyCon
lt <- Translation -> [TyCon]
orderingLT forall a. Given a => a
given]
  forall a. [a] -> [a] -> [a]
++ [(TyCon
eq, Expr -> Expr -> Prop
(:==)) | TyCon
eq <- Translation -> [TyCon]
orderingEQ forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
gt, Expr -> Expr -> Prop
(:>)) | TyCon
gt <- Translation -> [TyCon]
orderingGT forall a. Given a => a
given]

deconsPred :: Ct -> Type
deconsPred :: Ct -> TcPredType
deconsPred = CtEvidence -> TcPredType
ctEvPred forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence

toPresburgerPred :: Given Translation => Type -> Machine Prop
toPresburgerPred :: Given Translation => TcPredType -> Machine Prop
toPresburgerPred (TyConApp TyCon
con (forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
t1, TcPredType
t2]))
  | TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Translation -> [TyCon]
natLeq forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natLeqBool forall a. Given a => a
given) =
    Expr -> Expr -> Prop
(:<=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPred (TyConApp TyCon
con [TcPredType
t1, TcPredType
_])
  | TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
assertTy forall a. Given a => a
given = Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
t1
toPresburgerPred TcPredType
ty
  | Just (TyCon
con, []) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
trueData forall a. Given a => a
given =
    forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
  | Just (TyCon
con, []) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
falseData forall a. Given a => a
given =
    forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PFalse
  | cls :: PredTree
cls@(EqPred EqRel
NomEq TcPredType
_ TcPredType
_) <- TcPredType -> PredTree
classifyPredType TcPredType
ty =
    Given Translation => PredTree -> Machine Prop
toPresburgerPredTree PredTree
cls
  | TcPredType -> Bool
isEqPred TcPredType
ty = Given Translation => PredTree -> Machine Prop
toPresburgerPredTree forall a b. (a -> b) -> a -> b
$ TcPredType -> PredTree
classifyPredType TcPredType
ty
  | Just (TyCon
con, [TcPredType
l, TcPredType
r]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
ty -- l ~ r
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Translation -> [TyCon]
tyEq forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
tyEqBool forall a. Given a => a
given) =
    Given Translation => PredTree -> Machine Prop
toPresburgerPredTree forall a b. (a -> b) -> a -> b
$ EqRel -> TcPredType -> TcPredType -> PredTree
EqPred EqRel
NomEq TcPredType
l TcPredType
r
  | Just (TyCon
con, [TcPredType
_k, TcPredType
l, TcPredType
r]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- l (:~: {k}) r
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyEqWitness forall a. Given a => a
given =
    Given Translation => PredTree -> Machine Prop
toPresburgerPredTree forall a b. (a -> b) -> a -> b
$ EqRel -> TcPredType -> TcPredType -> PredTree
EqPred EqRel
NomEq TcPredType
l TcPredType
r
  | Just (TyCon
con, [TcPredType
l]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- Empty l => ...
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
isEmpty forall a. Given a => a
given =
    Prop -> Prop
Not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- IsTrue l =>
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
isTrue forall a. Given a => a
given =
    Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- Not p (from Data.Type.Bool)
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyNot forall a. Given a => a
given =
    Prop -> Prop
Not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l, TcPredType
r]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- p && q (from Data.Type.Bool)
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyAnd forall a. Given a => a
given =
    Prop -> Prop -> Prop
(:&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
r
  | Just (TyCon
con, [TcPredType
l, TcPredType
r]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- p || q (from Data.Type.Bool)
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyOr forall a. Given a => a
given =
    Prop -> Prop -> Prop
(:||) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
r
  | Just (TyCon
con, forall a. Int -> [a] -> [a]
lastN Int
3 -> [TcPredType
p, TcPredType
t, TcPredType
f]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- If p t f (from Data.Type.Bool)
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyIf forall a. Given a => a
given = do
    Prop
p' <- Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
    Prop -> Prop -> Prop
(:||) 
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Prop
p' Prop -> Prop -> Prop
:&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
t) 
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Prop -> Prop
Not Prop
p'Prop -> Prop -> Prop
:&&) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
f)
  | Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
ty
    , HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
t1 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind
    , HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
t2 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind 
    , Just Expr -> Expr -> Prop
p <- forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic =
      Expr -> Expr -> Prop
p forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
  | Just DataCond{TcPredType
CondCases
condCases :: DataCond -> CondCases
rhs :: DataCond -> TcPredType
lhs :: DataCond -> TcPredType
condCases :: CondCases
rhs :: TcPredType
lhs :: TcPredType
..} <- Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
ty = do -- OrdCond
      CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
  | Bool
otherwise = Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred forall a. Given a => a
given Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty

splitTyConAppLastBin :: Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin :: TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t = do
  (TyCon
con, [TcPredType]
ts) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
t
  let !n :: Int
n = forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcPredType]
ts
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ Int
n forall a. Ord a => a -> a -> Bool
>= Int
2
  forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon
con, forall a. Int -> [a] -> [a]
drop (Int
n forall a. Num a => a -> a -> a
- Int
2) [TcPredType]
ts)

data DataCond = DataCond { DataCond -> TcPredType
lhs, DataCond -> TcPredType
rhs :: Type, DataCond -> CondCases
condCases :: CondCases }

data CondCases = CondCases { CondCases -> Bool
ltCase, CondCases -> Bool
eqCase, CondCases -> Bool
gtCase :: Bool }
  deriving (Int -> CondCases -> ShowS
[CondCases] -> ShowS
CondCases -> CommandLineOption
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
showList :: [CondCases] -> ShowS
$cshowList :: [CondCases] -> ShowS
show :: CondCases -> CommandLineOption
$cshow :: CondCases -> CommandLineOption
showsPrec :: Int -> CondCases -> ShowS
$cshowsPrec :: Int -> CondCases -> ShowS
Show, CondCases -> CondCases -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CondCases -> CondCases -> Bool
$c/= :: CondCases -> CondCases -> Bool
== :: CondCases -> CondCases -> Bool
$c== :: CondCases -> CondCases -> Bool
Eq, Eq CondCases
CondCases -> CondCases -> Bool
CondCases -> CondCases -> Ordering
CondCases -> CondCases -> CondCases
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CondCases -> CondCases -> CondCases
$cmin :: CondCases -> CondCases -> CondCases
max :: CondCases -> CondCases -> CondCases
$cmax :: CondCases -> CondCases -> CondCases
>= :: CondCases -> CondCases -> Bool
$c>= :: CondCases -> CondCases -> Bool
> :: CondCases -> CondCases -> Bool
$c> :: CondCases -> CondCases -> Bool
<= :: CondCases -> CondCases -> Bool
$c<= :: CondCases -> CondCases -> Bool
< :: CondCases -> CondCases -> Bool
$c< :: CondCases -> CondCases -> Bool
compare :: CondCases -> CondCases -> Ordering
$ccompare :: CondCases -> CondCases -> Ordering
Ord)

fromCondCases :: CondCases -> Expr -> Expr -> Prop
fromCondCases :: CondCases -> Expr -> Expr -> Prop
fromCondCases (CondCases Bool
True Bool
False Bool
False) = Expr -> Expr -> Prop
(:<)
fromCondCases (CondCases Bool
False Bool
True Bool
False) = Expr -> Expr -> Prop
(:==)
fromCondCases (CondCases Bool
False Bool
False Bool
True) = Expr -> Expr -> Prop
(:>)
fromCondCases (CondCases Bool
True Bool
True Bool
False) = Expr -> Expr -> Prop
(:<=)
fromCondCases (CondCases Bool
True Bool
False Bool
True) = Expr -> Expr -> Prop
(:/=)
fromCondCases (CondCases Bool
True Bool
True Bool
True) = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Prop
PTrue
fromCondCases (CondCases Bool
False Bool
True Bool
True) = Expr -> Expr -> Prop
(:>=)
fromCondCases (CondCases Bool
False Bool
False Bool
False) = forall a b. a -> b -> a
const forall a b. (a -> b) -> a -> b
$ forall a b. a -> b -> a
const Prop
PFalse

parseOrdCond :: Given Translation => Type -> Maybe DataCond
parseOrdCond :: Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
ty = do
  (TyCon
con, forall a. Int -> [a] -> [a]
lastN Int
4 -> [TcPredType
cmp, TcPredType
ltTy, TcPredType
eqTy, TcPredType
gtTy]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
ordCond forall a. Given a => a
given
  (TyCon
cmpCon, forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
lhs, TcPredType
rhs]) <- HasDebugCallStack => TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe  TcPredType
cmp
  forall (f :: * -> *). Alternative f => Bool -> f ()
guard forall a b. (a -> b) -> a -> b
$ TyCon
cmpCon forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given
  Bool
ltCase <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
ltTy
  Bool
eqCase <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
eqTy
  Bool
gtCase <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
gtTy
  let  condCases :: CondCases
condCases = CondCases{Bool
gtCase :: Bool
eqCase :: Bool
ltCase :: Bool
gtCase :: Bool
eqCase :: Bool
ltCase :: Bool
..}
  forall (f :: * -> *) a. Applicative f => a -> f a
pure DataCond{TcPredType
CondCases
condCases :: CondCases
rhs :: TcPredType
lhs :: TcPredType
condCases :: CondCases
rhs :: TcPredType
lhs :: TcPredType
..}

decodeTyBool :: Type -> Maybe Bool
decodeTyBool :: TcPredType -> Maybe Bool
decodeTyBool TcPredType
ty = do
  TyCon
con <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
ty
  (Bool
True forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
con forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon))
    forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Bool
False forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
con forall a. Eq a => a -> a -> Bool
== TyCon
promotedFalseDataCon))


toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop
toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
false) -- P ~ 'False <=> Not P ~ 'True
  | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
falseData forall a. Given a => a
given) forall a b. (a -> b) -> a -> b
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
false =
    Prop -> Prop
Not forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) -- (n :<=? m) ~ 'b
  | Just Bool
isTrue <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
b
    , Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
p
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natLeqBool forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:<=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else Expr -> Expr -> Prop
(:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) -- (n :<? m) ~ b
  | Just Bool
isTrue <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
b
    , Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
p
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natLtBool forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else Expr -> Expr -> Prop
(:>=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) -- (n :>? m) ~ b
  | Just Bool
isTrue <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
b
    , Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
p
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natGtBool forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else Expr -> Expr -> Prop
(:<=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) -- (n :>=? m) ~ b
  | Just Bool
isTrue <- TcPredType -> Maybe Bool
decodeTyBool TcPredType
b
    , Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
p
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natGeqBool forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:>=) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else Expr -> Expr -> Prop
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) 
  | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
trueData forall a. Given a => a
given) forall a b. (a -> b) -> a -> b
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
b =
    Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
b TcPredType
p) 
  | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
trueData forall a. Given a => a
given) forall a b. (a -> b) -> a -> b
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
b =
    Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
q) -- (p :: Bool) ~ (q :: Bool)
  | HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
p TcPredType -> TcPredType -> Bool
`eqType` TyCon -> TcPredType
mkTyConTy TyCon
promotedBoolTyCon = 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
$ CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: EQBOOL:" forall a b. (a -> b) -> a -> b
$ forall a. Outputable a => a -> SDoc
ppr (TcPredType
p, TcPredType
q)
    Prop -> Prop -> Prop
(<=>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
q
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
n TcPredType
m) -- (n :: Nat) ~ (m :: Nat)
  | HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
n TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind =
    Expr -> Expr -> Prop
(:==) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
toPresburgerPredTree (EqPred EqRel
_ TcPredType
t1 TcPredType
t2) -- CmpNat a b ~ CmpNat c d
  | Just (TyCon
con, forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t1
    , Just (TyCon
con', forall a. [a] -> [a]
lastTwo -> [TcPredType
c, TcPredType
d]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t2
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given
    , TyCon
con' forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given =
    Prop -> Prop -> Prop
(<=>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Expr -> Prop
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
b)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> Expr -> Prop
(:<) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
c forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
d)
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) -- CmpNat a b ~ x
  | Just (TyCon
con, forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t1
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given
    , Just TyCon
cmp <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
t2 =
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
cmp Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
b
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) -- x ~ CmpNat a b
  | Just (TyCon
con, forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t2
    , TyCon
con forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given
    , Just TyCon
cmp <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
t1 =
    forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
cmp Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic)
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
b
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
cond TcPredType
p) 
  -- OrdCond (CmpNat _ _) lt eq gt ~ ? (for GHC >= 9.2)
  | Just DataCond{TcPredType
CondCases
condCases :: CondCases
rhs :: TcPredType
lhs :: TcPredType
condCases :: DataCond -> CondCases
rhs :: DataCond -> TcPredType
lhs :: DataCond -> TcPredType
..} <- Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
cond = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p) 
      (\Bool
q -> if Bool
q then forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      forall a b. (a -> b) -> a -> b
$ TcPredType -> Maybe Bool
decodeTyBool TcPredType
p
  -- ? ~ OrdCond (CmpNat _ _) lt eq gt  (for GHC >= 9.2)
  | Just DataCond{TcPredType
CondCases
condCases :: CondCases
rhs :: TcPredType
lhs :: TcPredType
condCases :: DataCond -> CondCases
rhs :: DataCond -> TcPredType
lhs :: DataCond -> TcPredType
..} <- Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
p = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
    forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
cond) 
      (\Bool
q -> if Bool
q then forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      forall a b. (a -> b) -> a -> b
$ TcPredType -> Maybe Bool
decodeTyBool TcPredType
cond
toPresburgerPredTree (ClassPred Class
con [TcPredType]
ts)
  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)
  | [TcPredType
t1, TcPredType
t2] <- forall a. Int -> [a] -> [a]
lastN Int
2 [TcPredType]
ts
    , HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
t1 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind
    , HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
t2 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind =
    let p :: Maybe (Expr -> Expr -> Prop)
p = forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Class -> TyCon
classTyCon Class
con) Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic
     in forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Expr -> Expr -> Prop)
p) forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree PredTree
_ = forall (m :: * -> *) a. MonadPlus m => m a
mzero

binPropDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic :: Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic =
  [(TyCon
n, Expr -> Expr -> Prop
(:<)) | TyCon
n <- Translation -> [TyCon]
natLt forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natLtBool forall a. Given a => a
given]
  forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:>)) | TyCon
n <- Translation -> [TyCon]
natGt forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natGtBool forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:<=)) | TyCon
n <- Translation -> [TyCon]
natLeq forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natLeqBool forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:>=)) | TyCon
n <- Translation -> [TyCon]
natGeq forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natGeqBool forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:==)) | TyCon
n <- Translation -> [TyCon]
tyEq forall a. Given a => a
given forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
tyEqBool forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:/=)) | TyCon
n <- Translation -> [TyCon]
tyNeqBool forall a. Given a => a
given]
    forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:==)) | TyCon
n <- Translation -> [TyCon]
tyEqBool forall a. Given a => a
given]

toPresburgerExp :: Given Translation => Type -> Machine Expr
toPresburgerExp :: Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty = case TcPredType
ty of
  TyVarTy TcTyVar
t -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Name -> Expr
Var forall a b. (a -> b) -> a -> b
$ Int -> Name
toName forall a b. (a -> b) -> a -> b
$ Unique -> Int
getKey forall a b. (a -> b) -> a -> b
$ forall a. Uniquable a => a -> Unique
getUnique TcTyVar
t
  TyConApp TyCon
tc (forall a. Int -> [a] -> [a]
lastN Int
3 -> [TcPredType
p, TcPredType
t, TcPredType
f])
    | TyCon
tc forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyIf forall a. Given a => a
given ->
      Prop -> Expr -> Expr -> Expr
If forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
f 
  TyConApp TyCon
tc (forall a. Int -> [a] -> [a]
lastN Int
4 -> [TcPredType
cmpNM, TcPredType
l, TcPredType
e, TcPredType
g])
    | TyCon
tc forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
ordCond forall a. Given a => a
given
    , TyConApp TyCon
cmp (forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
n, TcPredType
m]) <- TcPredType
cmpNM
    , TyCon
cmp forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare forall a. Given a => a
given
    , forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TcPredType -> TypeEq
TypeEq TcPredType
n, TcPredType -> TypeEq
TypeEq TcPredType
m]) forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPredType -> TypeEq
TypeEq) [TcPredType
l,TcPredType
e,TcPredType
g]
    -> Given Translation =>
TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> Machine Expr
decodeMinMax TcPredType
n TcPredType
m TcPredType
l TcPredType
e TcPredType
g
  t :: TcPredType
t@(TyConApp TyCon
tc [TcPredType]
ts) ->
    Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr forall a. Given a => a
given Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon -> [TcPredType] -> Machine Expr
body TyCon
tc [TcPredType]
ts
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Uniquable a => a -> Unique
getUnique forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine TcTyVar
toVar TcPredType
t
  LitTy (NumTyLit Integer
n) -> forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Expr
K Integer
n)
  LitTy TyLit
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
  TcPredType
t ->
    Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr forall a. Given a => a
given Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty
      forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Uniquable a => a -> Unique
getUnique forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine TcTyVar
toVar TcPredType
t
  where
    body :: TyCon -> [TcPredType] -> Machine Expr
body TyCon
tc [TcPredType]
ts =
      let step :: TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> b
op
            | TyCon
tc forall a. Eq a => a -> a -> Bool
== TyCon
con
              , [TcPredType
tl, TcPredType
tr] <- forall a. [a] -> [a]
lastTwo [TcPredType]
ts =
              Expr -> Expr -> b
op forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
tl forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
tr
            | Bool
otherwise = forall (m :: * -> *) a. MonadPlus m => m a
mzero
       in case [TcPredType]
ts of
            [TcPredType
tl, TcPredType
tr] | TyCon
tc forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natTimes forall a. Given a => a
given ->
              case (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
tl, Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
tr) of
                (LitTy (NumTyLit Integer
n), LitTy (NumTyLit Integer
m)) -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Integer -> Expr
K forall a b. (a -> b) -> a -> b
$ Integer
n forall a. Num a => a -> a -> a
* Integer
m
                (LitTy (NumTyLit Integer
n), TcPredType
x) -> Integer -> Expr -> Expr
(:*) Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
x
                (TcPredType
x, LitTy (NumTyLit Integer
n)) -> Integer -> Expr -> Expr
(:*) Integer
n forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
x
                (TcPredType, TcPredType)
_ -> forall (m :: * -> *) a. MonadPlus m => m a
mzero
            [TcPredType]
_ ->
              forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum forall a b. (a -> b) -> a -> b
$
                [ forall {b}.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
(:+)
                | TyCon
con <- Translation -> [TyCon]
natPlus forall a. Given a => a
given
                ]
                  forall a. [a] -> [a] -> [a]
++ [ forall {b}.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
(:-)
                     | TyCon
con <- Translation -> [TyCon]
natMinus forall a. Given a => a
given
                     ]
                  forall a. [a] -> [a] -> [a]
++ [ forall {b}.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
Min
                     | TyCon
con <- Translation -> [TyCon]
natMin forall a. Given a => a
given
                     ]
                  forall a. [a] -> [a] -> [a]
++ [ forall {b}.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
Max
                     | TyCon
con <- Translation -> [TyCon]
natMin forall a. Given a => a
given
                     ]

decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr
decodeMinMax :: Given Translation =>
TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> Machine Expr
decodeMinMax TcPredType
n TcPredType
m TcPredType
lt TcPredType
eq TcPredType
gt 
  | TcPredType
lt TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
n Bool -> Bool -> Bool
&& TcPredType
eq TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
n Bool -> Bool -> Bool
&& TcPredType
gt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
m = 
    Expr -> Expr -> Expr
Min forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
  | TcPredType
lt TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
n Bool -> Bool -> Bool
&& TcPredType
eq TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
m Bool -> Bool -> Bool
&& TcPredType
gt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
m = 
    Expr -> Expr -> Expr
Min forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
  | TcPredType
lt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
m Bool -> Bool -> Bool
&& TcPredType
eq TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
m Bool -> Bool -> Bool
&& TcPredType
gt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
n = 
    Expr -> Expr -> Expr
Max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
  | TcPredType
lt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
m Bool -> Bool -> Bool
&& TcPredType
eq TcPredType -> TcPredType -> Bool
`eqType`  TcPredType
n Bool -> Bool -> Bool
&& TcPredType
gt TcPredType -> TcPredType -> Bool
`eqType` TcPredType
n = 
    Expr -> Expr -> Expr
Max forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
  | Bool
otherwise = forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- simplTypeCmp :: Type -> Type

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
lastN :: Int -> [a] -> [a]
lastN :: forall a. Int -> [a] -> [a]
lastN Int
n = 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
n 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

simpleExp :: Given Translation => Type -> Type
simpleExp :: Given Translation => TcPredType -> TcPredType
simpleExp (AppTy TcPredType
t1 TcPredType
t2) = TcPredType -> TcPredType -> TcPredType
AppTy (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t1) (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
#if MIN_VERSION_ghc(9,0,0)
simpleExp (FunTy AnonArgFlag
f TcPredType
m TcPredType
t1 TcPredType
t2) = AnonArgFlag -> TcPredType -> TcPredType -> TcPredType -> TcPredType
FunTy AnonArgFlag
f TcPredType
m (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t1) (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
#else
#if MIN_VERSION_ghc(8,10,1)
simpleExp (FunTy f t1 t2) = FunTy f (simpleExp t1) (simpleExp t2)
#else
simpleExp (FunTy t1 t2) = FunTy (simpleExp t1) (simpleExp t2)
#endif
#endif 
simpleExp (ForAllTy TyCoVarBinder
t1 TcPredType
t2) = TyCoVarBinder -> TcPredType -> TcPredType
ForAllTy TyCoVarBinder
t1 (Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
simpleExp (TyConApp TyCon
tc (forall a. [a] -> [a]
lastTwo -> [TcPredType]
ts)) =
  forall a. a -> Maybe a -> a
fromMaybe (TyCon -> [TcPredType] -> TcPredType
TyConApp TyCon
tc (forall a b. (a -> b) -> [a] -> [b]
map Given Translation => TcPredType -> TcPredType
simpleExp [TcPredType]
ts)) forall a b. (a -> b) -> a -> b
$
    forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
      ( forall a b. (a -> b) -> [a] -> [b]
map (TyCon, Integer -> Integer -> Integer) -> Maybe TcPredType
simpler forall a b. (a -> b) -> a -> b
$
          [(TyCon
c, forall a. Num a => a -> a -> a
(+)) | TyCon
c <- Translation -> [TyCon]
natPlus forall a. Given a => a
given]
          forall a. [a] -> [a] -> [a]
++ [(TyCon
c, (-)) | TyCon
c <- Translation -> [TyCon]
natMinus forall a. Given a => a
given]
            forall a. [a] -> [a] -> [a]
++ [(TyCon
c, forall a. Num a => a -> a -> a
(*)) | TyCon
c <- Translation -> [TyCon]
natTimes forall a. Given a => a
given]
            forall a. [a] -> [a] -> [a]
++ [(TyCon
c, forall a b. (Num a, Integral b) => a -> b -> a
(^)) | TyCon
c <- Translation -> [TyCon]
natExp forall a. Given a => a
given]
      )
  where
    simpler :: (TyCon, Integer -> Integer -> Integer) -> Maybe TcPredType
simpler (TyCon
con, Integer -> Integer -> Integer
op)
      | TyCon
con forall a. Eq a => a -> a -> Bool
== TyCon
tc
        , [TcPredType
tl, TcPredType
tr] <- forall a b. (a -> b) -> [a] -> [b]
map Given Translation => TcPredType -> TcPredType
simpleExp [TcPredType]
ts =
        forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$
          case (TcPredType
tl, TcPredType
tr) of
            (LitTy (NumTyLit Integer
n), LitTy (NumTyLit Integer
m)) -> TyLit -> TcPredType
LitTy (Integer -> TyLit
NumTyLit (Integer -> Integer -> Integer
op Integer
n Integer
m))
            (TcPredType, TcPredType)
_ -> TyCon -> [TcPredType] -> TcPredType
TyConApp TyCon
con [TcPredType
tl, TcPredType
tr]
      | Bool
otherwise = forall a. Maybe a
Nothing
simpleExp TcPredType
t = TcPredType
t

type ParseEnv = M.Map TypeEq TyVar

type Machine = MaybeT (StateT ParseEnv TcPluginM)

runMachine :: Machine a -> TcPluginM (Maybe a)
runMachine :: forall a. Machine a -> TcPluginM (Maybe a)
runMachine Machine a
act = do
  (Maybe a
ma, ParseEnv
dic) <- forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT Machine a
act) forall k a. Map k a
M.empty
  forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall k a. Map k a -> [(k, a)]
M.toList ParseEnv
dic) forall a b. (a -> b) -> a -> b
$ \(TypeEq TcPredType
ty, TcTyVar
var) ->
    CtLoc -> TcPredType -> TcPluginM CtEvidence
newWanted forall a. HasCallStack => a
undefined forall a b. (a -> b) -> a -> b
$ Role -> TcPredType -> TcPredType -> TcPredType
mkPrimEqPredRole Role
Nominal (TcTyVar -> TcPredType
mkTyVarTy TcTyVar
var) TcPredType
ty
  forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
ma

toVar :: Type -> Machine TyVar
toVar :: TcPredType -> Machine TcTyVar
toVar TcPredType
ty =
  forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (TcPredType -> TypeEq
TypeEq TcPredType
ty)) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just TcTyVar
v -> forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
v
    Maybe TcTyVar
Nothing -> do
      TcTyVar
v <- 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
$ TcPredType -> TcPluginM TcTyVar
newFlexiTyVar forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => TcPredType -> TcPredType
typeKind TcPredType
ty
      forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify forall a b. (a -> b) -> a -> b
$ forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (TcPredType -> TypeEq
TypeEq TcPredType
ty) TcTyVar
v
      forall (m :: * -> *) a. Monad m => a -> m a
return TcTyVar
v