oxilean_kernel/expr_cache/
exprkey_traits.rs

1//! # ExprKey - Trait Implementations
2//!
3//! This module contains trait implementations for `ExprKey`.
4//!
5//! ## Implemented Traits
6//!
7//! - `Hash`
8//! - `PartialEq`
9//! - `Eq`
10//!
11//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
12
13use crate::{BinderInfo, Expr, Level, Literal, Name};
14use std::hash::{Hash, Hasher};
15
16use super::functions::{hash_binder_info, hash_level, hash_literal, hash_name, hash_tag};
17use super::types::ExprKey;
18
19impl Hash for ExprKey {
20    fn hash<H: Hasher>(&self, state: &mut H) {
21        match &self.0 {
22            Expr::Sort(lvl) => {
23                hash_tag(state, 0);
24                hash_level(lvl, state);
25            }
26            Expr::BVar(idx) => {
27                hash_tag(state, 1);
28                idx.hash(state);
29            }
30            Expr::FVar(fvar_id) => {
31                hash_tag(state, 2);
32                fvar_id.hash(state);
33            }
34            Expr::Const(name, levels) => {
35                hash_tag(state, 3);
36                hash_name(name, state);
37                for lvl in levels {
38                    hash_level(lvl, state);
39                }
40            }
41            Expr::App(f, a) => {
42                hash_tag(state, 4);
43                ExprKey(*f.clone()).hash(state);
44                ExprKey(*a.clone()).hash(state);
45            }
46            Expr::Lam(bi, name, ty, body) => {
47                hash_tag(state, 5);
48                hash_binder_info(bi, state);
49                hash_name(name, state);
50                ExprKey(*ty.clone()).hash(state);
51                ExprKey(*body.clone()).hash(state);
52            }
53            Expr::Pi(bi, name, ty, body) => {
54                hash_tag(state, 6);
55                hash_binder_info(bi, state);
56                hash_name(name, state);
57                ExprKey(*ty.clone()).hash(state);
58                ExprKey(*body.clone()).hash(state);
59            }
60            Expr::Let(name, ty, val, body) => {
61                hash_tag(state, 7);
62                hash_name(name, state);
63                ExprKey(*ty.clone()).hash(state);
64                ExprKey(*val.clone()).hash(state);
65                ExprKey(*body.clone()).hash(state);
66            }
67            Expr::Lit(lit) => {
68                hash_tag(state, 8);
69                hash_literal(lit, state);
70            }
71            Expr::Proj(name, idx, expr) => {
72                hash_tag(state, 9);
73                hash_name(name, state);
74                idx.hash(state);
75                ExprKey(*expr.clone()).hash(state);
76            }
77        }
78    }
79}
80
81impl PartialEq for ExprKey {
82    fn eq(&self, other: &Self) -> bool {
83        self.0 == other.0
84    }
85}
86
87impl Eq for ExprKey {}
oxilean_kernel/expr_cache/exprkey_traits.rs

oxilean_kernel/expr_cache/
exprkey_traits.rs
