Sort mutual constants into a canonical ordering and group equal ones. Uses iterative refinement: sort by structure, group equals, re-sort with updated mutual context indices, until the partition stabilizes.
( cs: &[&'a MutConst], cache: &mut BlockCache, stt: &CompileState, )
| 2931 | ) |
| 2932 | }, |
| 2933 | (ExprData::Lam(..), _) => Ok(SOrd::lt(true)), |
| 2934 | (_, ExprData::Lam(..)) => Ok(SOrd::gt(true)), |
| 2935 | ( |
| 2936 | ExprData::ForallE(_, xt, xb, _, _), |
| 2937 | ExprData::ForallE(_, yt, yb, _, _), |
| 2938 | ) => SOrd::try_compare( |
| 2939 | compare_expr(xt, yt, mut_ctx, x_lvls, y_lvls, stt)?, |
| 2940 | || compare_expr(xb, yb, mut_ctx, x_lvls, y_lvls, stt), |
| 2941 | ), |
| 2942 | (ExprData::ForallE(..), _) => Ok(SOrd::lt(true)), |
| 2943 | (_, ExprData::ForallE(..)) => Ok(SOrd::gt(true)), |
| 2944 | ( |
| 2945 | ExprData::LetE(_, xt, xv, xb, _, _), |
| 2946 | ExprData::LetE(_, yt, yv, yb, _, _), |
| 2947 | ) => SOrd::try_zip( |
| 2948 | |a, b| compare_expr(a, b, mut_ctx, x_lvls, y_lvls, stt), |
| 2949 | &[xt, xv, xb], |
| 2950 | &[yt, yv, yb], |
| 2951 | ), |
| 2952 | (ExprData::LetE(..), _) => Ok(SOrd::lt(true)), |
| 2953 | (_, ExprData::LetE(..)) => Ok(SOrd::gt(true)), |
| 2954 | (ExprData::Lit(x, _), ExprData::Lit(y, _)) => Ok(SOrd::cmp(x, y)), |
| 2955 | (ExprData::Lit(..), _) => Ok(SOrd::lt(true)), |
| 2956 | (_, ExprData::Lit(..)) => Ok(SOrd::gt(true)), |
| 2957 | (ExprData::Proj(tnx, ix, tx, _), ExprData::Proj(tny, iy, ty, _)) => { |
| 2958 | let tn: Result<SOrd, CompileError> = |
| 2959 | match (mut_ctx.get(tnx), mut_ctx.get(tny)) { |
| 2960 | (Some(nx), Some(ny)) => Ok(SOrd::weak_cmp(nx, ny)), |
| 2961 | (Some(..), _) => Ok(SOrd::lt(true)), |
| 2962 | (None, Some(..)) => Ok(SOrd::gt(true)), |
| 2963 | (None, None) => { |
| 2964 | compare_external_refs(tnx, tny, stt, "compare_expr(Proj)") |
| 2965 | }, |
| 2966 | }; |
| 2967 | let tn = tn?; |
| 2968 | SOrd::try_compare(tn, || { |
| 2969 | SOrd::try_compare(SOrd::cmp(ix, iy), || { |
| 2970 | compare_expr(tx, ty, mut_ctx, x_lvls, y_lvls, stt) |
| 2971 | }) |
| 2972 | }) |
| 2973 | }, |
| 2974 | } |
| 2975 | } |
| 2976 | |
| 2977 | // =========================================================================== |
| 2978 | // Constant-level comparison and sorting |
| 2979 | // =========================================================================== |
| 2980 | |
| 2981 | /// Compare two definitions by kind, level parameter count, type, then value. |
| 2982 | pub fn compare_defn( |
| 2983 | x: &Def, |
| 2984 | y: &Def, |
| 2985 | mut_ctx: &MutCtx, |
| 2986 | stt: &CompileState, |
| 2987 | ) -> Result<SOrd, CompileError> { |
| 2988 | SOrd::try_compare( |
| 2989 | SOrd { strong: true, ordering: x.kind.cmp(&y.kind) }, |
| 2990 | || { |