diff --git a/CHANGELOG.md b/CHANGELOG.md index 0cd795755..851a2839b 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -30,6 +30,8 @@ Changes to the Lean backend: - Use the explicit monadic phase to insert `pure` and `←` only on demand, and not introduce extra `do` block (#1746) - Rename `Result` monad to `RustM` to avoid confusion with Rust `Result` type (#1768) + - Add support for default methods of traits (#1777) + - Gather definitions in namespaces, shortening names (#1780) Miscellaneous: - Reserve extraction folder for auto-generated files in Lean examples (#1754) diff --git a/Cargo.lock b/Cargo.lock index b3aed4f6a..6b382bb7d 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -143,6 +143,12 @@ dependencies = [ "serde", ] +[[package]] +name = "capitalize" +version = "0.3.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b5271031022835ee8c7582fe67403bd6cb3d962095787af7921027234bab5bf" + [[package]] name = "cargo-hax" version = "0.3.5" @@ -668,6 +674,7 @@ name = "hax-rust-engine" version = "0.3.5" dependencies = [ "camino", + "capitalize", "derive_generic_visitor", "hax-frontend-exporter", "hax-rust-engine-macros", diff --git a/engine/backends/lean/lean_backend.ml b/engine/backends/lean/lean_backend.ml index 3fc2c1e0f..f6f7f8e05 100644 --- a/engine/backends/lean/lean_backend.ml +++ b/engine/backends/lean/lean_backend.ml @@ -14,6 +14,7 @@ include include On.Quote include On.Dyn include On.Unsafe + include On.Trait_item_default end) (struct let backend = Diagnostics.Backend.FStar @@ -45,7 +46,7 @@ module SubtypeToInputLanguage and type state_passing_loop = Features.Off.state_passing_loop and type fold_like_loop = Features.Off.fold_like_loop and type match_guard = Features.Off.match_guard - and type trait_item_default = Features.Off.trait_item_default) = + and type trait_item_default = Features.On.trait_item_default) = struct module FB = InputLanguage @@ -120,7 +121,6 @@ module TransformToInputLanguage = |> Phases.Traits_specs |> Phases.Simplify_hoisting |> Phases.Newtype_as_refinement - |> Phases.Reject.Trait_item_default |> Phases.Bundle_cycles |> Phases.Reorder_fields |> Phases.Sort_items diff --git a/examples/lean_chacha20/Makefile b/examples/lean_chacha20/Makefile index d17d05d56..24332783d 100644 --- a/examples/lean_chacha20/Makefile +++ b/examples/lean_chacha20/Makefile @@ -6,5 +6,5 @@ default: lake build) clean: - -rm -f proofs/lean/extraction/lean_chacha20.lean + -rm -f proofs/lean/extraction/ -cd proofs/lean && lake clean diff --git a/rust-engine/Cargo.toml b/rust-engine/Cargo.toml index 353e6aa77..3ddb39068 100644 --- a/rust-engine/Cargo.toml +++ b/rust-engine/Cargo.toml @@ -22,3 +22,4 @@ pretty = "0.12" derive_generic_visitor = "0.3.0" pastey = "0.1.0" camino = "1.1.11" +capitalize = "0.3.4" \ No newline at end of file diff --git a/rust-engine/src/ast/identifiers/global_id.rs b/rust-engine/src/ast/identifiers/global_id.rs index 1ddc67aef..20c65de48 100644 --- a/rust-engine/src/ast/identifiers/global_id.rs +++ b/rust-engine/src/ast/identifiers/global_id.rs @@ -54,29 +54,6 @@ struct DefIdInner { kind: DefKind, } -impl DefIdInner { - fn to_debug_string(&self) -> String { - fn disambiguator_suffix(disambiguator: u32) -> String { - if disambiguator == 0 { - "".into() - } else { - format!("__{disambiguator}") - } - } - use itertools::Itertools; - std::iter::once(self.krate.clone()) - .chain(self.path.iter().map(|item| match &item.data { - DefPathItem::TypeNs(s) - | DefPathItem::ValueNs(s) - | DefPathItem::MacroNs(s) - | DefPathItem::LifetimeNs(s) => s.clone(), - DefPathItem::Impl => "impl".into(), - other => format!("{other:?}"), - } + &disambiguator_suffix(item.disambiguator))) - .join("::") - } -} - use std::{ cell::{LazyCell, RefCell}, collections::HashMap, @@ -153,6 +130,13 @@ pub struct FreshModule { label: String, } +impl FreshModule { + /// Renders a view of the fresh module identifier. + fn view(&self) -> view::View { + self.clone().into() + } +} + /// [`ReservedSuffix`] helps at deriving fresh identifiers out of existing (Rust) ones. #[derive_group_for_ast] pub enum ReservedSuffix { @@ -180,6 +164,8 @@ pub struct ConcreteId { enum GlobalIdInner { /// A concrete identifier that exists in Rust. Concrete(ConcreteId), + /// A fresh module introduced by Hax (typically, a bundle) + FreshModule(FreshModule), /// A projector. Tuple(TupleId), } @@ -232,8 +218,9 @@ impl From for GlobalId { } } -impl From for ConcreteId { - fn from(value: TupleId) -> Self { +impl TupleId { + /// Creates a ConcreteId from a TupleId: `Tuple(1)` returns `Tuple1` + fn into_owned_concrete_id(self) -> ConcreteId { fn patch_def_id(template: GlobalId, length: usize, field: usize) -> ConcreteId { let GlobalIdInner::Concrete(mut concrete_id) = template.0.get().clone() else { // `patch_def_id` is called with constant values (`hax::Tuple2` @@ -274,12 +261,40 @@ impl From for ConcreteId { use crate::names::rust_primitives::hax; - match value { + match self { TupleId::Type { length } => patch_def_id(hax::Tuple2, length, 0), TupleId::Constructor { length } => patch_def_id(hax::Tuple2::Constructor, length, 0), TupleId::Field { length, field } => patch_def_id(hax::Tuple2::_1, length, field), } } + + /// Creates a static [`ConcreteId`] from a [`TupleId`]: `Tuple(1)` returns `Tuple1`. The function is + /// memoized (as the same tuple ids may appear a lot in a program), and inserts identifiers in + /// the GlobalId table to return a static lifetime. + pub fn as_concreteid(self) -> &'static ConcreteId { + thread_local! { + static MEMO: LazyCell>> = + LazyCell::new(|| RefCell::new(HashMap::new())); + } + + MEMO.with(|memo| { + let mut memo = memo.borrow_mut(); + let reference: &'static ConcreteId = memo.entry(self).or_insert_with(|| { + match GlobalIdInner::Concrete(self.into_owned_concrete_id()) + .intern() + .get() + { + GlobalIdInner::Concrete(concrete_id) => concrete_id, + GlobalIdInner::FreshModule(_) | GlobalIdInner::Tuple(_) => { + // This is a match on the Id that was just inserted in the table as a + // ConcreteId + unreachable!() + } + } + }); + reference + }) + } } /// A interned global identifier in hax. @@ -290,13 +305,27 @@ pub struct GlobalId(Interned); impl GlobalId { /// Extracts the Crate info pub fn krate(self) -> &'static str { - &ConcreteId::from_global_id(self).def_id.def_id.krate + match self.0.get() { + GlobalIdInner::FreshModule(fresh_module) => { + &fresh_module + .hints + .first() + .expect("The hint list should always be non-empty") + .def_id + .krate + } + GlobalIdInner::Concrete(concrete_id) => &concrete_id.def_id.def_id.krate, + GlobalIdInner::Tuple(tuple_id) => &tuple_id.as_concreteid().def_id.def_id.krate, + } } /// Returns true if this global identifier refers to a anonymous constant item. /// TODO: drop this function. No logic should be derived from this. pub fn is_anonymous_const(self) -> bool { - let def_id = self.0.get().def_id(); + let GlobalIdInner::Concrete(concrete_id) = self.0.get() else { + return false; + }; + let def_id = concrete_id.def_id.def_id.get(); let Some(DisambiguatedDefPathItem { data: DefPathItem::ValueNs(s), .. @@ -304,13 +333,7 @@ impl GlobalId { else { return false; }; - matches!(self.0.get().def_id().kind, DefKind::Const) && s == "_" - } - - /// Debug printing of identifiers, for testing purposes only. - /// Prints path in a Rust-like way, as a `::` separated dismabiguated path. - pub fn to_debug_string(self) -> String { - ConcreteId::from_global_id(self).to_debug_string() + matches!(def_id.kind, DefKind::Const) && s == "_" } /// Returns true if the underlying identifier is a constructor @@ -335,41 +358,42 @@ impl GlobalId { self.0.get().is_postcondition() } - /// Renders a view of the concrete identifier. + /// Renders a view of the global identifier. pub fn view(self) -> view::View { - ConcreteId::from_global_id(self).view() + match self.0.get() { + GlobalIdInner::FreshModule(id) => id.view(), + GlobalIdInner::Concrete(id) => id.view(), + GlobalIdInner::Tuple(id) => id.as_concreteid().view(), + } } /// Returns a tuple identifier if `self` is indeed a tuple. pub fn expect_tuple(self) -> Option { match self.0.get() { - GlobalIdInner::Concrete(..) => None, GlobalIdInner::Tuple(tuple_id) => Some(*tuple_id), + _ => None, } } - /// Gets the closest module only parent identifier, that is, the closest - /// parent whose path contains only path chunks of kind `DefKind::Mod`. + /// Gets the closest module only parent identifier, that is, the closest parent whose path + /// contains only path chunks of kind `DefKind::Mod`. Can be itself (for fresh modules). pub fn mod_only_closest_parent(self) -> Self { - let concrete_id = ConcreteId::from_global_id(self).mod_only_closest_parent(); - Self(GlobalIdInner::Concrete(concrete_id).intern()) + match self.0.get() { + GlobalIdInner::FreshModule(_) => self, + GlobalIdInner::Concrete(concrete_id) => concrete_id.mod_only_closest_parent().into(), + GlobalIdInner::Tuple(tuple_id) => { + tuple_id.as_concreteid().mod_only_closest_parent().into() + } + } } } impl GlobalIdInner { - /// Extract the raw `DefId` from a `GlobalId`. - /// This should never be used for name printing. - fn def_id(&self) -> DefId { - ConcreteId::from_global_id(GlobalId(self.intern())) - .def_id - .def_id - } - /// Extract the `ExplicitDefId` from a `GlobalId`. fn explicit_def_id(&self) -> Option { match self { GlobalIdInner::Concrete(concrete_id) => Some(concrete_id.def_id.clone()), - GlobalIdInner::Tuple(_) => None, + _ => None, } } @@ -406,6 +430,12 @@ impl GlobalIdInner { } } +impl From for GlobalId { + fn from(concrete_id: ConcreteId) -> Self { + Self(GlobalIdInner::Concrete(concrete_id).intern()) + } +} + impl ConcreteId { /// Renders a view of the concrete identifier. fn view(&self) -> view::View { @@ -420,7 +450,7 @@ impl ConcreteId { let def_id = parents .into_iter() .take_while(|id| matches!(id.def_id.kind, DefKind::Mod)) - .next() + .last() .expect("Invariant broken: a DefId must always contain at least on `mod` segment (the crate)"); Self { def_id, @@ -428,35 +458,6 @@ impl ConcreteId { suffix: None, } } - - /// Get a static reference to a `ConcreteId` out of a `GlobalId`. - /// When a tuple is encountered, the tuple is rendered into a proper Rust name. - /// This function is memoized, so that we don't recompute Rust names for tuples all the time. - fn from_global_id(value: GlobalId) -> &'static ConcreteId { - thread_local! { - static MEMO: LazyCell>> = - LazyCell::new(|| RefCell::new(HashMap::new())); - } - - MEMO.with(|memo| { - let mut memo = memo.borrow_mut(); - let reference: &'static ConcreteId = - memo.entry(value).or_insert_with(|| match value.0.get() { - GlobalIdInner::Concrete(concrete_id) => concrete_id, - GlobalIdInner::Tuple(tuple_id) => { - match GlobalIdInner::Concrete((*tuple_id).into()).intern().get() { - GlobalIdInner::Concrete(concrete_id) => concrete_id, - GlobalIdInner::Tuple(_) => unreachable!(), - } - } - }); - reference - }) - } - - fn to_debug_string(&self) -> String { - self.def_id.def_id.get().to_debug_string() - } } impl PartialEq for GlobalId { @@ -485,3 +486,67 @@ impl PartialEq for ExplicitDefId { other == &self.def_id } } + +#[allow(unused)] +/// Prints identifiers for debugging/development. Should not be used in production code. +trait DebugString { + /// Debug printing of identifiers, for testing purposes only. + /// Prints path in a Rust-like way, as a `::` separated dismabiguated path. + fn to_debug_string(&self) -> String; +} + +impl DebugString for TupleId { + fn to_debug_string(&self) -> String { + match self { + TupleId::Type { length } => format!("Tuple_type({length})"), + TupleId::Constructor { length } => format!("Tuple_constructor({length})"), + TupleId::Field { length, field } => format!("Tuple_projector({length}, {field})"), + } + } +} + +impl DebugString for FreshModule { + /// Used only for debugging purposes. Does not guarantee to be unique + fn to_debug_string(&self) -> String { + format!("fresh_module_{}_{}", self.id, self.label) + } +} + +impl DebugString for ConcreteId { + fn to_debug_string(&self) -> String { + self.def_id.def_id.get().to_debug_string() + } +} + +impl DebugString for DefIdInner { + fn to_debug_string(&self) -> String { + fn disambiguator_suffix(disambiguator: u32) -> String { + if disambiguator == 0 { + "".into() + } else { + format!("__{disambiguator}") + } + } + use itertools::Itertools; + std::iter::once(self.krate.clone()) + .chain(self.path.iter().map(|item| match &item.data { + DefPathItem::TypeNs(s) + | DefPathItem::ValueNs(s) + | DefPathItem::MacroNs(s) + | DefPathItem::LifetimeNs(s) => s.clone(), + DefPathItem::Impl => "impl".into(), + other => format!("{other:?}"), + } + &disambiguator_suffix(item.disambiguator))) + .join("::") + } +} + +impl DebugString for GlobalId { + fn to_debug_string(&self) -> String { + match self.0.get() { + GlobalIdInner::Concrete(id) => id.to_debug_string(), + GlobalIdInner::FreshModule(id) => id.to_debug_string(), + GlobalIdInner::Tuple(id) => id.to_debug_string(), + } + } +} diff --git a/rust-engine/src/ast/identifiers/global_id/view.rs b/rust-engine/src/ast/identifiers/global_id/view.rs index 6675892e0..3e900f74a 100644 --- a/rust-engine/src/ast/identifiers/global_id/view.rs +++ b/rust-engine/src/ast/identifiers/global_id/view.rs @@ -109,6 +109,7 @@ use hax_frontend_exporter::{CtorOf, DefKind, DefPathItem, ImplInfos}; use crate::{ + ast::GlobalId, ast::identifiers::global_id::{DefId, ExplicitDefId}, symbol::Symbol, }; @@ -329,7 +330,13 @@ mod rustc_invariant_handling { impl ErrorDummyValue for DefId { fn error_dummy_value(_: Permit) -> Self { - names::rust_primitives::hax::failure.0.get().def_id() + match names::rust_primitives::hax::failure.0.get() { + crate::ast::identifiers::global_id::GlobalIdInner::Concrete(concrete_id) => { + concrete_id.def_id.def_id + } + // The error dummy value is generated by hax, with a concrete identifier + _ => unreachable!("Hax generated name for failure is concrete"), + } } } @@ -543,11 +550,9 @@ impl PathSegment { pub fn kind(&self) -> &K { &self.kind } -} -impl PathSegment { /// Maps the segment's `kind` while preserving all other fields. - fn map(self, f: impl Fn(T, &DefId) -> U) -> PathSegment { + fn map(self, f: impl Fn(K, &DefId) -> U) -> PathSegment { let Self { identifier, payload, @@ -564,6 +569,17 @@ impl PathSegment { } } +impl PartialEq for PathSegment { + fn eq(&self, other: &GlobalId) -> bool { + match other.0.get() { + super::GlobalIdInner::Concrete(concrete_id) => { + concrete_id.def_id.def_id == self.identifier + } + _ => false, + } + } +} + impl PathSegment { /// Asserts that this segment is a [`TypeDefKind`] and narrows the type. /// @@ -736,6 +752,8 @@ impl PathSegment { mod view_encapsulation { //! Encapsulation module to scope [`View`]'s invariants + use crate::ast::{identifiers::global_id::FreshModule, span::Span}; + use super::*; /// A view for an [`ExplicitDefId`], materialized as a list of typed /// [`PathSegment`]s ordered from the crate root/module towards the item. @@ -800,5 +818,29 @@ mod view_encapsulation { Self(inner) } } + + impl From for View { + fn from(value: FreshModule) -> Self { + use crate::ast::diagnostics::{Context, DiagnosticInfo}; + (DiagnosticInfo { + context: Context::NameView, + span: Span::dummy(), + kind: hax_types::diagnostics::Kind::Unimplemented { + issue_id: Some(1779), + details: Some( + "Unsupported fresh modules, which should only come from the fstar-phase for bundling" + .into(), + ), + }, + }).emit(); + // dummy value + value + .hints + .first() + .expect("The list of hints should be non-empty") + .clone() + .into() + } + } } pub use view_encapsulation::View; diff --git a/rust-engine/src/backends.rs b/rust-engine/src/backends.rs index c9cf53ddb..a82a231b6 100644 --- a/rust-engine/src/backends.rs +++ b/rust-engine/src/backends.rs @@ -81,31 +81,31 @@ pub trait Backend { /// Compute the relative filesystem path where a given module should be written. fn module_path(&self, module: &Module) -> Utf8PathBuf; -} -/// Apply a backend to a collection of AST items, producing output files. -/// -/// This runs all of the backend's [`Backend::phases`], groups the items into -/// modules via [`Backend::items_to_module`], and then uses the backend's printer -/// to generate source files with paths determined by [`Backend::module_path`]. -pub fn apply_backend(backend: B, mut items: Vec) -> Vec { - for phase in backend.phases() { - phase.apply(&mut items); - } + /// Apply a backend to a collection of AST items, producing output files. + /// + /// This runs all of the backend's [`Backend::phases`], groups the items into + /// modules via [`Backend::items_to_module`], and then uses the backend's printer + /// to generate source files with paths determined by [`Backend::module_path`]. + fn apply(&self, mut items: Vec) -> Vec { + for phase in self.phases() { + phase.apply(&mut items); + } - let modules = backend.items_to_module(items); - modules - .into_iter() - .map(|module: Module| { - let path = backend.module_path(&module).into_string(); - let (contents, _) = backend.printer().print(module); - File { - path, - contents, - sourcemap: None, - } - }) - .collect() + let modules = self.items_to_module(items); + modules + .into_iter() + .map(|module: Module| { + let path = self.module_path(&module).into_string(); + let (contents, _) = self.printer().print(module); + File { + path, + contents, + sourcemap: None, + } + }) + .collect() + } } mod prelude { diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 863de11db..b82886cca 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -4,10 +4,15 @@ //! Pretty::Doc type, which can in turn be exported to string (or, eventually, //! source maps). -use std::collections::HashSet; +use std::collections::{HashMap, HashSet}; use std::sync::LazyLock; +use capitalize::Capitalize; +use hax_types::engine_api::File; + use super::prelude::*; +use crate::ast::identifiers::global_id::view::View; +use crate::ast::span::Span; use crate::{ ast::identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind}, phase::{ @@ -29,9 +34,20 @@ const PURE: GlobalId = pure; /// The Lean printer #[setup_span_handling_struct] #[derive(Default, Clone)] -pub struct LeanPrinter; - +pub struct LeanPrinter { + current_namespace: Option, +} const INDENT: isize = 2; +const FILE_HEADER: &str = " +-- Experimental lean backend for Hax +-- The Hax prelude library can be found in hax/proof-libs/lean +import Hax +import Std.Tactic.Do +open Std.Do +set_option mvcgen.warning false +set_option linter.unusedVariables false + +"; static RESERVED_KEYWORDS: LazyLock> = LazyLock::new(|| { HashSet::from_iter( @@ -54,6 +70,27 @@ impl RenderView for LeanPrinter { fn separator(&self) -> &str { "." } + + fn render_string(&self, view: &View) -> String { + self.render_strings(view) + .collect::>() + .join(self.separator()) + } + + fn render_strings(&self, view: &View) -> impl Iterator { + let mut path = view.segments(); + if let Some(namespace) = self.current_namespace + && let Some((i, _)) = path + .iter() + .enumerate() + .find(|(_, segment)| *segment == &namespace) + { + path = path.get((i + 1)..).unwrap_or(path); + }; + path.iter() + .flat_map(|segment| self.render_path_segment(segment)) + } + fn render_path_segment(&self, chunk: &PathSegment) -> Vec { fn uppercase_first(s: &str) -> String { let mut c = s.chars(); @@ -62,6 +99,7 @@ impl RenderView for LeanPrinter { Some(first) => first.to_uppercase().collect::() + c.as_str(), } } + // Returning None indicates that the default rendering should be used (match chunk.kind() { AnyKind::Mod => { @@ -141,6 +179,71 @@ impl Backend for LeanBackend { fn phases(&self) -> Vec> { vec![Box::new(RejectNotDoLeanDSL), Box::new(ExplicitMonadic)] } + + fn items_to_module(&self, items: Vec) -> Vec { + // This is incorrect, as it ignores dependencies + let mut modules: HashMap<_, Vec<_>> = HashMap::new(); + for item in items { + let module_ident = item.ident.mod_only_closest_parent(); + modules.entry(module_ident).or_default().push(item); + } + modules + .into_iter() + .map(|(ident, items)| Module { + ident, + items, + meta: Metadata { + span: Span::dummy(), + attributes: vec![], + }, + }) + .collect() + } + + fn apply(&self, mut items: Vec) -> Vec { + // This function decides how the Lean backend turns a list of items into a list of + // files. Right now, all items are bundled in a single file. + + // Applying Rust-engine phases (OCaml engines phases have already been applied at this + // point) + for phase in self.phases() { + phase.apply(&mut items); + } + + // Removing unprintable items + let items: Vec = items + .into_iter() + .filter(LeanPrinter::printable_item) + .collect(); + + // All modules are bundled in a single file, named after the crate + let krate = items + .first() + .expect("The list of items should be non-empty") + .ident + .krate() + .capitalize(); + let mut path = camino::Utf8PathBuf::new(); + path.push(krate); + path.set_extension("lean"); + + // The split in modules is used to introduce namespaces + let modules = self.items_to_module(items); + let content = modules + .into_iter() + .map(|module: Module| self.printer().print(module).0) + .collect::>() + .join("\n"); + + let header: String = FILE_HEADER.to_string(); + + // Single bundle output + vec![File { + path: path.into_string(), + contents: header + &content, + sourcemap: None, + }] + } } impl LeanPrinter { @@ -324,6 +427,16 @@ const _: () = { fn do_block>(&self, body: D) -> DocBuilder { docs!["do", line!(), body].group() } + + /// Produces a fresh name for a constraint on an associated type. It needs a fresh name to + /// be added as an extra field + fn fresh_constraint_name( + &self, + associated_type_name: &String, + constraint: &ImplIdent, + ) -> String { + format!("_constr_{}_{}", associated_type_name, constraint.name) + } } impl PrettyAst for LeanPrinter { @@ -342,33 +455,28 @@ const _: () = { } fn module(&self, module: &Module) -> DocBuilder { + let current_namespace = module.ident; + let new_printer = LeanPrinter { + current_namespace: Some(current_namespace), + ..LeanPrinter::default() + }; let items = &module.items; - docs![ - intersperse!( - " --- Experimental lean backend for Hax --- The Hax prelude library can be found in hax/proof-libs/lean -import Hax -import Std.Tactic.Do -import Std.Do.Triple -import Std.Tactic.Do.Syntax -open Std.Do -open Std.Tactic -set_option mvcgen.warning false -set_option linter.unusedVariables false - - -" - .lines(), - hardline!(), - ), + docs![ + "namespace ", + current_namespace, + hardline!(), + hardline!(), intersperse!( - items - .iter() - .filter(|item| LeanPrinter::printable_item(item)), + items.iter().map(|item| { item.to_document(&new_printer) }), docs![hardline!(), hardline!()] - ) + ), + hardline!(), + hardline!(), + "end ", + current_namespace, + hardline!(), + hardline!(), ] } @@ -892,7 +1000,9 @@ set_option linter.unusedVariables false "Structures should always have a constructor (even empty ones)" ) }; - let args = if !variant.is_record { + let args = if variant.arguments.is_empty() { + comment!["no fields"] + } else if !variant.is_record { // Tuple-like structure, using positional arguments intersperse!( variant.arguments.iter().enumerate().map(|(i, (_, ty, _))| { @@ -928,11 +1038,16 @@ set_option linter.unusedVariables false docs![ docs!["inductive ", name, line!(), generics, ": Type"].group(), hardline!(), - concat!(variants.iter().map(|variant| docs![ - "| ", - docs![variant, applied_name.clone()].group().nest(INDENT), + intersperse!( + variants.iter().map(|variant| docs![ + "| ", + variant, + applied_name.clone() + ] + .group() + .nest(INDENT)), hardline!() - ])), + ), ] } } @@ -961,7 +1076,7 @@ set_option linter.unusedVariables false .map(|constraint: &GenericConstraint| { match constraint { GenericConstraint::Type(tc_constraint) => docs![ - format!("_constr_{}", tc_constraint.name), + self.fresh_constraint_name(&self.render_last(name), tc_constraint), " :", line!(), constraint @@ -1004,14 +1119,18 @@ set_option linter.unusedVariables false .nest(INDENT), docs![ hardline!(), - intersperse!( - items.iter().filter(|item| { - // TODO: should be treated directly by name rendering, see : - // https://github.com/cryspen/hax/issues/1646 - !(item.ident.is_precondition() || item.ident.is_postcondition()) - }), - hardline!() - ) + if items.is_empty() { + comment!["no fields"] + } else { + intersperse!( + items.iter().filter(|item| { + // TODO: should be treated directly by name rendering, see : + // https://github.com/cryspen/hax/issues/1646 + !(item.ident.is_precondition() || item.ident.is_postcondition()) + }), + hardline!() + ) + } ] .nest(INDENT), ], @@ -1077,7 +1196,7 @@ set_option linter.unusedVariables false concat!(constraints.iter().map(|c| docs![ hardline!(), docs![ - format!("_constr_{}", c.name), + self.fresh_constraint_name(&name, c), reflow!(" :"), line!(), &c.goal @@ -1088,8 +1207,22 @@ set_option linter.unusedVariables false ])) ] } - TraitItemKind::Default { .. } => - emit_error!(issue 1707, "Unsupported default implementation for trait items"), + TraitItemKind::Default { params, body } => docs![ + docs![ + name, + softline!(), + generics, + zip_right!(params, line!()).group(), + docs![": RustM ", body.ty].group(), + line!(), + ":= do", + ] + .group(), + line!(), + body, + ] + .group() + .nest(INDENT), TraitItemKind::Resugared(_) => { unreachable!("This backend has no resugaring for trait items") } diff --git a/rust-engine/src/main.rs b/rust-engine/src/main.rs index a022f4ca0..9c95ce9c4 100644 --- a/rust-engine/src/main.rs +++ b/rust-engine/src/main.rs @@ -1,5 +1,5 @@ use hax_rust_engine::{ - backends, + backends::{self, lean::LeanBackend, rust::RustBackend}, ocaml_engine::{ExtendedToEngine, Response}, }; use hax_types::{cli_options::Backend, engine_api::File}; @@ -24,7 +24,8 @@ fn main() { panic!() }; - let files = match &value.backend.backend { + let backend = &value.backend.backend; + let files = match backend { Backend::Fstar { .. } | Backend::Coq | Backend::Ssprove @@ -33,8 +34,8 @@ fn main() { "The Rust engine cannot be called with backend {}.", value.backend.backend ), - Backend::Lean => backends::apply_backend(backends::lean::LeanBackend, items), - Backend::Rust => backends::apply_backend(backends::rust::RustBackend, items), + Backend::Lean => backends::Backend::apply(&LeanBackend, items), + Backend::Rust => backends::Backend::apply(&RustBackend, items), Backend::GenerateRustEngineNames => vec![File { path: "generated.rs".into(), contents: hax_rust_engine::names::codegen::export_def_ids_to_mod(items), diff --git a/rustfmt.toml b/rustfmt.toml index 350113681..2083782d2 100644 --- a/rustfmt.toml +++ b/rustfmt.toml @@ -1 +1,2 @@ style_edition = "2024" +edition = "2024" diff --git a/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap b/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap index 2d6b10ec3..e9fa5e4f6 100644 --- a/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-core-models into-lean.snap @@ -33,137 +33,38 @@ diagnostics = [] -- The Hax prelude library can be found in hax/proof-libs/lean import Hax import Std.Tactic.Do -import Std.Do.Triple -import Std.Tactic.Do.Syntax open Std.Do -open Std.Tactic - set_option mvcgen.warning false set_option linter.unusedVariables false -inductive Lean_core_models.Result.E1 : Type -| C1 : Lean_core_models.Result.E1 -| C2 : u32 -> Lean_core_models.Result.E1 - - -instance Lean_core_models.Result.Impl : - Core.Clone.Clone Lean_core_models.Result.E1 - where - - -inductive Lean_core_models.Result.E2 : Type -| C1 : Lean_core_models.Result.E2 -| C2 : u32 -> Lean_core_models.Result.E2 - - -def Lean_core_models.Result.tests - (_ : Rust_primitives.Hax.Tuple0) - : Result (Core.Result.Result u32 Lean_core_models.Result.E1) - := do - let v1 : (Core.Result.Result u32 Lean_core_models.Result.E1) := - (Core.Result.Result.Ok (1 : u32)); - let v2 : (Core.Result.Result u32 Lean_core_models.Result.E1) := - (Core.Result.Result.Err Lean_core_models.Result.E1.C1); - let f : (u32 -> Result u32) := (fun x => (do (x +? (1 : u32)) : Result u32)); - let v5 : (Core.Result.Result i32 Lean_core_models.Result.E1) ← - (Core.Result.Impl.map i32 Lean_core_models.Result.E1 i32 (i32 -> Result i32) - (Core.Result.Result.Ok (1 : i32)) - (fun v => (do (v +? (1 : i32)) : Result i32))); - let v6 : u32 ← - (Core.Result.Impl.map_or - u32 - Lean_core_models.Result.E1 - u32 - (u32 -> Result u32) (Core.Result.Result.Ok (1 : u32)) (9 : u32) f); - let v7 : u32 ← - (Core.Result.Impl.map_or_else - u32 - Lean_core_models.Result.E1 - u32 - (Lean_core_models.Result.E1 -> Result u32) - (u32 -> Result u32) - (Core.Result.Result.Ok (1 : u32)) - (fun _ => (do (pure (10 : u32)) : Result u32)) - f); - let v8 : (Core.Result.Result i32 Lean_core_models.Result.E2) ← - (Core.Result.Impl.map_err - i32 - Lean_core_models.Result.E1 - Lean_core_models.Result.E2 - (Lean_core_models.Result.E1 -> Result Lean_core_models.Result.E2) - (Core.Result.Result.Ok (0 : i32)) - (fun e => (do - match e with - | (Lean_core_models.Result.E1.C1 ) - => (pure Lean_core_models.Result.E2.C1) - | (Lean_core_models.Result.E1.C2 x) - => (pure (Lean_core_models.Result.E2.C2 (← (x +? (1 : u32))))) : - Result Lean_core_models.Result.E2))); - let v9 : Bool ← (Core.Result.Impl.is_ok u32 Lean_core_models.Result.E1 v1); - let v10 : Bool ← (Core.Result.Impl.is_err u32 Lean_core_models.Result.E1 v1); - let v11 : (Core.Result.Result u32 Lean_core_models.Result.E1) ← - (Core.Result.Impl.and_then - u32 - Lean_core_models.Result.E1 - u32 - (u32 -> Result (Core.Result.Result u32 Lean_core_models.Result.E1)) - (← (Core.Clone.Clone.clone v1)) - (fun x => (do - (pure (Core.Result.Result.Ok (← (x +? (1 : u32))))) : Result - (Core.Result.Result u32 Lean_core_models.Result.E1)))); - let v12 : u32 ← - (Core.Result.Impl.unwrap u32 u32 - (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32))))); - let v13 : u32 ← - (Core.Result.Impl.expect u32 u32 - (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32)))) - "Should be Ok"); - match - (← (Core.Result.Impl.map - u32 - Lean_core_models.Result.E1 - u32 - (u32 -> Result u32) v1 f)) - with - | (Core.Result.Result.Ok hoist2) - => - match v2 with - | (Core.Result.Result.Ok hoist1) - => - let v3 : u32 ← (hoist2 +? hoist1); - (pure (Core.Result.Result.Ok v3)) - | (Core.Result.Result.Err err) => (pure (Core.Result.Result.Err err)) - | (Core.Result.Result.Err err) => (pure (Core.Result.Result.Err err)) +namespace Lean_core_models.Option -structure Lean_core_models.Option.S where +structure S where f1 : u32 -inductive Lean_core_models.Option.E : Type -| C : u32 -> Lean_core_models.Option.E - +inductive E : Type +| C : u32 -> E -instance Lean_core_models.Option.Impl : - Core.Default.Default Lean_core_models.Option.S - where +instance Impl : Core.Default.Default S where default (_ : Rust_primitives.Hax.Tuple0) := do - (pure (Lean_core_models.Option.S.mk (f1 := (42 : u32)))) + (pure (S.mk (f1 := (42 : u32)))) -def Lean_core_models.Option.test +def test (_ : Rust_primitives.Hax.Tuple0) - : Result Rust_primitives.Hax.Tuple0 + : RustM Rust_primitives.Hax.Tuple0 := do let o1 : (Core.Option.Option i32) := (Core.Option.Option.Some (4 : i32)); let o2 : (Core.Option.Option i32) := Core.Option.Option.None; let o3 : Bool ← - (Core.Option.Impl.is_some_and i32 (i32 -> Result Bool) + (Core.Option.Impl.is_some_and i32 (i32 -> RustM Bool) (← (Core.Clone.Clone.clone o1)) (fun x => (do - (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : Result Bool))); + (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool))); let o3 : Bool ← - (Core.Option.Impl.is_none_or i32 (i32 -> Result Bool) + (Core.Option.Impl.is_none_or i32 (i32 -> RustM Bool) (← (Core.Clone.Clone.clone o1)) (fun x => (do - (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : Result Bool))); + (Rust_primitives.Hax.Machine_int.eq x (0 : i32)) : RustM Bool))); let o4 : i32 ← (Core.Option.Impl.unwrap i32 (Core.Option.Option.Some (0 : i32))); let o5 : i32 ← @@ -173,53 +74,45 @@ def Lean_core_models.Option.test let o6 : i32 ← (Core.Option.Impl.unwrap_or_else i32 - (Rust_primitives.Hax.Tuple0 -> Result i32) + (Rust_primitives.Hax.Tuple0 -> RustM i32) (Core.Option.Option.Some (0 : i32)) - (fun _ => (do (pure (9 : i32)) : Result i32))); - let o7 : Lean_core_models.Option.S ← - (Core.Option.Impl.unwrap_or_default Lean_core_models.Option.S - Core.Option.Option.None); + (fun _ => (do (pure (9 : i32)) : RustM i32))); + let o7 : S ← (Core.Option.Impl.unwrap_or_default S Core.Option.Option.None); let o8 : (Core.Option.Option i32) ← - (Core.Option.Impl.map i32 i32 (i32 -> Result i32) + (Core.Option.Impl.map i32 i32 (i32 -> RustM i32) (Core.Option.Option.Some (0 : i32)) - (fun x => (do (x +? (1 : i32)) : Result i32))); + (fun x => (do (x +? (1 : i32)) : RustM i32))); let o9 : i32 ← - (Core.Option.Impl.map_or i32 i32 (i32 -> Result i32) + (Core.Option.Impl.map_or i32 i32 (i32 -> RustM i32) (Core.Option.Option.Some (1 : i32)) (9 : i32) - (fun x => (do (x +? (1 : i32)) : Result i32))); + (fun x => (do (x +? (1 : i32)) : RustM i32))); let o10 : i32 ← (Core.Option.Impl.map_or_else i32 i32 - (Rust_primitives.Hax.Tuple0 -> Result i32) - (i32 -> Result i32) + (Rust_primitives.Hax.Tuple0 -> RustM i32) + (i32 -> RustM i32) (Core.Option.Option.Some (2 : i32)) - (fun _ => (do (pure (9 : i32)) : Result i32)) - (fun x => (do (x +? (1 : i32)) : Result i32))); - let o11 : (Core.Result.Result i32 Lean_core_models.Option.E) ← - (Core.Option.Impl.ok_or i32 Lean_core_models.Option.E + (fun _ => (do (pure (9 : i32)) : RustM i32)) + (fun x => (do (x +? (1 : i32)) : RustM i32))); + let o11 : (Core.Result.Result i32 E) ← + (Core.Option.Impl.ok_or i32 E (Core.Option.Option.Some (3 : i32)) - (Lean_core_models.Option.E.C (0 : u32))); - let o12 : (Core.Result.Result i32 Lean_core_models.Option.E) ← - (Core.Option.Impl.ok_or_else - i32 - Lean_core_models.Option.E - (Rust_primitives.Hax.Tuple0 -> Result Lean_core_models.Option.E) + (E.C (0 : u32))); + let o12 : (Core.Result.Result i32 E) ← + (Core.Option.Impl.ok_or_else i32 E (Rust_primitives.Hax.Tuple0 -> RustM E) (Core.Option.Option.Some (1 : i32)) - (fun _ => (do - (pure (Lean_core_models.Option.E.C (1 : u32))) : Result - Lean_core_models.Option.E))); + (fun _ => (do (pure (E.C (1 : u32))) : RustM E))); let o13 : (Core.Option.Option u32) ← - (Core.Option.Impl.and_then u32 u32 (u32 -> Result (Core.Option.Option u32)) + (Core.Option.Impl.and_then u32 u32 (u32 -> RustM (Core.Option.Option u32)) Core.Option.Option.None (fun x => (do - (pure (Core.Option.Option.Some x)) : Result (Core.Option.Option u32)))); + (pure (Core.Option.Option.Some x)) : RustM (Core.Option.Option u32)))); let ⟨_, out⟩ ← - (Core.Option.Impl.take Lean_core_models.Option.S - (Core.Option.Option.Some - (Lean_core_models.Option.S.mk (f1 := (9 : u32))))); - let o14 : (Core.Option.Option Lean_core_models.Option.S) := out; + (Core.Option.Impl.take S + (Core.Option.Option.Some (S.mk (f1 := (9 : u32))))); + let o14 : (Core.Option.Option S) := out; let o15 : Bool ← (Core.Option.Impl.is_some i32 (Core.Option.Option.Some (1 : i32))); let o16 : Bool ← @@ -232,44 +125,31 @@ def Lean_core_models.Option.test (Core.Option.Impl.unwrap i32 (Core.Option.Option.Some (4 : i32))); (pure Rust_primitives.Hax.Tuple0.mk) -structure Lean_core_models.Default.Structs.S where +end Lean_core_models.Option + + +namespace Lean_core_models.Default.Structs + +structure S where f1 : usize -instance Lean_core_models.Default.Structs.Impl : - Core.Default.Default Lean_core_models.Default.Structs.S - where +instance Impl : Core.Default.Default S where default (_ : Rust_primitives.Hax.Tuple0) := do - (pure (Lean_core_models.Default.Structs.S.mk (f1 := (0 : usize)))) + (pure (S.mk (f1 := (0 : usize)))) -def Lean_core_models.Default.Structs.test - (_ : Rust_primitives.Hax.Tuple0) - : Result Lean_core_models.Default.Structs.S - := do +def test (_ : Rust_primitives.Hax.Tuple0) : RustM S := do (Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk) -inductive Lean_core_models.Default.Enums.E (T : Type) : Type -| C1 : u32 -> Lean_core_models.Default.Enums.E (T : Type) -| C2 : T -> Lean_core_models.Default.Enums.E (T : Type) +end Lean_core_models.Default.Structs -instance Lean_core_models.Default.Enums.Impl - (T : Type) [(Core.Default.Default T)] : - Core.Default.Default (Lean_core_models.Default.Enums.E T) - where - default (_ : Rust_primitives.Hax.Tuple0) := do - (pure (Lean_core_models.Default.Enums.E.C2 - (← (Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk)))) +namespace Lean_core_models.Function -def Lean_core_models.Function.test - (_ : Rust_primitives.Hax.Tuple0) - : Result u32 - := do - let f_1 : (u32 -> Result u32) := - (fun _ => (do (pure (9 : u32)) : Result u32)); - let f_2 : (u32 -> u32 -> Result u32) := - (fun x y => (do (x +? y) : Result u32)); - let f_2_tuple : ((Rust_primitives.Hax.Tuple2 u32 u32) -> Result u32) := - (fun ⟨x, y⟩ => (do (x +? y) : Result u32)); +def test (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do + let f_1 : (u32 -> RustM u32) := (fun _ => (do (pure (9 : u32)) : RustM u32)); + let f_2 : (u32 -> u32 -> RustM u32) := (fun x y => (do (x +? y) : RustM u32)); + let f_2_tuple : ((Rust_primitives.Hax.Tuple2 u32 u32) -> RustM u32) := + (fun ⟨x, y⟩ => (do (x +? y) : RustM u32)); ((← ((← (Core.Ops.Function.Fn.call f_1 (Rust_primitives.Hax.Tuple1.mk (0 : u32)))) @@ -279,4 +159,103 @@ def Lean_core_models.Function.test +? (← (Core.Ops.Function.Fn.call f_2_tuple (Rust_primitives.Hax.Tuple1.mk - (Rust_primitives.Hax.Tuple2.mk (1 : u32) (2 : u32))))))''' + (Rust_primitives.Hax.Tuple2.mk (1 : u32) (2 : u32)))))) + +end Lean_core_models.Function + + +namespace Lean_core_models.Default.Enums + +inductive E (T : Type) : Type +| C1 : u32 -> E (T : Type) +| C2 : T -> E (T : Type) + +instance Impl (T : Type) [(Core.Default.Default T)] : + Core.Default.Default (E T) + where + default (_ : Rust_primitives.Hax.Tuple0) := do + (pure (E.C2 + (← (Core.Default.Default.default Rust_primitives.Hax.Tuple0.mk)))) + +end Lean_core_models.Default.Enums + + +namespace Lean_core_models.Result + +inductive E1 : Type +| C1 : E1 +| C2 : u32 -> E1 + +instance Impl : Core.Clone.Clone E1 where + -- no fields + +inductive E2 : Type +| C1 : E2 +| C2 : u32 -> E2 + +def tests + (_ : Rust_primitives.Hax.Tuple0) + : RustM (Core.Result.Result u32 E1) + := do + let v1 : (Core.Result.Result u32 E1) := (Core.Result.Result.Ok (1 : u32)); + let v2 : (Core.Result.Result u32 E1) := (Core.Result.Result.Err E1.C1); + let f : (u32 -> RustM u32) := (fun x => (do (x +? (1 : u32)) : RustM u32)); + let v5 : (Core.Result.Result i32 E1) ← + (Core.Result.Impl.map i32 E1 i32 (i32 -> RustM i32) + (Core.Result.Result.Ok (1 : i32)) + (fun v => (do (v +? (1 : i32)) : RustM i32))); + let v6 : u32 ← + (Core.Result.Impl.map_or u32 E1 u32 (u32 -> RustM u32) + (Core.Result.Result.Ok (1 : u32)) + (9 : u32) + f); + let v7 : u32 ← + (Core.Result.Impl.map_or_else + u32 + E1 + u32 + (E1 -> RustM u32) + (u32 -> RustM u32) + (Core.Result.Result.Ok (1 : u32)) + (fun _ => (do (pure (10 : u32)) : RustM u32)) + f); + let v8 : (Core.Result.Result i32 E2) ← + (Core.Result.Impl.map_err i32 E1 E2 (E1 -> RustM E2) + (Core.Result.Result.Ok (0 : i32)) + (fun e => (do + match e with + | (E1.C1 ) => (pure E2.C1) + | (E1.C2 x) => (pure (E2.C2 (← (x +? (1 : u32))))) : RustM E2))); + let v9 : Bool ← (Core.Result.Impl.is_ok u32 E1 v1); + let v10 : Bool ← (Core.Result.Impl.is_err u32 E1 v1); + let v11 : (Core.Result.Result u32 E1) ← + (Core.Result.Impl.and_then + u32 + E1 + u32 + (u32 -> RustM (Core.Result.Result u32 E1)) + (← (Core.Clone.Clone.clone v1)) + (fun x => (do + (pure (Core.Result.Result.Ok (← (x +? (1 : u32))))) : RustM + (Core.Result.Result u32 E1)))); + let v12 : u32 ← + (Core.Result.Impl.unwrap u32 u32 + (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32))))); + let v13 : u32 ← + (Core.Result.Impl.expect u32 u32 + (← (Core.Clone.Clone.clone (Core.Result.Result.Ok (0 : u32)))) + "Should be Ok"); + match (← (Core.Result.Impl.map u32 E1 u32 (u32 -> RustM u32) v1 f)) with + | (Core.Result.Result.Ok hoist2) + => + match v2 with + | (Core.Result.Result.Ok hoist1) + => + let v3 : u32 ← (hoist2 +? hoist1); + (pure (Core.Result.Result.Ok v3)) + | (Core.Result.Result.Err err) => (pure (Core.Result.Result.Err err)) + | (Core.Result.Result.Err err) => (pure (Core.Result.Result.Err err)) + +end Lean_core_models.Result + +''' diff --git a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap index 9bca4d6b0..94ca2f589 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -83,238 +83,322 @@ spans = ['Span { lo: Loc { line: 8, col: 10 }, hi: Loc { line: 10, col: 10 }, fi -- The Hax prelude library can be found in hax/proof-libs/lean import Hax import Std.Tactic.Do -import Std.Do.Triple -import Std.Tactic.Do.Syntax open Std.Do -open Std.Tactic - set_option mvcgen.warning false set_option linter.unusedVariables false -class Lean_tests.Traits.Overlapping_methods.T1 (Self : Type) where - f : (Self -> RustM usize) +namespace Lean_tests.Structs.Base_expressions -class Lean_tests.Traits.Overlapping_methods.T2 (Self : Type) where - f : (Self -> RustM usize) +structure S where + f1 : u32 + f2 : u32 + f3 : u32 -class Lean_tests.Traits.Overlapping_methods.T3 (Self : Type) where - f : (Self -> RustM usize) +def test + (_ : Rust_primitives.Hax.Tuple0) + : RustM Rust_primitives.Hax.Tuple0 + := do + let s1 : S := (S.mk (f1 := (1 : u32)) (f2 := (2 : u32)) (f3 := (3 : u32))); + let _ := {s1 with f1 := (0 : u32)}; + let _ := {s1 with f2 := (0 : u32)}; + let _ := {s1 with f3 := (0 : u32)}; + let _ := {s1 with f1 := (0 : u32), f2 := (1 : u32)}; + let _ := {s1 with f2 := (0 : u32), f3 := (1 : u32)}; + let _ := {s1 with f3 := (0 : u32), f1 := (2 : u32)}; + let _ := {s1 with f1 := (0 : u32), f2 := (1 : u32), f3 := (0 : u32)}; + (pure Rust_primitives.Hax.Tuple0.mk) -instance Lean_tests.Traits.Overlapping_methods.Impl : - Lean_tests.Traits.Overlapping_methods.T1 u32 - where - f (self : u32) := do (pure (0 : usize)) +end Lean_tests.Structs.Base_expressions -instance Lean_tests.Traits.Overlapping_methods.Impl_1 : - Lean_tests.Traits.Overlapping_methods.T2 u32 - where - f (self : u32) := do (pure (1 : usize)) -instance Lean_tests.Traits.Overlapping_methods.Impl_2 : - Lean_tests.Traits.Overlapping_methods.T3 u32 - where - f (self : u32) := do (pure (2 : usize)) +namespace Lean_tests.Comments -def Lean_tests.Traits.Overlapping_methods.test - (_ : Rust_primitives.Hax.Tuple0) - : RustM usize - := do - let x : u32 := (9 : u32); - ((← ((← (Lean_tests.Traits.Overlapping_methods.T1.f x)) - +? (← (Lean_tests.Traits.Overlapping_methods.T2.f x)))) - +? (← (Lean_tests.Traits.Overlapping_methods.T3.f x))) +-- Single line doc comment +def f (_ : Rust_primitives.Hax.Tuple0) : RustM Rust_primitives.Hax.Tuple0 := do + (pure Rust_primitives.Hax.Tuple0.mk) -class Lean_tests.Traits.Inheritance.T1 (Self : Type) where +/-- + Block doc-comment : Lorem ipsum dolor sit amet, consectetur adipiscing elit. Vestibulum rutrum + orci ac tellus ullamcorper sollicitudin. Sed fringilla mi id arcu suscipit rhoncus. Pellentesque et + metus a ante feugiat lobortis. Nam a mauris eget nisl congue egestas. Duis et gravida + nulla. Curabitur mattis leo vel molestie posuere. Etiam malesuada et augue eget + varius. Pellentesque quis tincidunt erat. Vestibulum id consectetur turpis. Cras elementum magna id + urna volutpat fermentum. In vel erat quis nunc rhoncus porta. Aliquam sed pellentesque + tellus. Quisque odio diam, mollis ut venenatis non, scelerisque at nulla. Nunc urna ante, tristique + quis nisi quis, congue maximus nisl. Curabitur non efficitur odio. + -/ +def heavily_documented (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do + (pure (4 : u32)) + +end Lean_tests.Comments + + +namespace Lean_tests.Traits.Inheritance + +class T1 (Self : Type) where f1 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.T2 (Self : Type) where +class T2 (Self : Type) where f2 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.T3 (Self : Type) where - [_constr_i0 : (Lean_tests.Traits.Inheritance.T2 Self)] - [_constr_i1 : (Lean_tests.Traits.Inheritance.T1 Self)] +class T3 (Self : Type) where + [_constr_T3_i0 : (T2 Self)] + [_constr_T3_i1 : (T1 Self)] f3 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.Tp1 (Self : Type) where +class Tp1 (Self : Type) where f1 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.Tp2 (Self : Type) where - [_constr_i0 : (Lean_tests.Traits.Inheritance.Tp1 Self)] - [_constr_i1 : (Lean_tests.Traits.Inheritance.T3 Self)] +class Tp2 (Self : Type) where + [_constr_Tp2_i0 : (Tp1 Self)] + [_constr_Tp2_i1 : (T3 Self)] fp2 : (Self -> RustM usize) -structure Lean_tests.Traits.Inheritance.S where +structure S where + -- no fields +instance Impl : T1 S where + f1 (self : S) := do (pure (1 : usize)) -instance Lean_tests.Traits.Inheritance.Impl : - Lean_tests.Traits.Inheritance.T1 Lean_tests.Traits.Inheritance.S - where - f1 (self : Lean_tests.Traits.Inheritance.S) := do (pure (1 : usize)) +instance Impl_1 : T2 S where + f2 (self : S) := do (pure (2 : usize)) -instance Lean_tests.Traits.Inheritance.Impl_1 : - Lean_tests.Traits.Inheritance.T2 Lean_tests.Traits.Inheritance.S - where - f2 (self : Lean_tests.Traits.Inheritance.S) := do (pure (2 : usize)) +instance Impl_2 : T3 S where + f3 (self : S) := do (pure (3 : usize)) -instance Lean_tests.Traits.Inheritance.Impl_2 : - Lean_tests.Traits.Inheritance.T3 Lean_tests.Traits.Inheritance.S - where - f3 (self : Lean_tests.Traits.Inheritance.S) := do (pure (3 : usize)) +instance Impl_3 : Tp1 S where + f1 (self : S) := do (pure (10 : usize)) -instance Lean_tests.Traits.Inheritance.Impl_3 : - Lean_tests.Traits.Inheritance.Tp1 Lean_tests.Traits.Inheritance.S - where - f1 (self : Lean_tests.Traits.Inheritance.S) := do (pure (10 : usize)) +instance Impl_4 : Tp2 S where + fp2 (self : S) := do + ((← ((← ((← (Tp1.f1 self)) +? (← (T1.f1 self)))) +? (← (T2.f2 self)))) + +? (← (T3.f3 self))) -instance Lean_tests.Traits.Inheritance.Impl_4 : - Lean_tests.Traits.Inheritance.Tp2 Lean_tests.Traits.Inheritance.S - where - fp2 (self : Lean_tests.Traits.Inheritance.S) := do - ((← ((← ((← (Lean_tests.Traits.Inheritance.Tp1.f1 self)) - +? (← (Lean_tests.Traits.Inheritance.T1.f1 self)))) - +? (← (Lean_tests.Traits.Inheritance.T2.f2 self)))) - +? (← (Lean_tests.Traits.Inheritance.T3.f3 self))) +def test (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do + let s : S := S.mk; + ((← (T3.f3 s)) +? (1 : usize)) -def Lean_tests.Traits.Inheritance.test +end Lean_tests.Traits.Inheritance + + +namespace Lean_tests.Reject_do_dsl + +def rejected (_ : Rust_primitives.Hax.Tuple0) - : RustM usize + : RustM Rust_primitives.Hax.Tuple0 := do - let s : Lean_tests.Traits.Inheritance.S := Lean_tests.Traits.Inheritance.S.mk; - ((← (Lean_tests.Traits.Inheritance.T3.f3 s)) +? (1 : usize)) + let x1 : i32 ← ((1 : i32) +? sorry); + let x2 : i32 ← ((1 : i32) +? sorry); + let x : i32 := (9 : i32); + let x3 : i32 ← ((1 : i32) +? (← (x +? (1 : i32)))); + (pure Rust_primitives.Hax.Tuple0.mk) -class Lean_tests.Traits.Bounds.T1 (Self : Type) where - f1 : (Self -> RustM usize) +-- Code that should be produced from the rejected code +def accepted + (_ : Rust_primitives.Hax.Tuple0) + : RustM Rust_primitives.Hax.Tuple0 + := do + let x1_tmp : i32 ← if true then (pure (0 : i32)) else (pure (1 : i32)); + let x1 : i32 ← ((1 : i32) +? x1_tmp); + let x2_tmp : i32 ← + match (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32)) with + | _ => (pure (0 : i32)); + let x2 : i32 ← ((1 : i32) +? x2_tmp); + let x3_tmp_x : i32 := (9 : i32); + let x3_tmp : i32 ← (x3_tmp_x +? (1 : i32)); + let x3 : i32 ← ((1 : i32) +? x3_tmp); + (pure Rust_primitives.Hax.Tuple0.mk) -class Lean_tests.Traits.Bounds.T2 (Self : Type) where - f2 : (Self -> RustM usize) +def test + (_ : Rust_primitives.Hax.Tuple0) + : RustM + (Rust_primitives.Hax.Tuple2 + Rust_primitives.Hax.Tuple0 + Rust_primitives.Hax.Tuple0) + := do + let x1 : i32 ← + if true then + let y : i32 ← + if false then + let z : i32 ← + match Rust_primitives.Hax.Tuple0.mk with | _ => (pure (9 : i32)); + let z : i32 ← ((1 : i32) +? z); + (z +? (1 : i32)) + else + let z : i32 := (9 : i32); + let z : i32 ← (z +? (1 : i32)); + (pure z); + let y : i32 ← (y +? (1 : i32)); + (y +? (1 : i32)) + else + (pure (0 : i32)); + let x1 : i32 ← (x1 +? (1 : i32)); + let x2 : i32 ← + match (Core.Option.Option.Some (89 : i32)) with + | (Core.Option.Option.Some a) + => + let y : i32 ← ((1 : i32) +? a); + let y : i32 ← (y +? (1 : i32)); + if (← (Rust_primitives.Hax.Machine_int.eq y (0 : i32))) then + let z : i32 := (9 : i32); + let z : i32 ← ((← (z +? y)) +? (1 : i32)); + (pure z) + else + (pure (10 : i32)) + | (Core.Option.Option.None ) + => + let y : i32 ← + if false then + (pure (9 : i32)) + else + let z : i32 := (9 : i32); + let z : i32 ← (z +? (1 : i32)); + (z +? (9 : i32)); + let y : i32 ← (y +? (1 : i32)); + (pure y); + (pure (Rust_primitives.Hax.Tuple2.mk + Rust_primitives.Hax.Tuple0.mk Rust_primitives.Hax.Tuple0.mk)) -class Lean_tests.Traits.Bounds.Test (Self : Type) (T : Type) where - [_constr_i0 : (Lean_tests.Traits.Bounds.T2 Self)] - [_constr_i1 : (Lean_tests.Traits.Bounds.T1 T)] - f_test : (Self -> T -> RustM usize) +end Lean_tests.Reject_do_dsl -structure Lean_tests.Traits.Bounds.S1 where +namespace Lean_tests.Traits.Associated_types -instance Lean_tests.Traits.Bounds.Impl : - Lean_tests.Traits.Bounds.T1 Lean_tests.Traits.Bounds.S1 - where - f1 (self : Lean_tests.Traits.Bounds.S1) := do (pure (0 : usize)) +class Foo (Self : Type) (T : Type) where -structure Lean_tests.Traits.Bounds.S2 where +class Bar (Self : Type) where -instance Lean_tests.Traits.Bounds.Impl_1 : - Lean_tests.Traits.Bounds.T2 Lean_tests.Traits.Bounds.S2 - where - f2 (self : Lean_tests.Traits.Bounds.S2) := do (pure (1 : usize)) -instance Lean_tests.Traits.Bounds.Impl_2 : - Lean_tests.Traits.Bounds.Test - Lean_tests.Traits.Bounds.S2 - Lean_tests.Traits.Bounds.S1 - where - f_test (self : Lean_tests.Traits.Bounds.S2) - (x : Lean_tests.Traits.Bounds.S1) - := do - ((← ((← (Lean_tests.Traits.Bounds.T1.f1 x)) - +? (← (Lean_tests.Traits.Bounds.T2.f2 self)))) - +? (1 : usize)) +structure S where + -- no fields -def Lean_tests.Traits.Bounds.test - (x1 : Lean_tests.Traits.Bounds.S1) - (x2 : Lean_tests.Traits.Bounds.S2) - : RustM usize - := do - ((← (Lean_tests.Traits.Bounds.Test.f_test x2 x1)) - +? (← (Lean_tests.Traits.Bounds.T1.f1 x1))) +instance Impl_2 : Bar i16 where + -- no fields -class Lean_tests.Traits.Basic.T1 (Self : Type) where - f1 : (Self -> RustM usize) - f2 : (Self -> Self -> RustM usize) +instance Impl_3 (A : Type) : Foo (Rust_primitives.Hax.Tuple2 u32 A) i16 where + -- no fields -structure Lean_tests.Traits.Basic.S where +class T1 (Self : Type) where + T : Type + f : (Self -> T -> RustM T) +class T3 (Self : Type) where + T : Type + [_constr_T_i0 : (Bar T)] + Tp : Type + [_constr_Tp_i0 : (Foo Tp T)] + f (A : Type) [(Bar A)] : (Self -> T -> Tp -> RustM usize) -instance Lean_tests.Traits.Basic.Impl : - Lean_tests.Traits.Basic.T1 Lean_tests.Traits.Basic.S - where - f1 (self : Lean_tests.Traits.Basic.S) := do (pure (42 : usize)) - f2 (self : Lean_tests.Traits.Basic.S) - (other : Lean_tests.Traits.Basic.S) - := do - (pure (43 : usize)) +instance Impl : T1 S where + T := i32 + f (self : S) (x : i32) := do (pure (2121 : i32)) -def Lean_tests.Traits.Basic.f - (T : Type) [(Lean_tests.Traits.Basic.T1 T)] (x : T) - : RustM usize - := do - ((← (Lean_tests.Traits.Basic.T1.f1 x)) - +? (← (Lean_tests.Traits.Basic.T1.f2 x x))) +class T2 (Self : Type) where + T : Type + [_constr_T_i0 : (T1 T)] + f : (Self -> T -> RustM usize) -class Lean_tests.Traits.Associated_types.Foo (Self : Type) (T : Type) where +instance Impl_1 : T2 S where + T := S + f (self : S) (x : S) := do (pure (21 : usize)) +end Lean_tests.Traits.Associated_types -class Lean_tests.Traits.Associated_types.Bar (Self : Type) where +namespace Lean_tests.Traits.Bounds -structure Lean_tests.Traits.Associated_types.S where +class T1 (Self : Type) where + f1 : (Self -> RustM usize) +class T2 (Self : Type) where + f2 : (Self -> RustM usize) -instance Lean_tests.Traits.Associated_types.Impl_2 : - Lean_tests.Traits.Associated_types.Bar i16 - where +class Test (Self : Type) (T : Type) where + [_constr_Test_i0 : (T2 Self)] + [_constr_Test_i1 : (T1 T)] + f_test : (Self -> T -> RustM usize) +structure S1 where + -- no fields -instance Lean_tests.Traits.Associated_types.Impl_3 (A : Type) : - Lean_tests.Traits.Associated_types.Foo (Rust_primitives.Hax.Tuple2 u32 A) i16 - where +instance Impl : T1 S1 where + f1 (self : S1) := do (pure (0 : usize)) +structure S2 where + -- no fields -class Lean_tests.Traits.Associated_types.T1 (Self : Type) where - T : Type - f : (Self -> T -> RustM T) +instance Impl_1 : T2 S2 where + f2 (self : S2) := do (pure (1 : usize)) -class Lean_tests.Traits.Associated_types.T3 (Self : Type) where - T : Type - [_constr_i0 : (Lean_tests.Traits.Associated_types.Bar T)] - Tp : Type - [_constr_i0 : (Lean_tests.Traits.Associated_types.Foo Tp T)] - f (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] : - (Self -> T -> Tp -> RustM usize) +instance Impl_2 : Test S2 S1 where + f_test (self : S2) (x : S1) := do + ((← ((← (T1.f1 x)) +? (← (T2.f2 self)))) +? (1 : usize)) -instance Lean_tests.Traits.Associated_types.Impl : - Lean_tests.Traits.Associated_types.T1 Lean_tests.Traits.Associated_types.S - where - T := i32 - f (self : Lean_tests.Traits.Associated_types.S) (x : i32) := do - (pure (2121 : i32)) +def test (x1 : S1) (x2 : S2) : RustM usize := do + ((← (Test.f_test x2 x1)) +? (← (T1.f1 x1))) -class Lean_tests.Traits.Associated_types.T2 (Self : Type) where - T : Type - [_constr_i0 : (Lean_tests.Traits.Associated_types.T1 T)] - f : (Self -> T -> RustM usize) +end Lean_tests.Traits.Bounds + + +namespace Lean_tests.Enums + +inductive E : Type +| V1 : E +| V2 : E +| V3 : usize -> E +| V4 : usize -> usize -> usize -> E +| V5 (f1 : usize) (f2 : usize) : E +| V6 (f1 : usize) (f2 : usize) : E + +inductive MyList (T : Type) : Type +| Nil : MyList (T : Type) +| Cons (hd : T) (tl : (Alloc.Boxed.Box (MyList T) Alloc.Alloc.Global)) : MyList + (T : Type) + +def enums + (_ : Rust_primitives.Hax.Tuple0) + : RustM Rust_primitives.Hax.Tuple0 + := do + let e_v1 : E := E.V1; + let e_v2 : E := E.V2; + let e_v3 : E := (E.V3 (23 : usize)); + let e_v4 : E := (E.V4 (23 : usize) (12 : usize) (1 : usize)); + let e_v5 : E := (E.V5 (f1 := (23 : usize)) (f2 := (43 : usize))); + let e_v6 : E := (E.V6 (f1 := (12 : usize)) (f2 := (13 : usize))); + let nil : (MyList usize) := MyList.Nil; + let cons_1 : (MyList usize) := (MyList.Cons (hd := (1 : usize)) (tl := nil)); + let cons_2_1 : (MyList usize) := + (MyList.Cons (hd := (2 : usize)) (tl := cons_1)); + match e_v1 with + | (E.V1 ) => (pure Rust_primitives.Hax.Tuple0.mk) + | (E.V2 ) => (pure Rust_primitives.Hax.Tuple0.mk) + | (E.V3 _) => (pure Rust_primitives.Hax.Tuple0.mk) + | (E.V4 x1 x2 x3) + => + let y1 : usize ← (x1 +? x2); + let y2 : usize ← (y1 -? x2); + let y3 : usize ← (y2 +? x3); + (pure Rust_primitives.Hax.Tuple0.mk) + | (E.V5 (f1 := f1) (f2 := f2)) => (pure Rust_primitives.Hax.Tuple0.mk) + | (E.V6 (f1 := f1) (f2 := other_name_for_f2)) + => (pure Rust_primitives.Hax.Tuple0.mk) -instance Lean_tests.Traits.Associated_types.Impl_1 : - Lean_tests.Traits.Associated_types.T2 Lean_tests.Traits.Associated_types.S - where - T := Lean_tests.Traits.Associated_types.S - f (self : Lean_tests.Traits.Associated_types.S) - (x : Lean_tests.Traits.Associated_types.S) - := do - (pure (21 : usize)) +end Lean_tests.Enums -structure Lean_tests.Structs.Miscellaneous.S where + +namespace Lean_tests.Structs.Miscellaneous + +structure S where f : i32 -def Lean_tests.Structs.Miscellaneous.test_tuples +def test_tuples (_ : Rust_primitives.Hax.Tuple0) : RustM (Rust_primitives.Hax.Tuple2 i32 i32) := do let lit : i32 := (1 : i32); - let constr : Lean_tests.Structs.Miscellaneous.S := - (Lean_tests.Structs.Miscellaneous.S.mk (f := (42 : i32))); - let proj : i32 := (Lean_tests.Structs.Miscellaneous.S.f constr); + let constr : S := (S.mk (f := (42 : i32))); + let proj : i32 := (S.f constr); let ite : (Rust_primitives.Hax.Tuple2 i32 i32) ← if true then (pure (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32))) @@ -323,92 +407,154 @@ def Lean_tests.Structs.Miscellaneous.test_tuples (pure (Rust_primitives.Hax.Tuple2.mk z z)); (pure (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32))) -structure Lean_tests.Structs.Base_expressions.S where - f1 : u32 - f2 : u32 - f3 : u32 +end Lean_tests.Structs.Miscellaneous -def Lean_tests.Structs.Base_expressions.test - (_ : Rust_primitives.Hax.Tuple0) - : RustM Rust_primitives.Hax.Tuple0 - := do - let s1 : Lean_tests.Structs.Base_expressions.S := - (Lean_tests.Structs.Base_expressions.S.mk - (f1 := (1 : u32)) (f2 := (2 : u32)) (f3 := (3 : u32))); - let _ := {s1 with f1 := (0 : u32)}; - let _ := {s1 with f2 := (0 : u32)}; - let _ := {s1 with f3 := (0 : u32)}; - let _ := {s1 with f1 := (0 : u32), f2 := (1 : u32)}; - let _ := {s1 with f2 := (0 : u32), f3 := (1 : u32)}; - let _ := {s1 with f3 := (0 : u32), f1 := (2 : u32)}; - let _ := {s1 with f1 := (0 : u32), f2 := (1 : u32), f3 := (0 : u32)}; - (pure Rust_primitives.Hax.Tuple0.mk) -structure Lean_tests.Structs.T0 where +namespace Lean_tests.Loops +def loop1 (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do + let x : u32 := (0 : u32); + let x : u32 ← + (Rust_primitives.Hax.Folds.fold_range + (1 : u32) + (10 : u32) + (fun x _ => (do (pure true) : RustM Bool)) + x + (fun x i => (do (x +? i) : RustM u32))); + (pure x) -structure Lean_tests.Structs.T1 (A : Type) where +def loop2 (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do + let x : u32 := (0 : u32); + match + (← (Rust_primitives.Hax.Folds.fold_range_return + (1 : u32) + (10 : u32) + (fun x _ => (do (pure true) : RustM Bool)) + x + (fun x i => (do + if (← (Rust_primitives.Hax.Machine_int.eq i (5 : u32))) then + (pure (Core.Ops.Control_flow.ControlFlow.Break + (Core.Ops.Control_flow.ControlFlow.Break x))) + else + (pure (Core.Ops.Control_flow.ControlFlow.Continue (← (x +? i)))) : + RustM + (Core.Ops.Control_flow.ControlFlow + (Core.Ops.Control_flow.ControlFlow + u32 + (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32)) + u32))))) + with + | (Core.Ops.Control_flow.ControlFlow.Break ret) => (pure ret) + | (Core.Ops.Control_flow.ControlFlow.Continue x) => (pure x) + +end Lean_tests.Loops + + +namespace Lean_tests.Traits.Default + +class Easy (Self : Type) where + dft (self : Self) : RustM usize := do (pure (32 : usize)) + +instance Impl : Easy usize where + dft (self : usize) := do (self +? (1 : usize)) + +instance Impl_1 : Easy u32 where + -- no fields + +class T1 (Self : Type) where + f1 : (Self -> RustM usize) + f2 (self : Self) : RustM usize := do (pure (1 : usize)) + f3 (A : Type) (self : Self) (x : A) : RustM usize := do (pure (1 : usize)) + f4 (A : Type) [(Easy A)] (self : Self) (x : A) : RustM usize := do + ((← (Easy.dft x)) +? (1 : usize)) + +structure S (A : Type) where + _0 : usize + _1 : A + +instance Impl_2 : T1 (S usize) where + f1 (self : (S usize)) := do ((S._0 self) +? (S._1 self)) + f2 (self : (S usize)) := do (pure (S._1 self)) + +instance Impl_3 : T1 (S Bool) where + f1 (self : (S Bool)) := do + if (S._1 self) then (pure (S._0 self)) else (pure (9 : usize)) + f2 (self : (S Bool)) := do ((S._0 self) +? (1 : usize)) + +instance Impl_4 : T1 (S Alloc.String.String) where + f1 (self : (S Alloc.String.String)) := do (pure (0 : usize)) + +end Lean_tests.Traits.Default + + +namespace Lean_tests.Traits.Basic + +class T1 (Self : Type) where + f1 : (Self -> RustM usize) + f2 : (Self -> Self -> RustM usize) + +structure S where + -- no fields + +instance Impl : T1 S where + f1 (self : S) := do (pure (42 : usize)) + f2 (self : S) (other : S) := do (pure (43 : usize)) + +def f (T : Type) [(T1 T)] (x : T) : RustM usize := do + ((← (T1.f1 x)) +? (← (T1.f2 x x))) + +end Lean_tests.Traits.Basic + + +namespace Lean_tests.Structs + +structure T0 where + -- no fields + +structure T1 (A : Type) where _0 : A -structure Lean_tests.Structs.T2 (A : Type) (B : Type) where +structure T2 (A : Type) (B : Type) where _0 : A _1 : B -structure Lean_tests.Structs.T3 (A : Type) (B : Type) (C : Type) where +structure T3 (A : Type) (B : Type) (C : Type) where _0 : A _1 : B _2 : C -structure Lean_tests.Structs.T3p (A : Type) (B : Type) (C : Type) where +structure T3p (A : Type) (B : Type) (C : Type) where _0 : A - _1 : (Lean_tests.Structs.T2 B C) + _1 : (T2 B C) -def Lean_tests.Structs.tuple_structs +def tuple_structs (_ : Rust_primitives.Hax.Tuple0) : RustM Rust_primitives.Hax.Tuple0 := do - let t0 : Lean_tests.Structs.T0 := Lean_tests.Structs.T0.mk; - let t1 : (Lean_tests.Structs.T1 i32) := (Lean_tests.Structs.T1.mk (1 : i32)); - let t2 : (Lean_tests.Structs.T2 i32 i32) := - (Lean_tests.Structs.T2.mk (1 : i32) (2 : i32)); - let - t3 : (Lean_tests.Structs.T3 - Lean_tests.Structs.T0 - (Lean_tests.Structs.T1 i32) - (Lean_tests.Structs.T2 i32 i32)) := - (Lean_tests.Structs.T3.mk - Lean_tests.Structs.T0.mk - (Lean_tests.Structs.T1.mk (1 : i32)) - (Lean_tests.Structs.T2.mk (1 : i32) (2 : i32))); - let - t3p : (Lean_tests.Structs.T3p - Lean_tests.Structs.T0 - (Lean_tests.Structs.T1 i32) - (Lean_tests.Structs.T2 i32 i32)) := - (Lean_tests.Structs.T3p.mk - Lean_tests.Structs.T0.mk - (Lean_tests.Structs.T2.mk - (Lean_tests.Structs.T1.mk (1 : i32)) - (Lean_tests.Structs.T2.mk (1 : i32) (2 : i32)))); + let t0 : T0 := T0.mk; + let t1 : (T1 i32) := (T1.mk (1 : i32)); + let t2 : (T2 i32 i32) := (T2.mk (1 : i32) (2 : i32)); + let t3 : (T3 T0 (T1 i32) (T2 i32 i32)) := + (T3.mk T0.mk (T1.mk (1 : i32)) (T2.mk (1 : i32) (2 : i32))); + let t3p : (T3p T0 (T1 i32) (T2 i32 i32)) := + (T3p.mk T0.mk (T2.mk (T1.mk (1 : i32)) (T2.mk (1 : i32) (2 : i32)))); let ⟨⟩ := t0; let ⟨u1⟩ := t1; let ⟨u2, u3⟩ := t2; let ⟨⟨⟩, ⟨_⟩, ⟨_, _⟩⟩ := t3; let ⟨⟨⟩, ⟨⟨_⟩, ⟨_, _⟩⟩⟩ := t3p; - let _ := (Lean_tests.Structs.T1._0 t1); - let _ := (Lean_tests.Structs.T2._0 t2); - let _ := (Lean_tests.Structs.T2._1 t2); - let _ := (Lean_tests.Structs.T3._0 t3); - let _ := (Lean_tests.Structs.T3._1 t3); - let _ := (Lean_tests.Structs.T3._2 t3); - let _ := (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3._2 t3)); - let _ := (Lean_tests.Structs.T3p._0 t3p); - let _ := (Lean_tests.Structs.T3p._1 t3p); - let _ := - (Lean_tests.Structs.T2._0 - (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p))); - let _ := (Lean_tests.Structs.T2._0 (Lean_tests.Structs.T3p._1 t3p)); - let _ := (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p)); + let _ := (T1._0 t1); + let _ := (T2._0 t2); + let _ := (T2._1 t2); + let _ := (T3._0 t3); + let _ := (T3._1 t3); + let _ := (T3._2 t3); + let _ := (T2._1 (T3._2 t3)); + let _ := (T3p._0 t3p); + let _ := (T3p._1 t3p); + let _ := (T2._0 (T2._1 (T3p._1 t3p))); + let _ := (T2._0 (T3p._1 t3p)); + let _ := (T2._1 (T3p._1 t3p)); let _ ← match t0 with | ⟨⟩ => (pure Rust_primitives.Hax.Tuple0.mk); let _ ← match t1 with | ⟨u1⟩ => (pure Rust_primitives.Hax.Tuple0.mk); let _ ← match t2 with | ⟨u2, u3⟩ => (pure Rust_primitives.Hax.Tuple0.mk); @@ -420,33 +566,32 @@ def Lean_tests.Structs.tuple_structs | ⟨⟨⟩, ⟨⟨u1⟩, ⟨u2, u3⟩⟩⟩ => (pure Rust_primitives.Hax.Tuple0.mk); (pure Rust_primitives.Hax.Tuple0.mk) -structure Lean_tests.Structs.S1 where +structure S1 where f1 : usize f2 : usize -structure Lean_tests.Structs.S2 where - f1 : Lean_tests.Structs.S1 +structure S2 where + f1 : S1 f2 : usize -structure Lean_tests.Structs.S3 where +structure S3 where _end : usize _def : usize _theorem : usize _structure : usize _inductive : usize -def Lean_tests.Structs.normal_structs +def normal_structs (_ : Rust_primitives.Hax.Tuple0) : RustM Rust_primitives.Hax.Tuple0 := do - let s1 : Lean_tests.Structs.S1 := - (Lean_tests.Structs.S1.mk (f1 := (0 : usize)) (f2 := (1 : usize))); - let s2 : Lean_tests.Structs.S2 := - (Lean_tests.Structs.S2.mk - (f1 := (Lean_tests.Structs.S1.mk (f1 := (2 : usize)) (f2 := (3 : usize)))) + let s1 : S1 := (S1.mk (f1 := (0 : usize)) (f2 := (1 : usize))); + let s2 : S2 := + (S2.mk + (f1 := (S1.mk (f1 := (2 : usize)) (f2 := (3 : usize)))) (f2 := (4 : usize))); - let s3 : Lean_tests.Structs.S3 := - (Lean_tests.Structs.S3.mk + let s3 : S3 := + (S3.mk (_end := (0 : usize)) (_def := (0 : usize)) (_theorem := (0 : usize)) @@ -462,19 +607,17 @@ def Lean_tests.Structs.normal_structs _structure := _structure, _inductive := _inductive} := s3; - let _ := - (Rust_primitives.Hax.Tuple2.mk - (Lean_tests.Structs.S1.f1 s1) (Lean_tests.Structs.S1.f2 s1)); + let _ := (Rust_primitives.Hax.Tuple2.mk (S1.f1 s1) (S1.f2 s1)); let _ := (Rust_primitives.Hax.Tuple8.mk - (Lean_tests.Structs.S1.f1 s1) - (Lean_tests.Structs.S1.f2 s1) - (Lean_tests.Structs.S1.f1 (Lean_tests.Structs.S2.f1 s2)) - (Lean_tests.Structs.S1.f2 (Lean_tests.Structs.S2.f1 s2)) - (Lean_tests.Structs.S2.f2 s2) - (Lean_tests.Structs.S3._end s3) - (Lean_tests.Structs.S3._def s3) - (Lean_tests.Structs.S3._theorem s3)); + (S1.f1 s1) + (S1.f2 s1) + (S1.f1 (S2.f1 s2)) + (S1.f2 (S2.f1 s2)) + (S2.f2 s2) + (S3._end s3) + (S3._def s3) + (S3._theorem s3)); let _ ← match s1 with | {f1 := f1, f2 := f2} => (pure Rust_primitives.Hax.Tuple0.mk); @@ -490,52 +633,103 @@ def Lean_tests.Structs.normal_structs _inductive := _inductive} => (pure Rust_primitives.Hax.Tuple0.mk) -structure Lean_tests.Monadic.S where - f : u32 +end Lean_tests.Structs + + +namespace Lean_tests.Constants + +def C1 : u32 := RustM.of_isOk (do (pure (5678 : u32))) (by rfl) + +def C2 : u32 := RustM.of_isOk (do (C1 +? (1 : u32))) (by rfl) + +def C3 : u32 := + RustM.of_isOk + (do if true then (pure (890 : u32)) else ((9 : u32) /? (0 : u32))) + (by rfl) -def Lean_tests.Monadic.test +def computation (x : u32) : RustM u32 := do ((← (x +? x)) +? (1 : u32)) + +def C4 : u32 := RustM.of_isOk (do ((← (computation C1)) +? C2)) (by rfl) + +def test (_ : Rust_primitives.Hax.Tuple0) : RustM Rust_primitives.Hax.Tuple0 := do - let _ := (9 : i32); - let _ ← ((9 : i32) +? (9 : i32)); - let _ := (Lean_tests.Monadic.S.mk (f := (9 : u32))); - let _ := (Lean_tests.Monadic.S.mk (f := (← ((9 : u32) +? (9 : u32))))); - let _ := - (Lean_tests.Monadic.S.f - (Lean_tests.Monadic.S.mk (f := (← ((9 : u32) +? (9 : u32)))))); - let _ ← - ((Lean_tests.Monadic.S.f - (Lean_tests.Monadic.S.mk (f := (← ((9 : u32) +? (9 : u32)))))) - +? (9 : u32)); - let _ ← if true then ((3 : i32) +? (4 : i32)) else ((3 : i32) -? (4 : i32)); - let _ ← - if - (← (Rust_primitives.Hax.Machine_int.eq - (← ((9 : i32) +? (9 : i32))) - (0 : i32))) then - ((3 : i32) +? (4 : i32)) - else - ((3 : i32) -? (4 : i32)); - let _ ← - if true then - let x : i32 := (9 : i32); - let _ ← ((3 : i32) +? x); - (pure Rust_primitives.Hax.Tuple0.mk) - else - let y : i32 := (19 : i32); - let _ ← ((← ((3 : i32) +? y)) -? (4 : i32)); - (pure Rust_primitives.Hax.Tuple0.mk); + let x : u32 ← (C1 +? (1 : u32)); + let y : u32 ← (C2 +? C3); + let z : u32 ← (C4 -? C3); (pure Rust_primitives.Hax.Tuple0.mk) -inductive Lean_tests.Loops.Errors.Error : Type -| Foo : Lean_tests.Loops.Errors.Error -| Bar : u32 -> Lean_tests.Loops.Errors.Error +end Lean_tests.Constants + + +namespace Lean_tests + +def FORTYTWO : usize := RustM.of_isOk (do (pure (42 : usize))) (by rfl) + +def MINUS_FORTYTWO : isize := RustM.of_isOk (do (pure (-42 : isize))) (by rfl) + +def returns42 (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do + (pure FORTYTWO) + +def add_two_numbers (x : usize) (y : usize) : RustM usize := do (x +? y) + +def letBinding (x : usize) (y : usize) : RustM usize := do + let useless : Rust_primitives.Hax.Tuple0 := Rust_primitives.Hax.Tuple0.mk; + let result1 : usize ← (x +? y); + let result2 : usize ← (result1 +? (2 : usize)); + (result2 +? (1 : usize)) + +def closure (_ : Rust_primitives.Hax.Tuple0) : RustM i32 := do + let x : i32 := (41 : i32); + let f1 : (i32 -> RustM i32) := (fun y => (do (y +? x) : RustM i32)); + let f2 : (i32 -> i32 -> RustM i32) := + (fun y z => (do ((← (y +? x)) +? z) : RustM i32)); + let res1 : i32 ← + (Core.Ops.Function.Fn.call f1 (Rust_primitives.Hax.Tuple1.mk (1 : i32))); + let res2 : i32 ← + (Core.Ops.Function.Fn.call + f2 + (Rust_primitives.Hax.Tuple2.mk (2 : i32) (3 : i32))); + (res1 +? res2) +def _ : Rust_primitives.Hax.Tuple0 := + RustM.of_isOk (do (pure Rust_primitives.Hax.Tuple0.mk)) (by rfl) -def Lean_tests.Loops.Errors.loop3 +@[spec] + +def test_before_verbatime_single_line (x : u8) : RustM u8 := do (pure (42 : u8)) + +def __1 : Rust_primitives.Hax.Tuple0 := + RustM.of_isOk (do (pure Rust_primitives.Hax.Tuple0.mk)) (by rfl) + + +def multiline : Unit := () + + +def test_before_verbatim_multi_line (x : u8) : RustM u8 := do (pure (32 : u8)) + +def binop_resugarings (x : u32) : RustM u32 := do + let add : u32 ← (x +? (1 : u32)); + let sub : u32 ← (add -? (2 : u32)); + let mul : u32 ← (sub *? (3 : u32)); + let rem : u32 ← (mul %? (4 : u32)); + let div : u32 ← (rem /? (5 : u32)); + let rshift : u32 ← (div >>>? x); + (pure x) + +end Lean_tests + + +namespace Lean_tests.Loops.Errors + +inductive Error : Type +| Foo : Error +| Bar : u32 -> Error + +def loop3 (_ : Rust_primitives.Hax.Tuple0) - : RustM (Core.Result.Result u32 Lean_tests.Loops.Errors.Error) + : RustM (Core.Result.Result u32 Error) := do let x : u32 := (0 : u32); let _end : u32 := (10 : u32); @@ -549,13 +743,13 @@ def Lean_tests.Loops.Errors.loop3 if (← (Rust_primitives.Hax.Machine_int.eq i (5 : u32))) then (pure (Core.Ops.Control_flow.ControlFlow.Break (Core.Ops.Control_flow.ControlFlow.Break - (Core.Result.Result.Err Lean_tests.Loops.Errors.Error.Foo)))) + (Core.Result.Result.Err Error.Foo)))) else (pure (Core.Ops.Control_flow.ControlFlow.Continue (← (x +? (5 : u32))))) : RustM (Core.Ops.Control_flow.ControlFlow (Core.Ops.Control_flow.ControlFlow - (Core.Result.Result u32 Lean_tests.Loops.Errors.Error) + (Core.Result.Result u32 Error) (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32)) u32))))) with @@ -563,12 +757,9 @@ def Lean_tests.Loops.Errors.loop3 | (Core.Ops.Control_flow.ControlFlow.Continue x) => (pure (Core.Result.Result.Ok x)) -def Lean_tests.Loops.Errors.loop4 +def loop4 (_ : Rust_primitives.Hax.Tuple0) - : RustM - (Core.Result.Result - (Rust_primitives.Hax.Tuple2 u32 u32) - Lean_tests.Loops.Errors.Error) + : RustM (Core.Result.Result (Rust_primitives.Hax.Tuple2 u32 u32) Error) := do let e : u32 := (0 : u32); let f : (Rust_primitives.Hax.Tuple0 -> RustM u32) := @@ -585,15 +776,13 @@ def Lean_tests.Loops.Errors.loop4 if (← (Rust_primitives.Hax.Machine_int.gt i (10 : u32))) then (pure (Core.Ops.Control_flow.ControlFlow.Break (Core.Ops.Control_flow.ControlFlow.Break - (Core.Result.Result.Err (Lean_tests.Loops.Errors.Error.Bar e))))) + (Core.Result.Result.Err (Error.Bar e))))) else (pure (Core.Ops.Control_flow.ControlFlow.Continue (← (e +? i)))) : RustM (Core.Ops.Control_flow.ControlFlow (Core.Ops.Control_flow.ControlFlow - (Core.Result.Result - (Rust_primitives.Hax.Tuple2 u32 u32) - Lean_tests.Loops.Errors.Error) + (Core.Result.Result (Rust_primitives.Hax.Tuple2 u32 u32) Error) (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32)) u32))))) with @@ -601,253 +790,81 @@ def Lean_tests.Loops.Errors.loop4 | (Core.Ops.Control_flow.ControlFlow.Continue e) => (pure (Core.Result.Result.Ok (Rust_primitives.Hax.Tuple2.mk e e))) -inductive Lean_tests.Enums.E : Type -| V1 : Lean_tests.Enums.E -| V2 : Lean_tests.Enums.E -| V3 : usize -> Lean_tests.Enums.E -| V4 : usize -> usize -> usize -> Lean_tests.Enums.E -| V5 (f1 : usize) (f2 : usize) : Lean_tests.Enums.E -| V6 (f1 : usize) (f2 : usize) : Lean_tests.Enums.E - - -inductive Lean_tests.Enums.MyList (T : Type) : Type -| Nil : Lean_tests.Enums.MyList (T : Type) -| Cons (hd : T) - (tl : (Alloc.Boxed.Box (Lean_tests.Enums.MyList T) Alloc.Alloc.Global)) - : Lean_tests.Enums.MyList (T : Type) - - -def Lean_tests.Enums.enums - (_ : Rust_primitives.Hax.Tuple0) - : RustM Rust_primitives.Hax.Tuple0 - := do - let e_v1 : Lean_tests.Enums.E := Lean_tests.Enums.E.V1; - let e_v2 : Lean_tests.Enums.E := Lean_tests.Enums.E.V2; - let e_v3 : Lean_tests.Enums.E := (Lean_tests.Enums.E.V3 (23 : usize)); - let e_v4 : Lean_tests.Enums.E := - (Lean_tests.Enums.E.V4 (23 : usize) (12 : usize) (1 : usize)); - let e_v5 : Lean_tests.Enums.E := - (Lean_tests.Enums.E.V5 (f1 := (23 : usize)) (f2 := (43 : usize))); - let e_v6 : Lean_tests.Enums.E := - (Lean_tests.Enums.E.V6 (f1 := (12 : usize)) (f2 := (13 : usize))); - let nil : (Lean_tests.Enums.MyList usize) := Lean_tests.Enums.MyList.Nil; - let cons_1 : (Lean_tests.Enums.MyList usize) := - (Lean_tests.Enums.MyList.Cons (hd := (1 : usize)) (tl := nil)); - let cons_2_1 : (Lean_tests.Enums.MyList usize) := - (Lean_tests.Enums.MyList.Cons (hd := (2 : usize)) (tl := cons_1)); - match e_v1 with - | (Lean_tests.Enums.E.V1 ) => (pure Rust_primitives.Hax.Tuple0.mk) - | (Lean_tests.Enums.E.V2 ) => (pure Rust_primitives.Hax.Tuple0.mk) - | (Lean_tests.Enums.E.V3 _) => (pure Rust_primitives.Hax.Tuple0.mk) - | (Lean_tests.Enums.E.V4 x1 x2 x3) - => - let y1 : usize ← (x1 +? x2); - let y2 : usize ← (y1 -? x2); - let y3 : usize ← (y2 +? x3); - (pure Rust_primitives.Hax.Tuple0.mk) - | (Lean_tests.Enums.E.V5 (f1 := f1) (f2 := f2)) - => (pure Rust_primitives.Hax.Tuple0.mk) - | (Lean_tests.Enums.E.V6 (f1 := f1) (f2 := other_name_for_f2)) - => (pure Rust_primitives.Hax.Tuple0.mk) - -def Lean_tests.Constants.C1 : u32 := - RustM.of_isOk (do (pure (5678 : u32))) (by rfl) - -def Lean_tests.Constants.C2 : u32 := - RustM.of_isOk (do (Lean_tests.Constants.C1 +? (1 : u32))) (by rfl) +end Lean_tests.Loops.Errors -def Lean_tests.Constants.C3 : u32 := - RustM.of_isOk - (do if true then (pure (890 : u32)) else ((9 : u32) /? (0 : u32))) - (by rfl) -def Lean_tests.Constants.computation (x : u32) : RustM u32 := do - ((← (x +? x)) +? (1 : u32)) +namespace Lean_tests.Monadic -def Lean_tests.Constants.C4 : u32 := - RustM.of_isOk - (do - ((← (Lean_tests.Constants.computation Lean_tests.Constants.C1)) - +? Lean_tests.Constants.C2)) - (by rfl) +structure S where + f : u32 -def Lean_tests.Constants.test +def test (_ : Rust_primitives.Hax.Tuple0) : RustM Rust_primitives.Hax.Tuple0 := do - let x : u32 ← (Lean_tests.Constants.C1 +? (1 : u32)); - let y : u32 ← (Lean_tests.Constants.C2 +? Lean_tests.Constants.C3); - let z : u32 ← (Lean_tests.Constants.C4 -? Lean_tests.Constants.C3); + let _ := (9 : i32); + let _ ← ((9 : i32) +? (9 : i32)); + let _ := (S.mk (f := (9 : u32))); + let _ := (S.mk (f := (← ((9 : u32) +? (9 : u32))))); + let _ := (S.f (S.mk (f := (← ((9 : u32) +? (9 : u32)))))); + let _ ← ((S.f (S.mk (f := (← ((9 : u32) +? (9 : u32)))))) +? (9 : u32)); + let _ ← if true then ((3 : i32) +? (4 : i32)) else ((3 : i32) -? (4 : i32)); + let _ ← + if + (← (Rust_primitives.Hax.Machine_int.eq + (← ((9 : i32) +? (9 : i32))) + (0 : i32))) then + ((3 : i32) +? (4 : i32)) + else + ((3 : i32) -? (4 : i32)); + let _ ← + if true then + let x : i32 := (9 : i32); + let _ ← ((3 : i32) +? x); + (pure Rust_primitives.Hax.Tuple0.mk) + else + let y : i32 := (19 : i32); + let _ ← ((← ((3 : i32) +? y)) -? (4 : i32)); + (pure Rust_primitives.Hax.Tuple0.mk); (pure Rust_primitives.Hax.Tuple0.mk) -def Lean_tests.FORTYTWO : usize := - RustM.of_isOk (do (pure (42 : usize))) (by rfl) - -def Lean_tests.MINUS_FORTYTWO : isize := - RustM.of_isOk (do (pure (-42 : isize))) (by rfl) - -def Lean_tests.returns42 (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do - (pure Lean_tests.FORTYTWO) +end Lean_tests.Monadic -def Lean_tests.add_two_numbers (x : usize) (y : usize) : RustM usize := do - (x +? y) -def Lean_tests.letBinding (x : usize) (y : usize) : RustM usize := do - let useless : Rust_primitives.Hax.Tuple0 := Rust_primitives.Hax.Tuple0.mk; - let result1 : usize ← (x +? y); - let result2 : usize ← (result1 +? (2 : usize)); - (result2 +? (1 : usize)) - -def Lean_tests.closure (_ : Rust_primitives.Hax.Tuple0) : RustM i32 := do - let x : i32 := (41 : i32); - let f1 : (i32 -> RustM i32) := (fun y => (do (y +? x) : RustM i32)); - let f2 : (i32 -> i32 -> RustM i32) := - (fun y z => (do ((← (y +? x)) +? z) : RustM i32)); - let res1 : i32 ← - (Core.Ops.Function.Fn.call f1 (Rust_primitives.Hax.Tuple1.mk (1 : i32))); - let res2 : i32 ← - (Core.Ops.Function.Fn.call - f2 - (Rust_primitives.Hax.Tuple2.mk (2 : i32) (3 : i32))); - (res1 +? res2) - -@[spec] - -def Lean_tests.test_before_verbatime_single_line (x : u8) : RustM u8 := do - (pure (42 : u8)) +namespace Lean_tests.Traits.Overlapping_methods +class T1 (Self : Type) where + f : (Self -> RustM usize) -def multiline : Unit := () +class T2 (Self : Type) where + f : (Self -> RustM usize) +class T3 (Self : Type) where + f : (Self -> RustM usize) -def Lean_tests.test_before_verbatim_multi_line (x : u8) : RustM u8 := do - (pure (32 : u8)) +instance Impl : T1 u32 where + f (self : u32) := do (pure (0 : usize)) -def Lean_tests.binop_resugarings (x : u32) : RustM u32 := do - let add : u32 ← (x +? (1 : u32)); - let sub : u32 ← (add -? (2 : u32)); - let mul : u32 ← (sub *? (3 : u32)); - let rem : u32 ← (mul %? (4 : u32)); - let div : u32 ← (rem /? (5 : u32)); - let rshift : u32 ← (div >>>? x); - (pure x) +instance Impl_1 : T2 u32 where + f (self : u32) := do (pure (1 : usize)) -def Lean_tests.Reject_do_dsl.rejected - (_ : Rust_primitives.Hax.Tuple0) - : RustM Rust_primitives.Hax.Tuple0 - := do - let x1 : i32 ← ((1 : i32) +? sorry); - let x2 : i32 ← ((1 : i32) +? sorry); - let x : i32 := (9 : i32); - let x3 : i32 ← ((1 : i32) +? (← (x +? (1 : i32)))); - (pure Rust_primitives.Hax.Tuple0.mk) +instance Impl_2 : T3 u32 where + f (self : u32) := do (pure (2 : usize)) --- Code that should be produced from the rejected code -def Lean_tests.Reject_do_dsl.accepted - (_ : Rust_primitives.Hax.Tuple0) - : RustM Rust_primitives.Hax.Tuple0 - := do - let x1_tmp : i32 ← if true then (pure (0 : i32)) else (pure (1 : i32)); - let x1 : i32 ← ((1 : i32) +? x1_tmp); - let x2_tmp : i32 ← - match (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32)) with - | _ => (pure (0 : i32)); - let x2 : i32 ← ((1 : i32) +? x2_tmp); - let x3_tmp_x : i32 := (9 : i32); - let x3_tmp : i32 ← (x3_tmp_x +? (1 : i32)); - let x3 : i32 ← ((1 : i32) +? x3_tmp); - (pure Rust_primitives.Hax.Tuple0.mk) +def test (_ : Rust_primitives.Hax.Tuple0) : RustM usize := do + let x : u32 := (9 : u32); + ((← ((← (T1.f x)) +? (← (T2.f x)))) +? (← (T3.f x))) -def Lean_tests.Reject_do_dsl.test - (_ : Rust_primitives.Hax.Tuple0) - : RustM - (Rust_primitives.Hax.Tuple2 - Rust_primitives.Hax.Tuple0 - Rust_primitives.Hax.Tuple0) - := do - let x1 : i32 ← - if true then - let y : i32 ← - if false then - let z : i32 ← - match Rust_primitives.Hax.Tuple0.mk with | _ => (pure (9 : i32)); - let z : i32 ← ((1 : i32) +? z); - (z +? (1 : i32)) - else - let z : i32 := (9 : i32); - let z : i32 ← (z +? (1 : i32)); - (pure z); - let y : i32 ← (y +? (1 : i32)); - (y +? (1 : i32)) - else - (pure (0 : i32)); - let x1 : i32 ← (x1 +? (1 : i32)); - let x2 : i32 ← - match (Core.Option.Option.Some (89 : i32)) with - | (Core.Option.Option.Some a) - => - let y : i32 ← ((1 : i32) +? a); - let y : i32 ← (y +? (1 : i32)); - if (← (Rust_primitives.Hax.Machine_int.eq y (0 : i32))) then - let z : i32 := (9 : i32); - let z : i32 ← ((← (z +? y)) +? (1 : i32)); - (pure z) - else - (pure (10 : i32)) - | (Core.Option.Option.None ) - => - let y : i32 ← - if false then - (pure (9 : i32)) - else - let z : i32 := (9 : i32); - let z : i32 ← (z +? (1 : i32)); - (z +? (9 : i32)); - let y : i32 ← (y +? (1 : i32)); - (pure y); - (pure (Rust_primitives.Hax.Tuple2.mk - Rust_primitives.Hax.Tuple0.mk Rust_primitives.Hax.Tuple0.mk)) +end Lean_tests.Traits.Overlapping_methods -def Lean_tests.Loops.loop1 (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do - let x : u32 := (0 : u32); - let x : u32 ← - (Rust_primitives.Hax.Folds.fold_range - (1 : u32) - (10 : u32) - (fun x _ => (do (pure true) : RustM Bool)) - x - (fun x i => (do (x +? i) : RustM u32))); - (pure x) -def Lean_tests.Loops.loop2 (_ : Rust_primitives.Hax.Tuple0) : RustM u32 := do - let x : u32 := (0 : u32); - match - (← (Rust_primitives.Hax.Folds.fold_range_return - (1 : u32) - (10 : u32) - (fun x _ => (do (pure true) : RustM Bool)) - x - (fun x i => (do - if (← (Rust_primitives.Hax.Machine_int.eq i (5 : u32))) then - (pure (Core.Ops.Control_flow.ControlFlow.Break - (Core.Ops.Control_flow.ControlFlow.Break x))) - else - (pure (Core.Ops.Control_flow.ControlFlow.Continue (← (x +? i)))) : - RustM - (Core.Ops.Control_flow.ControlFlow - (Core.Ops.Control_flow.ControlFlow - u32 - (Rust_primitives.Hax.Tuple2 Rust_primitives.Hax.Tuple0 u32)) - u32))))) - with - | (Core.Ops.Control_flow.ControlFlow.Break ret) => (pure ret) - | (Core.Ops.Control_flow.ControlFlow.Continue x) => (pure x) +namespace Lean_tests.Ite -def Lean_tests.Ite.test1 (_ : Rust_primitives.Hax.Tuple0) : RustM i32 := do +def test1 (_ : Rust_primitives.Hax.Tuple0) : RustM i32 := do let x : i32 ← if true then (pure (0 : i32)) else (pure (1 : i32)); if false then (pure (2 : i32)) else (pure (3 : i32)) -def Lean_tests.Ite.test2 (b : Bool) : RustM i32 := do +def test2 (b : Bool) : RustM i32 := do let x : i32 ← if b then (pure (0 : i32)) else (pure (9 : i32)); let y : i32 := (0 : i32); let y : i32 ← @@ -859,25 +876,6 @@ def Lean_tests.Ite.test2 (b : Bool) : RustM i32 := do let z : i32 ← (y -? x); ((← (z +? y)) +? x) --- Single line doc comment -def Lean_tests.Comments.f - (_ : Rust_primitives.Hax.Tuple0) - : RustM Rust_primitives.Hax.Tuple0 - := do - (pure Rust_primitives.Hax.Tuple0.mk) +end Lean_tests.Ite -/-- - Block doc-comment : Lorem ipsum dolor sit amet, consectetur adipiscing elit. Vestibulum rutrum - orci ac tellus ullamcorper sollicitudin. Sed fringilla mi id arcu suscipit rhoncus. Pellentesque et - metus a ante feugiat lobortis. Nam a mauris eget nisl congue egestas. Duis et gravida - nulla. Curabitur mattis leo vel molestie posuere. Etiam malesuada et augue eget - varius. Pellentesque quis tincidunt erat. Vestibulum id consectetur turpis. Cras elementum magna id - urna volutpat fermentum. In vel erat quis nunc rhoncus porta. Aliquam sed pellentesque - tellus. Quisque odio diam, mollis ut venenatis non, scelerisque at nulla. Nunc urna ante, tristique - quis nisi quis, congue maximus nisl. Curabitur non efficitur odio. - -/ -def Lean_tests.Comments.heavily_documented - (_ : Rust_primitives.Hax.Tuple0) - : RustM u32 - := do - (pure (4 : u32))''' +''' diff --git a/tests/Cargo.lock b/tests/Cargo.lock index 8f6b599e2..c65b6a9e3 100644 --- a/tests/Cargo.lock +++ b/tests/Cargo.lock @@ -489,6 +489,13 @@ version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" +[[package]] +name = "lean-core-models" +version = "0.1.0" +dependencies = [ + "hax-lib", +] + [[package]] name = "lean-tests" version = "0.1.0" diff --git a/tests/Cargo.toml b/tests/Cargo.toml index 5becaf7a3..f27ad86de 100644 --- a/tests/Cargo.toml +++ b/tests/Cargo.toml @@ -13,6 +13,7 @@ members = [ "mut-ref-functionalization", "generics", "lean-tests", + "lean-core-models", "loops", "even", "odd", diff --git a/tests/lean-tests/src/traits.rs b/tests/lean-tests/src/traits.rs index a77e78e19..050dbcae7 100644 --- a/tests/lean-tests/src/traits.rs +++ b/tests/lean-tests/src/traits.rs @@ -198,3 +198,63 @@ mod inheritance { s.f3() + 1 } } + +mod default { + + trait Easy { + fn dft(&self) -> usize { + 32 + } + } + + impl Easy for usize { + fn dft(&self) -> usize { + self + 1 + } + } + + impl Easy for u32 {} + + trait T1 { + fn f1(&self) -> usize; + fn f2(&self) -> usize { + 1 + } + fn f3(&self, x: &A) -> usize { + 1 + } + fn f4(&self, x: &A) -> usize { + x.dft() + 1 + } + } + + struct S(usize, A); + + // Override + impl T1 for S { + fn f1(&self) -> usize { + self.0 + self.1 + } + + fn f2(&self) -> usize { + self.1 + } + } + + impl T1 for S { + fn f1(&self) -> usize { + if self.1 { self.0 } else { 9 } + } + + fn f2(&self) -> usize { + self.0 + 1 + } + } + + // No override + impl T1 for S { + fn f1(&self) -> usize { + 0 + } + } +}