haloumi-ir 0.5.11

Intermediate representation of the haloumi framework.
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55

use eqv::EqvRelation;
use haloumi_core::{eqv::SymbolicEqv, slot::Slot};
use haloumi_lowering::{Lowering, lowerable::LowerableStmt};

pub struct AssumeDeterministic(Slot);

impl AssumeDeterministic {
    pub fn new(f: Slot) -> Self {
        Self(f)
    }

    pub fn value(&self) -> Slot {
        self.0
    }

    pub fn value_mut(&mut self) -> &mut Slot {
        &mut self.0
    }
}

impl LowerableStmt for AssumeDeterministic {
    fn lower<L>(self, l: &L) -> haloumi_lowering::Result<()>
    where
        L: Lowering + ?Sized,
    {
        l.generate_assume_deterministic(self.0)
    }
}

impl Clone for AssumeDeterministic {
    fn clone(&self) -> Self {
        Self(self.0)
    }
}

impl PartialEq for AssumeDeterministic {
    fn eq(&self, other: &Self) -> bool {
        self.0 == other.0
    }
}

impl std::fmt::Debug for AssumeDeterministic {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "assume-deterministic {:?}", self.0)
    }
}

impl EqvRelation<AssumeDeterministic, AssumeDeterministic> for SymbolicEqv
where
    SymbolicEqv: EqvRelation<Slot, Slot>,
{
    fn equivalent(lhs: &AssumeDeterministic, rhs: &AssumeDeterministic) -> bool {
        SymbolicEqv::equivalent(&lhs.0, &rhs.0)
    }
}