Non-recursive definitions

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@{