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

juvix-stdlib

@@ -1 +1 @@
-Subproject commit deaafbb3c097fa2d84143018f6ae7266a2a92e14
+Subproject commit 8bc67b874860a26cba02d853b879e9c0a347efe2

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

tests/Anoma/Compilation/positive/test077.juvix

@@ -18,112 +18,115 @@ axiom anomaSignDetached : {A : Type} -> A -> ByteArray -> ByteArray;
 builtin anoma-verify-detached
 axiom anomaVerifyDetached : {A : Type} -> ByteArray -> A -> ByteArray -> Bool;
 
-main : Bool :=
-  let
-    msg : Nat := 1;
-    sig : ByteArray := anomaSignDetached msg privKey;
-  in trace (byteArrayLength sig) >-> anomaVerifyDetached (anomaSignDetached msg privKey) msg pubKey;
-
 privKey : ByteArray :=
   mkByteArray
-    [ 0xa9
-    ; 0xde
-    ; 0xd6
-    ; 0x29
-    ; 0x93
-    ; 0xfb
-    ; 0x52
-    ; 0x61
-    ; 0xfb
-    ; 0x59
-    ; 0xf7
-    ; 0xd4
-    ; 0x78
-    ; 0x42
-    ; 0xe5
-    ; 0xa7
-    ; 0x81
-    ; 0xf6
-    ; 0xe
-    ; 0x48
-    ; 0xb5
-    ; 0x83
-    ; 0xae
-    ; 0xf
-    ; 0x89
-    ; 0x85
-    ; 0x85
-    ; 0xda
-    ; 0x4b
-    ; 0x43
-    ; 0xec
-    ; 0x88
-    ; 0xbf
-    ; 0x1
-    ; 0x72
-    ; 0x9a
-    ; 0x6d
-    ; 0xa0
-    ; 0x83
-    ; 0xa5
-    ; 0x2f
-    ; 0x23
-    ; 0x43
-    ; 0x4e
-    ; 0x90
-    ; 0x87
-    ; 0x88
-    ; 0x51
-    ; 0xf0
-    ; 0x8a
-    ; 0x49
-    ; 0x5c
-    ; 0x8c
-    ; 0xb7
-    ; 0x97
-    ; 0x9b
-    ; 0x28
-    ; 0x88
-    ; 0xae
-    ; 0x12
-    ; 0x97
-    ; 0x9d
-    ; 0xc1
-    ; 0x35
+    [
+      0xa9;
+      0xde;
+      0xd6;
+      0x29;
+      0x93;
+      0xfb;
+      0x52;
+      0x61;
+      0xfb;
+      0x59;
+      0xf7;
+      0xd4;
+      0x78;
+      0x42;
+      0xe5;
+      0xa7;
+      0x81;
+      0xf6;
+      0xe;
+      0x48;
+      0xb5;
+      0x83;
+      0xae;
+      0xf;
+      0x89;
+      0x85;
+      0x85;
+      0xda;
+      0x4b;
+      0x43;
+      0xec;
+      0x88;
+      0xbf;
+      0x1;
+      0x72;
+      0x9a;
+      0x6d;
+      0xa0;
+      0x83;
+      0xa5;
+      0x2f;
+      0x23;
+      0x43;
+      0x4e;
+      0x90;
+      0x87;
+      0x88;
+      0x51;
+      0xf0;
+      0x8a;
+      0x49;
+      0x5c;
+      0x8c;
+      0xb7;
+      0x97;
+      0x9b;
+      0x28;
+      0x88;
+      0xae;
+      0x12;
+      0x97;
+      0x9d;
+      0xc1;
+      0x35;
     ];
 
 pubKey : ByteArray :=
   mkByteArray
-    [ 0xbf
-    ; 0x1
-    ; 0x72
-    ; 0x9a
-    ; 0x6d
-    ; 0xa0
-    ; 0x83
-    ; 0xa5
-    ; 0x2f
-    ; 0x23
-    ; 0x43
-    ; 0x4e
-    ; 0x90
-    ; 0x87
-    ; 0x88
-    ; 0x51
-    ; 0xf0
-    ; 0x8a
-    ; 0x49
-    ; 0x5c
-    ; 0x8c
-    ; 0xb7
-    ; 0x97
-    ; 0x9b
-    ; 0x28
-    ; 0x88
-    ; 0xae
-    ; 0x12
-    ; 0x97
-    ; 0x9d
-    ; 0xc1
-    ; 0x35
+    [
+      0xbf;
+      0x1;
+      0x72;
+      0x9a;
+      0x6d;
+      0xa0;
+      0x83;
+      0xa5;
+      0x2f;
+      0x23;
+      0x43;
+      0x4e;
+      0x90;
+      0x87;
+      0x88;
+      0x51;
+      0xf0;
+      0x8a;
+      0x49;
+      0x5c;
+      0x8c;
+      0xb7;
+      0x97;
+      0x9b;
+      0x28;
+      0x88;
+      0xae;
+      0x12;
+      0x97;
+      0x9d;
+      0xc1;
+      0x35;
     ];
+
+main : Bool :=
+  let
+    msg : Nat := 1;
+    sig : ByteArray := anomaSignDetached msg privKey;
+  in trace (byteArrayLength sig)
+    >-> anomaVerifyDetached (anomaSignDetached msg privKey) msg pubKey;

tests/Anoma/Compilation/positive/test078.juvix

@@ -18,11 +18,6 @@ axiom anomaSign : {A : Type} -> A -> ByteArray -> ByteArray;
 builtin anoma-verify-with-message
 axiom anomaVerifyWithMessage : {A : Type} -> ByteArray -> ByteArray -> Maybe A;
 
-main (input : List Nat) : List Nat :=
-  let
-    signedMessage : ByteArray := anomaSign input privKey;
-  in fromMaybe [] <| anomaVerifyWithMessage signedMessage pubKey;
-
 privKey : ByteArray :=
   mkByteArray
     [ 0x24
@@ -126,3 +121,8 @@ pubKey : ByteArray :=
     ; 0xc5
     ; 0xc3
     ];
+
+main (input : List Nat) : List Nat :=
+  let
+    signedMessage : ByteArray := anomaSign input privKey;
+  in fromMaybe [] <| anomaVerifyWithMessage signedMessage pubKey;

tests/Casm/Compilation/positive/test006.juvix

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

tests/Casm/Compilation/positive/test034.juvix

@@ -5,11 +5,9 @@ import Stdlib.Prelude 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/Casm/Compilation/positive/test060.juvix

@@ -29,11 +29,11 @@ main : 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 sum <| ite
     (mf
       mkPair@{

tests/Casm/Compilation/positive/test064.juvix

@@ -29,7 +29,7 @@ odd : Nat -> Bool
   | (suc n) := even n;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
 {-# inline: false #-}
 even' : Nat -> Bool := even;
@@ -38,5 +38,5 @@ main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
         | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
-        | false := f (3 + 4) (f 0 8) + loop
+        | false := f (3 + 4) (f 0 8) + loop 0
       };

tests/Compilation/positive/out/test083.out

@@ -0,0 +1 @@
+13

tests/Compilation/positive/test006.juvix

@@ -4,11 +4,11 @@ module test006;
 import Stdlib.Prelude open;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
 main : IO :=
   printNatLn
-      (ite (3 > 0) 1 loop
-        + ite (2 < 1) loop (ite (7 >= 8) loop 1))
-    >>> printBoolLn (2 > 0 || loop == 0)
-    >>> printBoolLn (2 < 0 && loop == 0);
+      (ite (3 > 0) 1 (loop 0)
+        + ite (2 < 1) (loop 0) (ite (7 >= 8) (loop 0) 1))
+    >>> printBoolLn (2 > 0 || (loop 0) == 0)
+    >>> printBoolLn (2 < 0 && (loop 0) == 0);

tests/Compilation/positive/test034.juvix

@@ -5,11 +5,9 @@ import Stdlib.Prelude 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 : IO :=

tests/Compilation/positive/test052.juvix

@@ -71,6 +71,11 @@ exprToString : Expr -> String
 instance
 showExprI : Show Expr := mkShow exprToString;
 
+--- ;Show; instance for ;Val;.
+terminating
+instance
+showValI : Show Val := mkShow valToString;
+
 terminating
 valToString : Val -> String
   | (vnum n) := natToString n
@@ -79,11 +84,6 @@ valToString : Val -> String
       ++str " ⊢ "
       ++str Show.show n;
 
---- ;Show; instance for ;Val;.
-terminating
-instance
-showValI : Show Val := mkShow valToString;
-
 syntax operator >>= seq;
 --- Monadic binding for ;Either;.
 >>=

tests/Compilation/positive/test060.juvix

@@ -24,8 +24,8 @@ mf : Pair' (Pair' Bool (List Nat)) (List Nat) → Bool
 main : Triple Nat Nat Nat :=
   let
     p : Triple Nat Nat Nat := mkTriple 2 2 2;
-    p' : Triple Nat Nat Nat := p@Triple{fst := fst + 1; snd := snd * 3 + thd + fst};
-    f : Triple Nat Nat Nat -> Triple Nat Nat Nat := (@Triple{fst := fst * 10});
+    p' : Triple Nat Nat Nat := p@Triple{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 := \{p := p@Triple{fst := Triple.fst p * 10}};
     pp :=
       mkPair@{
         fst :=

tests/Compilation/positive/test064.juvix

@@ -29,7 +29,7 @@ odd : Nat -> Bool
   | (suc n) := even n;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
 {-# inline: false #-}
 even' : Nat -> Bool := even;
@@ -38,5 +38,5 @@ main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
         | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
-        | false := f (3 + 4) (f 0 8) + loop
+        | false := f (3 + 4) (f 0 8) + loop 0
       };

tests/Compilation/positive/test083.juvix

@@ -0,0 +1,13 @@
+-- Record update
+module test083;
+
+import Stdlib.Prelude open;
+
+type R := mkR@{
+  x : Nat;
+  y : Nat;
+};
+
+f (r : R) : R := let x := 7 in r@R{x := R.x r + x; y := x};
+
+main : Nat := case f (mkR 1 2) of mkR x y := x + 5;

tests/Internal/Core/positive/test006.juvix

@@ -3,9 +3,9 @@ module test006;
 import Stdlib.Prelude open;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
-e : Nat := (ite (3 > 0) 1 loop) + (ite (2 < 1) loop (ite (7 >= 8) loop 1));
+e : Nat := (ite (3 > 0) 1 (loop 0)) + (ite (2 < 1) (loop 0) (ite (7 >= 8) (loop 0) 1));
 
 main : IO := printNatLn e;
 

tests/Internal/positive/Lambda.juvix

@@ -2,35 +2,20 @@ module Lambda;
 
 import Stdlib.Prelude open public;
 
-id' : {A : Type} → A → A := λ {| a := a};
+id' : {A : Type} → A → A := λ{| a := a};
 
-uncurry'
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (A → B → C)
-    → Pair A B
-    → C := λ {| f (a, b) := f a b};
+uncurry' : {A : Type} → {B : Type} → {C : Type} → (A → B → C) → Pair A B → C :=
+  λ{| f (a, b) := f a b};
 
 fst' : {A : Type} → {B : Type} → Pair A B → A
-  | {_} := λ {| (a, _) := a};
+  | {_} := λ{| (a, _) := a};
 
 first'
-  : {A : Type}
-    → {B : Type}
-    → {A' : Type}
-    → (A → A')
-    → Pair A B
-    → Pair A' B := λ {| f (a, b) := f a, b};
+  : {A : Type} → {B : Type} → {A' : Type} → (A → A') → Pair A B → Pair A' B :=
+  λ{| f (a, b) := f a, b};
 
-foldr'
-  : {A : Type}
-    → {B : Type}
-    → (A → B → B)
-    → B
-    → List A
-    → B :=
-  λ {
+foldr' {A B : Type} : (A → B → B) → B → List A → B :=
+  λ{
     | _ z nil := z
     | f z (h :: hs) := f h (foldr' f z hs)
   };

tests/Rust/Compilation/positive/test006.juvix

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

tests/Rust/Compilation/positive/test034.juvix

@@ -5,11 +5,9 @@ import Stdlib.Prelude 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/Rust/Compilation/positive/test060.juvix

@@ -29,11 +29,11 @@ main : 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 sum <| ite
     (mf
       mkPair@{

tests/Rust/Compilation/positive/test064.juvix

@@ -29,7 +29,7 @@ odd : Nat -> Bool
   | (suc n) := even n;
 
 terminating
-loop : Nat := loop;
+loop (dummy : Nat) : Nat := loop dummy;
 
 {-# inline: false #-}
 even' : Nat -> Bool := even;
@@ -38,5 +38,5 @@ main : Nat :=
   sum 3
     + case even' 6 || g true || h true of {
         | true := ite (g false) (f 1 2 + sum 7 + j 0) 0
-        | false := f (3 + 4) (f 0 8) + loop
+        | false := f (3 + 4) (f 0 8) + loop 0
       };

tests/negative/AppLeftImplicit.juvix

@@ -1,3 +1,3 @@
 module AppLeftImplicit;
 
-x : Type := {x};
+x (dummy : Type) : Type := {x dummy};

tests/negative/Termination/Axiom.juvix

@@ -1,5 +1,5 @@
 module Axiom;
 
 axiom A : let
-            x : Type := x;
+            x (y : Type) : Type := x y;
           in x;

tests/positive/Internal/Lambda.juvix

@@ -43,10 +43,10 @@ idB : {A : Type} → A → A
 
 mapB : {A : Type} → (A → A) → A → A := λ {f a := f a};
 
-add : Nat → Nat → Nat :=
+countDown {A} : Nat → A → A :=
   λ {
     | zero n := n
-    | (suc n) m := add n m
+    | (suc n) m := countDown n m
   };
 
 fst : {A : Type} → {B : Type} → A × B → A
@@ -90,10 +90,8 @@ map : {A : Type} → {B : Type} → (A → B) → List A → List B
 pairEval : {A : Type} → {B : Type} → (A → B) × A → B :=
   λ {(f, x) := f x};
 
-foldr
-  : {A : Type}
-    → {B : Type}
-    → (A → B → B)
+foldr {A B}
+  : (A → B → B)
     → B
     → List A
     → B :=
@@ -102,10 +100,8 @@ foldr
     | f z (h :: hs) := f h (foldr f z hs)
   };
 
-foldl
-  : {A : Type}
-    → {B : Type}
-    → (B → A → B)
+foldl {A B}
+  : (B → A → B)
     → B
     → List A
     → B :=
@@ -124,25 +120,22 @@ ite : {A : Type} → Bool → A → A → A :=
     | false _ b := b
   };
 
-filter : {A : Type} → (A → Bool) → List A → List A :=
+filter {A} : (A → Bool) → List A → List A :=
   λ {
     | _ nil := nil
     | f (h :: hs) := ite (f h) (h :: filter f hs) (filter f hs)
   };
 
-partition
-  : {A : Type} → (A → Bool) → List A → List A × List A :=
+partition {A}
+  : (A → Bool) → List A → List A × List A :=
   λ {
     | _ nil := nil, nil
     | f (x :: xs) :=
       ite (f x) first second ((::) x) (partition f xs)
   };
 
-zipWith
-  : {A : Type}
-    → {B : Type}
-    → {C : Type}
-    → (_ → _ → _)
+zipWith {A B C}
+  : (_ → _ → _)
     → List A
     → List B
     → List C :=

tests/positive/Records2.juvix

@@ -11,4 +11,4 @@ type Pair (A B : Type) :=
 main : Pair Nat Nat :=
   let
     p : Pair Nat Nat := mkPair 2 2;
-  in p@Pair{pfst := pfst + psnd};
+  in p@Pair{pfst := Pair.pfst p + Pair.psnd p};

tests/positive/Termination/Undefined.juvix

@@ -3,4 +3,4 @@ module Undefined;
 axiom A : Type;
 
 terminating
-undefined : A := undefined;
+undefined (dummy : A) : A := undefined dummy;

tests/smoke/Commands/repl.smoke.yaml

@@ -5,7 +5,7 @@ tests:
     command:
       - juvix
       - repl
-    stdin: "let x : Bool := x in x"
+    stdin: "let x (dummy : Bool) : Bool := x dummy in x true"
     stdout:
       matches: |
         .*