Non-recursive definitions (#3138)

* Closes #2968 
* Implements detection of function-like definitions, which either:
  - have some arguments on the left of `:`, or
  - have at least one clause.
* Only function-like definitions are recursive.
* Non-recursive definitions are not mutually recursive either, and can
be used only after their definition. This necessitates rearranging some
definitions in existing Juvix code.
* Changes the scoping of identifiers in record updates. Now field names
on the right side don't refer to the old values of the record fields but
to identifiers in scope defined outside the record update. To refer to
old values, one needs to explicitly use record projections, e.g.
```
r@Rec{x := Rec.x r}
```

cntlines.sh

@@ -40,10 +40,12 @@ EXTRA=$(count src/Juvix/Extra/)
 DATA=$(count src/Juvix/Data/)
 PRELUDE=$(count src/Juvix/Prelude/)
 STORE=$(count src/Juvix/Compiler/Store/)
+ANOMA=$(count src/Anoma/)
+PARALLEL=$(count src/Parallel/)
 
 FRONT=$((CONCRETE + INTERNAL + BUILTINS + PIPELINE))
 BACK=$((BACKENDC + BACKENDRUST + VAMPIR + NOCK + REG + ASM + TREE + CORE + CASM + CAIRO))
-OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE))
+OTHER=$((APP + STORE + HTML + MARKDOWN + ISABELLE + EXTRA + DATA + PRELUDE + ANOMA + PARALLEL))
 TESTS=$(count test/)
 STDLIB=$(count_ext '*.juvix' juvix-stdlib/Stdlib)
 
@@ -79,6 +81,8 @@ echo "   Isabelle: $ISABELLE LOC"
 echo "   Extra: $EXTRA LOC"
 echo "   Data: $DATA LOC"
 echo "   Prelude: $PRELUDE LOC"
+echo "   Anoma: $ANOMA LOC"
+echo "   Parallel: $PARALLEL LOC"
 echo "Tests: $TESTS LOC"
 echo "Standard library: $STDLIB LOC"
 echo ""

include/package/PackageDescription/V1.juvix

@@ -43,6 +43,9 @@ type Dependency :=
   | --- The ;defaultStdlib; that is bundled with the Juvix compiler.
     defaultStdlib;
 
+--- The default version used in `defaultPackage`.
+defaultVersion : SemVer := mkVersion 0 0 0;
+
 --- Construct a ;Package; with useful default arguments.
 defaultPackage
   {name : String := "my-project"}
@@ -67,9 +70,6 @@ mkVersion
     meta;
   };
 
---- The default version used in `defaultPackage`.
-defaultVersion : SemVer := mkVersion 0 0 0;
-
 --- Constructs a GitHub dependency.
 github (org repo ref : String) : Dependency :=
   git

include/package/PackageDescription/V2.juvix

@@ -43,16 +43,6 @@ type Dependency :=
   | --- The ;defaultStdlib; that is bundled with the Juvix compiler.
     defaultStdlib;
 
---- Construct a ;Package; with useful default arguments.
-defaultPackage
-  {name : String := "my-project"}
-  {version : SemVer := defaultVersion}
-  {dependencies : List Dependency := [defaultStdlib]}
-  {main : Maybe String := nothing}
-  {buildDir : Maybe String := nothing}
-  : Package :=
-  mkPackage name version dependencies main buildDir;
-
 --- Construct a ;SemVer; with useful default arguments.
 mkVersion
   (major minor patch : Nat)
@@ -70,6 +60,16 @@ mkVersion
 --- The default version used in `defaultPackage`.
 defaultVersion : SemVer := mkVersion 0 0 0;
 
+--- Construct a ;Package; with useful default arguments.
+defaultPackage
+  {name : String := "my-project"}
+  {version : SemVer := defaultVersion}
+  {dependencies : List Dependency := [defaultStdlib]}
+  {main : Maybe String := nothing}
+  {buildDir : Maybe String := nothing}
+  : Package :=
+  mkPackage name version dependencies main buildDir;
+
 --- Constructs a GitHub dependency.
 github (org repo ref : String) : Dependency :=
   git

src/Juvix/Compiler/Concrete/Extra.hs

@@ -8,6 +8,7 @@ module Juvix.Compiler.Concrete.Extra
     getExpressionAtomIden,
     getPatternAtomIden,
     isBodyExpression,
+    isFunctionLike,
     symbolParsed,
   )
 where
@@ -106,3 +107,7 @@ isBodyExpression :: FunctionDefBody a -> Bool
 isBodyExpression = \case
   SigBodyExpression {} -> True
   SigBodyClauses {} -> False
+
+isFunctionLike :: FunctionDef a -> Bool
+isFunctionLike = \case
+  FunctionDef {..} -> not (null _signArgs) || not (isBodyExpression _signBody)

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

@@ -17,7 +17,6 @@ import Juvix.Compiler.Concrete.Data.NameSignature
 import Juvix.Compiler.Concrete.Data.Scope
 import Juvix.Compiler.Concrete.Data.ScopedName (nameConcrete)
 import Juvix.Compiler.Concrete.Data.ScopedName qualified as S
-import Juvix.Compiler.Concrete.Extra (recordNameSignatureByIndex)
 import Juvix.Compiler.Concrete.Extra qualified as P
 import Juvix.Compiler.Concrete.Gen qualified as G
 import Juvix.Compiler.Concrete.Language
@@ -436,6 +435,14 @@ reserveAxiomSymbol a =
     kindPretty :: NameKind
     kindPretty = maybe KNameAxiom getNameKind (a ^? axiomBuiltin . _Just . withLocParam)
 
+reserveFunctionLikeSymbol ::
+  (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) =>
+  FunctionDef 'Parsed ->
+  Sem r ()
+reserveFunctionLikeSymbol f =
+  when (P.isFunctionLike f) $
+    void (reserveFunctionSymbol f)
+
 bindFunctionSymbol ::
   (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, InfoTableBuilder, Reader InfoTable, State ScoperState, Reader BindingStrategy] r) =>
   Symbol ->
@@ -1077,14 +1084,17 @@ checkFunctionDef ::
   (Members '[HighlightBuilder, Reader ScopeParameters, Error ScoperError, State Scope, State ScoperState, InfoTableBuilder, Reader InfoTable, NameIdGen, Reader PackageId, State ScoperSyntax, Reader BindingStrategy] r) =>
   FunctionDef 'Parsed ->
   Sem r (FunctionDef 'Scoped)
-checkFunctionDef FunctionDef {..} = do
-  sigName' <- bindFunctionSymbol _signName
+checkFunctionDef fdef@FunctionDef {..} = do
   sigDoc' <- mapM checkJudoc _signDoc
   (args', sigType', sigBody') <- withLocalScope $ do
     a' <- mapM checkArg _signArgs
     t' <- mapM checkParseExpressionAtoms _signRetType
     b' <- checkBody
     return (a', t', b')
+  sigName' <-
+    if
+        | P.isFunctionLike fdef -> bindFunctionSymbol _signName
+        | otherwise -> reserveFunctionSymbol fdef
   let def =
         FunctionDef
           { _signName = sigName',
@@ -1481,7 +1491,7 @@ checkSections sec = topBindings helper
         goDefinitions :: DefinitionsSection 'Parsed -> Sem r' (DefinitionsSection 'Scoped)
         goDefinitions DefinitionsSection {..} = goDefs [] [] (toList _definitionsSection)
           where
-            -- This functions goes through a section reserving definitions and
+            -- This functions go through a section reserving definitions and
             -- collecting inductive modules. It breaks a section when the
             -- collected inductive modules are non-empty (there were some
             -- inductive definitions) and the next definition is a function
@@ -1575,9 +1585,9 @@ checkSections sec = topBindings helper
             reserveDefinition :: Definition 'Parsed -> Sem r' (Maybe (Module 'Parsed 'ModuleLocal))
             reserveDefinition = \case
               DefinitionSyntax s -> resolveSyntaxDef s $> Nothing
-              DefinitionFunctionDef d -> void (reserveFunctionSymbol d) >> return Nothing
-              DefinitionAxiom d -> void (reserveAxiomSymbol d) >> return Nothing
-              DefinitionProjectionDef d -> void (reserveProjectionSymbol d) >> return Nothing
+              DefinitionFunctionDef d -> reserveFunctionLikeSymbol d >> return Nothing
+              DefinitionAxiom d -> reserveAxiomSymbol d >> return Nothing
+              DefinitionProjectionDef d -> reserveProjectionSymbol d >> return Nothing
               DefinitionInductive d -> Just <$> reserveInductive d
               where
                 -- returns the module generated for the inductive definition
@@ -2701,7 +2711,7 @@ checkExpressionAtom e = case e of
 
 reserveNamedArgumentName :: (Members '[Error ScoperError, NameIdGen, State ScoperSyntax, State Scope, State ScoperState, Reader BindingStrategy, InfoTableBuilder, Reader InfoTable] r) => NamedArgumentNew 'Parsed -> Sem r ()
 reserveNamedArgumentName a = case a of
-  NamedArgumentNewFunction f -> void (reserveFunctionSymbol (f ^. namedArgumentFunctionDef))
+  NamedArgumentNewFunction f -> reserveFunctionLikeSymbol (f ^. namedArgumentFunctionDef)
   NamedArgumentItemPun {} -> return ()
 
 checkNamedApplicationNew ::
@@ -2794,7 +2804,7 @@ checkRecordUpdate RecordUpdate {..} = do
   info <- getRecordInfo tyName'
   let sig = info ^. recordInfoSignature
   (vars' :: IntMap (IsImplicit, S.Symbol), fields') <- withLocalScope $ do
-    vs <- mapM bindRecordUpdateVariable (recordNameSignatureByIndex sig)
+    vs <- mapM bindRecordUpdateVariable (P.recordNameSignatureByIndex sig)
     fs <- mapM (checkUpdateField sig) _recordUpdateFields
     return (vs, fs)
   let extra' =
@@ -2814,7 +2824,7 @@ checkRecordUpdate RecordUpdate {..} = do
     bindRecordUpdateVariable :: NameItem 'Parsed -> Sem r (IsImplicit, S.Symbol)
     bindRecordUpdateVariable NameItem {..} = do
       -- all fields have names so it is safe to use fromJust
-      v <- bindVariableSymbol (fromJust _nameItemSymbol)
+      v <- ignoreSyntax $ freshVariable (fromJust _nameItemSymbol)
       return (_nameItemImplicit, v)
 
 checkUpdateField ::

test/Compilation/Positive.hs

@@ -485,5 +485,10 @@ tests =
         "Test082: Pattern matching with side conditions"
         $(mkRelDir ".")
         $(mkRelFile "test082.juvix")
-        $(mkRelFile "out/test082.out")
+        $(mkRelFile "out/test082.out"),
+      posTest
+        "Test083: Record update"
+        $(mkRelDir ".")
+        $(mkRelFile "test083.juvix")
+        $(mkRelFile "out/test083.out")
     ]

tests/Anoma/Compilation/positive/test006.juvix

@@ -5,10 +5,10 @@ import Stdlib.Prelude open;
 import Stdlib.Debug open;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
 main : Bool :=
   trace
-      (ite (3 > 0) 1 loop + ite (2 < 1) loop (ite (7 >= 8) loop 1))
-    >-> trace (2 > 0 || loop == 0)
-    >-> 2 < 0 && loop == 0;
+      (ite (3 > 0) 1 (loop 0) + ite (2 < 1) (loop 0) (ite (7 >= 8) (loop 0) 1))
+    >-> trace (2 > 0 || loop 0 == 0)
+    >-> 2 < 0 && loop 0 == 0;

tests/Anoma/Compilation/positive/test034.juvix

@@ -6,11 +6,9 @@ import Stdlib.Debug.Trace open;
 
 sum : Nat → Nat :=
   let
-    sum' : Nat → Nat :=
-      λ {
-        zero := zero
-        | (suc n) := suc n + sum' n
-      };
+    sum' : Nat → Nat
+      | zero := zero
+      | (suc n) := suc n + sum' n
   in sum';
 
 mutrec : Nat :=

tests/Anoma/Compilation/positive/test060.juvix

@@ -26,11 +26,11 @@ main : Triple Nat Nat Nat :=
     p : Triple Nat Nat Nat := mkTriple 2 2 2;
     p' : Triple Nat Nat Nat :=
       p@Triple{
-        fst := fst + 1;
-        snd := snd * 3 + thd + fst
+        fst := Triple.fst p + 1;
+        snd := Triple.snd p * 3 + Triple.thd p + Triple.fst p
       };
     f : Triple Nat Nat Nat -> Triple Nat Nat Nat :=
-      (@Triple{fst := fst * 10});
+      \{p := p@Triple{fst := Triple.fst p * 10}};
   in ite
     (mf
       mkPair@{