add check for #[main] type

lib/Quox/CheckBuiltin.idr

@@ -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

lib/Quox/Parser/FromParser.idr

@@ -8,6 +8,7 @@ import Quox.Parser.Syntax
 import Quox.Parser.Parser
 import public Quox.Parser.LoadFile
 import Quox.Typechecker
+import Quox.CheckBuiltin
 
 import Data.List
 import Data.Maybe
@@ -333,6 +334,13 @@ liftTC tc = runEff tc $ with Union.(::)
    \g => send g,
    \g => send g]
 
+private
+liftWhnf : Eff Whnf a -> Eff FromParserPure a
+liftWhnf tc = runEff tc $ with Union.(::)
+  [handleExcept $ \e => throw $ WrapTypeError e,
+   \g => send g,
+   \g => send g]
+
 private
 addDef : Has DefsState fs => Name -> Definition -> Eff fs NDefinition
 addDef name def = do
@@ -344,7 +352,8 @@ export covering
 fromPDef : PDefinition -> Eff FromParserPure NDefinition
 fromPDef def = do
   name <- fromPBaseNameNS def.name
-  when !(getsAt DEFS $ isJust . lookup name) $ do
+  defs <- getAt DEFS
+  when (isJust $ lookup name defs) $ do
     throw $ AlreadyExists def.loc name
   gqty <- globalPQty def.qty
   let sqty = globalToSubj gqty
@@ -352,17 +361,19 @@ fromPDef def = do
     PConcrete ptype pterm => do
       type <- traverse fromPTerm ptype
       term <- fromPTerm pterm
-      case type of
+      type <- case type of
         Just type => do
           ignore $ liftTC $ do
             checkTypeC empty type Nothing
             checkC empty sqty term type
-          addDef name $ mkDef gqty type term def.scheme def.main def.loc
+          pure type
         Nothing => do
           let E elim = term
             | _ => throw $ AnnotationNeeded term.loc empty term
           res <- liftTC $ inferC empty sqty elim
-          addDef name $ mkDef gqty res.type term def.scheme def.main def.loc
+          pure res.type
+      when def.main $ liftWhnf $ expectMainType defs type
+      addDef name $ mkDef gqty type term def.scheme def.main def.loc
     PPostulate ptype => do
       type <- fromPTerm ptype
       addDef name $ mkPostulate gqty type def.scheme def.main def.loc

lib/Quox/Syntax.idr

@@ -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

lib/Quox/Syntax/Builtin.idr

@@ -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

lib/Quox/Typing.idr

@@ -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 {}) `(())

lib/Quox/Typing/Context.idr

@@ -21,10 +21,6 @@ record LocalVar d n where
   term : Maybe (Term d n) -- if from a `let`
 %runElab deriveIndexed "LocalVar" [Show]
 
-export
-CanShift (LocalVar d) where
-  l // by = {type $= (// by), term $= map (// by)} l
-
 namespace LocalVar
   export %inline
   letVar : (type, term : Term d n) -> LocalVar d n
@@ -34,15 +30,25 @@ namespace LocalVar
   lamVar : (type : Term d n) -> LocalVar d n
   lamVar type = MkLocal {type, term = Nothing}
 
-  subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
+  export %inline
-  subD th = {type $= (// th), term $= map (// th)}
+  mapVar : (Term d n -> Term d' n') -> LocalVar d n -> LocalVar d' n'
+  mapVar f = {type $= f, term $= map f}
 
+  export %inline
+  subD : DSubst d1 d2 -> LocalVar d1 n -> LocalVar d2 n
+  subD th = mapVar (// th)
+
+  export %inline
   weakD : LocalVar d n -> LocalVar (S d) n
   weakD = subD $ shift 1
 
+export %inline CanShift  (LocalVar d) where l // by = mapVar (// by) l
+export %inline CanDSubst LocalVar     where l // by = mapVar (// by) l
+export %inline CanTSubst LocalVar     where l // by = mapVar (// by) l
+
 public export
 TContext : TermLike
-TContext d = Context (\n => LocalVar d n)
+TContext d = Context (LocalVar d)
 
 public export
 QOutput : Nat -> Type
@@ -59,7 +65,7 @@ record TyContext d n where
   {auto dimLen  : Singleton d}
   {auto termLen : Singleton n}
   dctx   : DimEq d
-  dnames : BContext d
+  dnames : BContext d -- only used for printing
   tctx   : TContext d n
   tnames : BContext n -- only used for printing
   qtys   : QContext n -- only used for printing
@@ -122,8 +128,9 @@ CtxExtensionLet0 d = Telescope ((BindName,) . LocalVar d)
 namespace TyContext
   public export %inline
   empty : TyContext 0 0
-  empty =
+  empty = MkTyContext {
-    MkTyContext {dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]}
+    dctx = new, dnames = [<], tctx = [<], tnames = [<], qtys = [<]
+  }
 
   public export %inline
   null : TyContext d n -> Bool

lib/Quox/Typing/Error.idr

@@ -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
@@ -62,18 +63,19 @@ namespace WhnfContext
 
 public export
 data Error
-= ExpectedTYPE   Loc (NameContexts d n) (Term d n)
+= ExpectedTYPE    Loc (NameContexts d n) (Term d n)
-| ExpectedPi     Loc (NameContexts d n) (Term d n)
+| ExpectedPi      Loc (NameContexts d n) (Term d n)
-| ExpectedSig    Loc (NameContexts d n) (Term d n)
+| ExpectedSig     Loc (NameContexts d n) (Term d n)
-| ExpectedEnum   Loc (NameContexts d n) (Term d n)
+| ExpectedEnum    Loc (NameContexts d n) (Term d n)
-| ExpectedEq     Loc (NameContexts d n) (Term d n)
+| ExpectedEq      Loc (NameContexts d n) (Term d n)
-| ExpectedNAT    Loc (NameContexts d n) (Term d n)
+| ExpectedNAT     Loc (NameContexts d n) (Term d n)
-| ExpectedSTRING Loc (NameContexts d n) (Term d n)
+| ExpectedSTRING  Loc (NameContexts d n) (Term d n)
-| ExpectedBOX    Loc (NameContexts d n) (Term d n)
+| ExpectedBOX     Loc (NameContexts d n) (Term d n)
-| BadUniverse    Loc Universe Universe
+| ExpectedIOState Loc (NameContexts d n) (Term d n)
-| TagNotIn       Loc TagVal (SortedSet TagVal)
+| BadUniverse     Loc Universe Universe
-| BadCaseEnum    Loc (SortedSet TagVal) (SortedSet TagVal)
+| TagNotIn        Loc TagVal (SortedSet TagVal)
-| BadQtys        Loc String (TyContext d n) (List (QOutput n, Term d n))
+| BadCaseEnum     Loc (SortedSet TagVal) (SortedSet TagVal)
+| BadQtys         Loc String (TyContext d n) (List (QOutput n, Term d n))
 
 -- first term arg of ClashT is the type
 | ClashT  Loc (EqContext n) EqMode (Term 0 n) (Term 0 n) (Term 0 n)
@@ -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
@@ -122,27 +127,30 @@ ErrorEff = Except Error
 
 export
 Located Error where
-  (ExpectedTYPE    loc _ _).loc         = loc
+  (ExpectedTYPE     loc _ _).loc        = loc
-  (ExpectedPi      loc _ _).loc         = loc
+  (ExpectedPi       loc _ _).loc        = loc
-  (ExpectedSig     loc _ _).loc         = loc
+  (ExpectedSig      loc _ _).loc        = loc
-  (ExpectedEnum    loc _ _).loc         = loc
+  (ExpectedEnum     loc _ _).loc        = loc
-  (ExpectedEq      loc _ _).loc         = loc
+  (ExpectedEq       loc _ _).loc        = loc
-  (ExpectedNAT     loc _ _).loc         = loc
+  (ExpectedNAT      loc _ _).loc        = loc
-  (ExpectedSTRING  loc _ _).loc         = loc
+  (ExpectedSTRING   loc _ _).loc        = loc
-  (ExpectedBOX     loc _ _).loc         = loc
+  (ExpectedBOX      loc _ _).loc        = loc
-  (BadUniverse     loc _ _).loc         = loc
+  (ExpectedIOState  loc _ _).loc        = loc
-  (TagNotIn        loc _ _).loc         = loc
+  (BadUniverse      loc _ _).loc        = loc
-  (BadCaseEnum     loc _ _).loc         = loc
+  (TagNotIn         loc _ _).loc        = loc
-  (BadQtys         loc _ _ _).loc       = loc
+  (BadCaseEnum      loc _ _).loc        = loc
-  (ClashT          loc _ _ _ _ _).loc   = loc
+  (BadQtys          loc _ _ _).loc      = loc
-  (ClashTy         loc _ _ _ _).loc     = loc
+  (ClashT           loc _ _ _ _ _).loc  = loc
-  (ClashE          loc _ _ _ _).loc     = loc
+  (ClashTy          loc _ _ _ _).loc    = loc
-  (ClashU          loc _ _ _).loc       = loc
+  (ClashE           loc _ _ _ _).loc    = loc
-  (ClashQ          loc _ _).loc         = loc
+  (ClashU           loc _ _ _).loc      = loc
-  (NotInScope      loc _).loc           = loc
+  (ClashQ           loc _ _).loc        = loc
-  (NotType         loc _ _).loc         = loc
+  (NotInScope       loc _).loc          = loc
-  (WrongType       loc _ _ _).loc       = loc
+  (NotType          loc _ _).loc        = loc
-  (MissingEnumArm  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
   (WhileInferring  _ _ _ 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)]

lib/quox-lib.ipkg

@@ -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,