1 | module Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Impl

  3 | import public Control.Monad.State

  4 | import public Control.Monad.State.Tuple

  6 | import public Data.Collections.Analysis

  7 | import public Data.Either

  8 | import public Data.Fin.Map

  9 | import public Data.SortedSet.Extra

 10 | import public Data.Vect.Ex

 12 | import public Decidable.Equality

 14 | import public Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Interface

 15 | import public Deriving.DepTyCheck.Gen.Labels

 16 | import public Deriving.DepTyCheck.Gen.Tuning

 18 | %default total

 24 | record Determination (0 con : Con) where

 25 |   constructor MkDetermination

 26 |   ||| Args which cannot be determined by this arg, e.g. because it is used in a non-trivial expression.

 27 |   stronglyDeterminingArgs : SortedSet $ Fin con.args.length

 28 |   ||| Args which this args depends on, which are not strongly determining.

 29 |   argsDependsOn : SortedSet $ Fin con.args.length

 30 |   ||| Count of influencing arguments

 31 |   influencingArgs : Nat

 33 | mapDetermination : {0 con : Con} -> (SortedSet (Fin con.args.length) -> SortedSet (Fin con.args.length)) -> Determination con -> Determination con

 34 | mapDetermination f oldDet = do

 35 |   let newDet : Determination con := {stronglyDeterminingArgs $= f, argsDependsOn $= f} oldDet

 36 |   let patchInfl = if null (newDet.stronglyDeterminingArgs) && not (null oldDet.stronglyDeterminingArgs) then S else id

 37 |   ({influencingArgs $= patchInfl} newDet)

 39 | removeDeeply : Foldable f =>

 40 |                (toRemove : f $ Fin con.args.length) ->

 41 |                (fromWhat : FinMap con.args.length $ Determination con) ->

 42 |                FinMap con.args.length $ Determination con

 43 | removeDeeply toRemove fromWhat = foldl delete' fromWhat toRemove <&> mapDetermination (\s => foldl delete' s toRemove)

 45 | record TypeApp (0 con : Con) where

 46 |   constructor MkTypeApp

 47 |   argHeadType : TypeInfo

 48 |   {auto 0 argHeadTypeGood : AllTyArgsNamed argHeadType}

 49 |   argApps : Vect argHeadType.args.length .| Either (Fin con.args.length) TTImp

 51 | getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length (Either (FC, String) $ TypeApp con, Determination con)

 52 | getTypeApps con = do

 53 |   let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName' arg, idx)

 55 |   -- Analyse that we can do subgeneration for each constructor argument

 56 |   -- Fails using `Elaboration` if the given expression is not an application to a type constructor

 57 |   let analyseTypeApp : TTImp -> m (Either (FC, String) $ TypeApp con, Determination con)

 58 |       analyseTypeApp expr = do

 59 |         let (lhs, args) = unAppAny expr

 60 |         let as = args.asVect <&> \arg => case getExpr arg of

 61 |                    expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs

 62 |                    expr            => Right expr

 63 |         ty <- case lhs of

 64 |           IVar _ lhsName     => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type`

 65 |                                      | Just found => pure $ pure found

 66 |                                    -- we haven't found, failing, there are at least two reasons

 67 |                                    if isNamespaced lhsName

 68 |                                      then failAt (getFC lhs) "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)"

 69 |                                      else pure $ Left (getFC lhs, "Unsupported applications to a non-concrete type `\{lhsName}` in \{show con.name}")

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

 71 |           IType _            => pure $ pure typeInfoForTypeOfTypes

 72 |           lhs@(IPi {})       => pure $ Left (getFC lhs, "Fields with function types are not supported in constructors, like in \{show con.name}")

 73 |           lhs                => pure $ Left (getFC lhs, "Unsupported type of a constructor's \{show con.name} field: \{show lhs}")

 74 |         ta <- Prelude.for ty $ \ty : TypeInfo => do

 75 |           let Yes lengthCorrect = decEq ty.args.length args.length

 76 |             | No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application"

 77 |           _ <- ensureTyArgsNamed ty

 78 |           pure $ MkTypeApp ty $ rewrite lengthCorrect in as

 79 |         let strongDetermination = rights as.asList <&> mapMaybe (lookup' conArgIdxs) . allVarNames

 80 |         let strongDeterminationWeight = concatMap @{Additive} (max 1 . length) strongDetermination -- we add 1 for constant givens

 81 |         let stronglyDeterminedBy = fromList $ join strongDetermination

 82 |         let argsDependsOn = fromList (lefts as.asList) `difference` stronglyDeterminedBy

 83 |         pure (ta, MkDetermination stronglyDeterminedBy argsDependsOn $ argsDependsOn.size + strongDeterminationWeight)

 85 |   for con.args.asVect $ analyseTypeApp . type

 87 | enrichStrongDet : FinMap con.args.length (Determination con) -> List (Fin con.args.length) -> List (Fin con.args.length)

 88 | enrichStrongDet determ xs = go xs xs where

 89 |   go : (acc : List $ Fin con.args.length) -> List (Fin con.args.length) -> List (Fin con.args.length)

 90 |   go acc [] = acc

 91 |   go acc (x::xs) = do

 92 |     let subx = fromMaybe empty $ stronglyDeterminingArgs <$> Fin.Map.lookup x determ

 93 |     let subx = Prelude.toList $ foldl delete' subx $ x :: acc

 94 |     assert_total $ go (subx ++ acc) (xs ++ subx) -- total since we wouldn't add repeating elements and the thus we're closer to the full list

101 | refineBasePri : Num p => {con : _} -> FinMap con.args.length (Determination con, p) -> FinMap con.args.length (Determination con, p)

102 | refineBasePri ps = snd $ execState (Fin.Set.empty {n=con.args.length}, ps) $ traverse_ go $ List.allFins _ where

103 |   go : (visited : MonadState (FinSet con.args.length) m) =>

104 |        (pris : MonadState (FinMap con.args.length (Determination con, p)) m) =>

105 |        Monad m =>

106 |        Fin con.args.length ->

107 |        m ()

108 |   go curr = do

110 |     visited <- get

111 |     -- if we already managed the current item, then exit

112 |     let False = Fin.Set.contains curr visited | True => pure ()

113 |     -- remember that we are in charge of the current item

114 |     let visited = Fin.Set.insert curr visited

115 |     put visited

117 |     let Just (det, currPri) = lookup curr !(get @{pris}) | Nothing => pure ()

119 |     let unvisitedDeps = fromFoldable $ det.argsDependsOn `union` det.stronglyDeterminingArgs

121 |     -- run this for all dependences

122 |     for_ (unvisitedDeps `difference` visited) $ assert_total go

124 |     -- compute what needs to be added to the current priority

125 |     newPri <- do

126 |       pris <- get @{pris}

127 |       pure $ foldl (\curr => maybe curr ((curr+) . snd) . lookup' pris) currPri unvisitedDeps

129 |     -- update the priority of the currently managed argument

130 |     modify $ updateExisting (mapSnd $ const newPri) curr

132 | propagateStrongDet, propagateDep : Ord a => FinMap con.args.length (Determination con, a) -> FinMap con.args.length (Determination con, a)

134 | propagateDep dets = dets <&> \(det, pri) => (det,) $ foldl (\x => maybe x (max x . snd) . lookup' dets) pri $ det.argsDependsOn

136 | propagateStrongDet dets =

137 |   foldl (\dets, (det, pri) => foldl (flip $ updateExisting $ map $ max pri) dets det.stronglyDeterminingArgs) dets dets

139 | propagatePri : Ord a => FinMap con.args.length (Determination con, a) -> FinMap con.args.length (Determination con, a)

140 | propagatePri dets = do

141 |   let next = propagatePriOnce dets

142 |   if ((==) `on` map snd) dets next

143 |     then dets

144 |     else assert_total propagatePri next

145 |   where

146 |     propagatePriOnce : FinMap con.args.length (Determination con, a) -> FinMap con.args.length (Determination con, a)

147 |     propagatePriOnce = propagateDep . propagateStrongDet

149 | data PriorityOrigin = Original | Propagated

151 | Eq PriorityOrigin where

152 |   Original   == Original   = True

153 |   Propagated == Propagated = True

154 |   _ == _ = False

156 | Ord PriorityOrigin where

157 |   compare Original   Original   = EQ

158 |   compare Original   Propagated = GT

159 |   compare Propagated Original   = LT

160 |   compare Propagated Propagated = EQ

165 | assignPriorities : {con : _} -> FinMap con.args.length (Determination con) -> FinMap con.args.length (Determination con, Nat, PriorityOrigin, Nat)

166 | assignPriorities dets = do

167 |   let invStrongDetPwr = do

168 |     let _ : Monoid Nat = Additive

169 |     flip concatMap dets $ \det => fromList $ (,1) <$> det.stronglyDeterminingArgs.asList

170 |   -- the original priority is the count of already determined given arguments for each argument

171 |   let origPri = refineBasePri $ dets <&> \det => (det,) $ det.influencingArgs `minus` det.argsDependsOn.size

172 |   Fin.Map.mapWithKey' .| map snd origPri `zip` propagatePri origPri .| \idx, (origPri, det, newPri) =>

173 |     (det, newPri, if origPri == newPri then Original else Propagated, fromMaybe 0 (Fin.Map.lookup idx invStrongDetPwr) + det.argsDependsOn.size)

175 | findFirstMax : Ord p => List (a, b, p) -> Maybe (a, b)

176 | findFirstMax [] = Nothing

177 | findFirstMax ((x, y, pri)::xs) = Just $ go (x, y) pri xs where

178 |   go : (a, b) -> p -> List (a, b, p) -> (a, b)

179 |   go curr _       []                = curr

180 |   go curr currPri ((x, y, pri)::xs) = if pri > currPri then go (x, y) pri xs else go curr currPri xs

182 | searchOrder : {con : _} ->

183 |               (left : FinMap con.args.length $ Determination con) ->

184 |               List $ Fin con.args.length

185 | searchOrder left = do

187 |   -- find all arguments that are not strongly determined by anyone, among them find all that are not determined even weakly, if any

188 |   let notDetermined = filter (\(idx, det, _) => null det.stronglyDeterminingArgs) $ kvList $ assignPriorities left

190 |   -- choose the one from the variants

191 |   -- It's important to do so, since after discharging one of the selected variable, set of available variants can extend

192 |   -- (e.g. because of discharging of strong determination), and new alternative have more priority than current ones.

193 |   -- TODO to determine the best among current variants taking into account which indices are more complex (transitively!)

194 |   let Just (curr, currDet) = findFirstMax notDetermined

195 |     | Nothing => []

197 |   -- remove information about all currently chosen args

198 |   let next = removeDeeply .| Id curr .| removeDeeply currDet.argsDependsOn left

200 |   -- `next` is smaller than `left` because `curr` must be not empty

201 |   curr :: searchOrder (assert_smaller left next)

203 | callCon : (con : Con) -> Vect con.args.length TTImp -> TTImp

204 | callCon con = reAppAny (var con.name) . toList . mapI (appArg . index' con.args)

224 | [LeastEffort] DeriveBodyRhsForCon where

225 |   consGenExpr sig con givs fuel = do

227 |     -------------------------------------------------------------

228 |     -- Prepare intermediate data and functions using this data --

229 |     -------------------------------------------------------------

231 |     -- Compute left-to-right need of generation when there are non-trivial types at the left

232 |     (argsTypeApps, argsDeterms) <- unzip <$> getTypeApps con

234 |     -- Decide how constructor arguments would be named during generation

235 |     let bindNames = argName' <$> fromList con.args

237 |     -- Get arguments which any other argument depends on

238 |     let dependees = dependees con.args

240 |     -- Form the expression of calling the current constructor

241 |     let callCons = do

242 |       let constructorCall = callCon con $ bindNames.withIdx <&> \(idx, n) => if contains idx dependees then implicitTrue else var n

243 |       let wrapImpls : Nat -> TTImp

244 |           wrapImpls Z     = constructorCall

245 |           wrapImpls (S n) = var `{Builtin.DPair.MkDPair} .$ implicitTrue .$ wrapImpls n

246 |       let consExpr = wrapImpls $ sig.targetType.args.length `minus` sig.givenParams.size

247 |       `(Prelude.pure {f=Test.DepTyCheck.Gen.Gen _} ~consExpr)

249 |     -- Derive constructor calling expression for given order of generation

250 |     let genForOrder : List (Fin con.args.length) -> m TTImp

251 |         -- ... state is the set of arguments that are already present (given or generated)

252 |         genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do

254 |           -- Get info for the `genedArg`

255 |           let Right $ MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ Either _ $ TypeApp con) argsTypeApps

256 |             | Left (fc, str) => failAt fc str

258 |           -- Acquire the set of arguments that are already present

259 |           presentArguments <- get

261 |           -- TODO to put the following check as up as possible as soon as it typecheks O_O

262 |           -- Check that those argument that we need to generate is not already present

263 |           let False = contains genedArg presentArguments

264 |             | True => pure id

266 |           -- Filter arguments classification according to the set of arguments that are left to be generated;

267 |           -- Those which are `Right` are given, those which are `Left` are needs to be generated.

268 |           let depArgs : Vect typeOfGened.args.length (Either (Fin con.args.length) TTImp) := argsOfTypeOfGened <&> \case

269 |             Right expr => Right expr

270 |             Left i     => if contains i presentArguments then Right $ var $ index i bindNames else Left i

272 |           -- Determine which arguments will be on the left of dpair in subgen call, in correct order

273 |           let subgeneratedArgs = mapMaybe getLeft $ toList depArgs

275 |           -- Make sure generated arguments will not be generated again

276 |           modify $ insert genedArg . union (fromList subgeneratedArgs)

278 |           -- Form a task for subgen

279 |           let (subgivensLength ** subgivens) = mapMaybe (\(ie, idx) => (idx,) <$> getRight ie) $ depArgs `zip` Fin.range

280 |           let subsig : GenSignature := MkGenSignature typeOfGened $ fromList $ fst <$> toList subgivens

281 |           let Yes Refl = decEq subsig.givenParams.size subgivensLength

282 |             | No _ => fail "INTERNAL ERROR: error in given params set length computation"

284 |           -- Check if called subgenerator can call the current one

285 |           let mutRec = hasNameInsideDeep sig.targetType.name $ var subsig.targetType.name

287 |           -- Decide whether to use local (decreasing) or outmost fuel, depending on whether we are in mutual recursion with subgen

288 |           let subfuel = if mutRec then fuel else var outmostFuelArg

290 |           -- Form an expression to call the subgen

291 |           (subgenCall, reordering) <- callGen subsig subfuel $ snd <$> subgivens

293 |           -- Form an expression of binding the result of subgen

294 |           let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames

295 |           let Just subgeneratedArgs = reorder'' reordering subgeneratedArgs

296 |             | Nothing => fail "INTERNAL ERROR: cannot reorder subgenerated arguments"

297 |           let bindSubgenResult = foldr (\l, r => var `{Builtin.DPair.MkDPair} .$ l .$ r) genedArg subgeneratedArgs

299 |           -- Form an expression of the RHS of a bind; simplify lambda if subgeneration result type does not require pattern matching

300 |           let bindRHS = \cont => case bindSubgenResult of

301 |                                    IBindVar _ n => lam (MkArg MW ExplicitArg (Just n) implicitFalse) cont

302 |                                    _            => `(\ ~bindSubgenResult => ~cont)

304 |           -- Chain the subgen call with a given continuation

305 |           pure $ \cont => `(~subgenCall >>= ~(bindRHS cont))

307 |     --------------------------------------------

308 |     -- Compute possible orders of generation ---

309 |     --------------------------------------------

311 |     -- Compute determination map without weak determination information

312 |     let determ = insertFrom' empty $ withIndex argsDeterms

314 |     logPoint Debug "deptycheck.derive.least-effort" [sig, con] "- determ: \{determ}"

315 |     logPoint Debug "deptycheck.derive.least-effort" [sig, con] "- givs: \{givs}"

317 |     -- Find user-imposed tuning of the order

318 |     userImposed <- findUserImposedDeriveFirst

320 |     -- Compute the order

321 |     let nonDetermGivs = removeDeeply givs determ

322 |     let userImposed = enrichStrongDet nonDetermGivs userImposed

323 |     let theOrder = userImposed ++ searchOrder (removeDeeply userImposed nonDetermGivs)

325 |     logPoint FineDetails "deptycheck.derive.least-effort" [sig, con] "- used final order: \{theOrder}"

327 |     --------------------------

328 |     -- Producing the result --

329 |     --------------------------

331 |     with FromString.(.label)

332 |     labelGen "\{show con.name} (orders)".label <$> genForOrder theOrder

334 |     where

336 |       Interpolation (Fin con.args.length) where

337 |         interpolate i = case name $ index' con.args i of

338 |           Just (UN n) => "#\{show i} (\{show n})"

339 |           _           => "#\{show i}"

341 |       Foldable f => Interpolation (f $ Fin con.args.length) where

342 |         interpolate = ("[" ++) . (++ "]") . joinBy ", " . map interpolate . toList

344 |       Interpolation (Determination con) where

345 |         interpolate ta = "<=\{ta.stronglyDeterminingArgs} ->\{ta.argsDependsOn}"

347 |       findUserImposedDeriveFirst : m $ List $ Fin con.args.length

348 |       findUserImposedDeriveFirst = do

349 |         Just impl <- search $ GenOrderTuning $ Con.name con | Nothing => pure []

350 |         pure () -- WTF is going on? If you remove this, elaborator script hangs O_O

351 |         let Yes tyLen = decEq (isConstructor @{impl}).fst.typeInfo.args.length sig.targetType.args.length

352 |           | No _ => fail "INTERNAL ERROR: type args length of found gen order tuning is wrong"

353 |         let Yes conLen = decEq (isConstructor @{impl}).fst.conInfo.args.length con.args.length

354 |           | No _ => fail "INTERNAL ERROR: con args length of found gen order tuning is wrong"

355 |         -- TODO to get rid of `believe_me` below

356 |         let df = believe_me $ deriveFirst @{impl} (rewrite tyLen in Prelude.toList sig.givenParams) (rewrite conLen in Prelude.toList givs)

357 |         let userImposed = filter (not . contains' givs) $ nub $ conArgIdx <$> df

358 |         logValue FineDetails "deptycheck.derive.least-effort" [sig, con] "- user-imposed: \{userImposed}" userImposed