{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}

module Jikka.Core.Language.AssertedHint
  ( AssertedHint (..),
    pattern EqualHint,
    parseHints,

    -- * Functions using hints
    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 n@ for a integer variable @x@ means @x /= n@
    NotEqualHint ArithmeticExpr
  | -- | @BoundHint l r@ for a integer variable @x@ means @l <= x < r@
    BoundHint (Maybe ArithmeticExpr) (Maybe ArithmeticExpr)
  | -- | @LengthHint t hint@ for a list variable @xs@ means @length xs@ satisfies @hint@
    LengthHint Type AssertedHint
  | -- | @AllHint t hint@ for a list variable @xs@ means that @x@ satisfies @hint@ for all @x@ in @xs@
    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
  -- Jikka.Core.Language.EqualitiySolving makes rhs nil
  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` makes @a + b + c@ to @[(a, b + c), (b, a + c), (c, a + b)]@ in a convenient way, because Jikka.Core.Language.EqualitiySolving makes @a == b@ to @a - b == 0@.
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
_ -> []
  -- Jikka.Core.Language.EqualitiySolving makes rhs 0 and removes GreaterEqual and GreaterThan
  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