1 
use mcrl2_sys::atermpp;
2 
use mcrl2_sys::cxx::UniquePtr;
3 
use mcrl2_sys::data::ffi;
4 

            

        

            

                5
            

            

                
            

            

                
use crate::aterm::ATerm;

            

        

            

                6
            

            

                
            

            

                
use crate::data::DataSpecification;

            

        

            

                7
            

            

                
            

            

                

            

        

            

                8
            

            

                
            

            

                
use super::DataExpression;

            

        

            

                9
            

            

                
            

            

                

            

        

            

                10
            

            

                
            

            

                
pub struct JittyRewriter {

            

        

            

                11
            

            

                
            

            

                
    rewriter: UniquePtr<ffi::RewriterJitty>,

            

        

            

                12
            

            

                
            

            

                
}

            

        

            

                13
            

            

                
            

            

                

            

        

            

                14
            

            

                
            

            

                
impl JittyRewriter {

            

        

            

                15
            

            

                
            

            

                
    /// Create a rewriter instance from the given data specification.

            

        

            

                16
            

            

                1
            

            

                
    pub fn new(spec: &DataSpecification) -> JittyRewriter {

            

        

            

                17
            

            

                1
            

            

                
        JittyRewriter {

            

        

            

                18
            

            

                1
            

            

                
            rewriter: ffi::create_jitty_rewriter(&spec.data_spec),

            

        

            

                19
            

            

                1
            

            

                
        }

            

        

            

                20
            

            

                1
            

            

                
    }

            

        

            

                21
            

            

                
            

            

                

            

        

            

                22
            

            

                
            

            

                
    /// Rewrites the term with the jitty rewriter.

            

        

            

                23
            

            

                1
            

            

                
    pub fn rewrite(&mut self, term: DataExpression) -> DataExpression {

            

        

            

                24
            

            

                1
            

            

                
        unsafe {

            

        

            

                25
            

            

                1
            

            

                
            atermpp::ffi::enable_automatic_garbage_collection(true);

            

        

            

                26
            

            

                1
            

            

                
            let result: ATerm = ffi::rewrite(self.rewriter.pin_mut(), term.get()).into();

            

        

            

                27
            

            

                1
            

            

                
            atermpp::ffi::enable_automatic_garbage_collection(false);

            

        

            

                28
            

            

                1
            

            

                
            result.into()

            

        

            

                29
            

            

                1
            

            

                
        }

            

        

            

                30
            

            

                1
            

            

                
    }

            

        

            

                31
            

            

                
            

            

                
}

            

        

            

                32
            

            

                
            

            

                

            

        

            

                33
            

            

                
            

            

                
#[cfg(test)]

            

        

            

                34
            

            

                
            

            

                
mod tests {

            

        

            

                35
            

            

                
            

            

                
    use crate::data::DataExpression;

            

        

            

                36
            

            

                
            

            

                

            

        

            

                37
            

            

                
            

            

                
    use super::*;

            

        

            

                38
            

            

                
            

            

                

            

        

            

                39
            

            

                
            

            

                
    #[test]

            

        

            

                40
            

            

                1
            

            

                
    fn test_jitty() {

            

        

            

                41
            

            

                1
            

            

                
        let spec = DataSpecification::new(&include_str!("../../../../examples/REC/mcrl2/revelt.dataspec")).unwrap();

            

        

            

                42
            

            

                1
            

            

                
        let terms: Vec<DataExpression> = include_str!("../../../../examples/REC/mcrl2/revelt.expressions")

            

        

            

                43
            

            

                1
            

            

                
            .lines()

            

        

            

                44
            

            

                1
            

            

                
            .map(|text| spec.parse(text).unwrap())

            

        

            

                45
            

            

                1
            

            

                
            .collect();

            

        

            

                46
            

            

                1
            

            

                

            

        

            

                47
            

            

                1
            

            

                
        // let mut sa = SabreRewriter::new(tp.clone(), &spec.clone().into());

            

        

            

                48
            

            

                1
            

            

                
        let mut inner = JittyRewriter::new(&spec);

            

        

            

                49
            

            

                1
            

            

                
        let mut expected = include_str!("../../../sabre/tests/snapshot/result_revelt.txt").split('\n');

            

        

            

                50
            

            

                
            

            

                

            

        

            

                51
            

            

                2
            

            

                
        for term in &terms {

            

        

            

                52
            

            

                1
            

            

                
            let expected_result = spec.parse(expected.next().unwrap()).unwrap();

            

        

            

                53
            

            

                1
            

            

                

            

        

            

                54
            

            

                1
            

            

                
            let result = inner.rewrite(term.clone());

            

        

            

                55
            

            

                1
            

            

                
            assert_eq!(

            

        

            

                56
            

            

                1
            

            

                
                result,

            

        

            

                57
            

            

                1
            

            

                
                expected_result.into(),

            

        

            

                58
            

            

                
            

            

                
                "The inner rewrite result doesn't match the expected result"

            

        

            

                59
            

            

                
            

            

                
            );

            

        

            

                60
            

            

                
            

            

                
        }

            

        

            

                61
            

            

                1
            

            

                
    }

            

        

            

                62
            

            

                
            

            

                
}