0 | ||| Main implementation of the derivator core interface
  1 | module Deriving.DepTyCheck.Gen.ForOneType.Impl
  2 |
  3 | import public Data.Either
  4 |
  5 | import public Deriving.DepTyCheck.Gen.Labels
  6 | import public Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl
  7 | import public Deriving.DepTyCheck.Gen.ForOneType.Interface
  8 |
  9 | %default total
 10 |
 11 | ------------------------------------
 12 | --- Expressions generation utils ---
 13 | ------------------------------------
 14 |
 15 | defArgNames : {sig : GenSignature} -> Vect sig.givenParams.size Name
 16 | defArgNames = sig.givenParams.asVect <&> argName' . index' sig.targetType.args
 17 |
 18 | export %inline
 19 | canonicDefaultLHS' : (namesFun : Name -> Name) -> GenSignature -> Name -> (fuel : Name) -> TTImp
 20 | canonicDefaultLHS' nmf sig n fuel = callCanonic sig n .| bindVar fuel .| bindVar . nmf <$> defArgNames
 21 |
 22 | export %inline
 23 | canonicDefaultRHS' : (namesFun : Name -> Name) -> GenSignature -> Name -> (fuel : TTImp) -> TTImp
 24 | canonicDefaultRHS' nmf sig n fuel = callCanonic sig n fuel .| var . nmf <$> defArgNames
 25 |
 26 | export %inline
 27 | canonicDefaultLHS : GenSignature -> Name -> (fuel : Name) -> TTImp
 28 | canonicDefaultLHS = canonicDefaultLHS' id
 29 |
 30 | export %inline
 31 | canonicDefaultRHS : GenSignature -> Name -> (fuel : TTImp) -> TTImp
 32 | canonicDefaultRHS = canonicDefaultRHS' id
 33 |
 34 | ----------------------------
 35 | --- Derivation functions ---
 36 | ----------------------------
 37 |
 38 | export
 39 | DeriveBodyRhsForCon => DeriveBodyForType where
 40 |   canonicBody sig n = do
 41 |
 42 |     -- check that there is at least one constructor
 43 |     Prelude.when .| null sig.targetType.cons .| fail "No constructors found for the type `\{show sig.targetType.name}`"
 44 |
 45 |     -- check that desired `Gen` is not a generator of `Gen`s
 46 |     Prelude.when .| sig.targetType.name == `{Test.DepTyCheck.Gen.Gen} .| fail "Target type of a derived `Gen` cannot be a `Gen`"
 47 |
 48 |     -- generate claims for generators per constructors
 49 |     let consClaims = sig.targetType.cons <&> \con => export' (consGenName con) (canonicSig sig)
 50 |
 51 |     -- derive bodies for generators per constructors
 52 |     consBodies <- for sig.targetType.cons $ \con => logBounds Info "deptycheck.derive.consBody" [sig, con] $
 53 |       canonicConsBody sig (consGenName con) con <&> def (consGenName con)
 54 |
 55 |     -- calculate which constructors are recursive and spend fuel, and which are not
 56 |     let Just consRecs = lookupConsWithWeight sig
 57 |       | Nothing => fail "INTERNAL ERROR: unknown type for consRecs: \{show sig.targetType.name}"
 58 |
 59 |     -- compute all needed weigthing functions, if any
 60 |     let typesWithWeightFun = mapMaybe (usedWeightFun . snd) consRecs
 61 |
 62 |     -- decide how to name a fuel argument on the LHS
 63 |     let fuelArg = "^fuel_arg^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend
 64 |
 65 |     -- generate the case expression deciding whether will we go into recursive constructors or not
 66 |     let outmostRHS = fuelDecisionExpr fuelArg $ map @{Compose} weightExpr consRecs
 67 |
 68 |     -- return function definition
 69 |     pure $ MkPair typesWithWeightFun [ canonicDefaultLHS' interimNamesWrapper sig n fuelArg .= local (consClaims ++ consBodies) outmostRHS ]
 70 |
 71 |   where
 72 |
 73 |     consGenName : Con -> Name
 74 |     consGenName con = UN $ Basic $ "<<\{show con.name}>>"
 75 |     -- I'm using `UN` but containing chars that cannot be present in the code parsed from the Idris frontend
 76 |
 77 |     fuelDecisionExpr : (fuelArg : Name) -> List (Con, Either TTImp (Name -> TTImp)) -> TTImp
 78 |     fuelDecisionExpr fuelAr consRecs = do
 79 |
 80 |       let callConstFreqs : CTLabel -> (fuel : TTImp) -> List (Con, TTImp) -> TTImp
 81 |           callConstFreqs l fuel cons = if isJust $ find (not . isWeight1 . snd) cons
 82 |             then callFrequency l $ cons <&> map (callConsGen fuel) . swap
 83 |             else callOneOf l $ cons <&> callConsGen fuel . fst
 84 |
 85 |       -- check if there are any non-recursive constructors
 86 |       let Nothing = for consRecs $ \(con, w) => (con,) <$> getLeft w
 87 |           -- only constantly weighted constructors (usually, non-recursive), thus just call all without spending fuel
 88 |         | Just consRecs => callConstFreqs "\{logPosition sig} (non-spending)".label (var fuelAr) consRecs
 89 |
 90 |       -- pattern match on the fuel argument
 91 |       iCase .| var fuelAr .| var `{Data.Fuel.Fuel} .|
 92 |
 93 |         [ -- if fuel is dry, call all non-recursive constructors on `Dry`
 94 |           let nonSpendCons = mapMaybe (\(con, w) => (con,) <$> getLeft w) consRecs in
 95 |           var `{Data.Fuel.Dry}                        .= callConstFreqs "\{logPosition sig} (dry fuel)".label (var fuelAr) nonSpendCons
 96 |
 97 |         , do -- if fuel is `More`, call spending constructors on the rest and other on the original fuel
 98 |           -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend
 99 |           let subFuelArg = UN $ Basic $ "^sub" ++ show fuelAr
100 |           let weightAndFuel = either ((var fuelAr,)) (\f => (var subFuelArg, f subFuelArg))
101 |           var `{Data.Fuel.More} .$ bindVar subFuelArg .= callFrequency "\{logPosition sig} (non-dry fuel)".label
102 |             (consRecs <&> \(con, rec) => let (f, w) = weightAndFuel rec in (w, callConsGen f con))
103 |         ]
104 |
105 |       where
106 |
107 |         callConsGen : (fuel : TTImp) -> Con -> TTImp
108 |         callConsGen fuel con = canonicDefaultRHS' interimNamesWrapper sig .| consGenName con .| fuel
109 |
110 | export
111 | MainCoreDerivator : DeriveBodyRhsForCon => DeriveBodyForType
112 | MainCoreDerivator = %search
113 |