1 | module Deriving.DepTyCheck.Gen

  3 | import public Data.Fuel

  4 | import public Data.List.Lazy

  6 | import public Deriving.DepTyCheck.Gen.ForAllNeededTypes.Impl

  7 | import public Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Impl

  8 | import public Deriving.DepTyCheck.Gen.ForOneType.Impl

 10 | import public Test.DepTyCheck.Gen -- for `Gen` data type

 12 | import public Language.Reflection.Expr.Interpolation -- for `deriveGenPrinter`

 14 | %default total

 22 | record GenSignatureFC where

 23 |   constructor MkGenSignatureFC

 24 |   sigFC        : FC

 25 |   genFC        : FC

 26 |   targetTypeFC : FC

 30 | record GenExternals where

 31 |   constructor MkGenExternals

 32 |   externals : List (ExternalGenSignature, TTImp)

 36 | data GenCheckSide

 37 |   = DerivationTask

 38 |   | ExternalGen

 40 | isDerivationTask : GenCheckSide -> Bool

 41 | isDerivationTask DerivationTask = True

 42 | isDerivationTask _              = False

 44 | isExternalGen : GenCheckSide -> Bool

 45 | isExternalGen ExternalGen = True

 46 | isExternalGen _           = False

 48 | OriginalSignatureInfo : ExternalGenSignature -> GenExternals -> Type

 49 | OriginalSignatureInfo sig exts = FinSet $ sig.givenParams.size + exts.externals.length

 51 | CheckResult : GenCheckSide -> Type

 52 | CheckResult DerivationTask = (sig : ExternalGenSignature ** exts : GenExternals ** OriginalSignatureInfo sig exts)

 53 | CheckResult ExternalGen    = (GenSignatureFC, ExternalGenSignature)

 57 | mapAndPerm : Ord a => List (a, b) -> Maybe (xs : SortedMap a b ** Vect xs.size $ Fin xs.size)

 58 | mapAndPerm xs = do

 59 |   let idxs = fst <$> xs

 60 |   let m = SortedMap.fromList xs

 61 |   let Yes lenCorr = m.size `decEq` idxs.length | No _ => Nothing

 62 |   pure (m ** rewrite lenCorr in orderIndices idxs)

 64 | checkTypeIsGen : (checkSide : GenCheckSide) -> TTImp -> Elab $ CheckResult checkSide

 65 | checkTypeIsGen checkSide origsig@sig = do

 67 |   -- check the given expression is a type, and normalise it

 68 |   sig <- normaliseAsType sig

 70 |   -- treat the given type expression as a (possibly 0-ary) function type

 71 |   let (sigArgs, sigResult) = unPi sig

 73 |   -----------------------------------------

 74 |   -- First checks in the given arguments --

 75 |   -----------------------------------------

 77 |   -- check that there are at least some parameters in the signature

 78 |   let (firstArg::sigArgs) = sigArgs

 79 |     | [] => failAt (getFC sig) "No arguments in the generator function signature, at least a fuel argument must be present"

 81 |   -- check that the first argument an explicit unnamed one

 82 |   let MkArg MW ExplicitArg (Just (MN _ _)) (IVar firstArgFC firstArgTypeName) = firstArg

 83 |     | _ => failAt (getFC firstArg.type) "The first argument must be explicit, unnamed, present at runtime and of type `Fuel`"

 85 |   -- check the type of the fuel argument

 86 |   unless !(firstArgTypeName `isSameTypeAs` `{Data.Fuel.Fuel}) $

 87 |     failAt firstArgFC "The first argument must be of type `Fuel`"

 89 |   ---------------------------------------------------------------

 90 |   -- First looks at the resulting type of a generator function --

 91 |   ---------------------------------------------------------------

 93 |   -- check the resulting type is `Gen`

 94 |   let IApp _ (IApp _ (IVar genFC topmostResultName) (IVar _ genEmptiness)) targetType = sigResult

 95 |     | _ => failAt (getFC sigResult) "The result type of the generator function must be of type \"`Gen MaybeEmpty` of desired result\""

 97 |   unless !(topmostResultName `isSameTypeAs` `{Test.DepTyCheck.Gen.Gen}) $

 98 |     failAt (getFC sigResult) "The result type of the generator function must be of type \"`Gen MaybeEmpty` of desired result\""

100 |   unless (genEmptiness `nameConformsTo` `{Test.DepTyCheck.Gen.Emptiness.MaybeEmpty}) $

101 |     failAt genFC "Only `MaybeEmpty` variant of generator is supported, `\{show genEmptiness}` is given"

102 |     -- this check can be changed to `==` as soon as we gen the result type normalised properly.

104 |   -- treat the generated type as a dependent pair

105 |   let Just (paramsToBeGenerated, targetType) = unDPairUnAlt targetType

106 |     | Nothing => failAt (getFC targetType) "Unable to interpret type under `Gen` as a dependent pair"

108 |   -- remember the right target type position

109 |   let targetTypeFC = getFC targetType

111 |   -- treat the target type as a function application

112 |   let (targetType, targetTypeArgs) = unAppAny targetType

114 |   -- check out applications types

115 |   let targetTypeArgs = targetTypeArgs <&> getExpr

117 |   -----------------------------------------

118 |   -- Working with the target type family --

119 |   -----------------------------------------

121 |   -- acquire `TypeInfo` out of the target type `TTImp` expression

122 |   targetType <- case targetType of

124 |     -- Normal type

125 |     IVar _ targetType => getInfo' targetType <|> failAt genFC "Target type `\{show targetType}` is not a top-level data definition"

127 |     -- Primitive type

128 |     IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t

130 |     -- Type of types

131 |     IType _ => pure typeInfoForTypeOfTypes

133 |     _ => failAt targetTypeFC "Target type is not a simple name"

135 |   -- check that target type has all unnamed arguments resolved with machine-generated names

136 |   _ <- ensureTyArgsNamed targetType

138 |   ------------------------------------------------------------

139 |   -- Parse `Reflect` structures to what's needed to further --

140 |   ------------------------------------------------------------

142 |   -- check that all parameters of `DPair` are as expected

143 |   paramsToBeGenerated <- for paramsToBeGenerated $ \case

144 |     MkArg MW ExplicitArg (Just $ UN nm) t => pure (nm, t)

145 |     MkArg MW ExplicitArg (Just $ MN {}) t => failAt (getFC t) "Argument of dependent pair under the resulting `Gen` seems to be repeated or badly typed"

146 |     MkArg _  _           _              t => failAt (getFC t) "Argument of dependent pair under the resulting `Gen` must be named"

148 |   -- check that all arguments are omega, not erased or linear; and that all arguments are properly named

149 |   (givenParams, autoImplArgs, givenParamsPositions) <- map partitionEithersPos $ Prelude.for sigArgs.asVect $ \case

150 |     MkArg MW ImplicitArg (Just $ UN name) type => pure $ Left (Signature.ImplicitArg, name, type)

151 |     MkArg MW ExplicitArg (Just $ UN name) type => pure $ Left (Signature.ExplicitArg, name, type)

152 |     MkArg MW AutoImplicit (Just $ MN _ _) type => pure $ Right type

153 |     MkArg MW AutoImplicit Nothing         type => pure $ Right type

155 |     MkArg MW ImplicitArg     _ ty => failAt (getFC ty) "Implicit argument must be named and must not shadow any other name"

156 |     MkArg MW ExplicitArg     _ ty => failAt (getFC ty) "Explicit argument must be named and must not shadow any other name"

157 |     MkArg MW AutoImplicit    _ ty => failAt (getFC ty) "Auto-implicit argument must be unnamed"

159 |     MkArg M0 _               _ ty => failAt (getFC ty) "Erased arguments are not supported in generator function signatures"

160 |     MkArg M1 _               _ ty => failAt (getFC ty) "Linear arguments are not supported in generator function signatures"

161 |     MkArg MW (DefImplicit _) _ ty => failAt (getFC ty) "Default implicit arguments are not supported in generator function signatures"

163 |   --------------------------------------------------

164 |   -- Target type family's arguments' first checks --

165 |   --------------------------------------------------

167 |   -- check all the arguments of the target type are correct variable names, not complex expressions

168 |   targetTypeArgs <- do

169 |     let inGivenOrGenerated : UserName -> Bool

170 |         inGivenOrGenerated n = any (\(_, n', _) => n == n') givenParams || any (\(n', _) => n == n') paramsToBeGenerated

171 |     let err : Name -> String -> String

172 |         err n suffix = "Name `\{show n}` is used in target's type, but is not a generated or given parameter (goes after the fuel argument); \{suffix}"

173 |     for targetTypeArgs $ \case

174 |       IVar fc un@(UN argName) => if inGivenOrGenerated argName then pure argName else failAt fc $ err un "did you forget to add one?"

175 |       IVar fc mn@(MN {}) => failAt fc $ err mn "looks like it is an implicit parameter of some underdeclared type; specify types with more precision"

176 |       nonVarArg => failAt (getFC nonVarArg) "Target type's argument must be a variable name, got `\{show nonVarArg}`"

178 |   -- check that all arguments names are unique

179 |   let [] = findDiffPairWhich (==) targetTypeArgs

180 |     | _ :: _ => failAt targetTypeFC "All arguments of the target type must be different"

182 |   -- check the given type info corresponds to the given type application, and convert a `List` to an appropriate `Vect`

183 |   let Yes targetTypeArgsLengthCorrect = targetType.tyArgs.length `decEq` targetTypeArgs.length

184 |     | No _ => fail "INTERNAL ERROR: unequal argument lists lengths: \{show targetTypeArgs.length} and \{show targetType.args.length}"

186 |   ----------------------------------------------------------------------

187 |   -- Check that generated and given parameter lists are actually sets --

188 |   ----------------------------------------------------------------------

190 |   -- check that all parameters in `parametersToBeGenerated` have different names

191 |   let [] = findDiffPairWhich ((==) `on` fst) paramsToBeGenerated

192 |     | (_, (_, ty)) :: _ => failAt (getFC ty) "Name of the argument is not unique in the dependent pair under the resulting `Gen`"

194 |   -- check that all given parameters have different names

195 |   let [] = findDiffPairWhich ((==) `on` \(_, n, _) => n) givenParams

196 |     | (_, (_, _, ty)) :: _ => failAt (getFC ty) "Name of the generator function's argument is not unique"

198 |   -----------------------------------------------------------------------

199 |   -- Link generated and given parameters lists to the `targetTypeArgs` --

200 |   -----------------------------------------------------------------------

202 |   -- check that all parameters to be generated are actually used inside the target type

203 |   paramsToBeGenerated <- for {b=Fin targetType.args.length} paramsToBeGenerated $ \(name, ty) => case findIndex (== name) targetTypeArgs of

204 |     Just found => pure $ rewrite targetTypeArgsLengthCorrect in found

205 |     Nothing => failAt (getFC ty) "Generated parameter is not used in the target type"

207 |   -- check that all target type's parameters classified as "given" are present in the given params list

208 |   givenParams <- for {b=(Fin targetType.args.length, _)} givenParams $ \(explicitness, name, ty) => case findIndex (== name) targetTypeArgs of

209 |     Just found => pure (rewrite targetTypeArgsLengthCorrect in found, explicitness, UN name)

210 |     Nothing => failAt (getFC ty) "Given parameter is not used in the target type"

212 |   -- remember the order of given params as a permutation and forget the order of the given params, convert to a map from index to explicitness

213 |   let Just (givenParams ** givensOrder) = mapAndPerm givenParams

214 |     | Nothing => fail "INTERNAL ERROR: can't compute correct given params permutation"

216 |   -- compute the order of generated params as a permutation

217 |   let gendOrder = orderIndices paramsToBeGenerated

219 |   -- make the resulting signature

220 |   let genSig = MkExternalGenSignature targetType givenParams givensOrder gendOrder

222 |   -------------------------------------

223 |   -- Auto-implicit generators checks --

224 |   -------------------------------------

226 |   -- check that external gen does not have its own external gens

227 |   when (isExternalGen checkSide) $

228 |     when (not $ null autoImplArgs) $

229 |       failAt genFC "Auto-implicit argument should not contain its own auto-implicit arguments"

231 |   -- check all auto-implicit arguments pass the checks for the `Gen` in an appropriate context

232 |   autoImplArgs <- for autoImplArgs $ \tti => mapSnd (,tti) <$> checkTypeIsGen ExternalGen (assert_smaller origsig tti)

234 |   -- check that all auto-imlicit arguments are unique

235 |   let [] = findDiffPairWhich ((==) `on` \(_, sig, _) => sig) autoImplArgs

236 |     | (_, (fc, _)) :: _ => failAt fc.targetTypeFC "Repetition of an auto-implicit external generator"

238 |   -- check that the resulting generator is not in externals

239 |   let Nothing = find ((== genSig) . \(_, sig, _) => sig) autoImplArgs

240 |     | Just (fc, _) => failAt fc.genFC "External generators contain the generator asked to be derived"

242 |   -- forget FCs of subparsed externals

243 |   let autoImplArgs = snd <$> autoImplArgs

245 |   ------------

246 |   -- Result --

247 |   ------------

249 |   case checkSide of

250 |     DerivationTask => do

251 |       let Yes prf = genSig.givenParams.size + autoImplArgs.length `decEq` sigArgs.length

252 |         | No _ => fail $ "INTERNAL ERROR: positions length is incorrect"

253 |                       ++ ", \{show sigArgs.length} is not \{show genSig.givenParams.size} + \{show autoImplArgs.length}"

254 |       pure (genSig ** MkGenExternals autoImplArgs ** rewrite prf in givenParamsPositions)

255 |     ExternalGen    => do

256 |       let fc = MkGenSignatureFC {sigFC=getFC sig, genFC, targetTypeFC}

257 |       pure (fc, genSig)

261 | nameForGen : ExternalGenSignature -> Name

262 | nameForGen sig = let (ty, givs) = characteristics sig in UN $ Basic $ "external^<\{ty}>\{show givs}"

266 | nameMod : Name -> Name

267 | nameMod n = UN $ Basic "outer^<\{show n}>"

269 | internalGenCallingLambda : Elaboration m => CheckResult DerivationTask -> TTImp -> m TTImp

270 | internalGenCallingLambda (sig ** exts ** givsPos) call = do

271 |     let (givensReordered ** lenCorr) = reorder' sig.givenParams.asList sig.givensOrder

272 |     let Just args = joinEithersPos givensReordered exts.externals $ rewrite lenCorr in givsPos

273 |       | Nothing => fail "INTERNAL ERROR: can't join partitioned args back"

274 |     pure $ foldr mkLam call args

276 |   where

278 |   -- either given param or auto param

279 |   mkLam : Either (Fin sig.targetType.args.length, ArgExplicitness, Name) (ExternalGenSignature, TTImp) -> TTImp -> TTImp

280 |   mkLam $ Left (idx, expl, name) = lam $ MkArg MW expl.toTT .| Just (nameMod name) .| implicitTrue -- (index' sig.targetType.args idx).type

281 |                                                                                    -- ^^^ no type because of `nameMod` above

282 |   mkLam $ Right (extSig, ty)     = lam $ MkArg MW AutoImplicit .| Just (nameForGen extSig) .| ty

283 |                                    -- TODO to think whether it's okay to calculate the name twice: here and below for a map

285 | callMainDerivedGen : DerivationClosure m => NamesInfoInTypes => ConsRecs => ExternalGenSignature -> (fuelArg : Name) -> m TTImp

286 | callMainDerivedGen sig fuelArg = do

287 |   let Element intSig prf = internalise sig

288 |   map (reorderGend True sig.gendOrder . fst) $

289 |     callGen intSig (var fuelArg) $ rewrite prf in sig.givenParams.asVect <&> \(_, _, name) => var $ nameMod name

291 | wrapFuel : (fuelArg : Name) -> TTImp -> TTImp

292 | wrapFuel fuelArg = lam $ MkArg MW ExplicitArg (Just fuelArg) `(Data.Fuel.Fuel)

299 | deriveGenExpr : DeriveBodyForType => (signature : TTImp) -> Elab TTImp

300 | deriveGenExpr signature = do

301 |   checkResult@(signature ** externals ** _) <- checkTypeIsGen DerivationTask signature

302 |   let externalsSigToName = fromList $ externals.externals <&> \(sig, _) => (sig, nameForGen sig)

303 |   let fuelArg = outmostFuelArg

304 |   _ <- logBounds Trace "deptycheck.derive.namesInfo" [] $ getNamesInfoInTypes signature.targetType

305 |   _ <- logBounds Trace "deptycheck.derive.consRec" [] getConsRecs

306 |   (callExpr, locals) <- runCanonic externalsSigToName $ callMainDerivedGen signature fuelArg

307 |   wrapFuel fuelArg <$> internalGenCallingLambda checkResult (local locals callExpr)

346 | export %macro

347 | deriveGen : DeriveBodyForType => Elab a

348 | deriveGen = do

349 |   Just signature <- goal

350 |      | Nothing => fail "The goal signature is not found. Generators derivation must be used only for fully defined signatures"

351 |   tt <- deriveGenExpr signature

352 |   check tt

366 | export %macro

367 | deriveGenFor : DeriveBodyForType => (0 a : Type) -> Elab a

368 | deriveGenFor a = do

369 |   sig <- quote a

370 |   tt <- deriveGenExpr sig

371 |   check tt

378 | deriveGenPrinter : {default True printTTImp : _} -> {default True logDerivation : _} -> DeriveBodyForType => (0 a : Type) -> Elab Unit

379 | deriveGenPrinter ty = do

380 |   ty <- quote ty

381 |   when logDerivation $ declare `[%logging "deptycheck.derive.print" 5; %logging "deptycheck.derive.least-effort" 7]

382 |   logSugaredTerm "deptycheck.derive.print" (toNatLevel Details) "type" ty

383 |   expr <- deriveGenExpr ty

384 |   expr <- quote expr

385 |   printTTImp <- quote printTTImp

386 |   declare `[

387 |     export

388 |     main : IO Unit

389 |     main = do

390 |       putStr $ if ~printTTImp then interpolate ~expr else show ~expr

391 |       putStrLn ""

392 |   ]

398 | %defaulthint %inline

399 | public export

400 | DefaultConstructorDerivator : DeriveBodyRhsForCon

401 | DefaultConstructorDerivator = LeastEffort