[ refactor ] Try to use simpler data structures and less convertions

src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr

@@ -43,13 +43,14 @@ record Determination (0 con : Con) where
 mapDetermination : {0 con : Con} -> (SortedSet (Fin con.args.length) -> SortedSet (Fin con.args.length)) -> Determination con -> Determination con
 mapDetermination f $ MkDetermination sda da wda = MkDetermination (f sda) (f da) (f wda)
 
-removeDeeply : (toRemove : SortedSet $ Fin con.args.length) ->
+removeDeeply : Foldable f =>
+               (toRemove : f $ Fin con.args.length) ->
                (fromWhat : SortedMap .| Fin con.args.length .| Determination con) ->
                SortedMap .| Fin con.args.length .| Determination con
-removeDeeply toRemove fromWhat = foldl delete' fromWhat (SortedSet.toList toRemove) <&> mapDetermination (`difference` toRemove)
+removeDeeply toRemove fromWhat = foldl delete' fromWhat toRemove <&> mapDetermination (\s => foldl delete' s toRemove)
 
 searchOrder : (left : SortedMap .| Fin con.args.length .| Determination con) ->
-              List $ SortedSet $ Fin con.args.length
+              List $ Fin con.args.length
 searchOrder left = do
   -- find all arguments that are not stongly determined by anyone
   let nonStronglyDetermined = filter (\(_, det) => null det.stronglyDeterminingArgs) $ SortedMap.toList left
@@ -67,13 +68,13 @@ searchOrder left = do
   let determined = concatMap (determinableArgs . snd) curr
 
   -- clean up representation
-  let curr = SortedSet.fromList $ fst <$> curr
+  let curr = fst <$> curr
 
   -- remove information about all currently chosen args
-  let next = removeDeeply (curr `union` determined) left
+  let next = removeDeeply curr $ removeDeeply determined left
 
   -- `next` is smaller than `left` because `curr` must be not empty
-  curr :: searchOrder (assert_smaller left next)
+  curr ++ searchOrder (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.
@@ -216,14 +217,11 @@ namespace NonObligatoryExts
           updWeakDeterm $ Both d w = {weaklyDeterminingArgs := w} d
       let determ = cozipWith updWeakDeterm determ canBeDetermined
 
-      -- Compute all possible appropriate orders
-      let abstractOrder = searchOrder $ removeDeeply givs determ
-
       --------------------------
       -- Producing the result --
       --------------------------
 
-      let theOrder = abstractOrder >>= SortedSet.toList
+      let theOrder = searchOrder $ removeDeeply givs determ
 
       logPoint {level=10} "least-effort.order" [sig, con] "- used final order: \{show theOrder}"