Extend support for generators that don’t consume Fuel

[L3odr0id]

Generator for such type can potentially run without fuel, even if it's totality can't be proven by Idris2

public export
data FinConsumer : Fin n -> Type where
  Consume : FinConsumer f

public export
data ConsumersList : Fin (S n) -> Type where
  Nil  : ConsumersList FZ
  (::) : FinConsumer f -> ConsumersList (weaken i) -> ConsumersList (FS i)

A generator printed by collection nightly-250824

import Deriving.DepTyCheck.Gen

%language ElabReflection

%runElab deriveGenPrinter $ Fuel -> {n' : _} -> (n : Fin $ S n') -> Gen MaybeEmpty $ ConsumersList n

, IDef
    emptyFC
    "<<Test.Verilog.Things.Test.Nil>>"
    [       var "<<Test.Verilog.Things.Test.Nil>>"
        .$ bindVar "^cons_fuel^"
        .$ bindVar "{n:5317}"
        .$ (var "Data.Fin.FZ" .! ("k", implicitTrue))
    .=    var "Test.DepTyCheck.Gen.label"
        .$ (var "fromString" .$ primVal (Str "Test.Verilog.Things.Test.Nil (orders)"))
        .$ (   var "Prelude.pure"
            .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
            .$ (var "Test.Verilog.Things.Test.Nil" .! ("{n:5317}", var "{n:5317}")))
    , var "<<Test.Verilog.Things.Test.Nil>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
    ]
, IDef
    emptyFC
    "<<Test.Verilog.Things.Test.(::)>>"
    [       var "<<Test.Verilog.Things.Test.(::)>>"
        .$ bindVar "^cons_fuel^"
        .$ bindVar "{n:5337}"
        .$ (var "Data.Fin.FS" .! ("k", implicitTrue) .$ bindVar "i")
    .=    var "Test.DepTyCheck.Gen.label"
        .$ (var "fromString" .$ primVal (Str "Test.Verilog.Things.Test.(::) (orders)"))
        .$ (   var ">>="
            .$ (   var "<Test.Verilog.Things.Test.ConsumersList>[0, 1]"
                .$ var "^cons_fuel^"
                .$ var "{n:5337}"
                .$ (var "Data.Fin.weaken" .! ("n", var "{n:5337}") .$ var "i"))
            .$ (    MkArg MW ExplicitArg (Just "{arg:5323}") implicitFalse
                .=>    var ">>="
                    .$ (var "<Test.Verilog.Things.Test.FinConsumer>[]" .$ var "^outmost-fuel^")
                    .$ (    MkArg MW ExplicitArg (Just "{lamc:0}") implicitFalse
                        .=> iCase
                            { sc = var "{lamc:0}"
                            , ty = implicitFalse
                            , clauses =
                                [       var "Builtin.DPair.MkDPair"
                                        .$ bindVar "{n:5340}"
                                        .$ (var "Builtin.DPair.MkDPair" .$ bindVar "f" .$ bindVar "{arg:5319}")
                                    .=    var "Prelude.pure"
                                        .! ("f", var "Test.DepTyCheck.Gen.Gen" .$ implicitTrue)
                                        .$ (   var "Test.Verilog.Things.Test.(::)"
                                            .! ("{n:5340}", implicitTrue)
                                            .! ("{n:5337}", implicitTrue)
                                            .! ("i", implicitTrue)
                                            .! ("f", implicitTrue)
                                            .$ var "{arg:5319}"
                                            .$ var "{arg:5323}")
                                ]
                            })))
    , var "<<Test.Verilog.Things.Test.(::)>>" .$ implicitTrue .$ implicitTrue .$ implicitTrue .= var "empty"
    ]
]
    , scope =
        iCase
        { sc = var "^fuel_arg^"
        , ty = var "Data.Fuel.Fuel"
        , clauses =
            [    var "Data.Fuel.Dry"
                .=    var "Test.DepTyCheck.Gen.label"
                .$ (var "fromString" .$ primVal (Str "Test.Verilog.Things.Test.ConsumersList[0(n), 1] (dry fuel)"))
                .$ (var "<<Test.Verilog.Things.Test.Nil>>" .$ var "^fuel_arg^" .$ var "inter^<n>" .$ var "inter^<{arg:5308}>")
            ,    var "Data.Fuel.More" .$ bindVar "^sub^fuel_arg^"
                .=    var "Test.DepTyCheck.Gen.label"
                .$ (var "fromString" .$ primVal (Str "Test.Verilog.Things.Test.ConsumersList[0(n), 1] (non-dry fuel)"))
                .$ (   var "Test.DepTyCheck.Gen.frequency"
                    .$ (   var "::"
                        .$ (   var "Builtin.MkPair"
                            .$ var "Data.Nat1.one"
                            .$ (   var "<<Test.Verilog.Things.Test.Nil>>"
                                .$ var "^fuel_arg^"
                                .$ var "inter^<n>"
                                .$ var "inter^<{arg:5308}>"))
                        .$ (   var "::"
                            .$ (   var "Builtin.MkPair"
                                .$ (var "Deriving.DepTyCheck.Gen.ConsRecs.leftDepth" .$ var "^sub^fuel_arg^")
                                .$ (   var "<<Test.Verilog.Things.Test.(::)>>"
                                    .$ var "^sub^fuel_arg^"
                                    .$ var "inter^<n>"
                                    .$ var "inter^<{arg:5308}>"))
                            .$ var "Nil")))
            ]
        }
    }
]