add CheckBuiltin
This commit is contained in:
parent
32b9fe124f
commit
dd697ba56e
6 changed files with 126 additions and 33 deletions
33
lib/Quox/CheckBuiltin.idr
Normal file
33
lib/Quox/CheckBuiltin.idr
Normal file
|
@ -0,0 +1,33 @@
|
|||
||| 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
|
|
@ -6,4 +6,5 @@ import public Quox.Syntax.Qty
|
|||
import public Quox.Syntax.Shift
|
||||
import public Quox.Syntax.Subst
|
||||
import public Quox.Syntax.Term
|
||||
import public Quox.Syntax.Builtin
|
||||
import public Quox.Var
|
||||
|
|
27
lib/Quox/Syntax/Builtin.idr
Normal file
27
lib/Quox/Syntax/Builtin.idr
Normal file
|
@ -0,0 +1,27 @@
|
|||
module Quox.Syntax.Builtin
|
||||
|
||||
import Derive.Prelude
|
||||
import Quox.PrettyValExtra
|
||||
import Quox.Pretty
|
||||
import Quox.Syntax.Term
|
||||
|
||||
|
||||
%default total
|
||||
%language ElabReflection
|
||||
|
||||
public export
|
||||
data Builtin
|
||||
= Main
|
||||
%runElab derive "Builtin" [Eq, Ord, Show, PrettyVal]
|
||||
|
||||
public export
|
||||
builtinDesc : Builtin -> String
|
||||
builtinDesc Main = "a function declared as #[main]"
|
||||
|
||||
public export
|
||||
builtinTypeDoc : {opts : LayoutOpts} -> Builtin -> Eff Pretty (Doc opts)
|
||||
builtinTypeDoc Main =
|
||||
prettyTerm [<] [<] $
|
||||
Pi One (IOState noLoc)
|
||||
(SN $ Sig (Enum (fromList [!(ifUnicode "𝑎" "a")]) noLoc)
|
||||
(SN (IOState noLoc)) noLoc) noLoc
|
|
@ -123,6 +123,10 @@ parameters (defs : Definitions)
|
|||
expectBOX : Term d n -> Eff fs (Qty, Term d n)
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
|
||||
|
||||
export covering %inline
|
||||
expectIOState : Term d n -> Eff fs ()
|
||||
expectIOState = expect ExpectedIOState `(IOState {}) `(())
|
||||
|
||||
|
||||
namespace EqContext
|
||||
parameters (ctx : EqContext n) (sg : SQty) (loc : Loc)
|
||||
|
@ -174,3 +178,7 @@ parameters (defs : Definitions)
|
|||
export covering %inline
|
||||
expectBOX : Term 0 n -> Eff fs (Qty, Term 0 n)
|
||||
expectBOX = expect ExpectedBOX `(BOX {qty, ty, _}) `((qty, ty))
|
||||
|
||||
export covering %inline
|
||||
expectIOState : Term 0 n -> Eff fs ()
|
||||
expectIOState = expect ExpectedIOState `(IOState {}) `(())
|
||||
|
|
|
@ -2,6 +2,7 @@ module Quox.Typing.Error
|
|||
|
||||
import Quox.Loc
|
||||
import Quox.Syntax
|
||||
import Quox.Syntax.Builtin
|
||||
import Quox.Typing.Context
|
||||
import Quox.Typing.EqMode
|
||||
import Quox.Pretty
|
||||
|
@ -70,6 +71,7 @@ data Error
|
|||
| ExpectedNAT Loc (NameContexts d n) (Term d n)
|
||||
| ExpectedSTRING Loc (NameContexts d n) (Term d n)
|
||||
| ExpectedBOX Loc (NameContexts d n) (Term d n)
|
||||
| ExpectedIOState Loc (NameContexts d n) (Term d n)
|
||||
| BadUniverse Loc Universe Universe
|
||||
| TagNotIn Loc TagVal (SortedSet TagVal)
|
||||
| BadCaseEnum Loc (SortedSet TagVal) (SortedSet TagVal)
|
||||
|
@ -86,6 +88,9 @@ data Error
|
|||
| NotType Loc (TyContext d n) (Term d n)
|
||||
| WrongType Loc (EqContext n) (Term 0 n) (Term 0 n)
|
||||
|
||||
| WrongBuiltinType Builtin Error
|
||||
| ExpectedSingleEnum Loc (NameContexts d n) (Term d n)
|
||||
|
||||
| MissingEnumArm Loc TagVal (List TagVal)
|
||||
|
||||
-- extra context
|
||||
|
@ -130,6 +135,7 @@ Located Error where
|
|||
(ExpectedNAT loc _ _).loc = loc
|
||||
(ExpectedSTRING loc _ _).loc = loc
|
||||
(ExpectedBOX loc _ _).loc = loc
|
||||
(ExpectedIOState loc _ _).loc = loc
|
||||
(BadUniverse loc _ _).loc = loc
|
||||
(TagNotIn loc _ _).loc = loc
|
||||
(BadCaseEnum loc _ _).loc = loc
|
||||
|
@ -142,6 +148,8 @@ Located Error where
|
|||
(NotInScope loc _).loc = loc
|
||||
(NotType loc _ _).loc = loc
|
||||
(WrongType loc _ _ _).loc = loc
|
||||
(WrongBuiltinType _ err).loc = err.loc
|
||||
(ExpectedSingleEnum loc _ _).loc = loc
|
||||
(MissingEnumArm loc _ _).loc = loc
|
||||
(WhileChecking _ _ _ _ err).loc = err.loc
|
||||
(WhileCheckingTy _ _ _ err).loc = err.loc
|
||||
|
@ -306,6 +314,10 @@ parameters {opts : LayoutOpts} (showContext : Bool)
|
|||
hangDSingle "expected a box type, but got"
|
||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
||||
|
||||
ExpectedIOState _ ctx s =>
|
||||
hangDSingle "expected IOState, but got"
|
||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
||||
|
||||
BadUniverse _ k l => pure $
|
||||
sep ["the universe level" <++> !(prettyUniverse k),
|
||||
"is not strictly less than" <++> !(prettyUniverse l)]
|
||||
|
@ -364,6 +376,16 @@ parameters {opts : LayoutOpts} (showContext : Bool)
|
|||
[hangDSingle "the term" !(prettyTerm [<] ctx.tnames s),
|
||||
hangDSingle "cannot have type" !(prettyTerm [<] ctx.tnames ty)]
|
||||
|
||||
WrongBuiltinType b err => pure $
|
||||
vappend
|
||||
(sep [sep ["when checking", text $ builtinDesc b],
|
||||
sep ["has type", !(builtinTypeDoc b)]])
|
||||
!(prettyErrorNoLoc err)
|
||||
|
||||
ExpectedSingleEnum _ ctx s =>
|
||||
hangDSingle "expected an enumeration type with one case, but got"
|
||||
!(prettyTerm ctx.dnames ctx.tnames s)
|
||||
|
||||
MissingEnumArm _ tag tags => pure $
|
||||
sep [hsep ["the tag", !(prettyTag tag), "is not contained in"],
|
||||
!(prettyTerm [<] [<] $ Enum (fromList tags) noLoc)]
|
||||
|
|
|
@ -26,6 +26,7 @@ modules =
|
|||
Quox.OPE,
|
||||
Quox.Pretty,
|
||||
Quox.Syntax,
|
||||
Quox.Syntax.Builtin,
|
||||
Quox.Syntax.Dim,
|
||||
Quox.Syntax.DimEq,
|
||||
Quox.Syntax.Qty,
|
||||
|
@ -54,6 +55,7 @@ modules =
|
|||
Quox.Typing.Error,
|
||||
Quox.Typing,
|
||||
Quox.Typechecker,
|
||||
Quox.CheckBuiltin,
|
||||
Quox.Parser.Lexer,
|
||||
Quox.Parser.Syntax,
|
||||
Quox.Parser.Parser,
|
||||
|
|
Loading…
Reference in a new issue