fn test_term_rewriter()

in smt2parser/src/rewriter.rs [924:1044]


fn test_term_rewriter() {
    use crate::concrete::*;

    // (assert (let ((x (f x 2))) (= x 3)))
    let command = Command::Assert {
        term: Term::Let {
            var_bindings: vec![(
                Symbol("x".into()),
                Term::Application {
                    qual_identifier: QualIdentifier::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("f".into()),
                        },
                    },
                    arguments: vec![
                        Term::QualIdentifier(QualIdentifier::Simple {
                            identifier: Identifier::Simple {
                                symbol: Symbol("x".into()),
                            },
                        }),
                        Term::Constant(Constant::Numeral(num::BigUint::from(2u32))),
                    ],
                },
            )],
            term: Box::new(Term::Application {
                qual_identifier: QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("=".into()),
                    },
                },
                arguments: vec![
                    Term::QualIdentifier(QualIdentifier::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("x".into()),
                        },
                    }),
                    Term::Constant(Constant::Numeral(num::BigUint::from(3u32))),
                ],
            }),
        },
    };

    #[derive(Default)]
    struct Builder(crate::concrete::SyntaxBuilder);
    impl Rewriter for Builder {
        type V = crate::concrete::SyntaxBuilder;
        type Error = crate::concrete::Error;

        fn visitor(&mut self) -> &mut Self::V {
            &mut self.0
        }

        fn process_symbol(&mut self, s: Symbol) -> Result<Symbol, Self::Error> {
            Ok(Symbol(s.0 + "__"))
        }
    }

    let mut builder = Builder::default();

    let command2 = command.clone().accept(&mut builder).unwrap();
    let command3 = Command::Assert {
        term: Term::Let {
            var_bindings: vec![(
                Symbol("x__".into()),
                Term::Application {
                    qual_identifier: QualIdentifier::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("f__".into()),
                        },
                    },
                    arguments: vec![
                        Term::QualIdentifier(QualIdentifier::Simple {
                            identifier: Identifier::Simple {
                                symbol: Symbol("x__".into()),
                            },
                        }),
                        Term::Constant(Constant::Numeral(num::BigUint::from(2u32))),
                    ],
                },
            )],
            term: Box::new(Term::Application {
                qual_identifier: QualIdentifier::Simple {
                    identifier: Identifier::Simple {
                        symbol: Symbol("=__".into()),
                    },
                },
                arguments: vec![
                    Term::QualIdentifier(QualIdentifier::Simple {
                        identifier: Identifier::Simple {
                            symbol: Symbol("x__".into()),
                        },
                    }),
                    Term::Constant(Constant::Numeral(num::BigUint::from(3u32))),
                ],
            }),
        },
    };

    assert_eq!(command2, command3);

    #[derive(Default)]
    struct Builder2(crate::concrete::SyntaxBuilder);
    impl Rewriter for Builder2 {
        type V = crate::concrete::SyntaxBuilder;
        type Error = crate::concrete::Error;

        fn visitor(&mut self) -> &mut Self::V {
            &mut self.0
        }

        fn visit_assert(&mut self, _: Term) -> Result<Command, Self::Error> {
            Ok(Command::Exit)
        }
    }

    let mut builder = Builder2::default();

    let command2 = command.accept(&mut builder).unwrap();
    let command3 = Command::Exit;
    assert_eq!(command2, command3);
}