pub fn rewrite_data_spec(

    tp: Rc<RefCell<TermPool>>,

    rewriter: Rewriter,

    filename_dataspec: &str,

    filename_terms: &str,

    output: bool,

) -> anyhow::Result<()> {

    let data_spec_text = fs::read_to_string(filename_dataspec)?;

    let data_spec = DataSpecification::new(&data_spec_text)?;

    let file = File::open(filename_terms).unwrap();

    // Read and convert the terms

    let terms: Vec<DataExpression> = BufReader::new(file)

        .lines()

        .map(|x| data_spec.parse(&x.unwrap()).unwrap())

        .collect();

    match rewriter {

            let mut jitty_rewriter = JittyRewriter::new(&data_spec);

            // Read the file line by line, and return an iterator of the lines of the file.

            let now = Instant::now();

            for term in &terms {

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

                if output {

                    println!("{}", result)

                }

            println!("Jitty rewrite took {} ms", now.elapsed().as_millis());

            let rewrite_spec = RewriteSpecification::from(data_spec.clone());

            let mut inner_rewriter = InnermostRewriter::new(tp.clone(), &rewrite_spec);

            // Read the file line by line, and return an iterator of the lines of the file.

            let now = Instant::now();

            for term in &terms {

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

                if output {

                    println!("{}", result)

                }

            println!("Innermost rewrite took {} ms", now.elapsed().as_millis());

            let rewrite_spec = RewriteSpecification::from(data_spec.clone());

            let mut sabre_rewriter = SabreRewriter::new(tp.clone(), &rewrite_spec);

            let now = Instant::now();

            for term in &terms {

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

                if output {

                    println!("{}", result)

                }

            println!("Sabre rewrite took {} ms", now.elapsed().as_millis());

    Ok(())

}

pub fn rewrite_rec(rewriter: Rewriter, filename_specification: &str, output: bool) -> anyhow::Result<()> {

    let tp = Rc::new(RefCell::new(TermPool::new()));

    let (syntax_spec, syntax_terms) = load_REC_from_file(&mut tp.borrow_mut(), filename_specification.into()).unwrap();

    let spec = syntax_spec.to_rewrite_spec(&mut tp.borrow_mut());

    match rewriter {

            let mut inner = InnermostRewriter::new(tp.clone(), &spec);

            let now = Instant::now();

            for term in &syntax_terms {

                let term = to_untyped_data_expression(&mut tp.borrow_mut(), term, &AHashSet::new());

                let result = inner.rewrite(term);

                if output {

                    println!("{}", result)

                }

            println!("Innermost rewrite took {} ms", now.elapsed().as_millis());

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

            let now = Instant::now();

            for term in &syntax_terms {

                let term = to_untyped_data_expression(&mut tp.borrow_mut(), term, &AHashSet::new());

                let result = sa.rewrite(term);

                if output {

                    println!("{}", result)

                }

            println!("Sabre rewrite took {} ms", now.elapsed().as_millis());

            bail!("Cannot use REC specifications with mCRL2's jitty rewriter");

    Ok(())

}