From 6c776408738d441ee4efac9dcccaab53cdbfd738 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 20 Jun 2024 10:35:06 +0200 Subject: [PATCH 1/3] fix(engine/fstar): fixes #719 --- engine/backends/fstar/fstar_backend.ml | 10 +-- ...oolchain__attribute-opaque into-fstar.snap | 4 +- .../toolchain__attributes into-fstar.snap | 9 +-- .../toolchain__generics into-fstar.snap | 25 +++---- .../toolchain__include-flag into-fstar.snap | 4 +- .../toolchain__loops into-fstar.snap | 73 +++++++++---------- ..._mut-ref-functionalization into-fstar.snap | 44 +++++------ .../toolchain__naming into-fstar.snap | 6 +- .../toolchain__side-effects into-fstar.snap | 2 +- .../toolchain__traits into-fstar.snap | 71 +++++++++--------- 10 files changed, 121 insertions(+), 127 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2ec0f58d8..7866c05c8 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -458,7 +458,7 @@ struct |> List.map ~f:(function | GConst const -> (pexpr const, F.AST.Nothing) | GLifetime _ -> . - | GType ty -> (pty e.span ty, F.AST.Hash)) + | GType ty -> (pty e.span ty, F.AST.Nothing)) in let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in F.mk_app (pexpr f) (generic_args @ args) @@ -626,7 +626,7 @@ struct type kind = Implicit | Tcresolve | Explicit type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term } - let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t + let of_generic_param ?(kind : kind = Explicit) span (p : generic_param) : t = let ident = plocal_ident p.ident in match p.kind with @@ -641,8 +641,8 @@ struct let typ = c_trait_goal span goal in { kind = Tcresolve; ident = F.id name; typ } - let of_generics ?(kind : kind = Implicit) span generics : t list = - List.map ~f:(of_generic_param ~kind span) generics.params + let of_generics ?(kind : kind = Explicit) span generics : t list = + List.map ~f:(of_generic_param ~kind:Explicit span) generics.params @ List.mapi ~f:(of_generic_constraint span) generics.constraints let of_typ span (nth : int) typ : t = @@ -1166,7 +1166,7 @@ struct ~f:(fun i -> let name = U.Concrete_ident_view.to_definition_name i.ti_ident in let generics = - FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics + FStarBinder.of_generics ~kind:Explicit i.ti_span i.ti_generics in let bds = generics |> List.map ~f:FStarBinder.to_binder in let fields = 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..d4868435a 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 eda0b67cf..a08ea4488 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); @@ -172,8 +172,8 @@ let t_NoE = x: Alloc.String.t_String { let _, out:(Core.Str.Iter.t_Chars & bool) = - Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars - (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string) + Core.Iter.Traits.Iterator.f_any Core.Str.Iter.t_Chars + (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref Alloc.String.t_String x <: string) <: Core.Str.Iter.t_Chars) (fun ch -> @@ -183,8 +183,7 @@ let t_NoE = ~.out } let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy = - (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +! - (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8) + (Hax_lib.f_get (t_BoundedU8 12uy 15uy) x <: u8) +! (Hax_lib.f_get (t_BoundedU8 10uy 11uy) y <: u8) <: t_BoundedU8 1uy 23uy diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index db8f3cd46..d13b45a4d 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -45,7 +45,7 @@ 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) = { @@ -63,11 +63,8 @@ let impl_Foo_for_usize: t_Foo usize = 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) - (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 dup (v_T: Type0) (#[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 @@ -75,14 +72,14 @@ let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3 let g (v_N: usize) - (#v_T: Type0) + (v_T: Type0) (#[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 - (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N) - (Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N) - (Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N) + (Core.Option.impl__unwrap_or usize + (Core.Iter.Traits.Iterator.f_max (Core.Array.Iter.t_IntoIter usize v_N) + (Core.Iter.Traits.Collect.f_into_iter (t_Array usize v_N) + (Core.Convert.f_into v_T (t_Array usize v_N) arr <: t_Array usize v_N) <: Core.Array.Iter.t_IntoIter usize v_N) <: @@ -94,7 +91,7 @@ let g let call_g (_: Prims.unit) : usize = (g (sz 3) - #(t_Array usize (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); Rust_primitives.Hax.array_of_list 3 list) @@ -105,7 +102,7 @@ let call_g (_: Prims.unit) : 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 + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN } <: @@ -122,7 +119,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = let repeat (v_LEN: usize) - (#v_T: Type0) + (v_T: Type0) (#[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 a4ce27894..703ee4730 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -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 @@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () } /// Entrypoint let main (_: Prims.unit) : Prims.unit = - let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in + let _:Prims.unit = main_a t_Foo (Foo <: t_Foo) in let _:Prims.unit = main_b () in let _:Prims.unit = main_c () in () diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 169518fc5..17a373143 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -40,14 +40,14 @@ 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 acc:usize = sz 0 in let chunks:Core.Slice.Iter.t_ChunksExact usize = - Core.Slice.impl__chunks_exact #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) + Core.Slice.impl__chunks_exact usize + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) v_CHUNK_LEN in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_ChunksExact usize) - (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks + (Core.Clone.f_clone (Core.Slice.Iter.t_ChunksExact usize) chunks <: Core.Slice.Iter.t_ChunksExact usize) <: @@ -58,7 +58,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global let chunk:t_Slice usize = chunk in let mean:usize = sz 0 in let mean:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize) chunk <: Core.Slice.Iter.t_Iter usize) @@ -72,8 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global acc) in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) - (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize) + (Core.Slice.Iter.impl_87__remainder usize chunks <: t_Slice usize) <: Core.Slice.Iter.t_Iter usize) acc @@ -87,10 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global let composed_range (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize) - #(Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_chain (Core.Ops.Range.t_Range usize) + (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } <: Core.Ops.Range.t_Range usize) @@ -117,11 +117,11 @@ let composed_range (n: usize) : usize = let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) - (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize) - (Core.Slice.impl__chunks #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Chunks usize) + (Core.Slice.impl__chunks usize + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) (sz 4) @@ -135,10 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc temp_1_ -> let acc:usize = acc in let i, chunk:(usize & t_Slice usize) = temp_1_ in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize)) - (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize) + (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Iter usize) + (Core.Slice.impl__iter usize chunk <: Core.Slice.Iter.t_Iter usize) <: Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize)) <: @@ -155,8 +155,7 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let f (_: Prims.unit) : u8 = let acc:u8 = 0uy in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8 - ) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8) <: Core.Ops.Range.t_Range u8) @@ -171,10 +170,10 @@ let f (_: Prims.unit) : u8 = let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Slice.impl__iter usize + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) <: @@ -192,10 +191,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Slice.impl__iter usize + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) <: @@ -206,9 +205,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc item -> let acc:usize = acc in let item:usize = item in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item } <: Core.Ops.Range.t_Range usize) @@ -221,12 +220,12 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = acc in let i:usize = i in let acc:usize = acc +! sz 1 in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Zip.t_Zip (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize) - #(Core.Ops.Range.t_Range usize) - (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_zip (Core.Slice.Iter.t_Iter usize) + (Core.Ops.Range.t_Range usize) + (Core.Slice.impl__iter usize + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) @@ -254,7 +253,7 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) arr <: @@ -270,7 +269,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize let range1 (_: Prims.unit) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 } <: @@ -288,7 +287,7 @@ let range1 (_: Prims.unit) : usize = let range2 (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize } <: @@ -306,9 +305,9 @@ let range2 (n: usize) : usize = let rev_range (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } <: Core.Ops.Range.t_Range 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 76f5002cd..a17972835 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 @@ -45,15 +45,15 @@ let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) = x let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy + Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 1uy in let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy + Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 2uy in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in vec let h (x: u8) : u8 = @@ -83,8 +83,8 @@ let k (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec #u8 - #Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec u8 + Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) @@ -95,8 +95,8 @@ let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit = let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec #u8 - #Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec u8 + Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -108,7 +108,7 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.Monomorphized_update_at.update_at_range v x - (Core.Slice.impl__copy_from_slice #u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8) + (Core.Slice.impl__copy_from_slice u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8) in let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v (sz 1) 3uy @@ -121,7 +121,7 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 = ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 } <: Core.Ops.Range.t_Range usize) - (Core.Slice.impl__copy_from_slice #u8 + (Core.Slice.impl__copy_from_slice u8 (x.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 } <: Core.Ops.Range.t_Range usize ] @@ -138,10 +138,10 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 = 42uy let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in + let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec #u8 - #Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec u8 + Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) @@ -152,14 +152,14 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = in let tmp0, tmp1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Alloc.Vec.impl_1__append #u8 #Alloc.Alloc.t_Global vec1 vec2 + Alloc.Vec.impl_1__append u8 Alloc.Alloc.t_Global vec1 vec2 in let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp0 in let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp1 in let _:Prims.unit = () in let vec1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Alloc.Vec.impl_1__append #u8 - #Alloc.Alloc.t_Global + Alloc.Vec.impl_1__append u8 + Alloc.Alloc.t_Global vec1 (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in @@ -195,7 +195,7 @@ let impl__S__update (self: t_S) (x: u8) : t_S = let foo (lhs rhs: t_S) : t_S = let lhs:t_S = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 } <: @@ -243,7 +243,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: @@ -258,7 +258,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) x with f_a = - Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i + Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global x.f_a i <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } @@ -266,14 +266,14 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } + { x with f_a = Core.Slice.impl__swap u8 x.f_a (sz 0) (sz 1) } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = { x with - f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + f_b = { x.f_b with f_field = Core.Slice.impl__swap u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index 68c009f19..d07cb6cbc 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -43,8 +43,8 @@ let debug (label value: u32) : Prims.unit = t_Slice string) (Rust_primitives.unsize (let list = [ - Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument + Core.Fmt.Rt.impl_1__new_display u32 label <: Core.Fmt.Rt.t_Argument; + Core.Fmt.Rt.impl_1__new_display u32 value <: Core.Fmt.Rt.t_Argument ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); @@ -128,7 +128,7 @@ 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) + (v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) (_: Prims.unit) : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index f99f13441..f0a29b925 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -117,7 +117,7 @@ let local_mutation (x: u32) : u32 = let y:u32 = x /! 2ul in let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in let y:u32 = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u32) ({ Core.Ops.Range.f_start = 0ul; Core.Ops.Range.f_end = 10ul } <: diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 8047ce566..1f6d1158e 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -36,7 +36,7 @@ class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl - (#v_P: Type0) + (v_P: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8) : t_Trait v_P = { __marker_trait = () } ''' @@ -48,10 +48,10 @@ open FStar.Mul let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) + (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8) (fun temp_0_ -> let _:u8 = temp_0_ in @@ -63,9 +63,9 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range : Prims.unit = let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) it in () @@ -73,18 +73,18 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit = let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) + (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8 ) (fun i -> let i:u8 = i in let _, out:(Core.Slice.Iter.t_Iter u8 & bool) = - Core.Iter.Traits.Iterator.f_any #(Core.Slice.Iter.t_Iter u8) - (Core.Slice.impl__iter #u8 - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list + Core.Iter.Traits.Iterator.f_any (Core.Slice.Iter.t_Iter u8) + (Core.Slice.impl__iter u8 + (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list <: t_Slice u8) <: @@ -111,9 +111,9 @@ class t_Foo (v_Self: Type0) (v_T: Type0) = { 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 + let _:u8 = f_to_t v_X u8 x in () ''' "Traits.Implicit_dependencies_issue_667_.Define_type.fst" = ''' @@ -170,7 +170,7 @@ let _ = () let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit = - Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType + Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType x ''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' @@ -185,8 +185,8 @@ class t_PolyOp (v_Self: Type0) = { 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) - : u32 = f_op #v_OP x x +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 @@ -208,7 +208,7 @@ let impl_1: t_PolyOp t_Times = f_op = fun (x: u32) (y: u32) -> x *! y } -let both (x: u32) : (u32 & u32) = twice #t_Plus x, twice #t_Times x <: (u32 & u32) +let both (x: u32) : (u32 & u32) = twice t_Plus x, twice t_Times x <: (u32 & u32) ''' "Traits.fst" = ''' module Traits @@ -222,8 +222,8 @@ class t_Bar (v_Self: Type0) = { 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) - : Prims.unit = f_bar #v_T x +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 @@ -281,35 +281,34 @@ class t_Foo (v_Self: Type0) = { } let closure_impl_expr - (#v_I: Type0) + (v_I: Type0) (#[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)) - #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit it (fun x -> x) + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) + (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_map v_I Prims.unit it (fun x -> x) <: Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) let closure_impl_expr_fngen - (#v_I #v_F: Type0) + (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) (it: v_I) (f: v_F) : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I v_F) - #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit #v_F it f - <: - Core.Iter.Adapters.Map.t_Map v_I v_F) + Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Map.t_Map v_I v_F) + (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_map v_I Prims.unit v_F it f <: 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 _:Prims.unit = f_assoc_f #v_T () in - f_method_f #v_T x +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) - : u32 = f_function_of_super_trait #i1.f_AssocType x +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 = @@ -322,7 +321,7 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit = f_assoc_f = (fun (_: Prims.unit) -> () <: Prims.unit); f_method_f_pre = (fun (self: Prims.unit) -> true); f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true); - f_method_f = (fun (self: Prims.unit) -> f_assoc_f #Prims.unit ()); + f_method_f = (fun (self: Prims.unit) -> f_assoc_f Prims.unit ()); f_assoc_type_pre = (fun (_: i32) -> true); f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true); f_assoc_type = fun (_: i32) -> () From 8dc62bec888183e2f498c5cb38d081cca4e6fe2e Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 20 Jun 2024 14:21:31 +0200 Subject: [PATCH 2/3] Revert "fix(engine/fstar): fixes #719" This reverts commit 6c776408738d441ee4efac9dcccaab53cdbfd738. --- engine/backends/fstar/fstar_backend.ml | 10 +-- ...oolchain__attribute-opaque into-fstar.snap | 4 +- .../toolchain__attributes into-fstar.snap | 9 ++- .../toolchain__generics into-fstar.snap | 25 ++++--- .../toolchain__include-flag into-fstar.snap | 4 +- .../toolchain__loops into-fstar.snap | 73 ++++++++++--------- ..._mut-ref-functionalization into-fstar.snap | 44 +++++------ .../toolchain__naming into-fstar.snap | 6 +- .../toolchain__side-effects into-fstar.snap | 2 +- .../toolchain__traits into-fstar.snap | 71 +++++++++--------- 10 files changed, 127 insertions(+), 121 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 7866c05c8..2ec0f58d8 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -458,7 +458,7 @@ struct |> List.map ~f:(function | GConst const -> (pexpr const, F.AST.Nothing) | GLifetime _ -> . - | GType ty -> (pty e.span ty, F.AST.Nothing)) + | GType ty -> (pty e.span ty, F.AST.Hash)) in let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in F.mk_app (pexpr f) (generic_args @ args) @@ -626,7 +626,7 @@ struct type kind = Implicit | Tcresolve | Explicit type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term } - let of_generic_param ?(kind : kind = Explicit) span (p : generic_param) : t + let of_generic_param ?(kind : kind = Implicit) span (p : generic_param) : t = let ident = plocal_ident p.ident in match p.kind with @@ -641,8 +641,8 @@ struct let typ = c_trait_goal span goal in { kind = Tcresolve; ident = F.id name; typ } - let of_generics ?(kind : kind = Explicit) span generics : t list = - List.map ~f:(of_generic_param ~kind:Explicit span) generics.params + let of_generics ?(kind : kind = Implicit) span generics : t list = + List.map ~f:(of_generic_param ~kind span) generics.params @ List.mapi ~f:(of_generic_constraint span) generics.constraints let of_typ span (nth : int) typ : t = @@ -1166,7 +1166,7 @@ struct ~f:(fun i -> let name = U.Concrete_ident_view.to_definition_name i.ti_ident in let generics = - FStarBinder.of_generics ~kind:Explicit i.ti_span i.ti_generics + FStarBinder.of_generics ~kind:Implicit i.ti_span i.ti_generics in let bds = generics |> List.map ~f:FStarBinder.to_binder in let fields = 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 d4868435a..3e5e8e8fb 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 a08ea4488..eda0b67cf 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); @@ -172,8 +172,8 @@ let t_NoE = x: Alloc.String.t_String { let _, out:(Core.Str.Iter.t_Chars & bool) = - Core.Iter.Traits.Iterator.f_any Core.Str.Iter.t_Chars - (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref Alloc.String.t_String x <: string) + Core.Iter.Traits.Iterator.f_any #Core.Str.Iter.t_Chars + (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String x <: string) <: Core.Str.Iter.t_Chars) (fun ch -> @@ -183,7 +183,8 @@ let t_NoE = ~.out } let bounded_u8 (x: t_BoundedU8 12uy 15uy) (y: t_BoundedU8 10uy 11uy) : t_BoundedU8 1uy 23uy = - (Hax_lib.f_get (t_BoundedU8 12uy 15uy) x <: u8) +! (Hax_lib.f_get (t_BoundedU8 10uy 11uy) y <: u8) + (Hax_lib.f_get #(t_BoundedU8 12uy 15uy) x <: u8) +! + (Hax_lib.f_get #(t_BoundedU8 10uy 11uy) y <: u8) <: t_BoundedU8 1uy 23uy diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index d13b45a4d..db8f3cd46 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -45,7 +45,7 @@ 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) = { @@ -63,8 +63,11 @@ let impl_Foo_for_usize: t_Foo usize = 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) (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 dup + (#v_T: Type0) + (#[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 @@ -72,14 +75,14 @@ let call_f (_: Prims.unit) : usize = (f (sz 10) (sz 3) <: usize) +! sz 3 let g (v_N: usize) - (v_T: Type0) + (#v_T: Type0) (#[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 - (Core.Iter.Traits.Iterator.f_max (Core.Array.Iter.t_IntoIter usize v_N) - (Core.Iter.Traits.Collect.f_into_iter (t_Array usize v_N) - (Core.Convert.f_into v_T (t_Array usize v_N) arr <: t_Array usize v_N) + (Core.Option.impl__unwrap_or #usize + (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N) + (Core.Iter.Traits.Collect.f_into_iter #(t_Array usize v_N) + (Core.Convert.f_into #v_T #(t_Array usize v_N) arr <: t_Array usize v_N) <: Core.Array.Iter.t_IntoIter usize v_N) <: @@ -91,7 +94,7 @@ let g let call_g (_: Prims.unit) : usize = (g (sz 3) - (t_Array usize (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); Rust_primitives.Hax.array_of_list 3 list) @@ -102,7 +105,7 @@ let call_g (_: Prims.unit) : 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 + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN } <: @@ -119,7 +122,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = let repeat (v_LEN: usize) - (v_T: Type0) + (#v_T: Type0) (#[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 703ee4730..a4ce27894 100644 --- a/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__include-flag into-fstar.snap @@ -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 @@ -80,7 +80,7 @@ let impl_Trait_for_Foo: t_Trait t_Foo = { __marker_trait = () } /// Entrypoint let main (_: Prims.unit) : Prims.unit = - let _:Prims.unit = main_a t_Foo (Foo <: t_Foo) in + let _:Prims.unit = main_a #t_Foo (Foo <: t_Foo) in let _:Prims.unit = main_b () in let _:Prims.unit = main_c () in () diff --git a/test-harness/src/snapshots/toolchain__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index 17a373143..169518fc5 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -40,14 +40,14 @@ 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 acc:usize = sz 0 in let chunks:Core.Slice.Iter.t_ChunksExact usize = - Core.Slice.impl__chunks_exact usize - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) + Core.Slice.impl__chunks_exact #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) v_CHUNK_LEN in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_ChunksExact + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_ChunksExact usize) - (Core.Clone.f_clone (Core.Slice.Iter.t_ChunksExact usize) chunks + (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks <: Core.Slice.Iter.t_ChunksExact usize) <: @@ -58,7 +58,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global let chunk:t_Slice usize = chunk in let mean:usize = sz 0 in let mean:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) chunk <: Core.Slice.Iter.t_Iter usize) @@ -72,8 +72,8 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global acc) in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (t_Slice usize) - (Core.Slice.Iter.impl_87__remainder usize chunks <: t_Slice usize) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) + (Core.Slice.Iter.impl_87__remainder #usize chunks <: t_Slice usize) <: Core.Slice.Iter.t_Iter usize) acc @@ -87,10 +87,10 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global let composed_range (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Chain.t_Chain + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Chain.t_Chain (Core.Ops.Range.t_Range usize) (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_chain (Core.Ops.Range.t_Range usize) - (Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize) + #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } <: Core.Ops.Range.t_Range usize) @@ -117,11 +117,11 @@ let composed_range (n: usize) : usize = let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Chunks usize)) - (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Chunks usize) - (Core.Slice.impl__chunks usize - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize) + (Core.Slice.impl__chunks #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) (sz 4) @@ -135,10 +135,10 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc temp_1_ -> let acc:usize = acc in let i, chunk:(usize & t_Slice usize) = temp_1_ in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Enumerate.t_Enumerate + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize)) - (Core.Iter.Traits.Iterator.f_enumerate (Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter usize chunk <: Core.Slice.Iter.t_Iter usize) + (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize) + (Core.Slice.impl__iter #usize chunk <: Core.Slice.Iter.t_Iter usize) <: Core.Iter.Adapters.Enumerate.t_Enumerate (Core.Slice.Iter.t_Iter usize)) <: @@ -155,7 +155,8 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let f (_: Prims.unit) : u8 = let acc:u8 = 0uy in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range u8) + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8 + ) ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8) <: Core.Ops.Range.t_Range u8) @@ -170,10 +171,10 @@ let f (_: Prims.unit) : u8 = let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter usize - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Slice.impl__iter #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) <: @@ -191,10 +192,10 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Slice.Iter.t_Iter + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter usize) - (Core.Slice.impl__iter usize - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Slice.impl__iter #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) <: @@ -205,9 +206,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = (fun acc item -> let acc:usize = acc in let item:usize = item in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item } <: Core.Ops.Range.t_Range usize) @@ -220,12 +221,12 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = acc in let i:usize = i in let acc:usize = acc +! sz 1 in - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Zip.t_Zip + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Zip.t_Zip (Core.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_zip (Core.Slice.Iter.t_Iter usize) - (Core.Ops.Range.t_Range usize) - (Core.Slice.impl__iter usize - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize) + #(Core.Ops.Range.t_Range usize) + (Core.Slice.impl__iter #usize + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr <: t_Slice usize) @@ -253,7 +254,7 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Alloc.Vec.t_Vec + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) arr <: @@ -269,7 +270,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize let range1 (_: Prims.unit) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 } <: @@ -287,7 +288,7 @@ let range1 (_: Prims.unit) : usize = let range2 (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize } <: @@ -305,9 +306,9 @@ let range2 (n: usize) : usize = let rev_range (n: usize) : usize = let acc:usize = sz 0 in let acc:usize = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Iter.Adapters.Rev.t_Rev + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Iter.Adapters.Rev.t_Rev (Core.Ops.Range.t_Range usize)) - (Core.Iter.Traits.Iterator.f_rev (Core.Ops.Range.t_Range usize) + (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } <: Core.Ops.Range.t_Range 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 a17972835..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 @@ -45,15 +45,15 @@ let array (x: t_Array u8 (sz 10)) : t_Array u8 (sz 10) = x let f (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 1uy + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 1uy in let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global vec 2uy + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global vec 2uy in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in - let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in + let vec:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Core.Slice.impl__swap #u8 vec (sz 0) (sz 1) in vec let h (x: u8) : u8 = @@ -83,8 +83,8 @@ let k (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & u16 & Prims.unit & u64) let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec u8 - Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec #u8 + #Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) @@ -95,8 +95,8 @@ let build_vec (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.unit = let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec u8 - Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec #u8 + #Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 1); Rust_primitives.Hax.array_of_list 1 list) @@ -108,7 +108,7 @@ let index_mutation (x: Core.Ops.Range.t_Range usize) (a: t_Slice u8) : Prims.uni let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.Monomorphized_update_at.update_at_range v x - (Core.Slice.impl__copy_from_slice u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8) + (Core.Slice.impl__copy_from_slice #u8 (v.[ x ] <: t_Slice u8) a <: t_Slice u8) in let v:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Rust_primitives.Hax.Monomorphized_update_at.update_at_usize v (sz 1) 3uy @@ -121,7 +121,7 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 = ({ Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 } <: Core.Ops.Range.t_Range usize) - (Core.Slice.impl__copy_from_slice u8 + (Core.Slice.impl__copy_from_slice #u8 (x.[ { Core.Ops.Range.f_start = sz 4; Core.Ops.Range.f_end = sz 5 } <: Core.Ops.Range.t_Range usize ] @@ -138,10 +138,10 @@ let index_mutation_unsize (x: t_Array u8 (sz 12)) : u8 = 42uy let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new u8 () in + let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = Alloc.Vec.impl__new #u8 () in let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Alloc.Slice.impl__into_vec u8 - Alloc.Alloc.t_Global + Alloc.Slice.impl__into_vec #u8 + #Alloc.Alloc.t_Global (Rust_primitives.unsize (Rust_primitives.Hax.box_new (let list = [1uy; 2uy; 3uy] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 3); Rust_primitives.Hax.array_of_list 3 list) @@ -152,14 +152,14 @@ let test_append (_: Prims.unit) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = in let tmp0, tmp1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Alloc.Vec.impl_1__append u8 Alloc.Alloc.t_Global vec1 vec2 + Alloc.Vec.impl_1__append #u8 #Alloc.Alloc.t_Global vec1 vec2 in let vec1:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp0 in let vec2:Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = tmp1 in let _:Prims.unit = () in let vec1:(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global & Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Alloc.Vec.impl_1__append u8 - Alloc.Alloc.t_Global + Alloc.Vec.impl_1__append #u8 + #Alloc.Alloc.t_Global vec1 (build_vec () <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in @@ -195,7 +195,7 @@ let impl__S__update (self: t_S) (x: u8) : t_S = let foo (lhs rhs: t_S) : t_S = let lhs:t_S = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 } <: @@ -243,7 +243,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = x in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: @@ -258,7 +258,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) x with f_a = - Alloc.Vec.impl_1__push u8 Alloc.Alloc.t_Global x.f_a i + Alloc.Vec.impl_1__push #u8 #Alloc.Alloc.t_Global x.f_a i <: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global } @@ -266,14 +266,14 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = - { x with f_a = Core.Slice.impl__swap u8 x.f_a (sz 0) (sz 1) } + { x with f_a = Core.Slice.impl__swap #u8 x.f_a (sz 0) (sz 1) } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) in let x:t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = { x with - f_b = { x.f_b with f_field = Core.Slice.impl__swap u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo + f_b = { x.f_b with f_field = Core.Slice.impl__swap #u8 x.f_b.f_field (sz 0) (sz 1) } <: t_Foo } <: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index d07cb6cbc..68c009f19 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -43,8 +43,8 @@ let debug (label value: u32) : Prims.unit = t_Slice string) (Rust_primitives.unsize (let list = [ - Core.Fmt.Rt.impl_1__new_display u32 label <: Core.Fmt.Rt.t_Argument; - Core.Fmt.Rt.impl_1__new_display u32 value <: Core.Fmt.Rt.t_Argument + Core.Fmt.Rt.impl_1__new_display #u32 label <: Core.Fmt.Rt.t_Argument; + Core.Fmt.Rt.impl_1__new_display #u32 value <: Core.Fmt.Rt.t_Argument ] in FStar.Pervasives.assert_norm (Prims.eq2 (List.Tot.length list) 2); @@ -128,7 +128,7 @@ 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) + (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_FooTrait v_T) (_: Prims.unit) : usize = f_ASSOCIATED_CONSTANT +! v_INHERENT_CONSTANT diff --git a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index f0a29b925..f99f13441 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -117,7 +117,7 @@ let local_mutation (x: u32) : u32 = let y:u32 = x /! 2ul in let y:u32 = Core.Num.impl__u32__wrapping_add y 2ul in let y:u32 = - Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter (Core.Ops.Range.t_Range + Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u32) ({ Core.Ops.Range.f_start = 0ul; Core.Ops.Range.f_end = 10ul } <: diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 1f6d1158e..8047ce566 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -36,7 +36,7 @@ class t_Trait (v_Self: Type0) = { __marker_trait_t_Trait:Prims.unit } [@@ FStar.Tactics.Typeclasses.tcinstance] let impl - (v_P: Type0) + (#v_P: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i0: Core.Ops.Function.t_FnMut v_P u8) : t_Trait v_P = { __marker_trait = () } ''' @@ -48,10 +48,10 @@ open FStar.Mul let minimized_1_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8) + #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8) (fun temp_0_ -> let _:u8 = temp_0_ in @@ -63,9 +63,9 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range : Prims.unit = let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) it in () @@ -73,18 +73,18 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) : Prims.unit = let (v__indices: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global):Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Filter.t_Filter + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) - (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_filter (Core.Ops.Range.t_Range u8) + #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) ({ Core.Ops.Range.f_start = 0uy; Core.Ops.Range.f_end = 5uy } <: Core.Ops.Range.t_Range u8 ) (fun i -> let i:u8 = i in let _, out:(Core.Slice.Iter.t_Iter u8 & bool) = - Core.Iter.Traits.Iterator.f_any (Core.Slice.Iter.t_Iter u8) - (Core.Slice.impl__iter u8 - (Core.Ops.Deref.f_deref (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list + Core.Iter.Traits.Iterator.f_any #(Core.Slice.Iter.t_Iter u8) + (Core.Slice.impl__iter #u8 + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list <: t_Slice u8) <: @@ -111,9 +111,9 @@ class t_Foo (v_Self: Type0) (v_T: Type0) = { 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 + let _:u8 = f_to_t #v_X #u8 x in () ''' "Traits.Implicit_dependencies_issue_667_.Define_type.fst" = ''' @@ -170,7 +170,7 @@ let _ = () let some_function (x: Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType) : Prims.unit = - Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType + Traits.Implicit_dependencies_issue_667_.Trait_definition.f_my_method #Traits.Implicit_dependencies_issue_667_.Define_type.t_MyType x ''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' @@ -185,8 +185,8 @@ class t_PolyOp (v_Self: Type0) = { 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) : u32 = - f_op v_OP x x +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 @@ -208,7 +208,7 @@ let impl_1: t_PolyOp t_Times = f_op = fun (x: u32) (y: u32) -> x *! y } -let both (x: u32) : (u32 & u32) = twice t_Plus x, twice t_Times x <: (u32 & u32) +let both (x: u32) : (u32 & u32) = twice #t_Plus x, twice #t_Times x <: (u32 & u32) ''' "Traits.fst" = ''' module Traits @@ -222,8 +222,8 @@ class t_Bar (v_Self: Type0) = { 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) - : Prims.unit = f_bar v_T x +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 @@ -281,34 +281,35 @@ class t_Foo (v_Self: Type0) = { } let closure_impl_expr - (v_I: Type0) + (#v_I: Type0) (#[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)) - (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_map v_I Prims.unit it (fun x -> x) + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) + #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit it (fun x -> x) <: Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) let closure_impl_expr_fngen - (v_I v_F: Type0) + (#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) (it: v_I) (f: v_F) : Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global = - Core.Iter.Traits.Iterator.f_collect (Core.Iter.Adapters.Map.t_Map v_I v_F) - (Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) - (Core.Iter.Traits.Iterator.f_map v_I Prims.unit v_F it f <: Core.Iter.Adapters.Map.t_Map v_I v_F - ) + Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Map.t_Map v_I v_F) + #(Alloc.Vec.t_Vec Prims.unit Alloc.Alloc.t_Global) + (Core.Iter.Traits.Iterator.f_map #v_I #Prims.unit #v_F it f + <: + 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 _:Prims.unit = f_assoc_f v_T () in - f_method_f v_T x +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) - : u32 = f_function_of_super_trait i1.f_AssocType x +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 = @@ -321,7 +322,7 @@ let impl_Foo_for_tuple_: t_Foo Prims.unit = f_assoc_f = (fun (_: Prims.unit) -> () <: Prims.unit); f_method_f_pre = (fun (self: Prims.unit) -> true); f_method_f_post = (fun (self: Prims.unit) (out: Prims.unit) -> true); - f_method_f = (fun (self: Prims.unit) -> f_assoc_f Prims.unit ()); + f_method_f = (fun (self: Prims.unit) -> f_assoc_f #Prims.unit ()); f_assoc_type_pre = (fun (_: i32) -> true); f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true); f_assoc_type = fun (_: i32) -> () From a855b795763f2727049edcbdef1d611e778585e1 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Thu, 20 Jun 2024 14:39:16 +0200 Subject: [PATCH 3/3] fix(engine/fstar): uniformize implicits on traits --- engine/backends/fstar/fstar_backend.ml | 29 +++--- .../toolchain__attributes into-fstar.snap | 8 +- .../toolchain__generics into-fstar.snap | 4 +- .../toolchain__include-flag into-fstar.snap | 4 +- .../toolchain__interface-only into-fstar.snap | 4 +- ..._mut-ref-functionalization into-fstar.snap | 4 +- .../toolchain__naming into-fstar.snap | 16 ++-- .../toolchain__traits into-fstar.snap | 95 ++++++++++++++++--- tests/traits/src/lib.rs | 13 +++ 9 files changed, 130 insertions(+), 47 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2ec0f58d8..2926e6d0b 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -407,6 +407,18 @@ struct (* in *) F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange)) + and fun_application ~span f args generic_args = + let generic_args = + generic_args + |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true) + |> List.map ~f:(function + | GConst const -> (pexpr const, F.AST.Nothing) + | GLifetime _ -> . + | GType ty -> (pty span ty, F.AST.Hash)) + in + let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in + F.mk_app f (generic_args @ args) + and pexpr_unwrapped (e : expr) = match e.e with | Literal l -> pliteral_as_expr e.span l @@ -452,16 +464,7 @@ struct chars: '" ^ s ^ "'"); F.AST.Const (F.Const.Const_int (s, None)) |> F.term | App { f; args; generic_args; bounds_impls = _; impl = _ } -> - let generic_args = - generic_args - |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true) - |> List.map ~f:(function - | GConst const -> (pexpr const, F.AST.Nothing) - | GLifetime _ -> . - | GType ty -> (pty e.span ty, F.AST.Hash)) - in - let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in - F.mk_app (pexpr f) (generic_args @ args) + fun_application ~span:e.span (pexpr f) args generic_args | If { cond; then_; else_ } -> F.term @@ F.AST.If @@ -1156,7 +1159,7 @@ struct | Trait { name; generics; items } -> let bds = List.map - ~f:FStarBinder.(of_generic_param ~kind:Explicit e.span >> to_binder) + ~f:FStarBinder.(of_generic_param e.span >> to_binder) generics.params in let name_str = U.Concrete_ident_view.to_definition_name name in @@ -1293,9 +1296,9 @@ struct @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics) in let typ = - F.mk_e_app + fun_application ~span:e.span (F.term @@ F.AST.Name (pglobal_ident e.span trait)) - (List.map ~f:(pgeneric_value e.span) generic_args) + [] generic_args in let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in let fields = diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index eda0b67cf..d49db0fb5 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); diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index db8f3cd46..33d524da6 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -48,7 +48,7 @@ open FStar.Mul 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) = { +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 @@ -56,7 +56,7 @@ class t_Foo (v_Self: Type0) = { } [@@ 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); 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 a4ce27894..39e2269d3 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 = () @@ -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 b3a95740d..e4173e16e 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__mut-ref-functionalization into-fstar.snap b/test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap index 76f5002cd..d01460536 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 68c009f19..9162f2abc 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -108,22 +108,22 @@ 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 @@ -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 8047ce566..36079953d 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -32,13 +32,13 @@ module Traits.For_clauses.Issue_495_.Minimized_3_ 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 = () } + : t_Trait #v_P = { __marker_trait = () } ''' "Traits.For_clauses.Issue_495_.fst" = ''' module Traits.For_clauses.Issue_495_ @@ -105,7 +105,7 @@ 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) @@ -132,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 = @@ -150,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 @@ -173,13 +173,80 @@ 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.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) = { + f_fun_pre: + 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_FunType: Type0 -> + t_Array v_FooType v_FooConst -> + t_Array v_FunType v_FunConst -> + Prims.unit + -> bool; + f_fun: + 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) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +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_FunType: Type0) + (x: t_Array v_FooType v_FooConst) + (y: t_Array v_FunType v_FunConst) + -> + true); + f_fun_post + = + (fun + (v_FunConst: usize) + (#v_FunType: Type0) + (x: t_Array v_FooType v_FooConst) + (y: t_Array v_FunType v_FunConst) + (out: Prims.unit) + -> + true); + f_fun + = + fun + (v_FunConst: usize) + (#v_FunType: Type0) + (x: t_Array v_FooType v_FooConst) + (y: t_Array v_FunType v_FunConst) + -> + () + } + +type t_Bar (v_FooConst: usize) (v_FooType: Type0) = + | Bar : t_Array v_FooType v_FooConst -> t_Bar v_FooConst v_FooType +''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' module Traits.Unconstrainted_types_issue_677_ #set-options "--fuel 0 --ifuel 1 --z3rlimit 15" 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) @@ -191,7 +258,7 @@ let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp 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); @@ -201,7 +268,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); @@ -216,7 +283,7 @@ 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) @@ -234,7 +301,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; @@ -242,7 +309,7 @@ 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) = { +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; @@ -253,7 +320,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); @@ -261,7 +328,7 @@ 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; @@ -312,7 +379,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x : 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 9821c42d0..1d01124ef 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -163,3 +163,16 @@ mod implicit_dependencies_issue_667 { } } } + +// Related to issue 719 +mod interlaced_consts_types { + struct Bar([FooType; FooConst]); + + trait Foo { + fn fun(x: [FooType; FooConst], y: [FunType; FunConst]); + } + + impl Foo for SelfType { + fn fun(x: [FooType; FooConst], y: [FunType; FunConst]) {} + } +}