( obj: LeanBorrowed<'_>, cache: &mut Cache<'_>, )
| 893 | Expr::letE(decl_name, typ, value, body, nondep) |
| 894 | }, |
| 895 | 9 => { |
| 896 | let lit = LeanIxLiteral::from_ctor(e.get_obj(0).as_ctor()); |
| 897 | let inner = lit.get_obj(0); |
| 898 | match lit.as_ctor().tag() { |
| 899 | 0 => Expr::lit(Literal::NatVal(LeanNat::to_nat(&inner))), |
| 900 | 1 => Expr::lit(Literal::StrVal(inner.as_string().to_string())), |
| 901 | tag => unreachable!("Invalid Lean.Literal tag: {tag}"), |
| 902 | } |
| 903 | }, |
| 904 | 10 => { |
| 905 | let kv_map: Vec<_> = collect_list_borrowed(e.get_obj(0).as_list()) |
| 906 | .into_iter() |
| 907 | .map(|o| decode_name_data_value(o, cache)) |
| 908 | .collect(); |
| 909 | let expr = decode_expr(e.get_obj(1), cache); |
| 910 | Expr::mdata(kv_map, expr) |
| 911 | }, |
| 912 | 11 => { |
| 913 | let typ_name = decode_name(e.get_obj(0), cache.global); |
| 914 | let idx = LeanNat::to_nat(&e.get_obj(1)); |
| 915 | let struct_expr = decode_expr(e.get_obj(2), cache); |
| 916 | Expr::proj(typ_name, idx, struct_expr) |
| 917 | }, |
| 918 | tag => unreachable!("Invalid Lean.Expr tag: {tag}"), |
| 919 | }; |
| 920 | cache.local.exprs.insert(ptr, expr.clone()); |
| 921 | expr |
| 922 | } |
| 923 | |
| 924 | fn decode_recursor_rule( |
| 925 | obj: LeanBorrowed<'_>, |
| 926 | cache: &mut Cache<'_>, |
| 927 | ) -> RecursorRule { |
| 928 | let r = LeanIxRecursorRule::from_ctor(obj.as_ctor()); |
| 929 | let ctor_name = decode_name(r.get_obj(0), cache.global); |
| 930 | let n_fields = LeanNat::to_nat(&r.get_obj(1)); |
| 931 | let rhs = decode_expr(r.get_obj(2), cache); |
| 932 | RecursorRule { ctor: ctor_name, n_fields, rhs } |
| 933 | } |
| 934 | |
| 935 | fn decode_constant_val( |
| 936 | obj: LeanBorrowed<'_>, |
| 937 | cache: &mut Cache<'_>, |
| 938 | ) -> ConstantVal { |
| 939 | let cv = LeanIxConstantVal::from_ctor(obj.as_ctor()); |
| 940 | let name = decode_name(cv.get_obj(0), cache.global); |
| 941 | let level_params: Vec<_> = collect_list_borrowed(cv.get_obj(1).as_list()) |
| 942 | .into_iter() |
| 943 | .map(|o| decode_name(o, cache.global)) |
| 944 | .collect(); |
| 945 | let typ = decode_expr(cv.get_obj(2), cache); |
| 946 | ConstantVal { name, level_params, typ } |
| 947 | } |
| 948 | |
| 949 | pub fn decode_constant_info( |
| 950 | obj: LeanBorrowed<'_>, |
| 951 | cache: &mut Cache<'_>, |
| 952 | ) -> ConstantInfo { |
no test coverage detected