Skip to content

Commit

Permalink
fix(engine/fstar): fix super typeclasses attributes
Browse files Browse the repository at this point in the history 
The PR #902 was reverted by #909 because #902 was generated redundant
fields names in classes for super clauses, which is a problem for F*.

This PR changes the naming scheme of super clauses for typeclasses in
F*. Those names now take into account the trait name. The super trait
names are now a 5 characters base 62 encoding of the hash of the
predicate ID concatenated with the trait name.

Fixes #630.
  • Loading branch information
@W95Psp
W95Psp committed Sep 23, 2024
1 parent 288f77f commit 66a1a6e
Show file tree
Hide file tree
Showing 5 changed files with 92 additions and 21 deletions.
1 change: 1 addition & 0 deletions engine/backends/fstar/fstar_ast.ml
View file
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
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
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
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
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 {}
}

0 comments on commit 66a1a6e

Please sign in to comment.