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

Jump to bottom

fix(engine/fstar): fix super typeclasses attributes #910

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

fix(engine/fstar): fix super typeclasses attributes #910

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
1 change: 1 addition & 0 deletions engine/backends/fstar/fstar_ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,6 +32,7 @@ let pat (pat : AST.pattern') = AST.{ pat; prange = dummyRange }

module Attrs = struct
let no_method = term @@ AST.Var FStar_Parser_Const.no_method_lid
let tcinstance = term @@ AST.Var FStar_Parser_Const.tcinstance_lid
end

let tcresolve = term @@ AST.Var FStar_Parser_Const.tcresolve_lid
Expand Down
30 changes: 22 additions & 8 deletions engine/backends/fstar/fstar_backend.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -339,6 +339,12 @@ struct
in
F.mk_e_abs [ pat ] (F.mk_e_app trait args)

and name_of_super_clause (trait_goal : trait_goal) (base_name : string) =
String.hash
(U.Concrete_ident_view.to_definition_name trait_goal.trait
^ "*" ^ base_name)
|> base62_of_int 5 |> ( ^ ) "_super_"

and pimpl_expr span (ie : impl_expr) =
let some = Option.some in
let hax_unstable_impl_exprs = false in
Expand All @@ -353,7 +359,7 @@ struct
pimpl_expr span impl
| Parent { impl; ident } when hax_unstable_impl_exprs ->
let* impl = pimpl_expr span impl in
let trait = "_super_" ^ ident.name in
let trait = name_of_super_clause ident.goal ident.name in
F.term @@ F.AST.Project (impl, F.lid [ trait ]) |> some
| ImplApp { impl; args = [] } when hax_unstable_impl_exprs ->
pimpl_expr span impl
Expand Down Expand Up @@ -1158,7 +1164,7 @@ struct
:: List.map
~f:
(fun {
goal = { trait; args };
goal = { trait; args } as goal;
name = impl_ident_name;
} ->
let base =
Expand All @@ -1167,10 +1173,11 @@ struct
let args =
List.map ~f:(pgeneric_value e.span) args
in
( F.id (name ^ "_" ^ impl_ident_name),
( F.id
(name ^ name_of_super_clause goal impl_ident_name),
(* Dodgy concatenation *)
None,
[],
[ F.Attrs.tcinstance ],
F.mk_e_app base args ))
bounds
| TIFn ty
Expand Down Expand Up @@ -1363,9 +1370,9 @@ struct
|> List.filter_map ~f:(fun c ->
match c with
| GCType { goal = bound; name = id } ->
let name = "_super_" ^ id in
let name = name_of_super_clause bound id in
let typ = pgeneric_constraint_type e.span c in
Some (F.id name, None, [ F.Attrs.no_method ], typ)
Some (F.id name, None, [ F.Attrs.tcinstance ], typ)
| GCProjection _ ->
(* TODO: Not yet implemented, see https://github.com/hacspec/hax/issues/785 *)
None
Expand Down Expand Up @@ -1436,14 +1443,21 @@ struct
(F.lid [ name ], pty ii_span typ)
:: List.map
~f:(fun (_impl_expr, impl_ident) ->
(F.lid [ name ^ "_" ^ impl_ident.name ], F.tc_solve))
( F.lid
[
name
^ name_of_super_clause impl_ident.goal
impl_ident.name;
],
F.tc_solve ))
parent_bounds)
items
in
let parent_bounds_fields =
List.map
~f:(fun (_impl_expr, impl_ident) ->
(F.lid [ "_super_" ^ impl_ident.name ], F.tc_solve))
( F.lid [ name_of_super_clause impl_ident.goal impl_ident.name ],
F.tc_solve ))
parent_bounds
in
let fields = parent_bounds_fields @ fields in
Expand Down
17 changes: 17 additions & 0 deletions engine/lib/utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -108,6 +108,23 @@ include (
(** Generates a temporary file path that ends with `suffix` *)
end)

(** Formats an integer as base 62 *)
let base62_of_int len : int -> string =
let alphabet =
"0123456789ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"
in
let max = String.length alphabet in
fun n ->
let n = ref n in
let f _i =
let i = !n % max in
n := !n / max;
String.get alphabet i
in
let arr = Array.init len ~f in
Array.rev_inplace arr;
String.of_array arr

module List = struct
include Base.List

Expand Down
56 changes: 43 additions & 13 deletions test-harness/src/snapshots/toolchain__traits into-fstar.snap
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -35,11 +35,11 @@ open FStar.Mul
class t_BlockSizeUser (v_Self: Type0) = { f_BlockSize:Type0 }

class t_ParBlocksSizeUser (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_10960599340086055385:t_BlockSizeUser v_Self
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_U5QdG:t_BlockSizeUser v_Self
}

class t_BlockBackend (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_15949286759387124191:t_ParBlocksSizeUser v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sNdEU:t_ParBlocksSizeUser v_Self;
f_proc_block_pre:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Type0;
f_proc_block_post:Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global -> Prims.unit -> Type0;
f_proc_block:x0: Alloc.Vec.t_Vec _ Alloc.Alloc.t_Global
Expand Down Expand Up @@ -329,11 +329,11 @@ let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg
}

class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_8779313392680198588:t_Trait v_Self
v_TypeArg
v_ConstArg;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_cyxbI:t_Trait v_Self v_TypeArg v_ConstArg;
f_AssocType:Type0;
f_AssocType_6369404467997533198:t_Trait f_AssocType v_TypeArg v_ConstArg
[@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_6oYyd:t_Trait f_AssocType
v_TypeArg
v_ConstArg
}

let associated_function_caller
Expand Down Expand Up @@ -454,14 +454,44 @@ open FStar.Mul

class t_Trait1 (v_Self: Type0) = {
f_T:Type0;
f_T_1640036513185240095:t_Trait1 f_T
[@@@ FStar.Tactics.Typeclasses.tcinstance]f_T_super_OOsUn:t_Trait1 f_T
}

class t_Trait2 (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_4567617955834163411:t_Trait1 v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_ev6bP:t_Trait1 v_Self;
f_U:Type0
}
'''
"Traits.Super_clauses_names.fst" = '''
module Traits.Super_clauses_names
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

class t_A (v_Self: Type0) = { __marker_trait_t_A:Prims.unit }

class t_B (v_Self: Type0) = { __marker_trait_t_B:Prims.unit }

class t_C (v_Self: Type0) = { __marker_trait_t_C:Prims.unit }

class t_ChildTrait1 (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self
}

class t_ChildTrait2 (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self
}

class t_ChildTrait3 (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_9FQrt:t_A v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_sXIun:t_B v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_C3uwc:t_C v_Self
}
'''
"Traits.Type_alias_bounds_issue_707_.fst" = '''
module Traits.Type_alias_bounds_issue_707_
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
Expand Down Expand Up @@ -541,7 +571,7 @@ class t_Lang (v_Self: Type0) = {
}

class t_SuperTrait (v_Self: Type0) = {
[@@@ FStar.Tactics.Typeclasses.no_method]_super_9442900250278684536:Core.Clone.t_Clone v_Self;
[@@@ FStar.Tactics.Typeclasses.tcinstance]_super_ex7xP:Core.Clone.t_Clone v_Self;
f_function_of_super_trait_pre:v_Self -> Type0;
f_function_of_super_trait_post:v_Self -> u32 -> Type0;
f_function_of_super_trait:x0: v_Self
Expand All @@ -553,16 +583,16 @@ class t_SuperTrait (v_Self: Type0) = {
[@@ FStar.Tactics.Typeclasses.tcinstance]
let impl_SuperTrait_for_i32: t_SuperTrait i32 =
{
_super_9442900250278684536 = FStar.Tactics.Typeclasses.solve;
_super_ex7xP = FStar.Tactics.Typeclasses.solve;
f_function_of_super_trait_pre = (fun (self: i32) -> true);
f_function_of_super_trait_post = (fun (self: i32) (out: u32) -> true);
f_function_of_super_trait = fun (self: i32) -> cast (Core.Num.impl__i32__abs self <: i32) <: u32
}

class t_Foo (v_Self: Type0) = {
f_AssocType:Type0;
f_AssocType_15525962639250476383:t_SuperTrait f_AssocType;
f_AssocType_17265963849229885182:Core.Clone.t_Clone f_AssocType;
[@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_SntST:t_SuperTrait f_AssocType;
[@@@ FStar.Tactics.Typeclasses.tcinstance]f_AssocType_super_LqPiP:Core.Clone.t_Clone f_AssocType;
f_N:usize;
f_assoc_f_pre:Prims.unit -> Type0;
f_assoc_f_post:Prims.unit -> Prims.unit -> Type0;
Expand Down Expand Up @@ -621,7 +651,7 @@ let g (#v_T: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_Foo v_T) (x
let impl_Foo_for_tuple_: t_Foo Prims.unit =
{
f_AssocType = i32;
f_AssocType_15525962639250476383 = FStar.Tactics.Typeclasses.solve;
f_AssocType_super_SntST = FStar.Tactics.Typeclasses.solve;
f_N = sz 32;
f_assoc_f_pre = (fun (_: Prims.unit) -> true);
f_assoc_f_post = (fun (_: Prims.unit) (out: Prims.unit) -> true);
Expand Down
9 changes: 9 additions & 0 deletions tests/traits/src/lib.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,3 +276,12 @@ mod recursive_trait_with_assoc_type {
type U;
}
}

mod super_clauses_names {
trait A {}
trait B {}
trait C {}
trait ChildTrait1: A + B + C {}
trait ChildTrait2: A + B + C {}
trait ChildTrait3: A + B + C {}
}
Loading