[ tests, upstream ] Update tests outputs to the current compiler's ver.

buzden · buzden · commit aae51dae429b · 2026-02-24T15:38:55.000+03:00
diff --git a/deptycheck.ipkg b/deptycheck.ipkg
@@ -9,7 +9,7 @@ license = "MPL-2.0"
 sourcedir = "src"
 builddir = ".build"
 
-version = 0.0.251218
+version = 0.0.260223
 
 modules = Deriving.DepTyCheck.Gen
         , Deriving.DepTyCheck.Gen.ConsRecs
diff --git a/examples/pil-reg/tests/lang/003-usage-negative/expected b/examples/pil-reg/tests/lang/003-usage-negative/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of bad_ass_no_var. Can't find an impleme
 
 Negative:12:3--12:15
  08 | -- Simple tests --
- 09 | 
+ 09 |
  10 | bad_ass_no_var : Statement TestOps vars regs vars regs
  11 | bad_ass_no_var = do
  12 |   "x" #= C' 42
@@ -13,7 +13,7 @@ Negative:12:3--12:15
 Error: While processing right hand side of bad_ass_type_mismatch. Can't find an implementation for FromString Int.
 
 Negative:17:12--17:17
- 13 | 
+ 13 |
  14 | bad_ass_type_mismatch : Statement TestOps vars regs (("x", Int')::vars) regs
  15 | bad_ass_type_mismatch = do
  16 |   Int'. "x"
@@ -55,9 +55,9 @@ and:
 Mismatch between: Type' and ?b -> ?c.
 
 Negative:35:19--35:23
- 31 | 
+ 31 |
  32 | --- Example statements ---
- 33 | 
+ 33 |
  34 | bad_for : Statement TestOps vars regs vars regs
  35 | bad_for = for (do Int'. "x" #= C 0; Int'. "y" #= C 0)
                         ^^^^
@@ -66,7 +66,7 @@ Error: While processing right hand side of bad_read_reg_base. Can't find an impl
 
 Negative:44:17--44:20
  40 | -- Registers-related --
- 41 | 
+ 41 |
  42 | bad_read_reg_base : Statement TestOps vars (Base [Nothing, Nothing, Just Int', Nothing]) vars (Base [Nothing, Nothing, Just Int', Nothing])
  43 | bad_read_reg_base = block $ do
  44 |   Int'. "x" !#= R 1
@@ -75,7 +75,7 @@ Negative:44:17--44:20
 Error: While processing right hand side of bad_read_reg_undef_with. Can't find an implementation for IsJust (index (natToFinLT 2) (With AllUndefined (FS (FS (FS FZ)), Just Int'))).
 
 Negative:49:17--49:20
- 45 | 
+ 45 |
  46 | bad_read_reg_undef_with : Statement TestOps vars (AllUndefined {rc=4} `With` (3, Just Int'))
  47 |                                     vars (AllUndefined {rc=4} `With` (3, Just Int'))
  48 | bad_read_reg_undef_with = block $ do
@@ -86,7 +86,7 @@ Error: While processing right hand side of bad_read_reg_with. Can't find an impl
 
 Negative:53:17--53:20
  49 |   Int'. "x" !#= R 2
- 50 | 
+ 50 |
  51 | bad_read_reg_with : {0 regs : Registers 5} -> Statement TestOps vars (regs `With` (3, Just Int')) vars (regs `With` (3, Just Int'))
  52 | bad_read_reg_with = block $ do
  53 |   Int'. "x" !#= R 2 + C 0
@@ -100,7 +100,7 @@ Mismatch between: FS (natToFinLT 2) and FZ.
 
 Negative:57:3--57:20
  53 |   Int'. "x" !#= R 2 + C 0
- 54 | 
+ 54 |
  55 | bad_registers_ass : {0 regs : Registers 5} -> Statement TestOps vars regs vars $ regs `With` (3, Just Int')
  56 | bad_registers_ass = block $ do
  57 |   Int'. "x" !#= C 0
@@ -110,7 +110,7 @@ Error: While processing right hand side of bad_registers_infer_nothing. Can't fi
 
 Negative:62:11--62:14
  58 |   6 %= V "x"
- 59 | 
+ 59 |
  60 | bad_registers_infer_nothing : Statement TestOps vars (AllUndefined {rc=4}) vars (AllUndefined {rc=4})
  61 | bad_registers_infer_nothing = block $ do
  62 |   "x" ?#= R 0
@@ -119,7 +119,7 @@ Negative:62:11--62:14
 Error: While processing right hand side of bad_if_access_local. Can't find an implementation for Lookup (MkName "x") ((Int' . MkName "y") :: vars).
 
 Negative:69:17--69:22
- 65 | 
+ 65 |
  66 | bad_if_access_local : {cond : Expression TestOps vars regs Bool'} -> Statement TestOps vars regs vars $ regs `Merge` regs
  67 | bad_if_access_local = block $ do
  68 |   if__ cond (Int'. "x" !#= C 1) (Int'. "x" !#= C 2)
diff --git a/tests/derivation/core/non-cons given match 001-neg/expected b/tests/derivation/core/non-cons given match 001-neg/expected
@@ -3,7 +3,7 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Argument #0 of DerivedGen.X2 with given type arguments [0] is not supported, argument expression: DerivedGen.boolToNat x, reason: name `DerivedGen.boolToNat` is not a constructor
 
 DerivedGen:1
- 12 | 
+ 12 |
  13 | data X : Nat -> Type where
  14 |   X0 : X 0
  15 |   X1 : Bool -> X 1
diff --git a/tests/derivation/core/norec nodep noext 003-neg/expected b/tests/derivation/core/norec nodep noext 003-neg/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  12 | XShow : Show X
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | checkedGen : Fuel -> Gen MaybeEmpty X
  16 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec nodep noext 004-neg/expected b/tests/derivation/core/norec nodep noext 004-neg/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  12 | XShow : Show X
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | checkedGen : Fuel -> Gen MaybeEmpty X
  16 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec nodep noext 005-neg/expected b/tests/derivation/core/norec nodep noext 005-neg/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  12 | XShow : Show X
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | checkedGen : Fuel -> Gen MaybeEmpty X
  16 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec part noext 001-neg/expected b/tests/derivation/core/norec part noext 001-neg/expected
@@ -4,9 +4,9 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  5 | %default total
- 6 | 
+ 6 |
  7 | %language ElabReflection
- 8 | 
+ 8 |
  9 | checkedGen : Fuel -> Gen MaybeEmpty (Maybe Bool)
                                                 ^^^^
 
diff --git a/tests/derivation/core/norec part noext 002-neg/expected b/tests/derivation/core/norec part noext 002-neg/expected
@@ -4,9 +4,9 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  5 | %default total
- 6 | 
+ 6 |
  7 | %language ElabReflection
- 8 | 
+ 8 |
  9 | checkedGen : Fuel -> Gen MaybeEmpty (Bool, Bool)
                                           ^^^^
 
diff --git a/tests/derivation/core/norec part noext 003/expected b/tests/derivation/core/norec part noext 003/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  12 | XShow : Show X
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | checkedGen : Fuel -> Gen MaybeEmpty X
  16 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec part noext 004/expected b/tests/derivation/core/norec part noext 004/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | export
  16 | checkedGen : Fuel -> Gen MaybeEmpty X
  17 | checkedGen = deriveGen
diff --git a/tests/derivation/core/norec part noext 005/expected b/tests/derivation/core/norec part noext 005/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | export
  16 | checkedGen : Fuel -> Gen MaybeEmpty X
  17 | checkedGen = deriveGen
diff --git a/tests/derivation/core/norec part w_ext 001/expected b/tests/derivation/core/norec part w_ext 001/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | export
  16 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty X
  17 | checkedGen = deriveGen
diff --git a/tests/derivation/core/norec part w_ext 002/expected b/tests/derivation/core/norec part w_ext 002/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | export
  16 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty X
  17 | checkedGen = deriveGen
diff --git a/tests/derivation/core/norec part w_ext 003/expected b/tests/derivation/core/norec part w_ext 003/expected
@@ -4,7 +4,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  13 | XShow = %runElab derive
- 14 | 
+ 14 |
  15 | export
  16 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty X
  17 | checkedGen = deriveGen
diff --git a/tests/derivation/core/norec part w_ext 004-neg/expected b/tests/derivation/core/norec part w_ext 004-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | export
  10 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => Gen MaybeEmpty (Maybe String)
                                                                                     ^^^^^^
diff --git a/tests/derivation/core/norec part w_ext 005-neg/expected b/tests/derivation/core/norec part w_ext 005-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | export
  10 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty (String, Nat)
                                                                                                               ^^^^^^
diff --git a/tests/derivation/core/norec part w_ext 006-neg/expected b/tests/derivation/core/norec part w_ext 006-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `String`
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | export
  10 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty String) => (Fuel -> Gen MaybeEmpty Nat) => Gen MaybeEmpty (String, Nat, String)
                                                                                                               ^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 001/expected b/tests/derivation/core/norec t-p.--.. w_ext 001/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (Maybe a)
  10 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 002/expected b/tests/derivation/core/norec t-p.--.. w_ext 002/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty b) => (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, b)
  10 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected b/tests/derivation/core/norec t-p.--.. w_ext 003-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (a, a)
  10 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected b/tests/derivation/core/norec t-p.--.. w_ext 004-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => (Fuel -> Gen MaybeEmpty b) => Gen MaybeEmpty (a, b, a)
  10 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 005/expected b/tests/derivation/core/norec t-p.--.. w_ext 005/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  11 | Show a => Show (X a) where
  12 |   show (MkX m) = "MkX \{show m}"
- 13 | 
+ 13 |
  14 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => Gen MaybeEmpty (X a)
  15 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-p.--.. w_ext 006/expected b/tests/derivation/core/norec t-p.--.. w_ext 006/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  11 | Show a => Show b => Show (X a b) where
  12 |   show (MkX m) = "MkX \{show m}"
- 13 | 
+ 13 |
  14 | checkedGen : Fuel -> (Fuel -> Gen MaybeEmpty a) => (Fuel -> Gen MaybeEmpty b) => Gen MaybeEmpty (X a b)
  15 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/norec t-pi--.. noext 001/expected b/tests/derivation/core/norec t-pi--.. noext 001/expected
@@ -4,9 +4,9 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 
 DerivedGen:1
  5 | %default total
- 6 | 
+ 6 |
  7 | %language ElabReflection
- 8 | 
+ 8 |
  9 | checkedGen : Fuel -> (a, b : Bool) -> Gen MaybeEmpty (a = b)
                                   ^^^^
 
diff --git a/tests/derivation/core/norec t-pi--.. noext 002/expected b/tests/derivation/core/norec t-pi--.. noext 002/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Target type's argument must be a variable name, got `Prelude.Types.Nat`
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | export
  10 | checkedGen : Fuel -> (a, b : Nat) -> Gen MaybeEmpty (a = b)
                                    ^^^
diff --git a/tests/derivation/core/norec t-pi--.. noext 003/expected b/tests/derivation/core/norec t-pi--.. noext 003/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  13 | Show (X b1 b2) where
  14 |   show (MkX b1 b2 _) = "MkX \{show b1} \{show b2} Refl"
- 15 | 
+ 15 |
  16 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
  17 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec t-pi--.. noext 004/expected b/tests/derivation/core/norec t-pi--.. noext 004/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  15 |   show (X0 b1 b2 _) = "X0 \{show b1} \{show b2} Refl"
  16 |   show X1           = "X1"
- 17 | 
+ 17 |
  18 | checkedGen : Fuel -> (b1 : Bool) -> (b2 : Bool) -> Gen MaybeEmpty (X b1 b2)
  19 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/norec t-pi--.. w_ext 002/expected b/tests/derivation/core/norec t-pi--.. w_ext 002/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: Name `a` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); did you forget to add one?
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : DecEq a => Fuel -> (x, y : a) -> Gen MaybeEmpty (x = y)
  10 | checkedGen = deriveGen
       ^^^^^^^^^^^^^^^^^^^^^^
diff --git a/tests/derivation/core/trivial 002-neg/expected b/tests/derivation/core/trivial 002-neg/expected
@@ -3,9 +3,9 @@
 Error: While processing right hand side of checkedGen. Error during reflection: No constructors found for the type `Builtin.Void`
 
 DerivedGen:1
- 06 | 
+ 06 |
  07 | %language ElabReflection
- 08 | 
+ 08 |
  09 | checkedGen : Fuel -> Gen MaybeEmpty Void
  10 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/trivial 003-neg/expected b/tests/derivation/core/trivial 003-neg/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  09 | Show (x ** Gen MaybeEmpty x) where
  10 |   show _ = "a generator"
- 11 | 
+ 11 |
  12 | checkedGen : Fuel -> (em : _) -> Gen MaybeEmpty (a ** Gen em a)
  13 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/trivial 004-neg/expected b/tests/derivation/core/trivial 004-neg/expected
@@ -5,7 +5,7 @@ Error: While processing right hand side of checkedGen. Error during reflection:
 DerivedGen:1
  09 | Show (Gen em x) where
  10 |   show _ = "a generator"
- 11 | 
+ 11 |
  12 | checkedGen : Fuel -> (em : _) -> (a : Type) -> Gen MaybeEmpty $ Gen em a
  13 | checkedGen = deriveGen
                    ^^^^^^^^^
diff --git a/tests/derivation/core/typealias con 003-neg/expected b/tests/derivation/core/typealias con 003-neg/expected
diff --git a/tests/derivation/inputvalidation/bad-args-in-target-type/expected b/tests/derivation/inputvalidation/bad-args-in-target-type/expected
diff --git a/tests/derivation/inputvalidation/bad-fuel/expected b/tests/derivation/inputvalidation/bad-fuel/expected
diff --git a/tests/derivation/inputvalidation/bad-param-names/expected b/tests/derivation/inputvalidation/bad-param-names/expected
diff --git a/tests/derivation/inputvalidation/external-gens/expected b/tests/derivation/inputvalidation/external-gens/expected
diff --git a/tests/derivation/inputvalidation/non-gen-target-type/expected b/tests/derivation/inputvalidation/non-gen-target-type/expected
diff --git a/tests/derivation/inputvalidation/odd-or-lacking-gen-params/expected b/tests/derivation/inputvalidation/odd-or-lacking-gen-params/expected
diff --git a/tests/derivation/inputvalidation/params-before-fuel/expected b/tests/derivation/inputvalidation/params-before-fuel/expected
diff --git a/tests/derivation/inputvalidation/unexpected-gen-target/expected b/tests/derivation/inputvalidation/unexpected-gen-target/expected
diff --git a/tests/derivation/inputvalidation/unexpected-multiplicity/expected b/tests/derivation/inputvalidation/unexpected-multiplicity/expected
diff --git a/tests/derivation/inputvalidation/wrong-params-order/expected b/tests/derivation/inputvalidation/wrong-params-order/expected
diff --git a/tests/derivation/least-effort/run/regression/function-in-cons/expected b/tests/derivation/least-effort/run/regression/function-in-cons/expected
