From 16fe74c43bb89a6ebedd16c6fb532a4149e351b8 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 16:43:23 -0500 Subject: [PATCH 1/3] Feat: Dafny-to-Rust code generator no longer emits r#_ but only _ in front of identifiers --- Source/DafnyCore/Backends/Dafny/ASTBuilder.cs | 8 +- .../Backends/Dafny/DafnyCodeGenerator.cs | 5 +- .../Rust/Dafny-compiler-rust-definitions.dfy | 23 ++-- .../Rust/Dafny-compiler-rust-proofs.dfy | 102 +++++++++++------- .../LitTests/LitTest/comp/rust/newtypes.dfy | 60 ++++++++++- 5 files changed, 143 insertions(+), 55 deletions(-) diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index aa6e8068dba..29087cbeb0a 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -188,7 +188,7 @@ public void AddMethod(DAST.Method item) { } public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); + parent.AddUnsupported("var/const for trait - " + item.dtor_name); } public object Finish() { @@ -240,11 +240,11 @@ public NewtypeBuilder(NewtypeContainer parent, string name, List ty } public void AddMethod(DAST.Method item) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); + parent.AddUnsupported("method for newtypes - " + item.dtor_name); } public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); + parent.AddUnsupported("const for newtypes - " + item.dtor_name); } public object Finish() { @@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) { } public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { - throw new UnsupportedFeatureException(Token.NoToken, Feature.RunAllTests); + parent.AddUnsupported("const for datatypes - " + item.dtor_name); } public object Finish() { diff --git a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs index 3e10637937f..0f55bd28e6f 100644 --- a/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs +++ b/Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs @@ -1577,12 +1577,13 @@ protected override void EmitLiteralExpr(ConcreteSyntaxTree wr, LiteralExpr e) { } protected override void EmitStringLiteral(string str, bool isVerbatim, ConcreteSyntaxTree wr) { - throw new UnsupportedInvalidOperationException("EmitStringLiteral"); + AddUnsupported("EmitStringLiteral"); } protected override ConcreteSyntaxTree EmitBitvectorTruncation(BitvectorType bvType, [CanBeNull] NativeType nativeType, bool surroundByUnchecked, ConcreteSyntaxTree wr) { - throw new UnsupportedInvalidOperationException("EmitBitvectorTruncation"); + AddUnsupported("EmitBitvectorTruncation"); + return wr; } protected override void EmitRotate(Expression e0, Expression e1, bool isRotateLeft, ConcreteSyntaxTree wr, diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy index 1ba1e84e853..7f2623cca51 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-definitions.dfy @@ -37,14 +37,16 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions { (|i| == 3 && i[2] in "0123456789")) } + // Given a Dafny-expanded fully qualified name with # or ., where ' has been replaced by _k, ? by _q and _ by __ + // detect if there are of the strings above predicate has_special(i: string) { if |i| == 0 then false else if i[0] == '.' then true else if i[0] == '#' then true // otherwise "escapeName("r#") becomes "r#"" else if i[0] == '_' then if 2 <= |i| then - if i[1] != '_' then true - else has_special(i[2..]) + if i[1] == '_' then has_special(i[2..]) + else true else true else @@ -88,6 +90,7 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions { predicate is_dafny_generated_id(i: string) { && |i| > 0 && i[0] == '_' && !has_special(i[1..]) + && (i != "_self" && i != "_Self") && (|i| >= 2 ==> i[1] != 'T') // To avoid conflict with tuple builders _T } @@ -101,21 +104,21 @@ module {:extern "Defs"} DafnyToRustCompilerDefinitions { } function escapeIdent(i: string): string { - if is_tuple_numeric(i) then + if is_tuple_numeric(i) then // _42 remains the same i - else if is_tuple_builder(i) then + else if is_tuple_builder(i) then // ___hMake42 becomes _T42 better_tuple_builder_name(i) - else if i == "self" || i == "Self" then - "r#_" + i + else if i == "self" || i == "Self" then // self becomes _self + "_" + i else if i in reserved_rust then "r#" + i - else if is_idiomatic_rust_id(i) then + else if is_idiomatic_rust_id(i) then // some__id becomes some_id idiomatic_rust(i) - else if is_dafny_generated_id(i) then + else if is_dafny_generated_id(i) then // _module remains _module i // Dafny-generated identifiers like "_module", cannot be written in Dafny itself - else + else // u16 becomes _u16, namespace.IsSomething_q becomes _namespace_dIsSomething_q var r := replaceDots(i); - "r#_" + r + "_" + r } // To be used when escaping variables diff --git a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy index 9b7e31813f0..c03cc6b580b 100644 --- a/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy +++ b/Source/DafnyCore/Backends/Rust/Dafny-compiler-rust-proofs.dfy @@ -87,15 +87,25 @@ module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompile else if i[0] == '_' then |i| >= 2 && - i[1] in "_qkh" && IsDafnyEncodedIdTail(i[2..]) + i[1] in ESCAPING && IsDafnyEncodedIdTail(i[2..]) else - i[0] in "aqkhd." && + (i[0] in SAMPLE_LETTERS || i[0] == '.') && IsDafnyEncodedIdTail(i[1..]) } - predicate IsDafnyEncodedId(i: string) { - if |i| == 0 then true - else i[0] in "aqkhd" && IsDafnyEncodedIdTail(i[1..]) + // Subset of characters supported in Dafny identifiers, for proof purposes + const SAMPLE_LETTERS := "aqkhd" + + // Letters that can come after a "_" in Dafny identifiers + // __ => _ + // _q => ? + // _k => ' + // _h => # + const ESCAPING := "_qkh" + + ghost predicate IsDafnyEncodedId(i: string) { + if |i| == 0 then false + else i[0] in SAMPLE_LETTERS && IsDafnyEncodedIdTail(i[1..]) } lemma DafnyEscapeCorrect(s: string) @@ -193,7 +203,7 @@ module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompile ensures escapeIdent("_m") == "_m" // any hidden variable ensures escapeIdent("___hMake1") == "_T1" // tuple deconstructor ensures escapeIdent("h__w") == "h_w" // only letters and underscore - ensures escapeIdent("h_kw") == "r#_h_kw" //contains special char + ensures escapeIdent("h_kw") == "_h_kw" //contains special char ensures escapeIdent("fn") == "r#fn" // Keyword { assert has_special("h_kw"); @@ -224,26 +234,26 @@ module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompile } function UnescapeIdent(s: string): string { - if |s| >= 2 && s[0..2] == "r#" then - if |s| >= 3 && s[2] == '_' then - ReverseReplaceDots(s[3..]) // General escape - else - s[2..] // Keyword - else if |s| >= 1 && s[0] == '_' then - if |s| >= 2 && s[1] == 'T' then - "___hMake" + s[2..] // Tuple builder - else if is_tuple_numeric(s) then + if |s| >= 1 && s[0] == '_' then + if is_tuple_numeric(s) then s + else if |s| >= 2 && s[1] == 'T' then + "___hMake" + s[2..] // Tuple builder + else if s == "_self" || s == "_Self" then + s[1..] else - s + ReverseReplaceDots(s[1..]) // We remove the extra "_" prefix and place dots again + else if |s| >= 2 && s[0..2] == "r#" then + s[2..] // Reserved identifier else // Idiomatic rust ReverseIdiomaticRust(s) } - lemma TupleIdentInvertible(s: string) - requires is_tuple_numeric(s) - ensures UnescapeIdent(escapeIdent(s)) == s - {} + lemma TupleIdentInvertible(i: string) + requires is_tuple_numeric(i) + ensures UnescapeIdent(escapeIdent(i)) == i + { + } lemma {:rlimit 500} TupleBuilderInvertible(i: string) requires !is_tuple_numeric(i) @@ -301,14 +311,24 @@ module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompile } } - lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(s: string) - requires !is_tuple_numeric(s) - requires !is_tuple_builder(s) - requires s !in reserved_rust - requires !is_idiomatic_rust_id(s) - requires is_dafny_generated_id(s) - ensures UnescapeIdent(escapeIdent(s)) == s + lemma {:rlimit 800} EscapeIdentInvertibleForDafnyGeneratedId(i: string) + requires IsDafnyEncodedId(i) + requires !is_tuple_numeric(i) + requires !is_tuple_builder(i) + requires i !in reserved_rust + requires !is_idiomatic_rust_id(i) + requires is_dafny_generated_id(i) + ensures UnescapeIdent(escapeIdent(i)) == i { + assert escapeIdent(i) == i; + var s := i; + assert |s| >= 1 && s[0] == '_'; + assert !(|s| >= 2 && s[1] == 'T'); + assert !(s == "_self" || s == "_Self"); + calc { + UnescapeIdent(s); + s; + } } lemma {:rlimit 800} EverythingElseInvertible(i: string) @@ -321,16 +341,24 @@ module {:extern "DafnyToRustCompilerProofs"} {:compile false} DafnyToRustCompile ensures UnescapeIdent(escapeIdent(i)) == i { var r := replaceDots(i); - var s := "r#_" + r; - assert |s| >= 2 && s[0..2] == "r#"; - assert |s| >= 3 && s[2] == '_'; - assert s[3..] == r; - calc { - UnescapeIdent(escapeIdent(i)); - UnescapeIdent(s); - ReverseReplaceDots(replaceDots(i)); - { ReplaceDotsInvertible(i); } - i; + var s := "_" + r; + assert escapeIdent(i) == s; + assert |s| >= 1 && s[0] == '_'; + assert !(|s| >= 2 && s[1] == 'T'); + assert !(s == "_self" || s == "_Self"); + assert |i| > 0; + if i[0] == '_' { + assert i[0] == '_'; // So if i[0] is not '_' + assert UnescapeIdent(escapeIdent(i)) == i; + } else { + calc { + UnescapeIdent(s); + ReverseReplaceDots(s[1..]); + ReverseReplaceDots(r); + ReverseReplaceDots(replaceDots(i)); + { ReplaceDotsInvertible(i); } + i; + } } } diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy index 080ec70510b..6375966da62 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy @@ -1,6 +1,40 @@ -// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" +// RUN: %testDafnyForEachCompiler --type-system-refresh --general-newtypes --refresh-exit-code=0 "%s" -newtype int2 = x: int | -2 <= x < 2 +newtype B = bool { + const b := this as bool + static const zero := false as B + static function Zero(): B { + zero + } + const n := Neg() + function Neg(): B + { + !this + } + method NegMethod() returns (z: B) { + z := Neg(); + } + static method NegMethodStatic(b: B) returns (z: B) { + z := b.NegMethod(); + } +} +newtype int2 = x: int | -2 <= x < 2 { + static const zero := 0 as int2 + static function Zero(): int2 { + zero + } + const n := Neg() + function Neg(): int2 + { + if this == -2 as int2 then this else -this + } + method NegMethod() returns (z: int2) { + z := Neg(); + } + static method NegMethodStatic(b: int2) returns (z: int2) { + z := b.NegMethod(); + } +} newtype int16 = x: int | -32768 <= x < 32768 const INT2_MAX: int2 := 1 type zero = x: int2 | x == 0 witness 0 @@ -13,6 +47,28 @@ type byte = uint8 newtype uint32 = x: int | 0 <= x < 0x1_00000000 method Main(){ + var trueb := true as B; + print trueb, "=true\n"; + print trueb.b, "=true\n"; + print B.zero, "=false\n"; + print B.Zero(), "=false\n"; + print trueb.n, "=false\n"; + print trueb.Neg(), "=false\n"; + trueb := trueb.NegMethod(); + print trueb, "=false\n"; + trueb := B.NegMethodStatic(trueb); + print trueb, "=true\n"; + var one := 1 as int2; + print int2.zero, "=0\n"; + print one, "=1\n"; + print one.n, "=-1\n"; + print int2.Zero(), "=0\n"; + print one.Neg(), "=-1\n"; + one := one.NegMethod(); + print one, "=-1\n"; + one := int2.NegMethodStatic(one); + print one, "=1\n"; + print INT2_MAX as int, "\n"; print Zero as int16, "\n"; print DChar, "\n"; From db9f88f9b88532088dc42b2b02c93633555f1913 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Fri, 18 Oct 2024 16:50:55 -0500 Subject: [PATCH 2/3] made pr --- Source/DafnyCore/Backends/Dafny/ASTBuilder.cs | 2 +- Source/DafnyCore/GeneratedFromDafny/Defs.cs | 12 +-- .../DafnyRuntimeRust/src/system/mod.rs | 80 +++++++++---------- 3 files changed, 47 insertions(+), 47 deletions(-) diff --git a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs index 29087cbeb0a..396055b1853 100644 --- a/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs +++ b/Source/DafnyCore/Backends/Dafny/ASTBuilder.cs @@ -344,7 +344,7 @@ public void AddMethod(DAST.Method item) { } public void AddField(DAST.Formal item, bool isConstant, _IOption defaultValue) { - parent.AddUnsupported("const for datatypes - " + item.dtor_name); + parent.AddUnsupported("const for datatypes - " + item.dtor_name); } public object Finish() { diff --git a/Source/DafnyCore/GeneratedFromDafny/Defs.cs b/Source/DafnyCore/GeneratedFromDafny/Defs.cs index bf93664d1ef..c8d2bc4c9ac 100644 --- a/Source/DafnyCore/GeneratedFromDafny/Defs.cs +++ b/Source/DafnyCore/GeneratedFromDafny/Defs.cs @@ -28,12 +28,12 @@ public static bool has__special(Dafny.ISequence i) { return true; } else if (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_'))) { if ((new BigInteger(2)) <= (new BigInteger((i).Count))) { - if (((i).Select(BigInteger.One)) != (new Dafny.Rune('_'))) { - return true; - } else { + if (((i).Select(BigInteger.One)) == (new Dafny.Rune('_'))) { Dafny.ISequence _in0 = (i).Drop(new BigInteger(2)); i = _in0; goto TAIL_CALL_START; + } else { + return true; } } else { return true; @@ -85,7 +85,7 @@ public static bool is__tuple__builder(Dafny.ISequence i) { return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_T"), (i).Drop(new BigInteger(8))); } public static bool is__dafny__generated__id(Dafny.ISequence i) { - return ((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T')))); + return (((((new BigInteger((i).Count)).Sign == 1) && (((i).Select(BigInteger.Zero)) == (new Dafny.Rune('_')))) && (!(Defs.__default.has__special((i).Drop(BigInteger.One))))) && ((!(i).Equals(Dafny.Sequence.UnicodeFromString("_self"))) && (!(i).Equals(Dafny.Sequence.UnicodeFromString("_Self"))))) && (!((new BigInteger((i).Count)) >= (new BigInteger(2))) || (((i).Select(BigInteger.One)) != (new Dafny.Rune('T')))); } public static bool is__idiomatic__rust__id(Dafny.ISequence i) { return ((((new BigInteger((i).Count)).Sign == 1) && (!(Defs.__default.has__special(i)))) && (!(Defs.__default.reserved__rust).Contains(i))) && (!(Defs.__default.reserved__rust__need__prefix).Contains(i)); @@ -99,7 +99,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence i) { } else if (Defs.__default.is__tuple__builder(i)) { return Defs.__default.better__tuple__builder__name(i); } else if (((i).Equals(Dafny.Sequence.UnicodeFromString("self"))) || ((i).Equals(Dafny.Sequence.UnicodeFromString("Self")))) { - return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("r#_"), i); + return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_"), i); } else if ((Defs.__default.reserved__rust).Contains(i)) { return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("r#"), i); } else if (Defs.__default.is__idiomatic__rust__id(i)) { @@ -108,7 +108,7 @@ public static bool is__idiomatic__rust__id(Dafny.ISequence i) { return i; } else { Dafny.ISequence _0_r = Defs.__default.replaceDots(i); - return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("r#_"), _0_r); + return Dafny.Sequence.Concat(Dafny.Sequence.UnicodeFromString("_"), _0_r); } } public static Dafny.ISequence escapeVar(Dafny.ISequence f) { diff --git a/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs b/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs index d30d8671ec0..eb25b8a8c4b 100644 --- a/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs +++ b/Source/DafnyRuntime/DafnyRuntimeRust/src/system/mod.rs @@ -64,8 +64,8 @@ pub mod _System { } impl Tuple2 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>) -> Rc) -> Tuple2> { - Rc::new(move |this: Self| -> Tuple2{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>) -> Rc) -> Tuple2<__T0, __T1>> { + Rc::new(move |this: Self| -> Tuple2<__T0, __T1>{ match this { Tuple2::_T2{_0, _1, } => { Tuple2::_T2 { @@ -207,8 +207,8 @@ pub mod _System { } impl Tuple1 { - pub fn coerce(f_0: Rc r#__T0 + 'static>) -> Rc) -> Tuple1> { - Rc::new(move |this: Self| -> Tuple1{ + pub fn coerce<__T0: DafnyType>(f_0: Rc __T0 + 'static>) -> Rc) -> Tuple1<__T0>> { + Rc::new(move |this: Self| -> Tuple1<__T0>{ match this { Tuple1::_T1{_0, } => { Tuple1::_T1 { @@ -303,8 +303,8 @@ pub mod _System { } impl Tuple3 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>) -> Rc) -> Tuple3> { - Rc::new(move |this: Self| -> Tuple3{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>) -> Rc) -> Tuple3<__T0, __T1, __T2>> { + Rc::new(move |this: Self| -> Tuple3<__T0, __T1, __T2>{ match this { Tuple3::_T3{_0, _1, _2, } => { Tuple3::_T3 { @@ -413,8 +413,8 @@ pub mod _System { } impl Tuple4 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>) -> Rc) -> Tuple4> { - Rc::new(move |this: Self| -> Tuple4{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>) -> Rc) -> Tuple4<__T0, __T1, __T2, __T3>> { + Rc::new(move |this: Self| -> Tuple4<__T0, __T1, __T2, __T3>{ match this { Tuple4::_T4{_0, _1, _2, _3, } => { Tuple4::_T4 { @@ -534,8 +534,8 @@ pub mod _System { } impl Tuple5 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>) -> Rc) -> Tuple5> { - Rc::new(move |this: Self| -> Tuple5{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>) -> Rc) -> Tuple5<__T0, __T1, __T2, __T3, __T4>> { + Rc::new(move |this: Self| -> Tuple5<__T0, __T1, __T2, __T3, __T4>{ match this { Tuple5::_T5{_0, _1, _2, _3, _4, } => { Tuple5::_T5 { @@ -666,8 +666,8 @@ pub mod _System { } impl Tuple6 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>) -> Rc) -> Tuple6> { - Rc::new(move |this: Self| -> Tuple6{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>) -> Rc) -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>> { + Rc::new(move |this: Self| -> Tuple6<__T0, __T1, __T2, __T3, __T4, __T5>{ match this { Tuple6::_T6{_0, _1, _2, _3, _4, _5, } => { Tuple6::_T6 { @@ -809,8 +809,8 @@ pub mod _System { } impl Tuple7 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>) -> Rc) -> Tuple7> { - Rc::new(move |this: Self| -> Tuple7{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>) -> Rc) -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>> { + Rc::new(move |this: Self| -> Tuple7<__T0, __T1, __T2, __T3, __T4, __T5, __T6>{ match this { Tuple7::_T7{_0, _1, _2, _3, _4, _5, _6, } => { Tuple7::_T7 { @@ -963,8 +963,8 @@ pub mod _System { } impl Tuple8 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>) -> Rc) -> Tuple8> { - Rc::new(move |this: Self| -> Tuple8{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>) -> Rc) -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>> { + Rc::new(move |this: Self| -> Tuple8<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7>{ match this { Tuple8::_T8{_0, _1, _2, _3, _4, _5, _6, _7, } => { Tuple8::_T8 { @@ -1128,8 +1128,8 @@ pub mod _System { } impl Tuple9 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>) -> Rc) -> Tuple9> { - Rc::new(move |this: Self| -> Tuple9{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>) -> Rc) -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>> { + Rc::new(move |this: Self| -> Tuple9<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8>{ match this { Tuple9::_T9{_0, _1, _2, _3, _4, _5, _6, _7, _8, } => { Tuple9::_T9 { @@ -1304,8 +1304,8 @@ pub mod _System { } impl Tuple10 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>) -> Rc) -> Tuple10> { - Rc::new(move |this: Self| -> Tuple10{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>) -> Rc) -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>> { + Rc::new(move |this: Self| -> Tuple10<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9>{ match this { Tuple10::_T10{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, } => { Tuple10::_T10 { @@ -1491,8 +1491,8 @@ pub mod _System { } impl Tuple11 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>) -> Rc) -> Tuple11> { - Rc::new(move |this: Self| -> Tuple11{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>) -> Rc) -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>> { + Rc::new(move |this: Self| -> Tuple11<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10>{ match this { Tuple11::_T11{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, } => { Tuple11::_T11 { @@ -1689,8 +1689,8 @@ pub mod _System { } impl Tuple12 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>) -> Rc) -> Tuple12> { - Rc::new(move |this: Self| -> Tuple12{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>) -> Rc) -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>> { + Rc::new(move |this: Self| -> Tuple12<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11>{ match this { Tuple12::_T12{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, } => { Tuple12::_T12 { @@ -1898,8 +1898,8 @@ pub mod _System { } impl Tuple13 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>) -> Rc) -> Tuple13> { - Rc::new(move |this: Self| -> Tuple13{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>) -> Rc) -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>> { + Rc::new(move |this: Self| -> Tuple13<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12>{ match this { Tuple13::_T13{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, } => { Tuple13::_T13 { @@ -2118,8 +2118,8 @@ pub mod _System { } impl Tuple14 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>) -> Rc) -> Tuple14> { - Rc::new(move |this: Self| -> Tuple14{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>) -> Rc) -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>> { + Rc::new(move |this: Self| -> Tuple14<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13>{ match this { Tuple14::_T14{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, } => { Tuple14::_T14 { @@ -2349,8 +2349,8 @@ pub mod _System { } impl Tuple15 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>) -> Rc) -> Tuple15> { - Rc::new(move |this: Self| -> Tuple15{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>) -> Rc) -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>> { + Rc::new(move |this: Self| -> Tuple15<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14>{ match this { Tuple15::_T15{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, } => { Tuple15::_T15 { @@ -2591,8 +2591,8 @@ pub mod _System { } impl Tuple16 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>) -> Rc) -> Tuple16> { - Rc::new(move |this: Self| -> Tuple16{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>) -> Rc) -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>> { + Rc::new(move |this: Self| -> Tuple16<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15>{ match this { Tuple16::_T16{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, } => { Tuple16::_T16 { @@ -2844,8 +2844,8 @@ pub mod _System { } impl Tuple17 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>) -> Rc) -> Tuple17> { - Rc::new(move |this: Self| -> Tuple17{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>) -> Rc) -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>> { + Rc::new(move |this: Self| -> Tuple17<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16>{ match this { Tuple17::_T17{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, } => { Tuple17::_T17 { @@ -3108,8 +3108,8 @@ pub mod _System { } impl Tuple18 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>) -> Rc) -> Tuple18> { - Rc::new(move |this: Self| -> Tuple18{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>) -> Rc) -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>> { + Rc::new(move |this: Self| -> Tuple18<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17>{ match this { Tuple18::_T18{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, } => { Tuple18::_T18 { @@ -3383,8 +3383,8 @@ pub mod _System { } impl Tuple19 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>, f_18: Rc r#__T18 + 'static>) -> Rc) -> Tuple19> { - Rc::new(move |this: Self| -> Tuple19{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>, f_18: Rc __T18 + 'static>) -> Rc) -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>> { + Rc::new(move |this: Self| -> Tuple19<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18>{ match this { Tuple19::_T19{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, } => { Tuple19::_T19 { @@ -3669,8 +3669,8 @@ pub mod _System { } impl Tuple20 { - pub fn coerce(f_0: Rc r#__T0 + 'static>, f_1: Rc r#__T1 + 'static>, f_2: Rc r#__T2 + 'static>, f_3: Rc r#__T3 + 'static>, f_4: Rc r#__T4 + 'static>, f_5: Rc r#__T5 + 'static>, f_6: Rc r#__T6 + 'static>, f_7: Rc r#__T7 + 'static>, f_8: Rc r#__T8 + 'static>, f_9: Rc r#__T9 + 'static>, f_10: Rc r#__T10 + 'static>, f_11: Rc r#__T11 + 'static>, f_12: Rc r#__T12 + 'static>, f_13: Rc r#__T13 + 'static>, f_14: Rc r#__T14 + 'static>, f_15: Rc r#__T15 + 'static>, f_16: Rc r#__T16 + 'static>, f_17: Rc r#__T17 + 'static>, f_18: Rc r#__T18 + 'static>, f_19: Rc r#__T19 + 'static>) -> Rc) -> Tuple20> { - Rc::new(move |this: Self| -> Tuple20{ + pub fn coerce<__T0: DafnyType, __T1: DafnyType, __T2: DafnyType, __T3: DafnyType, __T4: DafnyType, __T5: DafnyType, __T6: DafnyType, __T7: DafnyType, __T8: DafnyType, __T9: DafnyType, __T10: DafnyType, __T11: DafnyType, __T12: DafnyType, __T13: DafnyType, __T14: DafnyType, __T15: DafnyType, __T16: DafnyType, __T17: DafnyType, __T18: DafnyType, __T19: DafnyType>(f_0: Rc __T0 + 'static>, f_1: Rc __T1 + 'static>, f_2: Rc __T2 + 'static>, f_3: Rc __T3 + 'static>, f_4: Rc __T4 + 'static>, f_5: Rc __T5 + 'static>, f_6: Rc __T6 + 'static>, f_7: Rc __T7 + 'static>, f_8: Rc __T8 + 'static>, f_9: Rc __T9 + 'static>, f_10: Rc __T10 + 'static>, f_11: Rc __T11 + 'static>, f_12: Rc __T12 + 'static>, f_13: Rc __T13 + 'static>, f_14: Rc __T14 + 'static>, f_15: Rc __T15 + 'static>, f_16: Rc __T16 + 'static>, f_17: Rc __T17 + 'static>, f_18: Rc __T18 + 'static>, f_19: Rc __T19 + 'static>) -> Rc) -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>> { + Rc::new(move |this: Self| -> Tuple20<__T0, __T1, __T2, __T3, __T4, __T5, __T6, __T7, __T8, __T9, __T10, __T11, __T12, __T13, __T14, __T15, __T16, __T17, __T18, __T19>{ match this { Tuple20::_T20{_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19, } => { Tuple20::_T20 { From 74d4d75bc45589ec7a5fb59eca4230100ba92d67 Mon Sep 17 00:00:00 2001 From: Mikael Mayer Date: Thu, 24 Oct 2024 13:23:31 -0500 Subject: [PATCH 3/3] Accidentally committed a file --- .../LitTests/LitTest/comp/rust/newtypes.dfy | 60 +------------------ 1 file changed, 2 insertions(+), 58 deletions(-) diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy index 6375966da62..080ec70510b 100644 --- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy +++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/rust/newtypes.dfy @@ -1,40 +1,6 @@ -// RUN: %testDafnyForEachCompiler --type-system-refresh --general-newtypes --refresh-exit-code=0 "%s" +// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -newtype B = bool { - const b := this as bool - static const zero := false as B - static function Zero(): B { - zero - } - const n := Neg() - function Neg(): B - { - !this - } - method NegMethod() returns (z: B) { - z := Neg(); - } - static method NegMethodStatic(b: B) returns (z: B) { - z := b.NegMethod(); - } -} -newtype int2 = x: int | -2 <= x < 2 { - static const zero := 0 as int2 - static function Zero(): int2 { - zero - } - const n := Neg() - function Neg(): int2 - { - if this == -2 as int2 then this else -this - } - method NegMethod() returns (z: int2) { - z := Neg(); - } - static method NegMethodStatic(b: int2) returns (z: int2) { - z := b.NegMethod(); - } -} +newtype int2 = x: int | -2 <= x < 2 newtype int16 = x: int | -32768 <= x < 32768 const INT2_MAX: int2 := 1 type zero = x: int2 | x == 0 witness 0 @@ -47,28 +13,6 @@ type byte = uint8 newtype uint32 = x: int | 0 <= x < 0x1_00000000 method Main(){ - var trueb := true as B; - print trueb, "=true\n"; - print trueb.b, "=true\n"; - print B.zero, "=false\n"; - print B.Zero(), "=false\n"; - print trueb.n, "=false\n"; - print trueb.Neg(), "=false\n"; - trueb := trueb.NegMethod(); - print trueb, "=false\n"; - trueb := B.NegMethodStatic(trueb); - print trueb, "=true\n"; - var one := 1 as int2; - print int2.zero, "=0\n"; - print one, "=1\n"; - print one.n, "=-1\n"; - print int2.Zero(), "=0\n"; - print one.Neg(), "=-1\n"; - one := one.NegMethod(); - print one, "=-1\n"; - one := int2.NegMethodStatic(one); - print one, "=1\n"; - print INT2_MAX as int, "\n"; print Zero as int16, "\n"; print DChar, "\n";