0 | module Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface
 1 |
 2 | import public Deriving.DepTyCheck.Gen.ConsRecs
 3 | import public Deriving.DepTyCheck.Gen.Signature
 4 |
 5 | %default total
 6 |
 7 | --------------------------------------------------
 8 | --- Using and deriving of any needed generator ---
 9 | --------------------------------------------------
10 |
11 | public export
12 | interface Monad m => DerivationClosure m where
13 |   callGen : NamesInfoInTypes => ConsRecs =>
14 |             (sig : GenSignature) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> m (TTImp, Maybe (gend ** Vect gend $ Fin gend))
15 |   --                                                                                                     ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
16 |   --                                                                   this is a permutation of generated arguments --/
17 |   --                                                                   actually, `gend` can be calculated from `sig`, but we simplify things here
18 |
19 | export
20 | DerivationClosure m => MonadTrans t => Monad (t m) => DerivationClosure (t m) where
21 |   callGen sig fuel params = lift $ callGen sig fuel params
22 |
23 | -------------------
24 | --- Conventions ---
25 | -------------------
26 |
27 | export
28 | outmostFuelArg : Name
29 | outmostFuelArg = UN $ Basic "^outmost-fuel^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend
30 |