[ #4595 ] Add concrete syntax + proper pretty printing for Setωᵢ

src/full/Agda/Syntax/Scope/Monad.hs

@@ -41,7 +41,7 @@ import Agda.Syntax.Concrete.Definitions (DeclarationWarning(..)) -- TODO: move t
 import Agda.Syntax.Scope.Base as A
 
 import Agda.TypeChecking.Monad.Base
-import Agda.TypeChecking.Monad.Builtin ( HasBuiltins , getBuiltinName' , builtinSet , builtinProp )
+import Agda.TypeChecking.Monad.Builtin ( HasBuiltins , getBuiltinName' , builtinSet , builtinProp , builtinSetOmega )
 import Agda.TypeChecking.Monad.Debug
 import Agda.TypeChecking.Monad.State
 import Agda.TypeChecking.Monad.Trace
@@ -385,7 +385,8 @@ canHaveSuffixTest :: HasBuiltins m => m (A.QName -> Bool)
 canHaveSuffixTest = do
   builtinSet  <- getBuiltinName' builtinSet
   builtinProp <- getBuiltinName' builtinProp
-  return $ \x -> Just x == builtinSet || Just x == builtinProp
+  builtinSetOmega <- getBuiltinName' builtinSetOmega
+  return $ \x -> Just x `elem` [builtinSet, builtinProp, builtinSetOmega]
 
 -- | Look up a module in the scope.
 resolveModule :: C.QName -> ScopeM AbstractModule

src/full/Agda/Syntax/Translation/InternalToAbstract.hs

@@ -1327,12 +1327,8 @@ instance Reify Sort Expr where
         I.Prop a -> do
           a <- reify a
           return $ A.App defaultAppInfo_ (A.Def nameOfProp) (defaultNamedArg a)
-        I.Inf 0 -> do
-          I.Def inf [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSetOmega
-          return $ A.Def inf
-        I.Inf n -> do
-          infs <- freshName_ ("Setω+" ++ show n :: String) -- TODO: hack
-          return $ A.Var infs
+        I.Inf 0 -> return $ A.Def' nameOfSetOmega A.NoSuffix
+        I.Inf n -> return $ A.Def' nameOfSetOmega (A.Suffix n)
         I.SizeUniv  -> do
           I.Def sizeU [] <- fromMaybe __IMPOSSIBLE__ <$> getBuiltin' builtinSizeUniv
           return $ A.Def sizeU

src/full/Agda/TypeChecking/Rules/Application.hs

@@ -226,7 +226,7 @@ inferApplication exh hd args e = postponeInstanceConstraints $ do
     A.Proj o p | isAmbiguous p -> inferProjApp e o (unAmbQ p) args
     A.Def' x s | x == nameOfSet      -> inferSet e x s args
     A.Def' x s | x == nameOfProp     -> inferProp e x s args
-    A.Def  x   | x == nameOfSetOmega -> inferSetOmega e x args
+    A.Def' x s | x == nameOfSetOmega -> inferSetOmega e x s args
     _ -> do
       (f, t0) <- inferHead hd
       let r = getRange hd
@@ -457,7 +457,7 @@ checkHeadApplication cmp e t hd args = do
   case hd of
     A.Def' c s | c == nameOfSet      -> checkSet cmp e t c s args
     A.Def' c s | c == nameOfProp     -> checkProp cmp e t c s args
-    A.Def  c   | c == nameOfSetOmega -> checkSetOmega cmp e t c args
+    A.Def' c s | c == nameOfSetOmega -> checkSetOmega cmp e t c s args
 
     -- Type checking #. The # that the user can write will be a Def, but the
     -- sharp we generate in the body of the wrapper is a Con.
@@ -1189,16 +1189,20 @@ inferSetOrProp mkSort e q suffix args = case args of
   arg : _ -> typeError . GenericDocError =<< fsep
     [ prettyTCM q , "cannot be applied to more than one argument" ]
 
-checkSetOmega :: Comparison -> A.Expr -> Type -> QName -> [NamedArg A.Expr] -> TCM Term
-checkSetOmega cmp e t q args = do
-  (v, t0) <- inferSetOmega e q args
+checkSetOmega :: Comparison -> A.Expr -> Type -> QName -> Suffix -> [NamedArg A.Expr] -> TCM Term
+checkSetOmega cmp e t q s args = do
+  (v, t0) <- inferSetOmega e q s args
   coerce cmp v t0 t
 
-inferSetOmega :: A.Expr -> QName -> [NamedArg A.Expr] -> TCM (Term, Type)
-inferSetOmega e q args = case args of
-  [] -> return (Sort (Inf 0) , sort (Inf 1))
-  arg : _ -> typeError . GenericDocError =<< fsep
-      [ prettyTCM q , "cannot be applied to an argument" ]
+inferSetOmega :: A.Expr -> QName -> Suffix -> [NamedArg A.Expr] -> TCM (Term, Type)
+inferSetOmega e q suffix args = do
+  let n = case suffix of
+            NoSuffix -> 0
+            Suffix n -> n
+  case args of
+    [] -> return (Sort (Inf n) , sort (Inf $ 1 + n))
+    arg : _ -> typeError . GenericDocError =<< fsep
+        [ prettyTCM q , "cannot be applied to an argument" ]
 
 -----------------------------------------------------------------------------
 -- * Coinduction

src/full/Agda/TypeChecking/Rules/Term.hs

@@ -143,6 +143,11 @@ isType_ e = traceCall (IsType_ e) $ do
         NoSuffix -> return $ sort (mkProp 0)
         Suffix i -> return $ sort (mkProp i)
 
+    -- Setωᵢ
+    A.Def' x suffix | x == nameOfSetOmega -> case suffix of
+      NoSuffix -> return $ sort (Inf 0)
+      Suffix i -> return $ sort (Inf i)
+
     -- Set ℓ
     A.App i s arg
       | visible arg,