haloumi-ir 0.4.0

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
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124

use crate::{
    error::Error,
    expr::IRBexpr,
    stmt::IRStmt,
    traits::{Canonicalize, ConstantFolding},
};
use eqv::{EqvRelation, equiv};
use haloumi_core::eqv::SymbolicEqv;
use haloumi_lowering::{
    Lowering,
    lowerable::{LowerableExpr, LowerableStmt},
};

pub struct PostCond<T>(IRBexpr<T>);

impl<T> PostCond<T> {
    pub fn new(cond: IRBexpr<T>) -> Self {
        Self(cond)
    }

    pub fn cond(&self) -> &IRBexpr<T> {
        &self.0
    }

    pub fn cond_mut(&mut self) -> &mut IRBexpr<T> {
        &mut self.0
    }

    pub fn map<O>(self, f: &mut impl FnMut(T) -> O) -> PostCond<O> {
        PostCond::new(self.0.map(f))
    }

    pub fn map_into<O>(&self, f: &mut impl FnMut(&T) -> O) -> PostCond<O> {
        PostCond::new(self.0.map_into(f))
    }

    pub fn try_map<O, E>(self, f: &mut impl FnMut(T) -> Result<O, E>) -> Result<PostCond<O>, E> {
        self.0.try_map(f).map(PostCond::new)
    }

    pub fn map_inplace(&mut self, f: &mut impl FnMut(&mut T)) {
        self.0.map_inplace(f)
    }

    pub fn try_map_inplace<E>(
        &mut self,
        f: &mut impl FnMut(&mut T) -> Result<(), E>,
    ) -> Result<(), E> {
        self.0.try_map_inplace(f)
    }
    /// Folds the statements if the expressions are constant.
    /// If an assert-like statement folds into a tautology (i.e. `(= 0 0 )`), it gets removed. If it
    /// folds into a unsatisfiable proposition the method returns an error.
    pub fn constant_fold(&mut self) -> Result<Option<IRStmt<T>>, Error>
    where
        T: ConstantFolding + std::fmt::Debug + Clone,
        Error: From<T::Error>,
        T::T: Eq + Ord,
    {
        self.0.constant_fold()?;
        if let Some(b) = self.0.const_value() {
            if b {
                return Ok(Some(IRStmt::empty()));
            } else {
                return Err(Error::FoldedFalseStmt(
                    "post-condition",
                    format!("{:#?}", self.0),
                ));
            }
        }
        Ok(None)
    }
}

impl<T> PostCond<T>
where
    IRBexpr<T>: Canonicalize,
{
    /// Matches the statements against a series of known patterns and applies rewrites if able to.
    pub fn canonicalize(&mut self) {
        self.0.canonicalize();
    }
}

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

impl<T: Clone> Clone for PostCond<T> {
    fn clone(&self) -> Self {
        Self(self.0.clone())
    }
}

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

impl<T: std::fmt::Debug> std::fmt::Debug for PostCond<T> {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        write!(f, "post-condition ")?;
        if f.alternate() {
            write!(f, "{:#?}", self.0)
        } else {
            write!(f, "{:?}", self.0)
        }
    }
}

impl<L, R> EqvRelation<PostCond<L>, PostCond<R>> for SymbolicEqv
where
    SymbolicEqv: EqvRelation<L, R>,
{
    fn equivalent(lhs: &PostCond<L>, rhs: &PostCond<R>) -> bool {
        equiv! { SymbolicEqv | &lhs.0, &rhs.0 }
    }
}