path_semantics_std/
constrain.rs

1use *;
2
3/// Implemented by higher order representations of constrained functions.
4pub trait Constrain<I> {
5    type Lift;
6
7    /// Override input constraint even when existential path does not exist.
8    fn i_force(&self, I) -> Self::Lift;
9
10    /// Constrains input but only if an existential path is supported for the constraint.
11    fn i(&self, i: I) -> Self::Lift where Self::Lift: ExPath {self.i_force(i)}
12}
13
14impl<I> Constrain<I> for () {
15    type Lift = ();
16    fn i_force(&self, _: I) -> () {()}
17}
18
19impl<Co: Clone, Tr: Clone, Fa: Clone, I, I2> Constrain<I> for If<Co, Tr, Fa, I2> {
20    type Lift = If<Co, Tr, Fa, I>;
21    fn i_force(&self, i: I) -> Self::Lift {
22        If {co: self.co.clone(), tr: self.tr.clone(), fa: self.fa.clone(), i}
23    }
24}
25
26macro_rules! con_impl {
27    ($a:ident t) => {
28        impl<T, I, I2> Constrain<I2> for $a<T, I> {
29            type Lift = $a<T, I2>;
30            fn i_force(&self, i: I2) -> Self::Lift {$a {t: PhantomData, i}}
31        }
32    };
33    ($a:ident k) => {
34        impl<T: Clone, I, I2> Constrain<I2> for $a<T, I> {
35            type Lift = $a<T, I2>;
36            fn i_force(&self, i: I2) -> Self::Lift {$a {k: self.k.clone(), i}}
37        }
38    };
39    ($a:ident) => {
40        impl<I, I2> Constrain<I2> for $a<I> {
41            type Lift = $a<I2>;
42            fn i_force(&self, i: I2) -> Self::Lift {$a {i}}
43        }
44    }
45}
46
47con_impl!{Not}
48con_impl!{Id t}
49con_impl!{False1 t}
50con_impl!{And}
51con_impl!{Or}
52con_impl!{Eq t}
53con_impl!{Xor}
54con_impl!{Nand}
55con_impl!{Nor}
56con_impl!{Exc}
57con_impl!{Rexc}
58con_impl!{Nexc}
59con_impl!{Nrexc}
60con_impl!{Even t}
61con_impl!{Odd t}
62con_impl!{Add t}
63con_impl!{AddK k}
64con_impl!{GeK k}
65con_impl!{LtK k}
66con_impl!{EqK k}
path_semantics_std/constrain.rs

path_semantics_std/
constrain.rs
