[concrete] rename Expression/Pattern Sections into Atoms

src/MiniJuvix/Syntax/Concrete/Language.hs

@@ -1,4 +1,3 @@
-{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE UndecidableInstances #-}
 
 module MiniJuvix.Syntax.Concrete.Language
@@ -36,11 +35,11 @@ type family NameType (s :: Stage) :: (res :: GHC.Type) | res -> s where
   NameType 'Scoped = S.Name
 
 type family ExpressionType (s :: Stage) :: GHC.Type where
-  ExpressionType 'Parsed = (ExpressionSections 'Parsed)
+  ExpressionType 'Parsed = (ExpressionAtoms 'Parsed)
   ExpressionType 'Scoped = Expression
 
 type family PatternType (s :: Stage) :: GHC.Type where
-  PatternType 'Parsed = (PatternSection 'Parsed)
+  PatternType 'Parsed = (PatternAtom 'Parsed)
   PatternType 'Scoped = Pattern
 
 type family ImportType (s :: Stage) :: GHC.Type where
@@ -268,70 +267,70 @@ data Pattern
 -- Pattern section
 --------------------------------------------------------------------------------
 
-data PatternSection (s :: Stage)
-  = PatternSectionName (NameType s)
-  | PatternSectionWildcard
-  | PatternSectionEmpty
-  | PatternSectionParens (PatternSections s)
+data PatternAtom (s :: Stage)
+  = PatternAtomName (NameType s)
+  | PatternAtomWildcard
+  | PatternAtomEmpty
+  | PatternAtomParens (PatternAtoms s)
 
 deriving stock instance
   ( Show (ExpressionType s),
     Show (NameType s),
     Show (PatternType s)
   ) =>
-  Show (PatternSection s)
+  Show (PatternAtom s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
     Eq (NameType s),
     Eq (PatternType s)
   ) =>
-  Eq (PatternSection s)
+  Eq (PatternAtom s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
     Ord (NameType s),
     Ord (PatternType s)
   ) =>
-  Ord (PatternSection s)
+  Ord (PatternAtom s)
 
 deriving stock instance
   ( Lift (ExpressionType s),
     Lift (NameType s),
     Lift (PatternType s)
   ) =>
-  Lift (PatternSection s)
+  Lift (PatternAtom s)
 
-newtype PatternSections (s :: Stage)
-  = PatternSections (NonEmpty (PatternSection s))
+newtype PatternAtoms (s :: Stage)
+  = PatternAtoms (NonEmpty (PatternAtom s))
 
 deriving stock instance
   ( Show (ExpressionType s),
     Show (NameType s),
     Show (PatternType s)
   ) =>
-  Show (PatternSections s)
+  Show (PatternAtoms s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
     Eq (NameType s),
     Eq (PatternType s)
   ) =>
-  Eq (PatternSections s)
+  Eq (PatternAtoms s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
     Ord (NameType s),
     Ord (PatternType s)
   ) =>
-  Ord (PatternSections s)
+  Ord (PatternAtoms s)
 
 deriving stock instance
   ( Lift (ExpressionType s),
     Lift (NameType s),
     Lift (PatternType s)
   ) =>
-  Lift (PatternSections s)
+  Lift (PatternAtoms s)
 
 --------------------------------------------------------------------------------
 -- Function binding declaration
@@ -481,15 +480,15 @@ data Expression
 --------------------------------------------------------------------------------
 
 -- | Expressions without application
-data ExpressionSection (s :: Stage)
-  = SectionIdentifier (NameType s)
-  | SectionLambda (Lambda s)
-  | SectionLetBlock (LetBlock s)
-  | SectionUniverse Universe
-  | SectionFunction (Function s)
-  | SectionFunArrow
-  | SectionMatch (Match s)
-  | SectionParens (ExpressionSections s)
+data ExpressionAtom (s :: Stage)
+  = AtomIdentifier (NameType s)
+  | AtomLambda (Lambda s)
+  | AtomLetBlock (LetBlock s)
+  | AtomUniverse Universe
+  | AtomFunction (Function s)
+  | AtomFunArrow
+  | AtomMatch (Match s)
+  | AtomParens (ExpressionAtoms s)
 
 deriving stock instance
   ( Show (ExpressionType s),
@@ -497,7 +496,7 @@ deriving stock instance
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
-  Show (ExpressionSection s)
+  Show (ExpressionAtom s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
@@ -505,7 +504,7 @@ deriving stock instance
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
-  Eq (ExpressionSection s)
+  Eq (ExpressionAtom s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
@@ -513,7 +512,7 @@ deriving stock instance
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
-  Ord (ExpressionSection s)
+  Ord (ExpressionAtom s)
 
 deriving stock instance
   ( Lift (ExpressionType s),
@@ -521,11 +520,11 @@ deriving stock instance
     Lift (SymbolType s),
     Lift (PatternType s)
   ) =>
-  Lift (ExpressionSection s)
+  Lift (ExpressionAtom s)
 
 -- | Expressions without application
-newtype ExpressionSections (s :: Stage)
-  = ExpressionSections (NonEmpty (ExpressionSection s))
+newtype ExpressionAtoms (s :: Stage)
+  = ExpressionAtoms (NonEmpty (ExpressionAtom s))
 
 deriving stock instance
   ( Show (ExpressionType s),
@@ -533,7 +532,7 @@ deriving stock instance
     Show (SymbolType s),
     Show (PatternType s)
   ) =>
-  Show (ExpressionSections s)
+  Show (ExpressionAtoms s)
 
 deriving stock instance
   ( Eq (ExpressionType s),
@@ -541,7 +540,7 @@ deriving stock instance
     Eq (SymbolType s),
     Eq (PatternType s)
   ) =>
-  Eq (ExpressionSections s)
+  Eq (ExpressionAtoms s)
 
 deriving stock instance
   ( Ord (ExpressionType s),
@@ -549,7 +548,7 @@ deriving stock instance
     Ord (SymbolType s),
     Ord (PatternType s)
   ) =>
-  Ord (ExpressionSections s)
+  Ord (ExpressionAtoms s)
 
 deriving stock instance
   ( Lift (ExpressionType s),
@@ -557,7 +556,7 @@ deriving stock instance
     Lift (SymbolType s),
     Lift (PatternType s)
   ) =>
-  Lift (ExpressionSections s)
+  Lift (ExpressionAtoms s)
 
 --------------------------------------------------------------------------------
 -- Match expression
@@ -743,7 +742,7 @@ deriving stock instance
 -- Notes: An empty lambda, here called 'the impossible case', is a lambda
 -- expression with empty list of arguments and empty body.
 
-data Lambda (s :: Stage) = Lambda
+newtype Lambda (s :: Stage) = Lambda
   {lambdaClauses :: [LambdaClause s]}
 
 deriving stock instance

src/MiniJuvix/Syntax/Concrete/Parser.hs

@@ -128,20 +128,20 @@ import_ = do
 -- Expression
 --------------------------------------------------------------------------------
 
-expressionSection :: MonadParsec e Text m => m (ExpressionSection 'Parsed)
-expressionSection =
+expressionAtom :: MonadParsec e Text m => m (ExpressionAtom 'Parsed)
+expressionAtom =
   do
-    SectionIdentifier <$> name
-    <|> (SectionUniverse <$> universe)
-    <|> (SectionLambda <$> lambda)
-    <|> (SectionFunction <$> function)
-    <|> (SectionMatch <$> match)
-    <|> (SectionLetBlock <$> letBlock)
-    <|> (SectionFunArrow <$ kwRightArrow)
-    <|> parens (SectionParens <$> expressionSections)
+    AtomIdentifier <$> name
+    <|> (AtomUniverse <$> universe)
+    <|> (AtomLambda <$> lambda)
+    <|> (AtomFunction <$> function)
+    <|> (AtomMatch <$> match)
+    <|> (AtomLetBlock <$> letBlock)
+    <|> (AtomFunArrow <$ kwRightArrow)
+    <|> parens (AtomParens <$> expressionAtoms)
 
-expressionSections :: MonadParsec e Text m => m (ExpressionSections 'Parsed)
-expressionSections = ExpressionSections <$> P.some expressionSection
+expressionAtoms :: MonadParsec e Text m => m (ExpressionAtoms 'Parsed)
+expressionAtoms = ExpressionAtoms <$> P.some expressionAtom
 
 --------------------------------------------------------------------------------
 -- Match expression
@@ -149,15 +149,15 @@ expressionSections = ExpressionSections <$> P.some expressionSection
 
 matchAlt :: MonadParsec e Text m => m (MatchAlt 'Parsed)
 matchAlt = do
-  matchAltPattern <- patternSection
+  matchAltPattern <- patternAtom
   kwMapsTo
-  matchAltBody <- expressionSections
+  matchAltBody <- expressionAtoms
   return MatchAlt {..}
 
 match :: MonadParsec e Text m => m (Match 'Parsed)
 match = do
   kwMatch
-  matchExpression <- expressionSections
+  matchExpression <- expressionAtoms
   matchAlts <- braces (P.sepEndBy matchAlt kwSemicolon)
   return Match {..}
 
@@ -174,7 +174,7 @@ letBlock = do
   kwLet
   letClauses <- braces (P.sepEndBy letClause kwSemicolon)
   kwIn
-  letExpression <- expressionSections
+  letExpression <- expressionAtoms
   return LetBlock {..}
 
 --------------------------------------------------------------------------------
@@ -198,7 +198,7 @@ typeSignature ::
   m (TypeSignature 'Parsed)
 typeSignature sigName = do
   kwColon
-  sigType <- expressionSections
+  sigType <- expressionAtoms
   return TypeSignature {..}
 
 -------------------------------------------------------------------------------
@@ -224,7 +224,7 @@ axiomDef = do
   kwAxiom
   axiomName <- symbol
   kwColon
-  axiomType <- expressionSections
+  axiomType <- expressionAtoms
   return AxiomDef {..}
 
 --------------------------------------------------------------------------------
@@ -241,7 +241,7 @@ explicitFunParam = do
     n <- pName
     u <- pUsage
     return (n, u)
-  paramType <- expressionSections
+  paramType <- expressionAtoms
   rparen
   return $ FunctionParameter {..}
   where
@@ -263,7 +263,7 @@ function :: MonadParsec e Text m => m (Function 'Parsed)
 function = do
   funParameter <- functionParam
   kwRightArrow
-  funReturn <- expressionSections
+  funReturn <- expressionAtoms
   return Function {..}
 
 --------------------------------------------------------------------------------
@@ -289,9 +289,9 @@ whereClause =
 
 lambdaClause :: MonadParsec e Text m => m (LambdaClause 'Parsed)
 lambdaClause = do
-  lambdaParameters <- P.some patternSection
+  lambdaParameters <- P.some patternAtom
   kwMapsTo
-  lambdaBody <- expressionSections
+  lambdaBody <- expressionAtoms
   return LambdaClause {..}
 
 lambda :: MonadParsec e Text m => m (Lambda 'Parsed)
@@ -309,7 +309,7 @@ dataTypeDef = do
   kwInductive
   dataTypeName <- symbol
   dataTypeParameters <- P.many dataTypeParam
-  dataTypeType <- optional (kwColon >> expressionSections)
+  dataTypeType <- optional (kwColon >> expressionAtoms)
   dataTypeConstructors <- braces $ P.sepEndBy constructorDef kwSemicolon
   return DataTypeDef {..}
 
@@ -317,31 +317,31 @@ dataTypeParam :: MonadParsec e Text m => m (DataTypeParameter 'Parsed)
 dataTypeParam = parens $ do
   dataTypeParameterName <- symbol
   kwColon
-  dataTypeParameterType <- expressionSections
+  dataTypeParameterType <- expressionAtoms
   return DataTypeParameter {..}
 
 constructorDef :: MonadParsec e Text m => m (DataConstructorDef 'Parsed)
 constructorDef = do
   constructorName <- symbol
   kwColon
-  constructorType <- expressionSections
+  constructorType <- expressionAtoms
   return DataConstructorDef {..}
 
 --------------------------------------------------------------------------------
 -- Pattern section
 --------------------------------------------------------------------------------
 
-patternSection :: forall e m. MonadParsec e Text m => m (PatternSection 'Parsed)
-patternSection =
-  PatternSectionName <$> name
-    <|> PatternSectionWildcard <$ kwWildcard
-    <|> (PatternSectionParens <$> parens patternSections)
+patternAtom :: forall e m. MonadParsec e Text m => m (PatternAtom 'Parsed)
+patternAtom =
+  PatternAtomName <$> name
+    <|> PatternAtomWildcard <$ kwWildcard
+    <|> (PatternAtomParens <$> parens patternAtoms)
 
-patternSections ::
+patternAtoms ::
   forall e m.
   MonadParsec e Text m =>
-  m (PatternSections 'Parsed)
-patternSections = PatternSections <$> P.some patternSection
+  m (PatternAtoms 'Parsed)
+patternAtoms = PatternAtoms <$> P.some patternAtom
 
 --------------------------------------------------------------------------------
 -- Function binding declaration
@@ -353,9 +353,9 @@ functionClause ::
   Symbol ->
   m (FunctionClause 'Parsed)
 functionClause clauseOwnerFunction = do
-  clausePatterns <- P.many patternSection
+  clausePatterns <- P.many patternAtom
   kwAssignment
-  clauseBody <- expressionSections
+  clauseBody <- expressionAtoms
   clauseWhere <- optional whereBlock
   return FunctionClause {..}
 
@@ -399,9 +399,9 @@ openModule = do
 eval :: MonadParsec e Text m => m (Eval 'Parsed)
 eval = do
   kwEval
-  Eval <$> expressionSections
+  Eval <$> expressionAtoms
 
 printS :: MonadParsec e Text m => m (Print 'Parsed)
 printS = do
   kwPrint
-  Print <$> expressionSections
+  Print <$> expressionAtoms

src/MiniJuvix/Syntax/Concrete/Scoped/Scoper.hs

@@ -351,7 +351,7 @@ checkTypeSignature ::
   TypeSignature 'Parsed ->
   Sem r (TypeSignature 'Scoped)
 checkTypeSignature TypeSignature {..} = do
-  sigType' <- localScope (checkParseExpressionSections sigType)
+  sigType' <- localScope (checkParseExpressionAtoms sigType)
   sigName' <- bindFunctionSymbol sigName
   return
     TypeSignature
@@ -373,7 +373,7 @@ checkConstructorDef ::
   DataConstructorDef 'Parsed ->
   Sem r (DataConstructorDef 'Scoped)
 checkConstructorDef DataConstructorDef {..} = do
-  constructorType' <- checkParseExpressionSections constructorType
+  constructorType' <- checkParseExpressionAtoms constructorType
   constructorName' <- bindConstructorSymbol constructorName
   return
     DataConstructorDef
@@ -400,7 +400,7 @@ checkDataTypeDef DataTypeDef {..} = do
           case params of
             -- More params to check
             (DataTypeParameter {..} : ps) -> do
-              dataTypeParameterType' <- checkParseExpressionSections dataTypeParameterType
+              dataTypeParameterType' <- checkParseExpressionAtoms dataTypeParameterType
               dataTypeParameterName' <- freshVariable dataTypeParameterName
               let param' =
                     DataTypeParameter
@@ -411,7 +411,7 @@ checkDataTypeDef DataTypeDef {..} = do
                 go ps (dataTypeParameters' ++ [param'])
             -- All params have been checked
             [] -> do
-              dataTypeType' <- sequence (checkParseExpressionSections <$> dataTypeType)
+              dataTypeType' <- sequence (checkParseExpressionAtoms <$> dataTypeType)
               dataTypeName' <- bindInductiveSymbol dataTypeName
               dataTypeConstructors' <- mapM checkConstructorDef dataTypeConstructors
               return
@@ -534,11 +534,11 @@ checkFunctionClause ::
   Sem r (FunctionClause 'Scoped)
 checkFunctionClause FunctionClause {..} = do
   clauseOwnerFunction' <- checkSymbolInScope
-  clausePatterns' <- mapM checkParsePatternSection clausePatterns
+  clausePatterns' <- mapM checkParsePatternAtom clausePatterns
   (clauseWhere', clauseBody') <- localScope $
     withBindCurrentGroup $ do
       clw <- sequence (checkWhereBlock <$> clauseWhere)
-      clb <- checkParseExpressionSections clauseBody
+      clb <- checkParseExpressionAtoms clauseBody
       return (clw, clb)
   return
     FunctionClause
@@ -567,7 +567,7 @@ checkAxiom ::
   Sem r (AxiomDef 'Scoped)
 checkAxiom AxiomDef {..} = do
   axiomName' <- bindAxiomSymbol axiomName
-  axiomType' <- localScope $ checkParseExpressionSections axiomType
+  axiomType' <- localScope $ checkParseExpressionAtoms axiomType
   return
     AxiomDef
       { axiomName = axiomName',
@@ -581,13 +581,13 @@ checkEval ::
   Members '[Error ScopeError, State Scope, State ScopeState] r =>
   Eval 'Parsed ->
   Sem r (Eval 'Scoped)
-checkEval (Eval s) = Eval <$> localScope (checkParseExpressionSections s)
+checkEval (Eval s) = Eval <$> localScope (checkParseExpressionAtoms s)
 
 checkPrint ::
   Members '[Error ScopeError, State Scope, State ScopeState] r =>
   Print 'Parsed ->
   Sem r (Print 'Scoped)
-checkPrint (Print s) = Print <$> localScope (checkParseExpressionSections s)
+checkPrint (Print s) = Print <$> localScope (checkParseExpressionAtoms s)
 
 checkFunction ::
   forall r.
@@ -599,7 +599,7 @@ checkFunction Function {..} = do
   let scoped = case paramName funParameter' of
         Nothing -> id
         Just s -> withBindLocalVariable (LocalVariable s)
-  funReturn' <- scoped (checkParseExpressionSections funReturn)
+  funReturn' <- scoped (checkParseExpressionAtoms funReturn)
   return
     Function
       { funParameter = funParameter',
@@ -608,7 +608,7 @@ checkFunction Function {..} = do
   where
     checkParam :: Sem r (FunctionParameter 'Scoped)
     checkParam = do
-      paramType' <- checkParseExpressionSections paramType
+      paramType' <- checkParseExpressionAtoms paramType
       paramName' <- checkParamName
       return
         FunctionParameter
@@ -645,7 +645,7 @@ checkLetBlock ::
 checkLetBlock LetBlock {..} = do
   s <- get @Scope -- backup scope: we do not want local definitions to stay in scope
   letClauses' <- mapM checkLetClause letClauses
-  letExpression' <- checkParseExpressionSections letExpression
+  letExpression' <- checkParseExpressionAtoms letExpression
   put s -- restore scope
   return
     LetBlock
@@ -664,8 +664,8 @@ checkLambdaClause ::
   LambdaClause 'Parsed ->
   Sem r (LambdaClause 'Scoped)
 checkLambdaClause LambdaClause {..} = do
-  lambdaParameters' <- mapM checkParsePatternSection lambdaParameters
-  lambdaBody' <- withBindCurrentGroup (checkParseExpressionSections lambdaBody)
+  lambdaParameters' <- mapM checkParsePatternAtom lambdaParameters
+  lambdaBody' <- withBindCurrentGroup (checkParseExpressionAtoms lambdaBody)
   return
     LambdaClause
       { lambdaParameters = lambdaParameters',
@@ -785,21 +785,21 @@ checkPatternUnqualified s = do
     isConstructorKind :: S.NameKind -> Bool
     isConstructorKind = (== S.KNameConstructor)
 
-checkPatternSections ::
+checkPatternAtoms ::
   Members '[Error ScopeError, State Scope, State ScopeState] r =>
-  PatternSections 'Parsed ->
-  Sem r (PatternSections 'Scoped)
-checkPatternSections (PatternSections s) = PatternSections <$> mapM checkPatternSection s
+  PatternAtoms 'Parsed ->
+  Sem r (PatternAtoms 'Scoped)
+checkPatternAtoms (PatternAtoms s) = PatternAtoms <$> mapM checkPatternAtom s
 
-checkPatternSection ::
+checkPatternAtom ::
   Members '[Error ScopeError, State Scope, State ScopeState] r =>
-  PatternSection 'Parsed ->
-  Sem r (PatternSection 'Scoped)
-checkPatternSection p = case p of
-  PatternSectionWildcard -> return PatternSectionWildcard
-  PatternSectionEmpty -> return PatternSectionEmpty
-  PatternSectionParens e -> PatternSectionParens <$> checkPatternSections e
-  PatternSectionName n -> PatternSectionName <$> checkPatternName n
+  PatternAtom 'Parsed ->
+  Sem r (PatternAtom 'Scoped)
+checkPatternAtom p = case p of
+  PatternAtomWildcard -> return PatternAtomWildcard
+  PatternAtomEmpty -> return PatternAtomEmpty
+  PatternAtomParens e -> PatternAtomParens <$> checkPatternAtoms e
+  PatternAtomName n -> PatternAtomName <$> checkPatternName n
 
 checkName ::
   Members '[Error ScopeError, State Scope, Reader LocalVars] r =>
@@ -809,27 +809,27 @@ checkName n = case n of
   NameQualified q -> checkQualified q
   NameUnqualified s -> checkUnqualified s
 
-checkExpressionSection ::
+checkExpressionAtom ::
   Members '[Error ScopeError, State Scope, State ScopeState, Reader LocalVars] r =>
-  ExpressionSection 'Parsed ->
-  Sem r (ExpressionSection 'Scoped)
-checkExpressionSection e = case e of
-  SectionIdentifier n -> SectionIdentifier <$> checkName n
-  SectionLambda lam -> SectionLambda <$> checkLambda lam
-  SectionLetBlock letBlock -> SectionLetBlock <$> checkLetBlock letBlock
-  SectionUniverse uni -> return (SectionUniverse uni)
-  SectionFunction fun -> SectionFunction <$> checkFunction fun
-  SectionParens par -> SectionParens <$> checkExpressionSections par
-  SectionFunArrow -> return SectionFunArrow
-  SectionMatch match -> SectionMatch <$> checkMatch match
+  ExpressionAtom 'Parsed ->
+  Sem r (ExpressionAtom 'Scoped)
+checkExpressionAtom e = case e of
+  AtomIdentifier n -> AtomIdentifier <$> checkName n
+  AtomLambda lam -> AtomLambda <$> checkLambda lam
+  AtomLetBlock letBlock -> AtomLetBlock <$> checkLetBlock letBlock
+  AtomUniverse uni -> return (AtomUniverse uni)
+  AtomFunction fun -> AtomFunction <$> checkFunction fun
+  AtomParens par -> AtomParens <$> checkExpressionAtoms par
+  AtomFunArrow -> return AtomFunArrow
+  AtomMatch match -> AtomMatch <$> checkMatch match
 
 checkMatchAlt ::
   Members '[Error ScopeError, State Scope, Reader LocalVars, State ScopeState] r =>
   MatchAlt 'Parsed ->
   Sem r (MatchAlt 'Scoped)
 checkMatchAlt MatchAlt {..} = do
-  matchAltPattern' <- checkParsePatternSection matchAltPattern
-  matchAltBody' <- withBindCurrentGroup (checkParseExpressionSections matchAltBody)
+  matchAltPattern' <- checkParsePatternAtom matchAltPattern
+  matchAltBody' <- withBindCurrentGroup (checkParseExpressionAtoms matchAltBody)
   return
     MatchAlt
       { matchAltPattern = matchAltPattern',
@@ -841,7 +841,7 @@ checkMatch ::
   Match 'Parsed ->
   Sem r (Match 'Scoped)
 checkMatch Match {..} = do
-  matchExpression' <- checkParseExpressionSections matchExpression
+  matchExpression' <- checkParseExpressionAtoms matchExpression
   matchAlts' <- mapM checkMatchAlt matchAlts
   return
     Match
@@ -849,23 +849,23 @@ checkMatch Match {..} = do
         matchAlts = matchAlts'
       }
 
-checkExpressionSections ::
+checkExpressionAtoms ::
   Members '[Error ScopeError, State Scope, State ScopeState, Reader LocalVars] r =>
-  ExpressionSections 'Parsed ->
-  Sem r (ExpressionSections 'Scoped)
-checkExpressionSections (ExpressionSections l) = ExpressionSections <$> mapM checkExpressionSection l
+  ExpressionAtoms 'Parsed ->
+  Sem r (ExpressionAtoms 'Scoped)
+checkExpressionAtoms (ExpressionAtoms l) = ExpressionAtoms <$> mapM checkExpressionAtom l
 
-checkParseExpressionSections ::
+checkParseExpressionAtoms ::
   Members '[Error ScopeError, State Scope, State ScopeState, Reader LocalVars] r =>
-  ExpressionSections 'Parsed ->
+  ExpressionAtoms 'Parsed ->
   Sem r Expression
-checkParseExpressionSections = checkExpressionSections >=> parseExpressionSections
+checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
 
-checkParsePatternSection ::
+checkParsePatternAtom ::
   Members '[Error ScopeError, State Scope, State ScopeState] r =>
-  PatternSection 'Parsed ->
+  PatternAtom 'Parsed ->
   Sem r Pattern
-checkParsePatternSection = checkPatternSection >=> parsePatternSection
+checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
 checkStatement ::
   Members '[Error ScopeError, Reader ScopeParameters, Embed IO, State Scope, State ScopeState] r =>
@@ -934,9 +934,9 @@ makeExpressionTable = do
         parseSymbolId :: S.NameId -> Parse S.Name
         parseSymbolId uid = P.token getName mempty
           where
-            getName :: ExpressionSection 'Scoped -> Maybe S.Name
+            getName :: ExpressionAtom 'Scoped -> Maybe S.Name
             getName s = case s of
-              SectionIdentifier n'
+              AtomIdentifier n'
                 | uid == S._nameId n' -> Just n'
               _ -> Nothing
 
@@ -947,9 +947,9 @@ makeExpressionTable = do
         notFollowedByInfix :: Parse ()
         notFollowedByInfix = P.notFollowedBy (P.token infixName mempty)
           where
-            infixName :: ExpressionSection 'Scoped -> Maybe S.Name
+            infixName :: ExpressionAtom 'Scoped -> Maybe S.Name
             infixName s = case s of
-              SectionIdentifier n
+              AtomIdentifier n
                 | S.hasFixity n -> Just n
               _ -> Nothing
 
@@ -962,7 +962,7 @@ makeExpressionTable = do
               }
     -- Non-dependent function type: A → B
     functionOp :: P.Operator Parse Expression
-    functionOp = P.InfixR (nonDepFun <$ P.single SectionFunArrow)
+    functionOp = P.InfixR (nonDepFun <$ P.single AtomFunArrow)
       where
         nonDepFun :: Expression -> Expression -> Expression
         nonDepFun a b =
@@ -979,11 +979,11 @@ makeExpressionTable = do
                   paramType = a
                 }
 
-parseExpressionSections ::
+parseExpressionAtoms ::
   Members '[Error ScopeError, State Scope] r =>
-  ExpressionSections 'Scoped ->
+  ExpressionAtoms 'Scoped ->
   Sem r Expression
-parseExpressionSections (ExpressionSections sections) = do
+parseExpressionAtoms (ExpressionAtoms sections) = do
   tbl <- makeExpressionTable
   let parser :: Parse Expression
       parser = runM (mkExpressionParser tbl) <* P.eof
@@ -995,7 +995,7 @@ parseExpressionSections (ExpressionSections sections) = do
     filePath = "tmp"
 
 -- | Monad for parsing expression sections.
-type Parse = P.Parsec () [ExpressionSection 'Scoped]
+type Parse = P.Parsec () [ExpressionAtom 'Scoped]
 
 -- data Parser tok m a where
 --   EmbedParsec ::
@@ -1028,49 +1028,49 @@ parseTerm = do
     parseLambda :: Parse Expression
     parseLambda = ExpressionLambda <$> P.token lambda mempty
       where
-        lambda :: ExpressionSection 'Scoped -> Maybe (Lambda 'Scoped)
+        lambda :: ExpressionAtom 'Scoped -> Maybe (Lambda 'Scoped)
         lambda s = case s of
-          SectionLambda l -> Just l
+          AtomLambda l -> Just l
           _ -> Nothing
 
     parseMatch :: Parse Expression
     parseMatch = ExpressionMatch <$> P.token match mempty
       where
-        match :: ExpressionSection 'Scoped -> Maybe (Match 'Scoped)
+        match :: ExpressionAtom 'Scoped -> Maybe (Match 'Scoped)
         match s = case s of
-          SectionMatch l -> Just l
+          AtomMatch l -> Just l
           _ -> Nothing
 
     parseUniverse :: Parse Expression
     parseUniverse = ExpressionUniverse <$> P.token universe' mempty
       where
-        universe' :: ExpressionSection 'Scoped -> Maybe Universe
+        universe' :: ExpressionAtom 'Scoped -> Maybe Universe
         universe' s = case s of
-          SectionUniverse u -> Just u
+          AtomUniverse u -> Just u
           _ -> Nothing
 
     parseFunction :: Parse Expression
     parseFunction = ExpressionFunction <$> P.token function mempty
       where
-        function :: ExpressionSection 'Scoped -> Maybe (Function 'Scoped)
+        function :: ExpressionAtom 'Scoped -> Maybe (Function 'Scoped)
         function s = case s of
-          SectionFunction u -> Just u
+          AtomFunction u -> Just u
           _ -> Nothing
 
     parseLetBlock :: Parse Expression
     parseLetBlock = ExpressionLetBlock <$> P.token letBlock mempty
       where
-        letBlock :: ExpressionSection 'Scoped -> Maybe (LetBlock 'Scoped)
+        letBlock :: ExpressionAtom 'Scoped -> Maybe (LetBlock 'Scoped)
         letBlock s = case s of
-          SectionLetBlock u -> Just u
+          AtomLetBlock u -> Just u
           _ -> Nothing
 
     parseNoInfixIdentifier :: Parse Expression
     parseNoInfixIdentifier = ExpressionIdentifier <$> P.token identifierNoFixity mempty
       where
-        identifierNoFixity :: ExpressionSection 'Scoped -> Maybe S.Name
+        identifierNoFixity :: ExpressionAtom 'Scoped -> Maybe S.Name
         identifierNoFixity s = case s of
-          SectionIdentifier n
+          AtomIdentifier n
             | not (S.hasFixity n) -> Just n
           _ -> Nothing
 
@@ -1083,16 +1083,16 @@ parseTerm = do
       where
         strPath :: FilePath
         strPath = "inner parens"
-        parenExpr :: ExpressionSection 'Scoped -> Maybe [ExpressionSection 'Scoped]
+        parenExpr :: ExpressionAtom 'Scoped -> Maybe [ExpressionAtom 'Scoped]
         parenExpr s = case s of
-          SectionParens (ExpressionSections ss) -> Just (toList ss)
+          AtomParens (ExpressionAtoms ss) -> Just (toList ss)
           _ -> Nothing
 
 -------------------------------------------------------------------------------
 -- Infix Patterns
 -------------------------------------------------------------------------------
 
-type ParsePat = P.Parsec () [PatternSection 'Scoped]
+type ParsePat = P.Parsec () [PatternAtom 'Scoped]
 
 makePatternTable ::
   forall r.
@@ -1146,9 +1146,9 @@ makePatternTable = do
         parseSymbolId :: S.NameId -> ParsePat S.Name
         parseSymbolId uid = P.token getName mempty
           where
-            getName :: PatternSection 'Scoped -> Maybe S.Name
+            getName :: PatternAtom 'Scoped -> Maybe S.Name
             getName s = case s of
-              PatternSectionName n'
+              PatternAtomName n'
                 | uid == S._nameId n' -> Just n'
               _ -> Nothing
 
@@ -1159,9 +1159,9 @@ makePatternTable = do
         notFollowedByInfix :: ParsePat ()
         notFollowedByInfix = P.notFollowedBy (P.token infixName mempty)
           where
-            infixName :: PatternSection 'Scoped -> Maybe S.Name
+            infixName :: PatternAtom 'Scoped -> Maybe S.Name
             infixName s = case s of
-              PatternSectionName n
+              PatternAtomName n
                 | S.hasFixity n -> Just n
               _ -> Nothing
 
@@ -1183,34 +1183,34 @@ parsePrePatTerm = do
       PatternConstructor
         <$> P.token constructorNoFixity mempty
       where
-        constructorNoFixity :: PatternSection 'Scoped -> Maybe S.Name
+        constructorNoFixity :: PatternAtom 'Scoped -> Maybe S.Name
         constructorNoFixity s = case s of
-          PatternSectionName n
+          PatternAtomName n
             | not (S.hasFixity n) -> Just n
           _ -> Nothing
 
     parseWildcard :: ParsePat Pattern
     parseWildcard = PatternWildcard <$ P.satisfy isWildcard
       where
-        isWildcard :: PatternSection 'Scoped -> Bool
+        isWildcard :: PatternAtom 'Scoped -> Bool
         isWildcard s = case s of
-          PatternSectionWildcard -> True
+          PatternAtomWildcard -> True
           _ -> False
 
     parseEmpty :: ParsePat Pattern
     parseEmpty = PatternWildcard <$ P.satisfy isEmpty
       where
-        isEmpty :: PatternSection 'Scoped -> Bool
+        isEmpty :: PatternAtom 'Scoped -> Bool
         isEmpty s = case s of
-          PatternSectionEmpty -> True
+          PatternAtomEmpty -> True
           _ -> False
 
     parseVariable :: ParsePat Pattern
     parseVariable = PatternWildcard <$ P.token var mempty
       where
-        var :: PatternSection 'Scoped -> Maybe S.Symbol
+        var :: PatternAtom 'Scoped -> Maybe S.Symbol
         var s = case s of
-          PatternSectionName S.Name' {..}
+          PatternAtomName S.Name' {..}
             | NameUnqualified sym <- _nameConcrete,
               S.KNameLocal <- _nameKind ->
               Just
@@ -1229,9 +1229,9 @@ parsePrePatTerm = do
       where
         strPath :: FilePath
         strPath = "inner parens"
-        parenPat :: PatternSection 'Scoped -> Maybe [PatternSection 'Scoped]
+        parenPat :: PatternAtom 'Scoped -> Maybe [PatternAtom 'Scoped]
         parenPat s = case s of
-          PatternSectionParens (PatternSections ss) -> Just (toList ss)
+          PatternAtomParens (PatternAtoms ss) -> Just (toList ss)
           _ -> Nothing
 
 mkPatternParser ::
@@ -1249,9 +1249,9 @@ mkPatternParser table = embed @ParsePat pPattern
         parseTermRec :: Sem '[Embed ParsePat] Pattern
         parseTermRec = runReader pPattern parsePrePatTerm
 
-parsePatternSection ::
-  Members '[Error ScopeError, State Scope] r => PatternSection 'Scoped -> Sem r Pattern
-parsePatternSection sec = do
+parsePatternAtom ::
+  Members '[Error ScopeError, State Scope] r => PatternAtom 'Scoped -> Sem r Pattern
+parsePatternAtom sec = do
   tbl <- makePatternTable
   let parser :: ParsePat Pattern
       parser = runM (mkPatternParser tbl) <* P.eof