[ fixup ] Concentrate on particular highest-priority arguments

buzden · Oct 22, 2024 · 61b9d79 · 61b9d79
1 parent d83acdf
commit 61b9d79
Showing 1 changed file with 15 additions and 3 deletions.
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -88,6 +88,17 @@ removeDeeply : Foldable f =>
                FinMap con.args.length $ Determination con
 removeDeeply toRemove fromWhat = foldl delete' fromWhat toRemove <&> mapDetermination (\s => foldl delete' s toRemove)
 
+record ArgPriority (0 con : Con) where
+  constructor Pri
+  givenTyArguments  : Nat
+  targetConArgument : Fin con.args.length
+
+Eq (ArgPriority con) where
+  Pri gta tca == Pri gta' tca' = gta == gta' && tca == tca'
+
+Ord (ArgPriority con) where
+  compare (Pri gta tca) (Pri gta' tca') = compare gta gta' <+> compare @{Reverse} tca tca'
+
 propagatePriOnce : Ord p => FinMap con.args.length (Determination con, p) -> FinMap con.args.length (Determination con, p)
 propagatePriOnce =
   -- propagate back along dependencies
@@ -125,10 +136,11 @@ Ord PriorityOrigin where
 
 -- compute the priority
 -- priority is a count of given arguments, and it propagates back using `max` on strongly determining arguments and on arguments that depend on this
-propagatePri' : FinMap con.args.length (Determination con) -> FinMap con.args.length (Determination con, Nat, PriorityOrigin)
+propagatePri' : {con : _} -> FinMap con.args.length (Determination con) -> FinMap con.args.length (Determination con, ArgPriority con, PriorityOrigin)
 propagatePri' dets = do
-  let origPri = dets <&> \det => (det,) $ det.typeArgs `minus` det.argsDependsOn.size
-  map snd origPri `zip` propagatePri origPri <&> \(origPri, det, newPri) => (det, newPri, if origPri == newPri then Original else Propagated)
+  let origPri = fromList $ kvList dets <&> \(idx, det) => (idx, det,) $ Pri (det.typeArgs `minus` det.argsDependsOn.size) idx
+  map snd origPri `zip` propagatePri origPri <&>
+    \(origPri, det, newPri) => (det, newPri, if ((==) `on` givenTyArguments) origPri newPri then Original else Propagated)
 
 searchOrder : {con : _} ->
               (determinable : SortedSet $ Fin con.args.length) ->