Rust engine: errors resugaring.

rust-engine/src/ast/identifiers/global_id.rs

@@ -196,6 +196,17 @@ impl ConcreteId {
     pub fn into_concrete(self) -> GlobalId {
         GlobalId::Concrete(self)
     }
+
+    pub fn from_def_id(def_id: DefId) -> ConcreteId {
+        ConcreteId {
+            def_id: ExplicitDefId {
+                is_constructor: false,
+                def_id,
+            },
+            moved: None,
+            suffix: None,
+        }
+    }
 }
 
 impl PartialEq<DefId> for GlobalId {

rust-engine/src/backends/lean.rs

@@ -19,16 +19,19 @@ impl_doc_allocator_for!(LeanPrinter);
 
 impl Printer for LeanPrinter {
     fn resugaring_phases() -> Vec<Box<dyn Resugaring>> {
-        vec![Box::new(BinOp::new(&[
-            binops::add(),
-            binops::sub(),
-            binops::mul(),
-            binops::rem(),
-            binops::div(),
-            binops::shr(),
-            binops::logical_op_and(),
-            binops::logical_op_or(),
-        ]))]
+        vec![
+            Box::new(BinOp::new(&[
+                binops::add(),
+                binops::sub(),
+                binops::mul(),
+                binops::rem(),
+                binops::div(),
+                binops::shr(),
+                binops::logical_op_and(),
+                binops::logical_op_or(),
+            ])),
+            Box::new(crate::resugarings::Errors),
+        ]
     }
 
     const NAME: &str = "Lean";

rust-engine/src/resugarings.rs

@@ -65,3 +65,44 @@ impl Resugaring for BinOp {
         "binop".to_string()
     }
 }
+
+/// Errors resugaring. Transforms error nodes into applications
+/// of the `hax_error` function. This is actually a desugaring
+/// but it is useful at the same time as the resugarings so we
+/// keep it here.
+pub struct Errors;
+
+impl AstVisitorMut for Errors {
+    fn enter_expr(&mut self, x: &mut Expr) {
+        if let ExprKind::Error(ErrorNode { fragment, .. }) = x.kind() {
+            let error_fn = identifiers::global_id::ConcreteId::from_def_id(
+                crate::names::rust_primitives::hax::Failure(),
+            )
+            .into_concrete();
+            let head = Expr {
+                kind: Box::new(ExprKind::GlobalId(error_fn)),
+                ty: x.ty.clone(),
+                meta: x.meta.clone(),
+            };
+            let args = vec![
+                ExprKind::Literal(literals::Literal::String(crate::symbol::Symbol::new(
+                    format!("{:?}", fragment),
+                )))
+                .into_expr(x.meta.span.clone(), x.ty.clone(), Vec::new()),
+            ];
+            *x.kind = ExprKind::App {
+                head,
+                args,
+                generic_args: Vec::new(),
+                bounds_impls: Vec::new(),
+                trait_: None,
+            };
+        }
+    }
+}
+
+impl Resugaring for Errors {
+    fn name(&self) -> String {
+        "errors".to_string()
+    }
+}