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

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

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 (Mod Expr
l Integer
n) = Expr -> Integer -> Expr
Mod (Expr -> Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Integer -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Integer
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> RWST r (Set Prop) (Set Expr) m Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp (Div Expr
l Integer
n) = Expr -> Integer -> Expr
Div (Expr -> Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Expr
-> RWST r (Set Prop) (Set Expr) m (Integer -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Expr -> RWST r (Set Prop) (Set Expr) m Expr
loopExp Expr
l RWST r (Set Prop) (Set Expr) m (Integer -> Expr)
-> RWST r (Set Prop) (Set Expr) m Integer
-> RWST r (Set Prop) (Set Expr) m Expr
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Integer -> RWST r (Set Prop) (Set Expr) m Integer
forall (f :: * -> *) a. Applicative f => a -> f a
pure Integer
n
    loopExp e :: Expr
e@(K Integer
_) = Expr -> RWST r (Set Prop) (Set Expr) m Expr
forall (m :: * -> *) a. Monad m => a -> m a
return Expr
e

data Translation = Translation
  { Translation -> [TyCon]
isEmpty :: [TyCon]
  , Translation -> [TyCon]
ordCond :: [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]
-> [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
      , ordCond :: [TyCon]
ordCond = Translation -> [TyCon]
ordCond Translation
l [TyCon] -> [TyCon] -> [TyCon]
forall a. Semigroup a => a -> a -> a
<> Translation -> [TyCon]
ordCond Translation
r
      }

instance Monoid Translation where
  mempty :: Translation
mempty =
    Translation :: [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]
-> [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
      , ordCond :: [TyCon]
ordCond = [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
    if Maybe [(Int, Integer)] -> Bool
forall a. Maybe a -> Bool
isNothing (PropSet -> Maybe [(Int, Integer)]
checkSat PropSet
prems)
      then TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [Ct] -> TcPluginResult
TcPluginContradiction [Ct]
gs
      else TcPluginResult -> TcPluginM TcPluginResult
forall (m :: * -> *) a. Monad m => a -> m a
return (TcPluginResult -> TcPluginM TcPluginResult)
-> TcPluginResult -> TcPluginM TcPluginResult
forall a b. (a -> b) -> a -> b
$ [(EvTerm, Ct)] -> [Ct] -> TcPluginResult
TcPluginOk [] []
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
  [FastString]
packs <- TcPluginM [FastString]
preloadedUnitsM
  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
          FastString
pname <- [FastString]
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
eqBoolTyCon <- 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
dATA_TYPE_EQUALITY (String -> OccName
mkTcOcc String
"==")
  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
=<< TcPluginM Name
lookupTyNatPredLeq
  TyCon
tyLeqB <- TcPluginM TyCon
lookupTyNatBoolLeq
  Maybe TyCon
mTyLtP <- TcPluginM (Maybe TyCon)
lookupTyNatPredLt
  Maybe TyCon
mTyLtB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolLt
  Maybe TyCon
mTyGeqP <- TcPluginM (Maybe TyCon)
lookupTyNatPredGeq
  Maybe TyCon
mTyGeqB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolGeq
  Maybe TyCon
mTyGtP <- TcPluginM (Maybe TyCon)
lookupTyNatPredGt
  Maybe TyCon
mTyGtB <- TcPluginM (Maybe TyCon)
lookupTyNatBoolGt
  Maybe TyCon
mOrdCond <- TcPluginM (Maybe TyCon)
mOrdCondTyCon
  Maybe TyCon
mtyGenericCompare <- TcPluginM (Maybe TyCon)
lookupTyGenericCompare
  let trans :: Translation
trans =
        Translation
forall a. Monoid a => a
mempty
          { isEmpty :: [TyCon]
isEmpty = [TyCon]
isEmpties
          , tyEq :: [TyCon]
tyEq = [TyCon
eqTyCon_]
          , ordCond :: [TyCon]
ordCond = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mOrdCond
          , tyEqWitness :: [TyCon]
tyEqWitness = [TyCon
eqWitCon_]
          , tyEqBool :: [TyCon]
tyEqBool = [TyCon
eqBoolTyCon]
          , isTrue :: [TyCon]
isTrue = [TyCon]
isTrues
          , voids :: [TyCon]
voids = [TyCon
voidTyCon]
          , natMinus :: [TyCon]
natMinus = [TyCon
typeNatSubTyCon]
          , natPlus :: [TyCon]
natPlus = [TyCon
typeNatAddTyCon]
          , natTimes :: [TyCon]
natTimes = [TyCon
typeNatMulTyCon]
          , natExp :: [TyCon]
natExp = [TyCon
typeNatExpTyCon]
          , falseData :: [TyCon]
falseData = [TyCon
promotedFalseDataCon]
          , trueData :: [TyCon]
trueData = [TyCon
promotedTrueDataCon]
          , natLeqBool :: [TyCon]
natLeqBool = [TyCon
tyLeqB]
          , natLeq :: [TyCon]
natLeq = [TyCon
nLeq]
          , natGeqBool :: [TyCon]
natGeqBool = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGeqB
          , natGeq :: [TyCon]
natGeq = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGeqP
          , natGtBool :: [TyCon]
natGtBool = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGtB
          , natGt :: [TyCon]
natGt = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyGtP
          , natLtBool :: [TyCon]
natLtBool = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyLtB
          , natLt :: [TyCon]
natLt = Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mTyLtP
          , natCompare :: [TyCon]
natCompare = TyCon
typeNatCmpTyCon TyCon -> [TyCon] -> [TyCon]
forall a. a -> [a] -> [a]
: Maybe TyCon -> [TyCon]
forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Maybe TyCon
mtyGenericCompare
          , orderingEQ :: [TyCon]
orderingEQ = [TyCon
promotedEQDataCon]
          , orderingLT :: [TyCon]
orderingLT = [TyCon
promotedLTDataCon]
          , orderingGT :: [TyCon]
orderingGT = [TyCon
promotedGTDataCon]
          }
  String -> SDoc -> TcPluginM ()
tcPluginTrace String
"Final translation: " (Maybe TyCon -> SDoc
forall a. Outputable a => a -> SDoc
ppr Maybe TyCon
mTyGeqB)
  Translation -> TcPluginM Translation
forall (f :: * -> *) a. Applicative f => a -> f a
pure Translation
trans

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

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 (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [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]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin 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
  | Just (TyCon
con, [Type
t1, Type
t2]) <- Type -> Maybe (TyCon, [Type])
splitTyConAppLastBin Type
ty
    , 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 
    , Just Expr -> Expr -> Prop
p <- TyCon
-> [(TyCon, Expr -> Expr -> Prop)] -> Maybe (Expr -> Expr -> Prop)
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TyCon
con [(TyCon, Expr -> Expr -> Prop)]
Given Translation => [(TyCon, Expr -> Expr -> Prop)]
binPropDic =
      Expr -> Expr -> Prop
p (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
  | Just DataCond{Type
CondCases
condCases :: DataCond -> CondCases
rhs :: DataCond -> Type
lhs :: DataCond -> Type
condCases :: CondCases
rhs :: Type
lhs :: Type
..} <- Type -> Maybe DataCond
Given Translation => Type -> Maybe DataCond
parseOrdCond Type
ty = do -- OrdCond
      CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
lhs
          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
rhs
  | 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)

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

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

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

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

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


toPresburgerPredTree :: Given Translation => PredTree -> Machine Prop
toPresburgerPredTree :: 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
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
p
toPresburgerPredTree (EqPred EqRel
NomEq Type
p Type
b) -- (n :<=? m) ~ 'b
  | Just Bool
isTrue <- Type -> Maybe Bool
decodeTyBool 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 =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
       else Expr -> Expr -> Prop
(:>) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
b) -- (n :<? m) ~ b
  | Just Bool
isTrue <- Type -> Maybe Bool
decodeTyBool 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]
natLtBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:<) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
       else Expr -> Expr -> Prop
(:>=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
b) -- (n :>? m) ~ b
  | Just Bool
isTrue <- Type -> Maybe Bool
decodeTyBool 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]
natGtBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:>) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
       else Expr -> Expr -> Prop
(:<=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
b) -- (n :>=? m) ~ b
  | Just Bool
isTrue <- Type -> Maybe Bool
decodeTyBool 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]
natGeqBool Translation
forall a. Given a => a
given =
    if Bool
isTrue 
      then Expr -> Expr -> Prop
(:>=) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
       else Expr -> Expr -> Prop
(:<) (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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
b) 
  | 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 =
    Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
p
toPresburgerPredTree (EqPred EqRel
NomEq Type
b Type
p) 
  | 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 =
    Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
p
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 (EqPred EqRel
NomEq Type
cond Type
p) 
  -- OrdCond (CmpNat _ _) lt eq gt ~ ? (for GHC >= 9.2)
  | Just DataCond{Type
CondCases
condCases :: CondCases
rhs :: Type
lhs :: Type
condCases :: DataCond -> CondCases
rhs :: DataCond -> Type
lhs :: DataCond -> Type
..} <- Type -> Maybe DataCond
Given Translation => Type -> Maybe DataCond
parseOrdCond Type
cond = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
lhs
          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
rhs
    Machine Prop
-> (Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
p) 
      (\Bool
q -> if Bool
q then Prop -> Machine Prop
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else Prop -> Machine Prop
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Machine Prop) -> Prop -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      (Maybe Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Bool
decodeTyBool Type
p
  -- ? ~ OrdCond (CmpNat _ _) lt eq gt  (for GHC >= 9.2)
  | Just DataCond{Type
CondCases
condCases :: CondCases
rhs :: Type
lhs :: Type
condCases :: DataCond -> CondCases
rhs :: DataCond -> Type
lhs :: DataCond -> Type
..} <- Type -> Maybe DataCond
Given Translation => Type -> Maybe DataCond
parseOrdCond Type
p = do
    Prop
body <- CondCases -> Expr -> Expr -> Prop
fromCondCases CondCases
condCases
          (Expr -> Expr -> Prop)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Prop)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
lhs
          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
rhs
    Machine Prop
-> (Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall b a. b -> (a -> b) -> Maybe a -> b
maybe ((Prop
body Prop -> Prop -> Prop
<=>) (Prop -> Prop) -> Machine Prop -> Machine Prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Prop
Given Translation => Type -> Machine Prop
toPresburgerPred Type
cond) 
      (\Bool
q -> if Bool
q then Prop -> Machine Prop
forall (f :: * -> *) a. Applicative f => a -> f a
pure Prop
body else Prop -> Machine Prop
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Prop -> Machine Prop) -> Prop -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Prop -> Prop
Not Prop
body)
      (Maybe Bool -> Machine Prop) -> Maybe Bool -> Machine Prop
forall a b. (a -> b) -> a -> b
$ Type -> Maybe Bool
decodeTyBool Type
cond
toPresburgerPredTree (ClassPred Class
con [Type]
ts)
  -- (n :: Nat) (<=| < | > | >= | == | /=) (m :: Nat)
  | [Type
t1, Type
t2] <- Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
lastN 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]
    [(TyCon, Expr -> Expr -> Prop)]
-> [(TyCon, Expr -> Expr -> Prop)]
-> [(TyCon, Expr -> Expr -> Prop)]
forall a. [a] -> [a] -> [a]
++ [(TyCon
n, Expr -> Expr -> Prop
(:==)) | TyCon
n <- Translation -> [TyCon]
tyEqBool Translation
forall a. Given a => a
given]

toPresburgerExp :: Given Translation => Type -> Machine Expr
toPresburgerExp :: 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
  TyConApp TyCon
tc (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
lastN Int
4 -> [Type
cmpNM, Type
l, Type
e, Type
g])
    | TyCon
tc TyCon -> [TyCon] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` Translation -> [TyCon]
ordCond Translation
forall a. Given a => a
given
    , TyConApp TyCon
cmp (Int -> [Type] -> [Type]
forall a. Int -> [a] -> [a]
lastN Int
2 -> [Type
n, Type
m]) <- Type
cmpNM
    , TyCon
cmp 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
    , (Type -> Bool) -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((TypeEq -> [TypeEq] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Type -> TypeEq
TypeEq Type
n, Type -> TypeEq
TypeEq Type
m]) (TypeEq -> Bool) -> (Type -> TypeEq) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeEq
TypeEq) [Type
l,Type
e,Type
g]
    -> Type -> Type -> Type -> Type -> Type -> Machine Expr
Given Translation =>
Type -> Type -> Type -> Type -> Type -> Machine Expr
decodeMinMax Type
n Type
m Type
l Type
e Type
g
  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
n (Expr -> Expr) -> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Functor 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
n (Expr -> Expr) -> Machine Expr -> Machine Expr
forall (f :: * -> *) a b. Functor 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
                     ]

decodeMinMax :: Given Translation => Type -> Type -> Type -> Type -> Type -> Machine Expr
decodeMinMax :: Type -> Type -> Type -> Type -> Type -> Machine Expr
decodeMinMax Type
n Type
m Type
lt Type
eq Type
gt 
  | Type
lt Type -> Type -> Bool
`eqType`  Type
n Bool -> Bool -> Bool
&& Type
eq Type -> Type -> Bool
`eqType`  Type
n Bool -> Bool -> Bool
&& Type
gt Type -> Type -> Bool
`eqType` Type
m = 
    Expr -> Expr -> Expr
Min (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
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
m
  | Type
lt Type -> Type -> Bool
`eqType`  Type
n Bool -> Bool -> Bool
&& Type
eq Type -> Type -> Bool
`eqType`  Type
m Bool -> Bool -> Bool
&& Type
gt Type -> Type -> Bool
`eqType` Type
m = 
    Expr -> Expr -> Expr
Min (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
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
m
  | Type
lt Type -> Type -> Bool
`eqType` Type
m Bool -> Bool -> Bool
&& Type
eq Type -> Type -> Bool
`eqType`  Type
m Bool -> Bool -> Bool
&& Type
gt Type -> Type -> Bool
`eqType` Type
n = 
    Expr -> Expr -> Expr
Max (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
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
m
  | Type
lt Type -> Type -> Bool
`eqType` Type
m Bool -> Bool -> Bool
&& Type
eq Type -> Type -> Bool
`eqType`  Type
n Bool -> Bool -> Bool
&& Type
gt Type -> Type -> Bool
`eqType` Type
n = 
    Expr -> Expr -> Expr
Max (Expr -> Expr -> Expr)
-> Machine Expr
-> MaybeT (StateT ParseEnv TcPluginM) (Expr -> Expr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Type -> Machine Expr
Given Translation => Type -> Machine Expr
toPresburgerExp Type
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
m
  | Bool
otherwise = Machine Expr
forall (m :: * -> *) a. MonadPlus m => m a
mzero

-- 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
lastN :: Int -> [a] -> [a]
lastN :: Int -> [a] -> [a]
lastN Int
n = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Int -> [a] -> [a]) -> ([a] -> Int) -> [a] -> [a] -> [a]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
n (Int -> Int) -> ([a] -> Int) -> [a] -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Int
forall (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(9,0,0)
simpleExp (FunTy f m t1 t2) = FunTy f m (simpleExp t1) (simpleExp t2)
#else
#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
#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