34 lines
1.1 KiB
Idris
34 lines
1.1 KiB
Idris
||| 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
|