Deserialize a Name from bytes (full recursive deserialization).
(buf: &mut &[u8])
| 918 | pub fn put(&self, buf: &mut Vec<u8>) { |
| 919 | put_u64(self.idx, buf); |
| 920 | put_address(&self.block, buf); |
| 921 | } |
| 922 | |
| 923 | pub fn get(buf: &mut &[u8]) -> Result<Self, String> { |
| 924 | let idx = get_u64(buf)?; |
| 925 | let block = get_address(buf)?; |
| 926 | Ok(DefinitionProj { idx, block }) |
| 927 | } |
| 928 | } |
| 929 | |
| 930 | impl MutConst { |
| 931 | pub fn put(&self, buf: &mut Vec<u8>) { |
| 932 | match self { |
| 933 | Self::Defn(d) => { |
| 934 | put_u8(0, buf); |
| 935 | d.put(buf); |
| 936 | }, |
| 937 | Self::Indc(i) => { |
| 938 | put_u8(1, buf); |
| 939 | i.put(buf); |
| 940 | }, |
| 941 | Self::Recr(r) => { |
| 942 | put_u8(2, buf); |
| 943 | r.put(buf); |
| 944 | }, |
| 945 | } |
| 946 | } |
| 947 | |
| 948 | pub fn get(buf: &mut &[u8]) -> Result<Self, String> { |
| 949 | match get_u8(buf)? { |
| 950 | 0 => Ok(Self::Defn(Definition::get(buf)?)), |
| 951 | 1 => Ok(Self::Indc(Inductive::get(buf)?)), |
| 952 | 2 => Ok(Self::Recr(Recursor::get(buf)?)), |
| 953 | x => Err(format!("MutConst::get: invalid tag {x}")), |
| 954 | } |
| 955 | } |
| 956 | } |
| 957 | |
| 958 | impl ConstantInfo { |
| 959 | /// Serialize a non-Muts ConstantInfo (Muts is handled separately in Constant::put) |