diff --git a/.pack-collection b/.pack-collection index 649719141..76a220220 100644 --- a/.pack-collection +++ b/.pack-collection @@ -1 +1 @@ -nightly-230320 +nightly-230723 diff --git a/pack.toml b/pack.toml index aee876729..37259fcb1 100644 --- a/pack.toml +++ b/pack.toml @@ -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" ] diff --git a/tests/gen-derivation/cons-analysis/deep-cons-app-006/expected b/tests/gen-derivation/cons-analysis/deep-cons-app-006/expected index 0f17272f3..a93e2d635 100644 --- a/tests/gen-derivation/cons-analysis/deep-cons-app-006/expected +++ b/tests/gen-derivation/cons-analysis/deep-cons-app-006/expected @@ -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: [] @@ -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] diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/003 noparam/expected b/tests/gen-derivation/derivation/least-effort/print/adt/003 noparam/expected index 1cbd75116..ae5ad081f 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/003 noparam/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/003 noparam/expected @@ -69,10 +69,10 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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})))) ] ] diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/004 noparam/expected b/tests/gen-derivation/derivation/least-effort/print/adt/004 noparam/expected index e770bf682..28231cf0d 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/004 noparam/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/004 noparam/expected @@ -77,13 +77,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/006 param/expected b/tests/gen-derivation/derivation/least-effort/print/adt/006 param/expected index ff50bfa9e..810ee32d8 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/006 param/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/006 param/expected @@ -81,13 +81,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/007 right-to-left simple/expected b/tests/gen-derivation/derivation/least-effort/print/adt/007 right-to-left simple/expected index 89b857a53..25ce31afe 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/007 right-to-left simple/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/007 right-to-left simple/expected @@ -89,13 +89,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/008 right-to-left simple/expected b/tests/gen-derivation/derivation/least-effort/print/adt/008 right-to-left simple/expected index 202bf0c57..06b94def6 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/008 right-to-left simple/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/008 right-to-left simple/expected @@ -89,13 +89,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/009 left-to-right/expected b/tests/gen-derivation/derivation/least-effort/print/adt/009 left-to-right/expected index 7a27afc58..2c2ab7198 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/009 left-to-right/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/009 left-to-right/expected @@ -87,13 +87,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [0] [ PatClause (IApp. IVar [0] $ IBindVar ^fuel_arg^ diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected b/tests/gen-derivation/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected index 122156dcb..459882ae0 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected @@ -93,13 +93,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected b/tests/gen-derivation/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected index 8df000dd2..503419714 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected @@ -101,13 +101,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/012 right-to-left chained/expected b/tests/gen-derivation/derivation/least-effort/print/adt/012 right-to-left chained/expected index 605edef73..9b5729c5e 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/012 right-to-left chained/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/012 right-to-left chained/expected @@ -101,13 +101,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/adt/013 right-to-left nondet/expected b/tests/gen-derivation/derivation/least-effort/print/adt/013 right-to-left nondet/expected index 58dc0f3b1..a1bcb815f 100644 --- a/tests/gen-derivation/derivation/least-effort/print/adt/013 right-to-left nondet/expected +++ b/tests/gen-derivation/derivation/least-effort/print/adt/013 right-to-left nondet/expected @@ -107,13 +107,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> diff --git a/tests/gen-derivation/derivation/least-effort/print/gadt/001 gadt/expected b/tests/gen-derivation/derivation/least-effort/print/gadt/001 gadt/expected index 26a2c473f..02d2297e9 100644 --- a/tests/gen-derivation/derivation/least-effort/print/gadt/001 gadt/expected +++ b/tests/gen-derivation/derivation/least-effort/print/gadt/001 gadt/expected @@ -92,7 +92,7 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (IApp. IVar [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 @@ -100,7 +100,7 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (IApp. INamedApp (IVar Data.Fin.FS) k (IVar k) - $ IVar ^bnd^{arg:3101})))) + $ IVar ^bnd^{arg:3095})))) , PatClause (IApp. IVar <> $ Implicit True $ Implicit True) diff --git a/tests/gen-derivation/derivation/least-effort/print/gadt/002 gadt/expected b/tests/gen-derivation/derivation/least-effort/print/gadt/002 gadt/expected index d26304659..2bf8dd29b 100644 --- a/tests/gen-derivation/derivation/least-effort/print/gadt/002 gadt/expected +++ b/tests/gen-derivation/derivation/least-effort/print/gadt/002 gadt/expected @@ -81,13 +81,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) @@ -164,7 +164,7 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (Implicit False) [ PatClause (IApp. IVar Builtin.DPair.MkDPair $ IBindVar k - $ IBindVar ^bnd^{arg:3101}) + $ IBindVar ^bnd^{arg:3095}) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen @@ -174,4 +174,4 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (IApp. INamedApp (IVar Data.Fin.FS) k (IVar k) - $ IVar ^bnd^{arg:3101}))) ])) ] ] + $ IVar ^bnd^{arg:3095}))) ])) ] ] diff --git a/tests/gen-derivation/derivation/least-effort/print/gadt/003 right-to-left nondet/expected b/tests/gen-derivation/derivation/least-effort/print/gadt/003 right-to-left nondet/expected index 0c47567d2..f45dd6b5f 100644 --- a/tests/gen-derivation/derivation/least-effort/print/gadt/003 right-to-left nondet/expected +++ b/tests/gen-derivation/derivation/least-effort/print/gadt/003 right-to-left nondet/expected @@ -121,13 +121,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) diff --git a/tests/gen-derivation/derivation/least-effort/print/gadt/004 right-to-left det/expected b/tests/gen-derivation/derivation/least-effort/print/gadt/004 right-to-left det/expected index eb09e97d4..9f75e66b8 100644 --- a/tests/gen-derivation/derivation/least-effort/print/gadt/004 right-to-left det/expected +++ b/tests/gen-derivation/derivation/least-effort/print/gadt/004 right-to-left det/expected @@ -137,13 +137,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) diff --git a/tests/gen-derivation/derivation/least-effort/print/gadt/007 eq-n/expected b/tests/gen-derivation/derivation/least-effort/print/gadt/007 eq-n/expected index 164a78c4d..dbe3f133e 100644 --- a/tests/gen-derivation/derivation/least-effort/print/gadt/007 eq-n/expected +++ b/tests/gen-derivation/derivation/least-effort/print/gadt/007 eq-n/expected @@ -85,13 +85,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IApp. IVar >>= $ (IApp. IVar [] $ 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 [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^)