module Quox.Whnf.ComputeElimType

import Quox.Whnf.Interface
import Quox.Displace
import Quox.Pretty

%default total


||| performs the minimum work required to recompute the type of an elim.
|||
||| - assumes the elim is already typechecked
||| - the return value is not reduced
export covering
computeElimType :
  CanWhnf Term Interface.isRedexT =>
  CanWhnf Elim Interface.isRedexE =>
  (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
  Eff Whnf (Term d n)

||| computes a type and then reduces it to whnf
export covering
computeWhnfElimType0 :
  CanWhnf Term Interface.isRedexT =>
  CanWhnf Elim Interface.isRedexE =>
  (defs : Definitions) -> (ctx : WhnfContext d n) -> (0 sg : SQty) ->
  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
  Eff Whnf (Term d n)


private covering
computeElimTypeNoLog, computeWhnfElimType0NoLog :
  CanWhnf Term Interface.isRedexT =>
  CanWhnf Elim Interface.isRedexE =>
  (defs : Definitions) -> WhnfContext d n -> (0 sg : SQty) ->
  (e : Elim d n) -> (0 ne : No (isRedexE defs ctx sg e)) =>
  Eff Whnf (Term d n)

computeElimTypeNoLog defs ctx sg e =
  case e of
    F x u loc => do
      let Just def = lookup x defs
        | Nothing => throw $ NotInScope loc x
      pure $ def.typeWithAt ctx.dimLen ctx.termLen u

    B i _ =>
      pure (ctx.tctx !! i).type

    App f s loc =>
      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
        Pi {arg, res, _} => pure $ sub1 res $ Ann s arg loc
        ty               => throw $ ExpectedPi loc ctx.names ty

    CasePair {pair, ret, _} =>
      pure $ sub1 ret pair

    Fst pair loc =>
      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
        Sig {fst, _} => pure fst
        ty           => throw $ ExpectedSig loc ctx.names ty

    Snd pair loc =>
      case !(computeWhnfElimType0NoLog defs ctx sg pair {ne = noOr1 ne}) of
        Sig {snd, _} => pure $ sub1 snd $ Fst pair loc
        ty           => throw $ ExpectedSig loc ctx.names ty

    CaseEnum {tag, ret, _} =>
      pure $ sub1 ret tag

    CaseNat {nat, ret, _} =>
      pure $ sub1 ret nat

    CaseBox {box, ret, _} =>
      pure $ sub1 ret box

    DApp {fun = f, arg = p, loc} =>
      case !(computeWhnfElimType0NoLog defs ctx sg f {ne = noOr1 ne}) of
        Eq {ty, _} => pure $ dsub1 ty p
        t          => throw $ ExpectedEq loc ctx.names t

    Ann {ty, _} =>
      pure ty

    Coe {ty, q, _} =>
      pure $ dsub1 ty q

    Comp {ty, _} =>
      pure ty

    TypeCase {ret, _} =>
      pure ret

computeElimType defs ctx sg e {ne} = do
  let Val n = ctx.termLen
  say "whnf" 90 e.loc "computeElimType"
  say "whnf" 95 e.loc $ hsep ["ctx =", runPretty $ prettyWhnfContext ctx]
  say "whnf" 90 e.loc $
    hsep ["e =", runPretty $ prettyElim ctx.dnames ctx.tnames e]
  res <- computeElimTypeNoLog defs ctx sg e {ne}
  say "whnf" 91 e.loc $
    hsep ["⇝", runPretty $ prettyTerm ctx.dnames ctx.tnames res]
  pure res

computeWhnfElimType0 defs ctx sg e =
  computeElimType defs ctx sg e >>= whnf0 defs ctx SZero

computeWhnfElimType0NoLog defs ctx sg e {ne} =
  computeElimTypeNoLog defs ctx sg e {ne} >>= whnf0 defs ctx SZero