{-# LANGUAGE UndecidableInstances #-}

module Agda.Auto.CaseSplit where

import Data.IORef
import Data.Tuple (swap)
import Data.List (findIndex)
import Data.Monoid ((<>), Sum(..))
import Data.Foldable (foldMap)
import qualified Data.Set    as Set
import qualified Data.IntMap as IntMap
import Control.Monad.State as St hiding (lift)
import Control.Monad.Reader as Rd hiding (lift)
import qualified Control.Monad.State as St
import Data.Function

import Agda.Syntax.Common (Hiding(..))
import Agda.Auto.NarrowingSearch
import Agda.Auto.Syntax

import Agda.Auto.SearchControl
import Agda.Auto.Typecheck

import Agda.Utils.Impossible
import Agda.Utils.Monad (or2M)

abspatvarname :: String
abspatvarname = "\0absurdPattern"

costCaseSplitVeryHigh, costCaseSplitHigh, costCaseSplitLow, costAddVarDepth
  :: Cost
costCaseSplitVeryHigh = 10000
costCaseSplitHigh     = 5000
costCaseSplitLow      = 2000
costAddVarDepth       = 1000

data HI a = HI Hiding a

drophid :: [HI a] -> [a]
drophid = map (\(HI _ x) -> x)

type CSPat o = HI (CSPatI o)
type CSCtx o = [HI (MId, MExp o)]

data CSPatI o = CSPatConApp (ConstRef o) [CSPat o]
              | CSPatVar Nat
              | CSPatExp (MExp o)
              | CSWith (MExp o) -- always an App
              | CSAbsurd

              | CSOmittedArg
type Sol o = [(CSCtx o, [CSPat o], Maybe (MExp o))]

caseSplitSearch ::
  forall o . IORef Int -> Int -> [ConstRef o] ->
  Maybe (EqReasoningConsts o) -> Int -> Cost -> ConstRef o ->
  CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch ticks nsolwanted chints meqr depthinterval depth recdef ctx tt pats = do
 let branchsearch :: Cost -> CSCtx o -> MExp o ->
                     ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))
     branchsearch depth ctx tt termcheckenv = do

      nsol <- newIORef 1
      m <- initMeta
      sol <- newIORef Nothing
      let trm = Meta m
          hsol = do trm' <- expandMetas trm
                    writeIORef sol (Just trm')
          initcon = mpret
                  $ Sidecondition
                    (localTerminationSidecond termcheckenv recdef trm)
                  $ (case meqr of
                        Nothing  -> id
                        Just eqr -> mpret . Sidecondition (calcEqRState eqr trm)
                     ) $ tcSearch False (map (fmap closify) (drophid ctx))
                         (closify tt) trm
      recdefd <- readIORef recdef
      let env = RIEnv { rieHints = (recdef, HMRecCall) : map (, HMNormal) chints
                      , rieDefFreeVars = cddeffreevars recdefd
                      , rieEqReasoningConsts = meqr
                      }
      depreached <- topSearch ticks nsol hsol env initcon depth (depth + 1)
      rsol <- readIORef sol
      return rsol
     ctx' = ff 1 ctx
     ff _ [] = []
     ff n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : ff (n + 1) ctx
 caseSplitSearch' branchsearch depthinterval depth recdef ctx' tt pats

caseSplitSearch' :: forall o .
  (Cost -> CSCtx o -> MExp o -> ([Nat], Nat, [Nat]) -> IO (Maybe (MExp o))) ->
  Int -> Cost -> ConstRef o -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
caseSplitSearch' branchsearch depthinterval depth recdef ctx tt pats = do
  recdefd <- readIORef recdef
  sols <- rc depth (cddeffreevars recdefd) ctx tt pats
  return sols
 where
  rc :: Cost -> Int -> CSCtx o -> MExp o -> [CSPat o] -> IO [Sol o]
  rc depth _ _ _ _ | depth < 0 = return []
  rc depth nscrutavoid ctx tt pats = do

    mblkvar <- getblks tt
    fork
     mblkvar
   where
   fork :: [Nat] -> IO [Sol o]
   fork mblkvar = do
    sols1 <- dobody
    case sols1 of
     (_:_) -> return sols1
     [] -> do
      let r :: [Nat] -> IO [Sol o]
          r [] = return []
          r (v:vs) = do
           sols2 <- splitvar mblkvar v
           case sols2 of
            (_:_) -> return sols2
            [] -> r vs
      r [nv - x | x <- [0..nv]] -- [0..length ctx - 1 - nscrutavoid]
    where nv = length ctx - 1
   dobody :: IO [Sol o]
   dobody = do
    case findperm (map snd (drophid ctx)) of
     Just perm -> do
      let (ctx', tt', pats') = applyperm perm ctx tt pats
      res <- branchsearch depth ctx' tt' (localTerminationEnv pats')
      return $ case res of
       Just trm -> [[(ctx', pats', Just trm)]]
       Nothing -> []
     Nothing -> __IMPOSSIBLE__ -- no permutation found
   splitvar :: [Nat] -> Nat -> IO [Sol o]
   splitvar mblkvar scrut = do
    let scruttype = infertypevar ctx scrut
    case rm __IMPOSSIBLE__ scruttype of
     App _ _ (Const c) _ -> do
      cd <- readIORef c
      case cdcont cd of
       Datatype cons _ -> do
         sols <- dobranches cons
         return $ map (\sol -> case sol of
          [] ->
           case findperm (map snd (drophid ctx)) of
            Just perm ->
             let HI scrhid(_, scrt) = ctx !! scrut
                 ctx1 = take scrut ctx ++ (HI scrhid (Id abspatvarname, scrt)) : drop (scrut + 1) ctx
                 (ctx', _, pats') = applyperm perm ctx1 tt ({-map (replacep scrut 1 CSAbsurd __IMPOSSIBLE__) -}pats)
             in [(ctx', pats', Nothing)]
            Nothing -> __IMPOSSIBLE__ -- no permutation found
          _ -> sol
          ) sols
        where
         dobranches :: [ConstRef o] -> IO [Sol o]
         dobranches [] = return [[]]
         dobranches (con : cons) = do
          cond <- readIORef con
          let ff t = case rm __IMPOSSIBLE__ t of
                        Pi _ h _ it (Abs id ot) ->
                         let (xs, inft) = ff ot
                         in (((h, scrut + length xs), id, lift (scrut + length xs + 1) it) : xs, inft)
                        _ -> ([], lift scrut t)
              (newvars, inftype) = ff (cdtype cond)
              constrapp = NotM $ App Nothing (NotM OKVal) (Const con) (foldl (\xs ((h, v), _, _) -> NotM $ ALCons h (NotM $ App Nothing (NotM OKVal) (Var v) (NotM ALNil)) xs) (NotM ALNil) (reverse newvars))
              pconstrapp = CSPatConApp con (map (\((hid, v), _, _) -> HI hid (CSPatVar v)) newvars)
              thesub = replace scrut (length newvars) constrapp
              Id newvarprefix = fst $ (drophid ctx) !! scrut
              ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take scrut ctx) ++
                     reverse (map (\(((hid, _), id, t), i) ->
                       HI hid (Id (case id of {NoId -> newvarprefix{- ++ show i-}; Id id -> id}), t)
                      ) (zip newvars [0..])) ++
                     map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (scrut + 1) ctx)
              tt' = thesub tt
              pats' = map (replacep scrut (length newvars) pconstrapp constrapp) pats
              scruttype' = thesub scruttype  -- scruttype shouldn't really refer to scrutvar so lift is enough, but what if circular ref has been created and this is not detected until case split is done
          case unifyexp inftype scruttype' of
           Nothing -> do
            res <- notequal scrut (length newvars) scruttype' inftype
            if res then -- branch absurd
              dobranches cons
             else -- branch dont know
              return []
           Just unif ->
            do
             let (ctx2, tt2, pats2) = removevar ctx1 tt' pats' unif
                 --cost = if elem scrut mblkvar then costCaseSplit - (costCaseSplit - costCaseSplitFollow) `div` (length mblkvar) else costCaseSplit
                 cost = if null mblkvar then
                         if scrut < length ctx - nscrutavoid && nothid
                         then costCaseSplitLow + costAddVarDepth
                              * Cost (depthofvar scrut pats)
                         else costCaseSplitVeryHigh
                        else
                         if scrut `elem` mblkvar then costCaseSplitLow else (if scrut < length ctx - nscrutavoid && nothid then costCaseSplitHigh else costCaseSplitVeryHigh)

                 nothid = let HI hid _ = ctx !! scrut
                          in hid == NotHidden


             sols <- rc (depth - cost) (length ctx - 1 - scrut) ctx2 tt2 pats2
             case sols of
              [] -> return []
              _ -> do
               sols2 <- dobranches cons
               return $ concat (map (\sol -> map (\sol2 -> sol ++ sol2) sols2) sols)
       _ -> return [] -- split failed "scrut type is not datatype"
     _ -> return [] -- split failed "scrut type is not datatype"

infertypevar :: CSCtx o -> Nat -> MExp o
infertypevar ctx v = snd $ (drophid ctx) !! v

class Replace o t u | t u -> o where
  replace' :: Nat -> MExp o -> t -> Reader (Nat, Nat) u

replace :: Replace o t u => Nat -> Nat -> MExp o -> t -> u
replace sv nnew e t = replace' 0 e t `runReader` (sv, nnew)

instance Replace o t u => Replace o (Abs t) (Abs u) where
  replace' n re (Abs mid b) = Abs mid <$> replace' (n + 1) re b

instance Replace o (Exp o) (MExp o) where
  replace' n re e = case e of
    App uid ok elr@(Var v) args -> do
      ih         <- NotM <$> replace' n re args
      (sv, nnew) <- ask
      return $
        if v >= n
        then if v - n == sv
             then betareduce (lift n re) ih
             else if v - n > sv
                  then NotM $ App uid ok (Var (v + nnew - 1)) ih
                  else NotM $ App uid ok elr ih
        else NotM $ App uid ok elr ih
    App uid ok elr@Const{} args ->
      NotM . App uid ok elr . NotM <$> replace' n re args
    Lam hid b -> NotM . Lam hid <$> replace' (n + 1) re b
    Pi uid hid possdep it b ->
      fmap NotM $ Pi uid hid possdep <$> replace' n re it <*> replace' n re b
    Sort{} -> return $ NotM e
    AbsurdLambda{} -> return $ NotM e

instance Replace o t u => Replace o (MM t (RefInfo o)) u where
  replace' n re = replace' n re . rm __IMPOSSIBLE__

instance Replace o (ArgList o) (ArgList o) where
  replace' n re args = case args of
    ALNil           -> return ALNil
    ALCons hid a as ->
      ALCons hid <$> replace' n re a <*> (NotM <$> replace' n re as)
    ALProj{}        -> __IMPOSSIBLE__
    ALConPar as     -> ALConPar . NotM <$> replace' n re as


betareduce :: MExp o -> MArgList o -> MExp o
betareduce e args = case rm __IMPOSSIBLE__ args of
 ALNil -> e
 ALCons _ a rargs -> case rm __IMPOSSIBLE__ e of
  App uid ok elr eargs -> NotM $ App uid ok elr (concatargs eargs args)
  Lam _ (Abs _ b) -> betareduce (replace 0 0 a b) rargs
  _ -> __IMPOSSIBLE__ -- not type correct if this happens
 ALProj{} -> __IMPOSSIBLE__
 ALConPar as -> __IMPOSSIBLE__

concatargs :: MArgList o -> MArgList o -> MArgList o
concatargs xs ys = case rm __IMPOSSIBLE__ xs of
  ALNil -> ys

  ALCons hid x xs -> NotM $ ALCons hid x (concatargs xs ys)

  ALProj{} -> __IMPOSSIBLE__

  ALConPar as -> NotM $ ALConPar (concatargs xs ys)

replacep :: forall o. Nat -> Nat -> CSPatI o -> MExp o -> CSPat o -> CSPat o
replacep sv nnew rp re = r
 where
  r :: CSPat o -> CSPat o
  r (HI hid (CSPatConApp c ps)) = HI hid (CSPatConApp c (map r ps))
  r (HI hid (CSPatVar v)) = if v == sv then
                    HI hid rp
                   else
                    if v > sv then
                     HI hid (CSPatVar (v + nnew - 1))
                    else
                     HI hid (CSPatVar v)
  r (HI hid (CSPatExp e)) = HI hid (CSPatExp $ replace sv nnew re e)

  r p@(HI _ CSOmittedArg) = p

  r _ = __IMPOSSIBLE__ -- other constructors dont appear in indata Pats



-- Unification takes two values of the same type and generates a list
-- of assignments making the two terms equal.

type Assignments o = [(Nat, Exp o)]

class Unify o t | t -> o where
  unify'    :: t -> t -> StateT (Assignments o) Maybe ()
  notequal' :: t -> t -> ReaderT (Nat, Nat) (StateT (Assignments o) IO) Bool

unify :: Unify o t => t -> t -> Maybe (Assignments o)
unify t u = unify' t u `execStateT` []

notequal :: Unify o t => Nat -> Nat -> t -> t -> IO Bool
notequal fstnew nbnew t1 t2 = notequal' t1 t2 `runReaderT` (fstnew, nbnew)
                                              `evalStateT` []

instance Unify o t => Unify o (MM t (RefInfo o)) where
  unify' = unify' `on` rm __IMPOSSIBLE__

  notequal' = notequal' `on` rm __IMPOSSIBLE__

unifyVar :: Nat -> Exp o -> StateT (Assignments o) Maybe ()
unifyVar v e = do
  unif <- get
  case lookup v unif of
    Nothing -> modify ((v, e) :)
    Just e' -> unify' e e'

instance Unify o t => Unify o (Abs t) where
  unify' (Abs _ b1) (Abs _ b2) = unify' b1 b2

  notequal' (Abs _ b1) (Abs _ b2) = notequal' b1 b2

instance Unify o (Exp o) where
  unify' e1 e2 = case (e1, e2) of
   (App _ _ elr1 args1, App _ _ elr2 args2) | elr1 == elr2 -> unify' args1 args2
   (Lam hid1 b1, Lam hid2 b2)               | hid1 == hid2 -> unify' b1 b2
   (Pi _ hid1 _ a1 b1, Pi _ hid2 _ a2 b2)   | hid1 == hid2 -> unify' a1 a2
                                                           >> unify' b1 b2
   (Sort _, Sort _) -> return () -- a bit sloppy
   (App _ _ (Var v) (NotM ALNil), _)
     | v `Set.member` (freeVars e2) -> St.lift Nothing -- Occurs check
   (_, App _ _ (Var v) (NotM ALNil))
     | v `Set.member` (freeVars e1) -> St.lift Nothing -- Occurs check
   (App _ _ (Var v) (NotM ALNil), _) -> unifyVar v e2
   (_, App _ _ (Var v) (NotM ALNil)) -> unifyVar v e1
   _ -> St.lift Nothing

  notequal' e1 e2 = do
    (fstnew, nbnew) <- ask
    unifier         <- get
    case (e1, e2) of
      (App _ _ elr1 es1, App _ _ elr2 es2) | elr1 == elr2 -> notequal' es1 es2
      (_, App _ _ (Var v2) (NotM ALNil)) -- why is this not symmetric?!
        | fstnew <= v2 && v2 < fstnew + nbnew ->
        case lookup v2 unifier of
          Nothing  -> modify ((v2, e1):) >> return False
          Just e2' -> notequal' e1 e2'
{-
  GA: Skipped these: Not sure why we'd claim they're impossible
      (_, App _ _ (Var v2) (NotM ALProj{})) -> __IMPOSSIBLE__
      (_, App _ _ (Var v2) (NotM ALConPar{})) -> __IMPOSSIBLE__
-}
      (App _ _ (Const c1) es1, App _ _ (Const c2) es2) -> do
        cd1 <- liftIO $ readIORef c1
        cd2 <- liftIO $ readIORef c2
        case (cdcont cd1, cdcont cd2) of
          (Constructor{}, Constructor{}) -> if c1 == c2 then notequal' es1 es2
                                            else return True
          _ -> return False
{- GA: Why don't we have a case for distinct heads after all these
       unification cases for vars with no spines & metas that can
       be looked up?
      (App _ _ elr1 _, App _ _ elr2 _) | elr1 <> elr2 -> return True
-}
      _ -> return False

instance Unify o (ArgList o) where
  unify' args1 args2 = case (args1, args2) of
   (ALNil, ALNil) -> pure ()
   (ALCons hid1 a1 as1, ALCons hid2 a2 as2) | hid1 == hid2 -> unify' a1 a2
                                                           >> unify' as1 as2
   (ALConPar as1, ALCons _ _ as2) -> unify' as1 as2
   (ALCons _ _ as1, ALConPar as2) -> unify' as1 as2
   (ALConPar as1, ALConPar as2)   -> unify' as1 as2
   _ -> St.lift Nothing

  notequal' args1 args2 = case (args1, args2) of
    (ALCons _ e es, ALCons _ f fs) -> notequal' e f `or2M` notequal' es fs
    (ALConPar es1, ALConPar es2)   -> notequal' es1 es2
    _                              -> return False

-- This definition is only here to respect the previous interface.
unifyexp :: MExp o -> MExp o -> Maybe ([(Nat, MExp o)])
unifyexp e1 e2 = fmap (NotM <$>) <$> unify e1 e2

class Lift t where
  lift' :: Nat -> Nat -> t -> t

lift :: Lift t => Nat -> t -> t
lift 0 = id
lift n = lift' n 0

instance Lift t => Lift (Abs t) where
  lift' n j (Abs mid b) = Abs mid (lift' n (j + 1) b)

instance Lift t => Lift (MM t r) where
  lift' n j = NotM . lift' n j . rm __IMPOSSIBLE__

instance Lift (Exp o) where
  lift' n j e = case e of
    App uid ok elr args -> case elr of
      Var v | v >= j -> App uid ok (Var (v + n)) (lift' n j args)
      _ -> App uid ok elr (lift' n j args)
    Lam hid b -> Lam hid (lift' n j b)
    Pi uid hid possdep it b -> Pi uid hid possdep (lift' n j it) (lift' n j b)
    Sort{} -> e
    AbsurdLambda{} -> e

instance Lift (ArgList o) where
  lift' n j args = case args of
    ALNil           -> ALNil
    ALCons hid a as -> ALCons hid (lift' n j a) (lift' n j as)
    ALProj{}        -> __IMPOSSIBLE__
    ALConPar as     -> ALConPar (lift' n j as)


removevar :: CSCtx o -> MExp o -> [CSPat o] -> [(Nat, MExp o)] -> (CSCtx o, MExp o, [CSPat o])
removevar ctx tt pats [] = (ctx, tt, pats)
removevar ctx tt pats ((v, e) : unif) =
 let
  e2 = replace v 0 __IMPOSSIBLE__ {- occurs check failed -} e
  thesub = replace v 0 e2
  ctx1 = map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (take v ctx) ++
         map (\(HI hid (id, t)) -> HI hid (id, thesub t)) (drop (v + 1) ctx)
  tt' = thesub tt
  pats' = map (replacep v 0 (CSPatExp e2) e2) pats
  unif' = map (\(uv, ue) -> (if uv > v then uv - 1 else uv, thesub ue)) unif
 in
  removevar ctx1 tt' pats' unif'

findperm :: [MExp o] -> Maybe [Nat]
findperm ts =
 let
  frees = map freevars ts
  m = IntMap.fromList $
      map (\i -> (i, length (filter (elem i) frees)))
          [0..length ts - 1]
  r _ perm 0 = Just $ reverse perm
  r m perm n =
   case lookup 0 (map swap (IntMap.toList m)) of
    Nothing -> Nothing
    Just i -> r (foldl (flip $ IntMap.adjust (subtract 1))
                       (IntMap.insert i (-1) m)
                       (frees !! i))
                 (i : perm) (n - 1)
 in r m [] (length ts)


freevars :: FreeVars t => t -> [Nat]
freevars = Set.toList . freeVars

applyperm :: [Nat] -> CSCtx o -> MExp o -> [CSPat o] ->
             (CSCtx o, MExp o, [CSPat o])
applyperm perm ctx tt pats =
 let ctx1 = map (\(HI hid (id, t)) -> HI hid (id, rename (ren perm) t)) ctx
     ctx2 = map (\i -> ctx1 !! i) perm
     ctx3 = seqctx ctx2
     tt' = rename (ren perm) tt
     pats' = map (rename (ren perm)) pats
 in (ctx3, tt', pats')

ren :: [Nat] -> Nat -> Int
ren n i = let Just j = findIndex (== i) n in j

instance Renaming t => Renaming (HI t) where
  renameOffset j ren (HI hid t) = HI hid $ renameOffset j ren t

instance Renaming (CSPatI o) where
  renameOffset j ren e = case e of
    CSPatConApp c pats -> CSPatConApp c $ map (renameOffset j ren) pats
    CSPatVar i         -> CSPatVar $ j + ren i
    CSPatExp e         -> CSPatExp $ renameOffset j ren e
    CSOmittedArg       -> e
    _                  -> __IMPOSSIBLE__

seqctx :: CSCtx o -> CSCtx o
seqctx = r (-1)
 where
  r _ [] = []
  r n (HI hid (id, t) : ctx) = HI hid (id, lift n t) : r (n - 1) ctx
-- --------------------

depthofvar :: Nat -> [CSPat o] -> Nat
depthofvar v pats =
 let [depth] = concatMap (f 0) (drophid pats)
     f d (CSPatConApp _ pats) = concatMap (f (d + 1)) (drophid pats)
     f d (CSPatVar v') = if v == v' then [d] else []
     f _ _ = []
 in depth

-- --------------------
-- | Speculation: Type class computing the size (?) of a pattern
--   and collecting the vars it introduces
class LocalTerminationEnv a where
  sizeAndBoundVars :: a -> (Sum Nat, [Nat])

instance LocalTerminationEnv a => LocalTerminationEnv (HI a) where
  sizeAndBoundVars (HI _ p) = sizeAndBoundVars p

instance LocalTerminationEnv (CSPatI o) where
  sizeAndBoundVars p = case p of
    CSPatConApp _ ps -> (1, []) <> sizeAndBoundVars ps
    CSPatVar n       -> (0, [n])
    CSPatExp e       -> sizeAndBoundVars e
    _                -> (0, [])

instance LocalTerminationEnv a => LocalTerminationEnv [a] where
  sizeAndBoundVars = foldMap sizeAndBoundVars

instance LocalTerminationEnv (MExp o) where
--  sizeAndBoundVars e = case rm __IMPOSSIBLE__ e of
-- GA: 2017 06 27: Not actually impossible! (cf. #2620)
  sizeAndBoundVars Meta{} = (0, [])
-- Does this default behaviour even make sense? The catchall in the
-- following match seems to suggest it does
  sizeAndBoundVars (NotM e) = case e of
    App _ _ (Var v) _      -> (0, [v])
    App _ _ (Const _) args -> (1, []) <> sizeAndBoundVars args
    _                      -> (0, [])

instance (LocalTerminationEnv a, LocalTerminationEnv b) => LocalTerminationEnv (a, b) where
  sizeAndBoundVars (a, b) = sizeAndBoundVars a <> sizeAndBoundVars b

instance LocalTerminationEnv (MArgList o) where
  sizeAndBoundVars as = case rm __IMPOSSIBLE__ as of
    ALNil         -> (0, [])
    ALCons _ a as -> sizeAndBoundVars (a, as)
    ALProj{}      -> __IMPOSSIBLE__
    ALConPar as   -> sizeAndBoundVars as


-- | Take a list of patterns and returns (is, size, vars) where (speculation):
---  * the is are the pattern indices the vars are contained in
--   * size is total number of constructors removed (?) to access vars
localTerminationEnv :: [CSPat o] -> ([Nat], Nat, [Nat])
localTerminationEnv pats = (is, getSum s, vs) where

  (is , s , vs) = g 0 pats

  g :: Nat -> [CSPat o] -> ([Nat], Sum Nat, [Nat])
  g _ [] = ([], 0, [])
  g i (hp@(HI _ p) : ps) = case p of
    CSPatConApp{} -> let (size, vars) = sizeAndBoundVars hp
                     in ([i], size, vars) <> g (i + 1) ps
    _ -> g (i + 1) ps

localTerminationSidecond :: ([Nat], Nat, [Nat]) -> ConstRef o -> MExp o -> EE (MyPB o)
localTerminationSidecond (is, size, vars) reccallc b =
  ok b
 where
     ok e = mmpcase (False, prioNo, Nothing) e $ \e -> case e of
      App _ _ elr args -> mpret $ Sidecondition
       (oks args)
       (case elr of
          Const c | c == reccallc -> if size == 0 then mpret (Error "localTerminationSidecond: no size to decrement") else okcall 0 size vars args
          _ -> mpret OK
       )
      Lam _ (Abs _ e) -> ok e
      Pi _ _ _ it (Abs _ ot) -> mpret $ Sidecondition
       (ok it)
       (ok ot)
      Sort{} -> mpret OK

      AbsurdLambda{} -> mpret OK


     oks as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of
      ALNil -> mpret OK
      ALCons _ a as -> mpret $ Sidecondition
       (ok a)
       (oks as)

      ALProj eas _ _ as -> mpret $ Sidecondition (oks eas) (oks as)


      ALConPar as -> oks as

     okcall i size vars as = mmpcase (False, prioNo, Nothing) as $ \as -> case as of
      ALNil -> mpret OK
      ALCons _ a as | i `elem` is ->
       mbpcase prioNo Nothing (he size vars a) $ \x -> case x of
        Nothing -> mpret $ Error "localTerminationSidecond: reccall not ok"
        Just (size', vars') -> okcall (i + 1) size' vars' as
      ALCons _ a as -> okcall (i + 1) size vars as

      ALProj{} -> mpret OK


      ALConPar as -> __IMPOSSIBLE__

     he size vars e = mmcase e $ \e -> case e of
      App _ _ (Var v) _ ->
       case remove v vars of
        Nothing -> mbret Nothing
        Just vars' -> mbret $ Just (size, vars')
      App _ _ (Const c) args -> do
       cd <- readIORef c
       case cdcont cd of
        Constructor{} ->
         if size == 1 then
          mbret Nothing
         else
          hes (size - 1) vars args
        _ -> mbret Nothing
      _ -> mbret Nothing
     hes size vars as = mmcase as $ \as -> case as of
      ALNil -> mbret $ Just (size, vars)
      ALCons _ a as ->
       mbcase (he size vars a) $ \x -> case x of
        Nothing -> mbret Nothing
        Just (size', vars') -> hes size' vars' as

      ALProj{} -> __IMPOSSIBLE__


      ALConPar as -> __IMPOSSIBLE__

     remove _ [] = Nothing
     remove x (y : ys) | x == y = Just ys
     remove x (y : ys) = case remove x ys of {Nothing -> Nothing; Just ys' -> Just (y : ys')}

-- ---------------------------


getblks :: MExp o -> IO [Nat]
getblks tt = do
 NotB (hntt, blks) <- hnn_blks (Clos [] tt)
 case f blks of
  Just v -> return [v]
  Nothing -> case rawValue hntt of
   HNApp (Const c) args -> do
    cd <- readIORef c
    case cdcont cd of
     Datatype{} -> g [] args
     _ -> return []
   _ -> return []
 where
  f blks = case blks of
             (_:_) -> case rawValue (last blks) of
              HNApp (Var v) _ -> Just v
              _ -> Nothing
             _ -> Nothing
  g vs args = do
   NotB hnargs <- hnarglist args
   case hnargs of
    HNALCons _ a as -> do
     NotB (_, blks) <- hnn_blks a
     let vs' = case f blks of
                Just v | v `notElem` vs -> v : vs
                _ -> vs
     g vs' as
    _ -> return vs
-- ---------------------------