Skip to content

Commit

Permalink
[ perf ] Do not recalculate determinable each time
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Sep 24, 2024
1 parent 75c6d0e commit e29b575
Showing 1 changed file with 5 additions and 6 deletions.
11 changes: 5 additions & 6 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
Original file line number Diff line number Diff line change
Expand Up @@ -48,12 +48,10 @@ removeDeeply : Foldable f =>
removeDeeply toRemove fromWhat = foldl delete' fromWhat toRemove <&> mapDetermination (\s => foldl delete' s toRemove)

searchOrder : {con : _} ->
(determinable : SortedSet $ Fin con.args.length) ->
(left : FinMap con.args.length $ Determination con) ->
List $ Fin con.args.length
searchOrder left = do

-- compute arguments that are determinable by any other argument
let determinable = concatMap determinableArgs left
searchOrder determinable left = do

-- find all arguments that are not stongly determined by anyone, among them find all that are not determined even weakly, if any
let notDetermined = filter (\(idx, det) => not (contains idx determinable) && null det.stronglyDeterminingArgs) $ kvList left
Expand All @@ -75,7 +73,7 @@ searchOrder left = do
let next = removeDeeply .| Id curr .| removeDeeply determined left

-- `next` is smaller than `left` because `curr` must be not empty
curr :: searchOrder (assert_smaller left next)
curr :: searchOrder (determinable `difference` determined) (assert_smaller left next)

||| "Non-obligatory" means that some present external generator of some type
||| may be ignored even if its type is really used in a generated data constructor.
Expand Down Expand Up @@ -212,7 +210,8 @@ namespace NonObligatoryExts
logPoint {level=15} "least-effort" [sig, con] "- determ: \{determ}"
logPoint {level=15} "least-effort" [sig, con] "- givs: \{givs}"

let theOrder = searchOrder $ removeDeeply givs determ
let nonDetermGivs = removeDeeply givs determ
let theOrder = searchOrder (concatMap determinableArgs nonDetermGivs) nonDetermGivs

logPoint {level=10} "least-effort" [sig, con] "- used final order: \{theOrder}"

Expand Down

0 comments on commit e29b575

Please sign in to comment.