{-# 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
import GHC.TypeLits.Presburger.Flags

assert' :: Prop -> PropSet -> PropSet
assert' :: Prop -> PropSet -> PropSet
assert' Prop
p PropSet
ps = (Prop -> PropSet -> PropSet) -> PropSet -> [Prop] -> PropSet
forall a b. (a -> b -> b) -> b -> [a] -> b
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
$creadsPrec :: Int -> ReadS Proof
readsPrec :: Int -> ReadS Proof
$creadList :: ReadS [Proof]
readList :: ReadS [Proof]
$creadPrec :: ReadPrec Proof
readPrec :: ReadPrec Proof
$creadListPrec :: ReadPrec [Proof]
readListPrec :: ReadPrec [Proof]
Read, Int -> Proof -> ShowS
[Proof] -> ShowS
Proof -> CommandLineOption
(Int -> Proof -> ShowS)
-> (Proof -> CommandLineOption) -> ([Proof] -> ShowS) -> Show Proof
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Proof -> ShowS
showsPrec :: Int -> Proof -> ShowS
$cshow :: Proof -> CommandLineOption
show :: Proof -> CommandLineOption
$cshowList :: [Proof] -> ShowS
showList :: [Proof] -> ShowS
Show, Proof -> Proof -> Bool
(Proof -> Proof -> Bool) -> (Proof -> Proof -> Bool) -> Eq Proof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Proof -> Proof -> Bool
== :: Proof -> Proof -> Bool
$c/= :: Proof -> Proof -> Bool
/= :: 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
$ccompare :: Proof -> Proof -> Ordering
compare :: Proof -> Proof -> Ordering
$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
>= :: Proof -> Proof -> Bool
$cmax :: Proof -> Proof -> Proof
max :: Proof -> Proof -> Proof
$cmin :: Proof -> Proof -> Proof
min :: Proof -> Proof -> 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 (Min Expr
l Expr
r) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
l [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
r
varsExpr (Max Expr
l Expr
r) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
l [Name] -> [Name] -> [Name]
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) = [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
$creadsPrec :: Int -> ReadS PluginMode
readsPrec :: Int -> ReadS PluginMode
$creadList :: ReadS [PluginMode]
readList :: ReadS [PluginMode]
$creadPrec :: ReadPrec PluginMode
readPrec :: ReadPrec PluginMode
$creadListPrec :: ReadPrec [PluginMode]
readListPrec :: ReadPrec [PluginMode]
Read, Int -> PluginMode -> ShowS
[PluginMode] -> ShowS
PluginMode -> CommandLineOption
(Int -> PluginMode -> ShowS)
-> (PluginMode -> CommandLineOption)
-> ([PluginMode] -> ShowS)
-> Show PluginMode
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PluginMode -> ShowS
showsPrec :: Int -> PluginMode -> ShowS
$cshow :: PluginMode -> CommandLineOption
show :: PluginMode -> CommandLineOption
$cshowList :: [PluginMode] -> ShowS
showList :: [PluginMode] -> ShowS
Show, PluginMode -> PluginMode -> Bool
(PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool) -> Eq PluginMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PluginMode -> PluginMode -> Bool
== :: PluginMode -> PluginMode -> Bool
$c/= :: PluginMode -> PluginMode -> Bool
/= :: 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
$ccompare :: PluginMode -> PluginMode -> Ordering
compare :: PluginMode -> PluginMode -> Ordering
$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
>= :: PluginMode -> PluginMode -> Bool
$cmax :: PluginMode -> PluginMode -> PluginMode
max :: PluginMode -> PluginMode -> PluginMode
$cmin :: PluginMode -> PluginMode -> PluginMode
min :: PluginMode -> PluginMode -> PluginMode
Ord)

pluginWith :: TcPluginM Translation -> Plugin
pluginWith :: TcPluginM Translation -> Plugin
pluginWith TcPluginM Translation
trans =
  Plugin
defaultPlugin
    { tcPlugin = Just . presburgerPlugin trans . procOpts
    , pluginRecompile = purePlugin
    }
  where
    procOpts :: t a -> PluginMode
procOpts t a
opts
      | a
"allow-negated-numbers" a -> t a -> Bool
forall a. Eq a => 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 =
  CommandLineOption -> TcPlugin -> TcPlugin
tracePlugin
    CommandLineOption
"typelits-presburger"
    TcPlugin
      { tcPluginInit :: TcPluginM ()
tcPluginInit = () -> TcPluginM ()
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      , 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 a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
#if MIN_VERSION_ghc(9,4,1)
      , tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = TcPluginSolver -> () -> TcPluginSolver
forall a b. a -> b -> a
const (TcPluginSolver -> () -> TcPluginSolver)
-> TcPluginSolver -> () -> TcPluginSolver
forall a b. (a -> b) -> a -> b
$ \EvBindsVar
_ [Ct]
gs [Ct]
ws -> PluginMode
-> TcPluginM Translation
-> ()
-> [Ct]
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginSolveResult
decidePresburger PluginMode
mode TcPluginM Translation
trans () [Ct]
gs [] [Ct]
ws
#else
      , tcPluginSolve = decidePresburger mode trans
#endif

#if MIN_VERSION_ghc(9,4,1)
      , tcPluginRewrite :: () -> UniqFM TyCon TcPluginRewriter
tcPluginRewrite = () -> UniqFM TyCon TcPluginRewriter
forall a. Monoid a => a
mempty
#endif
      }

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 a b. (a -> b -> b) -> b -> Set a -> b
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 a. a -> RWST r (Set Prop) (Set Expr) m a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
    loop Prop
PFalse = Prop -> RWST r (Set Prop) (Set Expr) m Prop
forall a. a -> RWST r (Set Prop) (Set Expr) m a
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
(:<) (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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
(:>=) (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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
(:>) (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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
(:==) (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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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
(:/=) (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
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 <- 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 a. a -> RWST r (Set Prop) (Set Expr) m a
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 a. a -> RWST r (Set Prop) (Set Expr) m a
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 (Min Expr
l Expr
r) = Expr -> Expr -> Expr
Min (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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 (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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 (Prop -> Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Prop
-> RWST r (Set Prop) (Set Expr) m (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Prop -> RWST r (Set Prop) (Set Expr) m Prop
loop Prop
p RWST r (Set Prop) (Set Expr) m (Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
forall a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 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 a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
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 (Expr -> Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Integer -> 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 (Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Integer
-> RWST r (Set Prop) (Set Expr) m Expr
forall a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> RWST r (Set Prop) (Set Expr) m Integer
forall a. a -> RWST r (Set Prop) (Set Expr) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp (Div Expr
l Integer
n) = Expr -> Integer -> Expr
Div (Expr -> Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Integer -> 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 (Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Integer
-> RWST r (Set Prop) (Set Expr) m Expr
forall a b.
RWST r (Set Prop) (Set Expr) m (a -> b)
-> RWST r (Set Prop) (Set Expr) m a
-> RWST r (Set Prop) (Set Expr) m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> RWST r (Set Prop) (Set Expr) m Integer
forall a. a -> RWST r (Set Prop) (Set Expr) m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp e :: Expr
e@(K Integer
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall a. a -> RWST r (Set Prop) (Set Expr) m a
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 [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
      , assertTy :: [TyCon]
assertTy = Translation -> [TyCon]
assertTy Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
assertTy 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
      , tyNot :: [TyCon]
tyNot = Translation -> [TyCon]
tyNot Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyNot Translation
r
      , tyAnd :: [TyCon]
tyAnd = Translation -> [TyCon]
tyAnd Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyAnd Translation
r
      , tyOr :: [TyCon]
tyOr = Translation -> [TyCon]
tyOr Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyOr Translation
r
      , tyIf :: [TyCon]
tyIf = Translation -> [TyCon]
tyIf Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
tyIf 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 :: (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 Machine Prop -> Machine Prop -> Machine Prop
forall a.
MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
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 -> Machine Expr -> Machine Expr -> Machine Expr
forall a.
MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
(<|>) (Machine Expr -> Machine Expr -> Machine Expr)
-> (TcPredType -> Machine Expr)
-> TcPredType
-> Machine Expr
-> Machine Expr
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 (TcPredType -> Machine Expr -> Machine Expr)
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
forall a b.
(TcPredType -> a -> b) -> (TcPredType -> a) -> TcPredType -> b
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 [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natMin Translation
r
      , natMax :: [TyCon]
natMax = Translation -> [TyCon]
natMax Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
natMax Translation
r
      , ordCond :: [TyCon]
ordCond = Translation -> [TyCon]
ordCond Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
ordCond Translation
r
      }

instance Monoid Translation where
  mempty :: Translation
mempty =
    Translation
      { isEmpty :: [TyCon]
isEmpty = [TyCon]
forall a. Monoid a => a
mempty
      , isTrue :: [TyCon]
isTrue = [TyCon]
forall a. Monoid a => a
mempty
      , assertTy :: [TyCon]
assertTy = [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
      , tyNot :: [TyCon]
tyNot = [TyCon]
forall a. Monoid a => a
mempty
      , tyAnd :: [TyCon]
tyAnd = [TyCon]
forall a. Monoid a => a
mempty
      , tyOr :: [TyCon]
tyOr = [TyCon]
forall a. Monoid a => a
mempty
      , tyIf :: [TyCon]
tyIf = [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 :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred = (TcPredType -> Machine Prop)
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
forall a b. a -> b -> a
const ((TcPredType -> Machine Prop)
 -> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop)
-> (TcPredType -> Machine Prop)
-> (TcPredType -> Machine Expr)
-> TcPredType
-> Machine Prop
forall a b. (a -> b) -> a -> b
$ Machine Prop -> TcPredType -> Machine Prop
forall a b. a -> b -> a
const Machine Prop
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      , parseExpr :: (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr = (TcPredType -> Machine Expr)
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
forall a b. a -> b -> a
const ((TcPredType -> Machine Expr)
 -> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr)
-> (TcPredType -> Machine Expr)
-> (TcPredType -> Machine Expr)
-> TcPredType
-> Machine Expr
forall a b. (a -> b) -> a -> b
$ Machine Expr -> TcPredType -> Machine Expr
forall a b. a -> b -> a
const Machine Expr
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
      , natMin :: [TyCon]
natMin = [TyCon]
forall a. Monoid a => a
mempty
      , natMax :: [TyCon]
natMax = [TyCon]
forall a. Monoid a => a
mempty
      , ordCond :: [TyCon]
ordCond = [TyCon]
forall a. Monoid a => a
mempty
      }

decidePresburger :: PluginMode -> TcPluginM Translation -> () -> [Ct] -> [Ct] -> [Ct] -> TcPluginM TcPluginSolveResult
decidePresburger :: PluginMode
-> TcPluginM Translation
-> ()
-> [Ct]
-> [Ct]
-> [Ct]
-> TcPluginM TcPluginSolveResult
decidePresburger PluginMode
_ TcPluginM Translation
genTrans ()
_ [Ct]
gs [] [] = do
  CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Started givens with: " ([TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([TcPredType] -> SDoc) -> [TcPredType] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> TcPredType) -> [Ct] -> [TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map (CtEvidence -> TcPredType
ctEvPred (CtEvidence -> TcPredType)
-> (Ct -> CtEvidence) -> Ct -> TcPredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> CtEvidence
ctEvidence) [Ct]
gs)
  Translation
trans <- TcPluginM Translation
genTrans
  Translation
-> (Given Translation => TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginSolveResult
forall a r. a -> (Given a => r) -> r
give Translation
trans ((Given Translation => TcPluginM TcPluginSolveResult)
 -> TcPluginM TcPluginSolveResult)
-> (Given Translation => TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginSolveResult
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred (Ct -> TcPredType
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 a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Prop -> PropSet -> PropSet
assert' PropSet
noProps [Prop]
prems0
    if Maybe [(Int, Integer)] -> Bool
forall a. Maybe a -> Bool
isNothing (PropSet -> Maybe [(Int, Integer)]
checkSat PropSet
prems)
      then TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginSolveResult
TcPluginContradiction [Ct]
gs
      else TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
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
  Translation
-> (Given Translation => TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginSolveResult
forall a r. a -> (Given a => r) -> r
give Translation
trans ((Given Translation => TcPluginM TcPluginSolveResult)
 -> TcPluginM TcPluginSolveResult)
-> (Given Translation => TcPluginM TcPluginSolveResult)
-> TcPluginM TcPluginSolveResult
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" (Substitution -> SDoc
forall a. Outputable a => a -> SDoc
ppr Substitution
subst)
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: wanteds" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([TcPredType] -> SDoc) -> [TcPredType] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> TcPredType) -> [Ct] -> [TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TcPredType -> TcPredType
subsType Substitution
subst (TcPredType -> TcPredType)
-> (Ct -> TcPredType) -> Ct -> TcPredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPredType
deconsPred (Ct -> TcPredType) -> (Ct -> Ct) -> Ct -> TcPredType
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" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [TcPredType] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ([TcPredType] -> SDoc) -> [TcPredType] -> SDoc
forall a b. (a -> b) -> a -> b
$ (Ct -> TcPredType) -> [Ct] -> [TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map (Substitution -> TcPredType -> TcPredType
subsType Substitution
subst (TcPredType -> TcPredType)
-> (Ct -> TcPredType) -> Ct -> TcPredType
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 <-
        [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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred
                      ( Substitution -> TcPredType -> TcPredType
subsType Substitution
subst (TcPredType -> TcPredType) -> TcPredType -> TcPredType
forall a b. (a -> b) -> a -> b
$
                          Ct -> TcPredType
deconsPred (Ct -> TcPredType) -> Ct -> TcPredType
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)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [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
. TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred (TcPredType -> Machine Prop)
-> (Ct -> TcPredType) -> Ct -> Machine Prop
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution -> TcPredType -> TcPredType
subsType Substitution
subst (TcPredType -> TcPredType)
-> (Ct -> TcPredType) -> Ct -> TcPredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ct -> TcPredType
deconsPred)
          [Ct]
gs
      let prems :: PropSet
prems = (Prop -> PropSet -> PropSet) -> PropSet -> [Prop] -> PropSet
forall a b. (a -> b -> b) -> b -> [a] -> b
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 a. a -> TcPluginM a
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 b c d. (b -> c) -> (d, b) -> (d, c)
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 =
          [ (EvTerm
evProof, Ct
ct)
          | Ct
ct <- [Ct]
solved
          , Just EvTerm
evProof <- Maybe EvTerm -> [Maybe EvTerm]
forall a. a -> [a]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Maybe EvTerm -> [Maybe EvTerm]) -> Maybe EvTerm -> [Maybe EvTerm]
forall a b. (a -> b) -> a -> b
$ PredTree -> Maybe EvTerm
Given Translation => PredTree -> Maybe EvTerm
extractProof (PredTree -> Maybe EvTerm) -> PredTree -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ TcPredType -> PredTree
classifyPredType (TcPredType -> PredTree) -> TcPredType -> PredTree
forall a b. (a -> b) -> a -> b
$ Ct -> TcPredType
deconsPred Ct
ct
          ]
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: final premises" (CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ [Prop] -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show [Prop]
prems0)
    CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: final goals" (CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ [Prop] -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show ([Prop] -> CommandLineOption) -> [Prop] -> CommandLineOption
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 a b. (a -> b -> b) -> b -> [a] -> b
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
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: Proved" (CommandLineOption -> SDoc
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ [Prop] -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show ([Prop] -> CommandLineOption) -> [Prop] -> CommandLineOption
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)
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: ... with coercions" ([(EvTerm, Ct)] -> SDoc
forall a. Outputable a => a -> SDoc
ppr [(EvTerm, Ct)]
coerced)
        TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
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
forall doc. IsLine doc => CommandLineOption -> doc
text (CommandLineOption -> SDoc) -> CommandLineOption -> SDoc
forall a b. (a -> b) -> a -> b
$ [(Int, Integer)] -> CommandLineOption
forall a. Show a => a -> CommandLineOption
show [(Int, Integer)]
wit)
        TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginSolveResult -> TcPluginM TcPluginSolveResult)
-> TcPluginSolveResult -> TcPluginM TcPluginSolveResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginSolveResult
TcPluginContradiction ([Ct] -> TcPluginSolveResult) -> [Ct] -> TcPluginSolveResult
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


extractProof :: Given Translation => PredTree -> Maybe EvTerm
extractProof :: Given Translation => PredTree -> Maybe EvTerm
extractProof (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) = 
    EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
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 TcPredType
prd)
  | Just (TyCon
con, Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
_, TcPredType
_]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
prd
  , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
assertTy Translation
forall a. Given a => a
given = 
    EvTerm -> Maybe EvTerm
forall a. a -> Maybe a
Just (EvTerm -> Maybe EvTerm) -> EvTerm -> Maybe EvTerm
forall a b. (a -> b) -> a -> b
$ TcTyVar -> Expr TcTyVar
forall b. TcTyVar -> Expr b
GHC.Var (DataCon -> TcTyVar
dataConWrapId (DataCon -> TcTyVar) -> DataCon -> TcTyVar
forall a b. (a -> b) -> a -> b
$ Int -> DataCon
cTupleDataCon Int
0) Expr TcTyVar -> TcCoercion -> EvTerm
`evCast`
      UnivCoProvenance -> Role -> TcPredType -> TcPredType -> TcCoercion
mkUnivCo
      (CommandLineOption -> UnivCoProvenance
PluginProv (CommandLineOption -> UnivCoProvenance)
-> CommandLineOption -> UnivCoProvenance
forall a b. (a -> b) -> a -> b
$ CommandLineOption
"ghc-typelits-presburger: extractProof")
      Role
Representational
      (TyCon -> TcPredType
mkTyConTy (Int -> TyCon
cTupleTyCon Int
0))
      TcPredType
prd
#endif
extractProof PredTree
_ = Maybe EvTerm
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 = FastString -> [FastString] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem FastString
eqReasoning [FastString]
packs
  ([TyCon]
isEmpties, [TyCon]
isTrues) <-
    if Bool
eqThere
      then do
        CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: equational-reasoning activated!" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> SDoc
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 (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 (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"Empty"))
        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 (CommandLineOption -> OccName
mkTcOcc CommandLineOption
"IsTrue")
        ([TyCon], [TyCon]) -> TcPluginM ([TyCon], [TyCon])
forall a. a -> TcPluginM a
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." (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> SDoc
forall a. Outputable a => a -> SDoc
ppr ()
        ([TyCon], [TyCon]) -> TcPluginM ([TyCon], [TyCon])
forall a. a -> TcPluginM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])

  TyCon
eqTyCon_ <- TcPluginM TyCon
getEqTyCon
  TyCon
eqBoolTyCon <- TcPluginM TyCon
getEqBoolTyCon
  TyCon
eqWitCon_ <- TcPluginM TyCon
getEqWitnessTyCon
  Maybe TyCon
assertTy <- TcPluginM (Maybe TyCon)
lookupAssertTyCon
  TyCon
voidTyCon <- TcPluginM TyCon
getVoidTyCon
  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
=<< 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 <- Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
maybeToList (Maybe TyCon -> [TyCon])
-> TcPluginM (Maybe TyCon) -> TcPluginM [TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyNot
  [TyCon]
tyAnd <- Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
maybeToList (Maybe TyCon -> [TyCon])
-> TcPluginM (Maybe TyCon) -> TcPluginM [TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyAnd
  [TyCon]
tyOr <- Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
maybeToList (Maybe TyCon -> [TyCon])
-> TcPluginM (Maybe TyCon) -> TcPluginM [TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyOr
  [TyCon]
tyIf <- Maybe TyCon -> [TyCon]
forall a. Maybe a -> [a]
maybeToList (Maybe TyCon -> [TyCon])
-> TcPluginM (Maybe TyCon) -> TcPluginM [TyCon]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM (Maybe TyCon)
lookupTyIf
  let trans :: Translation
trans =
        Translation
forall a. Monoid a => a
mempty
          { isEmpty = isEmpties
          , assertTy = maybeToList assertTy
          , tyEq = [eqTyCon_]
          , tyNot
          , tyAnd
          , tyOr
          , tyIf
          , ordCond = F.toList mOrdCond
          , tyEqWitness = [eqWitCon_]
          , tyEqBool = [eqBoolTyCon]
          , isTrue = isTrues
          , voids = [voidTyCon]
          , natMinus = [typeNatSubTyCon]
          , natPlus = [typeNatAddTyCon]
          , natTimes = [typeNatMulTyCon]
          , natExp = [typeNatExpTyCon]
          , falseData = [promotedFalseDataCon]
          , trueData = [promotedTrueDataCon]
          , natLeqBool = [tyLeqB]
          , natLeq = [nLeq]
          , natGeqBool = F.toList mTyGeqB
          , natGeq = F.toList mTyGeqP
          , natGtBool = F.toList mTyGtB
          , natGt = F.toList mTyGtP
          , natLtBool = F.toList mTyLtB
          , natLt = F.toList mTyLtP
          , natCompare = typeNatCmpTyCon : F.toList mtyGenericCompare
          , orderingEQ = [promotedEQDataCon]
          , orderingLT = [promotedLTDataCon]
          , orderingGT = [promotedGTDataCon]
          }
  CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"Final translation: " (Maybe TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe TyCon
mTyGeqB)
  Translation -> TcPluginM Translation
forall a. a -> TcPluginM a
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 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 -> TcPredType
deconsPred = CtEvidence -> TcPredType
ctEvPred (CtEvidence -> TcPredType)
-> (Ct -> CtEvidence) -> Ct -> TcPredType
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 (Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
t1, TcPredType
t2]))
  | TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPred (TyConApp TyCon
con [TcPredType
t1, TcPredType
_])
  | TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
assertTy Translation
forall a. Given a => a
given = TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
t1
toPresburgerPred TcPredType
ty
  | Just (TyCon
con, []) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PTrue
  | Just (TyCon
con, []) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. Monad m => a -> m a
return Prop
PFalse
  | cls :: PredTree
cls@(EqPred EqRel
NomEq TcPredType
_ TcPredType
_) <- TcPredType -> PredTree
classifyPredType TcPredType
ty =
    PredTree -> Machine Prop
Given Translation => PredTree -> Machine Prop
toPresburgerPredTree PredTree
cls
  | TcPredType -> Bool
isEqPred TcPredType
ty = PredTree -> Machine Prop
Given Translation => PredTree -> Machine Prop
toPresburgerPredTree (PredTree -> Machine Prop) -> PredTree -> Machine Prop
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 TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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) =
    PredTree -> Machine Prop
Given Translation => PredTree -> Machine Prop
toPresburgerPredTree (PredTree -> Machine Prop) -> PredTree -> Machine Prop
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]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- l (:~: {k}) r
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyEqWitness Translation
forall a. Given a => a
given =
    PredTree -> Machine Prop
Given Translation => PredTree -> Machine Prop
toPresburgerPredTree (PredTree -> Machine Prop) -> PredTree -> Machine Prop
forall a b. (a -> b) -> a -> b
$ EqRel -> TcPredType -> TcPredType -> PredTree
EqPred EqRel
NomEq TcPredType
l TcPredType
r
  | Just (TyCon
con, [TcPredType
l]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- Empty l => ...
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- IsTrue l =>
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
isTrue Translation
forall a. Given a => a
given =
    TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- Not p (from Data.Type.Bool)
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyNot 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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l
  | Just (TyCon
con, [TcPredType
l, TcPredType
r]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- p && q (from Data.Type.Bool)
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyAnd 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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
r
  | Just (TyCon
con, [TcPredType
l, TcPredType
r]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- p || q (from Data.Type.Bool)
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyOr 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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
l MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
r
  | Just (TyCon
con, Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
3 -> [TcPredType
p, TcPredType
t, TcPredType
f]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty -- If p t f (from Data.Type.Bool)
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyIf Translation
forall a. Given a => a
given = do
    Prop
p' <- TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
    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
<$> ((Prop
p' Prop -> Prop -> Prop
:&&) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
t) 
      MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ((Prop -> Prop
Not Prop
p'Prop -> Prop -> Prop
:&&) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
f)
  | Just (TyCon
con, [TcPredType
t1, TcPredType
t2]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
ty
    , (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
t1 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind
    , (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
t2 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind 
    , Just Expr -> Expr -> Prop
p <- TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Prop)]
Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic =
      Expr -> Expr -> Prop
p (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
  | Just DataCond{TcPredType
CondCases
lhs :: TcPredType
rhs :: TcPredType
condCases :: CondCases
lhs :: DataCond -> TcPredType
rhs :: DataCond -> TcPredType
condCases :: DataCond -> CondCases
..} <- TcPredType -> Maybe DataCond
Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
ty = do -- OrdCond
      CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
  | Bool
otherwise = Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Prop
parsePred Translation
forall a. Given a => a
given TcPredType -> Machine Expr
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) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
t
  let !n :: Int
n = [TcPredType] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TcPredType]
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, [TcPredType]) -> Maybe (TyCon, [TcPredType])
forall a. a -> Maybe a
forall (m :: * -> *) a. Monad m => a -> m a
return (TyCon
con, Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
drop (Int
n Int -> Int -> Int
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
(Int -> CondCases -> ShowS)
-> (CondCases -> CommandLineOption)
-> ([CondCases] -> ShowS)
-> Show CondCases
forall a.
(Int -> a -> ShowS)
-> (a -> CommandLineOption) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CondCases -> ShowS
showsPrec :: Int -> CondCases -> ShowS
$cshow :: CondCases -> CommandLineOption
show :: CondCases -> CommandLineOption
$cshowList :: [CondCases] -> ShowS
showList :: [CondCases] -> ShowS
Show, CondCases -> CondCases -> Bool
(CondCases -> CondCases -> Bool)
-> (CondCases -> CondCases -> Bool) -> Eq CondCases
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CondCases -> CondCases -> Bool
== :: CondCases -> CondCases -> Bool
$c/= :: CondCases -> CondCases -> Bool
/= :: CondCases -> CondCases -> Bool
Eq, Eq CondCases
Eq CondCases =>
(CondCases -> CondCases -> Ordering)
-> (CondCases -> CondCases -> Bool)
-> (CondCases -> CondCases -> Bool)
-> (CondCases -> CondCases -> Bool)
-> (CondCases -> CondCases -> Bool)
-> (CondCases -> CondCases -> CondCases)
-> (CondCases -> CondCases -> CondCases)
-> Ord 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
$ccompare :: CondCases -> CondCases -> Ordering
compare :: CondCases -> CondCases -> Ordering
$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
>= :: CondCases -> CondCases -> Bool
$cmax :: CondCases -> CondCases -> CondCases
max :: CondCases -> CondCases -> CondCases
$cmin :: CondCases -> CondCases -> CondCases
min :: CondCases -> CondCases -> CondCases
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) = (Expr -> Prop) -> Expr -> Expr -> Prop
forall a b. a -> b -> a
const ((Expr -> Prop) -> Expr -> Expr -> Prop)
-> (Expr -> Prop) -> Expr -> Expr -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Expr -> Prop
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) = (Expr -> Prop) -> Expr -> Expr -> Prop
forall a b. a -> b -> a
const ((Expr -> Prop) -> Expr -> Expr -> Prop)
-> (Expr -> Prop) -> Expr -> Expr -> Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Expr -> Prop
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, Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
4 -> [TcPredType
cmp, TcPredType
ltTy, TcPredType
eqTy, TcPredType
gtTy]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe TcPredType
ty
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
ordCond Translation
forall a. Given a => a
given
  (TyCon
cmpCon, Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
lhs, TcPredType
rhs]) <- (() :: Constraint) => TcPredType -> Maybe (TyCon, [TcPredType])
TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConApp_maybe  TcPredType
cmp
  Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ TyCon
cmpCon TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
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
ltCase :: Bool
eqCase :: Bool
gtCase :: Bool
ltCase :: Bool
eqCase :: Bool
gtCase :: Bool
..}
  DataCond -> Maybe DataCond
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DataCond{TcPredType
CondCases
lhs :: TcPredType
rhs :: TcPredType
condCases :: CondCases
lhs :: TcPredType
rhs :: TcPredType
condCases :: CondCases
..}

decodeTyBool :: Type -> Maybe Bool
decodeTyBool :: TcPredType -> Maybe Bool
decodeTyBool TcPredType
ty = do
  TyCon
con <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
ty
  (Bool
True Bool -> Maybe () -> Maybe Bool
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
con TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
promotedTrueDataCon))
    Maybe Bool -> Maybe Bool -> Maybe Bool
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Bool
False Bool -> Maybe () -> Maybe Bool
forall a b. a -> Maybe b -> Maybe a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$ Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TyCon
con TyCon -> TyCon -> Bool
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
  | Bool -> (TyCon -> Bool) -> Maybe TyCon -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
false =
    Prop -> Prop
Not (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
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 TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natLeqBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natLtBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natGtBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natGeqBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
       else 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
b) 
  | Bool -> (TyCon -> Bool) -> Maybe TyCon -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
b =
    TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
b TcPredType
p) 
  | Bool -> (TyCon -> Bool) -> Maybe TyCon -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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
$ TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
b =
    TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
p TcPredType
q) -- (p :: Bool) ~ (q :: Bool)
  | (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
p TcPredType -> TcPredType -> Bool
`eqType` TyCon -> TcPredType
mkTyConTy TyCon
promotedBoolTyCon = do
    StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT ParseEnv TcPluginM ()
 -> MaybeT (StateT ParseEnv TcPluginM) ())
-> StateT ParseEnv TcPluginM ()
-> MaybeT (StateT ParseEnv TcPluginM) ()
forall a b. (a -> b) -> a -> b
$ TcPluginM () -> StateT ParseEnv TcPluginM ()
forall (m :: * -> *) a. Monad m => m a -> StateT ParseEnv m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (TcPluginM () -> StateT ParseEnv TcPluginM ())
-> TcPluginM () -> StateT ParseEnv TcPluginM ()
forall a b. (a -> b) -> a -> b
$ CommandLineOption -> SDoc -> TcPluginM ()
tcPluginTrace CommandLineOption
"pres: EQBOOL:" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ (TcPredType, TcPredType) -> SDoc
forall a. Outputable a => a -> SDoc
ppr (TcPredType
p, TcPredType
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
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p
      MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
q
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
n TcPredType
m) -- (n :: Nat) ~ (m :: Nat)
  | (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
n TcPredType -> TcPredType -> Bool
`eqType` TcPredType
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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
toPresburgerPredTree (EqPred EqRel
_ TcPredType
t1 TcPredType
t2) -- CmpNat a b ~ CmpNat c d
  | Just (TyCon
con, [TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t1
    , Just (TyCon
con', [TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo -> [TcPredType
c, TcPredType
d]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t2
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 a. Eq a => a -> [a] -> 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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
b)
      MaybeT (StateT ParseEnv TcPluginM) (Prop -> Prop)
-> Machine Prop -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
c MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
d)
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) -- CmpNat a b ~ x
  | Just (TyCon
con, [TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t1
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
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 a. a -> StateT ParseEnv TcPluginM a
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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
b
toPresburgerPredTree (EqPred EqRel
NomEq TcPredType
t1 TcPredType
t2) -- x ~ CmpNat a b
  | Just (TyCon
con, [TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo -> [TcPredType
a, TcPredType
b]) <- TcPredType -> Maybe (TyCon, [TcPredType])
splitTyConAppLastBin TcPredType
t2
    , TyCon
con TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> 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 <- TcPredType -> Maybe TyCon
tyConAppTyCon_maybe TcPredType
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 a. a -> StateT ParseEnv TcPluginM a
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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
a
      MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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
lhs :: DataCond -> TcPredType
rhs :: DataCond -> TcPredType
condCases :: DataCond -> CondCases
lhs :: TcPredType
rhs :: TcPredType
condCases :: CondCases
..} <- TcPredType -> Maybe DataCond
Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
cond = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
    Machine Prop
-> (Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p) 
      (\Bool
q -> if Bool
q then Prop -> Machine Prop
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else Prop -> Machine Prop
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Machine Prop) -> Prop -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      (Maybe Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
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
lhs :: DataCond -> TcPredType
rhs :: DataCond -> TcPredType
condCases :: DataCond -> CondCases
lhs :: TcPredType
rhs :: TcPredType
condCases :: CondCases
..} <- TcPredType -> Maybe DataCond
Given Translation => TcPredType -> Maybe DataCond
parseOrdCond TcPredType
p = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
lhs
          MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
rhs
    Machine Prop
-> (Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
cond) 
      (\Bool
q -> if Bool
q then Prop -> Machine Prop
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else Prop -> Machine Prop
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Machine Prop) -> Prop -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      (Maybe Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
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] <- Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
2 [TcPredType]
ts
    , (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
t1 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
typeNatKind
    , (() :: Constraint) => TcPredType -> TcPredType
TcPredType -> TcPredType
typeKind TcPredType
t2 TcPredType -> TcPredType -> Bool
`eqType` TcPredType
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 a. a -> StateT ParseEnv TcPluginM a
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 a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t1 MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
-> Machine Expr -> Machine Prop
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t2
toPresburgerPredTree PredTree
_ = Machine Prop
forall a. MaybeT (StateT ParseEnv TcPluginM) a
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 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]
    [(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]
tyEqBool Translation
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 -> Expr -> Machine Expr
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
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
$ TcTyVar -> Unique
forall a. Uniquable a => a -> Unique
getUnique TcTyVar
t
  TyConApp TyCon
tc (Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
3 -> [TcPredType
p, TcPredType
t, TcPredType
f])
    | TyCon
tc TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
tyIf Translation
forall a. Given a => a
given ->
      Prop -> Expr -> Expr -> Expr
If (Prop -> Expr -> Expr -> Expr)
-> Machine Prop
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Prop
Given Translation => TcPredType -> Machine Prop
toPresburgerPred TcPredType
p MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
t MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
f 
  TyConApp TyCon
tc (Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
4 -> [TcPredType
cmpNM, TcPredType
l, TcPredType
e, TcPredType
g])
    | TyCon
tc TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
ordCond Translation
forall a. Given a => a
given
    , TyConApp TyCon
cmp (Int -> [TcPredType] -> [TcPredType]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [TcPredType
n, TcPredType
m]) <- TcPredType
cmpNM
    , TyCon
cmp TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natCompare Translation
forall a. Given a => a
given
    , (TcPredType -> Bool) -> [TcPredType] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((TypeEq -> [TypeEq] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TcPredType -> TypeEq
TypeEq TcPredType
n, TcPredType -> TypeEq
TypeEq TcPredType
m]) (TypeEq -> Bool) -> (TcPredType -> TypeEq) -> TcPredType -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcPredType -> TypeEq
TypeEq) [TcPredType
l,TcPredType
e,TcPredType
g]
    -> TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> TcPredType
-> Machine Expr
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 Translation
forall a. Given a => a
given TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty
      Machine Expr -> Machine Expr -> Machine Expr
forall a.
MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> TyCon -> [TcPredType] -> Machine Expr
body TyCon
tc [TcPredType]
ts
      Machine Expr -> Machine Expr -> Machine Expr
forall a.
MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var (Name -> Expr) -> (TcTyVar -> Name) -> TcTyVar -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName (Int -> Name) -> (TcTyVar -> Int) -> TcTyVar -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey (Unique -> Int) -> (TcTyVar -> Unique) -> TcTyVar -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTyVar -> Unique
forall a. Uniquable a => a -> Unique
getUnique (TcTyVar -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) TcTyVar -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> MaybeT (StateT ParseEnv TcPluginM) TcTyVar
toVar TcPredType
t
  LitTy (NumTyLit Integer
n) -> Expr -> Machine Expr
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Expr
K Integer
n)
  LitTy TyLit
_ -> Machine Expr
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
  TcPredType
t ->
    Translation
-> (TcPredType -> Machine Expr) -> TcPredType -> Machine Expr
parseExpr Translation
forall a. Given a => a
given TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
ty
      Machine Expr -> Machine Expr -> Machine Expr
forall a.
MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Name -> Expr
Var (Name -> Expr) -> (TcTyVar -> Name) -> TcTyVar -> Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Name
toName (Int -> Name) -> (TcTyVar -> Int) -> TcTyVar -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Unique -> Int
getKey (Unique -> Int) -> (TcTyVar -> Unique) -> TcTyVar -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TcTyVar -> Unique
forall a. Uniquable a => a -> Unique
getUnique (TcTyVar -> Expr)
-> MaybeT (StateT ParseEnv TcPluginM) TcTyVar -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> MaybeT (StateT ParseEnv TcPluginM) 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 TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
con
              , [TcPredType
tl, TcPredType
tr] <- [TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo [TcPredType]
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
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
tl MaybeT (StateT ParseEnv TcPluginM) (Expr -> b)
-> Machine Expr -> MaybeT (StateT ParseEnv TcPluginM) b
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
tr
            | Bool
otherwise = MaybeT (StateT ParseEnv TcPluginM) b
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
       in case [TcPredType]
ts of
            [TcPredType
tl, TcPredType
tr] | TyCon
tc TyCon -> [TyCon] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
natTimes Translation
forall a. Given a => a
given ->
              case (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
tl, TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
tr) of
                (LitTy (NumTyLit Integer
n), LitTy (NumTyLit Integer
m)) -> Expr -> Machine Expr
forall a. a -> MaybeT (StateT ParseEnv TcPluginM) a
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), TcPredType
x) -> Integer -> Expr -> Expr
(:*) Integer
n (Expr -> Expr) -> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
x
                (TcPredType
x, LitTy (NumTyLit Integer
n)) -> Integer -> Expr -> Expr
(:*) Integer
n (Expr -> Expr) -> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
x
                (TcPredType, TcPredType)
_ -> Machine Expr
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero
            [TcPredType]
_ ->
              [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
                     ]
                  [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
Min
                     | TyCon
con <- Translation -> [TyCon]
natMin 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
Max
                     | TyCon
con <- Translation -> [TyCon]
natMin Translation
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 (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
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 (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
n MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
-> Machine Expr -> Machine Expr
forall a b.
MaybeT (StateT ParseEnv TcPluginM) (a -> b)
-> MaybeT (StateT ParseEnv TcPluginM) a
-> MaybeT (StateT ParseEnv TcPluginM) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TcPredType -> Machine Expr
Given Translation => TcPredType -> Machine Expr
toPresburgerExp TcPredType
m
  | Bool
otherwise = Machine Expr
forall a. MaybeT (StateT ParseEnv TcPluginM) a
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- simplTypeCmp :: Type -> Type

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

simpleExp :: Given Translation => Type -> Type
simpleExp :: Given Translation => TcPredType -> TcPredType
simpleExp (AppTy TcPredType
t1 TcPredType
t2) = TcPredType -> TcPredType -> TcPredType
AppTy (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t1) (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
simpleExp (FunTy FunTyFlag
f TcPredType
m TcPredType
t1 TcPredType
t2) = FunTyFlag -> TcPredType -> TcPredType -> TcPredType -> TcPredType
FunTy FunTyFlag
f TcPredType
m (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t1) (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
simpleExp (ForAllTy ForAllTyBinder
t1 TcPredType
t2) = ForAllTyBinder -> TcPredType -> TcPredType
ForAllTy ForAllTyBinder
t1 (TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp TcPredType
t2)
simpleExp (TyConApp TyCon
tc ([TcPredType] -> [TcPredType]
forall a. [a] -> [a]
lastTwo -> [TcPredType]
ts)) =
  TcPredType -> Maybe TcPredType -> TcPredType
forall a. a -> Maybe a -> a
fromMaybe (TyCon -> [TcPredType] -> TcPredType
TyConApp TyCon
tc ((TcPredType -> TcPredType) -> [TcPredType] -> [TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp [TcPredType]
ts)) (Maybe TcPredType -> TcPredType) -> Maybe TcPredType -> TcPredType
forall a b. (a -> b) -> a -> b
$
    [Maybe TcPredType] -> Maybe TcPredType
forall (t :: * -> *) (f :: * -> *) a.
(Foldable t, Alternative f) =>
t (f a) -> f a
asum
      ( ((TyCon, Integer -> Integer -> Integer) -> Maybe TcPredType)
-> [(TyCon, Integer -> Integer -> Integer)] -> [Maybe TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map (TyCon, Integer -> Integer -> Integer) -> Maybe TcPredType
simpler ([(TyCon, Integer -> Integer -> Integer)] -> [Maybe TcPredType])
-> [(TyCon, Integer -> Integer -> Integer)] -> [Maybe TcPredType]
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 TcPredType
simpler (TyCon
con, Integer -> Integer -> Integer
op)
      | TyCon
con TyCon -> TyCon -> Bool
forall a. Eq a => a -> a -> Bool
== TyCon
tc
        , [TcPredType
tl, TcPredType
tr] <- (TcPredType -> TcPredType) -> [TcPredType] -> [TcPredType]
forall a b. (a -> b) -> [a] -> [b]
map TcPredType -> TcPredType
Given Translation => TcPredType -> TcPredType
simpleExp [TcPredType]
ts =
        TcPredType -> Maybe TcPredType
forall a. a -> Maybe a
Just (TcPredType -> Maybe TcPredType) -> TcPredType -> Maybe TcPredType
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 = Maybe TcPredType
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) <- 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, TcTyVar)]
-> ((TypeEq, TcTyVar) -> TcPluginM CtEvidence) -> TcPluginM ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (ParseEnv -> [(TypeEq, TcTyVar)]
forall k a. Map k a -> [(k, a)]
M.toList ParseEnv
dic) (((TypeEq, TcTyVar) -> TcPluginM CtEvidence) -> TcPluginM ())
-> ((TypeEq, TcTyVar) -> TcPluginM CtEvidence) -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ \(TypeEq TcPredType
ty, TcTyVar
var) -> do
    CtLoc
loc <- TcM CtLoc -> TcPluginM CtLoc
forall a. TcM a -> TcPluginM a
unsafeTcPluginTcM (TcM CtLoc -> TcPluginM CtLoc) -> TcM CtLoc -> TcPluginM CtLoc
forall a b. (a -> b) -> a -> b
$ CtOrigin -> Maybe TypeOrKind -> TcM CtLoc
getCtLocM (CommandLineOption -> CtOrigin
Shouldn'tHappenOrigin CommandLineOption
"runMachine dummy wanted") Maybe TypeOrKind
forall a. Maybe a
Nothing
    CtLoc -> TcPredType -> TcPluginM CtEvidence
newWanted CtLoc
loc (TcPredType -> TcPluginM CtEvidence)
-> TcPredType -> TcPluginM CtEvidence
forall a b. (a -> b) -> a -> b
$ Role -> TcPredType -> TcPredType -> TcPredType
mkPrimEqPredRole Role
Nominal (TcTyVar -> TcPredType
mkTyVarTy TcTyVar
var) TcPredType
ty
  Maybe a -> TcPluginM (Maybe a)
forall a. a -> TcPluginM a
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe a
ma

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