Hash an expression node using Merkle-tree style hashing. Returns (hash, child_hashes, value_size) where value_size is the size of the serialized node value in a hash-consed store (not including the 32-byte key).
( expr: &Expr, child_hashes: &FxHashMap<*const Expr, blake3::Hash>, buf: &mut Vec<u8>, )
| 37 | /// Returns (hash, child_hashes, value_size) where value_size is the size of the |
| 38 | /// serialized node value in a hash-consed store (not including the 32-byte key). |
| 39 | fn hash_node( |
| 40 | expr: &Expr, |
| 41 | child_hashes: &FxHashMap<*const Expr, blake3::Hash>, |
| 42 | buf: &mut Vec<u8>, |
| 43 | ) -> (blake3::Hash, Vec<blake3::Hash>, usize) { |
| 44 | buf.clear(); |
| 45 | |
| 46 | let children = match expr { |
| 47 | Expr::Sort(univ_idx) => { |
| 48 | buf.push(Expr::FLAG_SORT); |
| 49 | buf.extend_from_slice(&univ_idx.to_le_bytes()); |
| 50 | vec![] |
| 51 | }, |
| 52 | Expr::Var(idx) => { |
| 53 | buf.push(Expr::FLAG_VAR); |
| 54 | buf.extend_from_slice(&idx.to_le_bytes()); |
| 55 | vec![] |
| 56 | }, |
| 57 | Expr::Ref(ref_idx, univ_indices) => { |
| 58 | buf.push(Expr::FLAG_REF); |
| 59 | buf.extend_from_slice(&ref_idx.to_le_bytes()); |
| 60 | buf.extend_from_slice(&(univ_indices.len() as u64).to_le_bytes()); |
| 61 | for idx in univ_indices { |
| 62 | buf.extend_from_slice(&idx.to_le_bytes()); |
| 63 | } |
| 64 | vec![] |
| 65 | }, |
| 66 | Expr::Rec(rec_idx, univ_indices) => { |
| 67 | buf.push(Expr::FLAG_REC); |
| 68 | buf.extend_from_slice(&rec_idx.to_le_bytes()); |
| 69 | buf.extend_from_slice(&(univ_indices.len() as u64).to_le_bytes()); |
| 70 | for idx in univ_indices { |
| 71 | buf.extend_from_slice(&idx.to_le_bytes()); |
| 72 | } |
| 73 | vec![] |
| 74 | }, |
| 75 | Expr::Prj(type_ref_idx, field_idx, val) => { |
| 76 | buf.push(Expr::FLAG_PRJ); |
| 77 | buf.extend_from_slice(&type_ref_idx.to_le_bytes()); |
| 78 | buf.extend_from_slice(&field_idx.to_le_bytes()); |
| 79 | let val_ptr = val.as_ref() as *const Expr; |
| 80 | let val_hash = child_hashes.get(&val_ptr).unwrap(); |
| 81 | buf.extend_from_slice(val_hash.as_bytes()); |
| 82 | vec![*val_hash] |
| 83 | }, |
| 84 | Expr::Str(ref_idx) => { |
| 85 | buf.push(Expr::FLAG_STR); |
| 86 | buf.extend_from_slice(&ref_idx.to_le_bytes()); |
| 87 | vec![] |
| 88 | }, |
| 89 | Expr::Nat(ref_idx) => { |
| 90 | buf.push(Expr::FLAG_NAT); |
| 91 | buf.extend_from_slice(&ref_idx.to_le_bytes()); |
| 92 | vec![] |
| 93 | }, |
| 94 | Expr::App(fun, arg) => { |
| 95 | buf.push(Expr::FLAG_APP); |
| 96 | let fun_ptr = fun.as_ref() as *const Expr; |