||| check that special functions (e.g. `main`) have the expected type
module Quox.CheckBuiltin

import Quox.Syntax
import Quox.Typing
import Quox.Whnf

%default total


export covering
expectSingleEnum : Definitions -> TyContext d n -> SQty -> Loc ->
                   Term d n -> Eff Whnf ()
expectSingleEnum defs ctx sg loc s = do
  let err = delay $ ExpectedSingleEnum loc ctx.names s
  cases <- wrapErr (const err) $ expectEnum defs ctx sg loc s
  unless (length (SortedSet.toList cases) == 1) $ throw err

||| `main` should have a type `1.IOState → {𝑎} × IOState`,
||| for some (single) tag `𝑎`
export covering
expectMainType : Definitions -> Term 0 0 -> Eff Whnf ()
expectMainType defs ty =
  wrapErr (WrongBuiltinType Main) $ do
    let ctx = TyContext.empty
    (qty, arg, res) <- expectPi defs ctx SZero ty.loc ty
    expectEqualQ ty.loc qty One
    expectIOState defs ctx SZero arg.loc arg
    let ctx = extendTy qty res.name arg ctx
    (ret, st) <- expectSig defs ctx SZero res.loc res.term
    expectSingleEnum defs ctx SZero ret.loc ret
    let ctx = extendTy qty st.name ret ctx
    expectIOState defs ctx SZero st.loc st.term