{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternGuards #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ViewPatterns #-}

-- | Since 0.3.0.0
module GHC.TypeLits.Presburger.Types
  ( pluginWith,
    defaultTranslation,
    Translation (..),
    ParseEnv,
    Machine,
    module Data.Integer.SAT,
  )
where

import Class (classTyCon)
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.Foldable (asum)
import Data.Integer.SAT (Expr (..), Prop (..), PropSet, assert, checkSat, noProps, toName)
import qualified Data.Integer.SAT as SAT
import Data.List (nub)
import qualified Data.Map.Strict as M
import Data.Maybe
  ( catMaybes,
    fromMaybe,
    isNothing,
  )
import Data.Reflection (Given, give, given)
import qualified Data.Set as Set
import GHC.TypeLits.Presburger.Compat
import Outputable (showSDocUnsafe)
import PrelNames
import TcPluginM
  ( lookupOrig,
    newFlexiTyVar,
    newWanted,
    tcLookupClass,
  )
import Type (mkTyVarTy)
import TysWiredIn
  ( promotedEQDataCon,
    promotedGTDataCon,
    promotedLTDataCon,
  )
#if MIN_VERSION_ghc(8,8,1)
import TysWiredIn (eqTyConName)
#else
import PrelNames (eqTyConName)
#endif

import Var

#if MIN_VERSION_ghc(8,6,0)
import Plugins (purePlugin)
#endif

assert' :: Prop -> PropSet -> PropSet
assert' :: Prop -> PropSet -> PropSet
assert' Prop
p PropSet
ps = (Prop -> PropSet -> PropSet) -> PropSet -> [Prop] -> PropSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert PropSet
ps (Prop
p Prop -> [Prop] -> [Prop]
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]
(Int -> ReadS Proof)
-> ReadS [Proof]
-> ReadPrec Proof
-> ReadPrec [Proof]
-> Read 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 -> String
(Int -> Proof -> ShowS)
-> (Proof -> String) -> ([Proof] -> ShowS) -> Show Proof
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Proof] -> ShowS
$cshowList :: [Proof] -> ShowS
show :: Proof -> String
$cshow :: Proof -> String
showsPrec :: Int -> Proof -> ShowS
$cshowsPrec :: Int -> Proof -> ShowS
Show, Proof -> Proof -> Bool
(Proof -> Proof -> Bool) -> (Proof -> Proof -> Bool) -> Eq Proof
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
Eq Proof
-> (Proof -> Proof -> Ordering)
-> (Proof -> Proof -> Bool)
-> (Proof -> Proof -> Bool)
-> (Proof -> Proof -> Bool)
-> (Proof -> Proof -> Bool)
-> (Proof -> Proof -> Proof)
-> (Proof -> Proof -> Proof)
-> Ord 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
$cp1Ord :: Eq Proof
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) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Prop -> [Name]
varsProp Prop
q
varsProp (Prop
p :&& Prop
q) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Prop -> [Name]
varsProp Prop
q
varsProp (Not Prop
p) = Prop -> [Name]
varsProp Prop
p
varsProp (Expr
e :== Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :/= Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :< Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :> Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :<= Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp (Expr
e :>= Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsProp Prop
_ = []

varsExpr :: Expr -> [SAT.Name]
varsExpr :: Expr -> [Name]
varsExpr (Expr
e :+ Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Expr
e :- Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
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 (Var Name
i) = [Name
i]
varsExpr (K Integer
_) = []
varsExpr (If Prop
p Expr
e Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Prop -> [Name]
varsProp Prop
p [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
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]
(Int -> ReadS PluginMode)
-> ReadS [PluginMode]
-> ReadPrec PluginMode
-> ReadPrec [PluginMode]
-> Read 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 -> String
(Int -> PluginMode -> ShowS)
-> (PluginMode -> String)
-> ([PluginMode] -> ShowS)
-> Show PluginMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PluginMode] -> ShowS
$cshowList :: [PluginMode] -> ShowS
show :: PluginMode -> String
$cshow :: PluginMode -> String
showsPrec :: Int -> PluginMode -> ShowS
$cshowsPrec :: Int -> PluginMode -> ShowS
Show, PluginMode -> PluginMode -> Bool
(PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool) -> Eq PluginMode
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
Eq PluginMode
-> (PluginMode -> PluginMode -> Ordering)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> PluginMode)
-> (PluginMode -> PluginMode -> PluginMode)
-> Ord 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
$cp1Ord :: Eq PluginMode
Ord)

pluginWith :: TcPluginM Translation -> Plugin
pluginWith :: TcPluginM Translation -> Plugin
pluginWith TcPluginM Translation
trans =
  Plugin
defaultPlugin
    { tcPlugin :: TcPlugin
tcPlugin = TcPlugin -> Maybe TcPlugin
forall a. a -> Maybe a
Just (TcPlugin -> Maybe TcPlugin) -> ([String] -> TcPlugin) -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin TcPluginM Translation
trans (PluginMode -> TcPlugin)
-> ([String] -> PluginMode) -> [String] -> TcPlugin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [String] -> PluginMode
forall (t :: * -> *) a.
(Foldable t, Eq a, IsString a) =>
t a -> PluginMode
procOpts
#if MIN_VERSION_ghc(8,6,0)
    , pluginRecompile :: [String] -> IO PluginRecompile
pluginRecompile = [String] -> IO PluginRecompile
purePlugin
#endif
    }
  where
    procOpts :: t a -> PluginMode
procOpts t a
opts
      | a
"allow-negated-numbers" a -> t a -> Bool
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 =
  String -> TcPlugin -> TcPlugin
tracePlugin
    String
"typelits-presburger"
    TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin
      { tcPluginInit :: TcPluginM ()
tcPluginInit = () -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      , tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = PluginMode -> TcPluginM Translation -> () -> TcPluginSolver
decidePresburger PluginMode
mode TcPluginM Translation
trans
      , tcPluginStop :: () -> TcPluginM ()
tcPluginStop = TcPluginM () -> () -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM () -> () -> TcPluginM ())
-> TcPluginM () -> () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      }

testIf :: PropSet -> Prop -> Proof
testIf :: PropSet -> Prop -> Proof
testIf PropSet
ps Prop
q = Proof
-> ([(Int, Integer)] -> Proof) -> Maybe [(Int, Integer)] -> Proof
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Proof
Proved [(Int, Integer)] -> Proof
Disproved (Maybe [(Int, Integer)] -> Proof)
-> Maybe [(Int, Integer)] -> Proof
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) = RWS () (Set Prop) (Set Expr) Prop
-> () -> Set Expr -> (Prop, Set Expr, Set Prop)
forall r w s a. RWS r w s a -> r -> s -> (a, s, w)
runRWS (Prop -> RWS () (Set Prop) (Set Expr) Prop
forall (m :: * -> *) r.
Monad m =>
Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
p0) () Set Expr
forall a. Set a
Set.empty
   in (Prop -> Prop -> Prop) -> Prop -> Set Prop -> Prop
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 = Prop -> RWST r (Set Prop) (Set Expr) m Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
    loop Prop
PFalse = Prop -> RWST r (Set Prop) (Set Expr) m Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PFalse
    loop (Prop
q :|| Prop
r) = Prop -> Prop -> Prop
(:||) (Prop -> Prop -> Prop)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m (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 RWST r (Set Prop) (Set Expr) m (Prop -> Prop)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m Prop
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
(:&&) (Prop -> Prop -> Prop)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m (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 RWST r (Set Prop) (Set Expr) m (Prop -> Prop)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m Prop
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 (Prop -> Prop)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m 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
    loop (Expr
l :<= Expr
r) = Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :< Expr
r) = Expr -> Expr -> Prop
(:<) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :>= Expr
r) = Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :> Expr
r) = Expr -> Expr -> Prop
(:>) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :== Expr
r) = Expr -> Expr -> Prop
(:==) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loop (Expr
l :/= Expr
r) = Expr -> Expr -> Prop
(:/=) (Expr -> Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Prop)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
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 <- RWST r (Set Prop) (Set Expr) m (Set Expr)
forall s (m :: * -> *). MonadState s m => m s
get
      Bool
-> RWST r (Set Prop) (Set Expr) m ()
-> RWST r (Set Prop) (Set Expr) m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Expr -> Set Expr -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Expr
pos Set Expr
dic) (RWST r (Set Prop) (Set Expr) m ()
 -> RWST r (Set Prop) (Set Expr) m ())
-> RWST r (Set Prop) (Set Expr) m ()
-> RWST r (Set Prop) (Set Expr) m ()
forall a b. (a -> b) -> a -> b
$ do
        (Set Expr -> Set Expr) -> RWST r (Set Prop) (Set Expr) m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Set Expr -> Set Expr) -> RWST r (Set Prop) (Set Expr) m ())
-> (Set Expr -> Set Expr) -> RWST r (Set Prop) (Set Expr) m ()
forall a b. (a -> b) -> a -> b
$ Expr -> Set Expr -> Set Expr
forall a. Ord a => a -> Set a -> Set a
Set.insert Expr
pos
        Set Prop -> RWST r (Set Prop) (Set Expr) m ()
forall (m :: * -> *) w r s. Monad m => w -> RWST r w s m ()
tell (Set Prop -> RWST r (Set Prop) (Set Expr) m ())
-> Set Prop -> RWST r (Set Prop) (Set Expr) m ()
forall a b. (a -> b) -> a -> b
$ [Prop] -> Set Prop
forall a. Ord a => [a] -> Set a
Set.fromList [Expr
pos Expr -> Expr -> Prop
:>= Integer -> Expr
K Integer
0]
      Expr -> RWST r (Set Prop) (Set Expr) m Expr
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
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive (Expr -> RWST r (Set Prop) (Set Expr) m Expr)
-> (Expr -> Expr) -> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
Negate (Expr -> RWST r (Set Prop) (Set Expr) m Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
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
(:-) (Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (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 RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
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
      Expr -> RWST r (Set Prop) (Set Expr) m Expr
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
(:+) (Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (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 RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
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 {} = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
    loopExp (Integer
c :* Expr
e)
      | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = (Integer
c Integer -> Expr -> Expr
:*) (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m 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 = (Integer -> Integer
forall a. Num a => a -> a
negate Integer
c Integer -> Expr -> Expr
:*) (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m 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 e :: Expr
e@(K Integer
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

data Translation = Translation
  { Translation -> [TyCon]
isEmpty :: [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]
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]
orderingLT :: [TyCon]
  , Translation -> [TyCon]
orderingGT :: [TyCon]
  , Translation -> [TyCon]
orderingEQ :: [TyCon]
  , Translation -> [TyCon]
natCompare :: [TyCon]
  , Translation -> (Type -> Machine Expr) -> Type -> Machine Prop
parsePred :: (Type -> Machine Expr) -> Type -> Machine Prop
  , Translation -> Type -> Machine Expr
parseExpr :: Type -> Machine Expr
  }

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

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

decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginResult
decidePresburger :: PluginMode -> TcPluginM Translation -> () -> TcPluginSolver
decidePresburger PluginMode
_ TcPluginM Translation
genTrans ()
_ [Ct]
gs [] [] = do
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: Started givens with: " ([Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Type] -> SDoc) -> [Type] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (CtEvidence -> Type
ctEvPred (CtEvidence -> Type) -> (Ct -> CtEvidence) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
gs)
  Translation
trans <- TcPluginM Translation
genTrans
  Translation
-> (Given Translation => TcPluginM TcPluginResult)
-> TcPluginM TcPluginResult
forall a r. a -> (Given a => r) -> r
give Translation
trans ((Given Translation => TcPluginM TcPluginResult)
 -> TcPluginM TcPluginResult)
-> (Given Translation => TcPluginM TcPluginResult)
-> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ do
    [Maybe (Ct, Prop)]
ngs <- (Ct -> TcPluginM (Maybe (Ct, Prop)))
-> [Ct] -> TcPluginM [Maybe (Ct, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (\Ct
a -> Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop))
forall a. Machine a -> TcPluginM (Maybe a)
runMachine (Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop)))
-> Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop))
forall a b. (a -> b) -> a -> b
$ (,) Ct
a (Prop -> (Ct, Prop)) -> Machine Prop -> Machine (Ct, Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred (Ct -> Type
deconsPred Ct
a)) [Ct]
gs
    let givens :: [(Ct, Prop)]
givens = [Maybe (Ct, Prop)] -> [(Ct, Prop)]
forall a. [Maybe a] -> [a]
catMaybes [Maybe (Ct, Prop)]
ngs
        prems0 :: [Prop]
prems0 = ((Ct, Prop) -> Prop) -> [(Ct, Prop)] -> [Prop]
forall a b. (a -> b) -> [a] -> [b]
map (Ct, Prop) -> Prop
forall a b. (a, b) -> b
snd [(Ct, Prop)]
givens
        prems :: PropSet
prems = (Prop -> PropSet -> PropSet) -> PropSet -> [Prop] -> PropSet
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert' PropSet
noProps [Prop]
prems0
        ([Ct]
solved, PropSet
_) = ((Ct, Prop) -> ([Ct], PropSet) -> ([Ct], PropSet))
-> ([Ct], PropSet) -> [(Ct, Prop)] -> ([Ct], PropSet)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Ct, Prop) -> ([Ct], PropSet) -> ([Ct], PropSet)
forall a. (a, Prop) -> ([a], PropSet) -> ([a], PropSet)
go ([], PropSet
noProps) [(Ct, Prop)]
givens
    if Maybe [(Int, Integer)] -> Bool
forall a. Maybe a -> Bool
isNothing (PropSet -> Maybe [(Int, Integer)]
checkSat PropSet
prems)
      then TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginResult
TcPluginContradiction [Ct]
gs
      else TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk ((Ct -> (EvTerm, Ct)) -> [Ct] -> [(EvTerm, Ct)]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> (EvTerm, Ct)
withEv [Ct]
solved) []
  where
    go :: (a, Prop) -> ([a], PropSet) -> ([a], PropSet)
go (a
ct, Prop
p) ([a]
ss, PropSet
prem)
      | Proof
Proved <- PropSet -> Prop -> Proof
testIf PropSet
prem Prop
p = (a
ct a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
ss, PropSet
prem)
      | Bool
otherwise = ([a]
ss, Prop -> PropSet -> PropSet
assert' Prop
p PropSet
prem)
decidePresburger PluginMode
mode TcPluginM Translation
genTrans ()
_ [Ct]
gs [Ct]
_ds [Ct]
ws = do
  Translation
trans <- TcPluginM Translation
genTrans
  Translation
-> (Given Translation => TcPluginM TcPluginResult)
-> TcPluginM TcPluginResult
forall a r. a -> (Given a => r) -> r
give Translation
trans ((Given Translation => TcPluginM TcPluginResult)
 -> TcPluginM TcPluginResult)
-> (Given Translation => TcPluginM TcPluginResult)
-> TcPluginM TcPluginResult
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'
    String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: Current subst" (Substitution -> SDoc
forall a. Outputable a => a -> SDoc
ppr Substitution
subst)
    String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: wanteds" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Type] -> SDoc) -> [Type] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> Type -> Type
subsType Substitution
subst (Type -> Type) -> (Ct -> Type) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Type
deconsPred (Ct -> Type) -> (Ct -> Ct) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> Ct -> Ct
subsCt Substitution
subst) [Ct]
ws
    String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: givens" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Type] -> SDoc) -> [Type] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> Type -> Type
subsType Substitution
subst (Type -> Type) -> (Ct -> Type) -> Ct -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> Type
deconsPred) [Ct]
gs
    String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: deriveds" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [Type] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([Type] -> SDoc) -> [Type] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> Type) -> [Ct] -> [Type]
forall a b. (a -> b) -> [a] -> [b]
map Ct -> Type
deconsPred [Ct]
_ds
    (PropSet
prems, [(Ct, Prop)]
wants, [Prop]
prems0) <- do
      [(Ct, Prop)]
wants <-
        [Maybe (Ct, Prop)] -> [(Ct, Prop)]
forall a. [Maybe a] -> [a]
catMaybes
          ([Maybe (Ct, Prop)] -> [(Ct, Prop)])
-> TcPluginM [Maybe (Ct, Prop)] -> TcPluginM [(Ct, Prop)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ct -> TcPluginM (Maybe (Ct, Prop)))
-> [Ct] -> TcPluginM [Maybe (Ct, Prop)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM
            ( \Ct
ct ->
                Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop))
forall a. Machine a -> TcPluginM (Maybe a)
runMachine (Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop)))
-> Machine (Ct, Prop) -> TcPluginM (Maybe (Ct, Prop))
forall a b. (a -> b) -> a -> b
$
                  (,) Ct
ct
                    (Prop -> (Ct, Prop)) -> Machine Prop -> Machine (Ct, Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred
                      ( Substitution -> Type -> Type
subsType Substitution
subst (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$
                          Ct -> Type
deconsPred (Ct -> Type) -> Ct -> Type
forall a b. (a -> b) -> a -> b
$ Substitution -> Ct -> Ct
subsCt Substitution
subst Ct
ct
                      )
            )
            ((Ct -> Bool) -> [Ct] -> [Ct]
forall a. (a -> Bool) -> [a] -> [a]
filter (CtEvidence -> Bool
isWanted (CtEvidence -> Bool) -> (Ct -> CtEvidence) -> Ct -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
ws)

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

defaultTranslation :: TcPluginM Translation
defaultTranslation :: TcPluginM Translation
defaultTranslation = do
  Module
emd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Proof.Propositional.Empty") (String -> FastString
fsLit String
"equational-reasoning")
  TyCon
emptyClsTyCon <- Class -> TyCon
classTyCon (Class -> TyCon) -> TcPluginM Class -> TcPluginM TyCon
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Name -> TcPluginM Class
tcLookupClass (Name -> TcPluginM Class) -> TcPluginM Name -> TcPluginM Class
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
emd (String -> OccName
mkTcOcc String
"Empty"))
  TyCon
eqTyCon_ <- TcPluginM TyCon
getEqTyCon
  TyCon
eqWitCon_ <- TcPluginM TyCon
getEqWitnessTyCon
  Module
pmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Proof.Propositional") (String -> FastString
fsLit String
"equational-reasoning")
  TyCon
isTrueCon_ <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
pmd (String -> OccName
mkTcOcc String
"IsTrue")
  Module
vmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Data.Void") (String -> FastString
fsLit String
"base")
  TyCon
voidTyCon <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
vmd (String -> OccName
mkTcOcc String
"Void")
  TyCon
nLeq <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
gHC_TYPENATS (String -> OccName
mkTcOcc String
"<=")
  Translation -> TcPluginM Translation
forall (m :: * -> *) a. Monad m => a -> m a
return
    Translation
forall a. Monoid a => a
mempty
      { isEmpty :: [TyCon]
isEmpty = [TyCon
emptyClsTyCon]
      , tyEq :: [TyCon]
tyEq = [TyCon
eqTyCon_]
      , tyEqWitness :: [TyCon]
tyEqWitness = [TyCon
eqWitCon_]
      , isTrue :: [TyCon]
isTrue = [TyCon
isTrueCon_]
      , 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
typeNatLeqTyCon]
      , natLeq :: [TyCon]
natLeq = [TyCon
nLeq]
      , natCompare :: [TyCon]
natCompare = [TyCon
typeNatCmpTyCon]
      , orderingEQ :: [TyCon]
orderingEQ = [TyCon
promotedEQDataCon]
      , orderingLT :: [TyCon]
orderingLT = [TyCon
promotedLTDataCon]
      , orderingGT :: [TyCon]
orderingGT = [TyCon
promotedGTDataCon]
      }

(<=>) :: 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)

withEv :: Ct -> (EvTerm, Ct)
withEv :: Ct -> (EvTerm, Ct)
withEv Ct
ct =
  case Type -> Pred
classifyPredType (Ct -> Type
deconsPred Ct
ct) of
    EqPred EqRel
_ Type
t1 Type
t2 -> (String -> Type -> Type -> EvTerm
evByFiat String
"ghc-typelits-presburger" Type
t1 Type
t2, Ct
ct)
    Pred
_ -> String -> (EvTerm, Ct)
forall a. HasCallStack => String -> a
error (String -> (EvTerm, Ct)) -> String -> (EvTerm, Ct)
forall a b. (a -> b) -> a -> b
$ String
"UnknownPredEv: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> SDoc -> String
showSDocUnsafe (Ct -> SDoc
forall a. Outputable a => a -> SDoc
ppr Ct
ct)

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

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

toPresburgerPred :: Given Translation => Type -> Machine Prop
toPresburgerPred :: Type -> Machine Prop
toPresburgerPred (TyConApp TyCon
con [Type
t1, Type
t2])
  | TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Translation -> [TyCon]
natLeq Translation
forall a. Given a => a
given [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
natLeqBool Translation
forall a. Given a => a
given) =
    Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t2
toPresburgerPred Type
ty
  | Just (TyCon
con, []) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
trueData Translation
forall a. Given a => a
given =
    Prop -> Machine Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
  | Just (TyCon
con, []) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
falseData Translation
forall a. Given a => a
given =
    Prop -> Machine Prop
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PFalse
  | cls :: Pred
cls@(EqPred EqRel
NomEq Type
_ Type
_) <- Type -> Pred
classifyPredType Type
ty =
    Pred -> Machine Prop
Given Translation => Pred -> Machine Prop
toPresburgerPredTree Pred
cls
  | Type -> Bool
isEqPred Type
ty = Pred -> Machine Prop
Given Translation => Pred -> Machine Prop
toPresburgerPredTree (Pred -> Machine Prop) -> Pred -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Type -> Pred
classifyPredType Type
ty
  | Just (TyCon
con, [Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty -- l ~ r
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Translation -> [TyCon]
tyEq Translation
forall a. Given a => a
given [TyCon] -> [TyCon] -> [TyCon]
forall a. [a] -> [a] -> [a]
++ Translation -> [TyCon]
tyEqBool Translation
forall a. Given a => a
given) =
    Pred -> Machine Prop
Given Translation => Pred -> Machine Prop
toPresburgerPredTree (Pred -> Machine Prop) -> Pred -> Machine Prop
forall a b. (a -> b) -> a -> b
$ EqRel -> Type -> Type -> Pred
EqPred EqRel
NomEq Type
l Type
r
  | Just (TyCon
con, [Type
_k, Type
l, Type
r]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty -- l (:~: {k}) r
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyEqWitness Translation
forall a. Given a => a
given =
    Pred -> Machine Prop
Given Translation => Pred -> Machine Prop
toPresburgerPredTree (Pred -> Machine Prop) -> Pred -> Machine Prop
forall a b. (a -> b) -> a -> b
$ EqRel -> Type -> Type -> Pred
EqPred EqRel
NomEq Type
l Type
r
  | Just (TyCon
con, [Type
l]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty -- Empty l => ...
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
isEmpty Translation
forall a. Given a => a
given =
    Prop -> Prop
Not (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
l
  | Just (TyCon
con, [Type
l]) <- HasDebugCallStack => Type -> Maybe (TyCon, [Type])
Type -> Maybe (TyCon, [Type])
splitTyConApp_maybe Type
ty -- IsTrue l =>
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
isTrue Translation
forall a. Given a => a
given =
    Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
l
  | Bool
otherwise = Translation -> (Type -> Machine Expr) -> Type -> Machine Prop
parsePred Translation
forall a. Given a => a
given Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
ty

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

toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop
toPresburgerPredTree :: Pred -> Machine Prop
toPresburgerPredTree (EqPred EqRel
NomEq Type
p Type
false) -- P ~ 'False <=> Not P ~ 'True
  | Bool -> (TyCon -> Bool) -> Maybe TyCon -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
falseData Translation
forall a. Given a => a
given) (Maybe TyCon -> Bool) -> Maybe TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Maybe TyCon
tyConAppTyCon_maybe Type
false =
    Prop -> Prop
Not (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Pred -> Machine Prop
Given Translation => Pred -> Machine Prop
toPresburgerPredTree (EqRel -> Type -> Type -> Pred
EqPred EqRel
NomEq Type
p (TyCon -> Type
mkTyConTy TyCon
promotedTrueDataCon))
toPresburgerPredTree (EqPred EqRel
NomEq Type
p Type
b) -- (n :<=? m) ~ 'True
  | Bool -> (TyCon -> Bool) -> Maybe TyCon -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
trueData Translation
forall a. Given a => a
given) (Maybe TyCon -> Bool) -> Maybe TyCon -> Bool
forall a b. (a -> b) -> a -> b
$ Type -> Maybe TyCon
tyConAppTyCon_maybe Type
b
    , Just (TyCon
con, [Type
t1, Type
t2]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
p
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natLeqBool Translation
forall a. Given a => a
given =
    Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t2
toPresburgerPredTree (EqPred EqRel
NomEq Type
p Type
q) -- (p :: Bool) ~ (q :: Bool)
  | HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
p Type -> Type -> Bool
`eqType` TyCon -> Type
mkTyConTy TyCon
promotedBoolTyCon = do
    StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM ()
 -> MaybeT (StateT ParseEnv TcPluginM) ())
-> StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TcPluginM () -> StateT ParseEnv TcPluginM ()
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM () -> StateT ParseEnv TcPluginM ())
-> TcPluginM () -> StateT ParseEnv TcPluginM ()
forall a b. (a -> b) -> a -> b
$ String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: EQBOOL:" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ (Type, Type) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (Type
p, Type
q)
    Prop -> Prop -> Prop
(<=>) (Prop -> Prop -> Prop)
-> Machine Prop
-> MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
p
      MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
q
toPresburgerPredTree (EqPred EqRel
NomEq Type
n Type
m) -- (n :: Nat) ~ (m :: Nat)
  | HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
n Type -> Type -> Bool
`eqType` Type
typeNatKind =
    Expr -> Expr -> Prop
(:==) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
n
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
m
toPresburgerPredTree (EqPred EqRel
_ Type
t1 Type
t2) -- CmpNat a b ~ CmpNat c d
  | Just (TyCon
con, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
a, Type
b]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
t1
    , Just (TyCon
con', [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
c, Type
d]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
t2
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
forall a. Given a => a
given
    , TyCon
con' TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
forall a. Given a => a
given =
    Prop -> Prop -> Prop
(<=>) (Prop -> Prop -> Prop)
-> Machine Prop
-> MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Expr -> Expr -> Prop
(:<) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
a MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
b)
      MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (Expr -> Expr -> Prop
(:<) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
c MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
d)
toPresburgerPredTree (EqPred EqRel
NomEq Type
t1 Type
t2) -- CmpNat a b ~ x
  | Just (TyCon
con, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
a, Type
b]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
t1
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
forall a. Given a => a
given
    , Just TyCon
cmp <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
t2 =
    StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe (Expr -> Expr -> Prop)
-> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Expr -> Expr -> Prop)
 -> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop)))
-> Maybe (Expr -> Expr -> Prop)
-> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
forall a b. (a -> b) -> a -> b
$ TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
cmp [(TyCon, Expr -> Expr -> Prop)]
Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic)
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
a
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
b
toPresburgerPredTree (EqPred EqRel
NomEq Type
t1 Type
t2) -- x ~ CmpNat a b
  | Just (TyCon
con, [Type] -> [Type]
forall a. [a] -> [a]
lastTwo -> [Type
a, Type
b]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
t2
    , TyCon
con TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
forall a. Given a => a
given
    , Just TyCon
cmp <- Type -> Maybe TyCon
tyConAppTyCon_maybe Type
t1 =
    StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe (Expr -> Expr -> Prop)
-> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe (Expr -> Expr -> Prop)
 -> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop)))
-> Maybe (Expr -> Expr -> Prop)
-> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
forall a b. (a -> b) -> a -> b
$ TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
cmp [(TyCon, Expr -> Expr -> Prop)]
Given Translation => [(TyCon, Expr -> Expr -> Prop)]
orderingDic)
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
a
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
b
toPresburgerPredTree (ClassPred Class
con [Type]
ts)
  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)
  | let n :: Int
n = [Type] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Type]
ts
    , Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
2
    , [Type
t1, Type
t2] <- Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
drop (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
2) [Type]
ts
    , HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t1 Type -> Type -> Bool
`eqType` Type
typeNatKind
    , HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
t2 Type -> Type -> Bool
`eqType` Type
typeNatKind =
    let p :: Maybe (Expr -> Expr -> Prop)
p = TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (Class -> TyCon
classTyCon Class
con) [(TyCon, Expr -> Expr -> Prop)]
Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic
     in StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (Maybe (Expr -> Expr -> Prop)
-> StateT ParseEnv TcPluginM (Maybe (Expr -> Expr -> Prop))
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe (Expr -> Expr -> Prop)
p) MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
t2
toPresburgerPredTree Pred
_ = Machine Prop
forall (m :: * -> *) a. MonadPlus m => m a
mzero

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

toPresburgerExp :: Given Translation => Type -> Machine Expr
toPresburgerExp :: Type -> Machine Expr
toPresburgerExp Type
ty = case Type
ty of
  TyVarTy Var
t -> Expr -> Machine Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Machine Expr) -> Expr -> Machine Expr
forall a b. (a -> b) -> a -> b
$ Name -> Expr
Var (Name -> Expr) -> Name -> Expr
forall a b. (a -> b) -> a -> b
$ Int -> Name
toName (Int -> Name) -> Int -> Name
forall a b. (a -> b) -> a -> b
$ Unique -> Int
getKey (Unique -> Int) -> Unique -> Int
forall a b. (a -> b) -> a -> b
$ Var -> Unique
forall a. Uniquable a => a -> Unique
getUnique Var
t
  t :: Type
t@(TyConApp TyCon
tc [Type]
ts) -> TyCon -> [Type] -> Machine Expr
body TyCon
tc [Type]
ts Machine Expr -> Machine Expr -> Machine Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var (Name -> Expr) -> (Var -> Name) -> Var -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName (Int -> Name) -> (Var -> Int) -> Var -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey (Unique -> Int) -> (Var -> Unique) -> Var -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Unique
forall a. Uniquable a => a -> Unique
getUnique (Var -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) Var -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> MaybeT (StateT ParseEnv TcPluginM) Var
toVar Type
t
  LitTy (NumTyLit Integer
n) -> Expr -> Machine Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Expr
K Integer
n)
  LitTy TyLit
_ -> Machine Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  Type
t ->
    Translation -> Type -> Machine Expr
parseExpr Translation
forall a. Given a => a
given Type
ty
      Machine Expr -> Machine Expr -> Machine Expr
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var (Name -> Expr) -> (Var -> Name) -> Var -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName (Int -> Name) -> (Var -> Int) -> Var -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey (Unique -> Int) -> (Var -> Unique) -> Var -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Var -> Unique
forall a. Uniquable a => a -> Unique
getUnique (Var -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) Var -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> MaybeT (StateT ParseEnv TcPluginM) Var
toVar Type
t
  where
    body :: TyCon -> [Type] -> Machine Expr
body TyCon
tc [Type]
ts =
      let step :: TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> b
op
            | TyCon
tc TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
con
              , [Type
tl, Type
tr] <- [Type] -> [Type]
forall a. [a] -> [a]
lastTwo [Type]
ts =
              Expr -> Expr -> b
op (Expr -> Expr -> b)
-> Machine Expr -> MaybeT (StateT ParseEnv TcPluginM) (Expr -> b)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
tl MaybeT (StateT ParseEnv TcPluginM) (Expr -> b)
-> Machine Expr -> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
tr
            | Bool
otherwise = MaybeT (StateT ParseEnv TcPluginM) b
forall (m :: * -> *) a. MonadPlus m => m a
mzero
       in case [Type]
ts of
            [Type
tl, Type
tr] | TyCon
tc TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natTimes Translation
forall a. Given a => a
given ->
              case (Type -> Type
Given Translation => Type -> Type
simpleExp Type
tl, Type -> Type
Given Translation => Type -> Type
simpleExp Type
tr) of
                (LitTy (NumTyLit Integer
n), LitTy (NumTyLit Integer
m)) -> Expr -> Machine Expr
forall (m :: * -> *) a. Monad m => a -> m a
return (Expr -> Machine Expr) -> Expr -> Machine Expr
forall a b. (a -> b) -> a -> b
$ Integer -> Expr
K (Integer -> Expr) -> Integer -> Expr
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
m
                (LitTy (NumTyLit Integer
n), Type
x) -> Integer -> Expr -> Expr
(:*) (Integer -> Expr -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) Integer
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> MaybeT (StateT ParseEnv TcPluginM) Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
x
                (Type
x, LitTy (NumTyLit Integer
n)) -> Integer -> Expr -> Expr
(:*) (Integer -> Expr -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) Integer
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> MaybeT (StateT ParseEnv TcPluginM) Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
x
                (Type, Type)
_ -> Machine Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            [Type]
_ ->
              [Machine Expr] -> Machine Expr
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum ([Machine Expr] -> Machine Expr) -> [Machine Expr] -> Machine Expr
forall a b. (a -> b) -> a -> b
$
                [ TyCon -> (Expr -> Expr -> Expr) -> Machine Expr
forall b.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
(:+)
                | TyCon
con <- Translation -> [TyCon]
natPlus Translation
forall a. Given a => a
given
                ]
                  [Machine Expr] -> [Machine Expr] -> [Machine Expr]
forall a. [a] -> [a] -> [a]
++ [ TyCon -> (Expr -> Expr -> Expr) -> Machine Expr
forall b.
TyCon
-> (Expr -> Expr -> b) -> MaybeT (StateT ParseEnv TcPluginM) b
step TyCon
con Expr -> Expr -> Expr
(:-)
                     | TyCon
con <- Translation -> [TyCon]
natMinus Translation
forall a. Given a => a
given
                     ]

-- simplTypeCmp :: Type -> Type

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

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

type ParseEnv = M.Map TypeEq TyVar

type Machine = MaybeT (StateT ParseEnv TcPluginM)

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

toVar :: Type -> Machine TyVar
toVar :: Type -> MaybeT (StateT ParseEnv TcPluginM) Var
toVar Type
ty =
  (ParseEnv -> Maybe Var)
-> MaybeT (StateT ParseEnv TcPluginM) (Maybe Var)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets (TypeEq -> ParseEnv -> Maybe Var
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Type -> TypeEq
TypeEq Type
ty)) MaybeT (StateT ParseEnv TcPluginM) (Maybe Var)
-> (Maybe Var -> MaybeT (StateT ParseEnv TcPluginM) Var)
-> MaybeT (StateT ParseEnv TcPluginM) Var
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Just Var
v -> Var -> MaybeT (StateT ParseEnv TcPluginM) Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
    Maybe Var
Nothing -> do
      Var
v <- StateT ParseEnv TcPluginM Var
-> MaybeT (StateT ParseEnv TcPluginM) Var
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM Var
 -> MaybeT (StateT ParseEnv TcPluginM) Var)
-> StateT ParseEnv TcPluginM Var
-> MaybeT (StateT ParseEnv TcPluginM) Var
forall a b. (a -> b) -> a -> b
$ TcPluginM Var -> StateT ParseEnv TcPluginM Var
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM Var -> StateT ParseEnv TcPluginM Var)
-> TcPluginM Var -> StateT ParseEnv TcPluginM Var
forall a b. (a -> b) -> a -> b
$ Type -> TcPluginM Var
newFlexiTyVar (Type -> TcPluginM Var) -> Type -> TcPluginM Var
forall a b. (a -> b) -> a -> b
$ HasDebugCallStack => Type -> Type
Type -> Type
typeKind Type
ty
      (ParseEnv -> ParseEnv) -> MaybeT (StateT ParseEnv TcPluginM) ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((ParseEnv -> ParseEnv) -> MaybeT (StateT ParseEnv TcPluginM) ())
-> (ParseEnv -> ParseEnv) -> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TypeEq -> Var -> ParseEnv -> ParseEnv
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Type -> TypeEq
TypeEq Type
ty) Var
v
      Var -> MaybeT (StateT ParseEnv TcPluginM) Var
forall (m :: * -> *) a. Monad m => a -> m a
return Var
v