Skip to content

Commit

Permalink
[ bump ] Use newer compiler and pack collection
Browse files Browse the repository at this point in the history
  • Loading branch information
@buzden
buzden committed Jul 24, 2023
1 parent 5f3eaf3 commit 7ba020f
Show file tree
Hide file tree
Showing 18 changed files with 40 additions and 40 deletions.
2 changes: 1 addition & 1 deletion .pack-collection
View file
Original file line number Diff line number Diff line change
@@ -1 +1 @@
nightly-230320
nightly-230723
4 changes: 2 additions & 2 deletions pack.toml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,12 +2,12 @@
### Settings ###
################

collection = "nightly-230515"
collection = "nightly-230723"

[idris2]
url = "https://github.com/buzden/Idris2"
version = "0.6.0"
commit = "5e9ae63d95d690c19c6aa7564939f9dec24872cb"
commit = "6732126043a8c01f914026a3b4239151d4f0c604"

[install]
whitelist = [ "deptycheck-tests", "pil-tests", "deptycheck-docs" ]
Expand Down
10 changes: 5 additions & 5 deletions tests/gen-derivation/cons-analysis/deep-cons-app-006/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ LOG gen.auto.deep-cons-app:0: ------------------------
LOG gen.auto.deep-cons-app:0: applied names: []
LOG gen.auto.deep-cons-app:0: bind expression: Nat
LOG gen.auto.deep-cons-app:0:
LOG gen.auto.deep-cons-app:0: given free names: [{arg:647}]
LOG gen.auto.deep-cons-app:0: given free names: [{arg:651}]
LOG gen.auto.deep-cons-app:0: original expression: Nat
LOG gen.auto.deep-cons-app:0: ------------------------
LOG gen.auto.deep-cons-app:0: applied names: []
Expand All @@ -25,16 +25,16 @@ LOG gen.auto.deep-cons-app:0: ------------------------
LOG gen.auto.deep-cons-app:0: applied names: [len, elem]
LOG gen.auto.deep-cons-app:0: bind expression: Vect (S len0) elem1
LOG gen.auto.deep-cons-app:0:
LOG gen.auto.deep-cons-app:0: given free names: [{a:2985}]
LOG gen.auto.deep-cons-app:0: given free names: [{a:2982}]
LOG gen.auto.deep-cons-app:0: original expression: Split []
LOG gen.auto.deep-cons-app:0: ------------------------
LOG gen.auto.deep-cons-app:0: applied names: [{a:2985}, {a:2985}]
LOG gen.auto.deep-cons-app:0: applied names: [{a:2982}, {a:2982}]
LOG gen.auto.deep-cons-app:0: bind expression: Split []
LOG gen.auto.deep-cons-app:0:
LOG gen.auto.deep-cons-app:0: given free names: [{a:2995}, x]
LOG gen.auto.deep-cons-app:0: given free names: [{a:2992}, x]
LOG gen.auto.deep-cons-app:0: original expression: Split [x]
LOG gen.auto.deep-cons-app:0: ------------------------
LOG gen.auto.deep-cons-app:0: applied names: [{a:2995}, {a:2995}, x, {a:2995}]
LOG gen.auto.deep-cons-app:0: applied names: [{a:2992}, {a:2992}, x, {a:2992}]
LOG gen.auto.deep-cons-app:0: bind expression: Split [x2]
LOG gen.auto.deep-cons-app:0:
LOG gen.auto.deep-cons-app:0: given free names: [a, n, m, x, xs, y, ys]
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/003 noparam/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -69,10 +69,10 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/004 noparam/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -77,13 +77,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (ICase (IVar ^fuel_arg^)
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/006 param/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,13 +81,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/007 right-to-left simple/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,13 +89,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/008 right-to-left simple/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -89,13 +89,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/009 left-to-right/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -87,13 +87,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[0]
[ PatClause (IApp. IVar <DerivedGen.X>[0]
$ IBindVar ^fuel_arg^
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -93,13 +93,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,13 +101,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <Builtin.Unit>[]
[ PatClause (IApp. IVar <Builtin.Unit>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<Builtin.MkUnit>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/012 right-to-left chained/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -101,13 +101,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X1>[]
[ PatClause (IApp. IVar <DerivedGen.X1>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX1>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/adt/013 right-to-left nondet/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -107,13 +107,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
(IApp. IVar >>=
$ (IApp. IVar <Prelude.Types.Nat>[]
$ IVar ^cons_fuel^)
$ (ILam. (MW ExplicitArg ^bnd^{arg:647} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. IVar Prelude.Types.S
$ IVar ^bnd^{arg:647})))) ] ]
$ IVar ^bnd^{arg:651})))) ] ]
IDef <DerivedGen.X>[]
[ PatClause (IApp. IVar <DerivedGen.X>[] $ IBindVar ^fuel_arg^)
(ILocal (IApp. IVar <<DerivedGen.MkX>>
Expand Down
4 changes: 2 additions & 2 deletions tests/gen-derivation/derivation/least-effort/print/gadt/001 gadt/expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -92,15 +92,15 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel)
$ (IApp. IVar <Data.Fin.Fin>[0]
$ IVar ^cons_fuel^
$ IVar k)
$ (ILam. (MW ExplicitArg ^bnd^{arg:3101} : Implicit False)
$ (ILam. (MW ExplicitArg ^bnd^{arg:3095} : Implicit False)
=> (IApp. INamedApp (IVar Prelude.pure)
f
(IApp. IVar Test.DepTyCheck.Gen.Gen
$ Implicit True)
$ (IApp. INamedApp (IVar Data.Fin.FS)
k
(IVar k)
$ IVar ^bnd^{arg:3101}))))
$ IVar ^bnd^{arg:3095}))))
, PatClause (IApp. IVar <<Data.Fin.FS>>
$ Implicit True
$ Implicit True)
Expand Down
Loading

0 comments on commit 7ba020f

Please sign in to comment.