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

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,21 +46,29 @@ 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))
           registerDoc (f ^. sigName . nameId) j
   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)