(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>)
| 786 | let args: Vec<_> = s |
| 787 | .get_obj(2) |
| 788 | .as_array() |
| 789 | .iter() |
| 790 | .map(|o| decode_syntax(o, cache)) |
| 791 | .collect(); |
| 792 | Syntax::Node(info, kind, args) |
| 793 | }, |
| 794 | 2 => { |
| 795 | let info = decode_source_info(s.get_obj(0)); |
| 796 | Syntax::Atom(info, s.get_obj(1).as_string().to_string()) |
| 797 | }, |
| 798 | 3 => { |
| 799 | let info = decode_source_info(s.get_obj(0)); |
| 800 | let raw_val = decode_substring(s.get_obj(1)); |
| 801 | let val = decode_name(s.get_obj(2), cache.global); |
| 802 | let preresolved = collect_list_borrowed(s.get_obj(3).as_list()) |
| 803 | .into_iter() |
| 804 | .map(|o| decode_syntax_preresolved(o, cache)) |
| 805 | .collect(); |
| 806 | Syntax::Ident(info, raw_val, val, preresolved) |
| 807 | }, |
| 808 | tag => unreachable!("Invalid Lean.Syntax tag: {tag}"), |
| 809 | } |
| 810 | } |
| 811 | |
| 812 | fn decode_name_data_value( |
| 813 | obj: LeanBorrowed<'_>, |
| 814 | cache: &mut Cache<'_>, |
| 815 | ) -> (Name, DataValue) { |
| 816 | // Outer Prod (Name × DataValue) has no public LeanProd<LeanBorrowed> |
| 817 | // constructor, so read the two fields through the raw ctor. |
| 818 | let pair = obj.as_ctor(); |
| 819 | let name = decode_name(pair.get(0), cache.global); |
| 820 | let dv = LeanIxDataValue::from_ctor(pair.get(1).as_ctor()); |
| 821 | let data_value = match dv.as_ctor().tag() { |
| 822 | 0 => DataValue::OfString(dv.get_obj(0).as_string().to_string()), |
| 823 | 1 => DataValue::OfBool(dv.get_num_8(0) != 0), |
| 824 | 2 => DataValue::OfName(decode_name(dv.get_obj(0), cache.global)), |
| 825 | 3 => DataValue::OfNat(LeanNat::to_nat(&dv.get_obj(0))), |
| 826 | 4 => { |
| 827 | let i = LeanIxInt::from_ctor(dv.get_obj(0).as_ctor()); |
| 828 | let nat = LeanNat::to_nat(&i.get_obj(0)); |
| 829 | let int = match i.as_ctor().tag() { |
| 830 | 0 => Int::OfNat(nat), |
| 831 | 1 => Int::NegSucc(nat), |
| 832 | tag => unreachable!("Invalid Lean.Int tag: {tag}"), |
| 833 | }; |
| 834 | DataValue::OfInt(int) |
| 835 | }, |
| 836 | 5 => DataValue::OfSyntax(decode_syntax(dv.get_obj(0), cache).into()), |
| 837 | tag => unreachable!("Invalid Lean.DataValue tag: {tag}"), |
| 838 | }; |
| 839 | (name, data_value) |
| 840 | } |
| 841 | |
| 842 | pub fn decode_expr(obj: LeanBorrowed<'_>, cache: &mut Cache<'_>) -> Expr { |
| 843 | let ptr = obj.as_raw(); |
| 844 | if let Some(cached) = cache.local.exprs.get(&ptr) { |
| 845 | return cached.clone(); |
no test coverage detected