From 5d3a4ba091dd2a69f769f9a63fa72b2964d1088d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 13 Sep 2023 21:41:00 +0300 Subject: [PATCH] [ test ] Fix print golden values --- tests/derivation/infra/ext print 004/expected | 24 +- .../print/adt/004 noparam/expected | 112 ++-- .../least-effort/print/adt/006 param/expected | 80 +-- .../adt/007 right-to-left simple/expected | 136 ++-- .../adt/008 right-to-left simple/expected | 136 ++-- .../print/adt/009 left-to-right/expected | 136 ++-- .../adt/010 right-to-left long-dpair/expected | 168 ++--- .../adt/011 right-to-left long-dpair/expected | 224 +++---- .../adt/012 right-to-left chained/expected | 224 +++---- .../adt/013 right-to-left nondet/expected | 276 ++++----- .../adt/014 right-to-left nondet ext/expected | 166 ++--- .../least-effort/print/gadt/002 gadt/expected | 142 ++--- .../gadt/003 right-to-left nondet/expected | 464 +++++++------- .../print/gadt/004 right-to-left det/expected | 586 +++++++++--------- .../least-effort/print/gadt/005 gadt/expected | 112 ++-- .../least-effort/print/gadt/006 gadt/expected | 396 ++++++------ .../least-effort/print/gadt/007 eq-n/expected | 94 +-- 17 files changed, 1738 insertions(+), 1738 deletions(-) diff --git a/tests/derivation/infra/ext print 004/expected b/tests/derivation/infra/ext print 004/expected index 882a9220c..afb7da299 100644 --- a/tests/derivation/infra/ext print 004/expected +++ b/tests/derivation/infra/ext print 004/expected @@ -15,23 +15,25 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [0] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ (IApp. IVar AlternativeCore.X'S + $ IVar {arg:5277})))) IClaim MW Export [] - (MkTy [0] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:5277} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar AlternativeCore.X'S - $ IVar {arg:5277})))) - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar fuel) + $ IVar Prelude.Types.Nat))) + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar fuel + $ Implicit True) (IApp. IVar <*> $ (IApp. IVar <$> $ IVar MkXSN @@ -39,10 +41,8 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ IVar ^outmost-fuel^)) $ (IApp. IVar [] $ IVar fuel)) ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar fuel - $ Implicit True) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar fuel) (IApp. IVar <*> $ (IApp. IVar <$> $ IVar MkXSN diff --git a/tests/derivation/least-effort/print/adt/004 noparam/expected b/tests/derivation/least-effort/print/adt/004 noparam/expected index 28231cf0d..02a140370 100644 --- a/tests/derivation/least-effort/print/adt/004 noparam/expected +++ b/tests/derivation/least-effort/print/adt/004 noparam/expected @@ -8,146 +8,146 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.X))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.X))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) (IVar Data.Fuel.Fuel) [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> + (IApp. IVar <> $ IVar Data.Fuel.Dry) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) description (IApp. IVar Just - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ IPrimVal DerivedGen.X[] (spend fuel)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> + $ (IApp. IVar <> $ IVar ^fuel_arg^)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> + $ (IApp. IVar <> $ IVar ^sub^fuel_arg^)) $ IVar Nil))) ])) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.X))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.X))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ IVar Prelude.Types.Z) ] - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.E) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] + $ (IApp. IVar [] $ IVar ^cons_fuel^) - $ (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:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + $ (ILam. (MW ExplicitArg ^bnd^{arg:3633} : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar DerivedGen.R + $ IVar ^bnd^{arg:3633} + $ IVar ^bnd^{arg:3636})))))) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) (IVar Data.Fuel.Fuel) [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> + (IApp. IVar <> $ IVar Data.Fuel.Dry) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) description (IApp. IVar Just - $ IPrimVal DerivedGen.X[] (spend fuel)) + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> + $ (IApp. IVar <> $ IVar ^fuel_arg^)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> + $ (IApp. IVar <> $ IVar ^sub^fuel_arg^)) $ IVar Nil))) ])) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.X))) + $ IVar Prelude.Types.Nat))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.X))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar Prelude.Types.Nat))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ IVar DerivedGen.E) ] - IDef <> - [ PatClause (IApp. IVar <> + $ IVar Prelude.Types.Z) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] + $ (IApp. IVar [] $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3633} : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar DerivedGen.R - $ IVar ^bnd^{arg:3633} - $ IVar ^bnd^{arg:3636})))))) ] ] + $ (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:651})))) ] ] diff --git a/tests/derivation/least-effort/print/adt/006 param/expected b/tests/derivation/least-effort/print/adt/006 param/expected index 810ee32d8..91a010af7 100644 --- a/tests/derivation/least-effort/print/adt/006 param/expected +++ b/tests/derivation/least-effort/print/adt/006 param/expected @@ -5,14 +5,6 @@ LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** X LOG gen.auto.derive.infra:0: ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) => ILocal (IApp. IVar [] $ IVar ^outmost-fuel^) - IClaim MW - Export - [] - (MkTy [] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) IClaim MW Export [] @@ -25,6 +17,46 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) => (IApp. IVar DerivedGen.X $ IVar {arg:3630})))))) + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkX) + n + (IVar n))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -88,35 +120,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkX) - n - (IVar n))))) ] ] diff --git a/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected b/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected index 25ce31afe..249469eca 100644 --- a/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected +++ b/tests/derivation/least-effort/print/adt/007 right-to-left simple/expected @@ -8,11 +8,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -28,11 +28,75 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ IBindVar ^bnd^{arg:3642}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (IVar DerivedGen.MkY) + n + (IVar n) + $ IVar ^bnd^{arg:3642})) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkX) + n + (IVar n))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -96,67 +160,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkX) - n - (IVar n))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ IBindVar ^bnd^{arg:3642}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.MkY) - n - (IVar n) - $ IVar ^bnd^{arg:3642})) ])) ] ] diff --git a/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected b/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected index 06b94def6..d2a677abe 100644 --- a/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected +++ b/tests/derivation/least-effort/print/adt/008 right-to-left simple/expected @@ -8,11 +8,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -28,11 +28,75 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ IBindVar ^bnd^{arg:3643}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (IVar DerivedGen.MkY) + n + (IVar n) + $ IVar ^bnd^{arg:3643})) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkX) + n + (IVar n))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -96,67 +160,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkX) - n - (IVar n))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ IBindVar ^bnd^{arg:3643}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.MkY) - n - (IVar n) - $ IVar ^bnd^{arg:3643})) ])) ] ] diff --git a/tests/derivation/least-effort/print/adt/009 left-to-right/expected b/tests/derivation/least-effort/print/adt/009 left-to-right/expected index 2c2ab7198..c93a0a8e4 100644 --- a/tests/derivation/least-effort/print/adt/009 left-to-right/expected +++ b/tests/derivation/least-effort/print/adt/009 left-to-right/expected @@ -8,11 +8,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -26,11 +26,75 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ (IApp. IVar Prelude.Types.mult + $ IVar n + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ IVar Prelude.Types.Z)))) + $ (ILam. (MW ExplicitArg ^bnd^{arg:3646} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (IVar DerivedGen.MkY) + n + (IVar n) + $ IVar ^bnd^{arg:3646})))))) ] ] + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3630}>) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar DerivedGen.X + $ IVar {arg:3630})))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^ + $ IBindVar n) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ INamedApp (IVar DerivedGen.MkX) + n + (IVar n)) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -94,67 +158,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3630}>) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.X - $ IVar {arg:3630})))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IBindVar n) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ INamedApp (IVar DerivedGen.MkX) - n - (IVar n)) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ (IApp. IVar Prelude.Types.mult - $ IVar n - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ IVar Prelude.Types.Z)))) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3646} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.MkY) - n - (IVar n) - $ IVar ^bnd^{arg:3646})))))) ] ] diff --git a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected index 459882ae0..1c12f3022 100644 --- a/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/010 right-to-left long-dpair/expected @@ -8,11 +8,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -32,11 +32,91 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3651})) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (IVar DerivedGen.MkY) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3651})) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (INamedApp (IVar DerivedGen.MkX) + n + (IVar n)) + m + (IVar m)))))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -100,83 +180,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (INamedApp (IVar DerivedGen.MkX) - n - (IVar n)) - m - (IVar m)))))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3651})) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (IVar DerivedGen.MkY) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3651})) ])) ] ] diff --git a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected index 503419714..a9825cb64 100644 --- a/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected +++ b/tests/derivation/least-effort/print/adt/011 right-to-left long-dpair/expected @@ -8,19 +8,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IClaim MW - Export - [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Builtin.Unit))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -40,11 +32,119 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Builtin.Unit))) + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3651})) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (IVar DerivedGen.MkY) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3651})) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Builtin.Unit + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Builtin.Unit) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (INamedApp (IVar DerivedGen.MkX) + n + (IVar n)) + m + (IVar m)))))))) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Builtin.Unit))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Builtin.MkUnit) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -108,103 +208,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Builtin.Unit))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Builtin.MkUnit) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Builtin.Unit - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Builtin.Unit) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (INamedApp (IVar DerivedGen.MkX) - n - (IVar n)) - m - (IVar m)))))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3651})) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (IVar DerivedGen.MkY) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3651})) ])) ] ] diff --git a/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected b/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected index 9b5729c5e..68579cd87 100644 --- a/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected +++ b/tests/derivation/least-effort/print/adt/012 right-to-left chained/expected @@ -8,43 +8,143 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X1 - $ IVar {arg:3630})))))) + $ (ILam. (MW ExplicitArg {arg:3641} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X2 + $ IVar {arg:3641})))))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3641} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X2 - $ IVar {arg:3641})))))) + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X1 + $ IVar {arg:3630})))))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ IBindVar ^bnd^{arg:3658}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (IVar DerivedGen.MkY) + n + (IVar n) + $ IVar ^bnd^{arg:3658})) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3641} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X2 + $ IVar {arg:3641})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ IBindVar ^bnd^{arg:3650}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.MkX2 + $ IVar n + $ IVar ^bnd^{arg:3650}))) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X1 + $ IVar {arg:3630})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.MkX1 + $ IVar n))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -108,103 +208,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X1 - $ IVar {arg:3630})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.MkX1 - $ IVar n))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3641} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X2 - $ IVar {arg:3641})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ IBindVar ^bnd^{arg:3650}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.MkX2 - $ IVar n - $ IVar ^bnd^{arg:3650}))) ])) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ IBindVar ^bnd^{arg:3658}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.MkY) - n - (IVar n) - $ IVar ^bnd^{arg:3658})) ])) ] ] diff --git a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected index a1bcb815f..cb25695c9 100644 --- a/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/adt/013 right-to-left nondet/expected @@ -8,112 +8,138 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy [] + (MkTy [0] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IClaim MW Export [] - (MkTy [0] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (ICase (IVar ^fuel_arg^) - (IVar Data.Fuel.Fuel) - [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> - $ IVar Data.Fuel.Dry) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) - description - (IApp. IVar Just - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> - $ IVar ^fuel_arg^)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth - $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) - $ IVar Nil))) ])) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ IBindVar ^bnd^{arg:3654})) + (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ IVar n) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3651}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3651} + $ IVar ^bnd^{arg:3654})) ])) ])) ] ] + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3630}>) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>)) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z) ] - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^ + $ IBindVar n) (IApp. IVar >>= $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:651} : Implicit False) + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) => (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:651})))) ] ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (INamedApp (IVar DerivedGen.MkX) + n + (IVar n)) + m + (IVar m))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> @@ -158,92 +184,66 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IVar n)) m (IVar m)))))))) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3630}>) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>)) + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (ICase (IVar ^fuel_arg^) + (IVar Data.Fuel.Fuel) + [ PatClause (IVar Data.Fuel.Dry) + (IApp. IVar <> + $ IVar Data.Fuel.Dry) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) + description + (IApp. IVar Just + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ IVar Data.Nat.Pos.one + $ (IApp. IVar <> + $ IVar ^fuel_arg^)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth + $ IVar ^sub^fuel_arg^) + $ (IApp. IVar <> + $ IVar ^sub^fuel_arg^)) + $ IVar Nil))) ])) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IBindVar n) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (INamedApp (IVar DerivedGen.MkX) - n - (IVar n)) - m - (IVar m))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) + $ IVar Prelude.Types.Nat))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar Prelude.Types.Nat))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Types.Z) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ IBindVar ^bnd^{arg:3654})) - (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ IVar n) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3651}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3651} - $ IVar ^bnd^{arg:3654})) ])) ])) ] ] + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (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:651})))) ] ] diff --git a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected index 993e26a03..b1a9fb908 100644 --- a/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected +++ b/tests/derivation/least-effort/print/adt/014 right-to-left nondet ext/expected @@ -16,19 +16,11 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IPrimVal String - $ (ILam. (MW ExplicitArg {arg:3630} : IPrimVal String) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + $ IVar DerivedGen.Y))) IClaim MW Export [] @@ -46,53 +38,68 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> + $ (IApp. IVar Builtin.DPair.DPair + $ IPrimVal String + $ (ILam. (MW ExplicitArg {arg:3630} : IPrimVal String) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> $ IVar ^fuel_arg^)) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IPrimVal String - $ (ILam. (MW ExplicitArg {arg:3630} : IPrimVal String) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar external^<^prim^.String>[] + $ (IApp. IVar [] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar external^[] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.MkX - $ IVar n - $ IVar m)))))))) ] ] + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ IBindVar ^bnd^{arg:3654})) + (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ IVar n) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3651}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3651} + $ IVar ^bnd^{arg:3654})) ])) ])) ] ] IDef [0] [ PatClause (IApp. IVar [0] $ IBindVar ^fuel_arg^ @@ -131,52 +138,45 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (IApp. IVar DerivedGen.MkX $ IVar n $ IVar m))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> $ IVar ^fuel_arg^)) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> + $ (IApp. IVar Builtin.DPair.DPair + $ IPrimVal String + $ (ILam. (MW ExplicitArg {arg:3630} : IPrimVal String) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] + $ (IApp. IVar external^<^prim^.String>[] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ IBindVar ^bnd^{arg:3654})) - (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ IVar n) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3651}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3651} - $ IVar ^bnd^{arg:3654})) ])) ])) ] ] + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar external^[] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.MkX + $ IVar n + $ IVar m)))))))) ] ] diff --git a/tests/derivation/least-effort/print/gadt/002 gadt/expected b/tests/derivation/least-effort/print/gadt/002 gadt/expected index 2bf8dd29b..537c7bdaa 100644 --- a/tests/derivation/least-effort/print/gadt/002 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/002 gadt/expected @@ -5,14 +5,6 @@ LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (n : Nat ** Fi LOG gen.auto.derive.infra:0: ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) => ILocal (IApp. IVar [] $ IVar ^outmost-fuel^) - IClaim MW - Export - [] - (MkTy [] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) IClaim MW Export [] @@ -25,69 +17,14 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (ILam. (MW ExplicitArg n : IVar Prelude.Types.Nat) => (IApp. IVar Data.Fin.Fin $ IVar n)))))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (ICase (IVar ^fuel_arg^) - (IVar Data.Fuel.Fuel) - [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> - $ IVar Data.Fuel.Dry) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) - description - (IApp. IVar Just - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> - $ IVar ^fuel_arg^)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth - $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) - $ IVar Nil))) ])) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z) ] - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (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:651})))) ] ] + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) @@ -175,3 +112,66 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) k (IVar k) $ IVar ^bnd^{arg:3095}))) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (ICase (IVar ^fuel_arg^) + (IVar Data.Fuel.Fuel) + [ PatClause (IVar Data.Fuel.Dry) + (IApp. IVar <> + $ IVar Data.Fuel.Dry) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) + description + (IApp. IVar Just + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ IVar Data.Nat.Pos.one + $ (IApp. IVar <> + $ IVar ^fuel_arg^)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth + $ IVar ^sub^fuel_arg^) + $ (IApp. IVar <> + $ IVar ^sub^fuel_arg^)) + $ IVar Nil))) ])) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Types.Z) ] + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (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:651})))) ] ] diff --git a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected index f45dd6b5f..6e0af795c 100644 --- a/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected +++ b/tests/derivation/least-effort/print/gadt/003 right-to-left nondet/expected @@ -8,27 +8,25 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy [] + (MkTy [1] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IClaim MW Export [] @@ -46,166 +44,212 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [1] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (ICase (IVar ^fuel_arg^) - (IVar Data.Fuel.Fuel) - [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> - $ IVar Data.Fuel.Dry) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) - description - (IApp. IVar Just - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> - $ IVar ^fuel_arg^)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth - $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) - $ IVar Nil))) ])) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + description + (IApp. IVar Just + $ IPrimVal DerivedGen.Y[] (non-recursive))) + em + (IVar MaybeEmpty) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ IVar Nil)))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z) ] - IDef <> - [ PatClause (IApp. IVar <> + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ IBindVar ^bnd^{arg:3660})) + (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ IVar n) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3657}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY1) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3657} + $ IVar ^bnd^{arg:3660})) ])) ])) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (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:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3669})) + (IApp. IVar >>= + $ (IApp. IVar [1] + $ IVar ^outmost-fuel^ + $ IVar m) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ IBindVar ^bnd^{arg:3666}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY2) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3666} + $ IVar ^bnd^{arg:3669})) ])) ])) ] ] + IDef [1] + [ PatClause (IApp. IVar [1] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3633}>) (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.X_GADT[] (non-recursive))) + $ IPrimVal DerivedGen.X_GADT[1] (non-recursive))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3633}>) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3633}>) $ IVar Nil)))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ IVar Prelude.Types.Z)))))) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ IVar DerivedGen.MkXG_4))) ] + $ IVar DerivedGen.MkXG_4)) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkXG_5) - m - (IVar m)))))) ] ] + $ IBindVar ^cons_fuel^ + $ IBindVar m) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkXG_5) + m + (IVar m))) ] ] IDef [0] [ PatClause (IApp. IVar [0] $ IBindVar ^fuel_arg^ @@ -298,188 +342,144 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True $ Implicit True) (IVar empty) ] ] - IDef [1] - [ PatClause (IApp. IVar [1] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3633}>) + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.X_GADT[1] (non-recursive))) + $ IPrimVal DerivedGen.X_GADT[] (non-recursive))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3633}>) + $ IVar ^fuel_arg^) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3633}>) + $ IVar ^fuel_arg^) $ IVar Nil)))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ IVar Prelude.Types.Z)))))) + $ IBindVar ^cons_fuel^) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ IVar DerivedGen.MkXG_4)) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ IVar DerivedGen.MkXG_4))) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IBindVar m) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkXG_5) - m - (IVar m))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - description - (IApp. IVar Just - $ IPrimVal DerivedGen.Y[] (non-recursive))) - em - (IVar MaybeEmpty) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ IVar Nil)))) + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkXG_5) + m + (IVar m)))))) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (ICase (IVar ^fuel_arg^) + (IVar Data.Fuel.Fuel) + [ PatClause (IVar Data.Fuel.Dry) + (IApp. IVar <> + $ IVar Data.Fuel.Dry) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) + description + (IApp. IVar Just + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ IVar Data.Nat.Pos.one + $ (IApp. IVar <> + $ IVar ^fuel_arg^)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth + $ IVar ^sub^fuel_arg^) + $ (IApp. IVar <> + $ IVar ^sub^fuel_arg^)) + $ IVar Nil))) ])) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar Prelude.Types.Nat))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ IBindVar ^bnd^{arg:3660})) - (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ IVar n) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3657}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY1) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3657} - $ IVar ^bnd^{arg:3660})) ])) ])) ] - IDef <> - [ PatClause (IApp. IVar <> + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Types.Z) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3669})) - (IApp. IVar >>= - $ (IApp. IVar [1] - $ IVar ^outmost-fuel^ - $ IVar m) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ IBindVar ^bnd^{arg:3666}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY2) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3666} - $ IVar ^bnd^{arg:3669})) ])) ])) ] ] + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (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:651})))) ] ] diff --git a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected index 9f75e66b8..b9bd9a500 100644 --- a/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected +++ b/tests/derivation/least-effort/print/gadt/004 right-to-left det/expected @@ -8,27 +8,41 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy [] + (MkTy [0] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) + $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_ADT + $ IVar {arg:3651} + $ IVar {arg:3654})))))) + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) => (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_ADT - $ IVar {arg:3651} - $ IVar {arg:3654})))))))) + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IClaim MW Export [] @@ -46,222 +60,233 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + $ (ILam. (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) => (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) - IClaim MW - Export - [] - (MkTy [0] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_ADT - $ IVar {arg:3651} - $ IVar {arg:3654})))))) + $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_ADT + $ IVar {arg:3651} + $ IVar {arg:3654})))))))) IClaim MW Export [] - (MkTy [] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (ICase (IVar ^fuel_arg^) - (IVar Data.Fuel.Fuel) - [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar <> - $ IVar Data.Fuel.Dry) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) - description - (IApp. IVar Just - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ IVar Data.Nat.Pos.one - $ (IApp. IVar <> - $ IVar ^fuel_arg^)) - $ (IApp. IVar :: - $ (IApp. IVar Builtin.MkPair - $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth - $ IVar ^sub^fuel_arg^) - $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) - $ IVar Nil))) ])) + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + description + (IApp. IVar Just + $ IPrimVal DerivedGen.Y[] (non-recursive))) + em + (IVar MaybeEmpty) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ IVar Nil)))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) + $ IVar DerivedGen.Y))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z) ] - IDef <> - [ PatClause (IApp. IVar <> + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ IBindVar ^bnd^{arg:3675})) + (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ IVar n) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3672}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY_LR) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3672} + $ IVar ^bnd^{arg:3675})) ])) ])) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (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:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar n + $ (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar k + $ IBindVar ^bnd^{arg:3684})) + (IApp. IVar >>= + $ (IApp. IVar [0] + $ IVar ^outmost-fuel^ + $ IVar n) + $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) + => ICase (IVar {lamc:0}) + (Implicit False) + [ PatClause (IApp. IVar Builtin.DPair.MkDPair + $ IBindVar m + $ IBindVar ^bnd^{arg:3681}) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY_RL) + k + (IVar k)) + m + (IVar m)) + n + (IVar n) + $ IVar ^bnd^{arg:3681} + $ IVar ^bnd^{arg:3684})) ])) ])) ] ] + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3651}>) (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3651}>)) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_ADT - $ IVar {arg:3651} - $ IVar {arg:3654})))))))) + $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_ADT + $ IVar {arg:3651} + $ IVar {arg:3654})))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ IBindVar n) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg n : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.MkX - $ IVar n - $ IVar m)))))))) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3630}>) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.MkX + $ IVar n + $ IVar m))))) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.X_GADT[0] (non-recursive))) + $ IPrimVal DerivedGen.X_GADT[] (non-recursive))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>) + $ IVar ^fuel_arg^) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>) + $ IVar ^fuel_arg^) $ IVar Nil)))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))) + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ IVar Prelude.Types.Z))))) + $ IBindVar ^cons_fuel^) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ IVar DerivedGen.MkXG_4)) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ IVar DerivedGen.MkXG_4))) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ (IApp. IVar Prelude.Types.S - $ IVar Prelude.Types.Z)))))) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^outmost-fuel^) @@ -272,76 +297,86 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ INamedApp (IVar DerivedGen.MkXG_5) - m - (IVar m))))) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] ] - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.MkXG_5) + m + (IVar m)))))) ] ] + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3630}>) (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.X_GADT[] (non-recursive))) + $ IPrimVal DerivedGen.X_GADT[0] (non-recursive))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar ^fuel_arg^) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>) $ IVar Nil)))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_GADT - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_GADT + $ IVar {arg:3630} + $ IVar {arg:3633})))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ IVar Prelude.Types.Z))))) (IApp. INamedApp (IVar Prelude.pure) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ IVar DerivedGen.MkXG_4))) ] + $ IVar DerivedGen.MkXG_4)) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ (IApp. IVar Prelude.Types.S + $ IVar Prelude.Types.Z)))))) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^outmost-fuel^) @@ -352,151 +387,116 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Builtin.DPair.MkDPair $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.MkXG_5) - m - (IVar m)))))) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3651}>) + $ INamedApp (IVar DerivedGen.MkXG_5) + m + (IVar m))))) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3651}>)) + $ IVar ^fuel_arg^)) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ (IApp. IVar Builtin.DPair.DPair $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.X_ADT - $ IVar {arg:3651} - $ IVar {arg:3654})))))) + $ (ILam. (MW ExplicitArg {arg:3651} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3654} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.X_ADT + $ IVar {arg:3651} + $ IVar {arg:3654})))))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IBindVar n) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg m : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.MkX - $ IVar n - $ IVar m))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - description - (IApp. IVar Just - $ IPrimVal DerivedGen.Y[] (non-recursive))) - em - (IVar MaybeEmpty) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ IVar Nil)))) + $ (ILam. (MW ExplicitArg n : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg m : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.MkX + $ IVar n + $ IVar m)))))))) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (ICase (IVar ^fuel_arg^) + (IVar Data.Fuel.Fuel) + [ PatClause (IVar Data.Fuel.Dry) + (IApp. IVar <> + $ IVar Data.Fuel.Dry) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) + description + (IApp. IVar Just + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ IVar Data.Nat.Pos.one + $ (IApp. IVar <> + $ IVar ^fuel_arg^)) + $ (IApp. IVar :: + $ (IApp. IVar Builtin.MkPair + $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth + $ IVar ^sub^fuel_arg^) + $ (IApp. IVar <> + $ IVar ^sub^fuel_arg^)) + $ IVar Nil))) ])) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) + $ IVar Prelude.Types.Nat))) IClaim MW Export [] - (MkTy <> + (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar DerivedGen.Y))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar Prelude.Types.Nat))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ IBindVar ^bnd^{arg:3675})) - (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ IVar n) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3672}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY_LR) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3672} - $ IVar ^bnd^{arg:3675})) ])) ])) ] - IDef <> - [ PatClause (IApp. IVar <> + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Types.Z) ] + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar n - $ (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar k - $ IBindVar ^bnd^{arg:3684})) - (IApp. IVar >>= - $ (IApp. IVar [0] - $ IVar ^outmost-fuel^ - $ IVar n) - $ (ILam. (MW ExplicitArg {lamc:0} : Implicit False) - => ICase (IVar {lamc:0}) - (Implicit False) - [ PatClause (IApp. IVar Builtin.DPair.MkDPair - $ IBindVar m - $ IBindVar ^bnd^{arg:3681}) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (INamedApp (INamedApp (IVar DerivedGen.MkY_RL) - k - (IVar k)) - m - (IVar m)) - n - (IVar n) - $ IVar ^bnd^{arg:3681} - $ IVar ^bnd^{arg:3684})) ])) ])) ] ] + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (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:651})))) ] ] diff --git a/tests/derivation/least-effort/print/gadt/005 gadt/expected b/tests/derivation/least-effort/print/gadt/005 gadt/expected index 865c53632..ac95ccd31 100644 --- a/tests/derivation/least-effort/print/gadt/005 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/005 gadt/expected @@ -13,14 +13,6 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty $ IPrimVal String)) => ILocal (IApp. IVar [] $ IVar ^outmost-fuel^) - IClaim MW - Export - [] - (MkTy [] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) IClaim MW Export [] @@ -33,54 +25,14 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) => (IApp. IVar DerivedGen.D $ IVar {arg:3630})))))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - description - (IApp. IVar Just - $ IPrimVal Prelude.Basics.Bool[] (non-recursive))) - em - (IVar MaybeEmpty) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ IVar Nil)))) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Basics.False) ] - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Basics.True) ] ] + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Basics.Bool))) IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) @@ -271,3 +223,51 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IVar b) $ IVar ^bnd^{arg:3659} $ IVar ^bnd^{arg:3662}))))) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + description + (IApp. IVar Just + $ IPrimVal Prelude.Basics.Bool[] (non-recursive))) + em + (IVar MaybeEmpty) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ IVar Nil)))) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Basics.Bool))) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Basics.Bool))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Basics.False) ] + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Basics.True) ] ] diff --git a/tests/derivation/least-effort/print/gadt/006 gadt/expected b/tests/derivation/least-effort/print/gadt/006 gadt/expected index 1b655ce7f..58daffe72 100644 --- a/tests/derivation/least-effort/print/gadt/006 gadt/expected +++ b/tests/derivation/least-effort/print/gadt/006 gadt/expected @@ -19,11 +19,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [] + (MkTy [0] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) + $ (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))) IClaim MW Export [] @@ -39,185 +41,131 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) IClaim MW Export [] - (MkTy [0] + (MkTy [] (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))) - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - description - (IApp. IVar Just - $ IPrimVal Prelude.Basics.Bool[] (non-recursive))) - em - (IVar MaybeEmpty) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ IVar Nil)))) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Basics.Bool))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Basics.False) ] - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Basics.True) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + $ IVar Prelude.Basics.Bool))) + IDef [0] + [ PatClause (IApp. IVar [0] + $ IBindVar ^fuel_arg^ + $ IBindVar inter^<{arg:3630}>) (ILocal (ICase (IVar ^fuel_arg^) (IVar Data.Fuel.Fuel) [ PatClause (IVar Data.Fuel.Dry) (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.D[] (dry fuel))) + $ IPrimVal DerivedGen.D[0] (dry fuel))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar Data.Fuel.Dry) + $ IVar Data.Fuel.Dry + $ IVar inter^<{arg:3630}>) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar Data.Fuel.Dry) + $ IVar Data.Fuel.Dry + $ IVar inter^<{arg:3630}>) $ IVar Nil))) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) description (IApp. IVar Just - $ IPrimVal DerivedGen.D[] (spend fuel)) + $ IPrimVal DerivedGen.D[0] (spend fuel)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one $ (IApp. IVar <> - $ IVar ^fuel_arg^)) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) + $ IVar ^sub^fuel_arg^ + $ IVar inter^<{arg:3630}>)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one $ (IApp. IVar <> - $ IVar ^fuel_arg^)) + $ IVar ^fuel_arg^ + $ IVar inter^<{arg:3630}>)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^)) + $ IVar ^sub^fuel_arg^ + $ IVar inter^<{arg:3630}>)) $ IVar Nil))))) ])) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Basics.Bool - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) - => (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))))) + $ (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Basics.Bool - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) - => (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))))) + $ (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Basics.Bool - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) - => (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))))) + $ (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Basics.Bool - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) - => (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))))) + $ (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ IBindVar b) (IApp. IVar >>= - $ (IApp. IVar [] + $ (IApp. IVar external^[] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg b : Implicit False) + $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) => (IApp. IVar >>= $ (IApp. IVar external^[] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) - => (IApp. IVar >>= - $ (IApp. IVar external^[] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3639} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. INamedApp (IVar DerivedGen.JJ) - b - (IVar b) - $ IVar ^bnd^{arg:3636} - $ IVar ^bnd^{arg:3639}))))))))) ] + $ (ILam. (MW ExplicitArg ^bnd^{arg:3639} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. INamedApp (IVar DerivedGen.JJ) + b + (IVar b) + $ IVar ^bnd^{arg:3636} + $ IVar ^bnd^{arg:3639})))))) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ IVar Prelude.Basics.False) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^cons_fuel^) @@ -235,16 +183,19 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. INamedApp (IVar DerivedGen.FN) - b - (IVar b) - $ IVar ^bnd^{arg:3645} - $ IVar ^bnd^{arg:3648}))))) ])) ] + $ (IApp. INamedApp (IVar DerivedGen.FN) + b + (IVar b) + $ IVar ^bnd^{arg:3645} + $ IVar ^bnd^{arg:3648})))) ])) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ IVar Prelude.Basics.True) (IApp. IVar >>= $ (IApp. IVar external^<^prim^.String>[] $ IVar ^outmost-fuel^) @@ -253,13 +204,16 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar DerivedGen.TL - $ IVar ^bnd^{arg:3654}))))) ] + $ (IApp. IVar DerivedGen.TL + $ IVar ^bnd^{arg:3654})))) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) + $ IBindVar ^cons_fuel^ + $ IVar Prelude.Basics.True) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^cons_fuel^) @@ -277,133 +231,139 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. INamedApp (IVar DerivedGen.TR) - b - (IVar b) - $ IVar ^bnd^{arg:3659} - $ IVar ^bnd^{arg:3662}))))) ])) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3630}>) + $ (IApp. INamedApp (IVar DerivedGen.TR) + b + (IVar b) + $ IVar ^bnd^{arg:3659} + $ IVar ^bnd^{arg:3662})))) ])) + , PatClause (IApp. IVar <> + $ Implicit True + $ Implicit True) + (IVar empty) ] ] + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (ICase (IVar ^fuel_arg^) (IVar Data.Fuel.Fuel) [ PatClause (IVar Data.Fuel.Dry) (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) description (IApp. IVar Just - $ IPrimVal DerivedGen.D[0] (dry fuel))) + $ IPrimVal DerivedGen.D[] (dry fuel))) em (IVar MaybeEmpty) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar Data.Fuel.Dry - $ IVar inter^<{arg:3630}>) + $ IVar Data.Fuel.Dry) $ (IApp. IVar :: $ (IApp. IVar <> - $ IVar Data.Fuel.Dry - $ IVar inter^<{arg:3630}>) + $ IVar Data.Fuel.Dry) $ IVar Nil))) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. INamedApp (IVar Test.DepTyCheck.Gen.frequency) description (IApp. IVar Just - $ IPrimVal DerivedGen.D[0] (spend fuel)) + $ IPrimVal DerivedGen.D[] (spend fuel)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>)) + $ IVar ^fuel_arg^)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^ - $ IVar inter^<{arg:3630}>)) + $ IVar ^sub^fuel_arg^)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ IVar Data.Nat.Pos.one $ (IApp. IVar <> - $ IVar ^fuel_arg^ - $ IVar inter^<{arg:3630}>)) + $ IVar ^fuel_arg^)) $ (IApp. IVar :: $ (IApp. IVar Builtin.MkPair $ (IApp. IVar Deriving.DepTyCheck.Util.Reflection.leftDepth $ IVar ^sub^fuel_arg^) $ (IApp. IVar <> - $ IVar ^sub^fuel_arg^ - $ IVar inter^<{arg:3630}>)) + $ IVar ^sub^fuel_arg^)) $ IVar Nil))))) ])) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))) + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Basics.Bool + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) + => (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))) + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Basics.Bool + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) + => (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))) + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Basics.Bool + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) + => (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))))) IClaim MW Export [] (MkTy <> (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) -> (IApp. IVar Test.DepTyCheck.Gen.Gen $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar DerivedGen.D - $ IVar {arg:3630})))) + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Basics.Bool + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Basics.Bool) + => (IApp. IVar DerivedGen.D + $ IVar {arg:3630})))))) IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IBindVar b) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= - $ (IApp. IVar external^[] + $ (IApp. IVar [] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) + $ (ILam. (MW ExplicitArg b : Implicit False) => (IApp. IVar >>= $ (IApp. IVar external^[] $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:3639} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.JJ) - b - (IVar b) - $ IVar ^bnd^{arg:3636} - $ IVar ^bnd^{arg:3639})))))) ] + $ (ILam. (MW ExplicitArg ^bnd^{arg:3636} : Implicit False) + => (IApp. IVar >>= + $ (IApp. IVar external^[] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg ^bnd^{arg:3639} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. INamedApp (IVar DerivedGen.JJ) + b + (IVar b) + $ IVar ^bnd^{arg:3636} + $ IVar ^bnd^{arg:3639}))))))))) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IVar Prelude.Basics.False) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^cons_fuel^) @@ -421,19 +381,16 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.FN) - b - (IVar b) - $ IVar ^bnd^{arg:3645} - $ IVar ^bnd^{arg:3648})))) ])) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. INamedApp (IVar DerivedGen.FN) + b + (IVar b) + $ IVar ^bnd^{arg:3645} + $ IVar ^bnd^{arg:3648}))))) ])) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IVar Prelude.Basics.True) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= $ (IApp. IVar external^<^prim^.String>[] $ IVar ^outmost-fuel^) @@ -442,16 +399,13 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. IVar DerivedGen.TL - $ IVar ^bnd^{arg:3654})))) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar DerivedGen.TL + $ IVar ^bnd^{arg:3654}))))) ] IDef <> [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^ - $ IVar Prelude.Basics.True) + $ IBindVar ^cons_fuel^) (IApp. IVar >>= $ (IApp. IVar [] $ IVar ^cons_fuel^) @@ -469,12 +423,58 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) f (IApp. IVar Test.DepTyCheck.Gen.Gen $ Implicit True) - $ (IApp. INamedApp (IVar DerivedGen.TR) - b - (IVar b) - $ IVar ^bnd^{arg:3659} - $ IVar ^bnd^{arg:3662})))) ])) - , PatClause (IApp. IVar <> - $ Implicit True - $ Implicit True) - (IVar empty) ] ] + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. INamedApp (IVar DerivedGen.TR) + b + (IVar b) + $ IVar ^bnd^{arg:3659} + $ IVar ^bnd^{arg:3662}))))) ])) ] ] + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (IApp. INamedApp (INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + description + (IApp. IVar Just + $ IPrimVal Prelude.Basics.Bool[] (non-recursive))) + em + (IVar MaybeEmpty) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ (IApp. IVar :: + $ (IApp. IVar <> + $ IVar ^fuel_arg^) + $ IVar Nil)))) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Basics.Bool))) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Basics.Bool))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Basics.False) ] + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ IVar Prelude.Basics.True) ] ] diff --git a/tests/derivation/least-effort/print/gadt/007 eq-n/expected b/tests/derivation/least-effort/print/gadt/007 eq-n/expected index dbe3f133e..f60b9cd3a 100644 --- a/tests/derivation/least-effort/print/gadt/007 eq-n/expected +++ b/tests/derivation/least-effort/print/gadt/007 eq-n/expected @@ -5,14 +5,6 @@ LOG gen.auto.derive.infra:0: type: (arg : Fuel) -> Gen MaybeEmpty (a : Nat ** (b LOG gen.auto.derive.infra:0: ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) => ILocal (IApp. IVar [] $ IVar ^outmost-fuel^) - IClaim MW - Export - [] - (MkTy [] - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ IVar Prelude.Types.Nat))) IClaim MW Export [] @@ -29,6 +21,53 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) => (IApp. IVar DerivedGen.EqualN $ IVar {arg:3630} $ IVar {arg:3633})))))))) + IClaim MW + Export + [] + (MkTy [] + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ IVar Prelude.Types.Nat))) + IDef [] + [ PatClause (IApp. IVar [] + $ IBindVar ^fuel_arg^) + (ILocal (IApp. IVar <> + $ IVar ^fuel_arg^)) + IClaim MW + Export + [] + (MkTy <> + (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) + -> (IApp. IVar Test.DepTyCheck.Gen.Gen + $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty + $ (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) + => (IApp. IVar Builtin.DPair.DPair + $ IVar Prelude.Types.Nat + $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) + => (IApp. IVar DerivedGen.EqualN + $ IVar {arg:3630} + $ IVar {arg:3633})))))))) + IDef <> + [ PatClause (IApp. IVar <> + $ IBindVar ^cons_fuel^) + (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^outmost-fuel^) + $ (ILam. (MW ExplicitArg x : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ (IApp. IVar Builtin.DPair.MkDPair + $ Implicit True + $ INamedApp (IVar DerivedGen.ReflN) + x + (IVar x)))))) ] ] IDef [] [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) @@ -92,42 +131,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:651})))) ] ] - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar <> - $ IVar ^fuel_arg^)) - IClaim MW - Export - [] - (MkTy <> - (IPi. (MW ExplicitArg : IVar Data.Fuel.Fuel) - -> (IApp. IVar Test.DepTyCheck.Gen.Gen - $ IVar Test.DepTyCheck.Gen.Emptiness.MaybeEmpty - $ (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3630} : IVar Prelude.Types.Nat) - => (IApp. IVar Builtin.DPair.DPair - $ IVar Prelude.Types.Nat - $ (ILam. (MW ExplicitArg {arg:3633} : IVar Prelude.Types.Nat) - => (IApp. IVar DerivedGen.EqualN - $ IVar {arg:3630} - $ IVar {arg:3633})))))))) - IDef <> - [ PatClause (IApp. IVar <> - $ IBindVar ^cons_fuel^) - (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^outmost-fuel^) - $ (ILam. (MW ExplicitArg x : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ (IApp. IVar Builtin.DPair.MkDPair - $ Implicit True - $ INamedApp (IVar DerivedGen.ReflN) - x - (IVar x)))))) ] ]