Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

fix(engine/fstar): fix implicit discrepancies in traits #726

Merged
merged 3 commits into from
Jun 24, 2024
Merged

fix(engine/fstar): fix implicit discrepancies in traits #726

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
6c77640
fix(engine/fstar): fixes #719
Jun 20, 2024
8dc62be
Revert "fix(engine/fstar): fixes #719"
Jun 20, 2024
a855b79
fix(engine/fstar): uniformize implicits on traits
Jun 20, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 16 additions & 13 deletions engine/backends/fstar/fstar_backend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 =
Expand Down
8 changes: 4 additions & 4 deletions test-harness/src/snapshots/toolchain__attributes into-fstar.snap
View file
Open in desktop
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 All @@ -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));
Expand All @@ -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
Expand Down Expand Up @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__generics into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,15 +48,15 @@ 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
-> Prims.Pure usize (f_const_add_pre v_N x0) (fun result -> f_const_add_post v_N x0 result)
}

[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_Foo_for_usize: t_Foo usize =
let impl_Foo_for_usize: t_Foo #usize =
{
f_const_add_pre = (fun (v_N: usize) (self: usize) -> true);
f_const_add_post = (fun (v_N: usize) (self: usize) (out: usize) -> true);
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__include-flag into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = ()
Expand Down Expand Up @@ -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 =
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__interface-only into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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);
Expand Down
4 changes: 2 additions & 2 deletions test-harness/src/snapshots/toolchain__mut-ref-functionalization into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down Expand Up @@ -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);
Expand Down
16 changes: 8 additions & 8 deletions test-harness/src/snapshots/toolchain__naming into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand All @@ -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
Expand Down
Loading
Loading