{-# LANGUAGE CPP #-}
module Agda.Compiler.Treeless.Uncase (caseToSeq) where

import Data.Monoid

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

import Agda.Utils.Impossible
#include "undefined.h"

caseToSeq :: Monad m => TTerm -> m TTerm
caseToSeq t = return $ uncase t

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

    doCase x t d bs
      | Just u <- mu,
        all (equalTo x u) bs = maybeSeq u
      | otherwise            = fallback
      where
        maybeSeq u | caseLazy t = u
                   | otherwise  = tApp (TPrim PSeq) [TVar x, u]
        fallback = TCase x t d bs
        (fv, mu)
          | isUnreachable d =
            case last bs of
              TACon _ a b -> (a, tryStrengthen a b)
              TALit l b   -> (0, Just b)
              TAGuard _ b -> (0, Just b)
          | otherwise = (0, Just d)

    equalTo :: Int -> TTerm -> TAlt -> Bool
    equalTo x t (TACon c a b)
      | Just b' <- tryStrengthen a b = equalTerms (subst x v t) (subst x v b')
      | otherwise                    = False
      where v = mkTApp (TCon c) (replicate a TErased)
    equalTo x t (TALit l b)   = equalTerms (subst x (TLit l) t) (subst x (TLit l) b)
    equalTo x t (TAGuard _ b) = equalTerms t b

    tLet e b =
      case occursIn 0 b of
        Occurs 0 _ _ -> strengthen __IMPOSSIBLE__ b
        _            -> TLet e b

    -- Primitive operations are already strict
    tApp (TPrim PSeq) [_, b@(TApp (TPrim op) _)]
      | op `elem` [PAdd, PSub, PMul, PLt, PGeq, PRem, PQuot] || isPrimEq op = b
    tApp f es = TApp f es