module Agda.Compiler.Treeless.Uncase (caseToSeq) where

import Agda.Syntax.Treeless
import Agda.TypeChecking.Substitute
import Agda.Compiler.Treeless.Subst
import Agda.Compiler.Treeless.Compare

import Agda.Utils.Impossible

caseToSeq :: Monad m => TTerm -> m TTerm
caseToSeq :: TTerm -> m TTerm
caseToSeq TTerm
t = TTerm -> m TTerm
forall (m :: * -> *) a. Monad m => a -> m a
return (TTerm -> m TTerm) -> TTerm -> m TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
uncase TTerm
t

uncase :: TTerm -> TTerm
uncase :: TTerm -> TTerm
uncase TTerm
t = case TTerm
t of
  TVar{}    -> TTerm
t
  TPrim{}   -> TTerm
t
  TDef{}    -> TTerm
t
  TApp TTerm
f Args
es -> TTerm -> Args -> TTerm
tApp (TTerm -> TTerm
uncase TTerm
f) ((TTerm -> TTerm) -> Args -> Args
forall a b. (a -> b) -> [a] -> [b]
map TTerm -> TTerm
uncase Args
es)
  TLam TTerm
b    -> TTerm -> TTerm
TLam (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
uncase TTerm
b
  TLit{}    -> TTerm
t
  TCon{}    -> TTerm
t
  TLet TTerm
e TTerm
b  -> TTerm -> TTerm -> TTerm
tLet (TTerm -> TTerm
uncase TTerm
e) (TTerm -> TTerm
uncase TTerm
b)
  TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
doCase Int
x CaseInfo
t (TTerm -> TTerm
uncase TTerm
d) ((TAlt -> TAlt) -> [TAlt] -> [TAlt]
forall a b. (a -> b) -> [a] -> [b]
map TAlt -> TAlt
uncaseAlt [TAlt]
bs)
  TUnit{}   -> TTerm
t
  TSort{}   -> TTerm
t
  TErased{} -> TTerm
t
  TError{}  -> TTerm
t
  TCoerce TTerm
t -> TTerm -> TTerm
TCoerce (TTerm -> TTerm
uncase TTerm
t)
  where
    uncaseAlt :: TAlt -> TAlt
uncaseAlt (TACon QName
c Int
a TTerm
b) = QName -> Int -> TTerm -> TAlt
TACon QName
c Int
a (TTerm -> TAlt) -> TTerm -> TAlt
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
uncase TTerm
b
    uncaseAlt (TALit Literal
l TTerm
b)   = Literal -> TTerm -> TAlt
TALit Literal
l (TTerm -> TAlt) -> TTerm -> TAlt
forall a b. (a -> b) -> a -> b
$ TTerm -> TTerm
uncase TTerm
b
    uncaseAlt (TAGuard TTerm
g TTerm
b) = TTerm -> TTerm -> TAlt
TAGuard (TTerm -> TTerm
uncase TTerm
g) (TTerm -> TTerm
uncase TTerm
b)

    doCase :: Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
doCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
      | Just TTerm
u <- Maybe TTerm
mu,
        (TAlt -> Bool) -> [TAlt] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Int -> TTerm -> TAlt -> Bool
equalTo Int
x TTerm
u) [TAlt]
bs = TTerm -> TTerm
maybeSeq TTerm
u
      | Bool
otherwise            = TTerm
fallback
      where
        maybeSeq :: TTerm -> TTerm
maybeSeq TTerm
u | CaseInfo -> Bool
caseLazy CaseInfo
t = TTerm
u
                   | Bool
otherwise  = TTerm -> Args -> TTerm
tApp (TPrim -> TTerm
TPrim TPrim
PSeq) [Int -> TTerm
TVar Int
x, TTerm
u]
        fallback :: TTerm
fallback = Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
x CaseInfo
t TTerm
d [TAlt]
bs
        (Int
fv, Maybe TTerm
mu)
          | TTerm -> Bool
forall a. Unreachable a => a -> Bool
isUnreachable TTerm
d =
            case [TAlt] -> TAlt
forall a. [a] -> a
last [TAlt]
bs of
              TACon QName
_ Int
a TTerm
b -> (Int
a, Int -> TTerm -> Maybe TTerm
forall a t. (HasFree a, Subst t a) => Int -> a -> Maybe a
tryStrengthen Int
a TTerm
b)
              TALit Literal
l TTerm
b   -> (Int
0, TTerm -> Maybe TTerm
forall a. a -> Maybe a
Just TTerm
b)
              TAGuard TTerm
_ TTerm
b -> (Int
0, TTerm -> Maybe TTerm
forall a. a -> Maybe a
Just TTerm
b)
          | Bool
otherwise = (Int
0, TTerm -> Maybe TTerm
forall a. a -> Maybe a
Just TTerm
d)

    equalTo :: Int -> TTerm -> TAlt -> Bool
    equalTo :: Int -> TTerm -> TAlt -> Bool
equalTo Int
x TTerm
t (TACon QName
c Int
a TTerm
b)
      | Just TTerm
b' <- Int -> TTerm -> Maybe TTerm
forall a t. (HasFree a, Subst t a) => Int -> a -> Maybe a
tryStrengthen Int
a TTerm
b = TTerm -> TTerm -> Bool
equalTerms (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst Int
x TTerm
v TTerm
t) (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst Int
x TTerm
v TTerm
b')
      | Bool
otherwise                    = Bool
False
      where v :: TTerm
v = TTerm -> Args -> TTerm
mkTApp (QName -> TTerm
TCon QName
c) (Int -> TTerm -> Args
forall a. Int -> a -> [a]
replicate Int
a TTerm
TErased)
    equalTo Int
x TTerm
t (TALit Literal
l TTerm
b)   = TTerm -> TTerm -> Bool
equalTerms (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst Int
x (Literal -> TTerm
TLit Literal
l) TTerm
t) (Int -> TTerm -> TTerm -> TTerm
forall t a. Subst t a => Int -> t -> a -> a
subst Int
x (Literal -> TTerm
TLit Literal
l) TTerm
b)
    equalTo Int
x TTerm
t (TAGuard TTerm
_ TTerm
b) = TTerm -> TTerm -> Bool
equalTerms TTerm
t TTerm
b

    tLet :: TTerm -> TTerm -> TTerm
tLet TTerm
e TTerm
b =
      case Int -> TTerm -> Occurs
forall a. HasFree a => Int -> a -> Occurs
occursIn Int
0 TTerm
b of
        Occurs Int
0 UnderLambda
_ SeqArg
_ -> Empty -> TTerm -> TTerm
forall t a. Subst t a => Empty -> a -> a
strengthen Empty
forall a. HasCallStack => a
__IMPOSSIBLE__ TTerm
b
        Occurs
_            -> TTerm -> TTerm -> TTerm
TLet TTerm
e TTerm
b

    -- Primitive operations are already strict
    tApp :: TTerm -> Args -> TTerm
tApp (TPrim TPrim
PSeq) [TTerm
_, b :: TTerm
b@(TApp (TPrim TPrim
op) Args
_)]
      | TPrim
op TPrim -> [TPrim] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [TPrim
PAdd, TPrim
PSub, TPrim
PMul, TPrim
PLt, TPrim
PGeq, TPrim
PRem, TPrim
PQuot] Bool -> Bool -> Bool
|| TPrim -> Bool
isPrimEq TPrim
op = TTerm
b
    tApp TTerm
f Args
es = TTerm -> Args -> TTerm
TApp TTerm
f Args
es