Merge pull request #1607 from cryspen/lean-update-printer

Update Lean printer to new infrastructure

Author: W95Psp

hax-lib/proof-libs/lean/Hax/Lib.lean

@@ -221,6 +221,8 @@ instance {β} : Coe (α -> i32 -> β) (α -> Nat -> β) where
 instance : OfNat (Result Nat) n where
   ofNat := pure (n)
 
+instance {α n} [i: OfNat α n] : OfNat (Result α) n where
+  ofNat := pure (i.ofNat)
 
 /-
 
@@ -889,7 +891,9 @@ end Fold
 Rust arrays, are represented as Lean `Vector` (Lean Arrays of known size)
 
 -/
-section Array
+section RustArray
+
+abbrev RustArray := Vector
 
 inductive array_TryFromSliceError where
   | array_TryFromSliceError
@@ -943,7 +947,7 @@ theorem convert_TryInto_try_success_spec {α n} (a: Array α) :
   split <;> grind
 
 
-end Array
+end RustArray
 
 /-
 
@@ -1133,6 +1137,8 @@ Rust vectors are represented as Lean Arrays (variable size)
 -/
 section RustVectors
 
+abbrev RustVector := Array
+
 def alloc_Global : Type := Unit
 def vec_Vec (α: Type) (_Allocator:Type) : Type := Array α
 

rust-engine/src/ast/identifiers.rs

@@ -105,7 +105,7 @@ pub mod global_id {
         /// Tests if the raw output is reduced to "_". Should be used only for
         /// testing. See https://github.com/cryspen/hax/issues/1599
         pub fn is_empty(&self) -> bool {
-            self.to_debug_string() == "_".to_string()
+            self.to_debug_string() == "_"
         }
 
         /// Extract the raw `DefId` from a `GlobalId`.

rust-engine/src/backends.rs

@@ -51,7 +51,7 @@ pub trait Backend {
 
     /// The AST phases to apply before printing.
     ///
-    /// Backends can override this to add transformations.  
+    /// Backends can override this to add transformations.
     /// The default is an empty list (no transformations).
     fn phases(&self) -> Vec<Box<dyn crate::phase::Phase>> {
         vec![]
@@ -111,10 +111,15 @@ mod prelude {
     //! Importing this prelude saves repetitive `use` lists in per-backend
     //! modules without forcing these names on downstream users.
     pub use super::Backend;
+    pub use crate::ast::identifiers::*;
+    pub use crate::ast::literals::*;
+    pub use crate::ast::resugared::*;
     pub use crate::ast::*;
     pub use crate::printer::*;
+    pub use crate::symbol::Symbol;
     pub use hax_rust_engine_macros::prepend_associated_functions_with;
     pub use pretty::DocAllocator;
+    pub use pretty::DocBuilder;
     pub use pretty::Pretty;
     pub use pretty_ast::install_pretty_helpers;
 }