hax_rust_engine/
resugarings.rs

1//! The "resugaring" phases used by printers.
2
3//! This module defines resugarings instances (see
4//! [`hax_rust_engine::ast::Resugaring`] for the definition of a
5//! resugaring). Each backend defines its own set of resugaring phases.
6
7use crate::ast::identifiers::global_id::DefId;
8use crate::ast::resugared::*;
9use crate::ast::visitors::*;
10use crate::ast::*;
11use crate::printer::*;
12use std::collections::HashSet;
13
14/// Binop resugaring. Used to identify expressions of the form `(f e1 e2)` where
15/// `f` is a known identifier.
16pub struct BinOp {
17    /// Stores a set of identifiers that should be resugared as binary
18    /// operations. Usually, those identifiers come from the hax encoding. Each
19    /// backend can select its own set of identifiers Typically, if the backend
20    /// has a special support for addition, `known_ops` will contain
21    /// `hax::machine::int::add`
22    pub known_ops: HashSet<DefId>,
23}
24
25impl BinOp {
26    /// Adds a new binary operation from a list of (hax-introduced) names
27    pub fn new(known_ops: &[DefId]) -> Self {
28        Self {
29            known_ops: HashSet::from_iter(known_ops.iter().cloned()),
30        }
31    }
32}
33
34impl AstVisitorMut for BinOp {
35    fn enter_expr_kind(&mut self, x: &mut ExprKind) {
36        let ExprKind::App {
37            head,
38            args,
39            generic_args,
40            bounds_impls,
41            trait_,
42        }: &mut ExprKind = x
43        else {
44            return;
45        };
46        let ExprKind::GlobalId(id) = &*head.kind else {
47            return;
48        };
49        let [lhs, rhs] = &args[..] else { return };
50        if self.known_ops.iter().any(|defid| id == defid) {
51            *x = ExprKind::Resugared(ResugaredExprKind::BinOp {
52                op: id.clone(),
53                lhs: lhs.clone(),
54                rhs: rhs.clone(),
55                generic_args: generic_args.clone(),
56                bounds_impls: bounds_impls.clone(),
57                trait_: trait_.clone(),
58            });
59        }
60    }
61}
62
63impl Resugaring for BinOp {
64    fn name(&self) -> String {
65        "binop".to_string()
66    }
67}
hax_rust_engine/resugarings.rs

hax_rust_engine/
resugarings.rs
