diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 05cda82d..cf5b1452 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -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 @@ -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. @@ -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}"