1	# NonDominatedSort — C# Unsga3.Core.NonDominatedSort.
2	# Fast non-dominated sorting by peeling (Deb et al.).
3	# `sort` uses Deb constraint-domination: feasible beats infeasible;
4	# both infeasible and unequal CV → smaller CV; equal CV is mutual
5	# non-domination (objectives are not compared). Both feasible → Pareto.
6	# `dominates` stays the Pareto predicate (law dominates_irreflexive).
7	# Zero constraints (cv 0) keeps today's Pareto fronts.
8	#
9	# Layout (Bend guide: Arrays cannot ride a fork tree; List.get is a
10	# cons walk): one sequential pass materializes `Row{index, objectives, cv}`
11	# so the peel never `List.get`s a fat Individual. Per-candidate split
12	# still mid-splits `a b = f(lo) f(hi)` (same front/leftover order as
13	# the tail-first walk). Inner is_dominated stays a sequential OR so a
14	# first hit skips the rest. Same ranks and index order when every cv is 0.
15	
16	import Base
17	import ./individual.bend as Ind
18	import ./util.bend as Util
19	
20	# One sort-row: population index plus the objective vector. Built once
21	# per `sort`; leftover peels reuse the same rows (no re-index).
22	type Row is Data:
23	  Row{
24	    i: Nat
25	    f: List<&2, F32>
26	    cv: F32
27	  }
28	
29	def row_idx(r: Row) -> Nat:
30	  match r:
31	    case Row{i, f, cv}:
32	      i
33	
34	def row_f(r: Row) -> List<&2, F32>:
35	  match r:
36	    case Row{i, f, cv}:
37	      f
38	
39	def row_cv(r: Row) -> F32:
40	  match r:
41	    case Row{i, f, cv}:
42	      cv
43	
44	def rows_of.go(pop: List<&2, Ind.Individual>, +i: Nat) -> List<&2, Row>:
45	  match pop:
46	    case Nil{}:
47	      Nil{}
48	    case +h <> t:
49	      Row{i, Ind.objectives(h), Ind.constraint_violation(h)} <> rows_of.go(t, 1n+i)
50	
51	def rows_of(+pop: List<&2, Ind.Individual>) -> List<&2, Row>:
52	  rows_of.go(pop, 0n)
53	
54	def row_idxs(rs: List<&2, Row>) -> List<&2, Nat>:
55	  match rs:
56	    case Nil{}:
57	      Nil{}
58	    case +r <> t:
59	      row_idx(r) <> row_idxs(t)
60	
61	def verdict.a(bb: Bool) -> Nat:
62	  match bb:
63	    case True{}:
64	      0n
65	    case False{}:
66	      1n
67	
68	def verdict.b(bb: Bool) -> Nat:
69	  match bb:
70	    case True{}:
71	      2n
72	    case False{}:
73	      0n
74	
75	# Minimization: 0n = mutual non-domination, 1n = a dominates b, 2n = b dominates a.
76	def verdict(ab: Bool, bb: Bool) -> Nat:
77	  match ab:
78	    case True{}:
79	      verdict.a(bb)
80	    case False{}:
81	      verdict.b(bb)
82	
83	def compare_pareto.go(a: List<&2, F32>, b: List<&2, F32>, ab: Bool, bb: Bool) -> Nat:
84	  # Unequal lengths: mutual non-domination (0), even if the shared prefix
85	  # is strictly better. C# ComparePareto throws. ZDT/DTLZ use one length.
86	  # Locked by src/nds_unequal.bend.
87	  match a b:
88	    case Nil{} Nil{}:
89	      verdict(ab, bb)
90	    case +x <> xs +y <> ys:
91	      compare_pareto.go(xs, ys, Bool.or(ab, F32.is_lt(x, y)), Bool.or(bb, F32.is_lt(y, x)))
92	    case Nil{} y <> ys:
93	      0n
94	    case x <> xs Nil{}:
95	      0n
96	
97	def compare_pareto(a: List<&2, F32>, b: List<&2, F32>) -> Nat:
98	  compare_pareto.go(a, b, False{}, False{})
99	
100	# Equal CV among infeasible points: 0. Deb does not Pareto-compare.
101	# C# CompareConstraintDominated on published main falls through to
102	# Pareto; this tree does not (Deb / constraint-domination target).
103	def compare_cd.infeas(+cva: F32, +cvb: F32, a_lt: Bool, b_lt: Bool) -> Nat:
104	  match a_lt:
105	    case True{}:
106	      1n
107	    case False{}:
108	      match b_lt:
109	        case True{}:
110	          2n
111	        case False{}:
112	          0n
113	
114	# 0 mutual, 1 a dominates b, 2 b dominates a.
115	# Feasible (cv ≤ 0) beats infeasible. Both feasible → Pareto,
116	# including unequal objective lengths (mutual non-domination).
117	def compare_cd.feas(
118	  +fa: List<&2, F32>,
119	  +fb: List<&2, F32>,
120	  +cva: F32,
121	  +cvb: F32,
122	  a_feas: Bool,
123	  b_feas: Bool
124	) -> Nat:
125	  match a_feas b_feas:
126	    case True{} True{}:
127	      compare_pareto(fa, fb)
128	    case True{} False{}:
129	      1n
130	    case False{} True{}:
131	      2n
132	    case False{} False{}:
133	      compare_cd.infeas(cva, cvb, F32.is_lt(cva, cvb), F32.is_lt(cvb, cva))
134	
135	def compare_cd(+fa: List<&2, F32>, +fb: List<&2, F32>, +cva: F32, +cvb: F32) -> Nat:
136	  compare_cd.feas(fa, fb, cva, cvb, F32.is_le(cva, 0.0), F32.is_le(cvb, 0.0))
137	
138	def compare_constraint(+a: Ind.Individual, +b: Ind.Individual) -> Nat:
139	  compare_cd(Ind.objectives(a), Ind.objectives(b), Ind.constraint_violation(a), Ind.constraint_violation(b))
140	
141	def dominates.is1(p: Nat) -> Bool:
142	  match p:
143	    case 0n:
144	      True{}
145	    case 1n+q:
146	      False{}
147	
148	def dominates.fin(c: Nat) -> Bool:
149	  match c:
150	    case 0n:
151	      False{}
152	    case 1n+p:
153	      dominates.is1(p)
154	
155	# Pareto only. Irreflexivity is closed in PROOF.bend on this predicate.
156	# `sort` uses compare_cd, not this function.
157	def dominates(a: Ind.Individual, b: Ind.Individual) -> Bool:
158	  dominates.fin(compare_pareto(Ind.objectives(a), Ind.objectives(b)))
159	
160	def dominates_ff(+fa: List<&2, F32>, +fb: List<&2, F32>) -> Bool:
161	  dominates.fin(compare_pareto(fa, fb))
162	
163	def dominates_cd(+fa: List<&2, F32>, +cva: F32, +fb: List<&2, F32>, +cvb: F32) -> Bool:
164	  dominates.fin(compare_cd(fa, fb, cva, cvb))
165	
166	# Sequential OR so a first hit can skip the rest. Candidate-level
167	# parallelism lives in split_walk (coarse mid-split). Walks `all`
168	# rows directly — no List.get into the population.
169	def is_dominated(+all: List<&2, Row>, +i: Nat, +fi: List<&2, F32>, +cvi: F32) -> Bool:
170	  match all:
171	    case Nil{}:
172	      False{}
173	    case +r <> rs:
174	      match r:
175	        case Row{+j, +fj, +cvj}:
176	          Bool.or(
177	            Bool.and(Bool.not(Nat.is_eq(i, j)), dominates_cd(fj, cvj, fi, cvi)),
178	            is_dominated(rs, i, fi, cvi)
179	          )
180	
181	def row_dom(+all: List<&2, Row>, +r: Row) -> Bool:
182	  match r:
183	    case Row{+i, +f, +cv}:
184	      is_dominated(all, i, f, cv)
185	
186	# Split remaining into (front indices, leftover rows). Same front
187	# membership and leftover order as the old index-list peel.
188	# |front| + |leftover| = |remaining| by construction.
189	type Split is Data:
190	  Split{
191	    ff: List<&2, Nat>
192	    ot: List<&2, Row>
193	  }
194	
195	def split_put(+r: Row, s: Split, dominated: Bool) -> Split:
196	  match s:
197	    case Split{ff, ot}:
198	      match dominated:
199	        case True{}:
200	          Split{ff, r <> ot}
201	        case False{}:
202	          Split{row_idx(r) <> ff, ot}
203	
204	def split_cat(a: Split, b: Split) -> Split:
205	  match a b:
206	    case Split{ff1, ot1} Split{ff2, ot2}:
207	      Split{List.append(&2, Nat, ff1, ff2), List.append(&2, Row, ot1, ot2)}
208	
209	# Per-candidate split is independent given `all`. Mid-split then
210	# concatenate fronts / leftovers so order matches the tail-first walk.
211	def split_walk.go(+all: List<&2, Row>, +fuel: Nat, cand: List<&2, Row>) -> Split:
212	  match fuel cand:
213	    case 0n Nil{}:
214	      Split{Nil{}, Nil{}}
215	    case 0n +r <> rest:
216	      split_put(r, split_walk.go(all, 0n, rest), row_dom(all, r))
217	    case 1n+p Nil{}:
218	      Split{Nil{}, Nil{}}
219	    case 1n+p +r <> Nil{}:
220	      split_put(r, Split{Nil{}, Nil{}}, row_dom(all, r))
221	    case 1n+p h <> t:
222	      +xs = {h <> t : List<&2, Row>}
223	      +mid = Nat.div(Util.list_len(Row, xs), 2n)
224	      lo hi = split_walk.go(all, p, List.take(&2, Row, xs, mid)) split_walk.go(all, p, List.drop(&2, Row, xs, mid))
225	      split_cat(lo, hi)
226	
227	def split_walk(+all: List<&2, Row>, +cand: List<&2, Row>) -> Split:
228	  split_walk.go(all, Util.list_len(Row, cand), cand)
229	
230	# Empty first front (unreachable on a finite Pareto set) keeps the head
231	# so peel stays a partition.
232	def split_ne(+r: Row, +rest: List<&2, Row>, s: Split) -> Split:
233	  match s:
234	    case Split{ff, ot}:
235	      match ff:
236	        case Nil{}:
237	          Split{row_idx(r) <> Nil{}, rest}
238	        case h <> t:
239	          Split{h <> t, ot}
240	
241	def split_front(remaining: List<&2, Row>) -> Split:
242	  match remaining:
243	    case Nil{}:
244	      Split{Nil{}, Nil{}}
245	    case +r <> +rest:
246	      split_ne(r, rest, split_walk(r <> rest, r <> rest))
247	
248	def split_fst(s: Split) -> List<&2, Nat>:
249	  match s:
250	    case Split{ff, ot}:
251	      ff
252	
253	def split_snd(s: Split) -> List<&2, Row>:
254	  match s:
255	    case Split{ff, ot}:
256	      ot
257	
258	def peel(fuel: Nat, remaining: List<&2, Row>) -> List<&2, List<&2, Nat>>:
259	  match fuel remaining:
260	    case 0n Nil{}:
261	      Nil{}
262	    case 1n+f Nil{}:
263	      Nil{}
264	    case 0n +r <> +rest:
265	      row_idxs({r <> rest : List<&2, Row>}) <> Nil{}
266	    case 1n+f +r <> +rest:
267	      +s = split_front({r <> rest : List<&2, Row>})
268	      split_fst(s) <> peel(f, split_snd(s))
269	
270	def sort(population: List<&2, Ind.Individual>) -> List<&2, List<&2, Nat>>:
271	  match population:
272	    case Nil{}:
273	      Nil{}
274	    case +h <> +t:
275	      +rs = rows_of.go({h <> t : List<&2, Ind.Individual>}, 0n)
276	      peel(Util.list_len(Row, rs), rs)
277	
278	def front_index_count(fronts: List<&2, List<&2, Nat>>) -> Nat:
279	  match fronts:
280	    case Nil{}:
281	      0n
282	    case h <> t:
283	      Nat.add(Util.list_len(Nat, h), front_index_count(t))