Skip to content

Commit

Permalink
fix(engine/fstar): fixes #719
Browse files Browse the repository at this point in the history
  • Loading branch information
Lucas Franceschino authored and W95Psp committed Jun 20, 2024
1 parent d10f891 commit 6c77640
Show file tree
Hide file tree
Showing 10 changed files with 121 additions and 127 deletions.
10 changes: 5 additions & 5 deletions engine/backends/fstar/fstar_backend.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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
Expand All @@ -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 =
Expand Down Expand Up @@ -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 =
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
'''
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down Expand Up @@ -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 ->
Expand All @@ -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

Expand Down
25 changes: 11 additions & 14 deletions test-harness/src/snapshots/toolchain__generics into-fstar.snap
Original file line number Diff line number Diff line change
Expand Up @@ -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) = {
Expand All @@ -63,26 +63,23 @@ 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

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)
<:
Expand All @@ -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)
Expand All @@ -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 }
<:
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
()
Expand Down
73 changes: 36 additions & 37 deletions test-harness/src/snapshots/toolchain__loops into-fstar.snap
Original file line number Diff line number Diff line change
Expand Up @@ -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)
<:
Expand All @@ -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)
Expand All @@ -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
Expand All @@ -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)
Expand All @@ -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)
Expand All @@ -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))
<:
Expand All @@ -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)
Expand All @@ -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)
<:
Expand All @@ -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)
<:
Expand All @@ -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)
Expand All @@ -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)
Expand Down Expand Up @@ -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
<:
Expand All @@ -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 }
<:
Expand All @@ -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 }
<:
Expand All @@ -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)
Expand Down
Loading

0 comments on commit 6c77640

Please sign in to comment.