diff --git a/CHANGELOG.md b/CHANGELOG.md
index 36c953376..c9aee47ef 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -17,6 +17,9 @@ Changes to the Rust Engine:
- Printers now emit proper diagnostics (PR #1669)
- Global identifiers are now interned (#1689)
- Global identifiers are encapsulated properly, and provide easy destructuring as tuple identifiers (#1693)
+ - Add support for `trait` and `impl` in the Lean backend (#1679): trait definitions, trait bounds
+ on functions, impl definitions. The typeclass resolution in the generated code is left implicit
+ (relies on Lean). Limited support for associated types. No support for default implementations.
Changes to the frontend:
- Add an explicit `Self: Trait` clause to trait methods and consts (#1559)
diff --git a/examples/Cargo.lock b/examples/Cargo.lock
index e17260173..5dfcbc65a 100644
--- a/examples/Cargo.lock
+++ b/examples/Cargo.lock
@@ -252,7 +252,7 @@ checksum = "f93e7192158dbcda357bdec5fb5788eebf8bbac027f3f33e719d29135ae84156"
[[package]]
name = "hax-bounded-integers"
-version = "0.3.2"
+version = "0.3.4"
dependencies = [
"duplicate",
"hax-lib",
@@ -261,7 +261,7 @@ dependencies = [
[[package]]
name = "hax-lib"
-version = "0.3.2"
+version = "0.3.4"
dependencies = [
"hax-lib-macros",
"num-bigint",
@@ -270,7 +270,7 @@ dependencies = [
[[package]]
name = "hax-lib-macros"
-version = "0.3.2"
+version = "0.3.4"
dependencies = [
"hax-lib-macros-types",
"proc-macro-error2",
@@ -281,7 +281,7 @@ dependencies = [
[[package]]
name = "hax-lib-macros-types"
-version = "0.3.2"
+version = "0.3.4"
dependencies = [
"proc-macro2",
"quote",
diff --git a/rust-engine/src/ast.rs b/rust-engine/src/ast.rs
index f60151b3d..fe88b575b 100644
--- a/rust-engine/src/ast.rs
+++ b/rust-engine/src/ast.rs
@@ -1531,7 +1531,7 @@ pub mod traits {
);
derive_has_kind!(
Item => ItemKind, Expr => ExprKind, Pat => PatKind, Guard => GuardKind,
- GenericParam => GenericParamKind, ImplItem => ImplItemKind, TraitItem => TraitItemKind
+ GenericParam => GenericParamKind, ImplItem => ImplItemKind, TraitItem => TraitItemKind, ImplExpr => ImplExprKind
);
impl HasSpan for Attribute {
diff --git a/rust-engine/src/ast/identifiers/global_id.rs b/rust-engine/src/ast/identifiers/global_id.rs
index a85827827..1ddc67aef 100644
--- a/rust-engine/src/ast/identifiers/global_id.rs
+++ b/rust-engine/src/ast/identifiers/global_id.rs
@@ -323,6 +323,18 @@ impl GlobalId {
self.0.get().is_projector()
}
+ /// Returns true if the underlying identifier is a precondition (trait/impl item)
+ /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+ pub fn is_precondition(self) -> bool {
+ self.0.get().is_precondition()
+ }
+
+ /// Returns true if the underlying identifier is a postcondition (trait/impl item)
+ /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+ pub fn is_postcondition(self) -> bool {
+ self.0.get().is_postcondition()
+ }
+
/// Renders a view of the concrete identifier.
pub fn view(self) -> view::View {
ConcreteId::from_global_id(self).view()
@@ -380,6 +392,18 @@ impl GlobalIdInner {
_ => false,
}
}
+
+ /// Returns true if the underlying identifier has the precondition suffix
+ /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+ pub fn is_precondition(&self) -> bool {
+ matches!(self, GlobalIdInner::Concrete(concrete_id) if matches!(concrete_id.suffix, Some(ReservedSuffix::Pre)))
+ }
+
+ /// Returns true if the underlying identifier has the postcondition suffix
+ /// Should be removed once https://github.com/cryspen/hax/issues/1646 has been fixed
+ pub fn is_postcondition(&self) -> bool {
+ matches!(self, GlobalIdInner::Concrete(concrete_id) if matches!(concrete_id.suffix, Some(ReservedSuffix::Post)))
+ }
}
impl ConcreteId {
diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs
index ba5f39319..26da17bb2 100644
--- a/rust-engine/src/backends/lean.rs
+++ b/rust-engine/src/backends/lean.rs
@@ -10,7 +10,6 @@ use std::sync::LazyLock;
use super::prelude::*;
use crate::{
ast::identifiers::global_id::view::{ConstructorKind, PathSegment, TypeDefKind},
- printer::pretty_ast::DebugJSON,
resugarings::BinOp,
};
@@ -163,6 +162,7 @@ impl LeanPrinter {
/// TODO: This should be treated directly in the name rendering engine, see
/// https://github.com/cryspen/hax/issues/1630
pub fn escape(&self, id: String) -> String {
+ let id = id.replace([' ', '<', '>'], "_");
if id.is_empty() {
"_ERROR_EMPTY_ID_".to_string()
} else if RESERVED_KEYWORDS.contains(&id) || id.starts_with(|c: char| c.is_ascii_digit()) {
@@ -172,6 +172,11 @@ impl LeanPrinter {
}
}
+ /// Renders a single symbol, used for anonymous implementations of typeclasses
+ pub fn render_symbol(&self, symbol: Symbol) -> String {
+ self.escape(symbol.to_string())
+ }
+
/// Renders the last, most local part of an id. Used for named arguments of constructors.
pub fn render_last(&self, id: &GlobalId) -> String {
let id = self
@@ -185,15 +190,6 @@ impl LeanPrinter {
self.escape(id)
}
- /// Renders expressions with an explicit ascription `(e : ty)`. Used for numeric literals (to
- /// prevent incorrect inference), etc.
- fn expr_typed<'a, 'b, A: 'a + Clone>(&'a self, expr: &'b Expr) -> DocBuilder<'a, Self, A> {
- install_pretty_helpers!(self: Self);
- docs![expr.kind(), reflow!(" : "), expr.ty.kind()]
- .parens()
- .group()
- }
-
/// Renders expressions with an explicit ascription `(e : Result ty)`. Used for the body of closure, for
/// numeric literals, etc.
fn expr_typed_result<'a, 'b, A: 'a + Clone>(
@@ -203,24 +199,47 @@ impl LeanPrinter {
macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
install_pretty_helpers!(self: Self);
docs![
- expr.kind(),
+ expr,
reflow!(" : "),
- docs!["Result", line!(), expr.ty.kind()].group()
+ docs!["Result", line!(), &expr.ty].group()
]
.group()
}
}
+/// Render parameters, adding a line after each parameter
+impl<'a, A: 'a + Clone> Pretty<'a, LeanPrinter, A> for &Vec {
+ fn pretty(self, allocator: &'a LeanPrinter) -> DocBuilder<'a, LeanPrinter, A> {
+ allocator.params(self)
+ }
+}
+
#[prepend_associated_functions_with(install_pretty_helpers!(self: Self))]
const _: () = {
// Boilerplate: define local macros to disambiguate otherwise `std` macros.
#[allow(unused)]
macro_rules! todo {($($tt:tt)*) => {disambiguated_todo!($($tt)*)};}
- #[allow(unused)]
+
+ // Insert a new line in a doc (pretty)
macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
- #[allow(unused)]
+
+ // Concatenate docs (pretty )
macro_rules! concat {($($tt:tt)*) => {disambiguated_concat!($($tt)*)};}
+ // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `ASBS...CS`
+ macro_rules! zip_right {
+ ($a:expr, $sep:expr) => {
+ docs![concat!($a.into_iter().map(|a| docs![a, $sep]))]
+ };
+ }
+
+ // Given an iterable `[A,B, ... , C]` and a separator `S`, create the doc `SASB...SC`
+ macro_rules! zip_left {
+ ($sep:expr, $a:expr) => {
+ docs![concat!($a.into_iter().map(|a| docs![$sep, a]))]
+ };
+ }
+
// Methods for handling arguments of variants (or struct constructor)
impl LeanPrinter {
/// Prints arguments a variant or constructor of struct, using named or unamed arguments based
@@ -271,6 +290,14 @@ const _: () = {
macro_rules! line {($($tt:tt)*) => {disambiguated_line!($($tt)*)};}
docs![intersperse!(fields.iter().map(|(_, e)| e), line!())].group()
}
+
+ /// Prints parameters of functions (items, trait items, impl items)
+ fn params<'a, 'b, A: 'a + Clone>(
+ &'a self,
+ params: &'b Vec,
+ ) -> DocBuilder<'a, Self, A> {
+ zip_right!(params, line!())
+ }
}
impl<'a, 'b, A: 'a + Clone> PrettyAst<'a, 'b, A> for LeanPrinter {
@@ -312,28 +339,46 @@ set_option linter.unusedVariables false
}
/// Render generics, adding a space after each parameter
- fn generics(&'a self, generics: &'b Generics) -> DocBuilder<'a, Self, A> {
+ fn generics(
+ &'a self,
+ Generics {
+ params,
+ constraints,
+ }: &'b Generics,
+ ) -> DocBuilder<'a, Self, A> {
// TODO : The lean backend should not ignore constraints on generic params, see
// https://github.com/cryspen/hax/issues/1636
- concat!(generics.params.iter().map(|param| {
- match param.kind {
- GenericParamKind::Lifetime => unreachable!(),
- GenericParamKind::Type => docs![param, reflow!(" : Type")]
- .parens()
- .group()
- .append(line!()),
- GenericParamKind::Const { .. } => {
- todo!("-- to debug const param run: {}", DebugJSON(param))
- }
- }
- }))
+ docs![
+ zip_right!(params, line!()),
+ zip_right!(
+ constraints
+ .iter()
+ .map(|constraint| docs![constraint].brackets()),
+ line!()
+ ),
+ ]
.group()
}
- fn expr(&'a self, expr: &'b Expr) -> DocBuilder<'a, Self, A> {
- match *expr.kind {
- ExprKind::Literal(Literal::Int { .. }) => self.expr_typed(expr),
- _ => docs![expr.kind()],
+ fn generic_constraint(
+ &'a self,
+ generic_constraint: &'b GenericConstraint,
+ ) -> DocBuilder<'a, Self, A> {
+ match generic_constraint {
+ GenericConstraint::Type(impl_ident) => docs![impl_ident],
+ _ => todo!("-- unsupported constraint"),
+ }
+ }
+
+ fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
+ match generic_param.kind() {
+ GenericParamKind::Type => docs![&generic_param.ident, reflow!(" : Type")]
+ .parens()
+ .group(),
+ GenericParamKind::Lifetime => unreachable!(),
+ GenericParamKind::Const { .. } => {
+ todo!("-- Unsupported const param")
+ }
}
}
@@ -341,8 +386,11 @@ set_option linter.unusedVariables false
docs![&*pat.kind, reflow!(" : "), &pat.ty].parens().group()
}
- fn expr_kind(&'a self, expr_kind: &'b ExprKind) -> DocBuilder<'a, Self, A> {
- match expr_kind {
+ fn expr(&'a self, Expr { kind, ty, meta: _ }: &'b Expr) -> DocBuilder<'a, Self, A> {
+ match &**kind {
+ ExprKind::Literal(int_lit @ Literal::Int { .. }) => {
+ docs![int_lit, reflow!(" : "), ty].parens().group()
+ }
ExprKind::If {
condition,
then,
@@ -352,12 +400,13 @@ set_option linter.unusedVariables false
// TODO: have a proper monadic resugaring, see
// https://github.com/cryspen/hax/issues/1620
docs![
- docs!["if", line!(), condition, reflow!(" then")].group(),
- docs![line!(), "do", line!(), then].nest(INDENT),
+ docs!["← if", line!(), condition, reflow!(" then do")].group(),
+ docs![line!(), then].nest(INDENT),
line!(),
- "else",
- docs![line!(), "do", line!(), else_branch].nest(INDENT)
+ reflow!("else do"),
+ docs![line!(), else_branch].nest(INDENT)
]
+ .parens()
.group()
} else {
// The Hax engine should ensure that there is always an else branch
@@ -390,6 +439,7 @@ set_option linter.unusedVariables false
.group(),
);
docs![monadic_lift, head, generic_args, args]
+ .nest(INDENT)
.parens()
.group()
}
@@ -398,7 +448,8 @@ set_option linter.unusedVariables false
"#v[",
intersperse!(exprs, docs![",", line!()])
.nest(INDENT)
- .group(),
+ .group()
+ .align(),
"]"
]
.group(),
@@ -413,12 +464,10 @@ set_option linter.unusedVariables false
docs![constructor]
} else if base.is_some() {
// TODO : support base expressions. see https://github.com/cryspen/hax/issues/1637
- todo!(
- "-- Unsupported base expressions for structs. To see the ast of the item run : {}",
- DebugJSON(expr_kind)
- )
+ todo!("-- Unsupported base expressions for structs.")
} else {
docs![constructor, line!(), self.arguments(fields, is_record)]
+ .nest(INDENT)
.parens()
.group()
}
@@ -443,7 +492,7 @@ set_option linter.unusedVariables false
]
.group(),
" ←",
- line!(),
+ softline!(),
docs!["pure", line!(), rhs].parens().group(),
";"
]
@@ -508,8 +557,9 @@ set_option linter.unusedVariables false
// TODO: This monad lifting should be handled by a phase/resugaring, see
// https://github.com/cryspen/hax/issues/1620
- docs!["← ", lhs, softline!(), symbol, softline!(), rhs]
+ docs!["← ", lhs, line!(), docs![symbol, softline!(), rhs].group()]
.group()
+ .nest(INDENT)
.parens()
}
ResugaredExprKind::Tuple { .. } => {
@@ -611,34 +661,37 @@ set_option linter.unusedVariables false
}
fn ty(&'a self, ty: &'b Ty) -> DocBuilder<'a, Self, A> {
- docs![ty.kind()]
- }
-
- fn ty_kind(&'a self, ty_kind: &'b TyKind) -> DocBuilder<'a, Self, A> {
- match ty_kind {
+ match ty.kind() {
TyKind::Primitive(primitive_ty) => docs![primitive_ty],
TyKind::App { head, args } => {
if args.is_empty() {
docs![head]
} else {
- docs![head, softline!(), intersperse!(args, softline!())]
+ docs![head, zip_left!(line!(), args)]
.parens()
.group()
+ .nest(INDENT)
}
}
TyKind::Arrow { inputs, output } => docs![
- concat![inputs.iter().map(|input| docs![input, reflow!(" -> ")])],
+ zip_right!(inputs, docs![line!(), reflow!("-> ")]),
"Result ",
output
- ],
+ ]
+ .group(),
TyKind::Param(local_id) => docs![local_id],
TyKind::Slice(ty) => docs!["RustSlice", line!(), ty].parens().group(),
- TyKind::Array { ty, length } => {
- docs!["RustArray", line!(), ty, line!(), &(*length.kind)]
- .parens()
- .group()
+ TyKind::Array { ty, length } => docs!["RustArray", line!(), ty, line!(), &**length]
+ .parens()
+ .group(),
+ TyKind::AssociatedType { impl_, item } => {
+ let kind = impl_.kind();
+ match &kind {
+ ImplExprKind::Self_ => docs![self.render_last(item)],
+ _ => todo!("sorry \n-- support only local associated types\n"), // Support only local associated types
+ }
}
- _ => todo!(),
+ _ => todo!("sorry \n-- unsupported type\n"),
}
}
@@ -685,13 +738,13 @@ set_option linter.unusedVariables false
(Signedness::Signed, IntSize::S16) => "i16",
(Signedness::Signed, IntSize::S32) => "i32",
(Signedness::Signed, IntSize::S64) => "i64",
- (Signedness::Signed, IntSize::S128) => todo!(),
+ (Signedness::Signed, IntSize::S128) => "i128",
(Signedness::Signed, IntSize::SSize) => "isize",
(Signedness::Unsigned, IntSize::S8) => "u8",
(Signedness::Unsigned, IntSize::S16) => "u16",
(Signedness::Unsigned, IntSize::S32) => "u32",
(Signedness::Unsigned, IntSize::S64) => "u64",
- (Signedness::Unsigned, IntSize::S128) => todo!(),
+ (Signedness::Unsigned, IntSize::S128) => "u128",
(Signedness::Unsigned, IntSize::SSize) => "usize",
}]
}
@@ -723,12 +776,18 @@ set_option linter.unusedVariables false
docs![¶m.pat]
}
- fn generic_param(&'a self, generic_param: &'b GenericParam) -> DocBuilder<'a, Self, A> {
- docs![&generic_param.ident]
- }
-
- fn item_kind(&'a self, item_kind: &'b ItemKind) -> DocBuilder<'a, Self, A> {
- match item_kind {
+ fn item(
+ &'a self,
+ item @ Item {
+ ident,
+ kind,
+ meta: _,
+ }: &'b Item,
+ ) -> DocBuilder<'a, Self, A> {
+ if !LeanPrinter::printable_item(item) {
+ return nil!();
+ };
+ match kind {
ItemKind::Fn {
name,
generics,
@@ -738,41 +797,25 @@ set_option linter.unusedVariables false
} => match &*body.kind {
// TODO: Literal consts. This should be done by a resugaring, see
// https://github.com/cryspen/hax/issues/1614
- ExprKind::Literal(l) if params.is_empty() => docs![
- reflow!("def "),
- name,
- reflow!(" : "),
- &body.ty,
- reflow!(" := "),
- l
- ]
- .group(),
- _ => {
- let generics = (!generics.params.is_empty()).then_some(
- docs![intersperse!(&generics.params, line!()).braces().group()].group(),
- );
+ ExprKind::Literal(l) if params.is_empty() => {
+ docs!["def ", name, reflow!(" : "), &body.ty, reflow!(" := "), l].group()
+ }
+ _ => docs![
docs![
- docs![
- reflow!("def "),
- name,
- softline!(),
- generics,
- softline!(),
- docs![intersperse!(params, line!())].group(),
- line!(),
- ": Result",
- softline!(),
- &body.ty,
- line!(),
- ":= do",
- ]
- .group(),
+ docs!["def", line!(), name].group(),
+ line!(),
+ generics,
+ params,
+ docs![": Result", line!(), &body.ty].group(),
line!(),
- &*body.kind
+ ":= do"
]
- .group()
- .nest(INDENT)
- }
+ .group(),
+ line!(),
+ body
+ ]
+ .group()
+ .nest(INDENT),
},
ItemKind::TyAlias {
name,
@@ -820,25 +863,16 @@ set_option linter.unusedVariables false
hardline!()
)
};
- let generics = (!generics.params.is_empty()).then_some(
- concat![generics.params.iter().map(|param| docs![param, line!()])]
- .group(),
- );
docs![
- docs!["structure ", name, line!(), generics, "where"].group(),
- docs![hardline!(), args].nest(INDENT),
+ docs![reflow!("structure "), name, line!(), generics, "where"].group(),
+ docs![hardline!(), args],
]
+ .nest(INDENT)
.group()
} else {
// Enums
- let applied_name: DocBuilder<'a, Self, A> = docs![
- name,
- concat!(generics.params.iter().map(|param| match param.kind {
- GenericParamKind::Type => docs![line!(), param],
- _ => nil!(),
- }))
- ]
- .group();
+ let applied_name: DocBuilder<'a, Self, A> =
+ docs![name, line!(), generics].group();
docs![
docs!["inductive ", name, line!(), generics, ": Type"].group(),
hardline!(),
@@ -850,27 +884,194 @@ set_option linter.unusedVariables false
]
}
}
- _ => todo!("-- to debug missing item run: {}", DebugJSON(item_kind)),
+ ItemKind::Trait {
+ name,
+ generics,
+ items,
+ } => {
+ // Type parameters are also parameters of the class, but constraints are fields of the class
+ docs![
+ docs![
+ docs![reflow!("class "), name],
+ (!generics.params.is_empty()).then_some(docs![
+ line!(),
+ intersperse!(&generics.params, line!()).group()
+ ]),
+ line!(),
+ "where"
+ ]
+ .group(),
+ hardline!(),
+ (!generics.constraints.is_empty()).then_some(docs![zip_right!(
+ generics
+ .constraints
+ .iter()
+ .map(|constraint: &GenericConstraint| {
+ match constraint {
+ GenericConstraint::Type(tc_constraint) => docs![
+ format!("_constr_{}", tc_constraint.name),
+ " :",
+ line!(),
+ constraint
+ ]
+ .group()
+ .brackets(),
+ _ => {
+ todo!("unsupported type constraint in trait definition")
+ }
+ }
+ }),
+ 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!()
+ )
+ ]
+ .nest(INDENT)
+ }
+ ItemKind::Impl {
+ generics,
+ self_ty: _,
+ of_trait: (trait_, args),
+ items,
+ parent_bounds: _,
+ safety: _,
+ } => docs![
+ docs![
+ docs![reflow!("instance "), ident, line!(), generics, ":"].group(),
+ line!(),
+ docs![trait_, concat!(args.iter().map(|gv| docs![line!(), gv]))].group(),
+ line!(),
+ "where",
+ ]
+ .group()
+ .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!()
+ )
+ ]
+ .nest(INDENT),
+ ],
+ _ => todo!("-- unsupported item"),
}
}
- fn item(&'a self, item: &'b Item) -> DocBuilder<'a, Self, A> {
- if LeanPrinter::printable_item(item) {
- docs![item.kind()]
- } else {
- nil!()
+ fn trait_item(
+ &'a self,
+ TraitItem {
+ meta: _,
+ kind,
+ generics,
+ ident,
+ }: &'b TraitItem,
+ ) -> DocBuilder<'a, Self, A> {
+ let name = self.render_last(ident);
+ docs![match kind {
+ TraitItemKind::Fn(ty) => {
+ docs![name, softline!(), generics, ":", line!(), ty]
+ .group()
+ .nest(INDENT)
+ }
+ TraitItemKind::Type(constraints) => {
+ docs![
+ name.clone(),
+ reflow!(" : Type"),
+ concat!(constraints.iter().map(|c| docs![
+ hardline!(),
+ docs![format!("_constr_{}", c.name),
+ reflow!(" :"),
+ line!(),
+ &c.goal
+ ]
+ .group()
+ .nest(INDENT)
+ .brackets()]))
+ ]
+ }
+ _ => todo!("-- unsupported trait item"),
+ }]
+ }
+
+ fn impl_item(
+ &'a self,
+ ImplItem {
+ meta: _,
+ generics,
+ kind,
+ ident,
+ }: &'b ImplItem,
+ ) -> DocBuilder<'a, Self, A> {
+ let name = self.render_last(ident);
+ match kind {
+ ImplItemKind::Type {
+ ty,
+ parent_bounds: _,
+ } => docs![name, reflow!(" := "), ty],
+ ImplItemKind::Fn { body, params } => docs![
+ docs![
+ name,
+ softline!(),
+ generics,
+ zip_right!(params, line!()).group().align(),
+ ":= do",
+ ]
+ .group(),
+ line!(),
+ body
+ ]
+ .group()
+ .nest(INDENT),
+ ImplItemKind::Resugared(_) => todo!(),
}
}
- fn variant(&'a self, variant: &'b Variant) -> DocBuilder<'a, Self, A> {
+ fn impl_ident(
+ &'a self,
+ ImplIdent { goal, name: _ }: &'b ImplIdent,
+ ) -> DocBuilder<'a, Self, A> {
+ docs![goal]
+ }
+
+ fn trait_goal(
+ &'a self,
+ TraitGoal { trait_, args }: &'b TraitGoal,
+ ) -> DocBuilder<'a, Self, A> {
+ docs![trait_, concat!(args.iter().map(|arg| docs![line!(), arg]))]
+ .parens()
+ .nest(INDENT)
+ .group()
+ }
+
+ fn variant(
+ &'a self,
+ Variant {
+ name,
+ arguments,
+ is_record,
+ attributes: _,
+ }: &'b Variant,
+ ) -> DocBuilder<'a, Self, A> {
docs![
- self.render_last(&variant.name),
+ self.render_last(name),
softline!(),
- if variant.is_record {
+ // args
+ if *is_record {
// Use named the arguments, keeping only the head of the identifier
docs![
intersperse!(
- variant.arguments.iter().map(|(id, ty, _)| {
+ arguments.iter().map(|(id, ty, _)| {
docs![self.render_last(id), reflow!(" : "), ty]
.parens()
.group()
@@ -879,15 +1080,16 @@ set_option linter.unusedVariables false
)
.align()
.nest(INDENT),
- reflow!(" : ")
+ line!(),
+ reflow!(": "),
]
+ .group()
} else {
// Use anonymous arguments
docs![
- reflow!(" : "),
+ reflow!(": "),
concat!(
- variant
- .arguments
+ arguments
.iter()
.map(|(_, ty, _)| { docs![ty, reflow!(" -> ")] })
)
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 1f52a18d0..0f62729a7 100644
--- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
+++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap
@@ -41,50 +41,285 @@ 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 -> Result usize
+
+class Lean_tests.Traits.Overlapping_methods.T2 (Self : Type) where
+ f : Self -> Result usize
+
+class Lean_tests.Traits.Overlapping_methods.T3 (Self : Type) where
+ f : Self -> Result usize
+
+instance Lean_tests.Traits.Overlapping_methods.Impl :
+ Lean_tests.Traits.Overlapping_methods.T1 u32
+ where
+ f (self : u32) := do (0 : usize)
+
+instance Lean_tests.Traits.Overlapping_methods.Impl_1 :
+ Lean_tests.Traits.Overlapping_methods.T2 u32
+ where
+ f (self : u32) := do (1 : usize)
+
+instance Lean_tests.Traits.Overlapping_methods.Impl_2 :
+ Lean_tests.Traits.Overlapping_methods.T3 u32
+ where
+ f (self : u32) := do (2 : usize)
+
+def Lean_tests.Traits.Overlapping_methods.test
+ (_ : Rust_primitives.Hax.Tuple0)
+ : Result usize
+ := do
+ let (x : u32) ← (pure (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))
+
+class Lean_tests.Traits.Inheritance.T1 (Self : Type) where
+ f1 : Self -> Result usize
+
+class Lean_tests.Traits.Inheritance.T2 (Self : Type) where
+ f2 : Self -> Result usize
+
+class Lean_tests.Traits.Inheritance.T3 (Self : Type) where
+ [_constr_5860918688139008796 : (Lean_tests.Traits.Inheritance.T2 Self)]
+ [_constr_2614080591691505761 : (Lean_tests.Traits.Inheritance.T1 Self)]
+ f3 : Self -> Result usize
+
+class Lean_tests.Traits.Inheritance.Tp1 (Self : Type) where
+ f1 : Self -> Result usize
+
+class Lean_tests.Traits.Inheritance.Tp2 (Self : Type) where
+ [_constr_9900012313089209274 : (Lean_tests.Traits.Inheritance.Tp1 Self)]
+ [_constr_3518312647081482353 : (Lean_tests.Traits.Inheritance.T3 Self)]
+ fp2 : Self -> Result usize
+
+structure Lean_tests.Traits.Inheritance.S where
+
+
+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 (1 : 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 (2 : 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 (3 : 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 (10 : usize)
+
+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 Lean_tests.Traits.Inheritance.test
+ (_ : Rust_primitives.Hax.Tuple0)
+ : Result usize
+ := do
+ let s : Lean_tests.Traits.Inheritance.S ← (pure
+ Lean_tests.Traits.Inheritance.S.mk);
+ (← (← Lean_tests.Traits.Inheritance.T3.f3 s) +? (1 : usize))
+
+class Lean_tests.Traits.Bounds.T1 (Self : Type) where
+ f1 : Self -> Result usize
+
+class Lean_tests.Traits.Bounds.T2 (Self : Type) where
+ f2 : Self -> Result usize
+
+class Lean_tests.Traits.Bounds.Test (Self : Type) (T : Type) where
+ [_constr_11094313111027375411 : (Lean_tests.Traits.Bounds.T2 Self)]
+ [_constr_11502165326992889641 : (Lean_tests.Traits.Bounds.T1 T)]
+ f_test : Self -> T -> Result usize
+
+structure Lean_tests.Traits.Bounds.S1 where
+
+
+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 (0 : usize)
+
+structure Lean_tests.Traits.Bounds.S2 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 (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))
+
+def Lean_tests.Traits.Bounds.test
+ (x1 : Lean_tests.Traits.Bounds.S1)
+ (x2 : Lean_tests.Traits.Bounds.S2)
+ : Result usize
+ := do
+ (← (← Lean_tests.Traits.Bounds.Test.f_test x2 x1)
+ +? (← Lean_tests.Traits.Bounds.T1.f1 x1))
+
+class Lean_tests.Traits.Basic.T1 (Self : Type) where
+ f1 : Self -> Result usize
+ f2 : Self -> Self -> Result usize
+
+structure Lean_tests.Traits.Basic.S where
+
+
+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 (42 : usize)
+ f2 (self : Lean_tests.Traits.Basic.S)
+ (other : Lean_tests.Traits.Basic.S)
+ := do
+ (43 : usize)
+
+def Lean_tests.Traits.Basic.f
+ (T : Type) [(Lean_tests.Traits.Basic.T1 T)] (x : T)
+ : Result usize
+ := do
+ (← (← Lean_tests.Traits.Basic.T1.f1 x)
+ +? (← Lean_tests.Traits.Basic.T1.f2 x x))
+
+class Lean_tests.Traits.Associated_types.Foo (Self : Type) (T : Type) where
+
+
+class Lean_tests.Traits.Associated_types.Bar (Self : Type) where
+
+
+structure Lean_tests.Traits.Associated_types.S where
+
+
+instance Lean_tests.Traits.Associated_types.Impl_2 :
+ Lean_tests.Traits.Associated_types.Bar i16
+ where
+
+
+instance Lean_tests.Traits.Associated_types.Impl_3 (A : Type) :
+ Lean_tests.Traits.Associated_types.Foo (Rust_primitives.Hax.Tuple2 u32 A) i16
+ where
+
+
+class Lean_tests.Traits.Associated_types.T1 (Self : Type) where
+ T : Type
+ f : Self -> T -> Result T
+
+class Lean_tests.Traits.Associated_types.T3 (Self : Type) where
+ T : Type
+ [_constr_9884638762124940061 : (Lean_tests.Traits.Associated_types.Bar T)]
+ Tp : Type
+ [_constr_16271648697586611929 : (Lean_tests.Traits.Associated_types.Foo Tp T)]
+ f (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] :
+ Self -> T -> Tp -> Result 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 (2121 : i32)
+
+class Lean_tests.Traits.Associated_types.T2 (Self : Type) where
+ T : Type
+ [_constr_11855681382024687155 : (Lean_tests.Traits.Associated_types.T1 T)]
+ f : Self -> T -> Result usize
+
+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
+ (21 : usize)
+
+structure Lean_tests.Structs.Miscellaneous.S where
+ f : i32
+
+def Lean_tests.Structs.Miscellaneous.test_tuples
+ (_ : Rust_primitives.Hax.Tuple0)
+ : Result (Rust_primitives.Hax.Tuple2 i32 i32)
+ := do
+ let lit : i32 ← (pure (1 : i32));
+ let constr : Lean_tests.Structs.Miscellaneous.S ← (pure
+ (Lean_tests.Structs.Miscellaneous.S.mk (f := (42 : i32))));
+ let proj : i32 ← (pure (Lean_tests.Structs.Miscellaneous.S.f constr));
+ let ite : (Rust_primitives.Hax.Tuple2 i32 i32) ← (pure
+ (← if true then do
+ (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32))
+ else do
+ let z : i32 ← (pure (← (1 : i32) +? (2 : i32)));
+ (Rust_primitives.Hax.Tuple2.mk z z)));
+ (Rust_primitives.Hax.Tuple2.mk (1 : i32) (2 : i32))
+
structure Lean_tests.Structs.T0 where
-structure Lean_tests.Structs.T1 A where
+structure Lean_tests.Structs.T1 (A : Type) where
_0 : A
-structure Lean_tests.Structs.T2 A B where
+structure Lean_tests.Structs.T2 (A : Type) (B : Type) where
_0 : A
_1 : B
-structure Lean_tests.Structs.T3 A B C where
+structure Lean_tests.Structs.T3 (A : Type) (B : Type) (C : Type) where
_0 : A
_1 : B
_2 : C
-structure Lean_tests.Structs.T3p A B C where
+structure Lean_tests.Structs.T3p (A : Type) (B : Type) (C : Type) where
_0 : A
_1 : (Lean_tests.Structs.T2 B C)
-def Lean_tests.Structs.tuple_structs (_ : Rust_primitives.Hax.Tuple0)
+def Lean_tests.Structs.tuple_structs
+ (_ : Rust_primitives.Hax.Tuple0)
: Result Rust_primitives.Hax.Tuple0
:= do
let t0 : Lean_tests.Structs.T0 ← (pure Lean_tests.Structs.T0.mk);
- let t1 : (Lean_tests.Structs.T1 i32) ←
- (pure (Lean_tests.Structs.T1.mk (1 : i32)));
- let t2 : (Lean_tests.Structs.T2 i32 i32) ←
- (pure (Lean_tests.Structs.T2.mk (1 : i32) (2 : i32)));
+ let t1 : (Lean_tests.Structs.T1 i32) ← (pure
+ (Lean_tests.Structs.T1.mk (1 : i32)));
+ let t2 : (Lean_tests.Structs.T2 i32 i32) ← (pure
+ (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)) ←
- (pure
+ t3 : (Lean_tests.Structs.T3
+ Lean_tests.Structs.T0
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32)) ← (pure
(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))));
+ 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)) ←
- (pure
+ t3p : (Lean_tests.Structs.T3p
+ Lean_tests.Structs.T0
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32)) ← (pure
(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)))));
+ 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 (⟨⟩ : Lean_tests.Structs.T0) ← (pure t0);
let (⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)) ← (pure t1);
let (⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32)) ← (pure t2);
@@ -92,62 +327,63 @@ def Lean_tests.Structs.tuple_structs (_ : Rust_primitives.Hax.Tuple0)
(⟨(⟨⟩ : Lean_tests.Structs.T0),
(⟨(_ : i32)⟩ : (Lean_tests.Structs.T1 i32)),
(⟨(_ : i32), (_ : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
- (Lean_tests.Structs.T3 Lean_tests.Structs.T0 (Lean_tests.Structs.T1 i32)
- (Lean_tests.Structs.T2 i32 i32))) ←
- (pure t3);
+ (Lean_tests.Structs.T3
+ Lean_tests.Structs.T0
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32))) ← (pure t3);
let
(⟨(⟨⟩ : Lean_tests.Structs.T0),
(⟨(⟨(_ : i32)⟩ : (Lean_tests.Structs.T1 i32)),
(⟨(_ : i32), (_ : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
- (Lean_tests.Structs.T2 (Lean_tests.Structs.T1 i32) (Lean_tests.Structs.T2
- i32 i32)))⟩ : (Lean_tests.Structs.T3p Lean_tests.Structs.T0
- (Lean_tests.Structs.T1 i32) (Lean_tests.Structs.T2 i32 i32))) ←
- (pure t3p);
+ (Lean_tests.Structs.T2
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32)))⟩ : (Lean_tests.Structs.T3p
+ Lean_tests.Structs.T0
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32))) ← (pure t3p);
let (_ : i32) ← (pure (Lean_tests.Structs.T1._0 t1));
let (_ : i32) ← (pure (Lean_tests.Structs.T2._0 t2));
let (_ : i32) ← (pure (Lean_tests.Structs.T2._1 t2));
let (_ : Lean_tests.Structs.T0) ← (pure (Lean_tests.Structs.T3._0 t3));
let (_ : (Lean_tests.Structs.T1 i32)) ← (pure (Lean_tests.Structs.T3._1 t3));
- let (_ : (Lean_tests.Structs.T2 i32 i32)) ←
- (pure (Lean_tests.Structs.T3._2 t3));
- let (_ : i32) ←
- (pure (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3._2 t3)));
+ let (_ : (Lean_tests.Structs.T2 i32 i32)) ← (pure
+ (Lean_tests.Structs.T3._2 t3));
+ let (_ : i32) ← (pure
+ (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3._2 t3)));
let (_ : Lean_tests.Structs.T0) ← (pure (Lean_tests.Structs.T3p._0 t3p));
let
- (_ : (Lean_tests.Structs.T2 (Lean_tests.Structs.T1 i32)
- (Lean_tests.Structs.T2 i32 i32))) ←
- (pure (Lean_tests.Structs.T3p._1 t3p));
- let (_ : i32) ←
- (pure
+ (_ : (Lean_tests.Structs.T2
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32))) ← (pure
+ (Lean_tests.Structs.T3p._1 t3p));
+ let (_ : i32) ← (pure
(Lean_tests.Structs.T2._0
- (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p))));
- let (_ : (Lean_tests.Structs.T1 i32)) ←
- (pure (Lean_tests.Structs.T2._0 (Lean_tests.Structs.T3p._1 t3p)));
- let (_ : (Lean_tests.Structs.T2 i32 i32)) ←
- (pure (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p)));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure (match t0 with | ⟨⟩ => do Rust_primitives.Hax.Tuple0.mk));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure (match t1 with | ⟨(u1 : i32)⟩ => do Rust_primitives.Hax.Tuple0.mk));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure
+ (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p))));
+ let (_ : (Lean_tests.Structs.T1 i32)) ← (pure
+ (Lean_tests.Structs.T2._0 (Lean_tests.Structs.T3p._1 t3p)));
+ let (_ : (Lean_tests.Structs.T2 i32 i32)) ← (pure
+ (Lean_tests.Structs.T2._1 (Lean_tests.Structs.T3p._1 t3p)));
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
+ (match t0 with | ⟨⟩ => do Rust_primitives.Hax.Tuple0.mk));
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
+ (match t1 with | ⟨(u1 : i32)⟩ => do Rust_primitives.Hax.Tuple0.mk));
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
(match t2 with
| ⟨(u2 : i32), (u3 : i32)⟩ => do Rust_primitives.Hax.Tuple0.mk));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
(match t3 with
| ⟨(⟨⟩ : Lean_tests.Structs.T0),
(⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)),
(⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩
=> do Rust_primitives.Hax.Tuple0.mk));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
(match t3p with
| ⟨(⟨⟩ : Lean_tests.Structs.T0),
(⟨(⟨(u1 : i32)⟩ : (Lean_tests.Structs.T1 i32)),
(⟨(u2 : i32), (u3 : i32)⟩ : (Lean_tests.Structs.T2 i32 i32))⟩ :
- (Lean_tests.Structs.T2 (Lean_tests.Structs.T1 i32)
- (Lean_tests.Structs.T2 i32 i32)))⟩
+ (Lean_tests.Structs.T2
+ (Lean_tests.Structs.T1 i32)
+ (Lean_tests.Structs.T2 i32 i32)))⟩
=> do Rust_primitives.Hax.Tuple0.mk));
Rust_primitives.Hax.Tuple0.mk
@@ -166,65 +402,64 @@ structure Lean_tests.Structs.S3 where
_structure : usize
_inductive : usize
-def Lean_tests.Structs.normal_structs (_ : Rust_primitives.Hax.Tuple0)
+def Lean_tests.Structs.normal_structs
+ (_ : Rust_primitives.Hax.Tuple0)
: Result Rust_primitives.Hax.Tuple0
:= do
- let s1 : Lean_tests.Structs.S1 ←
- (pure (Lean_tests.Structs.S1.mk (f1 := (0 : usize)) (f2 := (1 : usize))));
- let s2 : Lean_tests.Structs.S2 ←
- (pure
+ let s1 : Lean_tests.Structs.S1 ← (pure
+ (Lean_tests.Structs.S1.mk (f1 := (0 : usize)) (f2 := (1 : usize))));
+ let s2 : Lean_tests.Structs.S2 ← (pure
(Lean_tests.Structs.S2.mk
- (f1 := (Lean_tests.Structs.S1.mk (f1 := (2 : usize)) (f2 := (3 : usize))))
- (f2 := (4 : usize))));
- let s3 : Lean_tests.Structs.S3 ←
- (pure
+ (f1 := (Lean_tests.Structs.S1.mk (f1 := (2 : usize)) (f2 := (3 : usize))))
+ (f2 := (4 : usize))));
+ let s3 : Lean_tests.Structs.S3 ← (pure
(Lean_tests.Structs.S3.mk
- (_end := (0 : usize))
- (_def := (0 : usize))
- (_theorem := (0 : usize))
- (_structure := (0 : usize))
- (_inductive := (0 : usize))));
- let ({f1 := (f1 : usize), f2 := (f2 : usize)} : Lean_tests.Structs.S1) ←
- (pure s1);
+ (_end := (0 : usize))
+ (_def := (0 : usize))
+ (_theorem := (0 : usize))
+ (_structure := (0 : usize))
+ (_inductive := (0 : usize))));
+ let ({f1 := (f1 : usize), f2 := (f2 : usize)} : Lean_tests.Structs.S1) ← (pure
+ s1);
let
({f1 := (f1 : usize), f2 := (other_name_for_f2 : usize)} :
- Lean_tests.Structs.S1) ←
- (pure s1);
+ Lean_tests.Structs.S1) ← (pure s1);
let
({f1 := ({f1 := (f1 : usize), f2 := (f2 : usize)} : Lean_tests.Structs.S1),
- f2 := (other_name_for_f2 : usize)} : Lean_tests.Structs.S2) ←
- (pure s2);
+ f2 := (other_name_for_f2 : usize)} : Lean_tests.Structs.S2) ← (pure s2);
let
({_end := (_end : usize),
_def := (_def : usize),
_theorem := (_theorem : usize),
_structure := (_structure : usize),
- _inductive := (_inductive : usize)} : Lean_tests.Structs.S3) ←
- (pure s3);
- let (_ : (Rust_primitives.Hax.Tuple2 usize usize)) ←
- (pure
+ _inductive := (_inductive : usize)} : Lean_tests.Structs.S3) ← (pure s3);
+ let (_ : (Rust_primitives.Hax.Tuple2 usize usize)) ← (pure
(Rust_primitives.Hax.Tuple2.mk
- (Lean_tests.Structs.S1.f1 s1) (Lean_tests.Structs.S1.f2 s1)));
+ (Lean_tests.Structs.S1.f1 s1) (Lean_tests.Structs.S1.f2 s1)));
let
- (_ : (Rust_primitives.Hax.Tuple8 usize usize usize usize usize usize usize
- usize)) ←
- (pure
+ (_ : (Rust_primitives.Hax.Tuple8
+ usize
+ usize
+ usize
+ usize
+ usize
+ usize
+ usize
+ usize)) ← (pure
(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)));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure
+ (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)));
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
(match s1 with
| {f1 := (f1 : usize), f2 := (f2 : usize)}
=> do Rust_primitives.Hax.Tuple0.mk));
- let (_ : Rust_primitives.Hax.Tuple0) ←
- (pure
+ let (_ : Rust_primitives.Hax.Tuple0) ← (pure
(match s2 with
| {f1 := ({f1 := (f1 : usize), f2 := (other_name_for_f2 : usize)} :
Lean_tests.Structs.S1),
@@ -239,39 +474,40 @@ def Lean_tests.Structs.normal_structs (_ : Rust_primitives.Hax.Tuple0)
=> do Rust_primitives.Hax.Tuple0.mk)
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
+| 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
+| 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
+ (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)
+def Lean_tests.Enums.enums
+ (_ : Rust_primitives.Hax.Tuple0)
: Result Rust_primitives.Hax.Tuple0
:= do
let e_v1 : Lean_tests.Enums.E ← (pure Lean_tests.Enums.E.V1);
let e_v2 : Lean_tests.Enums.E ← (pure Lean_tests.Enums.E.V2);
let e_v3 : Lean_tests.Enums.E ← (pure (Lean_tests.Enums.E.V3 (23 : usize)));
- let e_v4 : Lean_tests.Enums.E ←
- (pure (Lean_tests.Enums.E.V4 (23 : usize) (12 : usize) (1 : usize)));
- let e_v5 : Lean_tests.Enums.E ←
- (pure (Lean_tests.Enums.E.V5 (f1 := (23 : usize)) (f2 := (43 : usize))));
- let e_v6 : Lean_tests.Enums.E ←
- (pure (Lean_tests.Enums.E.V6 (f1 := (12 : usize)) (f2 := (13 : usize))));
- let (nil : (Lean_tests.Enums.MyList usize)) ←
- (pure Lean_tests.Enums.MyList.Nil);
- let cons_1 : (Lean_tests.Enums.MyList usize) ←
- (pure (Lean_tests.Enums.MyList.Cons (hd := (1 : usize)) (tl := nil)));
- let cons_2_1 : (Lean_tests.Enums.MyList usize) ←
- (pure (Lean_tests.Enums.MyList.Cons (hd := (2 : usize)) (tl := cons_1)));
+ let e_v4 : Lean_tests.Enums.E ← (pure
+ (Lean_tests.Enums.E.V4 (23 : usize) (12 : usize) (1 : usize)));
+ let e_v5 : Lean_tests.Enums.E ← (pure
+ (Lean_tests.Enums.E.V5 (f1 := (23 : usize)) (f2 := (43 : usize))));
+ let e_v6 : Lean_tests.Enums.E ← (pure
+ (Lean_tests.Enums.E.V6 (f1 := (12 : usize)) (f2 := (13 : usize))));
+ let (nil : (Lean_tests.Enums.MyList usize)) ← (pure
+ Lean_tests.Enums.MyList.Nil);
+ let cons_1 : (Lean_tests.Enums.MyList usize) ← (pure
+ (Lean_tests.Enums.MyList.Cons (hd := (1 : usize)) (tl := nil)));
+ let cons_2_1 : (Lean_tests.Enums.MyList usize) ← (pure
+ (Lean_tests.Enums.MyList.Cons (hd := (2 : usize)) (tl := cons_1)));
(match e_v1 with
| (Lean_tests.Enums.E.V1 ) => do Rust_primitives.Hax.Tuple0.mk
| (Lean_tests.Enums.E.V2 ) => do Rust_primitives.Hax.Tuple0.mk
@@ -292,46 +528,46 @@ def Lean_tests.FORTYTWO : usize := 42
def Lean_tests.MINUS_FORTYTWO : isize := -42
-def Lean_tests.returns42 (_ : Rust_primitives.Hax.Tuple0) : Result usize := do
+def Lean_tests.returns42 (_ : Rust_primitives.Hax.Tuple0) : Result usize := do
Lean_tests.FORTYTWO
-def Lean_tests.add_two_numbers (x : usize) (y : usize) : Result usize := do
+def Lean_tests.add_two_numbers (x : usize) (y : usize) : Result usize := do
(← x +? y)
-def Lean_tests.letBinding (x : usize) (y : usize) : Result usize := do
- let useless : Rust_primitives.Hax.Tuple0 ←
- (pure Rust_primitives.Hax.Tuple0.mk);
+def Lean_tests.letBinding (x : usize) (y : usize) : Result usize := do
+ let useless : Rust_primitives.Hax.Tuple0 ← (pure
+ Rust_primitives.Hax.Tuple0.mk);
let result1 : usize ← (pure (← x +? y));
let result2 : usize ← (pure (← result1 +? (2 : usize)));
(← result2 +? (1 : usize))
-def Lean_tests.closure (_ : Rust_primitives.Hax.Tuple0) : Result i32 := do
+def Lean_tests.closure (_ : Rust_primitives.Hax.Tuple0) : Result i32 := do
let x : i32 ← (pure (41 : i32));
- let f1 : i32 -> Result i32 ←
- (pure (fun (y : i32) => (do (← y +? x) : Result i32)));
- let f2 : i32 -> i32 -> Result i32 ←
- (pure (fun (y : i32) (z : i32) => (do (← (← y +? x) +? z) : Result i32)));
- let res1 : i32 ←
- (pure
+ let f1 : i32 -> Result i32 ← (pure
+ (fun (y : i32) => (do (← y +? x) : Result i32)));
+ let f2 : i32 -> i32 -> Result i32 ← (pure
+ (fun (y : i32) (z : i32) => (do (← (← y +? x) +? z) : Result i32)));
+ let res1 : i32 ← (pure
(← Core.Ops.Function.Fn.call f1 (Rust_primitives.Hax.Tuple1.mk (1 : i32))));
- let res2 : i32 ←
- (pure
+ let res2 : i32 ← (pure
(← Core.Ops.Function.Fn.call
- f2
- (Rust_primitives.Hax.Tuple2.mk (2 : i32) (3 : i32))));
+ f2
+ (Rust_primitives.Hax.Tuple2.mk (2 : i32) (3 : i32))));
(← res1 +? res2)
@[spec]
-def Lean_tests.test_before_verbatime_single_line (x : u8) : Result u8 := do 42
+def Lean_tests.test_before_verbatime_single_line (x : u8) : Result u8 := do
+ (42 : u8)
def multiline : Unit := ()
-def Lean_tests.test_before_verbatim_multi_line (x : u8) : Result u8 := do 32
+def Lean_tests.test_before_verbatim_multi_line (x : u8) : Result u8 := do
+ (32 : u8)
-def Lean_tests.binop_resugarings (x : u32) : Result u32 := do
+def Lean_tests.binop_resugarings (x : u32) : Result u32 := do
let add : u32 ← (pure (← x +? (1 : u32)));
let sub : u32 ← (pure (← add -? (2 : u32)));
let mul : u32 ← (pure (← sub *? (3 : u32)));
diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs
index 5aa8e9d1b..5dd030221 100644
--- a/tests/lean-tests/src/lib.rs
+++ b/tests/lean-tests/src/lib.rs
@@ -3,6 +3,7 @@
pub mod enums;
pub mod structs;
+pub mod traits;
const FORTYTWO: usize = 42;
const MINUS_FORTYTWO: isize = -42;
diff --git a/tests/lean-tests/src/structs.rs b/tests/lean-tests/src/structs.rs
index 7accefbec..1ec171dd0 100644
--- a/tests/lean-tests/src/structs.rs
+++ b/tests/lean-tests/src/structs.rs
@@ -143,3 +143,22 @@ fn normal_structs() -> () {
} => {}
}
}
+
+mod miscellaneous {
+ struct S {
+ f: i32,
+ }
+
+ fn test_tuples() -> (i32, i32) {
+ let lit = 1;
+ let constr = S { f: 42 };
+ let proj = constr.f;
+ let ite = if true {
+ (1, 2)
+ } else {
+ let z = 1 + 2;
+ (z, z)
+ };
+ (1, 2)
+ }
+}
diff --git a/tests/lean-tests/src/traits.rs b/tests/lean-tests/src/traits.rs
new file mode 100644
index 000000000..a77e78e19
--- /dev/null
+++ b/tests/lean-tests/src/traits.rs
@@ -0,0 +1,200 @@
+// Tests on traits
+#![allow(dead_code)]
+#![allow(unused_variables)]
+
+// Simple trait
+mod basic {
+ trait T1 {
+ fn f1(&self) -> usize;
+ fn f2(&self, other: &Self) -> usize;
+ }
+
+ // Simple Impl
+ struct S;
+
+ impl T1 for S {
+ fn f1(&self) -> usize {
+ 42
+ }
+
+ fn f2(&self, other: &Self) -> usize {
+ 43
+ }
+ }
+
+ // Simple ImplExpr
+ fn f(x: T) -> usize {
+ x.f1() + x.f2(&x)
+ }
+}
+
+// Bounds on parameters and on self
+mod bounds {
+ trait T1 {
+ fn f1(&self) -> usize;
+ }
+ trait T2 {
+ fn f2(&self) -> usize;
+ }
+
+ trait Test: T2 {
+ fn f_test(&self, x: &T) -> usize;
+ }
+
+ struct S1;
+ impl T1 for S1 {
+ fn f1(&self) -> usize {
+ 0
+ }
+ }
+
+ struct S2;
+ impl T2 for S2 {
+ fn f2(&self) -> usize {
+ 1
+ }
+ }
+
+ impl Test for S2 {
+ fn f_test(&self, x: &S1) -> usize {
+ x.f1() + self.f2() + 1
+ }
+ }
+
+ fn test(x1: S1, x2: S2) -> usize {
+ x2.f_test(&x1) + x1.f1()
+ }
+}
+
+mod associated_types {
+ trait T1 {
+ type T;
+ fn f(&self, x: Self::T) -> Self::T;
+ }
+
+ trait T2 {
+ type T: T1;
+ fn f(&self, x: Self::T) -> usize;
+ }
+
+ trait Foo {}
+ trait Bar {}
+
+ trait T3 {
+ type T: Bar;
+ type Tp: Foo;
+ fn f(&self, x: Self::T, y: Self::Tp) -> usize;
+ }
+
+ struct S {}
+ impl T1 for S {
+ type T = i32;
+
+ fn f(&self, x: Self::T) -> Self::T {
+ 2121
+ }
+ }
+ impl T2 for S {
+ type T = S;
+
+ fn f(&self, x: Self::T) -> usize {
+ 21
+ }
+ }
+
+ impl Bar for i16 {}
+ impl Foo for (u32, A) {}
+
+ // impl T3 for S {
+ // type T = i16;
+
+ // type Tp = (u32, A);
+
+ // fn f(&self, x: Self::T, y: Self::Tp) -> usize {
+ // 12
+ // }
+ // }
+}
+
+mod overlapping_methods {
+
+ trait T1 {
+ fn f(&self) -> usize;
+ }
+ trait T2 {
+ fn f(&self) -> usize;
+ }
+ trait T3 {
+ fn f(&self) -> usize;
+ }
+ impl T1 for u32 {
+ fn f(&self) -> usize {
+ 0
+ }
+ }
+ impl T2 for u32 {
+ fn f(&self) -> usize {
+ 1
+ }
+ }
+ impl T3 for u32 {
+ fn f(&self) -> usize {
+ 2
+ }
+ }
+ fn test() -> usize {
+ let x: u32 = 9;
+ T1::f(&x) + T2::f(&x) + T3::f(&x)
+ }
+}
+
+mod inheritance {
+ trait T1 {
+ fn f1(&self) -> usize;
+ }
+ trait T2 {
+ fn f2(&self) -> usize;
+ }
+ trait T3: T2 + T1 {
+ fn f3(&self) -> usize;
+ }
+ trait Tp1 {
+ fn f1(&self) -> usize;
+ }
+ trait Tp2: Tp1 + T3 {
+ fn fp2(&self) -> usize;
+ }
+
+ struct S {}
+ impl T1 for S {
+ fn f1(&self) -> usize {
+ 1
+ }
+ }
+ impl T2 for S {
+ fn f2(&self) -> usize {
+ 2
+ }
+ }
+ impl T3 for S {
+ fn f3(&self) -> usize {
+ 3
+ }
+ }
+
+ impl Tp1 for S {
+ fn f1(&self) -> usize {
+ 10
+ }
+ }
+
+ impl Tp2 for S {
+ fn fp2(&self) -> usize {
+ Tp1::f1(self) + T1::f1(self) + T2::f2(self) + T3::f3(self)
+ }
+ }
+ fn test() -> usize {
+ let s = S {};
+ s.f3() + 1
+ }
+}