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};
15use std::rc::Rc;
16
17use super::functions::{hash_binder_info, hash_level, hash_literal, hash_name, hash_tag};
18use super::types::ExprKey;
19
20impl Hash for ExprKey {
21    fn hash<H: Hasher>(&self, state: &mut H) {
22        match &self.0 {
23            Expr::Sort(lvl) => {
24                hash_tag(state, 0);
25                hash_level(lvl, state);
26            }
27            Expr::BVar(idx) => {
28                hash_tag(state, 1);
29                idx.hash(state);
30            }
31            Expr::FVar(fvar_id) => {
32                hash_tag(state, 2);
33                fvar_id.hash(state);
34            }
35            Expr::Const(name, levels) => {
36                hash_tag(state, 3);
37                hash_name(name, state);
38                for lvl in levels {
39                    hash_level(lvl, state);
40                }
41            }
42            Expr::App(f, a) => {
43                hash_tag(state, 4);
44                ExprKey((**f).clone()).hash(state);
45                ExprKey((**a).clone()).hash(state);
46            }
47            Expr::Lam(bi, name, ty, body) => {
48                hash_tag(state, 5);
49                hash_binder_info(bi, state);
50                hash_name(name, state);
51                ExprKey((**ty).clone()).hash(state);
52                ExprKey((**body).clone()).hash(state);
53            }
54            Expr::Pi(bi, name, ty, body) => {
55                hash_tag(state, 6);
56                hash_binder_info(bi, state);
57                hash_name(name, state);
58                ExprKey((**ty).clone()).hash(state);
59                ExprKey((**body).clone()).hash(state);
60            }
61            Expr::Let(name, ty, val, body) => {
62                hash_tag(state, 7);
63                hash_name(name, state);
64                ExprKey((**ty).clone()).hash(state);
65                ExprKey((**val).clone()).hash(state);
66                ExprKey((**body).clone()).hash(state);
67            }
68            Expr::Lit(lit) => {
69                hash_tag(state, 8);
70                hash_literal(lit, state);
71            }
72            Expr::Proj(name, idx, expr) => {
73                hash_tag(state, 9);
74                hash_name(name, state);
75                idx.hash(state);
76                ExprKey((**expr).clone()).hash(state);
77            }
78        }
79    }
80}
81
82impl PartialEq for ExprKey {
83    fn eq(&self, other: &Self) -> bool {
84        self.0 == other.0
85    }
86}
87
88impl Eq for ExprKey {}
oxilean_kernel/expr_cache/exprkey_traits.rs

oxilean_kernel/expr_cache/
exprkey_traits.rs
