hax_rust_engine/phase/
reject_not_do_lean_dsl.rs

1use crate::ast::*;
2use crate::ast::{diagnostics::*, visitors::*};
3use crate::phase::Phase;
4
5/// Rejection Phase for patterns unsupported by Lean's do-notation DSL
6///
7/// This phase rejects unsupported interleavings of expressions and statements.
8/// It is built as a visitor.
9#[derive(Default)]
10pub struct RejectNotDoLeanDSL;
11
12/// Expressions are either do-statements or do-expressions. The former can be downgraded into the
13/// latter.
14#[derive(Clone, Copy, Debug)]
15enum DoDSLExprKind {
16    Statement,
17    Expression,
18}
19
20/// Gives the "kind" of an expression in the do-notation DSL
21fn dsl_expr_kind(expr_kind: &ExprKind) -> DoDSLExprKind {
22    match expr_kind {
23        ExprKind::If { .. } | ExprKind::Match { .. } | ExprKind::Let { .. } => {
24            DoDSLExprKind::Statement
25        }
26        _ => DoDSLExprKind::Expression,
27    }
28}
29
30/// The default value for entry points of expression (function items, function impl items)
31impl Default for DoDSLExprKind {
32    fn default() -> Self {
33        Self::Statement
34    }
35}
36
37/// Visitor internal state
38#[setup_error_handling_struct]
39#[derive(Default)]
40pub struct RejectNotDoLeanDSLVisitor {
41    /// Expected kind for the visited expression. Used by `visit_expr`, ignored by other methods
42    dsl_expr_kind: DoDSLExprKind,
43}
44
45impl VisitorWithContext for RejectNotDoLeanDSLVisitor {
46    fn context(&self) -> Context {
47        Context::Phase(stringify!(RejectNotDoLeanDSL).to_string())
48    }
49}
50
51impl AstVisitorMut for RejectNotDoLeanDSLVisitor {
52    setup_error_handling_impl!();
53
54    fn visit_expr(&mut self, expr: &mut Expr) {
55        use DoDSLExprKind::*;
56        let parent_dsl_expr_kind = self.dsl_expr_kind;
57        self.dsl_expr_kind = match (self.dsl_expr_kind, dsl_expr_kind(&expr.kind)) {
58            // A do-expression cannot be upgraded to a do-statement, we throw an error
59            (Expression, Statement) => {
60                self.error(
61                    expr.clone(),
62                    DiagnosticInfoKind::ExplicitRejection {
63                        reason: "This interleaving of expression and statements does not fit in Lean's do-notation DSL.\
64                                 \nYou may try hoisting out let-bindings and control-flow.".to_string(),
65                        issue_id: Some(1741),
66                    },
67                );
68                Statement
69            }
70            // Closures body are do-statement, as a `do` keyword is introduced
71            (_, _) if matches!(&*expr.kind, ExprKind::Closure { .. }) => Statement,
72            // In other cases, we keep the computed kind
73            (_, kind) => kind,
74        };
75        self.visit_inner(expr);
76        self.dsl_expr_kind = parent_dsl_expr_kind;
77    }
78
79    /// Visitor for types. Array lengths can be any (const) expression, so they are checked for dsl
80    /// patterns (as DoDSL-expressions)
81    fn visit_ty(&mut self, ty: &mut Ty) {
82        if let TyKind::Array { length, .. } = ty.kind_mut() {
83            // The Lean Backend does not support computation in array lengths yet.  It should be
84            // possible to have do-blocks, and treat them like constants. See
85            // https://github.com/cryspen/hax/issues/1713
86            let parent_dsl_expr_kind = self.dsl_expr_kind;
87            self.dsl_expr_kind = DoDSLExprKind::Expression;
88            self.visit_inner(&mut *length);
89            self.dsl_expr_kind = parent_dsl_expr_kind;
90        }
91    }
92}
93
94impl Phase for RejectNotDoLeanDSL {
95    fn apply(&self, items: &mut Vec<Item>) {
96        // Entry points are statements
97        RejectNotDoLeanDSLVisitor::default().visit(items)
98    }
99}
hax_rust_engine/phase/reject_not_do_lean_dsl.rs

hax_rust_engine/phase/
reject_not_do_lean_dsl.rs
