| 87 | /// rebuilds every constant's expressions with sharing local to that |
| 88 | /// constant, so structurally equal subterms (common types, applied |
| 89 | /// prefixes) would otherwise each hold a private copy per referencing |
| 90 | /// constant — a multiple of the whole env's footprint. Constants |
| 91 | /// entering `env` are canonicalized through this table |
| 92 | /// ([`Self::insert_interned`]); `decompile_env` drops the table |
| 93 | /// before returning, since `env` keeps the canonical `Arc`s alive. |
| 94 | expr_intern: DashMap<[u8; 32], LeanExpr>, |
| 95 | } |
| 96 | |
| 97 | #[derive(Debug)] |
| 98 | pub struct DecompileStateStats { |
| 99 | pub env: usize, |
| 100 | } |
| 101 | |
| 102 | impl DecompileState { |
| 103 | pub fn stats(&self) -> DecompileStateStats { |
| 104 | DecompileStateStats { env: self.env.len() } |
| 105 | } |
| 106 | |
| 107 | /// Insert a decompiled constant, canonicalizing its expressions |
| 108 | /// through [`Self::expr_intern`]. |
| 109 | fn insert_interned(&self, name: Name, ci: LeanConstantInfo) { |
| 110 | self.env.insert(name, self.intern_ci(ci)); |
| 111 | } |
| 112 | |
| 113 | /// Canonicalize every expression field of `ci` — see |
| 114 | /// [`Self::expr_intern`]. |
| 115 | fn intern_ci(&self, mut ci: LeanConstantInfo) -> LeanConstantInfo { |
| 116 | match &mut ci { |
| 117 | LeanConstantInfo::AxiomInfo(v) => { |
nothing calls this directly
no outgoing calls
no test coverage detected