{-# OPTIONS_GHC -Wunused-imports #-}

module Agda.Compiler.Treeless.Simplify (simplifyTTerm) where

import Control.Applicative
import Control.Monad        ( (>=>), guard )
import Control.Monad.Reader ( MonadReader(..), asks, Reader, runReader )
import Control.Monad.Trans
import Control.Monad.Trans.Maybe
import qualified Data.List as List

import Agda.Syntax.Internal (termSize)
import Agda.Syntax.Treeless
import Agda.Syntax.Literal

import Agda.TypeChecking.Monad
import Agda.TypeChecking.Primitive
import Agda.TypeChecking.Substitute

import Agda.Compiler.Treeless.Compare

import Agda.Utils.IndexMap (IndexMap)
import qualified Agda.Utils.IndexMap as IndexMap
import Agda.Utils.List
import Agda.Utils.Maybe
import Agda.Utils.Tuple ( (***), second )

import Agda.Utils.Impossible

data SEnv = SEnv
  { SEnv -> Substitution' TTerm
envSubst :: Substitution' TTerm
  , SEnv -> IndexMap Strictness
envStrictness :: IndexMap Strictness
    -- ^ What strictness was the given variable bound with?
  , SEnv -> [(TTerm, TTerm)]
envRewrite :: [(TTerm, TTerm)] }

type S = Reader SEnv

runS :: S a -> a
runS :: forall a. S a -> a
runS S a
m = S a -> SEnv -> a
forall r a. Reader r a -> r -> a
runReader S a
m (SEnv -> a) -> SEnv -> a
forall a b. (a -> b) -> a -> b
$ Substitution' TTerm
-> IndexMap Strictness -> [(TTerm, TTerm)] -> SEnv
SEnv Substitution' TTerm
forall a. Substitution' a
IdS IndexMap Strictness
forall a. IndexMap a
IndexMap.nil []

lookupVar :: Int -> S (Strictness, TTerm)
lookupVar :: Int -> S (Strictness, TTerm)
lookupVar Int
i = do
  env <- ReaderT SEnv Identity SEnv
forall r (m :: * -> *). MonadReader r m => m r
ask
  return (IndexMap.index i (envStrictness env), lookupS (envSubst env) i)

onSubst :: (Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
onSubst :: forall a.
(Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
onSubst Substitution' TTerm -> Substitution' TTerm
f = (SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall a.
(SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((SEnv -> SEnv)
 -> ReaderT SEnv Identity a -> ReaderT SEnv Identity a)
-> (SEnv -> SEnv)
-> ReaderT SEnv Identity a
-> ReaderT SEnv Identity a
forall a b. (a -> b) -> a -> b
$ \ SEnv
env -> SEnv
env { envSubst = f (envSubst env) }

onStrictness :: (IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
onStrictness :: forall a.
(IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
onStrictness IndexMap Strictness -> IndexMap Strictness
f =
  (SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall a.
(SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local (\SEnv
env -> SEnv
env { envStrictness = f (envStrictness env) })

onRewrite :: Substitution' TTerm -> S a -> S a
onRewrite :: forall a. Substitution' TTerm -> S a -> S a
onRewrite Substitution' TTerm
rho = (SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall a.
(SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((SEnv -> SEnv)
 -> ReaderT SEnv Identity a -> ReaderT SEnv Identity a)
-> (SEnv -> SEnv)
-> ReaderT SEnv Identity a
-> ReaderT SEnv Identity a
forall a b. (a -> b) -> a -> b
$ \ SEnv
env -> SEnv
env { envRewrite = map (applySubst rho *** applySubst rho) (envRewrite env) }

addRewrite :: TTerm -> TTerm -> S a -> S a
addRewrite :: forall a. TTerm -> TTerm -> S a -> S a
addRewrite TTerm
lhs TTerm
rhs = (SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall a.
(SEnv -> SEnv)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity a
forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
local ((SEnv -> SEnv)
 -> ReaderT SEnv Identity a -> ReaderT SEnv Identity a)
-> (SEnv -> SEnv)
-> ReaderT SEnv Identity a
-> ReaderT SEnv Identity a
forall a b. (a -> b) -> a -> b
$ \ SEnv
env -> SEnv
env { envRewrite = (lhs, rhs) : envRewrite env }

-- | There is one strictness per binding, and the first element in the
-- list corresponds to the first new binding.

underLams :: [Strictness] -> S a -> S a
underLams :: forall a. [Strictness] -> S a -> S a
underLams [Strictness]
ss =
  Substitution' TTerm -> S a -> S a
forall a. Substitution' TTerm -> S a -> S a
onRewrite (Int -> Substitution' TTerm
forall a. Int -> Substitution' a
raiseS Int
i) (S a -> S a) -> (S a -> S a) -> S a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
forall a.
(Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
onSubst (Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i) (S a -> S a) -> (S a -> S a) -> S a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
forall a.
(IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
onStrictness ((IndexMap Strictness -> [Strictness] -> IndexMap Strictness)
-> [Strictness] -> IndexMap Strictness -> IndexMap Strictness
forall a b c. (a -> b -> c) -> b -> a -> c
flip IndexMap Strictness -> [Strictness] -> IndexMap Strictness
forall a. IndexMap a -> [a] -> IndexMap a
IndexMap.append [Strictness]
ss)
  where
  i :: Int
i = [Strictness] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Strictness]
ss

underLam :: Strictness -> S a -> S a
underLam :: forall a. Strictness -> S a -> S a
underLam Strictness
s = [Strictness] -> S a -> S a
forall a. [Strictness] -> S a -> S a
underLams [Strictness
s]

underLet :: Strictness -> TTerm -> S a -> S a
underLet :: forall a. Strictness -> TTerm -> S a -> S a
underLet Strictness
s TTerm
u =
  Substitution' TTerm -> S a -> S a
forall a. Substitution' TTerm -> S a -> S a
onRewrite (Int -> Substitution' TTerm
forall a. Int -> Substitution' a
raiseS Int
1) (S a -> S a) -> (S a -> S a) -> S a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
forall a.
(Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
onSubst (\Substitution' TTerm
rho -> Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 (Substitution' TTerm -> Substitution' TTerm)
-> Substitution' TTerm -> Substitution' TTerm
forall a b. (a -> b) -> a -> b
$ TTerm
u TTerm -> Substitution' TTerm -> Substitution' TTerm
forall a. a -> Substitution' a -> Substitution' a
:# Substitution' TTerm
rho) (S a -> S a) -> (S a -> S a) -> S a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
forall a.
(IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
onStrictness ((IndexMap Strictness -> Strictness -> IndexMap Strictness)
-> Strictness -> IndexMap Strictness -> IndexMap Strictness
forall a b c. (a -> b -> c) -> b -> a -> c
flip IndexMap Strictness -> Strictness -> IndexMap Strictness
forall a. IndexMap a -> a -> IndexMap a
IndexMap.snoc Strictness
s)

bindVar :: Int -> Strictness -> TTerm -> S a -> S a
bindVar :: forall a. Int -> Strictness -> TTerm -> S a -> S a
bindVar Int
x Strictness
s TTerm
u =
  (Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
forall a.
(Substitution' TTerm -> Substitution' TTerm) -> S a -> S a
onSubst (Int -> TTerm -> Substitution' TTerm
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
x TTerm
u Substitution' TTerm -> Substitution' TTerm -> Substitution' TTerm
forall a.
EndoSubst a =>
Substitution' a -> Substitution' a -> Substitution' a
`composeS`) (S a -> S a) -> (S a -> S a) -> S a -> S a
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
forall a.
(IndexMap Strictness -> IndexMap Strictness) -> S a -> S a
onStrictness (Int -> Strictness -> IndexMap Strictness -> IndexMap Strictness
forall a. Int -> a -> IndexMap a -> IndexMap a
IndexMap.update Int
x Strictness
s)

rewrite :: TTerm -> S TTerm
rewrite :: TTerm -> S TTerm
rewrite TTerm
t = do
  rules <- (SEnv -> [(TTerm, TTerm)])
-> ReaderT SEnv Identity [(TTerm, TTerm)]
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SEnv -> [(TTerm, TTerm)]
envRewrite
  case [ rhs | (lhs, rhs) <- rules, equalTerms t lhs ] of
    TTerm
rhs : [TTerm]
_ -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
rhs
    []      -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

data FunctionKit = FunctionKit
  { FunctionKit -> Maybe QName
modAux, FunctionKit -> Maybe QName
divAux, FunctionKit -> Maybe QName
natMinus, FunctionKit -> Maybe QName
true, FunctionKit -> Maybe QName
false :: Maybe QName }

simplifyTTerm :: EvaluationStrategy -> TTerm -> TCM TTerm
simplifyTTerm :: EvaluationStrategy -> TTerm -> TCM TTerm
simplifyTTerm EvaluationStrategy
eval TTerm
t = do
  kit <- Maybe QName
-> Maybe QName
-> Maybe QName
-> Maybe QName
-> Maybe QName
-> FunctionKit
FunctionKit (Maybe QName
 -> Maybe QName
 -> Maybe QName
 -> Maybe QName
 -> Maybe QName
 -> FunctionKit)
-> TCMT IO (Maybe QName)
-> TCMT
     IO
     (Maybe QName
      -> Maybe QName -> Maybe QName -> Maybe QName -> FunctionKit)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNatModSucAux
                     TCMT
  IO
  (Maybe QName
   -> Maybe QName -> Maybe QName -> Maybe QName -> FunctionKit)
-> TCMT IO (Maybe QName)
-> TCMT
     IO (Maybe QName -> Maybe QName -> Maybe QName -> FunctionKit)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNatDivSucAux
                     TCMT IO (Maybe QName -> Maybe QName -> Maybe QName -> FunctionKit)
-> TCMT IO (Maybe QName)
-> TCMT IO (Maybe QName -> Maybe QName -> FunctionKit)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinNatMinus
                     TCMT IO (Maybe QName -> Maybe QName -> FunctionKit)
-> TCMT IO (Maybe QName) -> TCMT IO (Maybe QName -> FunctionKit)
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinTrue
                     TCMT IO (Maybe QName -> FunctionKit)
-> TCMT IO (Maybe QName) -> TCMT IO FunctionKit
forall a b. TCMT IO (a -> b) -> TCMT IO a -> TCMT IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BuiltinId -> TCMT IO (Maybe QName)
forall (m :: * -> *).
(HasBuiltins m, MonadReduce m) =>
BuiltinId -> m (Maybe QName)
getBuiltinName BuiltinId
builtinFalse
  return $ runS $ simplify eval kit t

simplify :: EvaluationStrategy -> FunctionKit -> TTerm -> S TTerm
simplify :: EvaluationStrategy -> FunctionKit -> TTerm -> S TTerm
simplify EvaluationStrategy
eval FunctionKit{ Maybe QName
divAux :: FunctionKit -> Maybe QName
divAux :: Maybe QName
divAux, Maybe QName
modAux :: FunctionKit -> Maybe QName
modAux :: Maybe QName
modAux, Maybe QName
natMinus :: FunctionKit -> Maybe QName
natMinus :: Maybe QName
natMinus, Maybe QName
true :: FunctionKit -> Maybe QName
true :: Maybe QName
true, Maybe QName
false :: FunctionKit -> Maybe QName
false :: Maybe QName
false } =
  TTerm -> S TTerm
simpl
  where
    simpl :: TTerm -> S TTerm
simpl = TTerm -> S TTerm
rewrite' (TTerm -> S TTerm) -> (TTerm -> S TTerm) -> TTerm -> S TTerm
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> TTerm -> S TTerm
unchainCase (TTerm -> S TTerm) -> (TTerm -> S TTerm) -> TTerm -> S TTerm
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> \case

      t :: TTerm
t@TDef{}  -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TPrim{} -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TVar{}  -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

      TApp (TDef QName
f) [TLit (LitNat Integer
0), TTerm
m, TTerm
n, TTerm
m']
        -- div/mod are equivalent to quot/rem on natural numbers.
        | TTerm
m TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
m', QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
divAux -> TTerm -> S TTerm
simpl (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PQuot TTerm
n (Integer -> TTerm -> TTerm
tPlusK Integer
1 TTerm
m)
        | TTerm
m TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
m', QName -> Maybe QName
forall a. a -> Maybe a
Just QName
f Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
modAux -> TTerm -> S TTerm
simpl (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PRem TTerm
n (Integer -> TTerm -> TTerm
tPlusK Integer
1 TTerm
m)

      -- Word64 primitives --

      --  toWord (a ∙ b) == toWord a ∙64 toWord b
      TPFn TPrim
PITo64 (TPOp TPrim
op TTerm
a TTerm
b)
        | Just TPrim
op64 <- TPrim -> Maybe TPrim
opTo64 TPrim
op -> TTerm -> S TTerm
simpl (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op64 (TPrim -> TTerm -> TTerm
TPFn TPrim
PITo64 TTerm
a) (TPrim -> TTerm -> TTerm
TPFn TPrim
PITo64 TTerm
b)
        where
          opTo64 :: TPrim -> Maybe TPrim
opTo64 TPrim
op = TPrim -> [(TPrim, TPrim)] -> Maybe TPrim
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TPrim
op [(TPrim
PAdd, TPrim
PAdd64), (TPrim
PSub, TPrim
PSub64), (TPrim
PMul, TPrim
PMul64),
                                 (TPrim
PQuot, TPrim
PQuot64), (TPrim
PRem, TPrim
PRem64)]

      t :: TTerm
t@(TApp (TPrim TPrim
_) [TTerm]
_) -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t  -- taken care of by rewrite'

      TCoerce TTerm
t -> TTerm -> TTerm
TCoerce (TTerm -> TTerm) -> S TTerm -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
simpl TTerm
t

      TApp TTerm
f [TTerm]
es -> do
        f  <- TTerm -> S TTerm
simpl TTerm
f
        es <- traverse simpl es
        maybeMinusToPrim f es
      TLam TTerm
b     -> TTerm -> TTerm
TLam (TTerm -> TTerm) -> S TTerm -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Strictness -> S TTerm -> S TTerm
forall a. Strictness -> S a -> S a
underLam (EvaluationStrategy -> Strictness
defaultStrictness EvaluationStrategy
eval) (TTerm -> S TTerm
simpl TTerm
b)
      t :: TTerm
t@TLit{}   -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TCon{}   -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      TLet Strictness
s TTerm
e TTerm
b -> do
        TTerm -> S TTerm
simpl TTerm
e S TTerm -> (TTerm -> S TTerm) -> S TTerm
forall a b.
ReaderT SEnv Identity a
-> (a -> ReaderT SEnv Identity b) -> ReaderT SEnv Identity b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
          TPFn TPrim
P64ToI TTerm
a -> do
            -- Inline calls to P64ToI since these trigger optimisations.
            -- Ideally, the optimisations would trigger anyway, but at the
            -- moment they only do if inlining the entire let looks like a
            -- good idea.
            let rho :: Substitution' TTerm
rho = Int -> TTerm -> Substitution' TTerm
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
0 (TPrim -> TTerm -> TTerm
TPFn TPrim
P64ToI (Int -> TTerm
TVar Int
0))
            Strictness -> TTerm -> TTerm -> TTerm
tLet Strictness
s TTerm
a (TTerm -> TTerm) -> S TTerm -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Strictness -> TTerm -> S TTerm -> S TTerm
forall a. Strictness -> TTerm -> S a -> S a
underLet Strictness
s TTerm
a (TTerm -> S TTerm
simpl (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
Substitution' TTerm
rho TTerm
b))
          TTerm
e -> Strictness -> TTerm -> TTerm -> TTerm
tLet Strictness
s TTerm
e (TTerm -> TTerm) -> S TTerm -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Strictness -> TTerm -> S TTerm -> S TTerm
forall a. Strictness -> TTerm -> S a -> S a
underLet Strictness
s TTerm
e (TTerm -> S TTerm
simpl TTerm
b)

      TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs -> do
        (_, v) <- Int -> S (Strictness, TTerm)
lookupVar Int
x
        let (lets, u) = tLetView v
        (d, bs) <-
          pruneBoolGuards d <$>
            traverse (simplAlt x (caseInduction t)) bs
        case u of                          -- TODO: also for literals
          TTerm
_ | Just (QName
c, [TTerm]
as) <- TTerm -> Maybe (QName, [TTerm])
conView TTerm
u ->
              TTerm -> S TTerm
simpl (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ [(Strictness, TTerm)]
-> QName -> [TTerm] -> Induction -> TTerm -> [TAlt] -> TTerm
matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as (CaseInfo -> Induction
caseInduction CaseInfo
t) TTerm
d [TAlt]
bs
            | Just (Integer
k, TVar Int
y) <- TTerm -> Maybe (Integer, TTerm)
plusKView TTerm
u -> TTerm -> S TTerm
simpl (TTerm -> S TTerm) -> ([TAlt] -> TTerm) -> [TAlt] -> S TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(Strictness, TTerm)] -> TTerm -> TTerm
forall {t :: * -> *}.
Foldable t =>
t (Strictness, TTerm) -> TTerm -> TTerm
mkLets [(Strictness, TTerm)]
lets (TTerm -> TTerm) -> ([TAlt] -> TTerm) -> [TAlt] -> TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
y CaseInfo
t TTerm
d ([TAlt] -> S TTerm) -> ReaderT SEnv Identity [TAlt] -> S TTerm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< (TAlt -> ReaderT SEnv Identity TAlt)
-> [TAlt] -> ReaderT SEnv Identity [TAlt]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Int -> Int -> Integer -> TAlt -> ReaderT SEnv Identity TAlt
matchPlusK Int
y Int
x Integer
k) [TAlt]
bs
            -- We are not normalizing the case-of-case commuting converison
            -- since it can lead to major code duplication without join points
            -- or continuations. See issue #7595.
            | Bool
otherwise -> do
            d <- TTerm -> S TTerm
simpl TTerm
d
            tCase x t d bs

      t :: TTerm
t@TTerm
TUnit    -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TTerm
TSort    -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TTerm
TErased  -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t
      t :: TTerm
t@TError{} -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

    conView :: TTerm -> Maybe (QName, [TTerm])
conView (TCon QName
c)    = (QName, [TTerm]) -> Maybe (QName, [TTerm])
forall a. a -> Maybe a
Just (QName
c, [])
    conView (TApp TTerm
f [TTerm]
as) = ([TTerm] -> [TTerm]) -> (QName, [TTerm]) -> (QName, [TTerm])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second ([TTerm] -> [TTerm] -> [TTerm]
forall a. [a] -> [a] -> [a]
++ [TTerm]
as) ((QName, [TTerm]) -> (QName, [TTerm]))
-> Maybe (QName, [TTerm]) -> Maybe (QName, [TTerm])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> Maybe (QName, [TTerm])
conView TTerm
f
    conView TTerm
e           = Maybe (QName, [TTerm])
forall a. Maybe a
Nothing

    -- Collapse chained cases (case x of bs -> vs; _ -> case x of bs' -> vs'  ==>
    --                         case x of bs -> vs; bs' -> vs')
    unchainCase :: TTerm -> S TTerm
    unchainCase :: TTerm -> S TTerm
unchainCase e :: TTerm
e@(TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs) = do
      let ([(Strictness, TTerm)]
lets, TTerm
u) = TTerm -> ([(Strictness, TTerm)], TTerm)
tLetView TTerm
d
          k :: Int
k = [(Strictness, TTerm)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Strictness, TTerm)]
lets
      case TTerm
u of
        TCase Int
y CaseInfo
_ TTerm
d' [TAlt]
bs' | Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> do
          lets <- MaybeT (ReaderT SEnv Identity) [(Strictness, TTerm)]
-> ReaderT SEnv Identity (Maybe [(Strictness, TTerm)])
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (((Strictness, TTerm)
 -> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm))
-> [(Strictness, TTerm)]
-> MaybeT (ReaderT SEnv Identity) [(Strictness, TTerm)]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
safeLet [(Strictness, TTerm)]
lets)
          return $ case lets of
            Just [(Strictness, TTerm)]
lets ->
              [(Strictness, TTerm)] -> TTerm -> TTerm
forall {t :: * -> *}.
Foldable t =>
t (Strictness, TTerm) -> TTerm -> TTerm
mkLets [(Strictness, TTerm)]
lets (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
y CaseInfo
t TTerm
d' ([TAlt] -> TTerm) -> [TAlt] -> TTerm
forall a b. (a -> b) -> a -> b
$
              Int -> [TAlt] -> [TAlt]
forall a. Subst a => Int -> a -> a
raise Int
k [TAlt]
bs [TAlt] -> [TAlt] -> [TAlt]
forall a. [a] -> [a] -> [a]
++ (TAlt -> Bool) -> [TAlt] -> [TAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter (TAlt -> [TAlt] -> Bool
forall {t :: * -> *}. Foldable t => TAlt -> t TAlt -> Bool
`noOverlap` [TAlt]
bs) [TAlt]
bs'
            Maybe [(Strictness, TTerm)]
Nothing -> TTerm
e
        TTerm
_ -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
e
    unchainCase TTerm
e = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
e

    -- If chained cases of the following form are collapsed, and the
    -- lets moved to the outside, then performance could take a hit
    -- (see issue #8767):
    --
    --   case x of
    --     ⋮
    --     _ -> let … in case y of …
    --
    -- If strict evaluation is used, then this transformation is only
    -- allowed if all let bindings are "safe", i.e. non-strict or
    -- (heuristically) cheap to compute. If non-strict evaluation is
    -- used, then "unsafe" bindings are made non-strict.

    safeLet :: (Strictness, TTerm) -> MaybeT S (Strictness, TTerm)
    safeLet :: (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
safeLet l :: (Strictness, TTerm)
l@(Strictness
NonStrict, TTerm
_) =
      (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (Strictness, TTerm)
l
    safeLet l :: (Strictness, TTerm)
l@(Strictness
Strict, TTerm
t) = S (Maybe (Strictness, TTerm))
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
forall (m :: * -> *) a. m (Maybe a) -> MaybeT m a
MaybeT (S (Maybe (Strictness, TTerm))
 -> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm))
-> S (Maybe (Strictness, TTerm))
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
forall a b. (a -> b) -> a -> b
$ do
      t' <- MaybeT (ReaderT SEnv Identity) TTerm
-> ReaderT SEnv Identity (Maybe TTerm)
forall (m :: * -> *) a. MaybeT m a -> m (Maybe a)
runMaybeT (do
        -- The number 30 does not have any special significance other
        -- than being "not too small, but not very large".
        Bool -> MaybeT (ReaderT SEnv Identity) ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (TTerm -> Int
forall a. TermSize a => a -> Int
termSize TTerm
t Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
30)
        TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
cheap TTerm
t)
      return $ case t' of
        Just TTerm
t  -> (Strictness, TTerm) -> Maybe (Strictness, TTerm)
forall a. a -> Maybe a
Just (Strictness
Strict, TTerm
t)
        Maybe TTerm
Nothing -> case EvaluationStrategy
eval of
          LazyEvaluation Strictness
_ -> (Strictness, TTerm) -> Maybe (Strictness, TTerm)
forall a. a -> Maybe a
Just (Strictness
NonStrict, TTerm
t)
          EvaluationStrategy
EagerEvaluation  -> Maybe (Strictness, TTerm)
forall a. Maybe a
Nothing
      where
      cheap :: TTerm -> MaybeT S TTerm
      cheap :: TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
cheap TTerm
t = case TTerm
t of
        -- Error calls should definitely not be evaluated prematurely.
        TError{} -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty
        -- Case expressions and top-level definitions are treated as
        -- expensive.
        TCase{} -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty
        TDef{}  -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty
        -- Strictly bound variables are treated as cheap.
        TVar Int
x -> do
          (s, _) <- S (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
forall (m :: * -> *) a. Monad m => m a -> MaybeT m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (Int -> S (Strictness, TTerm)
lookupVar Int
x)
          case s of
            Strictness
NonStrict -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty
            Strictness
Strict    -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        -- Lets, coercions and applications of primitives are handled
        -- recursively.
        TLet Strictness
s TTerm
t1 TTerm
t2 -> (Strictness -> TTerm -> TTerm -> TTerm)
-> (Strictness, TTerm) -> TTerm -> TTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Strictness -> TTerm -> TTerm -> TTerm
TLet ((Strictness, TTerm) -> TTerm -> TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (TTerm -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Strictness, TTerm)
-> MaybeT (ReaderT SEnv Identity) (Strictness, TTerm)
safeLet (Strictness
s, TTerm
t1) MaybeT (ReaderT SEnv Identity) (TTerm -> TTerm)
-> MaybeT (ReaderT SEnv Identity) TTerm
-> MaybeT (ReaderT SEnv Identity) TTerm
forall a b.
MaybeT (ReaderT SEnv Identity) (a -> b)
-> MaybeT (ReaderT SEnv Identity) a
-> MaybeT (ReaderT SEnv Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
cheap TTerm
t2
        TCoerce TTerm
t    -> TTerm -> TTerm
TCoerce (TTerm -> TTerm)
-> MaybeT (ReaderT SEnv Identity) TTerm
-> MaybeT (ReaderT SEnv Identity) TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
cheap TTerm
t
        TApp TTerm
t [TTerm]
args  -> case TTerm
t of
          TPrim TPrim
p -> TTerm -> [TTerm] -> TTerm
TApp (TTerm -> [TTerm] -> TTerm)
-> MaybeT (ReaderT SEnv Identity) TTerm
-> MaybeT (ReaderT SEnv Identity) ([TTerm] -> TTerm)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (if TPrim -> Bool
cheapPrim TPrim
p then TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return (TPrim -> TTerm
TPrim TPrim
p)
                               else MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty)
                          MaybeT (ReaderT SEnv Identity) ([TTerm] -> TTerm)
-> MaybeT (ReaderT SEnv Identity) [TTerm]
-> MaybeT (ReaderT SEnv Identity) TTerm
forall a b.
MaybeT (ReaderT SEnv Identity) (a -> b)
-> MaybeT (ReaderT SEnv Identity) a
-> MaybeT (ReaderT SEnv Identity) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> (TTerm -> MaybeT (ReaderT SEnv Identity) TTerm)
-> [TTerm] -> MaybeT (ReaderT SEnv Identity) [TTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
cheap [TTerm]
args
          TTerm
_       -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. MaybeT (ReaderT SEnv Identity) a
forall (f :: * -> *) a. Alternative f => f a
empty
        -- Things that are known to be (basically) values are treated
        -- as cheap.
        TPrim{}   -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TLam{}    -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TLit{}    -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TCon{}    -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TUnit{}   -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TSort{}   -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t
        TErased{} -> TTerm -> MaybeT (ReaderT SEnv Identity) TTerm
forall a. a -> MaybeT (ReaderT SEnv Identity) a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
t

      cheapPrim :: TPrim -> Bool
cheapPrim = \case
        -- String comparison might be expensive.
        TPrim
PEqS -> Bool
False
        -- If expressions are treated as expensive, just like case
        -- expressions.
        TPrim
PIf -> Bool
False
        -- All other primitives are treated as cheap, including PSeq.
        TPrim
PSeq    -> Bool
True
        TPrim
PAdd    -> Bool
True
        TPrim
PAdd64  -> Bool
True
        TPrim
PSub    -> Bool
True
        TPrim
PSub64  -> Bool
True
        TPrim
PMul    -> Bool
True
        TPrim
PMul64  -> Bool
True
        TPrim
PQuot   -> Bool
True
        TPrim
PQuot64 -> Bool
True
        TPrim
PRem    -> Bool
True
        TPrim
PRem64  -> Bool
True
        TPrim
PGeq    -> Bool
True
        TPrim
PLt     -> Bool
True
        TPrim
PLt64   -> Bool
True
        TPrim
PEqI    -> Bool
True
        TPrim
PEq64   -> Bool
True
        TPrim
PEqF    -> Bool
True
        TPrim
PEqC    -> Bool
True
        TPrim
PEqQ    -> Bool
True
        TPrim
PITo64  -> Bool
True
        TPrim
P64ToI  -> Bool
True

    mkLets :: t (Strictness, TTerm) -> TTerm -> TTerm
mkLets t (Strictness, TTerm)
es TTerm
b = ((Strictness, TTerm) -> TTerm -> TTerm)
-> TTerm -> t (Strictness, TTerm) -> TTerm
forall a b. (a -> b -> b) -> b -> t a -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Strictness -> TTerm -> TTerm -> TTerm)
-> (Strictness, TTerm) -> TTerm -> TTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Strictness -> TTerm -> TTerm -> TTerm
TLet) TTerm
b t (Strictness, TTerm)
es

    matchCon :: [(Strictness, TTerm)]
-> QName -> [TTerm] -> Induction -> TTerm -> [TAlt] -> TTerm
matchCon [(Strictness, TTerm)]
_ QName
_ [TTerm]
_ Induction
_ TTerm
d [] = TTerm
d
    matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d (TALit{}   : [TAlt]
bs) = [(Strictness, TTerm)]
-> QName -> [TTerm] -> Induction -> TTerm -> [TAlt] -> TTerm
matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d [TAlt]
bs
    matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d (TAGuard{} : [TAlt]
bs) = [(Strictness, TTerm)]
-> QName -> [TTerm] -> Induction -> TTerm -> [TAlt] -> TTerm
matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d [TAlt]
bs
    matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d (TACon QName
c' Int
a TTerm
b : [TAlt]
bs)
      | QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
c'   = (TTerm -> [(Strictness, TTerm)] -> TTerm)
-> [(Strictness, TTerm)] -> TTerm -> TTerm
forall a b c. (a -> b -> c) -> b -> a -> c
flip (((Strictness, TTerm) -> TTerm -> TTerm)
-> TTerm -> [(Strictness, TTerm)] -> TTerm
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Strictness -> TTerm -> TTerm -> TTerm)
-> (Strictness, TTerm) -> TTerm -> TTerm
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Strictness -> TTerm -> TTerm -> TTerm
TLet)) [(Strictness, TTerm)]
lets (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$
                    Int -> [TTerm] -> TTerm -> TTerm
mkLet Int
0 [TTerm]
as (Int -> Int -> TTerm -> TTerm
forall a. Subst a => Int -> Int -> a -> a
raiseFrom Int
a ([(Strictness, TTerm)] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [(Strictness, TTerm)]
lets) TTerm
b)
      | Bool
otherwise = [(Strictness, TTerm)]
-> QName -> [TTerm] -> Induction -> TTerm -> [TAlt] -> TTerm
matchCon [(Strictness, TTerm)]
lets QName
c [TTerm]
as Induction
i TTerm
d [TAlt]
bs
      where
      s :: Strictness
s = EvaluationStrategy -> Induction -> Strictness
defaultConstructorStrictness EvaluationStrategy
eval Induction
i

      mkLet :: Int -> [TTerm] -> TTerm -> TTerm
mkLet Int
_ []       TTerm
b = TTerm
b
      mkLet Int
i (TTerm
a : [TTerm]
as) TTerm
b = Strictness -> TTerm -> TTerm -> TTerm
TLet Strictness
s (Int -> TTerm -> TTerm
forall a. Subst a => Int -> a -> a
raise Int
i TTerm
a) (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Int -> [TTerm] -> TTerm -> TTerm
mkLet (Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [TTerm]
as TTerm
b

    -- Simplify let y = x + k in case y of j     -> u; _ | g[y]     -> v
    -- to       let y = x + k in case x of j - k -> u; _ | g[x + k] -> v
    matchPlusK :: Int -> Int -> Integer -> TAlt -> S TAlt
    matchPlusK :: Int -> Int -> Integer -> TAlt -> ReaderT SEnv Identity TAlt
matchPlusK Int
x Int
y Integer
k (TALit (LitNat Integer
j) TTerm
b) = TAlt -> ReaderT SEnv Identity TAlt
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TAlt -> ReaderT SEnv Identity TAlt)
-> TAlt -> ReaderT SEnv Identity TAlt
forall a b. (a -> b) -> a -> b
$ Literal -> TTerm -> TAlt
TALit (Integer -> Literal
LitNat (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
k)) TTerm
b
    matchPlusK Int
x Int
y Integer
k (TAGuard TTerm
g TTerm
b) = (TTerm -> TTerm -> TAlt) -> TTerm -> TTerm -> TAlt
forall a b c. (a -> b -> c) -> b -> a -> c
flip TTerm -> TTerm -> TAlt
TAGuard TTerm
b (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
simpl (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> TTerm -> Substitution' TTerm
forall a. EndoSubst a => Int -> a -> Substitution' a
inplaceS Int
y (Integer -> TTerm -> TTerm
tPlusK Integer
k (Int -> TTerm
TVar Int
x))) TTerm
g)
    matchPlusK Int
x Int
y Integer
k TACon{} = ReaderT SEnv Identity TAlt
forall a. HasCallStack => a
__IMPOSSIBLE__
    matchPlusK Int
x Int
y Integer
k TALit{} = ReaderT SEnv Identity TAlt
forall a. HasCallStack => a
__IMPOSSIBLE__

    simplPrim :: TTerm -> S TTerm
simplPrim (TApp f :: TTerm
f@TPrim{} [TTerm]
args) = do
        args    <- (TTerm -> S TTerm) -> [TTerm] -> ReaderT SEnv Identity [TTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TTerm -> S TTerm
simpl [TTerm]
args
        inlined <- mapM inline args
        let u = TTerm -> [TTerm] -> TTerm
TApp TTerm
f [TTerm]
args
            v = TTerm -> TTerm
simplPrim' (TTerm -> [TTerm] -> TTerm
TApp TTerm
f [TTerm]
inlined)
        pure $ if v `betterThan` u then v else u
      where
        inline :: TTerm -> S TTerm
inline (TVar Int
x)                   = do
          (_, v) <- Int -> S (Strictness, TTerm)
lookupVar Int
x
          if v == TVar x then pure v else inline v
        inline (TApp f :: TTerm
f@TPrim{} [TTerm]
args)        = TTerm -> [TTerm] -> TTerm
TApp TTerm
f ([TTerm] -> TTerm) -> ReaderT SEnv Identity [TTerm] -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (TTerm -> S TTerm) -> [TTerm] -> ReaderT SEnv Identity [TTerm]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM TTerm -> S TTerm
inline [TTerm]
args
        inline u :: TTerm
u@(TLet Strictness
_ TTerm
_ (TCase Int
0 CaseInfo
_ TTerm
_ [TAlt]
_)) = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
u
        inline (TLet Strictness
_ TTerm
e TTerm
b)                 = TTerm -> S TTerm
inline (Int -> SubstArg TTerm -> TTerm -> TTerm
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 SubstArg TTerm
TTerm
e TTerm
b)
        inline TTerm
u                            = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
u
    simplPrim TTerm
t = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

    simplPrim' :: TTerm -> TTerm
    simplPrim' :: TTerm -> TTerm
simplPrim' (TApp (TPrim TPrim
PSeq) (TTerm
u : TTerm
v : [TTerm]
vs))
      | TTerm
u TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm
v             = TTerm -> [TTerm] -> TTerm
mkTApp TTerm
v [TTerm]
vs
      | TApp TCon{} [TTerm]
_ <- TTerm
u = TTerm -> [TTerm] -> TTerm
mkTApp TTerm
v [TTerm]
vs
      | TApp TLit{} [TTerm]
_ <- TTerm
u = TTerm -> [TTerm] -> TTerm
mkTApp TTerm
v [TTerm]
vs
    simplPrim' (TApp (TPrim TPrim
PLt) [TTerm
u, TTerm
v])
      | Just (TPrim
PAdd, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u,
        Just (TPrim
PAdd, Integer
j, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PLt TTerm
u TTerm
v
      | Just (TPrim
PSub, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u,
        Just (TPrim
PSub, Integer
j, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PLt TTerm
v TTerm
u
      | Just (TPrim
PAdd, Integer
k, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        TApp (TPrim TPrim
P64ToI) [TTerm
u] <- TTerm
u,
        Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
64, Just QName
trueCon <- Maybe QName
true = QName -> TTerm
TCon QName
trueCon
      | Just Integer
k <- TTerm -> Maybe Integer
intView TTerm
u
      , Just Integer
j <- TTerm -> Maybe Integer
intView TTerm
v
      , Just QName
trueCon <- Maybe QName
true
      , Just QName
falseCon <- Maybe QName
false = if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
j then QName -> TTerm
TCon QName
trueCon else QName -> TTerm
TCon QName
falseCon
    simplPrim' (TApp (TPrim TPrim
PGeq) [TTerm
u, TTerm
v])
      | Just (TPrim
PAdd, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u,
        Just (TPrim
PAdd, Integer
j, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PGeq TTerm
u TTerm
v
      | Just (TPrim
PSub, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u,
        Just (TPrim
PSub, Integer
j, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PGeq TTerm
v TTerm
u
      | Just Integer
k <- TTerm -> Maybe Integer
intView TTerm
u
      , Just Integer
j <- TTerm -> Maybe Integer
intView TTerm
v
      , Just QName
trueCon <- Maybe QName
true
      , Just QName
falseCon <- Maybe QName
false = if Integer
k Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
j then QName -> TTerm
TCon QName
trueCon else QName -> TTerm
TCon QName
falseCon
    simplPrim' (TApp (TPrim TPrim
op) [TTerm
u, TTerm
v])
      | TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PGeq, TPrim
PLt, TPrim
PEqI]
      , Just (TPrim
PAdd, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u
      , Just Integer
j <- TTerm -> Maybe Integer
intView TTerm
v = TTerm -> [TTerm] -> TTerm
TApp (TPrim -> TTerm
TPrim TPrim
op) [TTerm
u, Integer -> TTerm
tInt (Integer
j Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
k)]
    simplPrim' (TApp (TPrim TPrim
PEqI) [TTerm
u, TTerm
v])
      | Just (TPrim
op1, Integer
k, TTerm
u) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
u,
        Just (TPrim
op2, Integer
j, TTerm
v) <- TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView TTerm
v,
        TPrim
op1 TPrim -> TPrim -> Bool
forall a. Eq a => a -> a -> Bool
== TPrim
op2, Integer
k Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
j,
        TPrim
op1 TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PAdd, TPrim
PSub] = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PEqI TTerm
u TTerm
v
    simplPrim' (TPOp TPrim
op TTerm
u TTerm
v)
      | Bool
zeroL, Bool
isMul Bool -> Bool -> Bool
|| Bool
isDiv = Integer -> TTerm
tInt Integer
0
      | Bool
zeroL, Bool
isAdd          = TTerm
v
      | Bool
zeroR, Bool
isMul          = Integer -> TTerm
tInt Integer
0
      | Bool
zeroR, Bool
isAdd Bool -> Bool -> Bool
|| Bool
isSub = TTerm
u
      where zeroL :: Bool
zeroL = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0 Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm -> Maybe Integer
intView TTerm
u Bool -> Bool -> Bool
|| Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
0 Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm -> Maybe Word64
word64View TTerm
u
            zeroR :: Bool
zeroR = Integer -> Maybe Integer
forall a. a -> Maybe a
Just Integer
0 Maybe Integer -> Maybe Integer -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm -> Maybe Integer
intView TTerm
v Bool -> Bool -> Bool
|| Word64 -> Maybe Word64
forall a. a -> Maybe a
Just Word64
0 Maybe Word64 -> Maybe Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== TTerm -> Maybe Word64
word64View TTerm
v
            isAdd :: Bool
isAdd = TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PAdd, TPrim
PAdd64]
            isSub :: Bool
isSub = TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PSub, TPrim
PSub64]
            isMul :: Bool
isMul = TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PMul, TPrim
PMul64]
            isDiv :: Bool
isDiv = TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PQuot, TPrim
PQuot64, TPrim
PRem, TPrim
PRem64]
    simplPrim' (TApp (TPrim TPrim
op) [TTerm
u, TTerm
v])
      | Just TTerm
u <- TTerm -> Maybe TTerm
negView TTerm
u,
        Just TTerm
v <- TTerm -> Maybe TTerm
negView TTerm
v,
        TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PMul, TPrim
PQuot] = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op TTerm
u TTerm
v
      | Just TTerm
u <- TTerm -> Maybe TTerm
negView TTerm
u,
        TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PMul, TPrim
PQuot] = TTerm -> TTerm
simplArith (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub (Integer -> TTerm
tInt Integer
0) (TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op TTerm
u TTerm
v)
      | Just TTerm
v <- TTerm -> Maybe TTerm
negView TTerm
v,
        TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PMul, TPrim
PQuot] = TTerm -> TTerm
simplArith (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub (Integer -> TTerm
tInt Integer
0) (TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op TTerm
u TTerm
v)
    simplPrim' (TApp (TPrim TPrim
PRem) [TTerm
u, TTerm
v])
      | Just TTerm
u <- TTerm -> Maybe TTerm
negView TTerm
u  = TTerm -> TTerm
simplArith (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub (Integer -> TTerm
tInt Integer
0) (TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PRem TTerm
u (TTerm -> TTerm
unNeg TTerm
v))
      | Just TTerm
v <- TTerm -> Maybe TTerm
negView TTerm
v  = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PRem TTerm
u TTerm
v

      -- (fromWord a == fromWord b) = (a ==64 b)
    simplPrim' (TPOp TPrim
op (TPFn TPrim
P64ToI TTerm
a) (TPFn TPrim
P64ToI TTerm
b))
        | Just TPrim
op64 <- TPrim -> Maybe TPrim
opTo64 TPrim
op = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
op64 TTerm
a TTerm
b
        where
          opTo64 :: TPrim -> Maybe TPrim
opTo64 TPrim
op = TPrim -> [(TPrim, TPrim)] -> Maybe TPrim
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup TPrim
op [(TPrim
PEqI, TPrim
PEq64), (TPrim
PLt, TPrim
PLt64)]

      -- toWord/fromWord k == fromIntegral k
    simplPrim' (TPFn TPrim
PITo64 (TLit (LitNat Integer
n)))    = Literal -> TTerm
TLit (Word64 -> Literal
LitWord64 (Integer -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral Integer
n))
    simplPrim' (TPFn TPrim
P64ToI (TLit (LitWord64 Word64
n))) = Literal -> TTerm
TLit (Integer -> Literal
LitNat    (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n))

      -- toWord (fromWord a) == a
    simplPrim' (TPFn TPrim
PITo64 (TPFn TPrim
P64ToI TTerm
a)) = TTerm
a

    simplPrim' (TApp f :: TTerm
f@(TPrim TPrim
op) [TTerm
u, TTerm
v]) = TTerm -> TTerm
simplArith (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
TApp TTerm
f [TTerm -> TTerm
simplPrim' TTerm
u, TTerm -> TTerm
simplPrim' TTerm
v]
    simplPrim' TTerm
u = TTerm
u

    unNeg :: TTerm -> TTerm
unNeg TTerm
u | Just TTerm
v <- TTerm -> Maybe TTerm
negView TTerm
u = TTerm
v
            | Bool
otherwise           = TTerm
u

    negView :: TTerm -> Maybe TTerm
negView (TApp (TPrim TPrim
PSub) [TTerm
a, TTerm
b])
      | Just Integer
0 <- TTerm -> Maybe Integer
intView TTerm
a = TTerm -> Maybe TTerm
forall a. a -> Maybe a
Just TTerm
b
    negView TTerm
_ = Maybe TTerm
forall a. Maybe a
Nothing

    -- Count arithmetic operations
    betterThan :: TTerm -> TTerm -> Bool
betterThan TTerm
u TTerm
v = TTerm -> Integer
forall {t}. Num t => TTerm -> t
operations TTerm
u Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
<= TTerm -> Integer
forall {t}. Num t => TTerm -> t
operations TTerm
v
      where
        operations :: TTerm -> t
operations (TApp (TPrim TPrim
_) [TTerm
a, TTerm
b]) = t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ TTerm -> t
operations TTerm
a t -> t -> t
forall a. Num a => a -> a -> a
+ TTerm -> t
operations TTerm
b
        operations (TApp (TPrim TPrim
PSeq) (TTerm
a : [TTerm]
_))
          | TTerm -> Bool
notVar TTerm
a                       = t
1000000  -- only seq on variables!
        operations (TApp (TPrim TPrim
_) [TTerm
a])    = t
1 t -> t -> t
forall a. Num a => a -> a -> a
+ TTerm -> t
operations TTerm
a
        operations TVar{}                  = t
0
        operations TLit{}                  = t
0
        operations TCon{}                  = t
0
        operations TDef{}                  = t
0
        operations TTerm
_                       = t
1000

        notVar :: TTerm -> Bool
notVar TVar{} = Bool
False
        notVar TTerm
_      = Bool
True

    rewrite' :: TTerm -> S TTerm
rewrite' TTerm
t = TTerm -> S TTerm
rewrite (TTerm -> S TTerm) -> S TTerm -> S TTerm
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< TTerm -> S TTerm
simplPrim TTerm
t

    constArithView :: TTerm -> Maybe (TPrim, Integer, TTerm)
    constArithView :: TTerm -> Maybe (TPrim, Integer, TTerm)
constArithView (TApp (TPrim TPrim
op) [TLit (LitNat Integer
k), TTerm
u])
      | TPrim
op TPrim -> [TPrim] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PAdd, TPrim
PSub] = (TPrim, Integer, TTerm) -> Maybe (TPrim, Integer, TTerm)
forall a. a -> Maybe a
Just (TPrim
op, Integer
k, TTerm
u)
    constArithView (TApp (TPrim TPrim
op) [TTerm
u, TLit (LitNat Integer
k)])
      | TPrim
op TPrim -> TPrim -> Bool
forall a. Eq a => a -> a -> Bool
== TPrim
PAdd = (TPrim, Integer, TTerm) -> Maybe (TPrim, Integer, TTerm)
forall a. a -> Maybe a
Just (TPrim
op, Integer
k, TTerm
u)
      | TPrim
op TPrim -> TPrim -> Bool
forall a. Eq a => a -> a -> Bool
== TPrim
PSub = (TPrim, Integer, TTerm) -> Maybe (TPrim, Integer, TTerm)
forall a. a -> Maybe a
Just (TPrim
PAdd, -Integer
k, TTerm
u)
    constArithView TTerm
_ = Maybe (TPrim, Integer, TTerm)
forall a. Maybe a
Nothing

    simplAlt :: Int -> Induction -> TAlt -> ReaderT SEnv Identity TAlt
simplAlt Int
x Induction
i (TACon QName
c Int
a TTerm
b) =
      QName -> Int -> TTerm -> TAlt
TACon QName
c Int
a (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        [Strictness] -> S TTerm -> S TTerm
forall a. [Strictness] -> S a -> S a
underLams (Int -> Strictness -> [Strictness]
forall a. Int -> a -> [a]
replicate Int
a (EvaluationStrategy -> Induction -> Strictness
defaultConstructorStrictness EvaluationStrategy
eval Induction
i))
          (Int -> TTerm -> S TTerm -> S TTerm
forall {b}.
Int -> TTerm -> ReaderT SEnv Identity b -> ReaderT SEnv Identity b
maybeAddRewrite (Int
x Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
a) TTerm
conTerm (S TTerm -> S TTerm) -> S TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> S TTerm
simpl TTerm
b)
      where
      conTerm :: TTerm
conTerm = TTerm -> [TTerm] -> TTerm
mkTApp (QName -> TTerm
TCon QName
c) ([TTerm] -> TTerm) -> [TTerm] -> TTerm
forall a b. (a -> b) -> a -> b
$ (Int -> TTerm) -> [Int] -> [TTerm]
forall a b. (a -> b) -> [a] -> [b]
map Int -> TTerm
TVar ([Int] -> [TTerm]) -> [Int] -> [TTerm]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
forall a. Integral a => a -> [a]
downFrom Int
a
    simplAlt Int
x Induction
_ (TALit Literal
l TTerm
b) =
      Literal -> TTerm -> TAlt
TALit Literal
l (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> TTerm -> S TTerm -> S TTerm
forall {b}.
Int -> TTerm -> ReaderT SEnv Identity b -> ReaderT SEnv Identity b
maybeAddRewrite Int
x (Literal -> TTerm
TLit Literal
l) (TTerm -> S TTerm
simpl TTerm
b)
    simplAlt Int
x Induction
_ (TAGuard TTerm
g TTerm
b) =
      TTerm -> TTerm -> TAlt
TAGuard (TTerm -> TTerm -> TAlt)
-> S TTerm -> ReaderT SEnv Identity (TTerm -> TAlt)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> S TTerm
simpl TTerm
g ReaderT SEnv Identity (TTerm -> TAlt)
-> S TTerm -> ReaderT SEnv Identity TAlt
forall a b.
ReaderT SEnv Identity (a -> b)
-> ReaderT SEnv Identity a -> ReaderT SEnv Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> TTerm -> S TTerm
simpl TTerm
b

    -- If x is already bound we add a rewrite, otherwise we bind x to rhs.
    maybeAddRewrite :: Int -> TTerm -> ReaderT SEnv Identity b -> ReaderT SEnv Identity b
maybeAddRewrite Int
x TTerm
rhs ReaderT SEnv Identity b
cont = do
      (s, v) <- Int -> S (Strictness, TTerm)
lookupVar Int
x
      case v of
        TVar Int
y | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y -> Int
-> Strictness
-> TTerm
-> ReaderT SEnv Identity b
-> ReaderT SEnv Identity b
forall a. Int -> Strictness -> TTerm -> S a -> S a
bindVar Int
x Strictness
s TTerm
rhs (ReaderT SEnv Identity b -> ReaderT SEnv Identity b)
-> ReaderT SEnv Identity b -> ReaderT SEnv Identity b
forall a b. (a -> b) -> a -> b
$ ReaderT SEnv Identity b
cont
        TTerm
_ -> TTerm
-> TTerm -> ReaderT SEnv Identity b -> ReaderT SEnv Identity b
forall a. TTerm -> TTerm -> S a -> S a
addRewrite TTerm
v TTerm
rhs ReaderT SEnv Identity b
cont

    isTrue :: TTerm -> Bool
isTrue (TCon QName
c) = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
true
    isTrue TTerm
_        = Bool
False

    isFalse :: TTerm -> Bool
isFalse (TCon QName
c) = QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
false
    isFalse TTerm
_        = Bool
False

    maybeMinusToPrim :: TTerm -> [TTerm] -> S TTerm
maybeMinusToPrim f :: TTerm
f@(TDef QName
minus) es :: [TTerm]
es@[TTerm
a, TTerm
b]
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
minus Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
natMinus = do
      leq  <- TTerm -> TTerm -> ReaderT SEnv Identity Bool
checkLeq TTerm
b TTerm
a
      if leq then pure $ tOp PSub a b
             else tApp f es

    maybeMinusToPrim TTerm
f [TTerm]
es = TTerm -> [TTerm] -> S TTerm
tApp TTerm
f [TTerm]
es

    tLet :: Strictness -> TTerm -> TTerm -> TTerm
tLet Strictness
_ (TVar Int
x) TTerm
b = Int -> SubstArg TTerm -> TTerm -> TTerm
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 (Int -> TTerm
TVar Int
x) TTerm
b
    tLet Strictness
_ TTerm
e (TVar Int
0) = TTerm
e
    tLet Strictness
s TTerm
e TTerm
b        = Strictness -> TTerm -> TTerm -> TTerm
TLet Strictness
s TTerm
e TTerm
b

    tCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
    tCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase Int
x CaseInfo
t TTerm
d [] = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
d
    tCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
      | TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
d =
        case [TAlt] -> [TAlt]
forall a. [a] -> [a]
reverse [TAlt]
bs' of
          [] -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
d
          TALit Literal
_ TTerm
b   : [TAlt]
as  -> Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase Int
x CaseInfo
t TTerm
b ([TAlt] -> [TAlt]
forall a. [a] -> [a]
reverse [TAlt]
as)
          TAGuard TTerm
_ TTerm
b : [TAlt]
as  -> Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase Int
x CaseInfo
t TTerm
b ([TAlt] -> [TAlt]
forall a. [a] -> [a]
reverse [TAlt]
as)
          TACon QName
c Int
a TTerm
b : [TAlt]
_   -> Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase' Int
x CaseInfo
t TTerm
d [TAlt]
bs'
      | Bool
otherwise = do
        d' <- TTerm -> S TTerm
lookupIfVar TTerm
d
        case d' of
          TCase Int
y CaseInfo
_ TTerm
d [TAlt]
bs'' | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y ->
            Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase Int
x CaseInfo
t TTerm
d ([TAlt]
bs' [TAlt] -> [TAlt] -> [TAlt]
forall a. [a] -> [a] -> [a]
++ (TAlt -> Bool) -> [TAlt] -> [TAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter (TAlt -> [TAlt] -> Bool
forall {t :: * -> *}. Foldable t => TAlt -> t TAlt -> Bool
`noOverlap` [TAlt]
bs') [TAlt]
bs'')
          TTerm
_ -> Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase' Int
x CaseInfo
t TTerm
d [TAlt]
bs'
      where
        bs' :: [TAlt]
bs' = (TAlt -> Bool) -> [TAlt] -> [TAlt]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool) -> (TAlt -> Bool) -> TAlt -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TAlt -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable) [TAlt]
bs

        lookupIfVar :: TTerm -> S TTerm
lookupIfVar (TVar Int
i) = (Strictness, TTerm) -> TTerm
forall a b. (a, b) -> b
snd ((Strictness, TTerm) -> TTerm) -> S (Strictness, TTerm) -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> S (Strictness, TTerm)
lookupVar Int
i
        lookupIfVar TTerm
t = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
t

    noOverlap :: TAlt -> t TAlt -> Bool
noOverlap TAlt
b t TAlt
bs = Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (TAlt -> Bool) -> t TAlt -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (TAlt -> TAlt -> Bool
overlapped TAlt
b) t TAlt
bs

    overlapped :: TAlt -> TAlt -> Bool
overlapped (TACon QName
c Int
_ TTerm
_)  (TACon QName
c' Int
_ TTerm
_) = QName
c QName -> QName -> Bool
forall a. Eq a => a -> a -> Bool
== QName
c'
    overlapped (TALit Literal
l TTerm
_)    (TALit Literal
l' TTerm
_)   = Literal
l Literal -> Literal -> Bool
forall a. Eq a => a -> a -> Bool
== Literal
l'
    overlapped TAlt
_              TAlt
_              = Bool
False

    -- Drop unreachable cases for Nat and Int cases.
    pruneLitCases :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
    pruneLitCases :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
pruneLitCases Int
x CaseInfo
t TTerm
d [TAlt]
bs | CaseType
CTNat CaseType -> CaseType -> Bool
forall a. Eq a => a -> a -> Bool
== CaseInfo -> CaseType
caseType CaseInfo
t =
      case [TAlt] -> [Integer] -> Maybe Integer -> Maybe [TAlt]
complete [TAlt]
bs [] Maybe Integer
forall a. Maybe a
Nothing of
        Just [TAlt]
bs' -> Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase Int
x CaseInfo
t TTerm
tUnreachable [TAlt]
bs'
        Maybe [TAlt]
Nothing  -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
      where
        complete :: [TAlt] -> [Integer] -> Maybe Integer -> Maybe [TAlt]
complete [TAlt]
bs [Integer]
small (Just Integer
upper)
          | [Integer] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Integer] -> Bool) -> [Integer] -> Bool
forall a b. (a -> b) -> a -> b
$ [Integer
0..Integer
upper Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1] [Integer] -> [Integer] -> [Integer]
forall a. Eq a => [a] -> [a] -> [a]
List.\\ [Integer]
small = [TAlt] -> Maybe [TAlt]
forall a. a -> Maybe a
Just []
        complete (b :: TAlt
b@(TALit (LitNat Integer
n) TTerm
_) : [TAlt]
bs) [Integer]
small Maybe Integer
upper =
          (TAlt
b TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:) ([TAlt] -> [TAlt]) -> Maybe [TAlt] -> Maybe [TAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TAlt] -> [Integer] -> Maybe Integer -> Maybe [TAlt]
complete [TAlt]
bs (Integer
n Integer -> [Integer] -> [Integer]
forall a. a -> [a] -> [a]
: [Integer]
small) Maybe Integer
upper
        complete (b :: TAlt
b@(TAGuard (TApp (TPrim TPrim
PGeq) [TVar Int
y, TLit (LitNat Integer
j)]) TTerm
_) : [TAlt]
bs) [Integer]
small Maybe Integer
upper | Int
x Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
y =
          (TAlt
b TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:) ([TAlt] -> [TAlt]) -> Maybe [TAlt] -> Maybe [TAlt]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [TAlt] -> [Integer] -> Maybe Integer -> Maybe [TAlt]
complete [TAlt]
bs [Integer]
small (Integer -> Maybe Integer
forall a. a -> Maybe a
Just (Integer -> Maybe Integer) -> Integer -> Maybe Integer
forall a b. (a -> b) -> a -> b
$ Integer -> (Integer -> Integer) -> Maybe Integer -> Integer
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Integer
j (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
min Integer
j) Maybe Integer
upper)
        complete [TAlt]
_ [Integer]
_ Maybe Integer
_ = Maybe [TAlt]
forall a. Maybe a
Nothing

    pruneLitCases Int
x CaseInfo
t TTerm
d [TAlt]
bs
      | CaseType
CTInt CaseType -> CaseType -> Bool
forall a. Eq a => a -> a -> Bool
== CaseInfo -> CaseType
caseType CaseInfo
t = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs -- TODO
      | Bool
otherwise           = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs

    -- Drop 'false' branches and drop everything after 'true' branches (including the default
    -- branch)
    pruneBoolGuards :: TTerm -> [TAlt] -> (TTerm, [TAlt])
pruneBoolGuards TTerm
d [] = (TTerm
d, [])
    pruneBoolGuards TTerm
d (b :: TAlt
b@(TAGuard (TCon QName
c) TTerm
_) : [TAlt]
bs)
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
true  = (TTerm
tUnreachable, [TAlt
b])
      | QName -> Maybe QName
forall a. a -> Maybe a
Just QName
c Maybe QName -> Maybe QName -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe QName
false = TTerm -> [TAlt] -> (TTerm, [TAlt])
pruneBoolGuards TTerm
d [TAlt]
bs
    pruneBoolGuards TTerm
d (TAlt
b : [TAlt]
bs) =
      ([TAlt] -> [TAlt]) -> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second (TAlt
b TAlt -> [TAlt] -> [TAlt]
forall a. a -> [a] -> [a]
:) ((TTerm, [TAlt]) -> (TTerm, [TAlt]))
-> (TTerm, [TAlt]) -> (TTerm, [TAlt])
forall a b. (a -> b) -> a -> b
$ TTerm -> [TAlt] -> (TTerm, [TAlt])
pruneBoolGuards TTerm
d [TAlt]
bs

    tCase' :: Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
tCase' Int
x CaseInfo
t TTerm
d [] = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (m :: * -> *) a. Monad m => a -> m a
return TTerm
d
    tCase' Int
x CaseInfo
t TTerm
d [TAlt]
bs = Int -> CaseInfo -> TTerm -> [TAlt] -> S TTerm
pruneLitCases Int
x CaseInfo
t TTerm
d [TAlt]
bs

    tApp :: TTerm -> [TTerm] -> S TTerm
    tApp :: TTerm -> [TTerm] -> S TTerm
tApp (TLet Strictness
s TTerm
e TTerm
b) [TTerm]
es = Strictness -> TTerm -> TTerm -> TTerm
TLet Strictness
s TTerm
e (TTerm -> TTerm) -> S TTerm -> S TTerm
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Strictness -> TTerm -> S TTerm -> S TTerm
forall a. Strictness -> TTerm -> S a -> S a
underLet Strictness
s TTerm
e (TTerm -> [TTerm] -> S TTerm
tApp TTerm
b (Int -> [TTerm] -> [TTerm]
forall a. Subst a => Int -> a -> a
raise Int
1 [TTerm]
es))
    tApp (TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs) [TTerm]
es = do
      d  <- TTerm -> [TTerm] -> S TTerm
tApp TTerm
d [TTerm]
es
      bs <- mapM (flip (tAppAlt (caseInduction t)) es) bs
      simpl $ TCase x t d bs    -- will resimplify branches
    tApp (TVar Int
x) [TTerm]
es = do
      (_, v) <- Int -> S (Strictness, TTerm)
lookupVar Int
x
      case v of
        TTerm
_ | TTerm
v TTerm -> TTerm -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> TTerm
TVar Int
x Bool -> Bool -> Bool
&& TTerm -> Bool
isAtomic TTerm
v -> TTerm -> [TTerm] -> S TTerm
tApp TTerm
v [TTerm]
es
        TLam{} -> TTerm -> [TTerm] -> S TTerm
tApp TTerm
v [TTerm]
es   -- could blow up the code
        TTerm
_      -> TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
mkTApp (Int -> TTerm
TVar Int
x) [TTerm]
es
    tApp TTerm
f [] = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure TTerm
f
    tApp (TLam TTerm
b) (TVar Int
i : [TTerm]
es) = TTerm -> [TTerm] -> S TTerm
tApp (Int -> SubstArg TTerm -> TTerm -> TTerm
forall a. Subst a => Int -> SubstArg a -> a -> a
subst Int
0 (Int -> TTerm
TVar Int
i) TTerm
b) [TTerm]
es
    tApp (TLam TTerm
b) (TTerm
e : [TTerm]
es) =
      TTerm -> [TTerm] -> S TTerm
tApp (Strictness -> TTerm -> TTerm -> TTerm
TLet (EvaluationStrategy -> Strictness
defaultStrictness EvaluationStrategy
eval) TTerm
e TTerm
b) [TTerm]
es
      -- Applications are strict in strict backends and non-strict in
      -- non-strict backends.
    tApp TTerm
f [TTerm]
es = TTerm -> S TTerm
forall a. a -> ReaderT SEnv Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TTerm -> S TTerm) -> TTerm -> S TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> [TTerm] -> TTerm
TApp TTerm
f [TTerm]
es

    tAppAlt :: Induction -> TAlt -> [TTerm] -> ReaderT SEnv Identity TAlt
tAppAlt Induction
i (TACon QName
c Int
a TTerm
b) [TTerm]
es =
      QName -> Int -> TTerm -> TAlt
TACon QName
c Int
a (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
        [Strictness] -> S TTerm -> S TTerm
forall a. [Strictness] -> S a -> S a
underLams (Int -> Strictness -> [Strictness]
forall a. Int -> a -> [a]
replicate Int
a (EvaluationStrategy -> Induction -> Strictness
defaultConstructorStrictness EvaluationStrategy
eval Induction
i))
          (TTerm -> [TTerm] -> S TTerm
tApp TTerm
b (Int -> [TTerm] -> [TTerm]
forall a. Subst a => Int -> a -> a
raise Int
a [TTerm]
es))
    tAppAlt Induction
_ (TALit Literal
l TTerm
b) [TTerm]
es   = Literal -> TTerm -> TAlt
TALit Literal
l   (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> [TTerm] -> S TTerm
tApp TTerm
b [TTerm]
es
    tAppAlt Induction
_ (TAGuard TTerm
g TTerm
b) [TTerm]
es = TTerm -> TTerm -> TAlt
TAGuard TTerm
g (TTerm -> TAlt) -> S TTerm -> ReaderT SEnv Identity TAlt
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TTerm -> [TTerm] -> S TTerm
tApp TTerm
b [TTerm]
es

    isAtomic :: TTerm -> Bool
isAtomic = \case
      TVar{}    -> Bool
True
      TCon{}    -> Bool
True
      TPrim{}   -> Bool
True
      TDef{}    -> Bool
True
      TLit{}    -> Bool
True
      TSort{}   -> Bool
True
      TErased{} -> Bool
True
      TError{}  -> Bool
True
      TTerm
_         -> Bool
False

    checkLeq :: TTerm -> TTerm -> ReaderT SEnv Identity Bool
checkLeq TTerm
a TTerm
b = do
      rho  <- (SEnv -> Substitution' TTerm)
-> ReaderT SEnv Identity (Substitution' TTerm)
forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
asks SEnv -> Substitution' TTerm
envSubst
      rwr  <- asks envRewrite
      let nf = TTerm -> (Integer, [Atom])
toArith (TTerm -> (Integer, [Atom]))
-> (TTerm -> TTerm) -> TTerm -> (Integer, [Atom])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
Substitution' TTerm
rho
          less = [ (TTerm -> (Integer, [Atom])
nf TTerm
a, TTerm -> (Integer, [Atom])
nf TTerm
b) | (TPOp TPrim
PLt TTerm
a TTerm
b, TTerm
rhs) <- [(TTerm, TTerm)]
rwr, TTerm -> Bool
isTrue  TTerm
rhs ]
          leq  = [ (TTerm -> (Integer, [Atom])
nf TTerm
b, TTerm -> (Integer, [Atom])
nf TTerm
a) | (TPOp TPrim
PLt TTerm
a TTerm
b, TTerm
rhs) <- [(TTerm, TTerm)]
rwr, TTerm -> Bool
isFalse TTerm
rhs ]

          match (a
j, a
as) (a
k, a
bs)
            | a
as a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
bs  = a -> Maybe a
forall a. a -> Maybe a
Just (a
j a -> a -> a
forall a. Num a => a -> a -> a
- a
k)
            | Bool
otherwise = Maybe a
forall a. Maybe a
Nothing

          -- Do we have x ≤ y given x' < y' + d ?
          matchEqn a
d (a, a)
x (a, a)
y ((a, a)
x', (a, a)
y') = Maybe () -> Bool
forall a. Maybe a -> Bool
isJust (Maybe () -> Bool) -> Maybe () -> Bool
forall a b. (a -> b) -> a -> b
$ do
            k <- (a, a) -> (a, a) -> Maybe a
forall {a} {a}. (Eq a, Num a) => (a, a) -> (a, a) -> Maybe a
match (a, a)
x (a, a)
x'     -- x = x' + k
            j <- match y y'     -- y = y' + j
            guard (k <= j + d)  -- x ≤ y if k ≤ j + d

          matchLess = Integer
-> (Integer, [Atom])
-> (Integer, [Atom])
-> ((Integer, [Atom]), (Integer, [Atom]))
-> Bool
forall {a} {a} {a}.
(Num a, Ord a, Eq a, Eq a) =>
a -> (a, a) -> (a, a) -> ((a, a), (a, a)) -> Bool
matchEqn Integer
1
          matchLeq  = Integer
-> (Integer, [Atom])
-> (Integer, [Atom])
-> ((Integer, [Atom]), (Integer, [Atom]))
-> Bool
forall {a} {a} {a}.
(Num a, Ord a, Eq a, Eq a) =>
a -> (a, a) -> (a, a) -> ((a, a), (a, a)) -> Bool
matchEqn Integer
0

          literal (a
j, []) (a
k, []) = a
j a -> a -> Bool
forall a. Ord a => a -> a -> Bool
<= a
k
          literal (a, [a])
_ (a, [a])
_ = Bool
False

          -- k + fromWord x ≤ y  if  k + 2^64 - 1 ≤ y
          wordUpperBound (Integer
k, [Pos (TApp (TPrim TPrim
P64ToI) [TTerm]
_)]) (Integer, [Atom])
y = (Integer, [Atom]) -> (Integer, [Atom]) -> Bool
go (Integer
k Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
2 Integer -> Integer -> Integer
forall a b. (Num a, Integral b) => a -> b -> a
^ Integer
64 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1, []) (Integer, [Atom])
y
          wordUpperBound (Integer, [Atom])
_ (Integer, [Atom])
_ = Bool
False

          -- x ≤ k + fromWord y  if  x ≤ k
          wordLowerBound (Integer, [Atom])
a (Integer
k, [Pos (TApp (TPrim TPrim
P64ToI) [TTerm]
_)]) = (Integer, [Atom]) -> (Integer, [Atom]) -> Bool
go (Integer, [Atom])
a (Integer
k, [])
          wordLowerBound (Integer, [Atom])
_ (Integer, [Atom])
_ = Bool
False

          go (Integer, [Atom])
x (Integer, [Atom])
y = [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or
            [ (Integer, [Atom]) -> (Integer, [Atom]) -> Bool
forall {a} {a} {a}. Ord a => (a, [a]) -> (a, [a]) -> Bool
literal (Integer, [Atom])
x (Integer, [Atom])
y
            , (Integer, [Atom]) -> (Integer, [Atom]) -> Bool
wordUpperBound (Integer, [Atom])
x (Integer, [Atom])
y
            , (Integer, [Atom]) -> (Integer, [Atom]) -> Bool
wordLowerBound (Integer, [Atom])
x (Integer, [Atom])
y
            , (((Integer, [Atom]), (Integer, [Atom])) -> Bool)
-> [((Integer, [Atom]), (Integer, [Atom]))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Integer, [Atom])
-> (Integer, [Atom])
-> ((Integer, [Atom]), (Integer, [Atom]))
-> Bool
matchLess (Integer, [Atom])
x (Integer, [Atom])
y) [((Integer, [Atom]), (Integer, [Atom]))]
less
            , (((Integer, [Atom]), (Integer, [Atom])) -> Bool)
-> [((Integer, [Atom]), (Integer, [Atom]))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any ((Integer, [Atom])
-> (Integer, [Atom])
-> ((Integer, [Atom]), (Integer, [Atom]))
-> Bool
matchLeq (Integer, [Atom])
x (Integer, [Atom])
y) [((Integer, [Atom]), (Integer, [Atom]))]
leq ]

      return $ go (nf a) (nf b)

type Arith = (Integer, [Atom])

data Atom = Pos TTerm | Neg TTerm
  deriving (Int -> Atom -> ShowS
[Atom] -> ShowS
Atom -> String
(Int -> Atom -> ShowS)
-> (Atom -> String) -> ([Atom] -> ShowS) -> Show Atom
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Atom -> ShowS
showsPrec :: Int -> Atom -> ShowS
$cshow :: Atom -> String
show :: Atom -> String
$cshowList :: [Atom] -> ShowS
showList :: [Atom] -> ShowS
Show, Atom -> Atom -> Bool
(Atom -> Atom -> Bool) -> (Atom -> Atom -> Bool) -> Eq Atom
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Atom -> Atom -> Bool
== :: Atom -> Atom -> Bool
$c/= :: Atom -> Atom -> Bool
/= :: Atom -> Atom -> Bool
Eq, Eq Atom
Eq Atom =>
(Atom -> Atom -> Ordering)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Bool)
-> (Atom -> Atom -> Atom)
-> (Atom -> Atom -> Atom)
-> Ord Atom
Atom -> Atom -> Bool
Atom -> Atom -> Ordering
Atom -> Atom -> Atom
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Atom -> Atom -> Ordering
compare :: Atom -> Atom -> Ordering
$c< :: Atom -> Atom -> Bool
< :: Atom -> Atom -> Bool
$c<= :: Atom -> Atom -> Bool
<= :: Atom -> Atom -> Bool
$c> :: Atom -> Atom -> Bool
> :: Atom -> Atom -> Bool
$c>= :: Atom -> Atom -> Bool
>= :: Atom -> Atom -> Bool
$cmax :: Atom -> Atom -> Atom
max :: Atom -> Atom -> Atom
$cmin :: Atom -> Atom -> Atom
min :: Atom -> Atom -> Atom
Ord)

aNeg :: Atom -> Atom
aNeg :: Atom -> Atom
aNeg (Pos TTerm
a) = TTerm -> Atom
Neg TTerm
a
aNeg (Neg TTerm
a) = TTerm -> Atom
Pos TTerm
a

aCancel :: [Atom] -> [Atom]
aCancel :: [Atom] -> [Atom]
aCancel (Atom
a : [Atom]
as)
  | (Atom -> Atom
aNeg Atom
a) Atom -> [Atom] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Atom]
as = [Atom] -> [Atom]
aCancel (Atom -> [Atom] -> [Atom]
forall a. Eq a => a -> [a] -> [a]
List.delete (Atom -> Atom
aNeg Atom
a) [Atom]
as)
  | Bool
otherwise          = Atom
a Atom -> [Atom] -> [Atom]
forall a. a -> [a] -> [a]
: [Atom] -> [Atom]
aCancel [Atom]
as
aCancel [] = []

sortR :: Ord a => [a] -> [a]
sortR :: forall a. Ord a => [a] -> [a]
sortR = (a -> a -> Ordering) -> [a] -> [a]
forall a. (a -> a -> Ordering) -> [a] -> [a]
List.sortBy ((a -> a -> Ordering) -> a -> a -> Ordering
forall a b c. (a -> b -> c) -> b -> a -> c
flip a -> a -> Ordering
forall a. Ord a => a -> a -> Ordering
compare)

aAdd :: Arith -> Arith -> Arith
aAdd :: (Integer, [Atom]) -> (Integer, [Atom]) -> (Integer, [Atom])
aAdd (Integer
a, [Atom]
xs) (Integer
b, [Atom]
ys) = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
b, [Atom] -> [Atom]
aCancel ([Atom] -> [Atom]) -> [Atom] -> [Atom]
forall a b. (a -> b) -> a -> b
$ [Atom] -> [Atom]
forall a. Ord a => [a] -> [a]
sortR ([Atom] -> [Atom]) -> [Atom] -> [Atom]
forall a b. (a -> b) -> a -> b
$ [Atom]
xs [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ [Atom]
ys)

aSub :: Arith -> Arith -> Arith
aSub :: (Integer, [Atom]) -> (Integer, [Atom]) -> (Integer, [Atom])
aSub (Integer
a, [Atom]
xs) (Integer
b, [Atom]
ys) = (Integer
a Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
b, [Atom] -> [Atom]
aCancel ([Atom] -> [Atom]) -> [Atom] -> [Atom]
forall a b. (a -> b) -> a -> b
$ [Atom] -> [Atom]
forall a. Ord a => [a] -> [a]
sortR ([Atom] -> [Atom]) -> [Atom] -> [Atom]
forall a b. (a -> b) -> a -> b
$ [Atom]
xs [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ (Atom -> Atom) -> [Atom] -> [Atom]
forall a b. (a -> b) -> [a] -> [b]
map Atom -> Atom
aNeg [Atom]
ys)

fromArith :: Arith -> TTerm
fromArith :: (Integer, [Atom]) -> TTerm
fromArith (Integer
n, []) = Integer -> TTerm
tInt Integer
n
fromArith (Integer
0, [Atom]
xs)
  | ([Atom]
ys, Pos TTerm
a : [Atom]
zs) <- (Atom -> Bool) -> [Atom] -> ([Atom], [Atom])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Atom -> Bool
isPos [Atom]
xs = (TTerm -> Atom -> TTerm) -> TTerm -> [Atom] -> TTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TTerm -> Atom -> TTerm
addAtom TTerm
a ([Atom]
ys [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ [Atom]
zs)
fromArith (Integer
n, [Atom]
xs)
  | Integer
n Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
< Integer
0, ([Atom]
ys, Pos TTerm
a : [Atom]
zs) <- (Atom -> Bool) -> [Atom] -> ([Atom], [Atom])
forall a. (a -> Bool) -> [a] -> ([a], [a])
break Atom -> Bool
isPos [Atom]
xs =
    TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub ((TTerm -> Atom -> TTerm) -> TTerm -> [Atom] -> TTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TTerm -> Atom -> TTerm
addAtom TTerm
a ([Atom]
ys [Atom] -> [Atom] -> [Atom]
forall a. [a] -> [a] -> [a]
++ [Atom]
zs)) (Integer -> TTerm
tInt (-Integer
n))
fromArith (Integer
n, [Atom]
xs) = (TTerm -> Atom -> TTerm) -> TTerm -> [Atom] -> TTerm
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl TTerm -> Atom -> TTerm
addAtom (Integer -> TTerm
tInt Integer
n) [Atom]
xs

isPos :: Atom -> Bool
isPos :: Atom -> Bool
isPos Pos{} = Bool
True
isPos Neg{} = Bool
False

addAtom :: TTerm -> Atom -> TTerm
addAtom :: TTerm -> Atom -> TTerm
addAtom TTerm
t (Pos TTerm
a) = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PAdd TTerm
t TTerm
a
addAtom TTerm
t (Neg TTerm
a) = TPrim -> TTerm -> TTerm -> TTerm
tOp TPrim
PSub TTerm
t TTerm
a

toArith :: TTerm -> Arith
toArith :: TTerm -> (Integer, [Atom])
toArith TTerm
t | Just Integer
n <- TTerm -> Maybe Integer
intView TTerm
t = (Integer
n, [])
toArith (TApp (TPrim TPrim
PAdd) [TTerm
a, TTerm
b]) = (Integer, [Atom]) -> (Integer, [Atom]) -> (Integer, [Atom])
aAdd (TTerm -> (Integer, [Atom])
toArith TTerm
a) (TTerm -> (Integer, [Atom])
toArith TTerm
b)
toArith (TApp (TPrim TPrim
PSub) [TTerm
a, TTerm
b]) = (Integer, [Atom]) -> (Integer, [Atom]) -> (Integer, [Atom])
aSub (TTerm -> (Integer, [Atom])
toArith TTerm
a) (TTerm -> (Integer, [Atom])
toArith TTerm
b)
toArith TTerm
t = (Integer
0, [TTerm -> Atom
Pos TTerm
t])

simplArith :: TTerm -> TTerm
simplArith :: TTerm -> TTerm
simplArith = (Integer, [Atom]) -> TTerm
fromArith ((Integer, [Atom]) -> TTerm)
-> (TTerm -> (Integer, [Atom])) -> TTerm -> TTerm
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TTerm -> (Integer, [Atom])
toArith