Compute the canonical aux ordering — kernel analogue of the compile-side aux partition-refinement sort (`src/ix/compile/aux_gen/nested.rs`). For each aux `FlatBlockMember`, synthesize a `KConst::Indc` view (with its constructor `KConst::Ctor` views) that mirrors the compile-side `MutConst::Indc` aux representation. Run `sort_kconsts_with_seed_key` on the synthetic aux and return a permutation `or
(
&mut self,
aux: &[FlatBlockMember<M>],
n_block_params: u64,
block_us: &[KUniv<M>],
all0_name: Option<&ix_common::env::Name>,
block_first_id: Option<&KId<M>>,
)
| 1039 | }, |
| 1040 | ExprData::Lam(n, bi, ty, body, _) => { |
| 1041 | let ty2 = self.replace_aux_refs_for_sort( |
| 1042 | ty, |
| 1043 | aux, |
| 1044 | aux_ids, |
| 1045 | block_us, |
| 1046 | n_block_params, |
| 1047 | local_depth, |
| 1048 | )?; |
| 1049 | let body2 = self.replace_aux_refs_for_sort( |
| 1050 | body, |
| 1051 | aux, |
| 1052 | aux_ids, |
| 1053 | block_us, |
| 1054 | n_block_params, |
| 1055 | local_depth + 1, |
| 1056 | )?; |
| 1057 | KExpr::lam(n.clone(), bi.clone(), ty2, body2) |
| 1058 | }, |
| 1059 | ExprData::All(n, bi, ty, body, _) => { |
| 1060 | let ty2 = self.replace_aux_refs_for_sort( |
| 1061 | ty, |
| 1062 | aux, |
| 1063 | aux_ids, |
| 1064 | block_us, |
| 1065 | n_block_params, |
| 1066 | local_depth, |
| 1067 | )?; |
| 1068 | let body2 = self.replace_aux_refs_for_sort( |
| 1069 | body, |
| 1070 | aux, |
| 1071 | aux_ids, |
| 1072 | block_us, |
| 1073 | n_block_params, |
| 1074 | local_depth + 1, |
| 1075 | )?; |
| 1076 | KExpr::all(n.clone(), bi.clone(), ty2, body2) |
| 1077 | }, |
| 1078 | ExprData::Let(n, ty, val, body, nd, _) => { |
| 1079 | let ty2 = self.replace_aux_refs_for_sort( |
| 1080 | ty, |
| 1081 | aux, |
| 1082 | aux_ids, |
| 1083 | block_us, |
| 1084 | n_block_params, |
| 1085 | local_depth, |
| 1086 | )?; |
| 1087 | let val2 = self.replace_aux_refs_for_sort( |
| 1088 | val, |
| 1089 | aux, |
| 1090 | aux_ids, |
| 1091 | block_us, |
| 1092 | n_block_params, |
| 1093 | local_depth, |
| 1094 | )?; |
| 1095 | let body2 = self.replace_aux_refs_for_sort( |
| 1096 | body, |
| 1097 | aux, |
| 1098 | aux_ids, |
no test coverage detected