From 35145cc2b4702317a20ff5ff6881542dc264d302 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 26 Jun 2024 18:07:44 +0200 Subject: [PATCH] fix(engine/fstar): add tests --- ...oolchain__attribute-opaque into-fstar.snap | 4 +- .../toolchain__attributes into-fstar.snap | 12 +- .../toolchain__generics into-fstar.snap | 38 +-- .../toolchain__include-flag into-fstar.snap | 6 +- .../toolchain__interface-only into-fstar.snap | 4 +- .../toolchain__loops into-fstar.snap | 2 +- ..._mut-ref-functionalization into-fstar.snap | 4 +- .../toolchain__naming into-fstar.snap | 18 +- .../toolchain__traits into-fstar.snap | 293 +++++++++++++----- tests/traits/src/lib.rs | 74 ++++- 10 files changed, 331 insertions(+), 124 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap index 3e5e8e8fb..7b881d431 100644 --- a/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attribute-opaque into-fstar.snap @@ -37,7 +37,7 @@ module Attribute_opaque open Core open FStar.Mul -val t_OpaqueEnum (v_X: usize) (#v_T #v_U: Type0) : Type0 +val t_OpaqueEnum (#v_X: usize) (#v_T #v_U: Type0) : Type0 -val t_OpaqueStruct (v_X: usize) (#v_T #v_U: Type0) : Type0 +val t_OpaqueStruct (#v_X: usize) (#v_T #v_U: Type0) : Type0 ''' diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index d49db0fb5..e10eb4bf5 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -62,7 +62,7 @@ let impl__SafeIndex__new (i: usize) : Core.Option.t_Option t_SafeIndex = else Core.Option.Option_None <: Core.Option.t_Option t_SafeIndex [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index #(t_Array v_T (sz 10)) #t_SafeIndex = +let impl_1 (#v_T: Type0) : Core.Ops.Index.t_Index (t_Array v_T (sz 10)) t_SafeIndex = { f_Output = v_T; f_index_pre = (fun (self: t_Array v_T (sz 10)) (index: t_SafeIndex) -> true); @@ -79,7 +79,7 @@ open FStar.Mul type t_Foo = | Foo : u8 -> t_Foo [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo = +let impl: Core.Ops.Arith.t_Add t_Foo t_Foo = { f_Output = t_Foo; f_add_pre = (fun (self: t_Foo) (rhs: t_Foo) -> self._0 <. (255uy -! rhs._0 <: u8)); @@ -88,7 +88,7 @@ let impl: Core.Ops.Arith.t_Add #t_Foo #t_Foo = } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1: Core.Ops.Arith.t_Mul #t_Foo #t_Foo = +let impl_1: Core.Ops.Arith.t_Mul t_Foo t_Foo = { f_Output = t_Foo; f_mul_pre @@ -131,7 +131,7 @@ let mutation_example (t_MyArray & t_Slice u8 & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: Core.Ops.Index.t_Index #t_MyArray #usize = +let impl: Core.Ops.Index.t_Index t_MyArray usize = { f_Output = u8; f_index_pre = (fun (self: t_MyArray) (index: usize) -> index <. v_MAX); @@ -145,7 +145,7 @@ module Attributes.Refinement_types open Core open FStar.Mul -let t_BoundedU8 (v_MIN v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX} +let t_BoundedU8 (#v_MIN #v_MAX: u8) = x: u8{x >=. v_MIN && x <=. v_MAX} /// Example of a specific constraint on a value let t_CompressionFactor = x: u8{x =. 4uy || x =. 5uy || x =. 10uy || x =. 11uy} @@ -158,7 +158,7 @@ let t_Even = x: u8{(x %! 2uy <: u8) =. 0uy} let t_FieldElement = x: u16{x <=. 2347us} /// A modular mutliplicative inverse -let t_ModInverse (v_MOD: u32) = +let t_ModInverse (#v_MOD: u32) = n: u32 { (((cast (n <: u32) <: u128) *! (cast (v_MOD <: u32) <: u128) <: u128) %! diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index 513b45f91..4c6691cf8 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -45,38 +45,38 @@ module Generics open Core open FStar.Mul -let impl__Bar__inherent_impl_generics (#v_T: Type0) (v_N: usize) (x: t_Array v_T v_N) : Prims.unit = +let impl__Bar__inherent_impl_generics (#v_T: Type0) (#v_N: usize) (x: t_Array v_T v_N) : Prims.unit = () -class t_Foo (#v_Self: Type0) = { - f_const_add_pre:v_N: usize -> v_Self -> bool; - f_const_add_post:v_N: usize -> v_Self -> usize -> bool; - f_const_add:v_N: usize -> x0: v_Self - -> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result) +class t_Foo (v_Self: Type0) = { + f_const_add_pre:#v_N: usize -> v_Self -> bool; + f_const_add_post:#v_N: usize -> v_Self -> usize -> bool; + f_const_add:#v_N: usize -> x0: v_Self + -> Prims.Pure usize (f_const_add_pre #v_N x0) (fun result -> f_const_add_post #v_N x0 result) } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_Foo_for_usize: t_Foo #usize = +let impl_Foo_for_usize: t_Foo usize = { - f_const_add_pre = (fun (v_N: usize) (self: usize) -> true); - f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true); - f_const_add = fun (v_N: usize) (self: usize) -> self +! v_N + f_const_add_pre = (fun (#v_N: usize) (self: usize) -> true); + f_const_add_post = (fun (#v_N: usize) (self: usize) (out: usize) -> true); + f_const_add = fun (#v_N: usize) (self: usize) -> self +! v_N } let dup (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone #v_T) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Clone.t_Clone v_T) (x: v_T) : (v_T & v_T) = Core.Clone.f_clone #v_T x, Core.Clone.f_clone #v_T x <: (v_T & v_T) -let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x +let f (#v_N x: usize) : usize = (v_N +! v_N <: usize) +! x -let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3 +let call_f (_: Prims.unit) : usize = (f #(sz 10) (sz 3) <: usize) +! sz 3 let g - (v_N: usize) + (#v_N: usize) (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into #v_T #(t_Array usize v_N)) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Convert.t_Into v_T (t_Array usize v_N)) (arr: v_T) : usize = (Core.Option.impl__unwrap_or #usize @@ -93,7 +93,7 @@ let g v_N let call_g (_: Prims.unit) : usize = - (g (sz 3) + (g #(sz 3) #(t_Array usize (sz 3)) (let list = [sz 42; sz 3; sz 49] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); @@ -102,7 +102,7 @@ let call_g (_: Prims.unit) : usize = usize) +! sz 3 -let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = +let foo (#v_LEN: usize) (arr: t_Array usize v_LEN) : usize = let acc:usize = v_LEN +! sz 9 in let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range @@ -121,9 +121,9 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = acc let repeat - (v_LEN: usize) + (#v_LEN: usize) (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy #v_T) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Marker.t_Copy v_T) (x: v_T) : t_Array v_T v_LEN = Rust_primitives.Hax.repeat x v_LEN diff --git a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap index ec507f66b..a4ce27894 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -32,7 +32,7 @@ module Include_flag open Core open FStar.Mul -class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } +class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } /// Indirect dependencies let main_a_a (_: Prims.unit) : Prims.unit = () @@ -42,7 +42,7 @@ let main_a_b (_: Prims.unit) : Prims.unit = () let main_a_c (_: Prims.unit) : Prims.unit = () /// Direct dependencies -let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait #v_T) (x: v_T) +let main_a (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait v_T) (x: v_T) : Prims.unit = let _:Prims.unit = main_a_a () in let _:Prims.unit = main_a_b () in @@ -76,7 +76,7 @@ let main_c (_: Prims.unit) : Prims.unit = type t_Foo = | Foo : t_Foo [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_Trait_for_Foo: t_Trait #t_Foo = { __marker_trait = () } +let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () } /// Entrypoint let main (_: Prims.unit) : Prims.unit = diff --git a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap index e4173e16e..b3a95740d 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -54,7 +54,7 @@ type t_Bar = | Bar : t_Bar /// dropped. This might be a bit surprising: see /// https://github.com/hacspec/hax/issues/616. [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: Core.Convert.t_From #t_Bar #Prims.unit = +let impl: Core.Convert.t_From t_Bar Prims.unit = { f_from_pre = (fun ((): Prims.unit) -> true); f_from_post = (fun ((): Prims.unit) (out: t_Bar) -> true); @@ -65,7 +65,7 @@ val from__from: u8 -> Prims.Pure t_Bar Prims.l_True (fun _ -> Prims.l_True) /// If you need to drop the body of a method, please hoist it: [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1: Core.Convert.t_From #t_Bar #u8 = +let impl_1: Core.Convert.t_From t_Bar u8 = { f_from_pre = (fun (x: u8) -> true); f_from_post = (fun (x: u8) (out: t_Bar) -> true); diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 169518fc5..6a160acf7 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -37,7 +37,7 @@ open FStar.Mul let bool_returning (x: u8) : bool = x <. 10uy -let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = +let chunks (#v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let chunks:Core.Slice.Iter.t_ChunksExact usize = Core.Slice.impl__chunks_exact #usize diff --git a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index d01460536..76f5002cd 100644 --- a/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap @@ -32,7 +32,7 @@ module Mut_ref_functionalization open Core open FStar.Mul -class t_FooTrait (#v_Self: Type0) = { +class t_FooTrait (v_Self: Type0) = { f_z_pre:v_Self -> bool; f_z_post:v_Self -> v_Self -> bool; f_z:x0: v_Self -> Prims.Pure v_Self (f_z_pre x0) (fun result -> f_z_post x0 result) @@ -173,7 +173,7 @@ type t_Bar = { type t_Foo = { f_field:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_FooTrait_for_Foo: t_FooTrait #t_Foo = +let impl_FooTrait_for_Foo: t_FooTrait t_Foo = { f_z_pre = (fun (self: t_Foo) -> true); f_z_post = (fun (self: t_Foo) (out: t_Foo) -> true); diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index 7623fa00a..68c009f19 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -108,28 +108,28 @@ type t_Foo2 = | Foo2_A : t_Foo2 | Foo2_B { f_x:usize }: t_Foo2 -class t_FooTrait (#v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } +class t_FooTrait (v_Self: Type0) = { f_ASSOCIATED_CONSTANT:usize } -class t_T1 (#v_Self: Type0) = { __marker_trait_t_T1:Prims.unit } +class t_T1 (v_Self: Type0) = { __marker_trait_t_T1:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_T1_for_Foo: t_T1 #t_Foo = { __marker_trait = () } +let impl_T1_for_Foo: t_T1 t_Foo = { __marker_trait = () } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_T1_for_tuple_Foo_u8: t_T1 #(t_Foo & u8) = { __marker_trait = () } +let impl_T1_for_tuple_Foo_u8: t_T1 (t_Foo & u8) = { __marker_trait = () } -class t_T2_for_a (#v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit } +class t_T2_for_a (v_Self: Type0) = { __marker_trait_t_T2_for_a:Prims.unit } -class t_T3_e_for_a (#v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit } +class t_T3_e_for_a (v_Self: Type0) = { __marker_trait_t_T3_e_for_a:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a #t_Foo = { __marker_trait = () } +let impl_T3_e_e_for_a_for_Foo: t_T3_e_for_a t_Foo = { __marker_trait = () } let v_INHERENT_CONSTANT: usize = sz 3 let constants (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait #v_T) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) (_: Prims.unit) : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT @@ -146,7 +146,7 @@ let reserved_names (v_val v_noeq v_of: u8) : u8 = (v_val +! v_noeq <: u8) +! v_o type t_Arity1 (v_T: Type0) = | Arity1 : v_T -> t_Arity1 v_T [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a #(t_Arity1 (t_Foo & u8)) = +let impl_T2_e_for_a_for_Arity1_of_tuple_Foo_u8: t_T2_for_a (t_Arity1 (t_Foo & u8)) = { __marker_trait = () } type t_B = | B : t_B diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 64070b0e6..b12fe2503 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -26,49 +26,19 @@ exit = 0 diagnostics = [] [stdout.files] -"Traits.Calling_convention_trait_args.fst" = ''' -module Traits.Calling_convention_trait_args -#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" -open Core -open FStar.Mul - -class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } - -class t_Foo (#v_Self: Type0) = { - f_X:Type0; - f_X_4373360806090370338:t_Trait #f_X; - f_associated_function_pre:#v_T: Type0 -> {| i3: t_Trait #v_T |} -> Prims.unit -> bool; - f_associated_function_post:#v_T: Type0 -> {| i3: t_Trait #v_T |} -> Prims.unit -> Prims.unit - -> bool; - f_associated_function:#v_T: Type0 -> {| i3: t_Trait #v_T |} -> x0: Prims.unit - -> Prims.Pure Prims.unit - (f_associated_function_pre v_T i3 x0) - (fun result -> f_associated_function_post v_T i3 x0 result); - f_method_pre:#v_T: Type0 -> {| i4: t_Trait #v_T |} -> Prims.unit -> bool; - f_method_post:#v_T: Type0 -> {| i4: t_Trait #v_T |} -> Prims.unit -> Prims.unit -> bool; - f_method:#v_T: Type0 -> {| i4: t_Trait #v_T |} -> x0: Prims.unit - -> Prims.Pure Prims.unit (f_method_pre v_T i4 x0) (fun result -> f_method_post v_T i4 x0 result) -} - -let caller - (#v_T: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Trait #v_T) - (_: Prims.unit) - : Prims.unit = () -''' "Traits.For_clauses.Issue_495_.Minimized_3_.fst" = ''' module Traits.For_clauses.Issue_495_.Minimized_3_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -class t_Trait (#v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } +class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl (#v_P: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut #v_P #u8) - : t_Trait #v_P = { __marker_trait = () } + (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8) + : t_Trait v_P = { __marker_trait = () } ''' "Traits.For_clauses.Issue_495_.fst" = ''' module Traits.For_clauses.Issue_495_ @@ -135,13 +105,13 @@ module Traits.For_clauses open Core open FStar.Mul -class t_Foo (#v_Self: Type0) (#v_T: Type0) = { +class t_Foo (v_Self: Type0) (v_T: Type0) = { f_to_t_pre:v_Self -> bool; f_to_t_post:v_Self -> v_T -> bool; f_to_t:x0: v_Self -> Prims.Pure v_T (f_to_t_pre x0) (fun result -> f_to_t_post x0 result) } -let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo #v_X #u8) (x: v_X) +let v__f (#v_X: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_X u8) (x: v_X) : Prims.unit = let _:u8 = f_to_t #v_X #u8 x in () @@ -162,7 +132,7 @@ open FStar.Mul [@@ FStar.Tactics.Typeclasses.tcinstance] let impl: Traits.Implicit_dependencies_issue_667_.Trait_definition.t_MyTrait -#Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType = +Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType = { f_my_method_pre = @@ -180,7 +150,7 @@ module Traits.Implicit_dependencies_issue_667_.Trait_definition open Core open FStar.Mul -class t_MyTrait (#v_Self: Type0) = { +class t_MyTrait (v_Self: Type0) = { f_my_method_pre:v_Self -> bool; f_my_method_post:v_Self -> Prims.unit -> bool; f_my_method:x0: v_Self @@ -203,44 +173,221 @@ let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyTy Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType x ''' +"Traits.Implicit_explicit_calling_conventions.fst" = ''' +module Traits.Implicit_explicit_calling_conventions +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg } + +class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + f_method_pre: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg + -> bool; + f_method_post: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg -> + Prims.unit + -> bool; + f_method: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + x0: v_Self -> + x1: v_TypeArg -> + x2: t_Type v_TypeArg v_ConstArg + -> Prims.Pure Prims.unit + (f_method_pre #v_MethodTypeArg #v_MethodConstArg x0 x1 x2) + (fun result -> f_method_post #v_MethodTypeArg #v_MethodConstArg x0 x1 x2 result); + f_associated_function_pre: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg + -> bool; + f_associated_function_post: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg -> + Prims.unit + -> bool; + f_associated_function: + #v_MethodTypeArg: Type0 -> + #v_MethodConstArg: usize -> + x0: v_Self -> + x1: v_TypeArg -> + x2: t_Type v_TypeArg v_ConstArg + -> Prims.Pure Prims.unit + (f_associated_function_pre #v_MethodTypeArg #v_MethodConstArg x0 x1 x2) + (fun result -> f_associated_function_post #v_MethodTypeArg #v_MethodConstArg x0 x1 x2 result + ) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl (#v_TypeArg: Type0) (#v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg v_ConstArg = + { + f_method_pre + = + (fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + true); + f_method_post + = + (fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + (out: Prims.unit) + -> + true); + f_method + = + (fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + ()); + f_associated_function_pre + = + (fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + true); + f_associated_function_post + = + (fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + (out: Prims.unit) + -> + true); + f_associated_function + = + fun + (#v_MethodTypeArg: Type0) + (#v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + () + } + +class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9139092951006237722:t_Trait v_Self + v_TypeArg + v_ConstArg; + f_AssocType:Type0; + f_AssocType_11967135072657554621:t_Trait f_AssocType v_TypeArg v_ConstArg +} + +let associated_function_caller + (#v_MethodTypeArg #v_TypeArg: Type0) + (#v_ConstArg #v_MethodConstArg: usize) + (#v_ImplTrait: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: t_Trait v_ImplTrait v_TypeArg v_ConstArg) + (x: v_ImplTrait) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + : Prims.unit = + let _:Prims.unit = + f_associated_function #v_ImplTrait + #v_TypeArg + #v_ConstArg + #v_MethodTypeArg + #v_MethodConstArg + x + value_TypeArg + value_Type + in + () + +let method_caller + (#v_MethodTypeArg #v_TypeArg: Type0) + (#v_ConstArg #v_MethodConstArg: usize) + (#v_ImplTrait: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: t_Trait v_ImplTrait v_TypeArg v_ConstArg) + (x: v_ImplTrait) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + : Prims.unit = + let _:Prims.unit = + f_method #v_ImplTrait + #v_TypeArg + #v_ConstArg + #v_MethodTypeArg + #v_MethodConstArg + x + value_TypeArg + value_Type + in + () +''' "Traits.Interlaced_consts_types.fst" = ''' module Traits.Interlaced_consts_types #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" open Core open FStar.Mul -class t_Foo (#v_Self: Type0) (v_FooConst: usize) (#v_FooType: Type0) = { +class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = { f_fun_pre: - v_FunConst: usize -> + #v_FunConst: usize -> #v_FunType: Type0 -> t_Array v_FooType v_FooConst -> t_Array v_FunType v_FunConst -> bool; f_fun_post: - v_FunConst: usize -> + #v_FunConst: usize -> #v_FunType: Type0 -> t_Array v_FooType v_FooConst -> t_Array v_FunType v_FunConst -> Prims.unit -> bool; f_fun: - v_FunConst: usize -> + #v_FunConst: usize -> #v_FunType: Type0 -> x0: t_Array v_FooType v_FooConst -> x1: t_Array v_FunType v_FunConst -> Prims.Pure Prims.unit - (f_fun_pre v_FunConst v_FunType x0 x1) - (fun result -> f_fun_post v_FunConst v_FunType x0 x1 result) + (f_fun_pre #v_FunConst #v_FunType x0 x1) + (fun result -> f_fun_post #v_FunConst #v_FunType x0 x1 result) } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) - : t_Foo #v_SelfType v_FooConst #v_FooType = +let impl (#v_FooConst: usize) (#v_FooType #v_SelfType: Type0) + : t_Foo v_SelfType v_FooConst v_FooType = { f_fun_pre = (fun - (v_FunConst: usize) + (#v_FunConst: usize) (#v_FunType: Type0) (x: t_Array v_FooType v_FooConst) (y: t_Array v_FunType v_FunConst) @@ -249,7 +396,7 @@ let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) f_fun_post = (fun - (v_FunConst: usize) + (#v_FunConst: usize) (#v_FunType: Type0) (x: t_Array v_FooType v_FooConst) (y: t_Array v_FunType v_FunConst) @@ -259,7 +406,7 @@ let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) f_fun = fun - (v_FunConst: usize) + (#v_FunConst: usize) (#v_FunType: Type0) (x: t_Array v_FooType v_FooConst) (y: t_Array v_FunType v_FunConst) @@ -276,7 +423,7 @@ module Traits.Type_alias_bounds_issue_707_ open Core open FStar.Mul -type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone #v_T |} = +type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} = | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T ''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' @@ -285,19 +432,19 @@ module Traits.Unconstrainted_types_issue_677_ open Core open FStar.Mul -class t_PolyOp (#v_Self: Type0) = { +class t_PolyOp (v_Self: Type0) = { f_op_pre:u32 -> u32 -> bool; f_op_post:u32 -> u32 -> u32 -> bool; f_op:x0: u32 -> x1: u32 -> Prims.Pure u32 (f_op_pre x0 x1) (fun result -> f_op_post x0 x1 result) } -let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp #v_OP) (x: u32) +let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp v_OP) (x: u32) : u32 = f_op #v_OP x x type t_Plus = | Plus : t_Plus [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl: t_PolyOp #t_Plus = +let impl: t_PolyOp t_Plus = { f_op_pre = (fun (x: u32) (y: u32) -> true); f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true); @@ -307,7 +454,7 @@ let impl: t_PolyOp #t_Plus = type t_Times = | Times : t_Times [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_1: t_PolyOp #t_Times = +let impl_1: t_PolyOp t_Times = { f_op_pre = (fun (x: u32) (y: u32) -> true); f_op_post = (fun (x: u32) (y: u32) (out: u32) -> true); @@ -322,13 +469,13 @@ module Traits open Core open FStar.Mul -class t_Bar (#v_Self: Type0) = { +class t_Bar (v_Self: Type0) = { f_bar_pre:v_Self -> bool; f_bar_post:v_Self -> Prims.unit -> bool; f_bar:x0: v_Self -> Prims.Pure Prims.unit (f_bar_pre x0) (fun result -> f_bar_post x0 result) } -let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar #v_T) (x: v_T) +let impl_2__method (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Bar v_T) (x: v_T) : Prims.unit = f_bar #v_T x type t_Error = | Error_Fail : t_Error @@ -340,7 +487,7 @@ let impl__Error__for_application_callback (_: Prims.unit) : Prims.unit -> t_Err let t_Error_cast_to_repr (x: t_Error) : isize = match x with | Error_Fail -> isz 0 -class t_Lang (#v_Self: Type0) = { +class t_Lang (v_Self: Type0) = { f_Var:Type0; f_s_pre:v_Self -> i32 -> bool; f_s_post:v_Self -> i32 -> (v_Self & f_Var) -> bool; @@ -348,8 +495,8 @@ class t_Lang (#v_Self: Type0) = { -> Prims.Pure (v_Self & f_Var) (f_s_pre x0 x1) (fun result -> f_s_post x0 x1 result) } -class t_SuperTrait (#v_Self: Type0) = { - [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone #v_Self; +class t_SuperTrait (v_Self: Type0) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self; f_function_of_super_trait_pre:v_Self -> bool; f_function_of_super_trait_post:v_Self -> u32 -> bool; f_function_of_super_trait:x0: v_Self @@ -359,7 +506,7 @@ class t_SuperTrait (#v_Self: Type0) = { } [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_SuperTrait_for_i32: t_SuperTrait #i32 = +let impl_SuperTrait_for_i32: t_SuperTrait i32 = { _super_9442900250278684536 = FStar.Tactics.Typeclasses.solve; f_function_of_super_trait_pre = (fun (self: i32) -> true); @@ -367,10 +514,10 @@ let impl_SuperTrait_for_i32: t_SuperTrait #i32 = f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32 } -class t_Foo (#v_Self: Type0) = { +class t_Foo (v_Self: Type0) = { f_AssocType:Type0; - f_AssocType_17663802186765685673:t_SuperTrait #f_AssocType; - f_AssocType_10139459042277121690:Core.Clone.t_Clone #f_AssocType; + f_AssocType_17663802186765685673:t_SuperTrait f_AssocType; + f_AssocType_10139459042277121690:Core.Clone.t_Clone f_AssocType; f_N:usize; f_assoc_f_pre:Prims.unit -> bool; f_assoc_f_post:Prims.unit -> Prims.unit -> bool; @@ -380,15 +527,17 @@ class t_Foo (#v_Self: Type0) = { f_method_f_post:v_Self -> Prims.unit -> bool; f_method_f:x0: v_Self -> Prims.Pure Prims.unit (f_method_f_pre x0) (fun result -> f_method_f_post x0 result); - f_assoc_type_pre:{| i3: Core.Marker.t_Copy #f_AssocType |} -> f_AssocType -> bool; - f_assoc_type_post:{| i3: Core.Marker.t_Copy #f_AssocType |} -> f_AssocType -> Prims.unit -> bool; - f_assoc_type:{| i3: Core.Marker.t_Copy #f_AssocType |} -> x0: f_AssocType - -> Prims.Pure Prims.unit (f_assoc_type_pre i3 x0) (fun result -> f_assoc_type_post i3 x0 result) + f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> bool; + f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> bool; + f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType + -> Prims.Pure Prims.unit + (f_assoc_type_pre #i3 x0) + (fun result -> f_assoc_type_post #i3 x0 result) } let closure_impl_expr (#v_I: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator #v_I) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: Core.Iter.Traits.Iterator.t_Iterator v_I) (it: v_I) : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) @@ -399,8 +548,8 @@ let closure_impl_expr let closure_impl_expr_fngen (#v_I #v_F: Type0) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator #v_I) - (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut #v_F #Prims.unit) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i2: Core.Iter.Traits.Iterator.t_Iterator v_I) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: Core.Ops.Function.t_FnMut v_F Prims.unit) (it: v_I) (f: v_F) : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = @@ -410,15 +559,15 @@ let closure_impl_expr_fngen <: Core.Iter.Adapters.Map.t_Map v_I v_F) -let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo #v_T) (x: v_T) : Prims.unit = +let f (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: v_T) : Prims.unit = let _:Prims.unit = f_assoc_f #v_T () in f_method_f #v_T x -let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo #v_T) (x: i1.f_AssocType) +let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x: i1.f_AssocType) : u32 = f_function_of_super_trait #i1.f_AssocType x [@@ FStar.Tactics.Typeclasses.tcinstance] -let impl_Foo_for_tuple_: t_Foo #Prims.unit = +let impl_Foo_for_tuple_: t_Foo Prims.unit = { f_AssocType = i32; f_AssocType_17663802186765685673 = FStar.Tactics.Typeclasses.solve; diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 82ef6e00c..3d48dda4a 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -178,15 +178,73 @@ mod interlaced_consts_types { } // Related to issue 719 (after reopen) -mod calling_convention_trait_args { - trait Trait {} - - fn caller() {} +mod implicit_explicit_calling_conventions { + struct Type { + field: [TypeArg; ConstArg], + } + + trait Trait { + fn method( + self, + value_TypeArg: TypeArg, + value_Type: Type, + ); + fn associated_function( + _self: Self, + value_TypeArg: TypeArg, + value_Type: Type, + ); + } + + impl Trait for () { + fn method( + self, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + } + fn associated_function( + _self: Self, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + } + } - trait Foo { - type X: Trait; - fn associated_function(); - fn method(); + trait SubTrait: Trait { + type AssocType: Trait; + } + + fn method_caller< + MethodTypeArg, + TypeArg, + const ConstArg: usize, + const MethodConstArg: usize, + ImplTrait: Trait, + >( + x: ImplTrait, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + x.method::(value_TypeArg, value_Type); + } + + fn associated_function_caller< + MethodTypeArg, + TypeArg, + const ConstArg: usize, + const MethodConstArg: usize, + ImplTrait: Trait, + >( + x: ImplTrait, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + ImplTrait::associated_function::( + x, + value_TypeArg, + value_Type, + ); } }