module Quox.Typing

import public Quox.Typing.Context as Typing
import public Quox.Typing.EqMode as Typing
import public Quox.Typing.Error as Typing

import public Quox.Syntax
import public Quox.Definition
import public Quox.Reduce

%default total


public export
CheckResult' : Type -> Nat -> Type
CheckResult' = QOutput

public export
CheckResult : DimEq d -> Type -> Nat -> Type
CheckResult eqs q n = IfConsistent eqs $ CheckResult' q n

public export
record InferResult' q d n where
  constructor InfRes
  type : Term q d n
  qout : QOutput q n

public export
InferResult : DimEq d -> TermLike
InferResult eqs q d n = IfConsistent eqs $ InferResult' q d n


export
lookupFree' : HasErr q m => Definitions' q g -> Name -> m (Definition' q g)
lookupFree' defs x =
  case lookup x defs of
    Just d  => pure d
    Nothing => throwError $ NotInScope x


public export
substCasePairRet : Term q d n -> ScopeTerm q d n -> Term q d (2 + n)
substCasePairRet dty retty =
  let arg = Pair (BVT 0) (BVT 1) :# (dty // fromNat 2) in
  retty.term // (arg ::: shift 2)


parameters {auto _ : HasErr q m} (defs : Definitions' q _)
  export covering %inline
  whnfT : {0 isRedex : RedexTest tm} -> Whnf tm isRedex WhnfError =>
          tm q d n -> m (NonRedex tm q d n defs)
  whnfT = either (throwError . WhnfError) pure . whnf defs

  parameters (ctx : Lazy (TyContext q d1 n)) (th : Lazy (DSubst d2 d1))
    export covering %inline
    expectTYPE_ : Term q d2 n -> m Universe
    expectTYPE_ s = case fst !(whnfT s) of
      TYPE l => pure l
      _      => throwError $ ExpectedTYPE ctx (s // th)

    export covering %inline
    expectPi_ : Term q d2 n -> m (q, Term q d2 n, ScopeTerm q d2 n)
    expectPi_ s = case fst !(whnfT s) of
      Pi {qty, arg, res, _} => pure (qty, arg, res)
      _                     => throwError $ ExpectedPi ctx (s // th)

    export covering %inline
    expectSig_ : Term q d2 n -> m (Term q d2 n, ScopeTerm q d2 n)
    expectSig_ s = case fst !(whnfT s) of
      Sig {fst, snd, _} => pure (fst, snd)
      _                 => throwError $ ExpectedSig ctx (s // th)

    export covering %inline
    expectEnum_ : Term q d2 n -> m (SortedSet TagVal)
    expectEnum_ s = case fst !(whnfT s) of
      Enum tags => pure tags
      _         => throwError $ ExpectedEnum ctx (s // th)

    export covering %inline
    expectEq_ : Term q d2 n -> m (DScopeTerm q d2 n, Term q d2 n, Term q d2 n)
    expectEq_ s = case fst !(whnfT s) of
      Eq {ty, l, r, _} => pure (ty, l, r)
      _                => throwError $ ExpectedEq ctx (s // th)


  -- [fixme] refactor this stuff

  parameters (ctx : TyContext q d n)
    export covering %inline
    expectTYPE : Term q d n -> m Universe
    expectTYPE = expectTYPE_ ctx id

    export covering %inline
    expectPi : Term q d n -> m (q, Term q d n, ScopeTerm q d n)
    expectPi = expectPi_ ctx id

    export covering %inline
    expectSig : Term q d n -> m (Term q d n, ScopeTerm q d n)
    expectSig = expectSig_ ctx id

    export covering %inline
    expectEnum : Term q d n -> m (SortedSet TagVal)
    expectEnum = expectEnum_ ctx id

    export covering %inline
    expectEq : Term q d n -> m (DScopeTerm q d n, Term q d n, Term q d n)
    expectEq = expectEq_ ctx id


  parameters (ctx : EqContext q n)
    export covering %inline
    expectTYPEE : Term q 0 n -> m Universe
    expectTYPEE t = expectTYPE_ (toTyContext ctx) (shift0 ctx.dimLen) t

    export covering %inline
    expectPiE : Term q 0 n -> m (q, Term q 0 n, ScopeTerm q 0 n)
    expectPiE t = expectPi_ (toTyContext ctx) (shift0 ctx.dimLen) t

    export covering %inline
    expectSigE : Term q 0 n -> m (Term q 0 n, ScopeTerm q 0 n)
    expectSigE t = expectSig_ (toTyContext ctx) (shift0 ctx.dimLen) t

    export covering %inline
    expectEnumE : Term q 0 n -> m (SortedSet TagVal)
    expectEnumE t = expectEnum_ (toTyContext ctx) (shift0 ctx.dimLen) t

    export covering %inline
    expectEqE : Term q 0 n -> m (DScopeTerm q 0 n, Term q 0 n, Term q 0 n)
    expectEqE t = expectEq_ (toTyContext ctx) (shift0 ctx.dimLen) t