New syntax for function definitions (#2243)

- Closes #2060
- Closes #2189


- This pr adds support for the syntax described in #2189. It does not
drop support for the old syntax.

It is possible to automatically translate juvix files to the new syntax
by using the formatter with the `--new-function-syntax` flag. E.g.

```
juvix format --in-place --new-function-syntax
```
# Syntax changes
Type signatures follow this pattern:
```
f (a1 : Expr) .. (an : Expr) : Expr
```
where each `ai` is a non-empty list of symbols. Braces are used instead
of parentheses when the argument is implicit.

Then, we have these variants:
1. Simple body. After the signature we have `:= Expr;`.
2. Clauses. The function signature is followed by a non-empty sequence
of clauses. Each clause has the form:
```
| atomPat .. atomPat := Expr
```
# Mutual recursion
Now identifiers **do not need to be defined before they are used**,
making it possible to define mutually recursive functions/types without
any special syntax.
There are some exceptions to this. We cannot forward reference a symbol
`f` in some statement `s` if between `s` and the definition of `f` there
is one of the following statements:
1. Local module
2. Import statement
3. Open statement

I think it should be possible to drop the restriction for local modules
and import statements

Makefile

@@ -114,7 +114,7 @@ JUVIXFILESTOFORMAT=$(shell find  \
 	-type d \( -name ".juvix-build" -o -name "FancyPaths" \) -prune -o \
 	-type f -name "*.juvix" -print)
 
-JUVIXFORMATFLAGS?=--in-place
+JUVIXFORMATFLAGS?=--in-place --new-function-syntax
 JUVIXTYPECHECKFLAGS?=--only-errors
 
 .PHONY: format-juvix-files
@@ -124,12 +124,12 @@ format-juvix-files:
 		exit_code=$$?; \
 		if [ $$exit_code -eq 0 ]; then \
 			echo "[OK] $$file"; \
-      	elif [[ $$exit_code -ne 0 && "$$file" == *"tests/"* ]]; then \
+		elif [[ $$exit_code -ne 0 && "$$file" == *"tests/"* ]]; then \
 			echo "[CONTINUE] $$file is in tests directory."; \
-      	else \
- 			echo "[FAIL] $$file formatting failed" && exit 1; \
-      	fi; \
-      	done;
+		else \
+			echo "[FAIL] $$file formatting failed" && exit 1; \
+		fi; \
+		done;
 
 .PHONY: check-format-juvix-files
 check-format-juvix-files:
@@ -147,8 +147,8 @@ typecheck-juvix-examples:
 		if [ $$exit_code -eq 0 ]; then \
 			echo "[OK] $$file typechecks"; \
 		else \
- 			echo "[FAIL] Typecking failed for $$file" && exit 1; \
-      	fi; \
+			echo "[FAIL] Typecking failed for $$file" && exit 1; \
+		fi; \
 	done
 
 .PHONY: check-ormolu

app/Commands/Format.hs

@@ -33,7 +33,7 @@ targetFromOptions opts = do
   pkgDir <- askPkgDir
   case f of
     Just (Left p) -> return (TargetFile p)
-    Just (Right {}) -> return (TargetProject pkgDir)
+    Just Right {} -> return (TargetProject pkgDir)
     Nothing -> do
       isPackageGlobal <- askPackageGlobal
       if
@@ -49,8 +49,9 @@ targetFromOptions opts = do
 runCommand :: forall r. Members '[Embed IO, App, Resource, Files] r => FormatOptions -> Sem r ()
 runCommand opts = do
   target <- targetFromOptions opts
+  let newSyntax = NewSyntax (opts ^. formatNewSyntax)
   runOutputSem (renderFormattedOutput target opts) $ runScopeFileApp $ do
-    res <- case target of
+    res <- runReader newSyntax $ case target of
       TargetFile p -> format p
       TargetProject p -> formatProject p
       TargetStdin -> formatStdin
@@ -89,9 +90,9 @@ renderFormattedOutput target opts fInfo = do
     outputResult :: FormatRenderMode -> Sem r ()
     outputResult = \case
       EditInPlace i@FormattedFileInfo {..} ->
-        runTempFileIO $
-          restoreFileOnError _formattedFileInfoPath $
-            writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText)
+        runTempFileIO
+          . restoreFileOnError _formattedFileInfoPath
+          $ writeFile' _formattedFileInfoPath (i ^. formattedFileInfoContentsText)
       NoEdit m -> case m of
         ReformattedFile ts -> forM_ ts renderStdOut
         InputPath p -> say (pack (toFilePath p))

app/Commands/Format/Options.hs

@@ -5,6 +5,7 @@ import CommonOptions
 data FormatOptions = FormatOptions
   { _formatInput :: Maybe (Prepath FileOrDir),
     _formatCheck :: Bool,
+    _formatNewSyntax :: Bool,
     _formatInPlace :: Bool
   }
   deriving stock (Data)
@@ -28,6 +29,11 @@ parseFormat = do
       ( long "check"
           <> help "Do not print reformatted sources or unformatted file paths to standard output."
       )
+  _formatNewSyntax <-
+    switch
+      ( long "new-function-syntax"
+          <> help "Format the file using the new function syntax."
+      )
   _formatInPlace <-
     switch
       ( long "in-place"

app/Commands/Repl.hs

@@ -207,16 +207,16 @@ core input = do
   compileRes <- liftIO (compileReplInputIO' ctx (strip (pack input))) >>= replFromEither . snd
   whenJust compileRes (renderOutLn . Core.ppOut opts)
 
-ppConcrete :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl AnsiText
+ppConcrete :: Concrete.PrettyPrint a => a -> Repl AnsiText
 ppConcrete a = do
   gopts <- State.gets (^. replStateGlobalOptions)
   let popts :: GenericOptions = project' gopts
   return (Concrete.ppOut popts a)
 
-printConcrete :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl ()
+printConcrete :: Concrete.PrettyPrint a => a -> Repl ()
 printConcrete = ppConcrete >=> renderOut
 
-printConcreteLn :: (HasLoc a, Concrete.PrettyPrint a) => a -> Repl ()
+printConcreteLn :: Concrete.PrettyPrint a => a -> Repl ()
 printConcreteLn = ppConcrete >=> renderOutLn
 
 replParseIdentifiers :: String -> Repl (NonEmpty Concrete.ScopedIden)
@@ -252,11 +252,11 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
         printIdentifier :: Concrete.ScopedIden -> Repl ()
         printIdentifier s = do
           mdoc <- case s of
-            Concrete.ScopedAxiom a -> getDocAxiom (a ^. Concrete.axiomRefName . Scoped.nameId)
-            Concrete.ScopedInductive a -> getDocInductive (a ^. Concrete.inductiveRefName . Scoped.nameId)
+            Concrete.ScopedAxiom a -> getDocAxiom (a ^. Scoped.nameId)
+            Concrete.ScopedInductive a -> getDocInductive (a ^. Scoped.nameId)
             Concrete.ScopedVar {} -> return Nothing
-            Concrete.ScopedFunction f -> getDocFunction (f ^. Concrete.functionRefName . Scoped.nameId)
-            Concrete.ScopedConstructor c -> getDocConstructor (c ^. Concrete.constructorRefName . Scoped.nameId)
+            Concrete.ScopedFunction f -> getDocFunction (f ^. Scoped.nameId)
+            Concrete.ScopedConstructor c -> getDocConstructor (c ^. Scoped.nameId)
           printDoc mdoc
           where
             printDoc :: Maybe (Concrete.Judoc 'Concrete.Scoped) -> Repl ()
@@ -271,7 +271,7 @@ printDocumentation = replParseIdentifiers >=> printIdentifiers
             getDocFunction fun = do
               tbl :: Scoped.InfoTable <- getInfoTable
               let def :: Scoped.FunctionInfo = tbl ^?! Scoped.infoFunctions . at fun . _Just
-              return (def ^. Scoped.functionInfoType . Concrete.sigDoc)
+              return (def ^. Scoped.functionInfoDoc)
 
             getDocInductive :: Scoped.NameId -> Repl (Maybe (Concrete.Judoc 'Concrete.Scoped))
             getDocInductive ind = do
@@ -305,11 +305,11 @@ printDefinition = replParseIdentifiers >=> printIdentifiers
         printIdentifier :: Concrete.ScopedIden -> Repl ()
         printIdentifier s = do
           case s of
-            Concrete.ScopedAxiom a -> printAxiom (a ^. Concrete.axiomRefName . Scoped.nameId)
-            Concrete.ScopedInductive a -> printInductive (a ^. Concrete.inductiveRefName . Scoped.nameId)
+            Concrete.ScopedAxiom a -> printAxiom (a ^. Scoped.nameId)
+            Concrete.ScopedInductive a -> printInductive (a ^. Scoped.nameId)
             Concrete.ScopedVar {} -> return ()
-            Concrete.ScopedFunction f -> printFunction (f ^. Concrete.functionRefName . Scoped.nameId)
-            Concrete.ScopedConstructor c -> printConstructor (c ^. Concrete.constructorRefName . Scoped.nameId)
+            Concrete.ScopedFunction f -> printFunction (f ^. Scoped.nameId)
+            Concrete.ScopedConstructor c -> printConstructor (c ^. Scoped.nameId)
           where
             printLocation :: HasLoc s => s -> Repl ()
             printLocation def = do

juvix-stdlib

@@ -1 +1 @@
-Subproject commit 034c5236afb1c7b9dc0aa6754515001f5694cc7e
+Subproject commit 85751d3a7e5edd97a3d12dae197273731a2088cf

src/Juvix/Compiler/Concrete/Data/InfoTable.hs

@@ -4,12 +4,17 @@ import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude
 
-data FunctionInfo = FunctionInfo
-  { _functionInfoType :: TypeSignature 'Scoped,
-    _functionInfoClauses :: [FunctionClause 'Scoped]
+data OldFunctionInfo = OldFunctionInfo
+  { _oldFunctionInfoType :: TypeSignature 'Scoped,
+    _oldFunctionInfoClauses :: [FunctionClause 'Scoped]
   }
   deriving stock (Eq, Show)
 
+data FunctionInfo
+  = FunctionInfoOld OldFunctionInfo
+  | FunctionInfoNew (FunctionDef 'Scoped)
+  deriving stock (Eq, Show)
+
 data ConstructorInfo = ConstructorInfo
   { _constructorInfoDef :: InductiveConstructorDef 'Scoped,
     _constructorInfoTypeName :: S.Symbol
@@ -50,9 +55,25 @@ makeLenses ''InfoTable
 makeLenses ''InductiveInfo
 makeLenses ''ConstructorInfo
 makeLenses ''AxiomInfo
-makeLenses ''FunctionInfo
+makeLenses ''OldFunctionInfo
+
+_FunctionInfoOld :: Traversal' FunctionInfo OldFunctionInfo
+_FunctionInfoOld f = \case
+  FunctionInfoOld x -> FunctionInfoOld <$> f x
+  r@FunctionInfoNew {} -> pure r
+
+functionInfoDoc :: Lens' FunctionInfo (Maybe (Judoc 'Scoped))
+functionInfoDoc f = \case
+  FunctionInfoOld i -> do
+    i' <- traverseOf (oldFunctionInfoType . sigDoc) f i
+    pure (FunctionInfoOld i')
+  FunctionInfoNew i -> do
+    i' <- traverseOf signDoc f i
+    pure (FunctionInfoNew i')
 
 instance HasLoc FunctionInfo where
-  getLoc f =
-    getLoc (f ^. functionInfoType)
-      <>? (getLocSpan <$> nonEmpty (f ^. functionInfoClauses))
+  getLoc = \case
+    FunctionInfoOld f ->
+      getLoc (f ^. oldFunctionInfoType)
+        <>? (getLocSpan <$> nonEmpty (f ^. oldFunctionInfoClauses))
+    FunctionInfoNew f -> getLoc f

src/Juvix/Compiler/Concrete/Data/InfoTableBuilder.hs

@@ -13,6 +13,7 @@ data InfoTableBuilder m a where
   RegisterConstructor :: S.Symbol -> InductiveConstructorDef 'Scoped -> InfoTableBuilder m ()
   RegisterInductive :: InductiveDef 'Scoped -> InfoTableBuilder m ()
   RegisterTypeSignature :: TypeSignature 'Scoped -> InfoTableBuilder m ()
+  RegisterFunctionDef :: FunctionDef 'Scoped -> InfoTableBuilder m ()
   RegisterFunctionClause :: FunctionClause 'Scoped -> InfoTableBuilder m ()
   RegisterName :: (HasLoc c) => S.Name' c -> InfoTableBuilder m ()
   RegisterModule :: Module 'Scoped 'ModuleTop -> InfoTableBuilder m ()
@@ -45,13 +46,21 @@ toState = reinterpret $ \case
      in do
           modify (over infoInductives (HashMap.insert ref info))
           registerDoc (ity ^. inductiveName . nameId) j
+  RegisterFunctionDef f ->
+    let ref = f ^. signName . S.nameId
+        info = FunctionInfoNew f
+        j = f ^. signDoc
+     in do
+          modify (set (infoFunctions . at ref) (Just info))
+          registerDoc (f ^. signName . nameId) j
   RegisterTypeSignature f ->
     let ref = f ^. sigName . S.nameId
         info =
-          FunctionInfo
-            { _functionInfoType = f,
-              _functionInfoClauses = []
-            }
+          FunctionInfoOld
+            OldFunctionInfo
+              { _oldFunctionInfoType = f,
+                _oldFunctionInfoClauses = []
+              }
         j = f ^. sigDoc
      in do
           modify (set (infoFunctions . at ref) (Just info))
@@ -59,7 +68,7 @@ toState = reinterpret $ \case
   RegisterFunctionClause c ->
     -- assumes the signature has already been registered
     let key = c ^. clauseOwnerFunction . S.nameId
-     in modify (over (infoFunctions . at key . _Just . functionInfoClauses) (`snoc` c))
+     in modify (over (infoFunctions . at key . _Just . _FunctionInfoOld . oldFunctionInfoClauses) (`snoc` c))
   RegisterName n -> modify (over highlightNames (cons (S.AName n)))
   RegisterModule m -> do
     let j = m ^. moduleDoc

src/Juvix/Compiler/Concrete/Data/NameRef.hs

@@ -1,108 +1,9 @@
-{-# LANGUAGE UndecidableInstances #-}
-
 module Juvix.Compiler.Concrete.Data.NameRef where
 
 import Data.Kind qualified as GHC
-import Juvix.Compiler.Concrete.Data.Name qualified as C
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
-import Juvix.Prelude hiding (show)
-import Prelude (show)
 
 type RefNameType :: S.IsConcrete -> GHC.Type
 type family RefNameType c = res | res -> c where
   RefNameType 'S.Concrete = S.Name
   RefNameType 'S.NotConcrete = S.Name' ()
-
-type AxiomRef = AxiomRef' 'S.Concrete
-
-newtype AxiomRef' (n :: S.IsConcrete) = AxiomRef'
-  {_axiomRefName :: RefNameType n}
-
-makeLenses ''AxiomRef'
-
-instance HasLoc AxiomRef where
-  getLoc = getLoc . (^. axiomRefName)
-
-instance Hashable (RefNameType s) => Hashable (AxiomRef' s) where
-  hashWithSalt i = hashWithSalt i . (^. axiomRefName)
-
-instance (Eq (RefNameType s)) => Eq (AxiomRef' s) where
-  (==) = (==) `on` (^. axiomRefName)
-
-instance (Ord (RefNameType s)) => Ord (AxiomRef' s) where
-  compare = compare `on` (^. axiomRefName)
-
-instance (Show (RefNameType s)) => Show (AxiomRef' s) where
-  show = show . (^. axiomRefName)
-
-type InductiveRef = InductiveRef' 'S.Concrete
-
-newtype InductiveRef' (n :: S.IsConcrete) = InductiveRef'
-  { _inductiveRefName :: RefNameType n
-  }
-
-makeLenses ''InductiveRef'
-
-instance HasLoc InductiveRef where
-  getLoc = getLoc . (^. inductiveRefName)
-
-instance Hashable (RefNameType s) => Hashable (InductiveRef' s) where
-  hashWithSalt i = hashWithSalt i . (^. inductiveRefName)
-
-instance (Eq (RefNameType s)) => Eq (InductiveRef' s) where
-  (==) = (==) `on` (^. inductiveRefName)
-
-instance (Ord (RefNameType s)) => Ord (InductiveRef' s) where
-  compare = compare `on` (^. inductiveRefName)
-
-instance (Show (RefNameType s)) => Show (InductiveRef' s) where
-  show = show . (^. inductiveRefName)
-
-type FunctionRef = FunctionRef' 'S.Concrete
-
-newtype FunctionRef' (n :: S.IsConcrete) = FunctionRef'
-  { _functionRefName :: RefNameType n
-  }
-
-makeLenses ''FunctionRef'
-
-instance HasLoc FunctionRef where
-  getLoc = getLoc . (^. functionRefName)
-
-instance Hashable (RefNameType s) => Hashable (FunctionRef' s) where
-  hashWithSalt i = hashWithSalt i . (^. functionRefName)
-
-instance (Eq (RefNameType s)) => Eq (FunctionRef' s) where
-  (==) = (==) `on` (^. functionRefName)
-
-instance (Ord (RefNameType s)) => Ord (FunctionRef' s) where
-  compare = compare `on` (^. functionRefName)
-
-instance (Show (RefNameType s)) => Show (FunctionRef' s) where
-  show = show . (^. functionRefName)
-
-type ConstructorRef = ConstructorRef' 'S.Concrete
-
-newtype ConstructorRef' (n :: S.IsConcrete) = ConstructorRef'
-  { _constructorRefName :: RefNameType n
-  }
-
-makeLenses ''ConstructorRef'
-
-instance HasLoc ConstructorRef where
-  getLoc = getLoc . (^. constructorRefName)
-
-instance Hashable (RefNameType s) => Hashable (ConstructorRef' s) where
-  hashWithSalt i = hashWithSalt i . (^. constructorRefName)
-
-instance (Eq (RefNameType s)) => Eq (ConstructorRef' s) where
-  (==) = (==) `on` (^. constructorRefName)
-
-instance (Ord (RefNameType s)) => Ord (ConstructorRef' s) where
-  compare = compare `on` (^. constructorRefName)
-
-instance (Show (RefNameType s)) => Show (ConstructorRef' s) where
-  show = show . (^. constructorRefName)
-
-concreteFunctionRef :: C.Name -> FunctionRef' 'S.NotConcrete -> FunctionRef
-concreteFunctionRef s = over functionRefName (set S.nameConcrete s)

src/Juvix/Compiler/Concrete/Extra.hs

@@ -6,12 +6,14 @@ module Juvix.Compiler.Concrete.Extra
     unfoldApplication,
     groupStatements,
     flattenStatement,
+    migrateFunctionSyntax,
   )
 where
 
 import Data.HashMap.Strict qualified as HashMap
 import Data.List.NonEmpty qualified as NonEmpty
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
+import Juvix.Compiler.Concrete.Keywords
 import Juvix.Compiler.Concrete.Language
 import Juvix.Prelude hiding (some)
 import Juvix.Prelude.Parsing
@@ -98,6 +100,8 @@ groupStatements = \case
       (StatementModule {}, _) -> False
       (StatementAxiom {}, StatementAxiom {}) -> False
       (StatementAxiom {}, _) -> False
+      (StatementFunctionDef {}, _) -> False
+      (_, StatementFunctionDef {}) -> False
       (StatementTypeSignature sig, StatementFunctionClause fun) ->
         case sing :: SStage s of
           SParsed -> sig ^. sigName == fun ^. clauseOwnerFunction
@@ -134,3 +138,53 @@ flattenStatement :: Statement s -> [Statement s]
 flattenStatement = \case
   StatementModule m -> concatMap flattenStatement (m ^. moduleBody)
   s -> [s]
+
+migrateFunctionSyntax :: Module 'Scoped t -> Module 'Scoped t
+migrateFunctionSyntax m = over moduleBody (mapMaybe goStatement) m
+  where
+    goStatement :: Statement 'Scoped -> Maybe (Statement 'Scoped)
+    goStatement s = case s of
+      StatementSyntax {} -> Just s
+      StatementImport {} -> Just s
+      StatementAxiom {} -> Just s
+      StatementModule l -> Just (StatementModule (migrateFunctionSyntax l))
+      StatementInductive {} -> Just s
+      StatementOpenModule {} -> Just s
+      StatementFunctionDef {} -> Just s
+      StatementFunctionClause {} -> Nothing
+      StatementTypeSignature sig -> Just (StatementFunctionDef (mkFunctionDef sig (getClauses (sig ^. sigName))))
+
+    ss' :: [Statement 'Scoped]
+    ss' = m ^. moduleBody
+
+    mkFunctionDef :: TypeSignature 'Scoped -> [FunctionClause 'Scoped] -> FunctionDef 'Scoped
+    mkFunctionDef sig cls =
+      FunctionDef
+        { _signName = sig ^. sigName,
+          _signColonKw = sig ^. sigColonKw,
+          _signRetType = sig ^. sigType,
+          _signDoc = sig ^. sigDoc,
+          _signPragmas = sig ^. sigPragmas,
+          _signTerminating = sig ^. sigTerminating,
+          _signBuiltin = sig ^. sigBuiltin,
+          _signArgs = [],
+          _signBody = case sig ^. sigBody of
+            Just e -> SigBodyExpression e
+            Nothing -> case cls of
+              [] -> impossible
+              [c]
+                | null (c ^. clausePatterns) -> SigBodyExpression (c ^. clauseBody)
+                | otherwise -> SigBodyClauses (pure (mkClause c))
+              c : cs -> SigBodyClauses (mkClause <$> c :| cs)
+        }
+      where
+        mkClause :: FunctionClause 'Scoped -> NewFunctionClause 'Scoped
+        mkClause c =
+          NewFunctionClause
+            { _clausenPipeKw = Irrelevant (KeywordRef kwPipe (getLoc (c ^. clauseOwnerFunction)) Ascii),
+              _clausenAssignKw = c ^. clauseAssignKw,
+              _clausenBody = c ^. clauseBody,
+              _clausenPatterns = nonEmpty' (c ^. clausePatterns)
+            }
+    getClauses :: S.Symbol -> [FunctionClause 'Scoped]
+    getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]

src/Juvix/Compiler/Concrete/Language.hs

@@ -132,9 +132,41 @@ type ParsedIteratorAttribs = WithLoc (WithSource IteratorAttribs)
 -- Top level statement
 --------------------------------------------------------------------------------
 
+-- | We group consecutive definitions and reserve symbols in advance, so that we
+-- don't need extra syntax for mutually recursive definitions. Also, it allows
+-- us to be more flexible with the ordering of the definitions.
+data StatementSections (s :: Stage)
+  = SectionsDefinitions (DefinitionsSection s)
+  | SectionsNonDefinitions (NonDefinitionsSection s)
+  | SectionsEmpty
+
+data DefinitionsSection (s :: Stage) = DefinitionsSection
+  { _definitionsSection :: NonEmpty (Definition s),
+    _definitionsNext :: Maybe (NonDefinitionsSection s)
+  }
+
+data NonDefinitionsSection (s :: Stage) = NonDefinitionsSection
+  { _nonDefinitionsSection :: NonEmpty (NonDefinition s),
+    _nonDefinitionsNext :: Maybe (DefinitionsSection s)
+  }
+
+data Definition (s :: Stage)
+  = DefinitionSyntax SyntaxDef
+  | DefinitionFunctionDef (FunctionDef s)
+  | DefinitionInductive (InductiveDef s)
+  | DefinitionAxiom (AxiomDef s)
+  | DefinitionTypeSignature (TypeSignature s)
+
+data NonDefinition (s :: Stage)
+  = NonDefinitionImport (Import s)
+  | NonDefinitionModule (Module s 'ModuleLocal)
+  | NonDefinitionFunctionClause (FunctionClause s)
+  | NonDefinitionOpenModule (OpenModule s)
+
 data Statement (s :: Stage)
   = StatementSyntax SyntaxDef
   | StatementTypeSignature (TypeSignature s)
+  | StatementFunctionDef (FunctionDef s)
   | StatementImport (Import s)
   | StatementInductive (InductiveDef s)
   | StatementModule (Module s 'ModuleLocal)
@@ -242,6 +274,124 @@ instance HasLoc IteratorSyntaxDef where
 -- Type signature declaration
 -------------------------------------------------------------------------------
 
+data SigArg (s :: Stage) = SigArg
+  { _sigArgDelims :: Irrelevant (KeywordRef, KeywordRef),
+    _sigArgImplicit :: IsImplicit,
+    _sigArgColon :: Irrelevant KeywordRef,
+    _sigArgNames :: NonEmpty (SymbolType s),
+    _sigArgType :: ExpressionType s
+  }
+
+deriving stock instance (Show (ExpressionType s), Show (SymbolType s)) => Show (SigArg s)
+
+deriving stock instance (Eq (ExpressionType s), Eq (SymbolType s)) => Eq (SigArg s)
+
+deriving stock instance (Ord (ExpressionType s), Ord (SymbolType s)) => Ord (SigArg s)
+
+data NewFunctionClause (s :: Stage) = NewFunctionClause
+  { _clausenPipeKw :: Irrelevant KeywordRef,
+    _clausenPatterns :: NonEmpty (PatternAtomType s),
+    _clausenAssignKw :: Irrelevant KeywordRef,
+    _clausenBody :: ExpressionType s
+  }
+
+deriving stock instance
+  ( Show (PatternAtomType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
+    Show (SymbolType s),
+    Show (ExpressionType s)
+  ) =>
+  Show (NewFunctionClause s)
+
+deriving stock instance
+  ( Eq (PatternAtomType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
+    Eq (SymbolType s),
+    Eq (ExpressionType s)
+  ) =>
+  Eq (NewFunctionClause s)
+
+deriving stock instance
+  ( Ord (PatternAtomType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
+    Ord (SymbolType s),
+    Ord (ExpressionType s)
+  ) =>
+  Ord (NewFunctionClause s)
+
+data FunctionDefBody (s :: Stage)
+  = SigBodyExpression (ExpressionType s)
+  | SigBodyClauses (NonEmpty (NewFunctionClause s))
+
+deriving stock instance
+  ( Show (PatternAtomType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
+    Show (SymbolType s),
+    Show (ExpressionType s)
+  ) =>
+  Show (FunctionDefBody s)
+
+deriving stock instance
+  ( Eq (PatternAtomType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
+    Eq (SymbolType s),
+    Eq (ExpressionType s)
+  ) =>
+  Eq (FunctionDefBody s)
+
+deriving stock instance
+  ( Ord (PatternAtomType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
+    Ord (SymbolType s),
+    Ord (ExpressionType s)
+  ) =>
+  Ord (FunctionDefBody s)
+
+data FunctionDef (s :: Stage) = FunctionDef
+  { _signName :: FunctionName s,
+    _signArgs :: [SigArg s],
+    _signColonKw :: Irrelevant KeywordRef,
+    _signRetType :: ExpressionType s,
+    _signDoc :: Maybe (Judoc s),
+    _signPragmas :: Maybe ParsedPragmas,
+    _signBuiltin :: Maybe (WithLoc BuiltinFunction),
+    _signBody :: FunctionDefBody s,
+    _signTerminating :: Maybe KeywordRef
+  }
+
+deriving stock instance
+  ( Show (PatternAtomType s),
+    Show (IdentifierType s),
+    Show (ModuleRefType s),
+    Show (SymbolType s),
+    Show (ExpressionType s)
+  ) =>
+  Show (FunctionDef s)
+
+deriving stock instance
+  ( Eq (PatternAtomType s),
+    Eq (IdentifierType s),
+    Eq (ModuleRefType s),
+    Eq (SymbolType s),
+    Eq (ExpressionType s)
+  ) =>
+  Eq (FunctionDef s)
+
+deriving stock instance
+  ( Ord (PatternAtomType s),
+    Ord (IdentifierType s),
+    Ord (ModuleRefType s),
+    Ord (SymbolType s),
+    Ord (ExpressionType s)
+  ) =>
+  Ord (FunctionDef s)
+
 data TypeSignature (s :: Stage) = TypeSignature
   { _sigName :: FunctionName s,
     _sigColonKw :: Irrelevant KeywordRef,
@@ -345,22 +495,22 @@ data PatternApp = PatternApp
 
 data PatternInfixApp = PatternInfixApp
   { _patInfixLeft :: PatternArg,
-    _patInfixConstructor :: ConstructorRef,
+    _patInfixConstructor :: S.Name,
     _patInfixRight :: PatternArg
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternInfixApp where
-  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
+  getFixity (PatternInfixApp _ op _) = fromMaybe impossible (op ^. S.nameFixity)
 
 data PatternPostfixApp = PatternPostfixApp
   { _patPostfixParameter :: PatternArg,
-    _patPostfixConstructor :: ConstructorRef
+    _patPostfixConstructor :: S.Name
   }
   deriving stock (Show, Eq, Ord)
 
 instance HasFixity PatternPostfixApp where
-  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. constructorRefName . S.nameFixity)
+  getFixity (PatternPostfixApp _ op) = fromMaybe impossible (op ^. S.nameFixity)
 
 data PatternArg = PatternArg
   { _patternArgIsImplicit :: IsImplicit,
@@ -371,7 +521,7 @@ data PatternArg = PatternArg
 
 data Pattern
   = PatternVariable (SymbolType 'Scoped)
-  | PatternConstructor ConstructorRef
+  | PatternConstructor S.Name
   | PatternApplication PatternApp
   | PatternList (ListPattern 'Scoped)
   | PatternInfixApplication PatternInfixApp
@@ -400,7 +550,7 @@ instance HasAtomicity Pattern where
 
 data PatternScopedIden
   = PatternScopedVar S.Symbol
-  | PatternScopedConstructor ConstructorRef
+  | PatternScopedConstructor S.Name
   deriving stock (Show, Ord, Eq)
 
 data PatternBinding = PatternBinding
@@ -682,10 +832,10 @@ instance (Show (RefNameType s)) => Show (ModuleRef'' s t) where
   show ModuleRef'' {..} = show _moduleRefName
 
 data SymbolEntry
-  = EntryAxiom (AxiomRef' 'S.NotConcrete)
-  | EntryInductive (InductiveRef' 'S.NotConcrete)
-  | EntryFunction (FunctionRef' 'S.NotConcrete)
-  | EntryConstructor (ConstructorRef' 'S.NotConcrete)
+  = EntryAxiom (RefNameType 'S.NotConcrete)
+  | EntryInductive (RefNameType 'S.NotConcrete)
+  | EntryFunction (RefNameType 'S.NotConcrete)
+  | EntryConstructor (RefNameType 'S.NotConcrete)
   | EntryModule (ModuleRef' 'S.NotConcrete)
   | EntryVariable (S.Name' ())
   deriving stock (Show)
@@ -745,11 +895,11 @@ deriving stock instance
 type ScopedIden = ScopedIden' 'S.Concrete
 
 data ScopedIden' (n :: S.IsConcrete)
-  = ScopedAxiom (AxiomRef' n)
-  | ScopedInductive (InductiveRef' n)
+  = ScopedAxiom (RefNameType n)
+  | ScopedInductive (RefNameType n)
   | ScopedVar S.Symbol
-  | ScopedFunction (FunctionRef' n)
-  | ScopedConstructor (ConstructorRef' n)
+  | ScopedFunction (RefNameType n)
+  | ScopedConstructor (RefNameType n)
 
 deriving stock instance
   (Eq (RefNameType s)) => Eq (ScopedIden' s)
@@ -762,16 +912,16 @@ deriving stock instance
 
 identifierName :: forall n. (SingI n) => ScopedIden' n -> RefNameType n
 identifierName = \case
-  ScopedAxiom a -> a ^. axiomRefName
-  ScopedInductive i -> i ^. inductiveRefName
+  ScopedAxiom a -> a
+  ScopedInductive i -> i
   ScopedVar v ->
     ( case sing :: S.SIsConcrete n of
         S.SConcrete -> id
         S.SNotConcrete -> set S.nameConcrete ()
     )
       (unqualifiedSymbol v)
-  ScopedFunction f -> f ^. functionRefName
-  ScopedConstructor c -> c ^. constructorRefName
+  ScopedFunction f -> f
+  ScopedConstructor c -> c
 
 data Expression
   = ExpressionIdentifier ScopedIden
@@ -1273,6 +1423,7 @@ makeLenses ''IteratorSyntaxDef
 makeLenses ''InductiveConstructorDef
 makeLenses ''Module
 makeLenses ''TypeSignature
+makeLenses ''FunctionDef
 makeLenses ''AxiomDef
 makeLenses ''FunctionClause
 makeLenses ''InductiveParameters
@@ -1428,6 +1579,7 @@ instance HasLoc (Statement 'Scoped) where
   getLoc = \case
     StatementSyntax t -> getLoc t
     StatementTypeSignature t -> getLoc t
+    StatementFunctionDef t -> getLoc t
     StatementImport t -> getLoc t
     StatementInductive t -> getLoc t
     StatementModule t -> getLoc t
@@ -1531,13 +1683,38 @@ getLocExpressionType = case sing :: SStage s of
   SParsed -> getLoc
   SScoped -> getLoc
 
+instance HasLoc (SigArg s) where
+  getLoc SigArg {..} = getLoc l <> getLoc r
+    where
+      Irrelevant (l, r) = _sigArgDelims
+
+instance SingI s => HasLoc (NewFunctionClause s) where
+  getLoc NewFunctionClause {..} =
+    getLoc _clausenPipeKw
+      <> getLocExpressionType _clausenBody
+
+instance SingI s => HasLoc (FunctionDefBody s) where
+  getLoc = \case
+    SigBodyExpression e -> getLocExpressionType e
+    SigBodyClauses cl -> getLocSpan cl
+
+instance SingI s => HasLoc (FunctionDef s) where
+  getLoc FunctionDef {..} =
+    (getLoc <$> _signDoc)
+      ?<> (getLoc <$> _signPragmas)
+      ?<> (getLoc <$> _signBuiltin)
+      ?<> (getLoc <$> _signTerminating)
+      ?<> getLocSymbolType _signName
+      <> getLoc _signBody
+
 instance SingI s => HasLoc (TypeSignature s) where
   getLoc TypeSignature {..} =
     (getLoc <$> _sigDoc)
       ?<> (getLoc <$> _sigPragmas)
       ?<> (getLoc <$> _sigBuiltin)
       ?<> (getLoc <$> _sigTerminating)
-      ?<> (getLocExpressionType <$> _sigBody)
+      ?<> getLocSymbolType _sigName
+      <> (getLocExpressionType <$> _sigBody)
       ?<> getLocExpressionType _sigType
 
 instance HasLoc (Example s) where
@@ -1771,7 +1948,7 @@ instance IsApe PatternInfixApp ApeLeaf where
         { _infixFixity = getFixity i,
           _infixLeft = toApe l,
           _infixRight = toApe r,
-          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. constructorRefName . S.nameConcrete)),
+          _infixIsDelimiter = isDelimiterStr (prettyText (op ^. S.nameConcrete)),
           _infixOp = ApeLeafPattern (PatternConstructor op)
         }
 
@@ -1847,18 +2024,18 @@ instance HasAtomicity PatternArg where
 
 idenOverName :: (forall s. S.Name' s -> S.Name' s) -> ScopedIden -> ScopedIden
 idenOverName f = \case
-  ScopedAxiom a -> ScopedAxiom (over axiomRefName f a)
-  ScopedInductive i -> ScopedInductive (over inductiveRefName f i)
+  ScopedAxiom a -> ScopedAxiom (f a)
+  ScopedInductive i -> ScopedInductive (f i)
   ScopedVar v -> ScopedVar (f v)
-  ScopedFunction fun -> ScopedFunction (over functionRefName f fun)
-  ScopedConstructor c -> ScopedConstructor (over constructorRefName f c)
+  ScopedFunction fun -> ScopedFunction (f fun)
+  ScopedConstructor c -> ScopedConstructor (f c)
 
 entryPrism :: (S.Name' () -> S.Name' ()) -> SymbolEntry -> (S.Name' (), SymbolEntry)
 entryPrism f = \case
-  EntryAxiom a -> (a ^. axiomRefName, EntryAxiom (over axiomRefName f a))
-  EntryInductive i -> (i ^. inductiveRefName, EntryInductive (over inductiveRefName f i))
-  EntryFunction fun -> (fun ^. functionRefName, EntryFunction (over functionRefName f fun))
-  EntryConstructor c -> (c ^. constructorRefName, EntryConstructor (over constructorRefName f c))
+  EntryAxiom a -> (a, EntryAxiom (f a))
+  EntryInductive i -> (i, EntryInductive (f i))
+  EntryFunction fun -> (fun, EntryFunction (f fun))
+  EntryConstructor c -> (c, EntryConstructor (f c))
   EntryModule m -> (getModuleRefNameType m, EntryModule (overModuleRef'' (over moduleRefName f) m))
   EntryVariable m -> (m, EntryVariable (f m))
 
@@ -1904,10 +2081,10 @@ symbolEntryNameId = (^. S.nameId) . symbolEntryToSName
 
 symbolEntryToSName :: SymbolEntry -> S.Name' ()
 symbolEntryToSName = \case
-  EntryAxiom a -> a ^. axiomRefName
-  EntryInductive i -> i ^. inductiveRefName
-  EntryFunction f -> f ^. functionRefName
-  EntryConstructor c -> c ^. constructorRefName
+  EntryAxiom a -> a
+  EntryInductive i -> i
+  EntryFunction f -> f
+  EntryConstructor c -> c
   EntryModule m -> getModuleRefNameType m
   EntryVariable m -> m
 

src/Juvix/Compiler/Concrete/Pretty.hs

@@ -11,11 +11,11 @@ import Juvix.Compiler.Concrete.Print qualified as Print
 import Juvix.Data.PPOutput
 import Juvix.Prelude
 
-ppOutDefault :: (PrettyPrint c, HasLoc c) => c -> AnsiText
+ppOutDefault :: PrettyPrint c => c -> AnsiText
 ppOutDefault = Print.ppOutNoComments defaultOptions
 
-ppOut :: (HasLoc c, CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText
+ppOut :: (CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText
 ppOut = Print.ppOutNoComments
 
-ppTrace :: (HasLoc c, PrettyPrint c) => c -> Text
+ppTrace :: PrettyPrint c => c -> Text
 ppTrace = toAnsiText True . ppOut traceOptions

src/Juvix/Compiler/Concrete/Print.hs

@@ -17,5 +17,5 @@ ppOutDefault cs = mkAnsiText . PPOutput . doc defaultOptions cs
 ppOut :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> Comments -> c -> AnsiText
 ppOut o cs = mkAnsiText . PPOutput . doc (project o) cs
 
-ppOutNoComments :: (CanonicalProjection a Options, PrettyPrint c, HasLoc c) => a -> c -> AnsiText
-ppOutNoComments o = mkAnsiText . PPOutput . doc (project o) emptyComments
+ppOutNoComments :: (CanonicalProjection a Options, PrettyPrint c) => a -> c -> AnsiText
+ppOutNoComments o = mkAnsiText . PPOutput . docNoLoc (project o)

src/Juvix/Compiler/Concrete/Print/Base.hs

@@ -57,6 +57,9 @@ docHelper cs opts x =
     . ppCode
     $ x
 
+docNoLoc :: PrettyPrint c => Options -> c -> Doc Ann
+docNoLoc opts x = docHelper Nothing opts x
+
 doc :: (PrettyPrint c, HasLoc c) => Options -> Comments -> c -> Doc Ann
 doc opts cs x = docHelper (Just (fileComments file cs)) opts x
   where
@@ -113,8 +116,8 @@ ppExpressionType = case sing :: SStage s of
 
 ppPatternAtomType :: forall s. SingI s => PrettyPrinting (PatternAtomType s)
 ppPatternAtomType = case sing :: SStage s of
-  SParsed -> ppCode
-  SScoped -> ppCode
+  SParsed -> ppCodeAtom
+  SScoped -> ppCodeAtom
 
 ppPatternParensType :: forall s. SingI s => PrettyPrinting (PatternParensType s)
 ppPatternParensType = case sing :: SStage s of
@@ -190,12 +193,13 @@ instance SingI s => PrettyPrint (Iterator s) where
 instance PrettyPrint S.AName where
   ppCode (S.AName n) = annotated (AnnKind (S.getNameKind n)) (noLoc (pretty (n ^. S.nameVerbatim)))
 
--- TODO print without spaces when the type signature is not next to the clauses
 instance PrettyPrint FunctionInfo where
-  ppCode f = do
-    let ty = StatementTypeSignature (f ^. functionInfoType)
-        cs = map StatementFunctionClause (f ^. functionInfoClauses)
-    ppCode (ty : cs)
+  ppCode = \case
+    FunctionInfoOld f -> do
+      let ty = StatementTypeSignature (f ^. oldFunctionInfoType)
+          cs = map StatementFunctionClause (f ^. oldFunctionInfoClauses)
+      ppStatements (ty : cs)
+    FunctionInfoNew f -> ppCode f
 
 instance SingI s => PrettyPrint (List s) where
   ppCode List {..} = do
@@ -242,7 +246,7 @@ instance PrettyPrint S.NameId where
 instance (SingI t, SingI s) => PrettyPrint (Module s t) where
   ppCode :: forall r. (Members '[ExactPrint, Reader Options] r) => Module s t -> Sem r ()
   ppCode Module {..} = do
-    let moduleBody' = localIndent (ppCode _moduleBody)
+    let moduleBody' = localIndent (ppStatements _moduleBody)
         modulePath' = ppModulePathType _modulePath
         moduleDoc' = whenJust _moduleDoc ppCode
         modulePragmas' = whenJust _modulePragmas ppCode
@@ -276,12 +280,16 @@ instance (SingI t, SingI s) => PrettyPrint (Module s t) where
         SModuleLocal -> ppCode _moduleKwEnd
         SModuleTop -> end
 
-instance SingI s => PrettyPrint [Statement s] where
-  ppCode :: forall r. Members '[ExactPrint, Reader Options] r => [Statement s] -> Sem r ()
-  ppCode ss = paragraphs (ppGroup <$> Concrete.groupStatements ss)
-    where
-      ppGroup :: NonEmpty (Statement s) -> Sem r ()
-      ppGroup = vsep . sepEndSemicolon . fmap ppCode
+instance PrettyPrint a => PrettyPrint [a] where
+  ppCode x = do
+    let cs = map ppCode (toList x)
+    encloseSep (ppCode @Text "[") (ppCode @Text "]") (ppCode @Text ", ") cs
+
+ppStatements :: forall s r. (SingI s, Members '[ExactPrint, Reader Options] r) => [Statement s] -> Sem r ()
+ppStatements ss = paragraphs (ppGroup <$> Concrete.groupStatements ss)
+  where
+    ppGroup :: NonEmpty (Statement s) -> Sem r ()
+    ppGroup = vsep . sepEndSemicolon . fmap ppCode
 
 instance PrettyPrint TopModulePath where
   ppCode TopModulePath {..} =
@@ -310,18 +318,6 @@ instance PrettyPrint QualifiedName where
 instance PrettyPrint (ModuleRef'' 'S.Concrete 'ModuleTop) where
   ppCode m = ppCode (m ^. moduleRefName)
 
-instance PrettyPrint AxiomRef where
-  ppCode a = ppCode (a ^. axiomRefName)
-
-instance PrettyPrint InductiveRef where
-  ppCode a = ppCode (a ^. inductiveRefName)
-
-instance PrettyPrint FunctionRef where
-  ppCode a = ppCode (a ^. functionRefName)
-
-instance PrettyPrint ConstructorRef where
-  ppCode a = ppCode (a ^. constructorRefName)
-
 instance PrettyPrint ScopedIden where
   ppCode = \case
     ScopedAxiom a -> ppCode a
@@ -645,6 +641,45 @@ instance PrettyPrint BuiltinFunction where
 instance PrettyPrint BuiltinAxiom where
   ppCode i = ppCode Kw.kwBuiltin <+> keywordText (P.prettyText i)
 
+instance SingI s => PrettyPrint (NewFunctionClause s) where
+  ppCode :: forall r. Members '[ExactPrint, Reader Options] r => NewFunctionClause s -> Sem r ()
+  ppCode NewFunctionClause {..} = do
+    let pats' = hsep (ppPatternAtomType <$> _clausenPatterns)
+        e' = ppExpressionType _clausenBody
+    ppCode _clausenPipeKw <+> pats' <+> ppCode _clausenAssignKw <> oneLineOrNext e'
+
+instance SingI s => PrettyPrint (SigArg s) where
+  ppCode :: Members '[ExactPrint, Reader Options] r => SigArg s -> Sem r ()
+  ppCode SigArg {..} = do
+    let Irrelevant (l, r) = _sigArgDelims
+        names' = hsep (ppSymbolType <$> _sigArgNames)
+        colon' = ppCode _sigArgColon
+        ty' = ppExpressionType _sigArgType
+    ppCode l <> names' <+> colon' <+> ty' <> ppCode r
+
+instance SingI s => PrettyPrint (FunctionDef s) where
+  ppCode :: forall r. Members '[ExactPrint, Reader Options] r => FunctionDef s -> Sem r ()
+  ppCode FunctionDef {..} = do
+    let termin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _signTerminating
+        doc' :: Maybe (Sem r ()) = ppCode <$> _signDoc
+        pragmas' :: Maybe (Sem r ()) = ppCode <$> _signPragmas
+        args' = hsep . fmap ppCode <$> nonEmpty _signArgs
+        builtin' :: Maybe (Sem r ()) = (<> line) . ppCode <$> _signBuiltin
+        type' = oneLineOrNext (ppCode _signColonKw <+> ppExpressionType _signRetType)
+        name' = annDef _signName (ppSymbolType _signName)
+        body' = case _signBody of
+          SigBodyExpression e -> space <> ppCode Kw.kwAssign <> oneLineOrNext (ppExpressionType e)
+          SigBodyClauses k -> line <> indent (vsep (ppCode <$> k))
+    doc'
+      ?<> pragmas'
+      ?<> builtin'
+      ?<> termin'
+      ?<> ( name'
+              <+?> args'
+                <> type'
+                <> body'
+          )
+
 instance SingI s => PrettyPrint (TypeSignature s) where
   ppCode :: forall r. Members '[ExactPrint, Reader Options] r => TypeSignature s -> Sem r ()
   ppCode TypeSignature {..} = do
@@ -851,6 +886,7 @@ instance SingI s => PrettyPrint (Statement s) where
   ppCode = \case
     StatementSyntax s -> ppCode s
     StatementTypeSignature s -> ppCode s
+    StatementFunctionDef f -> ppCode f
     StatementImport i -> ppCode i
     StatementInductive i -> ppCode i
     StatementModule m -> ppCode m

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping.hs

@@ -18,6 +18,7 @@ import Juvix.Compiler.Concrete.Data.Scope
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Language
+import Juvix.Compiler.Concrete.Pretty (ppTrace)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Data.Context
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping.Error
 import Juvix.Compiler.Concrete.Translation.FromSource.Data.Context (ParserResult)
@@ -127,7 +128,7 @@ freshVariable = freshSymbol S.KNameLocal
 
 freshSymbol ::
   forall r.
-  (Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r) =>
+  Members '[State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators] r =>
   S.NameKind ->
   Symbol ->
   Sem r S.Symbol
@@ -165,13 +166,36 @@ freshSymbol _nameKind _nameConcrete = do
 
 reserveSymbolOf ::
   forall r.
-  (Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState] r) =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
   S.NameKind ->
   Symbol ->
   Sem r S.Symbol
 reserveSymbolOf k s = do
   checkNotBound
-  freshSymbol k s
+  s' <- freshSymbol k s
+  path <- gets (^. scopePath)
+  strat <- ask
+  modify (set (scopeLocalSymbols . at s) (Just s'))
+  let c = S.unConcrete s'
+      mentry :: Maybe SymbolEntry
+      mentry = case k of
+        S.KNameConstructor -> Just (EntryConstructor c)
+        S.KNameInductive -> Just (EntryInductive c)
+        S.KNameFunction -> Just (EntryFunction c)
+        S.KNameAxiom -> Just (EntryAxiom c)
+        S.KNameLocal -> Just (EntryVariable c)
+        S.KNameLocalModule -> Nothing
+        S.KNameTopModule -> Nothing
+      addS :: SymbolEntry -> Maybe SymbolInfo -> SymbolInfo
+      addS entry m = case m of
+        Nothing -> symbolInfoSingle entry
+        Just SymbolInfo {..} -> case strat of
+          BindingLocal -> symbolInfoSingle entry
+          BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo)
+  whenJust mentry $ \entry ->
+    modify (over scopeSymbols (HashMap.alter (Just . addS entry) s))
+
+  return s'
   where
     checkNotBound :: Sem r ()
     checkNotBound = do
@@ -185,12 +209,16 @@ reserveSymbolOf k s = do
                 }
           )
 
-bindReservedSymbol :: Members '[State Scope, InfoTableBuilder, Reader BindingStrategy] r => S.Symbol -> SymbolEntry -> Sem r ()
+bindReservedSymbol ::
+  Members '[State Scope, InfoTableBuilder, Reader BindingStrategy] r =>
+  S.Symbol ->
+  SymbolEntry ->
+  Sem r ()
 bindReservedSymbol s' entry = do
   path <- gets (^. scopePath)
   strat <- ask
+  -- TODO only modules are meant to be stored here?
   modify (over scopeSymbols (HashMap.alter (Just . addS strat path) s))
-  modify (set (scopeLocalSymbols . at s) (Just s'))
   registerName (S.unqualifiedSymbol s')
   where
     s :: Symbol
@@ -203,7 +231,7 @@ bindReservedSymbol s' entry = do
         BindingTop -> SymbolInfo (HashMap.insert path entry _symbolInfo)
 
 bindSymbolOf ::
-  (Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r) =>
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   S.NameKind ->
   (S.Name' () -> SymbolEntry) ->
   Symbol ->
@@ -213,42 +241,79 @@ bindSymbolOf k mkEntry s = do
   bindReservedSymbol s' (mkEntry (S.unConcrete s'))
   return s'
 
+bindReservedDefinitionSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
+  (S.Name' () -> SymbolEntry) ->
+  Symbol ->
+  Sem r S.Symbol
+bindReservedDefinitionSymbol mkEntry s = do
+  m <- gets (^. scopeLocalSymbols)
+  let s' = fromMaybe err (m ^. at s)
+      err = error ("impossible. Contents of scope:\n" <> ppTrace (toList m))
+  bindReservedSymbol s' (mkEntry (S.unConcrete s'))
+  return s'
+
 ignoreFixities :: Sem (State ScoperFixities ': r) a -> Sem r a
 ignoreFixities = evalState mempty
 
 ignoreIterators :: Sem (State ScoperIterators ': r) a -> Sem r a
 ignoreIterators = evalState mempty
 
--- variables are assumed to never be infix operators
+-- | variables are assumed to never be infix operators
 bindVariableSymbol ::
   Members '[Error ScoperError, NameIdGen, State Scope, InfoTableBuilder, State ScoperState] r =>
   Symbol ->
   Sem r S.Symbol
 bindVariableSymbol = localBindings . ignoreFixities . ignoreIterators . bindSymbolOf S.KNameLocal EntryVariable
 
+reserveInductiveSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Symbol ->
+  Sem r S.Symbol
+reserveInductiveSymbol = reserveSymbolOf S.KNameInductive
+
+reserveConstructorSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Symbol ->
+  Sem r S.Symbol
+reserveConstructorSymbol = reserveSymbolOf S.KNameConstructor
+
+reserveFunctionSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Symbol ->
+  Sem r S.Symbol
+reserveFunctionSymbol = reserveSymbolOf S.KNameFunction
+
+reserveAxiomSymbol ::
+  Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, State ScoperState, Reader BindingStrategy] r =>
+  Symbol ->
+  Sem r S.Symbol
+reserveAxiomSymbol = reserveSymbolOf S.KNameAxiom
+
+-- | symbols must be reserved in advance
 bindFunctionSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindFunctionSymbol = bindSymbolOf S.KNameFunction (EntryFunction . FunctionRef')
+bindFunctionSymbol = bindReservedDefinitionSymbol EntryFunction
 
 bindInductiveSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindInductiveSymbol = bindSymbolOf S.KNameInductive (EntryInductive . InductiveRef')
+bindInductiveSymbol = bindReservedDefinitionSymbol EntryInductive
 
 bindAxiomSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindAxiomSymbol = bindSymbolOf S.KNameAxiom (EntryAxiom . AxiomRef')
+bindAxiomSymbol = bindReservedDefinitionSymbol EntryAxiom
 
 bindConstructorSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
   Symbol ->
   Sem r S.Symbol
-bindConstructorSymbol = bindSymbolOf S.KNameConstructor (EntryConstructor . ConstructorRef')
+bindConstructorSymbol = bindReservedDefinitionSymbol EntryConstructor
 
 bindLocalModuleSymbol ::
   Members '[Error ScoperError, NameIdGen, State ScoperFixities, State ScoperIterators, State Scope, InfoTableBuilder, State ScoperState, Reader BindingStrategy] r =>
@@ -419,13 +484,13 @@ entryToScopedIden name e = do
       scopedName = set S.nameConcrete name (entryName e)
   registerName scopedName
   return $ case e of
-    EntryAxiom ref -> ScopedAxiom (set (axiomRefName . S.nameConcrete) name ref)
+    EntryAxiom ref -> ScopedAxiom (set S.nameConcrete name ref)
     EntryInductive ref ->
-      ScopedInductive (set (inductiveRefName . S.nameConcrete) name ref)
+      ScopedInductive (set S.nameConcrete name ref)
     EntryConstructor ref ->
-      ScopedConstructor (set (constructorRefName . S.nameConcrete) name ref)
+      ScopedConstructor (set S.nameConcrete name ref)
     EntryFunction ref ->
-      ScopedFunction (set (functionRefName . S.nameConcrete) name ref)
+      ScopedFunction (set S.nameConcrete name ref)
     EntryVariable v -> case name of
       NameQualified {} -> impossible
       NameUnqualified uname -> ScopedVar (set S.nameConcrete uname v)
@@ -514,8 +579,59 @@ checkIteratorSyntaxDef s@IteratorSyntaxDef {..} = do
 (@$>) :: Functor m => (a -> m ()) -> a -> m a
 (@$>) f a = f a $> a
 
+checkFunctionDef ::
+  forall r.
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r =>
+  FunctionDef 'Parsed ->
+  Sem r (FunctionDef 'Scoped)
+checkFunctionDef FunctionDef {..} = do
+  sigName' <- bindFunctionSymbol _signName
+  sigDoc' <- mapM checkJudoc _signDoc
+  (args', sigType', sigBody') <- withLocalScope $ do
+    a' <- mapM checkArg _signArgs
+    t' <- checkParseExpressionAtoms _signRetType
+    b' <- checkBody
+    return (a', t', b')
+  registerFunctionDef
+    @$> FunctionDef
+      { _signName = sigName',
+        _signRetType = sigType',
+        _signDoc = sigDoc',
+        _signBody = sigBody',
+        _signArgs = args',
+        ..
+      }
+  where
+    checkArg :: SigArg 'Parsed -> Sem r (SigArg 'Scoped)
+    checkArg SigArg {..} = do
+      names' <- mapM bindVariableSymbol _sigArgNames
+      ty' <- checkParseExpressionAtoms _sigArgType
+      return
+        SigArg
+          { _sigArgNames = names',
+            _sigArgType = ty',
+            ..
+          }
+    checkBody :: Sem r (FunctionDefBody 'Scoped)
+    checkBody = case _signBody of
+      SigBodyExpression e -> SigBodyExpression <$> checkParseExpressionAtoms e
+      SigBodyClauses cls -> SigBodyClauses <$> mapM checkClause cls
+    checkClause :: NewFunctionClause 'Parsed -> Sem r (NewFunctionClause 'Scoped)
+    checkClause NewFunctionClause {..} = do
+      (patterns', body') <- withLocalScope $ do
+        p <- mapM checkParsePatternAtom _clausenPatterns
+        b <- checkParseExpressionAtoms _clausenBody
+        return (p, b)
+      return
+        NewFunctionClause
+          { _clausenBody = body',
+            _clausenPatterns = patterns',
+            _clausenPipeKw,
+            _clausenAssignKw
+          }
+
 checkTypeSignature ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r =>
   TypeSignature 'Parsed ->
   Sem r (TypeSignature 'Scoped)
 checkTypeSignature TypeSignature {..} = do
@@ -534,7 +650,7 @@ checkTypeSignature TypeSignature {..} = do
 
 checkInductiveParameters ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   InductiveParameters 'Parsed ->
   Sem r (InductiveParameters 'Scoped)
 checkInductiveParameters params = do
@@ -544,16 +660,24 @@ checkInductiveParameters params = do
 
 checkInductiveDef ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators, Reader BindingStrategy] r =>
   InductiveDef 'Parsed ->
   Sem r (InductiveDef 'Scoped)
 checkInductiveDef InductiveDef {..} = do
-  inductiveName' <- topBindings (bindInductiveSymbol _inductiveName)
+  (inductiveName', constructorNames' :: NonEmpty S.Symbol) <- topBindings $ do
+    i <- bindInductiveSymbol _inductiveName
+    cs <- mapM (bindConstructorSymbol . (^. constructorName)) _inductiveConstructors
+    return (i, cs)
   (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors') <- withLocalScope $ do
     inductiveParameters' <- mapM checkInductiveParameters _inductiveParameters
     inductiveType' <- mapM checkParseExpressionAtoms _inductiveType
     inductiveDoc' <- mapM checkJudoc _inductiveDoc
-    inductiveConstructors' <- mapM (checkConstructorDef inductiveName') _inductiveConstructors
+    inductiveConstructors' <-
+      nonEmpty'
+        <$> sequence
+          [ checkConstructorDef inductiveName' cname cdef
+            | (cname, cdef) <- zipExact (toList constructorNames') (toList _inductiveConstructors)
+          ]
     return (inductiveParameters', inductiveType', inductiveDoc', inductiveConstructors')
   forM_ inductiveConstructors' bindConstructor
   registerInductive
@@ -576,15 +700,13 @@ checkInductiveDef InductiveDef {..} = do
         bindReservedSymbol
           (d ^. constructorName)
           ( EntryConstructor
-              ( ConstructorRef'
-                  (S.unConcrete (d ^. constructorName))
+              ( S.unConcrete (d ^. constructorName)
               )
           )
     -- note that the constructor name is not bound here
-    checkConstructorDef :: S.Symbol -> InductiveConstructorDef 'Parsed -> Sem r (InductiveConstructorDef 'Scoped)
-    checkConstructorDef tyName InductiveConstructorDef {..} = do
+    checkConstructorDef :: S.Symbol -> S.Symbol -> InductiveConstructorDef 'Parsed -> Sem r (InductiveConstructorDef 'Scoped)
+    checkConstructorDef tyName constructorName' InductiveConstructorDef {..} = do
       constructorType' <- checkParseExpressionAtoms _constructorType
-      constructorName' <- reserveSymbolOf S.KNameConstructor _constructorName
       doc' <- mapM checkJudoc _constructorDoc
       registerConstructor tyName
         @$> InductiveConstructorDef
@@ -601,10 +723,10 @@ createExportsTable ei = foldr (HashSet.insert . getNameId) HashSet.empty (HashMa
   where
     getNameId :: SymbolEntry -> NameId
     getNameId = \case
-      EntryAxiom r -> getNameRefId (r ^. axiomRefName)
-      EntryInductive r -> getNameRefId (r ^. inductiveRefName)
-      EntryFunction r -> getNameRefId (r ^. functionRefName)
-      EntryConstructor r -> getNameRefId (r ^. constructorRefName)
+      EntryAxiom r -> getNameRefId r
+      EntryInductive r -> getNameRefId r
+      EntryFunction r -> getNameRefId r
+      EntryConstructor r -> getNameRefId r
       EntryModule r -> getModuleRefNameId r
       EntryVariable v -> v ^. S.nameId
 
@@ -723,13 +845,180 @@ checkModuleBody ::
   [Statement 'Parsed] ->
   Sem r (ExportInfo, [Statement 'Scoped])
 checkModuleBody body = do
-  body' <- fixitiesBlock (iteratorsBlock (mapM checkStatement body))
+  body' <-
+    fmap flattenSections
+      . fixitiesBlock
+      . iteratorsBlock
+      $ checkSections (mkSections body)
   exported <- get >>= exportScope
   return (exported, body')
+  where
+    flattenSections :: forall s. StatementSections s -> [Statement s]
+    flattenSections s = run . execOutputList $ case s of
+      SectionsEmpty -> return ()
+      SectionsNonDefinitions n -> goNonDefinitions n
+      SectionsDefinitions n -> goDefinitions n
+      where
+        goNonDefinitions :: forall t. Members '[Output (Statement s)] t => NonDefinitionsSection s -> Sem t ()
+        goNonDefinitions NonDefinitionsSection {..} = do
+          mapM_ go _nonDefinitionsSection
+          whenJust _nonDefinitionsNext goDefinitions
+          where
+            go :: NonDefinition s -> Sem t ()
+            go = \case
+              NonDefinitionImport d -> output (StatementImport d)
+              NonDefinitionModule d -> output (StatementModule d)
+              NonDefinitionFunctionClause d -> output (StatementFunctionClause d)
+              NonDefinitionOpenModule d -> output (StatementOpenModule d)
+
+        goDefinitions :: forall t. Members '[Output (Statement s)] t => DefinitionsSection s -> Sem t ()
+        goDefinitions DefinitionsSection {..} = do
+          mapM_ go _definitionsSection
+          whenJust _definitionsNext goNonDefinitions
+          where
+            go :: Definition s -> Sem t ()
+            go = \case
+              DefinitionSyntax d -> output @(Statement s) (StatementSyntax d)
+              DefinitionAxiom d -> output (StatementAxiom d)
+              DefinitionFunctionDef d -> output @(Statement s) (StatementFunctionDef d)
+              DefinitionInductive d -> output @(Statement s) (StatementInductive d)
+              DefinitionTypeSignature d -> output @(Statement s) (StatementTypeSignature d)
+
+checkSections ::
+  forall r.
+  Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r =>
+  StatementSections 'Parsed ->
+  Sem r (StatementSections 'Scoped)
+checkSections sec = topBindings $ case sec of
+  SectionsEmpty -> return SectionsEmpty
+  SectionsDefinitions d -> SectionsDefinitions <$> goDefinitions d
+  SectionsNonDefinitions d -> SectionsNonDefinitions <$> goNonDefinitions d
+  where
+    goNonDefinitions :: NonDefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinitionsSection 'Scoped)
+    goNonDefinitions NonDefinitionsSection {..} = do
+      sec' <- mapM goNonDefinition _nonDefinitionsSection
+      next' <- mapM goDefinitions _nonDefinitionsNext
+      return
+        NonDefinitionsSection
+          { _nonDefinitionsNext = next',
+            _nonDefinitionsSection = sec'
+          }
+      where
+        goNonDefinition :: NonDefinition 'Parsed -> Sem (Reader BindingStrategy ': r) (NonDefinition 'Scoped)
+        goNonDefinition = \case
+          NonDefinitionModule m -> NonDefinitionModule <$> checkLocalModule m
+          NonDefinitionImport i -> NonDefinitionImport <$> checkImport i
+          NonDefinitionFunctionClause i -> NonDefinitionFunctionClause <$> checkFunctionClause i
+          NonDefinitionOpenModule i -> NonDefinitionOpenModule <$> checkOpenModule i
+
+    goDefinitions :: DefinitionsSection 'Parsed -> Sem (Reader BindingStrategy ': r) (DefinitionsSection 'Scoped)
+    goDefinitions DefinitionsSection {..} = do
+      mapM_ reserveDefinition _definitionsSection
+      sec' <- mapM goDefinition _definitionsSection
+      next' <- mapM goNonDefinitions _definitionsNext
+      return
+        DefinitionsSection
+          { _definitionsNext = next',
+            _definitionsSection = sec'
+          }
+      where
+        reserveDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) ()
+        reserveDefinition = \case
+          DefinitionSyntax s -> void (checkSyntaxDef s)
+          DefinitionFunctionDef d -> void (reserveFunctionSymbol (d ^. signName))
+          DefinitionTypeSignature d -> void (reserveFunctionSymbol (d ^. sigName))
+          DefinitionAxiom d -> void (reserveAxiomSymbol (d ^. axiomName))
+          DefinitionInductive d -> do
+            void (reserveInductiveSymbol (d ^. inductiveName))
+            mapM_ reserveConstructorSymbol (d ^.. inductiveConstructors . each . constructorName)
+        goDefinition :: Definition 'Parsed -> Sem (Reader BindingStrategy ': r) (Definition 'Scoped)
+        goDefinition = \case
+          DefinitionSyntax s -> return (DefinitionSyntax s)
+          DefinitionFunctionDef d -> DefinitionFunctionDef <$> checkFunctionDef d
+          DefinitionTypeSignature d -> DefinitionTypeSignature <$> checkTypeSignature d
+          DefinitionAxiom d -> DefinitionAxiom <$> checkAxiomDef d
+          DefinitionInductive d -> DefinitionInductive <$> checkInductiveDef d
+
+checkStatement ::
+  Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r =>
+  Statement 'Parsed ->
+  Sem r (Statement 'Scoped)
+checkStatement s = topBindings $ case s of
+  StatementSyntax synDef -> StatementSyntax <$> checkSyntaxDef synDef
+  StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig
+  StatementFunctionDef tySig -> StatementFunctionDef <$> checkFunctionDef tySig
+  StatementImport imp -> StatementImport <$> checkImport imp
+  StatementInductive dt -> StatementInductive <$> checkInductiveDef dt
+  StatementModule dt -> StatementModule <$> checkLocalModule dt
+  StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open
+  StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause
+  StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax
+
+mkLetSections :: [LetClause 'Parsed] -> StatementSections 'Parsed
+mkLetSections = mkSections . map fromLetClause
+  where
+    fromLetClause :: LetClause 'Parsed -> Statement 'Parsed
+    fromLetClause = \case
+      LetTypeSig t -> StatementTypeSignature t
+      LetFunClause c -> StatementFunctionClause c
+
+mkSections :: [Statement 'Parsed] -> StatementSections 'Parsed
+mkSections = \case
+  [] -> SectionsEmpty
+  h : hs -> case fromStatement h of
+    Left d -> SectionsDefinitions (goDefinitions (pure d) hs)
+    Right d -> SectionsNonDefinitions (goNonDefinitions (pure d) hs)
+  where
+    goDefinitions :: NonEmpty (Definition 'Parsed) -> [Statement 'Parsed] -> DefinitionsSection 'Parsed
+    goDefinitions acc = \case
+      s : ss -> case fromStatement s of
+        Left d -> goDefinitions (NonEmpty.cons d acc) ss
+        Right d ->
+          DefinitionsSection
+            { _definitionsSection = NonEmpty.reverse acc,
+              _definitionsNext = Just (goNonDefinitions (pure d) ss)
+            }
+      [] ->
+        DefinitionsSection
+          { _definitionsSection = NonEmpty.reverse acc,
+            _definitionsNext = Nothing
+          }
+    goNonDefinitions :: NonEmpty (NonDefinition 'Parsed) -> [Statement 'Parsed] -> NonDefinitionsSection 'Parsed
+    goNonDefinitions acc = \case
+      s : ss -> case fromStatement s of
+        Right d -> goNonDefinitions (NonEmpty.cons d acc) ss
+        Left d ->
+          NonDefinitionsSection
+            { _nonDefinitionsSection = NonEmpty.reverse acc,
+              _nonDefinitionsNext = Just (goDefinitions (pure d) ss)
+            }
+      [] ->
+        NonDefinitionsSection
+          { _nonDefinitionsSection = NonEmpty.reverse acc,
+            _nonDefinitionsNext = Nothing
+          }
+    fromStatement :: Statement 'Parsed -> Either (Definition 'Parsed) (NonDefinition 'Parsed)
+    fromStatement = \case
+      StatementAxiom a -> Left (DefinitionAxiom a)
+      StatementTypeSignature t -> Left (DefinitionTypeSignature t)
+      StatementFunctionDef n -> Left (DefinitionFunctionDef n)
+      StatementInductive i -> Left (DefinitionInductive i)
+      StatementSyntax s -> Left (DefinitionSyntax s)
+      StatementImport i -> Right (NonDefinitionImport i)
+      StatementModule m -> Right (NonDefinitionModule m)
+      StatementOpenModule o -> Right (NonDefinitionOpenModule o)
+      StatementFunctionClause c -> Right (NonDefinitionFunctionClause c)
+
+reserveLocalModuleSymbol ::
+  Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r =>
+  Symbol ->
+  Sem r S.Symbol
+reserveLocalModuleSymbol =
+  ignoreFixities . ignoreIterators . reserveSymbolOf S.KNameLocalModule
 
 checkLocalModule ::
   forall r.
-  (Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r) =>
+  Members '[Error ScoperError, State Scope, Reader ScopeParameters, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r =>
   Module 'Parsed 'ModuleLocal ->
   Sem r (Module 'Scoped 'ModuleLocal)
 checkLocalModule Module {..} = do
@@ -739,7 +1028,7 @@ checkLocalModule Module {..} = do
       (e, b) <- checkModuleBody _moduleBody
       doc' <- mapM checkJudoc _moduleDoc
       return (e, b, doc')
-  _modulePath' <- ignoreFixities (ignoreIterators (reserveSymbolOf S.KNameLocalModule _modulePath))
+  _modulePath' <- reserveLocalModuleSymbol _modulePath
   let moduleId = _modulePath' ^. S.nameId
       _moduleRefName = S.unConcrete _modulePath'
       _moduleRefModule =
@@ -997,7 +1286,7 @@ checkOpenModule op
 
 checkFunctionClause ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, Reader BindingStrategy] r =>
   FunctionClause 'Parsed ->
   Sem r (FunctionClause 'Scoped)
 checkFunctionClause clause@FunctionClause {..} = do
@@ -1027,7 +1316,7 @@ checkFunctionClause clause@FunctionClause {..} = do
         err = throw (ErrLacksTypeSig (LacksTypeSig clause))
 
 checkAxiomDef ::
-  (Members '[InfoTableBuilder, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r) =>
+  Members '[Reader ScopeParameters, InfoTableBuilder, Error ScoperError, State Scope, State ScoperState, NameIdGen, State ScoperFixities, State ScoperIterators, Reader BindingStrategy] r =>
   AxiomDef 'Parsed ->
   Sem r (AxiomDef 'Scoped)
 checkAxiomDef AxiomDef {..} = do
@@ -1041,7 +1330,7 @@ entryToSymbol sentry csym = set S.nameConcrete csym (symbolEntryToSName sentry)
 
 checkFunction ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Function 'Parsed ->
   Sem r (Function 'Scoped)
 checkFunction f = do
@@ -1058,14 +1347,47 @@ checkFunction f = do
         _funKw = f ^. funKw
     return Function {..}
 
--- for now functions defined in let clauses cannot be infix operators
-checkLetClause ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
-  LetClause 'Parsed ->
-  Sem r (LetClause 'Scoped)
-checkLetClause lc = localBindings . ignoreFixities . ignoreIterators $ case lc of
-  LetTypeSig t -> LetTypeSig <$> checkTypeSignature t
-  LetFunClause c -> LetFunClause <$> checkFunctionClause c
+-- | for now functions defined in let clauses cannot be infix operators
+checkLetClauses ::
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  NonEmpty (LetClause 'Parsed) ->
+  Sem r (NonEmpty (LetClause 'Scoped))
+checkLetClauses =
+  localBindings
+    . ignoreFixities
+    . ignoreIterators
+    . fmap fromSections
+    . checkSections
+    . mkLetSections
+    . toList
+  where
+    fromSections :: StatementSections s -> NonEmpty (LetClause s)
+    fromSections = \case
+      SectionsEmpty -> impossible
+      SectionsDefinitions d -> fromDefs d
+      SectionsNonDefinitions d -> fromNonDefs d
+      where
+        fromDefs :: DefinitionsSection s -> NonEmpty (LetClause s)
+        fromDefs DefinitionsSection {..} =
+          (fromDef <$> _definitionsSection) <>? (fromNonDefs <$> _definitionsNext)
+          where
+            fromDef :: Definition s -> LetClause s
+            fromDef = \case
+              DefinitionTypeSignature d -> LetTypeSig d
+              DefinitionFunctionDef {} -> impossible
+              DefinitionInductive {} -> impossible
+              DefinitionAxiom {} -> impossible
+              DefinitionSyntax {} -> impossible
+        fromNonDefs :: NonDefinitionsSection s -> NonEmpty (LetClause s)
+        fromNonDefs NonDefinitionsSection {..} =
+          (fromNonDef <$> _nonDefinitionsSection) <>? (fromDefs <$> _nonDefinitionsNext)
+          where
+            fromNonDef :: NonDefinition s -> LetClause s
+            fromNonDef = \case
+              NonDefinitionFunctionClause f -> LetFunClause f
+              NonDefinitionImport {} -> impossible
+              NonDefinitionModule {} -> impossible
+              NonDefinitionOpenModule {} -> impossible
 
 checkListPattern ::
   forall r.
@@ -1080,7 +1402,7 @@ checkListPattern l = do
 
 checkList ::
   forall r.
-  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   List 'Parsed ->
   Sem r (List 'Scoped)
 checkList l = do
@@ -1091,12 +1413,11 @@ checkList l = do
 
 checkLet ::
   forall r.
-  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Let 'Parsed ->
   Sem r (Let 'Scoped)
 checkLet Let {..} =
   withLocalScope $ do
-    -- local definitions should not stay in scope
     letClauses' <- checkLetClauses _letClauses
     letExpression' <- checkParseExpressionAtoms _letExpression
     return
@@ -1106,13 +1427,10 @@ checkLet Let {..} =
           _letKw,
           _letInKw
         }
-  where
-    checkLetClauses :: NonEmpty (LetClause 'Parsed) -> Sem r (NonEmpty (LetClause 'Scoped))
-    checkLetClauses = mapM checkLetClause
 
 checkCaseBranch ::
   forall r.
-  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   CaseBranch 'Parsed ->
   Sem r (CaseBranch 'Scoped)
 checkCaseBranch CaseBranch {..} = withLocalScope $ do
@@ -1133,7 +1451,7 @@ checkCaseBranch CaseBranch {..} = withLocalScope $ do
         (throw (ErrCaseBranchImplicitPattern (CaseBranchImplicitPattern p)))
 
 checkCase ::
-  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Case 'Parsed ->
   Sem r (Case 'Scoped)
 checkCase Case {..} = do
@@ -1148,7 +1466,7 @@ checkCase Case {..} = do
       }
 
 checkLambda ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Lambda 'Parsed ->
   Sem r (Lambda 'Scoped)
 checkLambda Lambda {..} = do
@@ -1161,7 +1479,7 @@ checkLambda Lambda {..} = do
       }
 
 checkLambdaClause ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   LambdaClause 'Parsed ->
   Sem r (LambdaClause 'Scoped)
 checkLambdaClause LambdaClause {..} = withLocalScope $ do
@@ -1187,13 +1505,13 @@ scopedVar s n = do
 
 scopedFunction ::
   (Members '[InfoTableBuilder] r) =>
-  FunctionRef' 'S.NotConcrete ->
+  RefNameType 'S.NotConcrete ->
   Symbol ->
-  Sem r FunctionRef
-scopedFunction (FunctionRef' fref) n = do
+  Sem r S.Name
+scopedFunction fref n = do
   let scoped :: S.Name = set S.nameConcrete (NameUnqualified n) fref
   registerName scoped
-  return (FunctionRef' scoped)
+  return scoped
 
 checkUnqualified ::
   (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder] r) =>
@@ -1239,14 +1557,14 @@ resolveShadowing es = go [(e, entryName e ^. S.nameWhyInScope) | e <- es]
 
 checkPatternName ::
   forall r.
-  (Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r) =>
+  Members '[Error ScoperError, State Scope, NameIdGen, State ScoperState, InfoTableBuilder] r =>
   Name ->
   Sem r PatternScopedIden
 checkPatternName n = do
   c <- getConstructorRef
   case c of
     Just constr -> do
-      registerName (constr ^. constructorRefName)
+      registerName constr
       return (PatternScopedConstructor constr) -- the symbol is a constructor
     Nothing -> PatternScopedVar <$> bindVariableSymbol sym -- the symbol is a variable
   where
@@ -1254,16 +1572,16 @@ checkPatternName n = do
       NameQualified (QualifiedName (SymbolPath p) s) -> (toList p, s)
       NameUnqualified s -> ([], s)
     -- check whether the symbol is a constructor in scope
-    getConstructorRef :: Sem r (Maybe ConstructorRef)
+    getConstructorRef :: Sem r (Maybe S.Name)
     getConstructorRef = do
       entries <- mapMaybe getConstructor <$> lookupQualifiedSymbol (path, sym)
       case entries of
         [] -> case SymbolPath <$> nonEmpty path of
           Nothing -> return Nothing -- There is no constructor with such a name
           Just pth -> throw (ErrQualSymNotInScope (QualSymNotInScope (QualifiedName pth sym)))
-        [e] -> return (Just (set (constructorRefName . S.nameConcrete) n e)) -- There is one constructor with such a name
+        [e] -> return (Just (set S.nameConcrete n e)) -- There is one constructor with such a name
         es -> throw (ErrAmbiguousSym (AmbiguousSym n (map EntryConstructor es)))
-    getConstructor :: SymbolEntry -> Maybe (ConstructorRef' 'S.NotConcrete)
+    getConstructor :: SymbolEntry -> Maybe (RefNameType 'S.NotConcrete)
     getConstructor = \case
       EntryConstructor r -> Just r
       _ -> Nothing
@@ -1313,7 +1631,7 @@ checkName n = case n of
   NameUnqualified s -> checkUnqualified s
 
 checkExpressionAtom ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtom 'Parsed ->
   Sem r (ExpressionAtom 'Scoped)
 checkExpressionAtom e = case e of
@@ -1332,7 +1650,7 @@ checkExpressionAtom e = case e of
   AtomIterator i -> AtomIterator <$> checkIterator i
 
 checkIterator ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Iterator 'Parsed ->
   Sem r (Iterator 'Scoped)
 checkIterator iter = do
@@ -1375,7 +1693,7 @@ checkIterator iter = do
     return Iterator {..}
 
 checkInitializer ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Initializer 'Parsed ->
   Sem r (Initializer 'Scoped)
 checkInitializer ini = do
@@ -1388,7 +1706,7 @@ checkInitializer ini = do
       }
 
 checkRange ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Range 'Parsed ->
   Sem r (Range 'Scoped)
 checkRange rng = do
@@ -1413,7 +1731,7 @@ checkHole h = do
       }
 
 checkParens ::
-  Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtoms 'Parsed ->
   Sem r Expression
 checkParens e@(ExpressionAtoms as _) = case as of
@@ -1427,19 +1745,19 @@ checkParens e@(ExpressionAtoms as _) = case as of
 
 checkExpressionAtoms ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtoms 'Parsed ->
   Sem r (ExpressionAtoms 'Scoped)
 checkExpressionAtoms (ExpressionAtoms l i) = (`ExpressionAtoms` i) <$> mapM checkExpressionAtom l
 
 checkJudoc ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   Judoc 'Parsed ->
   Sem r (Judoc 'Scoped)
 checkJudoc (Judoc groups) = Judoc <$> mapM checkJudocGroup groups
 
 checkJudocGroup ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   JudocGroup 'Parsed ->
   Sem r (JudocGroup 'Scoped)
 checkJudocGroup = \case
@@ -1447,7 +1765,7 @@ checkJudocGroup = \case
   JudocGroupLines l -> JudocGroupLines <$> mapM checkJudocBlock l
 
 checkJudocBlock ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   JudocBlock 'Parsed ->
   Sem r (JudocBlock 'Scoped)
 checkJudocBlock = \case
@@ -1455,19 +1773,19 @@ checkJudocBlock = \case
   JudocExample e -> JudocExample <$> traverseOf exampleExpression checkParseExpressionAtoms e
 
 checkJudocBlockParagraph ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   JudocBlockParagraph 'Parsed ->
   Sem r (JudocBlockParagraph 'Scoped)
 checkJudocBlockParagraph = traverseOf judocBlockParagraphBlocks (mapM checkJudocBlock)
 
 checkJudocLine ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   JudocLine 'Parsed ->
   Sem r (JudocLine 'Scoped)
 checkJudocLine (JudocLine delim atoms) = JudocLine delim <$> mapM (mapM checkJudocAtom) atoms
 
 checkJudocAtom ::
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   JudocAtom 'Parsed ->
   Sem r (JudocAtom 'Scoped)
 checkJudocAtom = \case
@@ -1476,7 +1794,7 @@ checkJudocAtom = \case
 
 checkParseExpressionAtoms ::
   forall r.
-  (Members '[Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r) =>
+  Members '[Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, NameIdGen] r =>
   ExpressionAtoms 'Parsed ->
   Sem r Expression
 checkParseExpressionAtoms = checkExpressionAtoms >=> parseExpressionAtoms
@@ -1487,20 +1805,6 @@ checkParsePatternAtom ::
   Sem r PatternArg
 checkParsePatternAtom = checkPatternAtom >=> parsePatternAtom
 
-checkStatement ::
-  (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) =>
-  Statement 'Parsed ->
-  Sem r (Statement 'Scoped)
-checkStatement s = topBindings $ case s of
-  StatementSyntax synDef -> StatementSyntax <$> checkSyntaxDef synDef
-  StatementTypeSignature tySig -> StatementTypeSignature <$> checkTypeSignature tySig
-  StatementImport imp -> StatementImport <$> checkImport imp
-  StatementInductive dt -> StatementInductive <$> checkInductiveDef dt
-  StatementModule dt -> StatementModule <$> checkLocalModule dt
-  StatementOpenModule open -> StatementOpenModule <$> checkOpenModule open
-  StatementFunctionClause clause -> StatementFunctionClause <$> checkFunctionClause clause
-  StatementAxiom ax -> StatementAxiom <$> checkAxiomDef ax
-
 checkSyntaxDef ::
   (Members '[Error ScoperError, Reader ScopeParameters, State Scope, State ScoperState, InfoTableBuilder, NameIdGen, State ScoperFixities, State ScoperIterators, State ScoperIterators] r) =>
   SyntaxDef ->
@@ -1755,29 +2059,29 @@ makePatternTable ::
   PatternAtoms 'Scoped -> [[P.Operator ParsePat PatternArg]]
 makePatternTable (PatternAtoms latoms _) = [appOp] : operators
   where
-    getConstructorRef :: PatternAtom 'Scoped -> Maybe ConstructorRef
+    getConstructorRef :: PatternAtom 'Scoped -> Maybe S.Name
     getConstructorRef = \case
       PatternAtomIden i -> case i of
         PatternScopedConstructor c -> Just c
         _ -> Nothing
       _ -> Nothing
     operators = mkSymbolTable (mapMaybe getConstructorRef (toList latoms))
-    mkSymbolTable :: [ConstructorRef] -> [[P.Operator ParsePat PatternArg]]
+    mkSymbolTable :: [S.Name] -> [[P.Operator ParsePat PatternArg]]
     mkSymbolTable = reverse . map (map snd) . groupSortOn' fst . mapMaybe unqualifiedSymbolOp
       where
-        unqualifiedSymbolOp :: ConstructorRef -> Maybe (Precedence, P.Operator ParsePat PatternArg)
-        unqualifiedSymbolOp (ConstructorRef' S.Name' {..})
+        unqualifiedSymbolOp :: S.Name -> Maybe (Precedence, P.Operator ParsePat PatternArg)
+        unqualifiedSymbolOp S.Name' {..}
           | Just Fixity {..} <- _nameFixity,
             _nameKind == S.KNameConstructor = Just $
               case _fixityArity of
                 Unary u -> (_fixityPrecedence, P.Postfix (unaryApp <$> parseSymbolId _nameId))
                   where
-                    unaryApp :: ConstructorRef -> PatternArg -> PatternArg
-                    unaryApp funName = case u of
-                      AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` funName)
+                    unaryApp :: S.Name -> PatternArg -> PatternArg
+                    unaryApp constrName = case u of
+                      AssocPostfix -> explicitP . PatternPostfixApplication . (`PatternPostfixApp` constrName)
                 Binary b -> (_fixityPrecedence, infixLRN (binaryInfixApp <$> parseSymbolId _nameId))
                   where
-                    binaryInfixApp :: ConstructorRef -> PatternArg -> PatternArg -> PatternArg
+                    binaryInfixApp :: S.Name -> PatternArg -> PatternArg -> PatternArg
                     binaryInfixApp name argLeft = explicitP . PatternInfixApplication . PatternInfixApp argLeft name
                     infixLRN :: ParsePat (PatternArg -> PatternArg -> PatternArg) -> P.Operator ParsePat PatternArg
                     infixLRN = case b of
@@ -1785,13 +2089,13 @@ makePatternTable (PatternAtoms latoms _) = [appOp] : operators
                       AssocRight -> P.InfixR
                       AssocNone -> P.InfixN
           | otherwise = Nothing
-        parseSymbolId :: S.NameId -> ParsePat ConstructorRef
+        parseSymbolId :: S.NameId -> ParsePat S.Name
         parseSymbolId uid = P.token getConstructorRefWithId mempty
           where
-            getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe ConstructorRef
+            getConstructorRefWithId :: PatternAtom 'Scoped -> Maybe S.Name
             getConstructorRefWithId s = do
               ref <- getConstructorRef s
-              guard (ref ^. constructorRefName . S.nameId == uid)
+              guard (ref ^. S.nameId == uid)
               return ref
 
     -- Application by juxtaposition.
@@ -1837,12 +2141,12 @@ parsePatternTerm = do
       explicitP . PatternConstructor
         <$> P.token constructorNoFixity mempty
       where
-        constructorNoFixity :: PatternAtom 'Scoped -> Maybe ConstructorRef
+        constructorNoFixity :: PatternAtom 'Scoped -> Maybe S.Name
         constructorNoFixity s = case s of
           PatternAtomIden (PatternScopedConstructor ref)
             | not (S.hasFixity n) -> Just ref
             where
-              n = ref ^. constructorRefName
+              n = ref
           _ -> Nothing
 
     parseWildcard :: ParsePat PatternArg

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error.hs

@@ -17,7 +17,6 @@ data ScoperError
   | ErrMultipleDeclarations MultipleDeclarations
   | ErrLacksTypeSig LacksTypeSig
   | ErrLacksFunctionClause LacksFunctionClause
-  | ErrDuplicateFunctionClause DuplicateFunctionClause
   | ErrImportCycle ImportCycle
   | ErrSymNotInScope NotInScope
   | ErrQualSymNotInScope QualSymNotInScope
@@ -44,7 +43,6 @@ data ScoperError
 instance ToGenericError ScoperError where
   genericError = \case
     ErrCaseBranchImplicitPattern e -> genericError e
-    ErrDuplicateFunctionClause e -> genericError e
     ErrInfixParser e -> genericError e
     ErrAppLeftImplicit e -> genericError e
     ErrInfixPattern e -> genericError e

src/Juvix/Compiler/Concrete/Translation/FromParsed/Analysis/Scoping/Error/Types.hs

@@ -643,35 +643,6 @@ instance ToGenericError ConstructorExpectedLeftApplication where
             "Constructor expected on the left of a pattern application:"
               <+> ppCode opts' pat
 
-data DuplicateFunctionClause = DuplicateFunctionClause
-  { _duplicateFunctionClauseSignature :: TypeSignature 'Scoped,
-    _duplicateFunctionClauseClause :: FunctionClause 'Scoped
-  }
-  deriving stock (Show)
-
-makeLenses ''DuplicateFunctionClause
-
-instance ToGenericError DuplicateFunctionClause where
-  genericError e = ask >>= generr
-    where
-      generr opts =
-        return
-          GenericError
-            { _genericErrorLoc = clLoc,
-              _genericErrorMessage = prettyError msg,
-              _genericErrorIntervals = [clLoc, sigLoc]
-            }
-        where
-          opts' = fromGenericOptions opts
-          cl :: FunctionClause 'Scoped
-          cl = e ^. duplicateFunctionClauseClause
-          name :: S.Symbol
-          name = e ^. duplicateFunctionClauseSignature . sigName
-          clLoc = getLoc (cl ^. clauseOwnerFunction)
-          sigLoc = getLoc name
-          msg =
-            "The function" <+> ppCode opts' name <+> "has already been assigned a definition and so it cannot have additional clauses"
-
 newtype CaseBranchImplicitPattern = CaseBranchImplicitPattern
   { _caseBranchImplicitPattern :: PatternArg
   }

src/Juvix/Compiler/Concrete/Translation/FromSource.hs

@@ -273,15 +273,34 @@ topModulePath = mkTopModulePath <$> dottedSymbol
 -- Top level statement
 --------------------------------------------------------------------------------
 
-statement :: (Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed)
+infixl 3 <?|>
+
+-- | Tries the left alternative. If it fails, backtracks and restores the contents of the pragmas and judoc stashes. Then parses the right atlernative
+(<?|>) :: Members '[PragmasStash, JudocStash] r => ParsecS r a -> ParsecS r a -> ParsecS r a
+l <?|> r = do
+  p <- P.lift (get @(Maybe ParsedPragmas))
+  j <- P.lift (get @(Maybe (Judoc 'Parsed)))
+  let recover = do
+        P.lift (put p)
+        P.lift (put j)
+        r
+  P.withRecovery (const recover) (P.try l)
+
+statement :: Members '[Files, Error ParserError, PathResolver, InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r => ParsecS r (Statement 'Parsed)
 statement = P.label "<top level statement>" $ do
   optional_ stashJudoc
   optional_ stashPragmas
   ms <-
     optional
       ( StatementSyntax <$> syntaxDef
-          <|> P.try (StatementOpenModule <$> newOpenSyntax)
-          <|> StatementOpenModule <$> openModule
+          <|> StatementOpenModule
+            <$> newOpenSyntax
+              -- TODO remove <?|> after removing old syntax
+              <?|> StatementFunctionDef
+            <$> newTypeSignature Nothing
+              -- TODO remove <?|> after removing old syntax
+              <?|> StatementOpenModule
+            <$> openModule
           <|> StatementImport <$> import_
           <|> StatementInductive <$> inductiveDef Nothing
           <|> StatementModule <$> moduleDef
@@ -476,11 +495,18 @@ builtinTypeSig b = do
   fun <- symbol
   typeSignature terminating fun (Just b)
 
+builtinNewTypeSig ::
+  Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
+  WithLoc BuiltinFunction ->
+  ParsecS r (FunctionDef 'Parsed)
+builtinNewTypeSig = newTypeSignature . Just
+
 builtinStatement :: (Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r) => ParsecS r (Statement 'Parsed)
 builtinStatement = do
   void (kw kwBuiltin)
   (builtinInductive >>= fmap StatementInductive . builtinInductiveDef)
-    <|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig)
+    <|> (builtinFunction >>= fmap StatementFunctionDef . builtinNewTypeSig)
+      <?|> (builtinFunction >>= fmap StatementTypeSignature . builtinTypeSig)
     <|> (builtinAxiom >>= fmap StatementAxiom . builtinAxiomDef)
 
 --------------------------------------------------------------------------------
@@ -793,8 +819,8 @@ auxTypeSigFunClause = do
           Left <$> typeSignature terminating sym Nothing
       | otherwise ->
           checkEq
-            <|> (Left <$> typeSignature terminating sym Nothing)
-            <|> (Right <$> functionClause sym)
+            <|> Left <$> typeSignature terminating sym Nothing
+            <|> Right <$> functionClause sym
   where
     checkEq :: ParsecS r a
     checkEq = do
@@ -802,6 +828,53 @@ auxTypeSigFunClause = do
       kw kwEq
       parseFailure off "expected \":=\" instead of \"=\""
 
+newTypeSignature ::
+  forall r.
+  Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
+  Maybe (WithLoc BuiltinFunction) ->
+  ParsecS r (FunctionDef 'Parsed)
+newTypeSignature _signBuiltin = P.label "<function definition>" $ do
+  _signTerminating <- optional (kw kwTerminating)
+  _signName <- symbol
+  _signArgs <- many parseArg
+  _signColonKw <- Irrelevant <$> kw kwColon
+  _signRetType <- parseExpressionAtoms
+  _signDoc <- getJudoc
+  _signPragmas <- getPragmas
+  _signBody <- parseBody
+  return FunctionDef {..}
+  where
+    parseArg :: ParsecS r (SigArg 'Parsed)
+    parseArg = do
+      (openDelim, _sigArgNames, _sigArgImplicit, _sigArgColon) <- P.try $ do
+        (opn, impl) <- implicitOpen
+        n <- some1 symbol
+        c <- Irrelevant <$> kw kwColon
+        return (opn, n, impl, c)
+      _sigArgType <- parseExpressionAtoms
+      closeDelim <- implicitClose _sigArgImplicit
+      let _sigArgDelims = Irrelevant (openDelim, closeDelim)
+      return SigArg {..}
+
+    parseBody :: ParsecS r (FunctionDefBody 'Parsed)
+    parseBody =
+      SigBodyExpression <$> bodyExpr
+        <|> (SigBodyClauses <$> bodyClauses)
+      where
+        bodyClause :: ParsecS r (NewFunctionClause 'Parsed)
+        bodyClause = do
+          _clausenPipeKw <- Irrelevant <$> kw kwPipe
+          _clausenPatterns <- some1 patternAtom
+          _clausenAssignKw <- Irrelevant <$> kw kwAssign
+          _clausenBody <- parseExpressionAtoms
+          return NewFunctionClause {..}
+        bodyClauses :: ParsecS r (NonEmpty (NewFunctionClause 'Parsed))
+        bodyClauses = some1 bodyClause
+        bodyExpr :: ParsecS r (ExpressionAtoms 'Parsed)
+        bodyExpr = do
+          void (kw kwAssign)
+          parseExpressionAtoms
+
 axiomDef ::
   Members '[InfoTableBuilder, PragmasStash, JudocStash, NameIdGen] r =>
   Maybe (WithLoc BuiltinAxiom) ->

src/Juvix/Compiler/Internal/Translation/FromConcrete.hs

@@ -278,20 +278,30 @@ goModuleBody stmts = do
   _moduleImports <- mapM goImport (scanImports stmts)
   otherThanFunctions :: [Indexed Internal.PreStatement] <- concatMapM (traverseM' goStatement) ss
   functions <- map (fmap Internal.PreFunctionDef) <$> compiledFunctions
+  newFunctions <- map (fmap Internal.PreFunctionDef) <$> newCompiledFunctions
   let _moduleStatements =
         map
           (^. indexedThing)
           ( sortOn
               (^. indexedIx)
-              (otherThanFunctions <> functions)
+              (otherThanFunctions <> functions <> newFunctions)
           )
   return Internal.ModuleBody {..}
   where
+    ss' :: [Statement 'Scoped]
     ss' = concatMap Concrete.flattenStatement stmts
 
     ss :: [Indexed (Statement 'Scoped)]
     ss = zipWith Indexed [0 ..] ss'
 
+    newCompiledFunctions :: Sem r [Indexed Internal.FunctionDef]
+    newCompiledFunctions =
+      sequence
+        [ Indexed i <$> funDef
+          | Indexed i (StatementFunctionDef f) <- ss,
+            let funDef = goTopNewFunctionDef f
+        ]
+
     compiledFunctions :: Sem r [Indexed Internal.FunctionDef]
     compiledFunctions =
       sequence
@@ -304,7 +314,7 @@ goModuleBody stmts = do
         getClauses :: S.Symbol -> [FunctionClause 'Scoped]
         getClauses name = [c | StatementFunctionClause c <- ss', name == c ^. clauseOwnerFunction]
         sigs :: [Indexed (TypeSignature 'Scoped)]
-        sigs = [Indexed i t | (Indexed i (StatementTypeSignature t)) <- ss]
+        sigs = [Indexed i t | Indexed i (StatementTypeSignature t) <- ss]
 
 scanImports :: [Statement 'Scoped] -> [Import 'Scoped]
 scanImports stmts = mconcatMap go stmts
@@ -319,6 +329,7 @@ scanImports stmts = mconcatMap go stmts
       StatementTypeSignature {} -> []
       StatementAxiom {} -> []
       StatementSyntax {} -> []
+      StatementFunctionDef {} -> []
       where
         openImport :: OpenModule 'Scoped -> Maybe (Import 'Scoped)
         openImport o = case o ^. openModuleImportKw of
@@ -352,6 +363,7 @@ guardNotCached (hit, m) = do
   guard (not hit)
   return m
 
+-- | Ignores functions
 goStatement ::
   forall r.
   Members '[Error ScoperError, Builtins, NameIdGen, Reader Pragmas] r =>
@@ -362,6 +374,7 @@ goStatement = \case
   StatementAxiom d -> pure . Internal.PreAxiomDef <$> goAxiom d
   StatementModule f -> goLocalModule f
   StatementImport {} -> return []
+  StatementFunctionDef {} -> return []
   StatementSyntax {} -> return []
   StatementOpenModule {} -> return []
   StatementTypeSignature {} -> return []
@@ -416,7 +429,7 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do
   _funDefPragmas <- goPragmas _sigPragmas
   _funDefClauses <- case (_sigBody, nonEmpty clauses) of
     (Nothing, Nothing) -> throw (ErrLacksFunctionClause (LacksFunctionClause sig))
-    (Just {}, Just clauses') -> throw (ErrDuplicateFunctionClause (DuplicateFunctionClause sig (head clauses')))
+    (Just {}, Just {}) -> error "duplicate function clause. TODO remove this when old function syntax is removed"
     (Just body, Nothing) -> do
       body' <- goExpression body
       return
@@ -430,6 +443,65 @@ goFunctionDefHelper sig@TypeSignature {..} clauses = do
     (Nothing, Just clauses') -> mapM goFunctionClause clauses'
   return Internal.FunctionDef {..}
 
+goTopNewFunctionDef ::
+  forall r.
+  (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
+  FunctionDef 'Scoped ->
+  Sem r Internal.FunctionDef
+goTopNewFunctionDef FunctionDef {..} = do
+  let _funDefName = goSymbol _signName
+      _funDefTerminating = isJust _signTerminating
+      _funDefBuiltin = (^. withLocParam) <$> _signBuiltin
+  _funDefType <- goDefType
+  _funDefExamples <- goExamples _signDoc
+  _funDefPragmas <- goPragmas _signPragmas
+  _funDefClauses <- goBody
+  return Internal.FunctionDef {..}
+  where
+    goBody :: Sem r (NonEmpty Internal.FunctionClause)
+    goBody = do
+      commonPatterns <- concatMapM (fmap toList . argToPattern) _signArgs
+      let _clauseName = goSymbol _signName
+          goClause :: NewFunctionClause 'Scoped -> Sem r Internal.FunctionClause
+          goClause NewFunctionClause {..} = do
+            let _clauseName = goSymbol _signName
+            _clauseBody <- goExpression _clausenBody
+            extraPatterns <- toList <$> (mapM goPatternArg _clausenPatterns)
+            let _clausePatterns = commonPatterns <> extraPatterns
+            return Internal.FunctionClause {..}
+      case _signBody of
+        SigBodyExpression body -> do
+          _clauseBody <- goExpression body
+          let _clausePatterns = commonPatterns
+          return (pure Internal.FunctionClause {..})
+        SigBodyClauses cls -> mapM goClause cls
+
+    goDefType :: Sem r Internal.Expression
+    goDefType = do
+      args <- concatMapM (fmap toList . argToParam) _signArgs
+      ret <- goExpression _signRetType
+      return (Internal.foldFunType args ret)
+      where
+        argToParam :: SigArg 'Scoped -> Sem r (NonEmpty Internal.FunctionParameter)
+        argToParam SigArg {..} = do
+          _paramType <- goExpression _sigArgType
+          let _paramImplicit = _sigArgImplicit
+              mk :: S.Symbol -> Sem r Internal.FunctionParameter
+              mk s =
+                let _paramName = Just (goSymbol s)
+                 in return Internal.FunctionParameter {..}
+          mapM mk _sigArgNames
+
+    argToPattern :: SigArg 'Scoped -> Sem r (NonEmpty Internal.PatternArg)
+    argToPattern SigArg {..} = do
+      let _patternArgIsImplicit = _sigArgImplicit
+          _patternArgName :: Maybe Internal.Name = Nothing
+          mk :: S.Symbol -> Sem r Internal.PatternArg
+          mk s = do
+            let _patternArgPattern = Internal.PatternVariable (goSymbol s)
+            return Internal.PatternArg {..}
+      mapM mk _sigArgNames
+
 goTopFunctionDef ::
   forall r.
   (Members '[Reader Pragmas, Error ScoperError, Builtins, NameIdGen] r) =>
@@ -671,11 +743,11 @@ goExpression = \case
 
     goIden :: Concrete.ScopedIden -> Internal.Expression
     goIden x = Internal.ExpressionIden $ case x of
-      ScopedAxiom a -> Internal.IdenAxiom (goName (a ^. Concrete.axiomRefName))
-      ScopedInductive i -> Internal.IdenInductive (goName (i ^. Concrete.inductiveRefName))
+      ScopedAxiom a -> Internal.IdenAxiom (goName a)
+      ScopedInductive i -> Internal.IdenInductive (goName i)
       ScopedVar v -> Internal.IdenVar (goSymbol v)
-      ScopedFunction fun -> Internal.IdenFunction (goName (fun ^. Concrete.functionRefName))
-      ScopedConstructor c -> Internal.IdenConstructor (goName (c ^. Concrete.constructorRefName))
+      ScopedFunction fun -> Internal.IdenFunction (goName fun)
+      ScopedConstructor c -> Internal.IdenConstructor (goName c)
 
     goLet :: Let 'Scoped -> Sem r Internal.Let
     goLet l = do
@@ -834,7 +906,7 @@ goPatternApplication a = uncurry mkConstructorApp <$> viewApp (PatternApplicatio
 
 goPatternConstructor ::
   Members '[Builtins, NameIdGen, Error ScoperError] r =>
-  ConstructorRef ->
+  S.Name ->
   Sem r Internal.ConstructorApp
 goPatternConstructor a = uncurry mkConstructorApp <$> viewApp (PatternConstructor a)
 
@@ -874,8 +946,8 @@ viewApp p = case p of
       | otherwise = viewApp (l ^. patternArgPattern)
     err = throw (ErrConstructorExpectedLeftApplication (ConstructorExpectedLeftApplication p))
 
-goConstructorRef :: ConstructorRef -> Internal.Name
-goConstructorRef (ConstructorRef' n) = goName n
+goConstructorRef :: S.Name -> Internal.Name
+goConstructorRef n = goName n
 
 goPatternArg :: Members '[Builtins, NameIdGen, Error ScoperError] r => PatternArg -> Sem r Internal.PatternArg
 goPatternArg p = do

src/Juvix/Formatter.hs

@@ -2,6 +2,7 @@ module Juvix.Formatter where
 
 import Data.List.NonEmpty qualified as NonEmpty
 import Data.Text qualified as T
+import Juvix.Compiler.Concrete.Extra (migrateFunctionSyntax)
 import Juvix.Compiler.Concrete.Language
 import Juvix.Compiler.Concrete.Print (ppOutDefault)
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
@@ -17,6 +18,8 @@ data FormattedFileInfo = FormattedFileInfo
     _formattedFileInfoContentsModified :: Bool
   }
 
+newtype NewSyntax = NewSyntax Bool
+
 data ScopeEff m a where
   ScopeFile :: Path Abs File -> ScopeEff m Scoper.ScoperResult
   ScopeStdin :: ScopeEff m Scoper.ScoperResult
@@ -62,7 +65,7 @@ formattedFileInfoContentsText = to infoToPlainText
 -- contents of the file.
 format ::
   forall r.
-  Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
+  Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
   Path Abs File ->
   Sem r FormatResult
 format p = do
@@ -88,7 +91,7 @@ format p = do
 -- subdirectories that contain a juvix.yaml file.
 formatProject ::
   forall r.
-  Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
+  Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
   Path Abs Dir ->
   Sem r FormatResult
 formatProject p = do
@@ -105,14 +108,14 @@ formatProject p = do
       subRes <- combineResults <$> mapM format juvixFiles
       return (res <> subRes, RecurseFilter (\hasJuvixYaml d -> not hasJuvixYaml && not (isHiddenDirectory d)))
 
-formatPath :: Members [Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText)
+formatPath :: Members [Reader NewSyntax, Reader Text, ScopeEff] r => Path Abs File -> Sem r (NonEmpty AnsiText)
 formatPath p = do
   res <- scopeFile p
   formatScoperResult res
 
 formatStdin ::
   forall r.
-  Members '[ScopeEff, Files, Output FormattedFileInfo] r =>
+  Members '[Reader NewSyntax, ScopeEff, Files, Output FormattedFileInfo] r =>
   Sem r FormatResult
 formatStdin = do
   res <- scopeStdin
@@ -144,10 +147,13 @@ formatResultFromContents formattedContents filepath = do
         )
       return res
 
-formatScoperResult :: Member (Reader Text) r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
+formatScoperResult :: Members [Reader NewSyntax, Reader Text] r => Scoper.ScoperResult -> Sem r (NonEmpty AnsiText)
 formatScoperResult res = do
   let cs = res ^. Scoper.comments
-      formattedModules = run (runReader cs (mapM formatTopModule (res ^. Scoper.resultModules)))
+  formattedModules <-
+    runReader cs
+      . mapM formatTopModule
+      $ res ^. Scoper.resultModules
   case res ^. Scoper.mainModule . modulePragmas of
     Just pragmas ->
       case pragmas ^. withLocParam . withSourceValue . pragmasFormat of
@@ -159,7 +165,11 @@ formatScoperResult res = do
     Nothing ->
       return formattedModules
   where
-    formatTopModule :: Member (Reader Comments) r => Module 'Scoped 'ModuleTop -> Sem r AnsiText
+    formatTopModule :: Members [Reader NewSyntax, Reader Comments] r => Module 'Scoped 'ModuleTop -> Sem r AnsiText
     formatTopModule m = do
+      NewSyntax newSyntax <- ask
       cs <- ask
-      return (ppOutDefault cs m)
+      let m'
+            | newSyntax = migrateFunctionSyntax m
+            | otherwise = m
+      return (ppOutDefault cs m')

test/Formatter/Positive.hs

@@ -22,7 +22,14 @@ makeFormatTest' Scope.PosTest {..} =
         { _testName = _name,
           _testRoot = tRoot,
           _testAssertion = Single $ do
-            d <- runM $ runError $ runOutputList @FormattedFileInfo $ runScopeEffIO $ runFilesIO $ format file'
+            d <-
+              runM
+                . runError
+                . runOutputList @FormattedFileInfo
+                . runScopeEffIO
+                . runFilesIO
+                . runReader (NewSyntax False)
+                $ format file'
             case d of
               Right (_, FormatResultOK) -> return ()
               Right (_, FormatResultNotFormatted) -> assertFailure ("File: " <> show file' <> " is not formatted")

test/Scope/Negative.hs

@@ -225,13 +225,6 @@ scoperErrorTests =
       $ \case
         ErrMultipleDeclarations {} -> Nothing
         _ -> wrongError,
-    NegTest
-      "A function has a duplicate clause"
-      $(mkRelDir ".")
-      $(mkRelFile "DuplicateClause.juvix")
-      $ \case
-        ErrDuplicateFunctionClause {} -> Nothing
-        _ -> wrongError,
     NegTest
       "A function lacks a type signature"
       $(mkRelDir ".")

test/Scope/Positive.hs

@@ -6,7 +6,6 @@ import Juvix.Compiler.Builtins (evalTopBuiltins)
 import Juvix.Compiler.Concrete qualified as Concrete
 import Juvix.Compiler.Concrete.Data.Highlight (ignoreHighlightBuilder)
 import Juvix.Compiler.Concrete.Extra
-import Juvix.Compiler.Concrete.Pretty qualified as M
 import Juvix.Compiler.Concrete.Print qualified as P
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.PathResolver
 import Juvix.Compiler.Concrete.Translation.FromParsed.Analysis.Scoping qualified as Scoper
@@ -26,11 +25,8 @@ makeLenses ''PosTest
 root :: Path Abs Dir
 root = relToProject $(mkRelDir "tests/positive")
 
-renderCodeOld :: (HasLoc c, M.PrettyPrint c) => c -> Text
-renderCodeOld = toPlainText . M.ppOutDefault
-
-renderCodeNew :: (HasLoc c, P.PrettyPrint c) => c -> Text
-renderCodeNew = toPlainText . P.ppOutDefault emptyComments
+renderCodeNew :: P.PrettyPrint c => c -> Text
+renderCodeNew = toPlainText . P.ppOutNoComments P.defaultOptions
 
 testDescr :: PosTest -> TestDescr
 testDescr PosTest {..} = helper renderCodeNew
@@ -84,7 +80,7 @@ testDescr PosTest {..} = helper renderCodeNew
                     fsParsed :: HashMap (Path Abs File) Text
                     fsParsed =
                       HashMap.fromList $
-                        [ (getModuleFilePath m, renderCodeOld m)
+                        [ (getModuleFilePath m, renderCodeNew m)
                           | m <- toList (p ^. Parser.resultTable . Parser.infoParsedModules)
                         ]
                           <> yamlFiles
@@ -239,6 +235,10 @@ tests =
       "Iterators"
       $(mkRelDir ".")
       $(mkRelFile "Iterators.juvix"),
+    PosTest
+      "New function syntax"
+      $(mkRelDir ".")
+      $(mkRelFile "Syntax.juvix"),
     PosTest
       "Format pragma"
       $(mkRelDir ".")

tests/Compilation/positive/test052.juvix

@@ -2,6 +2,7 @@
 module test052;
 
 open import Stdlib.Prelude;
+import Stdlib.Trait.Show as Show;
 
 fromShow : {a : Type} -> Show a -> a -> String;
 fromShow (mkShow s) a := s a;
@@ -84,7 +85,7 @@ module ExprTraits;
   toString (num n) := natToString n;
 
   --- ;Show; instance for ;Expr;.
-  Show : Show Expr;
+  Show : Show.Show Expr;
   Show := mkShow toString;
 end;
 
@@ -94,7 +95,7 @@ module ValTraits;
 
   --- ;Show; instance for ;Val;.
   terminating
-  Show : Show Val;
+  Show : Show.Show Val;
   Show := mkShow valToString;
 
   valToString (vnum n) := natToString n;

tests/negative/DuplicateClause.juvix

@@ -1,7 +0,0 @@
-module DuplicateClause;
-
-axiom T : Type;
-
-id : T → T := λ {t := t};
-id t := t;
-

tests/positive/Format.juvix

@@ -5,9 +5,9 @@ Format;
 import -- Import a module of name:
 Stdlib.Prelude open -- Bring all names into scope but..
 hiding -- Hide some names
-{-- like this 
+{-- like this
 ,; -- don't want , here
--- Bool either 
+-- Bool either
 Bool; true; false};
 
 import Stdlib.Data.Nat.Ord open;
@@ -117,8 +117,8 @@ axiom undefined : {A : Type} -> A;
 
 -- 200 in the body is idented with respect to the start of the chain
 -- (at {A : Type})
-exampleFunction2 :
-  {A : Type}
+exampleFunction2
+  : {A : Type}
     -> List A
     -> List A
     -> List A
@@ -127,20 +127,20 @@ exampleFunction2 :
     -> List A
     -> List A
     -> Nat :=
-    λ {_ _ _ _ _ _ _ :=
-      undefined
-        -- comment after first
-        + undefined
-        -- comment after second
-        + undefined
-        + undefined
-        + undefined
-        + undefined
-        + undefined
-        + undefined
-        + undefined
-        + undefined
-        + undefined};
+  λ {_ _ _ _ _ _ _ :=
+    undefined
+      -- comment after first
+      + undefined
+      -- comment after second
+      + undefined
+      + undefined
+      + undefined
+      + undefined
+      + undefined
+      + undefined
+      + undefined
+      + undefined
+      + undefined};
 
 positive
 type T0 (A : Type) :=

tests/positive/SignatureWithBody.juvix

@@ -2,20 +2,18 @@ module SignatureWithBody;
 
 import Stdlib.Prelude open;
 
-isNull :
-  {A : Type} → List A → Bool :=
-    λ {
-      | nil := true
-      | _ := false
-    };
+isNull : {A : Type} → List A → Bool :=
+  λ {
+    | nil := true
+    | _ := false
+  };
 
-isNull' :
-  {A : Type} → List A → Bool :=
-    let
-      aux :
-        {A : Type} → List A → Bool :=
-          λ {
-            | nil := true
-            | _ := false
-          };
-    in aux;
+isNull' : {A : Type} → List A → Bool :=
+  let
+    aux :
+      {A : Type} → List A → Bool :=
+        λ {
+          | nil := true
+          | _ := false
+        };
+  in aux;

tests/positive/Syntax.juvix

@@ -0,0 +1,60 @@
+module Syntax;
+
+compose {A B C : Type} (f : B -> C) (g : A -> B) (x : A)
+  : C := f (g x);
+
+compose' {A B C : Type} (f : B -> C) (g : A -> B) : A -> C
+  | x := f (g x);
+
+type Bool :=
+  | false : Bool
+  | true : Bool;
+
+type Nat :=
+  | zero : Nat
+  | suc : Nat -> Nat;
+
+not : Bool -> Bool
+  | false := true
+  | true := false;
+
+even : Nat -> Bool
+  | zero := true
+  | (suc n) := odd n;
+
+odd : Nat -> Bool
+  | zero := false
+  | (suc n) := even n;
+
+syntax infixl 4 ==1;
+
+==1 : Nat -> Nat -> Bool
+  | zero zero := true
+  | (suc a) (suc b) := a ==2 b
+  | _ _ := false;
+
+-- note that ==2 is used before its infix definition
+syntax infixl 4 ==2;
+
+==2 : Nat -> Nat -> Bool
+  | zero zero := true
+  | (suc a) (suc b) := a ==1 b
+  | _ _ := false;
+
+module MutualTypes;
+  -- we use Tree and isEmpty before their definition
+  isNotEmpty {a : Type} (t : Tree a) : Bool :=
+    not (isEmpty t);
+
+  isEmpty {a : Type} : (t : Tree a) -> Bool
+    | empty := true
+    | (node _ _) := false;
+
+  type Tree (a : Type) :=
+    | empty : Tree a
+    | node : a -> Forest a -> Tree a;
+
+  type Forest (a : Type) :=
+    | nil : Forest a
+    | cons : Tree a -> Forest a;
+end;

tests/smoke/Commands/repl.smoke.yaml

@@ -62,9 +62,9 @@ tests:
       contains: |
         --- Addition for ;Nat;s.
         builtin nat-plus
-        + : Nat → Nat → Nat;
-        + zero b := b;
-        + (suc a) b := suc (a + b);
+        + : Nat → Nat → Nat
+          | zero b := b
+          | (suc a) b := suc (a + b)
     exit-status: 0
 
   - name: repl-def-infix
@@ -77,9 +77,9 @@ tests:
       contains: |
         --- Addition for ;Nat;s.
         builtin nat-plus
-        + : Nat → Nat → Nat;
-        + zero b := b;
-        + (suc a) b := suc (a + b);
+        + : Nat → Nat → Nat
+          | zero b := b
+          | (suc a) b := suc (a + b)
     exit-status: 0
 
   - name: open