rain_lang/value/
judgement.rs

1/*!
2Judgemental equality and typing judgements
3*/
4use crate::graph::region::Parameter;
5use super::{
6    ValId,
7    ValueEnum,
8    lambda::Lambda,
9    expr::Sexpr
10};
11use super::primitive::{
12    logical::{Bool, LogicalOp, Unary, Binary},
13    Unit
14};
15
16/// Objects which can be compared for judgemental equality.
17///
18/// Equal objects should *always* be judgementally equal:
19/// equality will sometimes be referred to as "structural equality".
20pub trait JEq<Rhs=Self> {
21    /// Check whether two objects are judgementally equal
22    fn jeq(&self, other: &Rhs) -> bool;
23}
24
25/// Set judgemental equality between two types to be the same as `PartialEq`
26#[macro_export]
27macro_rules! trivial_judgemental_equality {
28    ($l:ty, $r:ty) => {
29        impl JEq<$r> for $l {
30            fn jeq(&self, other: &$r) -> bool { self.eq(other) }
31        }
32    };
33    ($l:ty, $r:ty, comm) => {
34        trivial_judgemental_equality!($l, $r);
35        trivial_judgemental_equality!($r, $l);
36    };
37    ($p:ty) => { trivial_judgemental_equality!($p, $p); };
38}
39
40/// Implement judgemental equality with `ValueEnum`, and `ValId` from `JEq<ValueEnum>`
41#[macro_export]
42macro_rules! value_judgemental_equality {
43    ($v:ty) => {
44        impl JEq<$v> for ValueEnum {
45            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(self) }
46        }
47        impl JEq<$v> for ValId {
48            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(&self.data().value) }
49        }
50        impl JEq<ValId> for $v {
51            #[inline] fn jeq(&self, v: &ValId) -> bool { v.jeq(self) }
52        }
53    }
54}
55
56/// Implemented judgemental equality with `Sexpr` from `JEq<ValueEnum>`
57#[macro_export]
58macro_rules! sexpr_judgemental_equality {
59    ($v:ty) => {
60        impl JEq<Sexpr> for $v {
61            #[inline] fn jeq(&self, s: &Sexpr) -> bool { s.singleton_jeq(self) }
62        }
63        impl JEq<$v> for Sexpr {
64            #[inline] fn jeq(&self, v: &$v) -> bool { v.jeq(self) }
65        }
66    }
67}
68
69/// Assert two values are judgementally equal
70#[macro_export]
71macro_rules! assert_jeq {
72    ($l:expr, $r:expr) => {{ use crate::value::judgement::JEq; assert!($l.jeq($r)) }};
73    ($l:expr, $r:expr, $m:literal $(, $vs:expr)*) => {{
74        use crate::value::judgement::JEq;
75        assert!($l.jeq($r), $m $(, $vs)*)
76    }}
77}
78
79macro_rules! value_enum_variant_jeq {
80    ($v:ty, $p:path) => {
81        impl JEq<ValueEnum> for $v {
82            fn jeq(&self, other: &ValueEnum) -> bool {
83                match other {
84                    ValueEnum::Sexpr(s) => s.jeq(self),
85                    $p(v) => v.jeq(self),
86                    _ => false
87                }
88            }
89        }
90        value_judgemental_equality!($v);
91    }
92}
93
94macro_rules! trivial_value_enum_variant_jeq {
95    ($v:ty, $p:path) => {
96        trivial_judgemental_equality!($v);
97        value_enum_variant_jeq!($v, $p);
98        sexpr_judgemental_equality!($v);
99    }
100}
101
102trivial_value_enum_variant_jeq!(bool, ValueEnum::Bool);
103trivial_value_enum_variant_jeq!(Bool, ValueEnum::BoolTy);
104trivial_value_enum_variant_jeq!(Unit, ValueEnum::UnitTy);
105trivial_value_enum_variant_jeq!(LogicalOp, ValueEnum::LogicalOp);
106trivial_value_enum_variant_jeq!(Lambda, ValueEnum::Lambda);
107trivial_value_enum_variant_jeq!(Parameter, ValueEnum::Parameter);
108trivial_judgemental_equality!(LogicalOp, Unary);
109trivial_judgemental_equality!(LogicalOp, Binary);
110trivial_value_enum_variant_jeq!(Unary, ValueEnum::LogicalOp);
111trivial_value_enum_variant_jeq!(Binary, ValueEnum::LogicalOp);
112
113impl Sexpr {
114    /// Check if an S-expression is a singleton judgementally equal to `other`
115    pub fn singleton_jeq<T: JEq<ValId>>(&self, other: &T) -> bool {
116        if self.len() == 1 { other.jeq(&self[0]) } else { false }
117    }
118    /// Check if an S-expression is a singleton equal to `other`
119    pub fn singleton_eq<T: PartialEq<ValId>>(&self, other: &T) -> bool {
120        if self.len() == 1 { other == &self[0] } else { false }
121    }
122    /// Check if an S-expression is judgementally equal to the given arguments
123    pub fn args_jeq<T: JEq<ValId>>(&self, other: &[T]) -> bool {
124        if self.len() != other.len() { false }
125        else {
126            for (v, t) in self.iter().zip(other.iter()) {
127                if !t.jeq(v) { return false }
128            }
129            return true
130        }
131    }
132}
133
134impl JEq<Sexpr> for Sexpr {
135    fn jeq(&self, other: &Sexpr) -> bool {
136        if self == other { true}
137        else if self.len() == other.len() {
138            for (l, r) in self.iter().zip(other.iter()) {
139                if !l.jeq(r) { return false }
140            }
141            true
142        } else if self.len() == 1 {
143            other.jeq(&self[0])
144        } else if other.len() == 1 {
145            self.jeq(&other[0])
146        } else {
147            false
148        }
149    }
150}
151
152impl JEq<ValueEnum> for Sexpr {
153    fn jeq(&self, other: &ValueEnum) -> bool {
154        match other {
155            ValueEnum::Sexpr(s) => self.jeq(s),
156            v => self.singleton_jeq(v)
157        }
158    }
159}
160
161value_judgemental_equality!(Sexpr);
162
163impl JEq for ValId {
164    fn jeq(&self, other: &ValId) -> bool {
165        self == other || self.data().value.jeq(other)
166    }
167}
168
169impl JEq<ValId> for ValueEnum {
170    fn jeq(&self, other: &ValId) -> bool {
171        match self {
172            ValueEnum::Sexpr(s) if s.singleton_eq(other) => true,
173            v => other.data().value.jeq(v)
174        }
175    }
176}
177
178impl JEq<ValueEnum> for ValId {
179    fn jeq(&self, other: &ValueEnum) -> bool { other.jeq(self) }
180}
181
182impl JEq for ValueEnum {
183    fn jeq(&self, other: &ValueEnum) -> bool {
184        match self {
185            ValueEnum::Bool(b) => other.jeq(b),
186            ValueEnum::BoolTy(b) => other.jeq(b),
187            ValueEnum::Lambda(l) => other.jeq(l),
188            ValueEnum::Parameter(p) => other.jeq(p),
189            ValueEnum::LogicalOp(l) => other.jeq(l),
190            ValueEnum::UnitTy(u) => other.jeq(u),
191            ValueEnum::Sexpr(s) => other.jeq(s)
192        }
193    }
194}
195
196#[cfg(test)]
197mod tests {
198    use smallvec::smallvec;
199    use super::*;
200
201    #[test]
202    fn boolean_judgemental_equality() {
203        for i in [false, true].iter() {
204            for j in [false, true].iter() {
205                assert_eq!(i.jeq(j), i == j);
206                assert_eq!(ValueEnum::Bool(*i).jeq(j), i == j);
207                assert_eq!(ValueEnum::Bool(*i).jeq(&ValueEnum::Bool(*j)), i == j);
208            }
209            assert!(!ValueEnum::Bool(*i).jeq(&ValueEnum::UnitTy(Unit)));
210            assert!(!Bool.jeq(&ValueEnum::Bool(*i)));
211            assert!(!Unit.jeq(&ValueEnum::Bool(*i)));
212        }
213        assert!(Bool.jeq(&Bool));
214    }
215
216    #[test]
217    fn basic_sexpr_judgemental_equality() {
218        let ts = Sexpr::build(smallvec![ValId::from(true)]).expect("Valid sexpr");
219        let fs = Sexpr::build(smallvec![
220            ValId::from(true), ValId::from(false), LogicalOp::Binary(Binary::And).into()])
221            .expect("Valid sexpr");
222        let bsxp = [(ts, true), (fs, false)];
223        let and = Sexpr::build(smallvec![LogicalOp::Binary(Binary::And).into()])
224            .expect("Valid sexpr");
225        for (i, iv) in bsxp.iter() {
226            for j in [false, true].iter() {
227                assert_eq!(i.singleton_jeq(j), iv == j,
228                    "[Singleton] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
229                assert_eq!(i.jeq(j), iv == j, "[Value] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
230                assert_eq!(i.jeq(&ValueEnum::Bool(*j)), iv == j,
231                    "[ValueEnum] (#{}) == #{} != #{} == #{}", iv, j, iv, j);
232            }
233            for (j, jv) in bsxp.iter() {
234                assert_eq!(i.singleton_jeq(j), iv == jv,
235                    "[Singleton] (#{}) == (#{}) != #{} == #{}", iv, jv, iv, jv);
236                assert_eq!(i.jeq(j), iv == jv,
237                    "[Value] (#{}) == (#{}) != #{} == #{}", iv, jv, iv, jv);
238            }
239            assert!(!i.jeq(&and));
240            assert!(!i.jeq(&ValueEnum::UnitTy(Unit)));
241            assert!(!Unit.jeq(i));
242            assert!(!Bool.jeq(i));
243        }
244        assert!(and.jeq(&and));
245        assert!(LogicalOp::Binary(Binary::And).jeq(&and));
246        assert!(Bool.jeq(&Bool));
247    }
248
249}
rain_lang/value/judgement.rs

rain_lang/value/
judgement.rs
