Compare two recursors by params, indices, motives, minors, k, type, then rules.
( x: &Rec, y: &Rec, mut_ctx: &MutCtx, stt: &CompileState, )
| 2744 | pub fn compile_mutual_block( |
| 2745 | mut_consts: Vec<IxonMutConst>, |
| 2746 | refs: Vec<Address>, |
| 2747 | univs: Vec<Arc<Univ>>, |
| 2748 | block_name: Option<&str>, |
| 2749 | ) -> CompiledMutualBlock { |
| 2750 | // Apply sharing analysis across all expressions in the mutual block |
| 2751 | let result = |
| 2752 | apply_sharing_to_mutual_block(mut_consts, refs, univs, block_name); |
| 2753 | let constant = result.constant; |
| 2754 | let hash_consed_size = result.hash_consed_size; |
| 2755 | |
| 2756 | // Compute content address and serialized size |
| 2757 | let mut bytes = Vec::new(); |
| 2758 | constant.put(&mut bytes); |
| 2759 | let serialized_size = bytes.len(); |
| 2760 | let addr = Address::hash(&bytes); |
| 2761 | |
| 2762 | CompiledMutualBlock { constant, addr, hash_consed_size, serialized_size } |
| 2763 | } |
| 2764 | |
| 2765 | /// Create Inductive from InductiveVal and Env. |
| 2766 | pub fn mk_indc( |
| 2767 | ind: &InductiveVal, |
| 2768 | env: &Arc<LeanEnv>, |
| 2769 | ) -> Result<Ind, CompileError> { |
| 2770 | let mut ctors = Vec::with_capacity(ind.ctors.len()); |
| 2771 | for ctor_name in &ind.ctors { |
| 2772 | if let Some(LeanConstantInfo::CtorInfo(c)) = |
| 2773 | env.as_ref().get(ctor_name).as_deref() |
| 2774 | { |
| 2775 | ctors.push(c.clone()); |
| 2776 | } else { |
| 2777 | return Err(CompileError::MissingConstant { |
| 2778 | name: ctor_name.pretty(), |
| 2779 | caller: "mk_indc(ctor_lookup)".into(), |
| 2780 | }); |
| 2781 | } |
| 2782 | } |
| 2783 | Ok(Ind { ind: ind.clone(), ctors }) |
| 2784 | } |
| 2785 | |
| 2786 | // =========================================================================== |
| 2787 | // Alpha-invariant comparison and sorting |
| 2788 | // |
| 2789 | // These functions establish a canonical ordering for constants within mutual |
| 2790 | // blocks. Since names are not alpha-invariant, we compare by structure: |
| 2791 | // universe levels, expressions, field counts, etc. The `SOrd` return type |
| 2792 | // tracks whether the comparison is "strong" (based solely on alpha-invariant |
| 2793 | // data) or "weak" (needed a name-based tiebreaker). |
| 2794 | // =========================================================================== |
| 2795 | |
| 2796 | /// Compare two universe levels structurally, using level parameter position |
no test coverage detected