{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
module Jikka.Core.Language.AssertedHint
( AssertedHint (..),
pattern EqualHint,
parseHints,
lowerBoundWithHints,
upperBoundWithHints,
isZeroWithHints,
nullWithHints,
lengthWithHints,
)
where
import Control.Monad
import Data.Semigroup
import Jikka.Core.Language.ArithmeticExpr
import Jikka.Core.Language.BuiltinPatterns
import Jikka.Core.Language.Expr
data AssertedHint
=
NotEqualHint ArithmeticExpr
|
BoundHint (Maybe ArithmeticExpr) (Maybe ArithmeticExpr)
|
LengthHint Type AssertedHint
|
AllHint Type AssertedHint
deriving (AssertedHint -> AssertedHint -> Bool
(AssertedHint -> AssertedHint -> Bool)
-> (AssertedHint -> AssertedHint -> Bool) -> Eq AssertedHint
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: AssertedHint -> AssertedHint -> Bool
$c/= :: AssertedHint -> AssertedHint -> Bool
== :: AssertedHint -> AssertedHint -> Bool
$c== :: AssertedHint -> AssertedHint -> Bool
Eq, Eq AssertedHint
Eq AssertedHint
-> (AssertedHint -> AssertedHint -> Ordering)
-> (AssertedHint -> AssertedHint -> Bool)
-> (AssertedHint -> AssertedHint -> Bool)
-> (AssertedHint -> AssertedHint -> Bool)
-> (AssertedHint -> AssertedHint -> Bool)
-> (AssertedHint -> AssertedHint -> AssertedHint)
-> (AssertedHint -> AssertedHint -> AssertedHint)
-> Ord AssertedHint
AssertedHint -> AssertedHint -> Bool
AssertedHint -> AssertedHint -> Ordering
AssertedHint -> AssertedHint -> AssertedHint
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 :: AssertedHint -> AssertedHint -> AssertedHint
$cmin :: AssertedHint -> AssertedHint -> AssertedHint
max :: AssertedHint -> AssertedHint -> AssertedHint
$cmax :: AssertedHint -> AssertedHint -> AssertedHint
>= :: AssertedHint -> AssertedHint -> Bool
$c>= :: AssertedHint -> AssertedHint -> Bool
> :: AssertedHint -> AssertedHint -> Bool
$c> :: AssertedHint -> AssertedHint -> Bool
<= :: AssertedHint -> AssertedHint -> Bool
$c<= :: AssertedHint -> AssertedHint -> Bool
< :: AssertedHint -> AssertedHint -> Bool
$c< :: AssertedHint -> AssertedHint -> Bool
compare :: AssertedHint -> AssertedHint -> Ordering
$ccompare :: AssertedHint -> AssertedHint -> Ordering
$cp1Ord :: Eq AssertedHint
Ord, Int -> AssertedHint -> ShowS
[AssertedHint] -> ShowS
AssertedHint -> String
(Int -> AssertedHint -> ShowS)
-> (AssertedHint -> String)
-> ([AssertedHint] -> ShowS)
-> Show AssertedHint
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [AssertedHint] -> ShowS
$cshowList :: [AssertedHint] -> ShowS
show :: AssertedHint -> String
$cshow :: AssertedHint -> String
showsPrec :: Int -> AssertedHint -> ShowS
$cshowsPrec :: Int -> AssertedHint -> ShowS
Show)
pattern EqualHint :: ArithmeticExpr -> AssertedHint
pattern $bEqualHint :: ArithmeticExpr -> AssertedHint
$mEqualHint :: forall r.
AssertedHint -> (ArithmeticExpr -> r) -> (Void# -> r) -> r
EqualHint l <-
(\case BoundHint (Just l) (Just r) | incrArithmeticExpr l == r -> Just l; _ -> Nothing -> Just l)
where
EqualHint ArithmeticExpr
l = Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just ArithmeticExpr
l) (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
incrArithmeticExpr ArithmeticExpr
l))
parseNilHint :: Expr -> [(VarName, AssertedHint)]
parseNilHint :: Expr -> [(VarName, AssertedHint)]
parseNilHint = \case
Equal' Type
_ (Var VarName
xs) (Nil' Type
t) -> [(VarName
xs, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (Integer -> ArithmeticExpr
integerArithmeticExpr Integer
0)) (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (Integer -> ArithmeticExpr
integerArithmeticExpr Integer
1))))]
NotEqual' Type
_ (Var VarName
xs) (Nil' Type
t) -> [(VarName
xs, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (Integer -> ArithmeticExpr
integerArithmeticExpr Integer
1)) Maybe ArithmeticExpr
forall a. Maybe a
Nothing))]
Expr
_ -> []
data Term
= VarTerm VarName
| LenTerm Type VarName
| NegatedTerm Term
deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c== :: Term -> Term -> Bool
Eq, Eq Term
Eq Term
-> (Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
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 :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmax :: Term -> Term -> Term
>= :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c< :: Term -> Term -> Bool
compare :: Term -> Term -> Ordering
$ccompare :: Term -> Term -> Ordering
$cp1Ord :: Eq Term
Ord, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Term] -> ShowS
$cshowList :: [Term] -> ShowS
show :: Term -> String
$cshow :: Term -> String
showsPrec :: Int -> Term -> ShowS
$cshowsPrec :: Int -> Term -> ShowS
Show, ReadPrec [Term]
ReadPrec Term
Int -> ReadS Term
ReadS [Term]
(Int -> ReadS Term)
-> ReadS [Term] -> ReadPrec Term -> ReadPrec [Term] -> Read Term
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Term]
$creadListPrec :: ReadPrec [Term]
readPrec :: ReadPrec Term
$creadPrec :: ReadPrec Term
readList :: ReadS [Term]
$creadList :: ReadS [Term]
readsPrec :: Int -> ReadS Term
$creadsPrec :: Int -> ReadS Term
Read)
decomposeArithmeticExpr :: Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr :: Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr Expr
e =
let es :: [ArithmeticExpr]
es = ArithmeticExpr -> [ArithmeticExpr]
splitToSumArithmeticExpr (ArithmeticExpr -> [ArithmeticExpr])
-> ArithmeticExpr -> [ArithmeticExpr]
forall a b. (a -> b) -> a -> b
$ Expr -> ArithmeticExpr
parseArithmeticExpr Expr
e
in ((Int -> [(Term, ArithmeticExpr)])
-> [Int] -> [(Term, ArithmeticExpr)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
`concatMap` [Int
0 .. [ArithmeticExpr] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ArithmeticExpr]
es Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]) ((Int -> [(Term, ArithmeticExpr)]) -> [(Term, ArithmeticExpr)])
-> (Int -> [(Term, ArithmeticExpr)]) -> [(Term, ArithmeticExpr)]
forall a b. (a -> b) -> a -> b
$ \Int
i ->
let e :: ArithmeticExpr
e = [ArithmeticExpr]
es [ArithmeticExpr] -> Int -> ArithmeticExpr
forall a. [a] -> Int -> a
!! Int
i
e' :: ArithmeticExpr
e' = [ArithmeticExpr] -> ArithmeticExpr
sumArithmeticExpr ([ArithmeticExpr] -> ArithmeticExpr)
-> [ArithmeticExpr] -> ArithmeticExpr
forall a b. (a -> b) -> a -> b
$ Int -> [ArithmeticExpr] -> [ArithmeticExpr]
forall a. Int -> [a] -> [a]
take Int
i [ArithmeticExpr]
es [ArithmeticExpr] -> [ArithmeticExpr] -> [ArithmeticExpr]
forall a. [a] -> [a] -> [a]
++ Int -> [ArithmeticExpr] -> [ArithmeticExpr]
forall a. Int -> [a] -> [a]
drop (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [ArithmeticExpr]
es
in case ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
e of
Var VarName
x -> [(VarName -> Term
VarTerm VarName
x, ArithmeticExpr
e')]
Negate' (Var VarName
x) -> [(Term -> Term
NegatedTerm (VarName -> Term
VarTerm VarName
x), ArithmeticExpr
e')]
Len' Type
t (Var VarName
x) -> [(Type -> VarName -> Term
LenTerm Type
t VarName
x, ArithmeticExpr
e')]
Negate' (Len' Type
t (Var VarName
x)) -> [(Term -> Term
NegatedTerm (Type -> VarName -> Term
LenTerm Type
t VarName
x), ArithmeticExpr
e')]
Expr
_ -> []
parseBoundHint :: Expr -> [(VarName, AssertedHint)]
parseBoundHint :: Expr -> [(VarName, AssertedHint)]
parseBoundHint = \case
Equal' Type
IntTy Expr
e (LitInt' Integer
0) -> do
(Term
x, ArithmeticExpr
e) <- Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr Expr
e
case Term
x of
VarTerm VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, ArithmeticExpr -> AssertedHint
EqualHint (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e))
NegatedTerm (VarTerm VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, ArithmeticExpr -> AssertedHint
EqualHint ArithmeticExpr
e)
LenTerm Type
t VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (ArithmeticExpr -> AssertedHint
EqualHint (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e)))
NegatedTerm (LenTerm Type
t VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (ArithmeticExpr -> AssertedHint
EqualHint ArithmeticExpr
e))
Term
_ -> []
NotEqual' Type
IntTy Expr
e (LitInt' Integer
0) -> do
(Term
x, ArithmeticExpr
e) <- Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr Expr
e
case Term
x of
VarTerm VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, ArithmeticExpr -> AssertedHint
NotEqualHint (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e))
NegatedTerm (VarTerm VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, ArithmeticExpr -> AssertedHint
NotEqualHint ArithmeticExpr
e)
LenTerm Type
t VarName
x | ArithmeticExpr -> Bool
isZeroArithmeticExpr ArithmeticExpr
e -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (Integer -> ArithmeticExpr
integerArithmeticExpr Integer
1)) Maybe ArithmeticExpr
forall a. Maybe a
Nothing))
NegatedTerm (LenTerm Type
t VarName
x) | ArithmeticExpr -> Bool
isZeroArithmeticExpr ArithmeticExpr
e -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (Integer -> ArithmeticExpr
integerArithmeticExpr Integer
1)) Maybe ArithmeticExpr
forall a. Maybe a
Nothing))
Term
_ -> []
LessEqual' Type
IntTy Expr
e (LitInt' Integer
0) -> do
(Term
x, ArithmeticExpr
e) <- Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr Expr
e
case Term
x of
VarTerm VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint Maybe ArithmeticExpr
forall a. Maybe a
Nothing (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
incrArithmeticExpr (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e))))
NegatedTerm (VarTerm VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just ArithmeticExpr
e) Maybe ArithmeticExpr
forall a. Maybe a
Nothing)
LenTerm Type
t VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint Maybe ArithmeticExpr
forall a. Maybe a
Nothing (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
incrArithmeticExpr (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e)))))
NegatedTerm (LenTerm Type
t VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just ArithmeticExpr
e) Maybe ArithmeticExpr
forall a. Maybe a
Nothing))
Term
_ -> []
LessThan' Type
IntTy Expr
e (LitInt' Integer
0) -> do
(Term
x, ArithmeticExpr
e) <- Expr -> [(Term, ArithmeticExpr)]
decomposeArithmeticExpr Expr
e
case Term
x of
VarTerm VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint Maybe ArithmeticExpr
forall a. Maybe a
Nothing (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e)))
NegatedTerm (VarTerm VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
incrArithmeticExpr ArithmeticExpr
e)) Maybe ArithmeticExpr
forall a. Maybe a
Nothing)
LenTerm Type
t VarName
x -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint Maybe ArithmeticExpr
forall a. Maybe a
Nothing (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
negateArithmeticExpr ArithmeticExpr
e))))
NegatedTerm (LenTerm Type
t VarName
x) -> (VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
x, Type -> AssertedHint -> AssertedHint
LengthHint Type
t (Maybe ArithmeticExpr -> Maybe ArithmeticExpr -> AssertedHint
BoundHint (ArithmeticExpr -> Maybe ArithmeticExpr
forall a. a -> Maybe a
Just (ArithmeticExpr -> ArithmeticExpr
incrArithmeticExpr ArithmeticExpr
e)) Maybe ArithmeticExpr
forall a. Maybe a
Nothing))
Term
_ -> []
Expr
_ -> []
parseAndHint :: Expr -> [(VarName, AssertedHint)]
parseAndHint :: Expr -> [(VarName, AssertedHint)]
parseAndHint = \case
And' Expr
e Expr
e' -> Expr -> [(VarName, AssertedHint)]
parseHints Expr
e [(VarName, AssertedHint)]
-> [(VarName, AssertedHint)] -> [(VarName, AssertedHint)]
forall a. [a] -> [a] -> [a]
++ Expr -> [(VarName, AssertedHint)]
parseHints Expr
e'
Expr
_ -> []
parseAllHint :: Expr -> [(VarName, AssertedHint)]
parseAllHint :: Expr -> [(VarName, AssertedHint)]
parseAllHint = \case
All' (Map' Type
t Type
_ (Lam VarName
x Type
_ Expr
pred) (Var VarName
xs)) -> do
(VarName
x', AssertedHint
hint) <- Expr -> [(VarName, AssertedHint)]
parseHints Expr
pred
Bool -> [()]
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> [()]) -> Bool -> [()]
forall a b. (a -> b) -> a -> b
$ VarName
x' VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
== VarName
x
(VarName, AssertedHint) -> [(VarName, AssertedHint)]
forall (m :: * -> *) a. Monad m => a -> m a
return (VarName
xs, Type -> AssertedHint -> AssertedHint
AllHint Type
t AssertedHint
hint)
Expr
_ -> []
parseHints :: Expr -> [(VarName, AssertedHint)]
parseHints :: Expr -> [(VarName, AssertedHint)]
parseHints Expr
e =
[[(VarName, AssertedHint)]] -> [(VarName, AssertedHint)]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ Expr -> [(VarName, AssertedHint)]
parseNilHint Expr
e,
Expr -> [(VarName, AssertedHint)]
parseBoundHint Expr
e,
Expr -> [(VarName, AssertedHint)]
parseAndHint Expr
e,
Expr -> [(VarName, AssertedHint)]
parseAllHint Expr
e
]
selectHints :: [(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints :: [(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
x = ((VarName, AssertedHint) -> AssertedHint)
-> [(VarName, AssertedHint)] -> [AssertedHint]
forall a b. (a -> b) -> [a] -> [b]
map (VarName, AssertedHint) -> AssertedHint
forall a b. (a, b) -> b
snd (((VarName, AssertedHint) -> Bool)
-> [(VarName, AssertedHint)] -> [(VarName, AssertedHint)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(VarName, AssertedHint)
hint -> (VarName, AssertedHint) -> VarName
forall a b. (a, b) -> a
fst (VarName, AssertedHint)
hint VarName -> VarName -> Bool
forall a. Eq a => a -> a -> Bool
== VarName
x) [(VarName, AssertedHint)]
hints)
maximum' :: Ord a => [Maybe a] -> Maybe a
maximum' :: [Maybe a] -> Maybe a
maximum' = (Max a -> a
forall a. Max a -> a
getMax (Max a -> a) -> Maybe (Max a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (Max a) -> Maybe a)
-> ([Maybe a] -> Maybe (Max a)) -> [Maybe a] -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Max a)] -> Maybe (Max a)
forall a. Monoid a => [a] -> a
mconcat ([Maybe (Max a)] -> Maybe (Max a))
-> ([Maybe a] -> [Maybe (Max a)]) -> [Maybe a] -> Maybe (Max a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe a -> Maybe (Max a)) -> [Maybe a] -> [Maybe (Max a)]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Max a
forall a. a -> Max a
Max (a -> Max a) -> Maybe a -> Maybe (Max a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
minimum' :: Ord a => [Maybe a] -> Maybe a
minimum' :: [Maybe a] -> Maybe a
minimum' = (Min a -> a
forall a. Min a -> a
getMin (Min a -> a) -> Maybe (Min a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (Min a) -> Maybe a)
-> ([Maybe a] -> Maybe (Min a)) -> [Maybe a] -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Min a)] -> Maybe (Min a)
forall a. Monoid a => [a] -> a
mconcat ([Maybe (Min a)] -> Maybe (Min a))
-> ([Maybe a] -> [Maybe (Min a)]) -> [Maybe a] -> Maybe (Min a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe a -> Maybe (Min a)) -> [Maybe a] -> [Maybe (Min a)]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Min a
forall a. a -> Min a
Min (a -> Min a) -> Maybe a -> Maybe (Min a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
lowerBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints = \case
LitInt' Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
Negate' Expr
e -> do
Integer
e <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ - (Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
Plus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
e2
Minus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- (Integer
e2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1)
Mult' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
e2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
e2
Var VarName
x ->
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
BoundHint (Just ArithmeticExpr
l) Maybe ArithmeticExpr
_ -> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
l)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
in [Maybe Integer] -> Maybe Integer
forall a. Ord a => [Maybe a] -> Maybe a
maximum' ((AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
x))
Expr
_ -> Maybe Integer
forall a. Maybe a
Nothing
upperBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints = \case
LitInt' Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1)
Negate' Expr
e -> do
Integer
e <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ - Integer
e Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
Plus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
e2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1
Minus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
e2
Mult' Expr
e1 Expr
e2 -> do
Integer
l1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
l2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer
r1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
r2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e2
Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ Integer
l1 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0 Bool -> Bool -> Bool
&& Integer
l2 Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ (Integer
r1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* (Integer
r2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
Var VarName
x ->
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
BoundHint Maybe ArithmeticExpr
_ (Just ArithmeticExpr
r) -> Integer -> Integer
forall a. Enum a => a -> a
pred (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
r)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
in [Maybe Integer] -> Maybe Integer
forall a. Ord a => [Maybe a] -> Maybe a
minimum' ((AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
x))
Expr
_ -> Maybe Integer
forall a. Maybe a
Nothing
isZeroWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool
isZeroWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool
isZeroWithHints [(VarName, AssertedHint)]
hints Expr
e =
case ([(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e, [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e) of
(Just Integer
0, Just Integer
1) -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
(Just Integer
l, Maybe Integer
_) | Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
1 -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
(Maybe Integer
_, Just Integer
r) | Integer
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
0 -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
(Maybe Integer, Maybe Integer)
_ -> Maybe Bool
forall a. Maybe a
Nothing
integerWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints = \case
LitInt' Integer
n -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
n
Negate' Expr
e -> do
Integer
e <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ - Integer
e
Plus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
e2
Minus' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
e2
Mult' Expr
e1 Expr
e2 -> do
Integer
e1 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e1
Integer
e2 <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints Expr
e2
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
e1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
e2
e :: Expr
e@(Var VarName
_) ->
case ([(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e, [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e) of
(Just Integer
l, Just Integer
r) | Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
r -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
l
(Maybe Integer, Maybe Integer)
_ -> Maybe Integer
forall a. Maybe a
Nothing
Expr
_ -> Maybe Integer
forall a. Maybe a
Nothing
nullWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool
nullWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Bool
nullWithHints [(VarName, AssertedHint)]
hints = \case
Nil' Type
_ -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
Cons' Type
_ Expr
_ Expr
_ -> Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
Range1' Expr
n -> [(VarName, AssertedHint)] -> Expr -> Maybe Bool
isZeroWithHints [(VarName, AssertedHint)]
hints Expr
n
Var VarName
xs -> do
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
LengthHint Type
_ (BoundHint (Just ArithmeticExpr
l) Maybe ArithmeticExpr
_) -> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
l)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
Integer
l <- [Maybe Integer] -> Maybe Integer
forall a. Ord a => [Maybe a] -> Maybe a
maximum' ((AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
xs))
if Integer
l Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
1
then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
else do
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
LengthHint Type
_ (NotEqualHint ArithmeticExpr
n) -> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
integerWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
n)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
let ns :: [Maybe Integer]
ns = (AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
xs)
if Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0 Maybe Integer -> [Maybe Integer] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Maybe Integer]
ns
then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
False
else do
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
LengthHint Type
_ (BoundHint Maybe ArithmeticExpr
_ (Just ArithmeticExpr
r)) -> Integer -> Integer
forall a. Enum a => a -> a
pred (Integer -> Integer) -> Maybe Integer -> Maybe Integer
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
r)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
Integer
r <- [Maybe Integer] -> Maybe Integer
forall a. Ord a => [Maybe a] -> Maybe a
minimum' ((AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
xs))
if Integer
r Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= Integer
1
then Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
True
else Maybe Bool
forall a. Maybe a
Nothing
Expr
_ -> Maybe Bool
forall a. Maybe a
Nothing
lengthWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lengthWithHints :: [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lengthWithHints [(VarName, AssertedHint)]
hints = \case
Nil' Type
_ -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0
Cons' Type
_ Expr
_ Expr
xs -> do
Integer
n <- [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lengthWithHints [(VarName, AssertedHint)]
hints Expr
xs
Integer -> Maybe Integer
forall (m :: * -> *) a. Monad m => a -> m a
return (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1
Range1' Expr
e -> case ([(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints Expr
e, [(VarName, AssertedHint)] -> Expr -> Maybe Integer
upperBoundWithHints [(VarName, AssertedHint)]
hints Expr
e) of
(Just Integer
l, Just Integer
r) | Integer
l Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
r -> Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
l
(Maybe Integer, Maybe Integer)
_ -> Maybe Integer
forall a. Maybe a
Nothing
Var VarName
xs -> do
let go :: AssertedHint -> Maybe Integer
go :: AssertedHint -> Maybe Integer
go = \case
LengthHint Type
_ (BoundHint (Just ArithmeticExpr
l) Maybe ArithmeticExpr
_) -> [(VarName, AssertedHint)] -> Expr -> Maybe Integer
lowerBoundWithHints [(VarName, AssertedHint)]
hints (ArithmeticExpr -> Expr
formatArithmeticExpr ArithmeticExpr
l)
AssertedHint
_ -> Maybe Integer
forall a. Maybe a
Nothing
let minimum' :: Ord a => [Maybe a] -> Maybe a
minimum' :: [Maybe a] -> Maybe a
minimum' = (Min a -> a
forall a. Min a -> a
getMin (Min a -> a) -> Maybe (Min a) -> Maybe a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (Min a) -> Maybe a)
-> ([Maybe a] -> Maybe (Min a)) -> [Maybe a] -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe (Min a)] -> Maybe (Min a)
forall a. Monoid a => [a] -> a
mconcat ([Maybe (Min a)] -> Maybe (Min a))
-> ([Maybe a] -> [Maybe (Min a)]) -> [Maybe a] -> Maybe (Min a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe a -> Maybe (Min a)) -> [Maybe a] -> [Maybe (Min a)]
forall a b. (a -> b) -> [a] -> [b]
map (a -> Min a
forall a. a -> Min a
Min (a -> Min a) -> Maybe a -> Maybe (Min a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
[Maybe Integer] -> Maybe Integer
forall a. Ord a => [Maybe a] -> Maybe a
minimum' ((AssertedHint -> Maybe Integer)
-> [AssertedHint] -> [Maybe Integer]
forall a b. (a -> b) -> [a] -> [b]
map AssertedHint -> Maybe Integer
go ([(VarName, AssertedHint)] -> VarName -> [AssertedHint]
selectHints [(VarName, AssertedHint)]
hints VarName
xs))
Expr
_ -> Maybe Integer
forall a. Maybe a
Nothing