{-# 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 #-}

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

import Class (classTyCon)
import Control.Applicative ((<|>))
import Control.Arrow (second)
import Control.Monad (forM, 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)
#if MIN_VERSION_ghc(8,8,1)
import TysWiredIn (eqTyConName)
#else
import PrelNames (eqTyConName)
#endif

#if MIN_VERSION_ghc(8,6,0)
import Plugins (purePlugin)
import GhcPlugins (InstalledUnitId, PackageName(..), lookupPackageName, fsToUnitId, lookupPackage)
#endif

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)
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 FastString
import GHC.TypeLits.Presburger.Compat
import HscTypes (HscEnv (hsc_dflags))
import Module (InstalledUnitId (InstalledUnitId))
import Outputable (showSDocUnsafe)
import Packages (initPackages)
import PrelNames
import TcPluginM
  ( getTopEnv,
    lookupOrig,
    newFlexiTyVar,
    newWanted,
    tcLookupClass,
    tcPluginIO,
  )
import Type (mkTyVarTy)
import TysWiredIn
  ( promotedEQDataCon,
    promotedGTDataCon,
    promotedLTDataCon,
  )
import Var

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

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

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

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

varsExpr :: Expr -> [SAT.Name]
varsExpr :: Expr -> [Name]
varsExpr (Expr
e :+ Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Expr
e :- Expr
v) = [Name] -> [Name]
forall a. Eq a => [a] -> [a]
nub ([Name] -> [Name]) -> [Name] -> [Name]
forall a b. (a -> b) -> a -> b
$ Expr -> [Name]
varsExpr Expr
e [Name] -> [Name] -> [Name]
forall a. [a] -> [a] -> [a]
++ Expr -> [Name]
varsExpr Expr
v
varsExpr (Integer
_ :* Expr
v) = Expr -> [Name]
varsExpr Expr
v
varsExpr (Negate Expr
e) = Expr -> [Name]
varsExpr Expr
e
varsExpr (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
readListPrec :: ReadPrec [PluginMode]
$creadListPrec :: ReadPrec [PluginMode]
readPrec :: ReadPrec PluginMode
$creadPrec :: ReadPrec PluginMode
readList :: ReadS [PluginMode]
$creadList :: ReadS [PluginMode]
readsPrec :: Int -> ReadS PluginMode
$creadsPrec :: Int -> ReadS PluginMode
Read, Int -> PluginMode -> ShowS
[PluginMode] -> ShowS
PluginMode -> String
(Int -> PluginMode -> ShowS)
-> (PluginMode -> String)
-> ([PluginMode] -> ShowS)
-> Show PluginMode
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PluginMode] -> ShowS
$cshowList :: [PluginMode] -> ShowS
show :: PluginMode -> String
$cshow :: PluginMode -> String
showsPrec :: Int -> PluginMode -> ShowS
$cshowsPrec :: Int -> PluginMode -> ShowS
Show, PluginMode -> PluginMode -> Bool
(PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool) -> Eq PluginMode
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: PluginMode -> PluginMode -> Bool
$c/= :: PluginMode -> PluginMode -> Bool
== :: PluginMode -> PluginMode -> Bool
$c== :: PluginMode -> PluginMode -> Bool
Eq, Eq PluginMode
Eq PluginMode
-> (PluginMode -> PluginMode -> Ordering)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> Bool)
-> (PluginMode -> PluginMode -> PluginMode)
-> (PluginMode -> PluginMode -> PluginMode)
-> Ord PluginMode
PluginMode -> PluginMode -> Bool
PluginMode -> PluginMode -> Ordering
PluginMode -> PluginMode -> PluginMode
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: PluginMode -> PluginMode -> PluginMode
$cmin :: PluginMode -> PluginMode -> PluginMode
max :: PluginMode -> PluginMode -> PluginMode
$cmax :: PluginMode -> PluginMode -> PluginMode
>= :: PluginMode -> PluginMode -> Bool
$c>= :: PluginMode -> PluginMode -> Bool
> :: PluginMode -> PluginMode -> Bool
$c> :: PluginMode -> PluginMode -> Bool
<= :: PluginMode -> PluginMode -> Bool
$c<= :: PluginMode -> PluginMode -> Bool
< :: PluginMode -> PluginMode -> Bool
$c< :: PluginMode -> PluginMode -> Bool
compare :: PluginMode -> PluginMode -> Ordering
$ccompare :: PluginMode -> PluginMode -> Ordering
$cp1Ord :: Eq PluginMode
Ord)

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

presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin :: TcPluginM Translation -> PluginMode -> TcPlugin
presburgerPlugin TcPluginM Translation
trans PluginMode
mode =
  String -> TcPlugin -> TcPlugin
tracePlugin
    String
"typelits-presburger"
    TcPlugin :: forall s.
TcPluginM s
-> (s -> TcPluginSolver) -> (s -> TcPluginM ()) -> TcPlugin
TcPlugin
      { tcPluginInit :: TcPluginM ()
tcPluginInit = () -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      , tcPluginSolve :: () -> TcPluginSolver
tcPluginSolve = PluginMode -> TcPluginM Translation -> () -> TcPluginSolver
decidePresburger PluginMode
mode TcPluginM Translation
trans
      , tcPluginStop :: () -> TcPluginM ()
tcPluginStop = TcPluginM () -> () -> TcPluginM ()
forall a b. a -> b -> a
const (TcPluginM () -> () -> TcPluginM ())
-> TcPluginM () -> () -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ () -> TcPluginM ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
      }

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

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

    loopExp :: Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp e :: Expr
e@(Negate Expr
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive (Expr -> RWST r (Set Prop) (Set Expr) m Expr)
-> (Expr -> Expr) -> Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Expr -> Expr
Negate (Expr -> RWST r (Set Prop) (Set Expr) m Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
e
    loopExp (Expr
l :- Expr
r) = do
      Expr
e <- Expr -> Expr -> Expr
(:-) (Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
      Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) r.
Monad m =>
Expr -> RWST r (Set Prop) (Set Expr) m Expr
withPositive Expr
e
    loopExp (Expr
l :+ Expr
r) = Expr -> Expr -> Expr
(:+) (Expr -> Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
r
    loopExp v :: Expr
v@Var {} = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
v
    loopExp (Integer
c :* Expr
e)
      | Integer
c Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
0 = (Integer
c Integer -> Expr -> Expr
:*) (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
e
      | Bool
otherwise = (Integer -> Integer
forall a. Num a => a -> a
negate Integer
c Integer -> Expr -> Expr
:*) (Expr -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp (Expr -> Expr
Negate Expr
e)
    loopExp (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 (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 (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 (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 (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 e :: Expr
e@(K Integer
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

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

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

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

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

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

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

defaultTranslation :: TcPluginM Translation
defaultTranslation :: TcPluginM Translation
defaultTranslation = do
  DynFlags
dflags <- HscEnv -> DynFlags
hsc_dflags (HscEnv -> DynFlags) -> TcPluginM HscEnv -> TcPluginM DynFlags
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TcPluginM HscEnv
getTopEnv
  (DynFlags
_, [PreloadUnitId]
packs) <- IO (DynFlags, [PreloadUnitId])
-> TcPluginM (DynFlags, [PreloadUnitId])
forall a. IO a -> TcPluginM a
tcPluginIO (IO (DynFlags, [PreloadUnitId])
 -> TcPluginM (DynFlags, [PreloadUnitId]))
-> IO (DynFlags, [PreloadUnitId])
-> TcPluginM (DynFlags, [PreloadUnitId])
forall a b. (a -> b) -> a -> b
$ DynFlags -> IO (DynFlags, [PreloadUnitId])
initPackages DynFlags
dflags
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"pres: packs" (SDoc -> TcPluginM ()) -> SDoc -> TcPluginM ()
forall a b. (a -> b) -> a -> b
$ [FastString] -> SDoc
forall a. Outputable a => a -> SDoc
ppr ((PreloadUnitId -> FastString) -> [PreloadUnitId] -> [FastString]
forall a b. (a -> b) -> [a] -> [b]
map (\(InstalledUnitId FastString
p) -> FastString
p) [PreloadUnitId]
packs)
  let eqThere :: Bool
eqThere = Bool -> Maybe Bool -> Bool
forall a. a -> Maybe a -> a
fromMaybe Bool
False (Maybe Bool -> Bool) -> Maybe Bool -> Bool
forall a b. (a -> b) -> a -> b
$
        [Bool] -> Maybe Bool
forall a. [a] -> Maybe a
listToMaybe ([Bool] -> Maybe Bool) -> [Bool] -> Maybe Bool
forall a b. (a -> b) -> a -> b
$ do
          InstalledUnitId FastString
pname <- [PreloadUnitId]
packs
          String
rest <-
            Maybe String -> [String]
forall a. Maybe a -> [a]
maybeToList (Maybe String -> [String]) -> Maybe String -> [String]
forall a b. (a -> b) -> a -> b
$
              String -> String -> Maybe String
forall a. Eq a => [a] -> [a] -> Maybe [a]
L.stripPrefix String
"equational-reasoning-" (String -> Maybe String) -> String -> Maybe String
forall a b. (a -> b) -> a -> b
$ FastString -> String
unpackFS FastString
pname
          Bool -> [Bool]
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Bool -> [Bool]) -> Bool -> [Bool]
forall a b. (a -> b) -> a -> b
$ String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
rest Bool -> Bool -> Bool
|| Char -> Bool
isDigit (String -> Char
forall a. [a] -> a
head String
rest)
  ([TyCon]
isEmpties, [TyCon]
isTrues) <-
    if Bool
eqThere
      then do
        String -> SDoc -> TcPluginM ()
tcPluginTrace String
"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 (String -> ModuleName
mkModuleName String
"Proof.Propositional.Empty") FastString
eqReasoning
        Module
pmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"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 (String -> OccName
mkTcOcc String
"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 (String -> OccName
mkTcOcc String
"IsTrue")
        ([TyCon], [TyCon]) -> TcPluginM ([TyCon], [TyCon])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([TyCon
emptyClsTyCon], [TyCon
isTrueCon_])
      else do
        String -> SDoc -> TcPluginM ()
tcPluginTrace String
"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 (f :: * -> *) a. Applicative f => a -> f a
pure ([], [])

  TyCon
eqTyCon_ <- TcPluginM TyCon
getEqTyCon
  TyCon
eqWitCon_ <- TcPluginM TyCon
getEqWitnessTyCon
  Module
vmd <- ModuleName -> FastString -> TcPluginM Module
lookupModule (String -> ModuleName
mkModuleName String
"Data.Void") (String -> FastString
fsLit String
"base")
  TyCon
voidTyCon <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
vmd (String -> OccName
mkTcOcc String
"Void")
  TyCon
nLeq <- Name -> TcPluginM TyCon
tcLookupTyCon (Name -> TcPluginM TyCon) -> TcPluginM Name -> TcPluginM TyCon
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Module -> OccName -> TcPluginM Name
lookupOrig Module
gHC_TYPENATS (String -> OccName
mkTcOcc String
"<=")
  Translation -> TcPluginM Translation
forall (m :: * -> *) a. Monad m => a -> m a
return
    Translation
forall a. Monoid a => a
mempty
      { isEmpty :: [TyCon]
isEmpty = [TyCon]
isEmpties
      , tyEq :: [TyCon]
tyEq = [TyCon
eqTyCon_]
      , tyEqWitness :: [TyCon]
tyEqWitness = [TyCon
eqWitCon_]
      , isTrue :: [TyCon]
isTrue = [TyCon]
isTrues
      , voids :: [TyCon]
voids = [TyCon
voidTyCon]
      , natMinus :: [TyCon]
natMinus = [TyCon
typeNatSubTyCon]
      , natPlus :: [TyCon]
natPlus = [TyCon
typeNatAddTyCon]
      , natTimes :: [TyCon]
natTimes = [TyCon
typeNatMulTyCon]
      , natExp :: [TyCon]
natExp = [TyCon
typeNatExpTyCon]
      , falseData :: [TyCon]
falseData = [TyCon
promotedFalseDataCon]
      , trueData :: [TyCon]
trueData = [TyCon
promotedTrueDataCon]
      , natLeqBool :: [TyCon]
natLeqBool = [TyCon
typeNatLeqTyCon]
      , natLeq :: [TyCon]
natLeq = [TyCon
nLeq]
      , natCompare :: [TyCon]
natCompare = [TyCon
typeNatCmpTyCon]
      , orderingEQ :: [TyCon]
orderingEQ = [TyCon
promotedEQDataCon]
      , orderingLT :: [TyCon]
orderingLT = [TyCon
promotedLTDataCon]
      , orderingGT :: [TyCon]
orderingGT = [TyCon
promotedGTDataCon]
      }

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

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

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

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

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

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

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

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

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

-- simplTypeCmp :: Type -> Type

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

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

type ParseEnv = M.Map TypeEq TyVar

type Machine = MaybeT (StateT ParseEnv TcPluginM)

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

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