Decode a Lean Ix.Expr to Rust Expr.
(&self)
| 158 | impl<R: LeanRef> LeanIxExpr<R> { |
| 159 | /// Decode a Lean Ix.Expr to Rust Expr. |
| 160 | pub fn decode(&self) -> Expr { |
| 161 | let ctor = self.as_ctor(); |
| 162 | match ctor.tag() { |
| 163 | 0 => { |
| 164 | // bvar |
| 165 | let idx = LeanNat::to_nat(&ctor.get(0)); |
| 166 | Expr::bvar(idx) |
| 167 | }, |
| 168 | 1 => { |
| 169 | // fvar |
| 170 | let name = LeanIxName(ctor.get(0)).decode(); |
| 171 | Expr::fvar(name) |
| 172 | }, |
| 173 | 2 => { |
| 174 | // mvar |
| 175 | let name = LeanIxName(ctor.get(0)).decode(); |
| 176 | Expr::mvar(name) |
| 177 | }, |
| 178 | 3 => { |
| 179 | // sort |
| 180 | let level = LeanIxLevel(ctor.get(0)).decode(); |
| 181 | Expr::sort(level) |
| 182 | }, |
| 183 | 4 => { |
| 184 | // const |
| 185 | let name = LeanIxName(ctor.get(0)).decode(); |
| 186 | let levels: Vec<Level> = |
| 187 | ctor.get(1).as_array().map(|x| LeanIxLevel(x).decode()); |
| 188 | |
| 189 | Expr::cnst(name, levels) |
| 190 | }, |
| 191 | 5 => { |
| 192 | // app |
| 193 | let fn_expr = LeanIxExpr(ctor.get(0)).decode(); |
| 194 | let arg_expr = LeanIxExpr(ctor.get(1)).decode(); |
| 195 | Expr::app(fn_expr, arg_expr) |
| 196 | }, |
| 197 | 6 => { |
| 198 | // lam: name, ty, body, hash, bi (scalar) |
| 199 | let name = LeanIxName(self.get_obj(0)).decode(); |
| 200 | let ty = LeanIxExpr(self.get_obj(1)).decode(); |
| 201 | let body = LeanIxExpr(self.get_obj(2)).decode(); |
| 202 | |
| 203 | let bi_byte = self.get_num_8(0); |
| 204 | let bi = LeanIxBinderInfo::<LeanOwned>::from_u8(bi_byte); |
| 205 | |
| 206 | Expr::lam(name, ty, body, bi) |
| 207 | }, |
| 208 | 7 => { |
| 209 | // forallE: same layout as lam |
| 210 | let name = LeanIxName(self.get_obj(0)).decode(); |
| 211 | let ty = LeanIxExpr(self.get_obj(1)).decode(); |
| 212 | let body = LeanIxExpr(self.get_obj(2)).decode(); |
| 213 | |
| 214 | let bi_byte = self.get_num_8(0); |
| 215 | let bi = LeanIxBinderInfo::<LeanOwned>::from_u8(bi_byte); |
| 216 | |
| 217 | Expr::all(name, ty, body, bi) |