diff --git a/src/Deriving/DepTyCheck/Gen/Checked.idr b/src/Deriving/DepTyCheck/Gen/Checked.idr index 8f6ece1e9..63f17c0fd 100644 --- a/src/Deriving/DepTyCheck/Gen/Checked.idr +++ b/src/Deriving/DepTyCheck/Gen/Checked.idr @@ -4,6 +4,7 @@ module Deriving.DepTyCheck.Gen.Checked import public Control.Monad.Either import public Control.Monad.Reader import public Control.Monad.State +import public Control.Monad.State.Tuple import public Control.Monad.Writer import public Control.Monad.RWS @@ -91,8 +92,10 @@ namespace ClojuringCanonicImpl ClojuringContext : (Type -> Type) -> Type ClojuringContext m = ( MonadReader (SortedMap GenSignature (ExternalGenSignature, Name)) m -- external gens - , MonadState (SortedMap GenSignature Name) m -- gens already asked to be derived - , MonadWriter (List Decl, List Decl) m -- function declarations and bodies + , MonadState (SortedMap GenSignature Name) m -- gens already asked to be derived + , MonadState (List (GenSignature, Name)) m -- queue of gens to be derived + , MonadState Bool m -- flat that there is a need to start derivation loop + , MonadWriter (List Decl, List Decl) m -- function declarations and bodies ) nameForGen : GenSignature -> Name @@ -110,6 +113,11 @@ namespace ClojuringCanonicImpl DerivatorCore => ClojuringContext m => Elaboration m => CanonicGen m where callGen sig fuel values = do + -- check if we are the first, then we need to start the loop + startLoop <- get {stateType=Bool} + -- say that no one needs any more startups, we are in charge + put False + -- look for external gens, and call it if exists let Nothing = lookupLengthChecked sig !ask | Just (name, Element extSig lenEq) => pure $ callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values @@ -118,7 +126,7 @@ namespace ClojuringCanonicImpl internalGenName <- do -- look for existing (already derived) internals, use it if exists - let Nothing = lookup sig !get + let Nothing = SortedMap.lookup sig !get | Just name => pure name -- nothing found, then derive! acquire the name @@ -127,23 +135,45 @@ namespace ClojuringCanonicImpl -- remember that we're responsible for this signature derivation modify $ insert sig name - -- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle - (genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name - - -- remember the derived stuff - tell ([genFunClaim], [genFunBody]) + -- remember the task to derive + modify {stateType=List _} $ (::) (sig, name) -- return the name of the newly derived generator pure name + -- if we were first to start the derivation loop, then... + when startLoop $ do + -- start the derivation loop itself + deriveAll + -- we now are not in charge of the derivation loop, so reset the flag + put True + -- call the internal gen pure $ callCanonic sig internalGenName fuel values + where + + deriveOne : (GenSignature, Name) -> m () + deriveOne (sig, name) = do + + -- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle + (genFunClaim, genFunBody) <- logBounds "type" [sig] $ assert_total $ deriveCanonical sig name + + -- remember the derived stuff + tell ([genFunClaim], [genFunBody]) + + deriveAll : m () + deriveAll = do + toDerive <- get {stateType=List _} + put {stateType=List _} [] + for_ toDerive deriveOne + when (not $ null toDerive) $ assert_total $ deriveAll + --- Canonic-dischagring function --- export runCanonic : DerivatorCore => SortedMap ExternalGenSignature Name -> (forall m. CanonicGen m => m a) -> Elab (a, List Decl) runCanonic exts calc = do let exts = SortedMap.fromList $ exts.asList <&> \namedSig => (fst $ internalise $ fst namedSig, namedSig) - (x, defs, bodies) <- evalRWST exts empty calc {s=SortedMap GenSignature Name} {w=(_, _)} + (x, defs, bodies) <- evalRWST exts (empty, empty, True) calc {s=(SortedMap GenSignature Name, List (GenSignature, Name), _)} {w=(_, _)} pure (x, defs ++ bodies) 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 d7759ea68..4849b3f45 100644 --- a/tests/derivation/least-effort/print/adt/004 noparam/expected +++ b/tests/derivation/least-effort/print/adt/004 noparam/expected @@ -8,164 +8,164 @@ 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> + $ IPrimVal DerivedGen.X[] (dry fuel)) + $ (IApp. IVar <> $ IVar Data.Fuel.Dry)) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ IPrimVal DerivedGen.X[] (spend fuel)) $ (IApp. IVar Test.DepTyCheck.Gen.frequency $ (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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) + $ IPrimVal DerivedGen.E (orders)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) + $ IPrimVal DerivedGen.R (orders)) $ (IApp. IVar >>= - $ (IApp. IVar [] + $ (IApp. IVar [] $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:789}))))) ] ] - 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (dry fuel)) - $ (IApp. IVar <> + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> $ IVar Data.Fuel.Dry)) , PatClause (IApp. IVar Data.Fuel.More $ IBindVar ^sub^fuel_arg^) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (spend fuel)) + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) $ (IApp. IVar Test.DepTyCheck.Gen.frequency $ (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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.E (orders)) + $ IPrimVal Prelude.Types.Z (orders)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.R (orders)) + $ IPrimVal Prelude.Types.S (orders)) $ (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:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] diff --git a/tests/derivation/least-effort/print/adt/006 param/expected b/tests/derivation/least-effort/print/adt/006 param/expected index 587e4c004..7a12c98f3 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,52 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX (orders)) + $ (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^) @@ -97,41 +135,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 4a284468f..4663a022d 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,87 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX (orders)) + $ (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^) @@ -105,79 +181,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) - $ (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 ca24ca306..7bb42e9f9 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,87 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX (orders)) + $ (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^) @@ -105,79 +181,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) - $ (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 dcaaedca2..f6a408784 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,87 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[0] (non-recursive)) + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX (orders)) + $ (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^) @@ -103,79 +179,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [0] - [ PatClause (IApp. IVar [0] - $ IBindVar ^fuel_arg^ - $ IBindVar inter^<{arg:3630}>) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[0] (non-recursive)) - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) - $ (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 3b91447a4..30cdc77f7 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,103 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX (orders)) + $ (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^) @@ -109,95 +201,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) - $ (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 3e0d851d1..270b61d7e 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,109 +32,61 @@ 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 (ICase (IVar ^fuel_arg^) - (IVar Data.Fuel.Fuel) - [ PatClause (IVar Data.Fuel.Dry) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> - $ IVar Data.Fuel.Dry)) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar Test.DepTyCheck.Gen.frequency - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) - $ (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + $ 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Builtin.Unit[] (non-recursive)) - $ (IApp. IVar <> + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Builtin.Unit))) - IDef <> - [ PatClause (IApp. IVar <> + $ IVar DerivedGen.Y))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Builtin.MkUnit (orders)) - $ (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Builtin.MkUnit)) ] ] + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label @@ -193,45 +137,101 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) (IVar n)) m (IVar m))))))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (IApp. IVar <> + $ IPrimVal Builtin.Unit[] (non-recursive)) + $ (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 <> + $ IVar Builtin.Unit))) + IDef <> + [ PatClause (IApp. IVar <> $ IBindVar ^cons_fuel^) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) + $ IPrimVal Builtin.MkUnit (orders)) + $ (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 (ICase (IVar ^fuel_arg^) + (IVar Data.Fuel.Fuel) + [ PatClause (IVar Data.Fuel.Dry) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> + $ IVar Data.Fuel.Dry)) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar Test.DepTyCheck.Gen.frequency + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Z (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.S (orders)) $ (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})) ]))) ] ] + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] 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 6e3aa2af6..5e53fa691 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,161 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X2[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX2 (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X1[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkX1 (orders)) + $ (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^) @@ -117,121 +235,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X1[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX1 (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X2[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX2 (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) - $ (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 b98667f83..1d0007ed6 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,121 +8,150 @@ 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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> - $ IVar Data.Fuel.Dry)) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar Test.DepTyCheck.Gen.frequency - $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.MkY (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X[0] (non-recursive)) + $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) - $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) + $ IPrimVal DerivedGen.MkX (orders)) $ (IApp. IVar >>= $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : 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:789}))))) ] ] + $ (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 Test.DepTyCheck.Gen.label @@ -173,104 +202,75 @@ 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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[0] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> + $ IVar Data.Fuel.Dry)) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar Test.DepTyCheck.Gen.frequency + $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) + $ IPrimVal Prelude.Types.Z (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.S (orders)) $ (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:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] 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 e94b8cb97..642844930 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,59 +38,74 @@ 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^) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X[] (non-recursive)) - $ (IApp. IVar <> + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkX (orders)) + $ IPrimVal DerivedGen.MkY (orders)) $ (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^ @@ -143,58 +150,51 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ (IApp. IVar DerivedGen.MkX $ IVar n $ IVar m)))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) + IDef [] + [ PatClause (IApp. IVar [] $ IBindVar ^fuel_arg^) (ILocal (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (IApp. IVar <> + $ IPrimVal DerivedGen.X[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY (orders)) + $ IPrimVal DerivedGen.MkX (orders)) $ (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 361d3583e..4b621d588 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,78 +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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> - $ IVar Data.Fuel.Dry)) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar Test.DepTyCheck.Gen.frequency - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) - $ (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:789}))))) ] ] + 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^) @@ -193,3 +121,75 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> + $ IVar Data.Fuel.Dry)) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar Test.DepTyCheck.Gen.frequency + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Z (orders)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.S (orders)) + $ (IApp. IVar >>= + $ (IApp. IVar [] + $ IVar ^cons_fuel^) + $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] 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 bda01f8cf..1e3297967 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,148 +44,194 @@ 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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> - $ IVar Data.Fuel.Dry)) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar Test.DepTyCheck.Gen.frequency - $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) - $ (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z)) ] - IDef <> - [ PatClause (IApp. IVar <> + $ IPrimVal DerivedGen.MkY1 (orders)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) + $ IPrimVal DerivedGen.MkY2 (orders)) $ (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:789}))))) ] ] - 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_GADT[] (non-recursive)) + $ IPrimVal DerivedGen.X_GADT[1] (non-recursive)) $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_4 (orders)) @@ -197,30 +241,27 @@ 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 - $ 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^ + $ IBindVar m) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_5 (orders)) - $ (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))))))) ] ] + $ (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^ @@ -319,62 +360,57 @@ 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_GADT[1] (non-recursive)) + $ IPrimVal DerivedGen.X_GADT[] (non-recursive)) $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_4 (orders)) @@ -384,135 +420,99 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ 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) + $ IBindVar ^cons_fuel^) (IApp. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_5 (orders)) - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - em - (IVar MaybeEmpty) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ (IApp. IVar :: - $ (IApp. IVar <> - $ IVar ^fuel_arg^) - $ IVar Nil))))) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> + $ IVar Data.Fuel.Dry)) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar Test.DepTyCheck.Gen.frequency + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY1 (orders)) - $ (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 <> + $ IPrimVal Prelude.Types.Z (orders)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY2 (orders)) + $ IPrimVal Prelude.Types.S (orders)) $ (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:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] 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 f444f3635..b64334629 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,217 +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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (dry fuel)) - $ (IApp. IVar <> - $ IVar Data.Fuel.Dry)) - , PatClause (IApp. IVar Data.Fuel.More - $ IBindVar ^sub^fuel_arg^) - (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Nat[] (spend fuel)) - $ (IApp. IVar Test.DepTyCheck.Gen.frequency - $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.Y[] (non-recursive)) + $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.Z (orders)) - $ (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ IVar Prelude.Types.Z)) ] - IDef <> - [ PatClause (IApp. IVar <> + $ IPrimVal DerivedGen.MkY_LR (orders)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal Prelude.Types.S (orders)) + $ IPrimVal DerivedGen.MkY_RL (orders)) $ (IApp. IVar >>= - $ (IApp. IVar [] - $ IVar ^cons_fuel^) - $ (ILam. (MW ExplicitArg ^bnd^{arg:789} : Implicit False) - => (IApp. INamedApp (IVar Prelude.pure) - f - (IApp. IVar Test.DepTyCheck.Gen.Gen - $ Implicit True) - $ (IApp. IVar Prelude.Types.S - $ IVar ^bnd^{arg:789}))))) ] ] - 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_ADT[] (non-recursive)) + $ IPrimVal DerivedGen.X_ADT[0] (non-recursive)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkX (orders)) $ (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}>) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_GADT[0] (non-recursive)) - $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.X_GADT[] (non-recursive)) + $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_4 (orders)) @@ -266,20 +296,12 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_5 (orders)) @@ -293,64 +315,66 @@ 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_GADT[] (non-recursive)) + $ IPrimVal DerivedGen.X_GADT[0] (non-recursive)) $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_4 (orders)) @@ -360,12 +384,20 @@ 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 - $ 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkXG_5 (orders)) @@ -379,163 +411,131 @@ 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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.X_ADT[0] (non-recursive)) + $ IPrimVal DerivedGen.X_ADT[] (non-recursive)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.MkX (orders)) $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.Y[] (non-recursive)) - $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (dry fuel)) + $ (IApp. IVar <> + $ IVar Data.Fuel.Dry)) + , PatClause (IApp. IVar Data.Fuel.More + $ IBindVar ^sub^fuel_arg^) + (IApp. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Types.Nat[] (spend fuel)) + $ (IApp. IVar Test.DepTyCheck.Gen.frequency + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY_LR (orders)) - $ (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 <> + $ IPrimVal Prelude.Types.Z (orders)) + $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.MkY_RL (orders)) + $ IPrimVal Prelude.Types.S (orders)) $ (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:789} : Implicit False) + => (IApp. INamedApp (IVar Prelude.pure) + f + (IApp. IVar Test.DepTyCheck.Gen.Gen + $ Implicit True) + $ (IApp. IVar Prelude.Types.S + $ IVar ^bnd^{arg:789}))))) ] ] diff --git a/tests/derivation/least-effort/print/gadt/005 gadt/expected b/tests/derivation/least-effort/print/gadt/005 gadt/expected index 6b18d750c..839aed152 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,60 +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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.Bool[] (non-recursive)) - $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - 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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.False (orders)) - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.True (orders)) - $ (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^) @@ -289,3 +235,57 @@ 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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.Bool[] (non-recursive)) + $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + 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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.False (orders)) + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.True (orders)) + $ (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 0fee1efb8..45db03590 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,194 +41,134 @@ 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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.Bool[] (non-recursive)) - $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) - 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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.False (orders)) - $ (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. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal Prelude.Basics.True (orders)) - $ (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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.D[] (dry fuel)) + $ IPrimVal DerivedGen.D[0] (dry fuel)) $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.D[] (spend fuel)) + $ IPrimVal DerivedGen.D[0] (spend fuel)) $ (IApp. IVar Test.DepTyCheck.Gen.frequency $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.JJ (orders)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.FN (orders)) @@ -247,16 +189,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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.TL (orders)) @@ -268,13 +213,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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.TR (orders)) @@ -295,136 +243,142 @@ 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.D[0] (dry fuel)) + $ IPrimVal DerivedGen.D[] (dry fuel)) $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) 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. IVar Test.DepTyCheck.Gen.label $ (IApp. IVar fromString - $ IPrimVal DerivedGen.D[0] (spend fuel)) + $ IPrimVal DerivedGen.D[] (spend fuel)) $ (IApp. IVar Test.DepTyCheck.Gen.frequency $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.JJ (orders)) $ (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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.FN (orders)) @@ -445,19 +399,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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.TL (orders)) @@ -469,16 +420,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 Test.DepTyCheck.Gen.label $ (IApp. IVar fromString $ IPrimVal DerivedGen.TR (orders)) @@ -499,12 +447,64 @@ 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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.Bool[] (non-recursive)) + $ (IApp. INamedApp (IVar Test.DepTyCheck.Gen.oneOf) + 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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.False (orders)) + $ (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. IVar Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal Prelude.Basics.True (orders)) + $ (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 4ef935bac..5b062f64e 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,59 @@ 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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.EqualN[] (non-recursive)) + $ (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 Test.DepTyCheck.Gen.label + $ (IApp. IVar fromString + $ IPrimVal DerivedGen.ReflN (orders)) + $ (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^) @@ -101,48 +146,3 @@ ILam. (MW ExplicitArg ^outmost-fuel^ : IVar Data.Fuel.Fuel) $ Implicit True) $ (IApp. IVar Prelude.Types.S $ IVar ^bnd^{arg:789}))))) ] ] - IDef [] - [ PatClause (IApp. IVar [] - $ IBindVar ^fuel_arg^) - (ILocal (IApp. IVar Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.EqualN[] (non-recursive)) - $ (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 Test.DepTyCheck.Gen.label - $ (IApp. IVar fromString - $ IPrimVal DerivedGen.ReflN (orders)) - $ (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))))))) ] ]