Decompile an Ixon DataValue (Address-based) to a Lean DataValue.
( dv: &DataValue, stt: &CompileState, )
| 176 | let child = |c: &LeanExpr| -> LeanExpr { |
| 177 | memo |
| 178 | .get(&Arc::as_ptr(&c.0)) |
| 179 | .expect("intern walk: child not canonicalized before parent") |
| 180 | .clone() |
| 181 | }; |
| 182 | let same = |
| 183 | |c: &LeanExpr, i: &LeanExpr| -> bool { Arc::ptr_eq(&c.0, &i.0) }; |
| 184 | let rebuilt = match e.as_data() { |
| 185 | ED::App(f, a, h) => { |
| 186 | let (fi, ai) = (child(f), child(a)); |
| 187 | if same(f, &fi) && same(a, &ai) { |
| 188 | e.clone() |
| 189 | } else { |
| 190 | LeanExpr(Arc::new(ED::App(fi, ai, *h))) |
| 191 | } |
| 192 | }, |
| 193 | ED::Lam(n, t, b, bi, h) => { |
| 194 | let (ti, bdi) = (child(t), child(b)); |
| 195 | if same(t, &ti) && same(b, &bdi) { |
| 196 | e.clone() |
| 197 | } else { |
| 198 | LeanExpr(Arc::new(ED::Lam(n.clone(), ti, bdi, bi.clone(), *h))) |
| 199 | } |
| 200 | }, |
| 201 | ED::ForallE(n, t, b, bi, h) => { |
| 202 | let (ti, bdi) = (child(t), child(b)); |
| 203 | if same(t, &ti) && same(b, &bdi) { |
| 204 | e.clone() |
| 205 | } else { |
| 206 | LeanExpr(Arc::new(ED::ForallE(n.clone(), ti, bdi, bi.clone(), *h))) |
| 207 | } |
| 208 | }, |
| 209 | ED::LetE(n, t, v, b, nd, h) => { |
| 210 | let (ti, vi, bdi) = (child(t), child(v), child(b)); |
no test coverage detected