diff --git a/CHANGELOG.md b/CHANGELOG.md index dc4d8cbff..1477930c2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -37,6 +37,7 @@ Changes to the Lean backend: - Add support for binding subpatterns in match constructs (#1790) - Add error when using patterns in function parameters (#1792) - Add support for constant parameters to functions and traits (#1797) + - Add support for associated types with equality constraints (#1806) Miscellaneous: - Reserve extraction folder for auto-generated files in Lean examples (#1754) diff --git a/rust-engine/src/ast.rs b/rust-engine/src/ast.rs index 40c9dc358..bbd77281a 100644 --- a/rust-engine/src/ast.rs +++ b/rust-engine/src/ast.rs @@ -1452,6 +1452,23 @@ pub struct Module { pub meta: Metadata, } +impl Generics { + /// Returns Iterator over all type constraints (`GenericConstraint::Type`) + pub fn type_constraints(&self) -> impl Iterator { + self.constraints.iter().filter_map(|c| match c { + GenericConstraint::Type(impl_id) => Some(impl_id), + _ => None, + }) + } + /// Returns Iterator over all projection constraints (`GenericConstraint::Projection`) + pub fn projection_constraints(&self) -> impl Iterator { + self.constraints.iter().filter_map(|c| match c { + GenericConstraint::Projection(pp) => Some(pp), + _ => None, + }) + } +} + /// Traits for utilities on AST data types pub mod traits { use super::*; diff --git a/rust-engine/src/backends/lean.rs b/rust-engine/src/backends/lean.rs index 666b07520..0e98874f5 100644 --- a/rust-engine/src/backends/lean.rs +++ b/rust-engine/src/backends/lean.rs @@ -36,6 +36,7 @@ const INDENT: isize = 2; static RESERVED_KEYWORDS: LazyLock> = LazyLock::new(|| { HashSet::from_iter( [ + // reserved for Lean: "end", "def", "abbrev", @@ -44,6 +45,9 @@ static RESERVED_KEYWORDS: LazyLock> = LazyLock::new(|| { "inductive", "structure", "from", + // reserved for hax encoding: + "associatedTypes", + "AssociatedTypes", ] .iter() .map(|s| s.to_string()), @@ -183,7 +187,10 @@ impl LeanPrinter { 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()) { + } else if RESERVED_KEYWORDS.contains(&id) + || id.starts_with("trait_constr_") + || id.starts_with(|c: char| c.is_ascii_digit()) + { format!("_{id}") } else { id @@ -333,7 +340,44 @@ const _: () = { associated_type_name: &String, constraint: &ImplIdent, ) -> String { - format!("_constr_{}_{}", associated_type_name, constraint.name) + format!("trait_constr_{}_{}", associated_type_name, constraint.name) + } + + /// Renders a named argument for associated types with equality constraints + /// (aka projections). If there are no equality constraints, returns None. + fn associated_type_projections( + &self, + impl_ident: &ImplIdent, + projections: Vec>, + ) -> Option> { + (!projections.is_empty()).then_some( + docs![ + "(associatedTypes := {", + line!(), + docs![ + "show", + line!(), + impl_ident.goal.trait_, + ".AssociatedTypes", + concat!(impl_ident.goal.args.iter().map(|arg| docs![line!(), arg])), + ] + .group() + .nest(INDENT), + line!(), + reflow!("by infer_instance"), + line!(), + docs![ + "with", + line!(), + intersperse!(projections, docs![",", line!()]), + ] + .group() + .nest(INDENT), + "})" + ] + .group() + .nest(INDENT), + ) } /// Turns an expression of type `RustM T` into one of type `T` (out of the monad), providing @@ -412,33 +456,56 @@ set_option linter.unusedVariables false } /// Render generics, adding a space after each parameter - fn generics( - &self, - Generics { - params, - constraints, - }: &Generics, - ) -> DocBuilder { + fn generics(&self, generics: &Generics) -> DocBuilder { docs![ - zip_right!(params, line!()), + zip_right!(&generics.params, line!()), zip_right!( - constraints - .iter() - .map(|constraint| docs![constraint].brackets()), + generics.type_constraints().map(|impl_ident| { + let projections = generics.projection_constraints() + .map(|p| + if let ImplExprKind::LocalBound { id } = &*p.impl_.kind && *id == impl_ident.name { + docs![p] + } else { + emit_error!(issue 1710, "Unsupported variant of associated type projection") + } + ) + .collect::>(); + docs![ + docs![ + impl_ident.goal.trait_, + ".AssociatedTypes", + concat!( + impl_ident.goal.args.iter().map(|arg| docs![line!(), arg]) + ) + ] + .brackets() + .group() + .nest(INDENT), + line!(), + docs![ + impl_ident.goal.trait_, + concat!( + impl_ident.goal.args.iter().map(|arg| docs![line!(), arg]) + ), + line!(), + self.associated_type_projections(impl_ident, projections) + ] + .brackets() + .nest(INDENT) + .group() + ] + .group() + }), line!() ), ] .group() } - fn generic_constraint(&self, generic_constraint: &GenericConstraint) -> DocBuilder { - match generic_constraint { - GenericConstraint::Type(impl_ident) => docs![impl_ident], - GenericConstraint::Projection(_) => { - emit_error!(issue 1710, "Unsupported equality constraints on associated types") - } - GenericConstraint::Lifetime(_) => unreachable_by_invariant!(Drop_references), - } + fn generic_constraint(&self, _: &GenericConstraint) -> DocBuilder { + unreachable!( + "Generic constraints are rendered inline because they must contain associated type projections." + ) } fn generic_param(&self, generic_param: &GenericParam) -> DocBuilder { @@ -790,9 +857,16 @@ set_option linter.unusedVariables false TyKind::AssociatedType { impl_, item } => { let kind = impl_.kind(); match &kind { - ImplExprKind::Self_ => docs![self.render_last(item)], + ImplExprKind::Self_ => docs!["associatedTypes.", self.render_last(item)], + ImplExprKind::LocalBound { .. } => docs![ + item, + concat!(impl_.goal.args.iter().map(|arg| docs![line!(), arg])), + ] + .parens() + .group() + .nest(INDENT), _ => { - emit_error!(issue 1710, "Unsupported non trait-local associated types") + emit_error!(issue 1710, "Unsupported variant of associated type") } } } @@ -1004,49 +1078,163 @@ set_option linter.unusedVariables false generics, items, } => { - // Type parameters are also parameters of the class, but constraints are fields of the class + let generic_types = generics.type_constraints().collect::>(); + if generic_types.len() < generics.constraints.len() { + emit_error!(issue 1710, "Unsupported equality constraints on associated types") + } docs![ + // A trait is encoded as two Lean type classes: one holding the associated types, + // and one holding all other fields. + // This is the type class holding the associated types: docs![ - docs![reflow!("class "), name], - (!generics.params.is_empty()).then_some(docs![ - line!(), - intersperse!(&generics.params, line!()).group() - ]), - line!(), - "where" + docs![ + docs![reflow!("class "), name, ".AssociatedTypes"], + (!generics.params.is_empty()).then_some(docs![ + softline!(), + intersperse!(&generics.params, softline!()).group() + ]), + softline!(), + "where" + ] + .group(), + zip_left!( + hardline!(), + generic_types.iter().map(|impl_ident| docs![ + self.fresh_constraint_name(&self.render_last(name), impl_ident), + " :", + line!(), + &impl_ident.goal.trait_, + ".AssociatedTypes", + line!(), + intersperse!(&impl_ident.goal.args, line!()) + ] + .group() + .brackets()) + ), + zip_left!( + hardline!(), + items + .iter() + .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) }) + ), ] - .group(), - hardline!(), - (!generics.constraints.is_empty()).then_some(docs![zip_right!( - generics - .constraints + .nest(INDENT), + // We add the `[instance]` attribute to the contained constraints to make + // them available for type inference: + zip_left!( + docs![hardline!(), hardline!()], + generic_types.iter().map(|impl_ident| docs![ + "attribute [instance]", + line!(), + name, + ".AssociatedTypes.", + self.fresh_constraint_name(&self.render_last(name), impl_ident), + ] + .group() + .nest(INDENT)) + ), + // When referencing associated types, we would like to refer to them as + // `TraitName.TypeName` instead of `TraitName.AssociatedTypes.TypeName`: + zip_left!( + docs![hardline!(), hardline!()], + items .iter() - .map(|constraint: &GenericConstraint| { - match constraint { - GenericConstraint::Type(tc_constraint) => docs![ - self.fresh_constraint_name(&self.render_last(name), tc_constraint), - " :", - line!(), - constraint + .filter(|item| { matches!(item.kind, TraitItemKind::Type(_)) }) + .map(|item| { + docs![ + "abbrev ", + name, + ".", + self.render_last(&item.ident), + " :=", + line!(), + name, + ".AssociatedTypes", + ".", + self.render_last(&item.ident), + ] + .nest(INDENT) + }) + ), + hardline!(), + hardline!(), + // This is the type class holding all other fields: + docs![ + docs![ + docs![reflow!("class "), name], + line!(), + docs![ + // Type parameters are also parameters of the class, but constraints are fields of the class + intersperse!(&generics.params, line!()), + line!(), + // The collection of associated types is an extra parameter so that we can encode + // equality constraints on associated types. + docs![ + reflow!("associatedTypes :"), + softline!(), + "outParam", + softline!(), + docs![ + name, + ".AssociatedTypes", + softline!(), + intersperse!(&generics.params, softline!()), ] - .group() - .brackets(), - GenericConstraint::Lifetime(_) => unreachable_by_invariant!(Drop_references), - GenericConstraint::Projection(_) => emit_error!(issue 1710, "Unsupported equality constraints on associated types"), - } - }), - 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!() - ) + .parens() + .nest(INDENT) + ] + .brackets() + .nest(INDENT) + ] + .group(), + line!(), + "where" + ] + .group(), + // Lean's `extends` does not work for us because one cannot implement + // different functions of the same name on the super- and on the + // subclass. So we treat supertraits like any other constraint: + zip_left!( + hardline!(), + generic_types.iter().map(|impl_ident| docs![ + self.fresh_constraint_name(&self.render_last(name), impl_ident), + " :", + line!(), + impl_ident.goal.trait_, + concat!( + impl_ident.goal.args.iter().map(|arg| docs![line!(), arg]) + ) + ] + .group() + .brackets()) + ), + zip_left!( + hardline!(), + 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() || + // Associated types are encoded in a separate type class. + matches!(item.kind, TraitItemKind::Type(_)) + )}) + ), + ] + .nest(INDENT), + // We add the `[instance]` attribute to the contained constraints to make + // them available for type inference: + zip_left!( + docs![hardline!(), hardline!()], + generic_types.iter().map(|impl_ident| docs![ + "attribute [instance]", + line!(), + name, + ".", + self.fresh_constraint_name(&self.render_last(name), impl_ident), + ] + .group() + .nest(INDENT)) + ), ] - .nest(INDENT) } ItemKind::Impl { generics, @@ -1056,6 +1244,40 @@ set_option linter.unusedVariables false parent_bounds: _, safety: _, } => docs![ + // An impl is encoded as two Lean instances: + // One for the associated types... + docs![ + docs![ + reflow!("instance "), + ident, + ".AssociatedTypes", + line!(), + generics, + ":" + ] + .group(), + line!(), + docs![ + trait_, + ".AssociatedTypes", + concat!(args.iter().map(|gv| docs![line!(), gv])) + ] + .group(), + line!(), + "where", + ] + .group() + .nest(INDENT), + docs![zip_left!( + hardline!(), + items + .iter() + .filter(|item| { matches!(item.kind, ImplItemKind::Type { .. }) }) + )] + .nest(INDENT), + hardline!(), + hardline!(), + // ...and one for all other fields: docs![ docs![reflow!("instance "), ident, line!(), generics, ":"].group(), line!(), @@ -1065,17 +1287,18 @@ set_option linter.unusedVariables false ] .group() .nest(INDENT), - docs![ + docs![zip_left!( hardline!(), - intersperse!( - items.iter().filter(|item| { + 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!() - ) - ] + item.ident.is_precondition() || item.ident.is_postcondition() || + // Associated types are encoded into a separate type class + matches!(item.kind, ImplItemKind::Type { .. }) + ) + }) + )] .nest(INDENT), ], ItemKind::Resugared(resugared_item_kind) => match resugared_item_kind { @@ -1125,23 +1348,10 @@ set_option linter.unusedVariables false .group() .nest(INDENT) } - TraitItemKind::Type(constraints) => { - docs![ - name.clone(), - reflow!(" : Type"), - concat!(constraints.iter().map(|c| docs![ - hardline!(), - docs![ - self.fresh_constraint_name(&name, c), - reflow!(" :"), - line!(), - &c.goal - ] - .group() - .nest(INDENT) - .brackets() - ])) - ] + TraitItemKind::Type(_) => { + docs![&self.render_last(ident), softline!(), ":", line!(), "Type"] + .group() + .nest(INDENT) } TraitItemKind::Default { params, body } => docs![ docs![ @@ -1200,15 +1410,16 @@ set_option linter.unusedVariables false } } - fn impl_ident(&self, ImplIdent { goal, name: _ }: &ImplIdent) -> DocBuilder { - docs![goal] + fn impl_ident(&self, ImplIdent { .. }: &ImplIdent) -> DocBuilder { + unreachable!( + "`ImplIdent`s are rendered inline because we have multiple variants of how they must be rendered." + ) } - fn trait_goal(&self, TraitGoal { trait_, args }: &TraitGoal) -> DocBuilder { - docs![trait_, concat!(args.iter().map(|arg| docs![line!(), arg]))] - .parens() - .nest(INDENT) - .group() + fn trait_goal(&self, TraitGoal { .. }: &TraitGoal) -> DocBuilder { + unreachable!( + "`TraitGoal`s are rendered inline because we have multiple variants of how they must be rendered." + ) } fn variant( @@ -1327,9 +1538,17 @@ set_option linter.unusedVariables false fn projection_predicate( &self, - _projection_predicate: &ProjectionPredicate, + projection_predicate: &ProjectionPredicate, ) -> DocBuilder { - emit_error!(issue 1710, "Projection predicate (type equalities on associated types) are unsupported") + docs![ + self.render_last(&projection_predicate.assoc_item), + softline!(), + ":=", + line!(), + projection_predicate.ty, + ] + .group() + .nest(INDENT) } fn error_node(&self, _error_node: &ErrorNode) -> DocBuilder { 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 0767dcd26..91aafb817 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 @@ -46,11 +46,14 @@ inductive Lean_core_models.Result.E1 : Type | C2 : u32 -> Lean_core_models.Result.E1 +instance Lean_core_models.Result.Impl.AssociatedTypes : + Core.Clone.Clone.AssociatedTypes Lean_core_models.Result.E1 + where + 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 @@ -142,6 +145,10 @@ inductive Lean_core_models.Option.E : Type | C : u32 -> Lean_core_models.Option.E +instance Lean_core_models.Option.Impl.AssociatedTypes : + Core.Default.Default.AssociatedTypes Lean_core_models.Option.S + where + instance Lean_core_models.Option.Impl : Core.Default.Default Lean_core_models.Option.S where @@ -235,6 +242,10 @@ def Lean_core_models.Option.test structure Lean_core_models.Default.Structs.S where f1 : usize +instance Lean_core_models.Default.Structs.Impl.AssociatedTypes : + Core.Default.Default.AssociatedTypes Lean_core_models.Default.Structs.S + where + instance Lean_core_models.Default.Structs.Impl : Core.Default.Default Lean_core_models.Default.Structs.S where @@ -252,8 +263,17 @@ inductive Lean_core_models.Default.Enums.E (T : Type) : Type | C2 : T -> Lean_core_models.Default.Enums.E (T : Type) +instance Lean_core_models.Default.Enums.Impl.AssociatedTypes + (T : Type) + [Core.Default.Default.AssociatedTypes T] [Core.Default.Default T ] + : + Core.Default.Default.AssociatedTypes (Lean_core_models.Default.Enums.E T) + where + instance Lean_core_models.Default.Enums.Impl - (T : Type) [(Core.Default.Default T)] : + (T : Type) + [Core.Default.Default.AssociatedTypes T] [Core.Default.Default T ] + : Core.Default.Default (Lean_core_models.Default.Enums.E T) where default (_ : Rust_primitives.Hax.Tuple0) := do 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 620a9da45..1fe34d048 100644 --- a/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap +++ b/test-harness/src/snapshots/toolchain__lean-tests into-lean.snap @@ -91,14 +91,26 @@ open Std.Tactic set_option mvcgen.warning false set_option linter.unusedVariables false +class Lean_tests.Traits.Trait_level_args.T1.AssociatedTypes (Self : Type) (A : + Type) (B : Type) where + class Lean_tests.Traits.Trait_level_args.T1 - (Self : Type) (A : Type) (B : Type) + (Self : Type) + (A : Type) + (B : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Trait_level_args.T1.AssociatedTypes (Self : Type) (A : + Type) (B : Type))] where f1 (C : Type) (D : Type) : (Self -> RustM Rust_primitives.Hax.Tuple0) f2 (C : Type) (D : Type) : (Self -> A -> RustM Rust_primitives.Hax.Tuple0) f3 (C : Type) (D : Type) : (Self -> A -> B -> RustM Rust_primitives.Hax.Tuple0) +instance Lean_tests.Traits.Trait_level_args.Impl.AssociatedTypes : + Lean_tests.Traits.Trait_level_args.T1.AssociatedTypes usize u32 u64 + where + instance Lean_tests.Traits.Trait_level_args.Impl : Lean_tests.Traits.Trait_level_args.T1 usize u32 u64 where @@ -142,7 +154,8 @@ def Lean_tests.Traits.Trait_level_args.test (C : Type) (D : Type) (U : Type) - [(Lean_tests.Traits.Trait_level_args.T1 U A B)] + [Lean_tests.Traits.Trait_level_args.T1.AssociatedTypes U A B] + [Lean_tests.Traits.Trait_level_args.T1 U A B ] (x : U) (a : A) (b : B) @@ -153,25 +166,58 @@ def Lean_tests.Traits.Trait_level_args.test let _ ← (Lean_tests.Traits.Trait_level_args.T1.f3 C D x a b); (pure Rust_primitives.Hax.Tuple0.mk) -class Lean_tests.Traits.Overlapping_methods.T1 (Self : Type) where +class Lean_tests.Traits.Overlapping_methods.T1.AssociatedTypes (Self : Type) + where + +class Lean_tests.Traits.Overlapping_methods.T1 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Overlapping_methods.T1.AssociatedTypes (Self : Type))] + where f : (Self -> RustM usize) -class Lean_tests.Traits.Overlapping_methods.T2 (Self : Type) where +class Lean_tests.Traits.Overlapping_methods.T2.AssociatedTypes (Self : Type) + where + +class Lean_tests.Traits.Overlapping_methods.T2 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Overlapping_methods.T2.AssociatedTypes (Self : Type))] + where f : (Self -> RustM usize) -class Lean_tests.Traits.Overlapping_methods.T3 (Self : Type) where +class Lean_tests.Traits.Overlapping_methods.T3.AssociatedTypes (Self : Type) + where + +class Lean_tests.Traits.Overlapping_methods.T3 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Overlapping_methods.T3.AssociatedTypes (Self : Type))] + where f : (Self -> RustM usize) +instance Lean_tests.Traits.Overlapping_methods.Impl.AssociatedTypes : + Lean_tests.Traits.Overlapping_methods.T1.AssociatedTypes u32 + where + instance Lean_tests.Traits.Overlapping_methods.Impl : Lean_tests.Traits.Overlapping_methods.T1 u32 where f (self : u32) := do (pure (0 : usize)) +instance Lean_tests.Traits.Overlapping_methods.Impl_1.AssociatedTypes : + Lean_tests.Traits.Overlapping_methods.T2.AssociatedTypes u32 + where + 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.AssociatedTypes : + Lean_tests.Traits.Overlapping_methods.T3.AssociatedTypes u32 + where + instance Lean_tests.Traits.Overlapping_methods.Impl_2 : Lean_tests.Traits.Overlapping_methods.T3 u32 where @@ -186,48 +232,127 @@ def Lean_tests.Traits.Overlapping_methods.test +? (← (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 +class Lean_tests.Traits.Inheritance.T1.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Inheritance.T1 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Inheritance.T1.AssociatedTypes + (Self : Type))] + where f1 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.T2 (Self : Type) where +class Lean_tests.Traits.Inheritance.T2.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Inheritance.T2 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Inheritance.T2.AssociatedTypes + (Self : Type))] + where f2 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.T3 (Self : Type) where - [_constr_T3_i0 : (Lean_tests.Traits.Inheritance.T2 Self)] - [_constr_T3_i1 : (Lean_tests.Traits.Inheritance.T1 Self)] +class Lean_tests.Traits.Inheritance.T3.AssociatedTypes (Self : Type) where + [trait_constr_T3_i0 : Lean_tests.Traits.Inheritance.T2.AssociatedTypes Self] + [trait_constr_T3_i1 : Lean_tests.Traits.Inheritance.T1.AssociatedTypes Self] + +attribute [instance] + Lean_tests.Traits.Inheritance.T3.AssociatedTypes.trait_constr_T3_i0 + +attribute [instance] + Lean_tests.Traits.Inheritance.T3.AssociatedTypes.trait_constr_T3_i1 + +class Lean_tests.Traits.Inheritance.T3 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Inheritance.T3.AssociatedTypes + (Self : Type))] + where + [trait_constr_T3_i0 : Lean_tests.Traits.Inheritance.T2 Self] + [trait_constr_T3_i1 : Lean_tests.Traits.Inheritance.T1 Self] f3 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.Tp1 (Self : Type) where +attribute [instance] Lean_tests.Traits.Inheritance.T3.trait_constr_T3_i0 + +attribute [instance] Lean_tests.Traits.Inheritance.T3.trait_constr_T3_i1 + +class Lean_tests.Traits.Inheritance.Tp1.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Inheritance.Tp1 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Inheritance.Tp1.AssociatedTypes + (Self : Type))] + where f1 : (Self -> RustM usize) -class Lean_tests.Traits.Inheritance.Tp2 (Self : Type) where - [_constr_Tp2_i0 : (Lean_tests.Traits.Inheritance.Tp1 Self)] - [_constr_Tp2_i1 : (Lean_tests.Traits.Inheritance.T3 Self)] +class Lean_tests.Traits.Inheritance.Tp2.AssociatedTypes (Self : Type) where + [trait_constr_Tp2_i0 : Lean_tests.Traits.Inheritance.Tp1.AssociatedTypes Self] + [trait_constr_Tp2_i1 : Lean_tests.Traits.Inheritance.T3.AssociatedTypes Self] + +attribute [instance] + Lean_tests.Traits.Inheritance.Tp2.AssociatedTypes.trait_constr_Tp2_i0 + +attribute [instance] + Lean_tests.Traits.Inheritance.Tp2.AssociatedTypes.trait_constr_Tp2_i1 + +class Lean_tests.Traits.Inheritance.Tp2 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Inheritance.Tp2.AssociatedTypes + (Self : Type))] + where + [trait_constr_Tp2_i0 : Lean_tests.Traits.Inheritance.Tp1 Self] + [trait_constr_Tp2_i1 : Lean_tests.Traits.Inheritance.T3 Self] fp2 : (Self -> RustM usize) +attribute [instance] Lean_tests.Traits.Inheritance.Tp2.trait_constr_Tp2_i0 + +attribute [instance] Lean_tests.Traits.Inheritance.Tp2.trait_constr_Tp2_i1 + structure Lean_tests.Traits.Inheritance.S where +instance Lean_tests.Traits.Inheritance.Impl.AssociatedTypes : + Lean_tests.Traits.Inheritance.T1.AssociatedTypes + 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 (pure (1 : usize)) +instance Lean_tests.Traits.Inheritance.Impl_1.AssociatedTypes : + Lean_tests.Traits.Inheritance.T2.AssociatedTypes + Lean_tests.Traits.Inheritance.S + where + 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 Lean_tests.Traits.Inheritance.Impl_2.AssociatedTypes : + Lean_tests.Traits.Inheritance.T3.AssociatedTypes + Lean_tests.Traits.Inheritance.S + where + 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 Lean_tests.Traits.Inheritance.Impl_3.AssociatedTypes : + Lean_tests.Traits.Inheritance.Tp1.AssociatedTypes + Lean_tests.Traits.Inheritance.S + where + 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 Lean_tests.Traits.Inheritance.Impl_4.AssociatedTypes : + Lean_tests.Traits.Inheritance.Tp2.AssociatedTypes + Lean_tests.Traits.Inheritance.S + where + instance Lean_tests.Traits.Inheritance.Impl_4 : Lean_tests.Traits.Inheritance.Tp2 Lean_tests.Traits.Inheritance.S where @@ -244,26 +369,46 @@ def Lean_tests.Traits.Inheritance.test let s : Lean_tests.Traits.Inheritance.S := Lean_tests.Traits.Inheritance.S.mk; ((← (Lean_tests.Traits.Inheritance.T3.f3 s)) +? (1 : usize)) -class Lean_tests.Traits.Default.Easy (Self : Type) where +class Lean_tests.Traits.Default.Easy.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Default.Easy + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Default.Easy.AssociatedTypes + (Self : Type))] + where dft (self : Self) : RustM usize := do (pure (32 : usize)) +instance Lean_tests.Traits.Default.Impl.AssociatedTypes : + Lean_tests.Traits.Default.Easy.AssociatedTypes usize + where + instance Lean_tests.Traits.Default.Impl : Lean_tests.Traits.Default.Easy usize where dft (self : usize) := do (self +? (1 : usize)) +instance Lean_tests.Traits.Default.Impl_1.AssociatedTypes : + Lean_tests.Traits.Default.Easy.AssociatedTypes u32 + where + instance Lean_tests.Traits.Default.Impl_1 : Lean_tests.Traits.Default.Easy u32 where +class Lean_tests.Traits.Default.T1.AssociatedTypes (Self : Type) where -class Lean_tests.Traits.Default.T1 (Self : Type) where +class Lean_tests.Traits.Default.T1 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Default.T1.AssociatedTypes + (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) [(Lean_tests.Traits.Default.Easy A)] (self : Self) - (x : A) - : RustM usize + f4 (A : Type) + [Lean_tests.Traits.Default.Easy.AssociatedTypes A] + [Lean_tests.Traits.Default.Easy A ] + (self : Self) (x : A) : RustM usize := do ((← (Lean_tests.Traits.Default.Easy.dft x)) +? (1 : usize)) @@ -271,6 +416,11 @@ structure Lean_tests.Traits.Default.S (A : Type) where _0 : usize _1 : A +instance Lean_tests.Traits.Default.Impl_2.AssociatedTypes : + Lean_tests.Traits.Default.T1.AssociatedTypes + (Lean_tests.Traits.Default.S usize) + where + instance Lean_tests.Traits.Default.Impl_2 : Lean_tests.Traits.Default.T1 (Lean_tests.Traits.Default.S usize) where @@ -280,6 +430,11 @@ instance Lean_tests.Traits.Default.Impl_2 : f2 (self : (Lean_tests.Traits.Default.S usize)) := do (pure (Lean_tests.Traits.Default.S._1 self)) +instance Lean_tests.Traits.Default.Impl_3.AssociatedTypes : + Lean_tests.Traits.Default.T1.AssociatedTypes + (Lean_tests.Traits.Default.S Bool) + where + instance Lean_tests.Traits.Default.Impl_3 : Lean_tests.Traits.Default.T1 (Lean_tests.Traits.Default.S Bool) where @@ -291,26 +446,67 @@ instance Lean_tests.Traits.Default.Impl_3 : f2 (self : (Lean_tests.Traits.Default.S Bool)) := do ((Lean_tests.Traits.Default.S._0 self) +? (1 : usize)) +instance Lean_tests.Traits.Default.Impl_4.AssociatedTypes : + Lean_tests.Traits.Default.T1.AssociatedTypes + (Lean_tests.Traits.Default.S Alloc.String.String) + where + instance Lean_tests.Traits.Default.Impl_4 : Lean_tests.Traits.Default.T1 (Lean_tests.Traits.Default.S Alloc.String.String) where f1 (self : (Lean_tests.Traits.Default.S Alloc.String.String)) := do (pure (0 : usize)) -class Lean_tests.Traits.Bounds.T1 (Self : Type) where +class Lean_tests.Traits.Bounds.T1.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Bounds.T1 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Bounds.T1.AssociatedTypes (Self + : Type))] + where f1 : (Self -> RustM usize) -class Lean_tests.Traits.Bounds.T2 (Self : Type) where +class Lean_tests.Traits.Bounds.T2.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Bounds.T2 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Bounds.T2.AssociatedTypes (Self + : Type))] + where f2 : (Self -> RustM usize) -class Lean_tests.Traits.Bounds.Test (Self : Type) (T : Type) where - [_constr_Test_i0 : (Lean_tests.Traits.Bounds.T2 Self)] - [_constr_Test_i1 : (Lean_tests.Traits.Bounds.T1 T)] +class Lean_tests.Traits.Bounds.Test.AssociatedTypes (Self : Type) (T : Type) + where + [trait_constr_Test_i0 : Lean_tests.Traits.Bounds.T2.AssociatedTypes Self] + [trait_constr_Test_i1 : Lean_tests.Traits.Bounds.T1.AssociatedTypes T] + +attribute [instance] + Lean_tests.Traits.Bounds.Test.AssociatedTypes.trait_constr_Test_i0 + +attribute [instance] + Lean_tests.Traits.Bounds.Test.AssociatedTypes.trait_constr_Test_i1 + +class Lean_tests.Traits.Bounds.Test + (Self : Type) + (T : Type) + [associatedTypes : outParam (Lean_tests.Traits.Bounds.Test.AssociatedTypes + (Self : Type) (T : Type))] + where + [trait_constr_Test_i0 : Lean_tests.Traits.Bounds.T2 Self] + [trait_constr_Test_i1 : Lean_tests.Traits.Bounds.T1 T] f_test : (Self -> T -> RustM usize) +attribute [instance] Lean_tests.Traits.Bounds.Test.trait_constr_Test_i0 + +attribute [instance] Lean_tests.Traits.Bounds.Test.trait_constr_Test_i1 + structure Lean_tests.Traits.Bounds.S1 where +instance Lean_tests.Traits.Bounds.Impl.AssociatedTypes : + Lean_tests.Traits.Bounds.T1.AssociatedTypes Lean_tests.Traits.Bounds.S1 + where + instance Lean_tests.Traits.Bounds.Impl : Lean_tests.Traits.Bounds.T1 Lean_tests.Traits.Bounds.S1 where @@ -319,11 +515,21 @@ instance Lean_tests.Traits.Bounds.Impl : structure Lean_tests.Traits.Bounds.S2 where +instance Lean_tests.Traits.Bounds.Impl_1.AssociatedTypes : + Lean_tests.Traits.Bounds.T2.AssociatedTypes 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 (pure (1 : usize)) +instance Lean_tests.Traits.Bounds.Impl_2.AssociatedTypes : + Lean_tests.Traits.Bounds.Test.AssociatedTypes + Lean_tests.Traits.Bounds.S2 + Lean_tests.Traits.Bounds.S1 + where + instance Lean_tests.Traits.Bounds.Impl_2 : Lean_tests.Traits.Bounds.Test Lean_tests.Traits.Bounds.S2 @@ -344,13 +550,23 @@ def Lean_tests.Traits.Bounds.test ((← (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 +class Lean_tests.Traits.Basic.T1.AssociatedTypes (Self : Type) where + +class Lean_tests.Traits.Basic.T1 + (Self : Type) + [associatedTypes : outParam (Lean_tests.Traits.Basic.T1.AssociatedTypes (Self + : Type))] + where f1 : (Self -> RustM usize) f2 : (Self -> Self -> RustM usize) structure Lean_tests.Traits.Basic.S where +instance Lean_tests.Traits.Basic.Impl.AssociatedTypes : + Lean_tests.Traits.Basic.T1.AssociatedTypes Lean_tests.Traits.Basic.S + where + instance Lean_tests.Traits.Basic.Impl : Lean_tests.Traits.Basic.T1 Lean_tests.Traits.Basic.S where @@ -361,59 +577,122 @@ instance Lean_tests.Traits.Basic.Impl : (pure (43 : usize)) def Lean_tests.Traits.Basic.f - (T : Type) [(Lean_tests.Traits.Basic.T1 T)] (x : T) + (T : Type) + [Lean_tests.Traits.Basic.T1.AssociatedTypes T] [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 Lean_tests.Traits.Associated_types.Foo (Self : Type) (T : Type) where +class Lean_tests.Traits.Associated_types.Foo.AssociatedTypes (Self : Type) (T : + Type) where +class Lean_tests.Traits.Associated_types.Foo + (Self : Type) + (T : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Associated_types.Foo.AssociatedTypes (Self : Type) (T : + Type))] + where -class Lean_tests.Traits.Associated_types.Bar (Self : Type) where +class Lean_tests.Traits.Associated_types.Bar.AssociatedTypes (Self : Type) where +class Lean_tests.Traits.Associated_types.Bar + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Associated_types.Bar.AssociatedTypes (Self : Type))] + where structure Lean_tests.Traits.Associated_types.S where +instance Lean_tests.Traits.Associated_types.Impl_2.AssociatedTypes : + Lean_tests.Traits.Associated_types.Bar.AssociatedTypes i16 + 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.AssociatedTypes (A : Type) : + Lean_tests.Traits.Associated_types.Foo.AssociatedTypes + (Rust_primitives.Hax.Tuple2 u32 A) + 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 +class Lean_tests.Traits.Associated_types.T1.AssociatedTypes (Self : Type) where T : Type - f : (Self -> T -> RustM T) -class Lean_tests.Traits.Associated_types.T3 (Self : Type) where +abbrev Lean_tests.Traits.Associated_types.T1.T := + Lean_tests.Traits.Associated_types.T1.AssociatedTypes.T + +class Lean_tests.Traits.Associated_types.T1 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Associated_types.T1.AssociatedTypes (Self : Type))] + where + f : (Self -> associatedTypes.T -> RustM associatedTypes.T) + +class Lean_tests.Traits.Associated_types.T3.AssociatedTypes (Self : Type) where T : Type - [_constr_T_i0 : (Lean_tests.Traits.Associated_types.Bar T)] Tp : Type - [_constr_Tp_i0 : (Lean_tests.Traits.Associated_types.Foo Tp T)] - f (A : Type) [(Lean_tests.Traits.Associated_types.Bar A)] : - (Self -> T -> Tp -> RustM usize) + +abbrev Lean_tests.Traits.Associated_types.T3.T := + Lean_tests.Traits.Associated_types.T3.AssociatedTypes.T + +abbrev Lean_tests.Traits.Associated_types.T3.Tp := + Lean_tests.Traits.Associated_types.T3.AssociatedTypes.Tp + +class Lean_tests.Traits.Associated_types.T3 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Associated_types.T3.AssociatedTypes (Self : Type))] + where + f (A : Type) + [Lean_tests.Traits.Associated_types.Bar.AssociatedTypes A] + [Lean_tests.Traits.Associated_types.Bar A ] + : + (Self -> associatedTypes.T -> associatedTypes.Tp -> RustM usize) + +instance Lean_tests.Traits.Associated_types.Impl.AssociatedTypes : + Lean_tests.Traits.Associated_types.T1.AssociatedTypes + Lean_tests.Traits.Associated_types.S + where + T := i32 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)) -class Lean_tests.Traits.Associated_types.T2 (Self : Type) where +class Lean_tests.Traits.Associated_types.T2.AssociatedTypes (Self : Type) where T : Type - [_constr_T_i0 : (Lean_tests.Traits.Associated_types.T1 T)] - f : (Self -> T -> RustM usize) + +abbrev Lean_tests.Traits.Associated_types.T2.T := + Lean_tests.Traits.Associated_types.T2.AssociatedTypes.T + +class Lean_tests.Traits.Associated_types.T2 + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Traits.Associated_types.T2.AssociatedTypes (Self : Type))] + where + f : (Self -> associatedTypes.T -> RustM usize) + +instance Lean_tests.Traits.Associated_types.Impl_1.AssociatedTypes : + Lean_tests.Traits.Associated_types.T2.AssociatedTypes + Lean_tests.Traits.Associated_types.S + where + T := Lean_tests.Traits.Associated_types.S 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 @@ -804,8 +1083,15 @@ def Lean_tests.Constants.Const_parameters.test (pure Rust_primitives.Hax.Tuple0.mk) -- Trait definition +class Lean_tests.Constants.Const_parameters.T.AssociatedTypes (Self : Type) + (N_TRAIT : usize) where + class Lean_tests.Constants.Const_parameters.T - (Self : Type) (N_TRAIT : usize) + (Self : Type) + (N_TRAIT : usize) + [associatedTypes : outParam + (Lean_tests.Constants.Const_parameters.T.AssociatedTypes (Self : Type) + (N_TRAIT : usize))] where f (N_FIELD : usize) : (Self -> RustM usize) @@ -813,6 +1099,13 @@ class Lean_tests.Constants.Const_parameters.T structure Lean_tests.Constants.Const_parameters.S (N : usize) where _0 : u32 +instance Lean_tests.Constants.Const_parameters.Impl.AssociatedTypes + (N_TRAIT : usize) : + Lean_tests.Constants.Const_parameters.T.AssociatedTypes + (Lean_tests.Constants.Const_parameters.S (N_TRAIT)) + (N_TRAIT) + where + instance Lean_tests.Constants.Const_parameters.Impl (N_TRAIT : usize) : Lean_tests.Constants.Const_parameters.T (Lean_tests.Constants.Const_parameters.S (N_TRAIT)) @@ -855,9 +1148,11 @@ in the application #guard_msgs in def Lean_tests.Constants.Const_parameters.test2 - (N2 : usize) (A : Type) [(Lean_tests.Constants.Const_parameters.T A (N2))] (x - : - A) + (N2 : usize) + (A : Type) + [Lean_tests.Constants.Const_parameters.T.AssociatedTypes A (N2)] + [Lean_tests.Constants.Const_parameters.T A (N2) ] + (x : A) : RustM usize := do let s : (Lean_tests.Constants.Const_parameters.S ((10 : usize))) := @@ -899,6 +1194,140 @@ def Lean_tests.Constants.test let z : u32 ← (Lean_tests.Constants.C4 -? Lean_tests.Constants.C3); (pure Rust_primitives.Hax.Tuple0.mk) +class Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes + (Self : Type) where + First : Type + Second : Type + +abbrev Lean_tests.Associated_types.Multiple_associated_types.Pair.First := + Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes.First + +abbrev Lean_tests.Associated_types.Multiple_associated_types.Pair.Second := + Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes.Second + +class Lean_tests.Associated_types.Multiple_associated_types.Pair + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes + (Self : Type))] + where + first : (Self -> RustM associatedTypes.First) + second : (Self -> RustM associatedTypes.Second) + +def Lean_tests.Associated_types.Multiple_associated_types.get_both + (P : Type) + [Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes P] + [Lean_tests.Associated_types.Multiple_associated_types.Pair P ] + (pair : P) + : RustM + (Rust_primitives.Hax.Tuple2 + (Lean_tests.Associated_types.Multiple_associated_types.Pair.First P) + (Lean_tests.Associated_types.Multiple_associated_types.Pair.Second P)) + := do + (pure (Rust_primitives.Hax.Tuple2.mk + (← (Lean_tests.Associated_types.Multiple_associated_types.Pair.first pair)) + (← (Lean_tests.Associated_types.Multiple_associated_types.Pair.second + pair)))) + +instance + Lean_tests.Associated_types.Multiple_associated_types.Impl.AssociatedTypes + : + Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes + (Rust_primitives.Hax.Tuple2 i32 Bool) + where + First := i32 + Second := Bool + +instance Lean_tests.Associated_types.Multiple_associated_types.Impl : + Lean_tests.Associated_types.Multiple_associated_types.Pair + (Rust_primitives.Hax.Tuple2 i32 Bool) + where + first (self : (Rust_primitives.Hax.Tuple2 i32 Bool)) := do + (pure (Rust_primitives.Hax.Tuple2._0 self)) + second (self : (Rust_primitives.Hax.Tuple2 i32 Bool)) := do + (pure (Rust_primitives.Hax.Tuple2._1 self)) + +def Lean_tests.Associated_types.Multiple_associated_types.b + (_ : Rust_primitives.Hax.Tuple0) + : RustM Rust_primitives.Hax.Tuple0 + := do + let pair : (Rust_primitives.Hax.Tuple2 i32 Bool) := + (Rust_primitives.Hax.Tuple2.mk (42 : i32) true); + let both : (Rust_primitives.Hax.Tuple2 i32 Bool) ← + (Lean_tests.Associated_types.Multiple_associated_types.get_both + (Rust_primitives.Hax.Tuple2 i32 Bool) pair); + (pure Rust_primitives.Hax.Tuple0.mk) + +def Lean_tests.Associated_types.Multiple_associated_types.get_first_as_i32 + (P : Type) + [Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes P] + [Lean_tests.Associated_types.Multiple_associated_types.Pair + P + (associatedTypes := { + show + Lean_tests.Associated_types.Multiple_associated_types.Pair.AssociatedTypes + P + by infer_instance + with First := i32})] + (pair : P) + : RustM i32 + := do + (Lean_tests.Associated_types.Multiple_associated_types.Pair.first pair) + +class Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes (Self : Type) + where + Item : Type + +abbrev Lean_tests.Associated_types.Basic.Iterable.Item := + Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes.Item + +class Lean_tests.Associated_types.Basic.Iterable + (Self : Type) + [associatedTypes : outParam + (Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes (Self : Type))] + where + first : (Self -> RustM associatedTypes.Item) + +def Lean_tests.Associated_types.Basic.just_the_first + (I : Type) + [Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes I] + [Lean_tests.Associated_types.Basic.Iterable I ] + (iter : I) + : RustM (Lean_tests.Associated_types.Basic.Iterable.Item I) + := do + (Lean_tests.Associated_types.Basic.Iterable.first iter) + +def Lean_tests.Associated_types.Basic.first_plus_1 + (I : Type) + [Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes I] + [Lean_tests.Associated_types.Basic.Iterable + I + (associatedTypes := { + show Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes I + by infer_instance + with Item := i32})] + (iter : I) + : RustM i32 + := do + ((← (Lean_tests.Associated_types.Basic.Iterable.first iter)) +? (1 : i32)) + +instance Lean_tests.Associated_types.Basic.Impl.AssociatedTypes : + Lean_tests.Associated_types.Basic.Iterable.AssociatedTypes Bool + where + Item := i32 + +instance Lean_tests.Associated_types.Basic.Impl : + Lean_tests.Associated_types.Basic.Iterable Bool + where + first (self : Bool) := do (pure (3 : i32)) + +def Lean_tests.Associated_types.Basic.a + (_ : Rust_primitives.Hax.Tuple0) + : RustM Rust_primitives.Hax.Tuple0 + := do + let _ ← (Lean_tests.Associated_types.Basic.first_plus_1 Bool true); + (pure Rust_primitives.Hax.Tuple0.mk) + def Lean_tests.FORTYTWO : usize := RustM.of_isOk (do (pure (42 : usize))) (by rfl) diff --git a/tests/lean-tests/src/associated_types.rs b/tests/lean-tests/src/associated_types.rs new file mode 100644 index 000000000..74d9da8dd --- /dev/null +++ b/tests/lean-tests/src/associated_types.rs @@ -0,0 +1,58 @@ +mod basic { + trait Iterable { + type Item; + fn first(&self) -> Self::Item; + } + + fn just_the_first(iter: I) -> I::Item { + iter.first() + } + + fn first_plus_1>(iter: I) -> i32 { + iter.first() + 1 + } + + impl Iterable for bool { + type Item = i32; + fn first(&self) -> i32 { + 3 + } + } + + fn a() { + first_plus_1(true); + } +} + +mod multiple_associated_types { + trait Pair { + type First; + type Second; + fn first(&self) -> Self::First; + fn second(&self) -> Self::Second; + } + + fn get_both(pair: P) -> (P::First, P::Second) { + (pair.first(), pair.second()) + } + + impl Pair for (i32, bool) { + type First = i32; + type Second = bool; + fn first(&self) -> i32 { + self.0 + } + fn second(&self) -> bool { + self.1 + } + } + + fn b() { + let pair = (42, true); + let both = get_both(pair); + } + + fn get_first_as_i32>(pair: P) -> i32 { + pair.first() + } +} diff --git a/tests/lean-tests/src/lib.rs b/tests/lean-tests/src/lib.rs index b705d5216..5346b28f3 100644 --- a/tests/lean-tests/src/lib.rs +++ b/tests/lean-tests/src/lib.rs @@ -1,6 +1,7 @@ #![allow(dead_code)] #![allow(unused_variables)] +pub mod associated_types; pub mod comments; pub mod constants; pub mod enums;