From 049d638cf2c57835e3a9f115fd6c7336e2b082af Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Mon, 8 Jul 2024 15:07:58 +0200 Subject: [PATCH 1/6] feat(engine): propagate trait-specific generics --- engine/backends/fstar/fstar_backend.ml | 12 +++++---- engine/lib/ast.ml | 2 +- engine/lib/ast_utils.ml | 27 ++++++++++--------- engine/lib/import_thir.ml | 24 +++++++---------- engine/lib/phases/phase_direct_and_mut.ml | 17 +++++++----- engine/lib/phases/phase_drop_references.ml | 11 ++++---- .../phase_reconstruct_question_marks.ml | 2 +- .../phases/phase_simplify_question_marks.ml | 2 +- engine/lib/phases/phase_specialize.ml | 2 +- engine/lib/side_effect_utils.ml | 4 +-- engine/lib/subtype.ml | 7 ++--- 11 files changed, 56 insertions(+), 54 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 2926e6d0b..5f4ecd7ca 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -407,7 +407,7 @@ struct (* in *) F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange)) - and fun_application ~span f args generic_args = + and fun_application ~span f args trait_generic_args generic_args = let generic_args = generic_args |> List.filter ~f:(function GType (TArrow _) -> false | _ -> true) @@ -449,7 +449,7 @@ struct { f = { e = GlobalVar f; _ }; args = [ { e = Literal (String s); _ } ]; - generic_args; + generic_args = _; } when Global_ident.eq_name Hax_lib__int__Impl_5___unsafe_from_str f -> (match @@ -463,8 +463,10 @@ struct @@ "pexpr: expected a integer, found the following non-digit \ chars: '" ^ s ^ "'"); F.AST.Const (F.Const.Const_int (s, None)) |> F.term - | App { f; args; generic_args; bounds_impls = _; impl = _ } -> - fun_application ~span:e.span (pexpr f) args generic_args + | App { f; args; generic_args; bounds_impls = _; trait } -> + fun_application ~span:e.span (pexpr f) args + (Option.map ~f:snd trait |> Option.value ~default:[]) + generic_args | If { cond; then_; else_ } -> F.term @@ F.AST.If @@ -1298,7 +1300,7 @@ struct let typ = fun_application ~span:e.span (F.term @@ F.AST.Name (pglobal_ident e.span trait)) - [] generic_args + [] [] generic_args in let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in let fields = diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index aff2e8901..268edc818 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -200,7 +200,7 @@ functor args : expr list (* ; f_span: span *); generic_args : generic_value list; bounds_impls : impl_expr list; - impl : impl_expr option; + trait : (impl_expr * generic_value list) option; } | Literal of literal | Array of expr list diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index 5f688e280..c5dcba702 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -79,8 +79,9 @@ module Make (F : Features.T) = struct * impl_expr list) option = match e.e with - | App { f; args; generic_args; impl; bounds_impls } -> - Some (f, args, generic_args, impl, bounds_impls) + | App { f; args; generic_args; trait; bounds_impls } -> + (* TODO: propagate full trait *) + Some (f, args, generic_args, Option.map ~f:fst trait, bounds_impls) | _ -> None let pbinding_simple (p : pat) : (local_ident * ty) option = @@ -96,7 +97,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar (`Concrete f'); _ }; args = [ e ]; generic_args = _; - impl = _; + trait = _; _; (* TODO: see issue #328 *) } @@ -201,7 +202,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar (`Primitive Deref); _ }; args = [ { e = Borrow { e = sub; _ }; _ } ]; generic_args = _; - impl = _; + trait = _; _; (* TODO: see issue #328 *) } -> @@ -343,7 +344,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar (`Primitive Cast); _ } as f; args = [ arg ]; generic_args; - impl; + trait; bounds_impls; } -> ascribe @@ -355,7 +356,7 @@ module Make (F : Features.T) = struct f; args = [ ascribe arg ]; generic_args; - impl; + trait; bounds_impls; }; } @@ -875,7 +876,7 @@ module Make (F : Features.T) = struct args; generic_args = []; bounds_impls = []; - impl; + trait = Option.map ~f:(fun impl -> (impl, [])) impl; }; typ = ret_typ; span; @@ -924,7 +925,7 @@ module Make (F : Features.T) = struct args = [ e ]; generic_args = _; bounds_impls = _; - impl = _; + trait = _; } -> next e | _ -> e @@ -960,7 +961,7 @@ module Make (F : Features.T) = struct args = [ e ]; generic_args = []; bounds_impls = []; - impl = None (* TODO: see issue #328 *); + trait = None (* TODO: see issue #328 *); }; typ; span; @@ -1060,7 +1061,7 @@ module Make (F : Features.T) = struct args = [ tuple ]; generic_args = [] (* TODO: see issue #328 *); bounds_impls = []; - impl = None (* TODO: see issue #328 *); + trait = None (* TODO: see issue #328 *); }; } @@ -1104,7 +1105,7 @@ module Make (F : Features.T) = struct args = [ place ]; generic_args = _; bounds_impls = _; - impl = _; + trait = _; (* TODO: see issue #328 *) } -> let* place = of_expr place in @@ -1115,7 +1116,7 @@ module Make (F : Features.T) = struct args = [ place; index ]; generic_args = _; bounds_impls = _; - impl = _; + trait = _; (* TODO: see issue #328 *) } when Global_ident.eq_name Core__ops__index__Index__index f -> @@ -1128,7 +1129,7 @@ module Make (F : Features.T) = struct args = [ place; index ]; generic_args = _; bounds_impls = _; - impl = _; + trait = _; (* TODO: see issue #328 *) } when Global_ident.eq_name Core__ops__index__IndexMut__index_mut f -> diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 29dab0eb5..586fa94ab 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -198,7 +198,7 @@ let resugar_index_mut (e : expr) : (expr * expr) option = f = { e = GlobalVar (`Concrete meth); _ }; args = [ { e = Borrow { e = x; _ }; _ }; index ]; generic_args = _ (* TODO: see issue #328 *); - impl = _ (* TODO: see issue #328 *); + trait = _ (* TODO: see issue #328 *); bounds_impls = _; } when Concrete_ident.eq_name Core__ops__index__IndexMut__index_mut meth -> @@ -208,7 +208,7 @@ let resugar_index_mut (e : expr) : (expr * expr) option = f = { e = GlobalVar (`Concrete meth); _ }; args = [ x; index ]; generic_args = _ (* TODO: see issue #328 *); - impl = _ (* TODO: see issue #328 *); + trait = _ (* TODO: see issue #328 *); bounds_impls = _; } when Concrete_ident.eq_name Core__ops__index__Index__index meth -> @@ -378,7 +378,7 @@ end) : EXPR = struct f; args = List.map ~f:c_expr args; generic_args = []; - impl = None; + trait = None; bounds_impls = []; } in @@ -435,13 +435,8 @@ end) : EXPR = struct } -> let args = List.map ~f:c_expr args in let bounds_impls = List.map ~f:(c_impl_expr e.span) bounds_impls in - let trait_generic_args = - Option.map ~f:snd trait |> Option.value ~default:[] - in - let generic_args = - List.map ~f:(c_generic_value e.span) - (trait_generic_args @ generic_args) - in + let c_generic_values = List.map ~f:(c_generic_value e.span) in + let generic_args = c_generic_values generic_args in let f = let f = c_expr fun' in match (trait, fun'.contents) with @@ -456,7 +451,8 @@ end) : EXPR = struct args; generic_args; bounds_impls; - impl = Option.map ~f:(fst >> c_impl_expr e.span) trait; + trait = + Option.map ~f:(c_impl_expr e.span *** c_generic_values) trait; } | Box { value } -> (U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e @@ -596,7 +592,7 @@ end) : EXPR = struct f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; args = [ lhs ]; generic_args = [] (* TODO: see issue #328 *); - impl = None (* TODO: see issue #328 *); + trait = None (* TODO: see issue #328 *); bounds_impls = []; } | TupleField { lhs; field } -> @@ -613,7 +609,7 @@ end) : EXPR = struct f = { e = projector; typ = TArrow ([ lhs.typ ], typ); span }; args = [ lhs ]; generic_args = [] (* TODO: see issue #328 *); - impl = None (* TODO: see issue #328 *); + trait = None (* TODO: see issue #328 *); bounds_impls = []; } | GlobalName { id } -> GlobalVar (def_id Value id) @@ -749,7 +745,7 @@ end) : EXPR = struct }; args = [ e ]; generic_args = _; - impl = _; + trait = _; bounds_impls = _; (* TODO: see issue #328 *) } -> diff --git a/engine/lib/phases/phase_direct_and_mut.ml b/engine/lib/phases/phase_direct_and_mut.ml index 1348c711a..03af8bb3e 100644 --- a/engine/lib/phases/phase_direct_and_mut.ml +++ b/engine/lib/phases/phase_direct_and_mut.ml @@ -101,7 +101,8 @@ struct and translate_app (span : span) (otype : A.ty) (f : A.expr) (raw_args : A.expr list) (generic_args : B.generic_value list) - (impl : B.impl_expr option) bounds_impls : B.expr = + (trait : (B.impl_expr * B.generic_value list) option) bounds_impls : + B.expr = (* `otype` and `_otype` (below) are supposed to be the same type, but sometimes `_otype` is less precise (i.e. an associated type while a concrete type is available) *) @@ -140,7 +141,7 @@ struct let args = List.map ~f:dexpr raw_args in B. { - e = B.App { f; args; generic_args; impl; bounds_impls }; + e = B.App { f; args; generic_args; trait; bounds_impls }; typ; span; } @@ -219,7 +220,8 @@ struct B. { e = - App { f; args = unmut_args; generic_args; impl; bounds_impls }; + App + { f; args = unmut_args; generic_args; trait; bounds_impls }; typ = pat.typ; span = pat.span; } @@ -269,11 +271,12 @@ struct and dexpr_unwrapped (expr : A.expr) : B.expr = let span = expr.span in match expr.e with - | App { f; args; generic_args; impl; bounds_impls } -> - let generic_args = List.map ~f:(dgeneric_value span) generic_args in - let impl = Option.map ~f:(dimpl_expr span) impl in + | App { f; args; generic_args; trait; bounds_impls } -> + let dgeneric_args = List.map ~f:(dgeneric_value span) in + let generic_args = dgeneric_args generic_args in + let trait = Option.map ~f:(dimpl_expr span *** dgeneric_args) trait in let bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls in - translate_app span expr.typ f args generic_args impl bounds_impls + translate_app span expr.typ f args generic_args trait bounds_impls | _ -> let e = dexpr' span expr.e in B.{ e; typ = dty expr.span expr.typ; span = expr.span } diff --git a/engine/lib/phases/phase_drop_references.ml b/engine/lib/phases/phase_drop_references.ml index 8bdd29ff2..cfcec417f 100644 --- a/engine/lib/phases/phase_drop_references.ml +++ b/engine/lib/phases/phase_drop_references.ml @@ -111,15 +111,14 @@ struct body = dexpr body; captures = List.map ~f:dexpr captures; } - | App { f; args; generic_args; impl; bounds_impls } -> + | App { f; args; generic_args; trait; bounds_impls } -> let f = dexpr f in let args = List.map ~f:dexpr args in - let impl = Option.map ~f:(dimpl_expr span) impl in - let generic_args = - List.filter_map ~f:(dgeneric_value span) generic_args - in + let dgeneric_args = List.filter_map ~f:(dgeneric_value span) in + let trait = Option.map ~f:(dimpl_expr span *** dgeneric_args) trait in + let generic_args = dgeneric_args generic_args in let bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls in - App { f; args; generic_args; impl; bounds_impls } + App { f; args; generic_args; trait; bounds_impls } | _ -> . [@@inline_ands bindings_of dexpr - dbinding_mode] diff --git a/engine/lib/phases/phase_reconstruct_question_marks.ml b/engine/lib/phases/phase_reconstruct_question_marks.ml index c5f0c855a..86cec7e96 100644 --- a/engine/lib/phases/phase_reconstruct_question_marks.ml +++ b/engine/lib/phases/phase_reconstruct_question_marks.ml @@ -113,7 +113,7 @@ module%inlined_contents Make (FA : Features.T) = struct { f = { e = GlobalVar f }; args = [ { e = LocalVar residual_var; _ } ]; - impl = Some impl; + trait = Some (impl, _); }; typ = return_typ; _; diff --git a/engine/lib/phases/phase_simplify_question_marks.ml b/engine/lib/phases/phase_simplify_question_marks.ml index 7426b15b9..03ea555bb 100644 --- a/engine/lib/phases/phase_simplify_question_marks.ml +++ b/engine/lib/phases/phase_simplify_question_marks.ml @@ -136,7 +136,7 @@ module%inlined_contents Make (FA : Features.T) = struct { f = { e = GlobalVar f }; args = [ { e = LocalVar residual_var; _ } ]; - impl = Some impl; + trait = Some (impl, _); }; typ = return_typ; _; diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index fc8021dd1..a3bde5b6f 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -134,7 +134,7 @@ module Make (F : Features.T) = { f; args = l; - impl = None; + trait = None; generic_args = []; bounds_impls = []; }; diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index 44799d3e0..aefa25663 100644 --- a/engine/lib/side_effect_utils.ml +++ b/engine/lib/side_effect_utils.ml @@ -347,7 +347,7 @@ struct m#plus (m#plus (no_lbs ethen) (no_lbs eelse)) effects in ({ e with e = If { cond; then_; else_ } }, effects)) - | App { f; args; generic_args; impl; bounds_impls } -> + | App { f; args; generic_args; trait; bounds_impls } -> HoistSeq.many env (List.map ~f:(self#visit_expr env) (f :: args)) (fun l effects -> @@ -358,7 +358,7 @@ struct in ( { e with - e = App { f; args; generic_args; impl; bounds_impls }; + e = App { f; args; generic_args; trait; bounds_impls }; }, effects )) | Literal _ -> (e, m#zero) diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index f58487482..95354fa7f 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -157,14 +157,15 @@ struct then_ = dexpr then_; else_ = Option.map ~f:dexpr else_; } - | App { f; args; generic_args; bounds_impls; impl } -> + | App { f; args; generic_args; bounds_impls; trait } -> + let dgeneric_values = List.map ~f:(dgeneric_value span) in App { f = dexpr f; args = List.map ~f:dexpr args; - generic_args = List.map ~f:(dgeneric_value span) generic_args; + generic_args = dgeneric_values generic_args; bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls; - impl = Option.map ~f:(dimpl_expr span) impl; + trait = Option.map ~f:(dimpl_expr span *** dgeneric_values) trait; } | Literal lit -> Literal lit | Array l -> Array (List.map ~f:dexpr l) From b1ca060abb7fecaa0373b310e0ab3de541e02069 Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 9 Jul 2024 08:59:01 +0200 Subject: [PATCH 2/6] feat(engine/f*): propagate trait-specific generics --- .../fstar-surface-ast/FStar_Parser_Const.ml | 2 + engine/backends/fstar/fstar_ast.ml | 1 + engine/backends/fstar/fstar_backend.ml | 100 +++++++++++------- 3 files changed, 65 insertions(+), 38 deletions(-) diff --git a/engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml b/engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml index dcfbcc9f9..ccbbeae43 100644 --- a/engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml +++ b/engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml @@ -499,6 +499,8 @@ let (mk_class_lid : FStar_Ident.lid) = fstar_tactics_lid' ["Typeclasses"; "mk_class"] let (tcresolve_lid : FStar_Ident.lid) = fstar_tactics_lid' ["Typeclasses"; "tcresolve"] +let (solve_lid : FStar_Ident.lid) = + fstar_tactics_lid' ["Typeclasses"; "solve"] let (tcclass_lid : FStar_Ident.lid) = fstar_tactics_lid' ["Typeclasses"; "tcclass"] let (tcinstance_lid : FStar_Ident.lid) = diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml index 2352ae732..a3b5a6cae 100644 --- a/engine/backends/fstar/fstar_ast.ml +++ b/engine/backends/fstar/fstar_ast.ml @@ -35,6 +35,7 @@ module Attrs = struct end let tcresolve = term @@ AST.Var FStar_Parser_Const.tcresolve_lid +let solve = term @@ AST.Var FStar_Parser_Const.solve_lid let pat_var_tcresolve (var : string option) = let tcresolve = Some (AST.Meta tcresolve) in diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index 5f4ecd7ca..db89c2435 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -407,17 +407,25 @@ struct (* in *) F.term @@ F.AST.Const (F.Const.Const_string ("failure", F.dummyRange)) - and fun_application ~span f args trait_generic_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) + and fun_application ~span f args ~trait_generic_args ~generic_args = + let pgeneric_args ?qualifier = + let qualifier_or default = Option.value ~default qualifier in + List.filter ~f:(function GType (TArrow _) -> false | _ -> true) + >> List.map ~f:(function + | GConst const -> (pexpr const, qualifier_or F.AST.Nothing) | GLifetime _ -> . - | GType ty -> (pty span ty, F.AST.Hash)) + | GType ty -> (pty span ty, qualifier_or F.AST.Hash)) in let args = List.map ~f:(pexpr &&& Fn.const F.AST.Nothing) args in - F.mk_app f (generic_args @ args) + let trait_generic_args = + Option.map + ~f: + (pgeneric_args ~qualifier:F.AST.Hash + >> Fn.flip ( @ ) [ (F.solve, F.AST.Hash) ]) + trait_generic_args + |> Option.value ~default:[] + in + F.mk_app f (trait_generic_args @ pgeneric_args generic_args @ args) and pexpr_unwrapped (e : expr) = match e.e with @@ -464,9 +472,9 @@ struct chars: '" ^ s ^ "'"); F.AST.Const (F.Const.Const_int (s, None)) |> F.term | App { f; args; generic_args; bounds_impls = _; trait } -> - fun_application ~span:e.span (pexpr f) args - (Option.map ~f:snd trait |> Option.value ~default:[]) - generic_args + let trait_generic_args = Option.map ~f:snd trait in + fun_application (pexpr f) args ~span:e.span ~trait_generic_args + ~generic_args | If { cond; then_; else_ } -> F.term @@ F.AST.If @@ -631,12 +639,14 @@ 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 make_explicit x = { x with kind = Explicit } + let make_implicit x = { x with kind = Implicit } + + let of_generic_param span (p : generic_param) : t = let ident = plocal_ident p.ident in match p.kind with | GPLifetime _ -> Error.assertion_failure span "pgeneric_param:LIFETIME" - | GPType { default = _ } -> { kind; typ = F.type0_term; ident } + | GPType { default = _ } -> { kind = Implicit; typ = F.type0_term; ident } | GPConst { typ } -> { kind = Explicit; typ = pty span typ; ident } let of_generic_constraint span (nth : int) (c : generic_constraint) = @@ -646,8 +656,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 span generics : t list = + List.map ~f:(of_generic_param span) generics.params @ List.mapi ~f:(of_generic_constraint span) generics.constraints let of_typ span (nth : int) typ : t = @@ -678,17 +688,24 @@ struct let to_term (x : t) : F.AST.term = F.term @@ F.AST.Var (FStar_Ident.lid_of_ns_and_id [] (to_ident x)) + let to_imp (x : t) : F.AST.imp = + match x.kind with Tcresolve | Implicit -> Hash | Explicit -> Nothing + + let to_qualified_term : t -> F.AST.term * F.AST.imp = to_term &&& to_imp + + let to_qualifier (x : t) : F.AST.arg_qualifier option = + match x.kind with + | Tcresolve -> Some TypeClassArg + | Implicit -> Some Implicit + | Explicit -> None + let to_binder (x : t) : F.AST.binder = F.AST. { b = F.AST.Annotated (x.ident, x.typ); brange = F.dummyRange; blevel = Un; - aqual = - (match x.kind with - | Tcresolve -> Some TypeClassArg - | Implicit -> Some Implicit - | Explicit -> None); + aqual = to_qualifier x; battributes = []; } end @@ -1016,7 +1033,8 @@ struct [ F.AST.TyconRecord ( F.id @@ U.Concrete_ident_view.to_definition_name name, - FStarBinder.of_generics ~kind:Explicit e.span generics + FStarBinder.of_generics e.span generics + |> List.map ~f:FStarBinder.make_explicit |> List.map ~f:FStarBinder.to_binder, None, [], @@ -1082,7 +1100,8 @@ struct [ F.AST.TyconVariant ( F.id @@ U.Concrete_ident_view.to_definition_name name, - FStarBinder.of_generics ~kind:Explicit e.span generics + FStarBinder.of_generics e.span generics + |> List.map ~f:FStarBinder.make_explicit |> List.map ~f:FStarBinder.to_binder, None, constructors ); @@ -1159,20 +1178,13 @@ struct | _ -> unsupported_macro ()) | _ -> unsupported_macro ()) | Trait { name; generics; items } -> - let bds = - List.map - ~f:FStarBinder.(of_generic_param e.span >> to_binder) - generics.params - in let name_str = U.Concrete_ident_view.to_definition_name name in let name_id = F.id @@ name_str in let fields = List.concat_map ~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 - in + let generics = FStarBinder.of_generics i.ti_span i.ti_generics in let bds = generics |> List.map ~f:FStarBinder.to_binder in let fields = match i.ti_v with @@ -1214,14 +1226,16 @@ struct let inputs = generics @ inputs in let output = pty e.span output in let ty_pre_post = - let inputs = List.map ~f:FStarBinder.to_term inputs in + let inputs = + List.map ~f:FStarBinder.to_qualified_term inputs + in let add_pre n = n ^ "_pre" in let pre_name_str = U.Concrete_ident_view.to_definition_name (Concrete_ident.Create.map_last ~f:add_pre i.ti_ident) in let pre = - F.mk_e_app (F.term_of_lid [ pre_name_str ]) inputs + F.mk_app (F.term_of_lid [ pre_name_str ]) inputs in let result = F.term_of_lid [ "result" ] in let add_post n = n ^ "_post" in @@ -1230,9 +1244,9 @@ struct (Concrete_ident.Create.map_last ~f:add_post i.ti_ident) in let post = - F.mk_e_app + F.mk_app (F.term_of_lid [ post_name_str ]) - (inputs @ [ result ]) + (inputs @ [ (result, Nothing) ]) in let post = F.mk_e_abs @@ -1279,7 +1293,17 @@ struct [ (F.id marker_field, None, [], pty e.span U.unit_typ) ] else fields in - let tcdef = F.AST.TyconRecord (name_id, bds, None, [], fields) in + let tcdef = + (* Binders are explicit on class definitions *) + let bds = + List.map + ~f: + FStarBinder.( + of_generic_param e.span >> make_explicit >> to_binder) + generics.params + in + F.AST.TyconRecord (name_id, bds, None, [], fields) + in let d = F.AST.Tycon (false, true, [ tcdef ]) in [ `Intf { d; drange = F.dummyRange; quals = []; attrs = [] } ] | Impl @@ -1298,9 +1322,9 @@ struct @@ F.AST.PatApp (pat, List.map ~f:FStarBinder.to_pattern generics) in let typ = - fun_application ~span:e.span + F.mk_e_app (F.term @@ F.AST.Name (pglobal_ident e.span trait)) - [] [] generic_args + (List.map ~f:(pgeneric_value e.span) generic_args) in let pat = F.pat @@ F.AST.PatAscribed (pat, (typ, None)) in let fields = From 64a1f39a1e428f39b9e0f6c57d04aef8f528700e Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 9 Jul 2024 09:04:44 +0200 Subject: [PATCH 3/6] test(engine/f*): propagate trait-specific generics --- .../toolchain__attributes into-fstar.snap | 15 +- .../toolchain__generics into-fstar.snap | 17 +- .../toolchain__include-flag into-fstar.snap | 4 +- .../toolchain__interface-only into-fstar.snap | 4 +- .../toolchain__loops into-fstar.snap | 44 ++- ..._mut-ref-functionalization into-fstar.snap | 6 +- .../toolchain__naming into-fstar.snap | 16 +- .../toolchain__side-effects into-fstar.snap | 9 +- .../toolchain__traits into-fstar.snap | 258 +++++++++++++++--- tests/traits/src/lib.rs | 71 +++++ 10 files changed, 383 insertions(+), 61 deletions(-) diff --git a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap index 5dc67c499..d2f995865 100644 --- a/test-harness/src/snapshots/toolchain__attributes into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__attributes into-fstar.snap @@ -72,7 +72,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); @@ -89,7 +89,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)); @@ -98,7 +98,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 @@ -141,7 +141,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); @@ -183,7 +183,12 @@ let t_NoE = 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) + #FStar.Tactics.Typeclasses.solve + (Core.Str.impl__str__chars (Core.Ops.Deref.f_deref #Alloc.String.t_String + #FStar.Tactics.Typeclasses.solve + x + <: + string) <: Core.Str.Iter.t_Chars) (fun ch -> diff --git a/test-harness/src/snapshots/toolchain__generics into-fstar.snap b/test-harness/src/snapshots/toolchain__generics into-fstar.snap index 054403fb6..ce160e3e5 100644 --- a/test-harness/src/snapshots/toolchain__generics into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__generics into-fstar.snap @@ -46,7 +46,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 @@ -54,7 +54,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); @@ -65,7 +65,11 @@ 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) + : (v_T & v_T) = + Core.Clone.f_clone #v_T #FStar.Tactics.Typeclasses.solve x, + Core.Clone.f_clone #v_T #FStar.Tactics.Typeclasses.solve x + <: + (v_T & v_T) let f (v_N x: usize) : usize = (v_N +! v_N <: usize) +! x @@ -79,8 +83,12 @@ let g : usize = (Core.Option.impl__unwrap_or #usize (Core.Iter.Traits.Iterator.f_max #(Core.Array.Iter.t_IntoIter usize v_N) + #FStar.Tactics.Typeclasses.solve (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) + #FStar.Tactics.Typeclasses.solve + (Core.Convert.f_into #v_T #(t_Array usize v_N) #FStar.Tactics.Typeclasses.solve arr + <: + t_Array usize v_N) <: Core.Array.Iter.t_IntoIter usize v_N) <: @@ -105,6 +113,7 @@ let foo (v_LEN: usize) (arr: t_Array usize v_LEN) : usize = let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = v_LEN } <: Core.Ops.Range.t_Range usize) 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 39e2269d3..a4ce27894 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 9d23e9942..cf2674e03 100644 --- a/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__interface-only into-fstar.snap @@ -52,7 +52,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); @@ -63,7 +63,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__loops into-fstar.snap b/test-harness/src/snapshots/toolchain__loops into-fstar.snap index d4c2e2066..ca9d2fa70 100644 --- a/test-harness/src/snapshots/toolchain__loops into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__loops into-fstar.snap @@ -39,13 +39,20 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global 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.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + 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 usize) - (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) chunks + #FStar.Tactics.Typeclasses.solve + (Core.Clone.f_clone #(Core.Slice.Iter.t_ChunksExact usize) + #FStar.Tactics.Typeclasses.solve + chunks <: Core.Slice.Iter.t_ChunksExact usize) <: @@ -57,6 +64,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global 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) + #FStar.Tactics.Typeclasses.solve chunk <: Core.Slice.Iter.t_Iter usize) @@ -71,6 +79,7 @@ let chunks (v_CHUNK_LEN: usize) (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global in let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(t_Slice usize) + #FStar.Tactics.Typeclasses.solve (Core.Slice.Iter.impl_88__remainder #usize chunks <: t_Slice usize) <: Core.Slice.Iter.t_Iter usize) @@ -87,7 +96,9 @@ let composed_range (n: usize) : usize = let acc:usize = 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)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_chain #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve #(Core.Ops.Range.t_Range usize) ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n } <: @@ -117,9 +128,13 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = 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)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Chunks usize) + #FStar.Tactics.Typeclasses.solve (Core.Slice.impl__chunks #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + arr <: t_Slice usize) (sz 4) @@ -135,7 +150,9 @@ let enumerate_chunks (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = 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.Slice.Iter.t_Iter usize)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_enumerate #(Core.Slice.Iter.t_Iter usize) + #FStar.Tactics.Typeclasses.solve (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,6 +172,7 @@ 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 ) + #FStar.Tactics.Typeclasses.solve ({ 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,8 +189,11 @@ let iterator (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter usize) + #FStar.Tactics.Typeclasses.solve (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + arr <: t_Slice usize) <: @@ -192,8 +213,11 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Slice.Iter.t_Iter usize) + #FStar.Tactics.Typeclasses.solve (Core.Slice.impl__iter #usize - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) arr + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + arr <: t_Slice usize) <: @@ -206,7 +230,9 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = 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.Ops.Range.t_Range usize)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = item } <: Core.Ops.Range.t_Range usize) @@ -221,10 +247,13 @@ let nested (arr: Alloc.Vec.t_Vec usize Alloc.Alloc.t_Global) : usize = 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.Slice.Iter.t_Iter usize) (Core.Ops.Range.t_Range usize)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_zip #(Core.Slice.Iter.t_Iter usize) + #FStar.Tactics.Typeclasses.solve #(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) + #FStar.Tactics.Typeclasses.solve arr <: t_Slice usize) @@ -254,6 +283,7 @@ let pattern (arr: Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) : usize let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Alloc.Vec.t_Vec (usize & usize) Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve arr <: Alloc.Vec.Into_iter.t_IntoIter (usize & usize) Alloc.Alloc.t_Global) @@ -270,6 +300,7 @@ let range1 (_: Prims.unit) : usize = let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 15 } <: Core.Ops.Range.t_Range usize) @@ -288,6 +319,7 @@ let range2 (n: usize) : usize = let acc:usize = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = n +! sz 10 <: usize } <: Core.Ops.Range.t_Range usize) @@ -306,7 +338,9 @@ let rev_range (n: usize) : usize = let acc:usize = 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)) + #FStar.Tactics.Typeclasses.solve (Core.Iter.Traits.Iterator.f_rev #(Core.Ops.Range.t_Range usize) + #FStar.Tactics.Typeclasses.solve ({ 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 d01460536..492d1f7e8 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); @@ -197,6 +197,7 @@ 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 usize) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = sz 0; Core.Ops.Range.f_end = sz 1 } <: Core.Ops.Range.t_Range usize) @@ -245,6 +246,7 @@ let g (x: t_Pair (Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global)) 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 u8) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = 1uy; Core.Ops.Range.f_end = 10uy } <: Core.Ops.Range.t_Range u8) diff --git a/test-harness/src/snapshots/toolchain__naming into-fstar.snap b/test-harness/src/snapshots/toolchain__naming into-fstar.snap index 1da402b0f..4de303564 100644 --- a/test-harness/src/snapshots/toolchain__naming into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__naming into-fstar.snap @@ -104,22 +104,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 @@ -142,7 +142,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__side-effects into-fstar.snap b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap index 40618a18c..66de5587a 100644 --- a/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__side-effects into-fstar.snap @@ -50,7 +50,9 @@ let direct_result_question_mark_coercion (y: Core.Result.t_Result i8 u16) match y with | Core.Result.Result_Ok hoist1 -> Core.Result.Result_Ok hoist1 <: Core.Result.t_Result i8 u32 | Core.Result.Result_Err err -> - Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result i8 u32 + Core.Result.Result_Err (Core.Convert.f_from #FStar.Tactics.Typeclasses.solve err) + <: + Core.Result.t_Result i8 u32 /// Exercise early returns with control flow and loops let early_returns (x: u32) : u32 = @@ -117,6 +119,7 @@ let local_mutation (x: u32) : u32 = let y:u32 = Core.Iter.Traits.Iterator.f_fold (Core.Iter.Traits.Collect.f_into_iter #(Core.Ops.Range.t_Range u32) + #FStar.Tactics.Typeclasses.solve ({ Core.Ops.Range.f_start = 0ul; Core.Ops.Range.f_end = 10ul } <: Core.Ops.Range.t_Range u32) @@ -270,7 +273,9 @@ let question_mark (x: u32) : Core.Result.t_Result u32 u32 = | Core.Result.Result_Err err -> let! _:Prims.unit = Core.Ops.Control_flow.ControlFlow_Break - (Core.Result.Result_Err (Core.Convert.f_from err) <: Core.Result.t_Result u32 u32) + (Core.Result.Result_Err (Core.Convert.f_from #FStar.Tactics.Typeclasses.solve err) + <: + Core.Result.t_Result u32 u32) <: Core.Ops.Control_flow.t_ControlFlow (Core.Result.t_Result u32 u32) Prims.unit in diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 32b9dbe21..13c1c318a 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_ @@ -50,8 +50,10 @@ 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.Ops.Range.t_Range u8) (u8 -> bool)) + #FStar.Tactics.Typeclasses.solve #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) + #FStar.Tactics.Typeclasses.solve ({ 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 @@ -65,6 +67,7 @@ let minimized_2_ (it: Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range = Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + #FStar.Tactics.Typeclasses.solve #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) it in @@ -75,16 +78,21 @@ let original_function_from_495_ (list: Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) = Core.Iter.Traits.Iterator.f_collect #(Core.Iter.Adapters.Filter.t_Filter (Core.Ops.Range.t_Range u8) (u8 -> bool)) + #FStar.Tactics.Typeclasses.solve #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) (Core.Iter.Traits.Iterator.f_filter #(Core.Ops.Range.t_Range u8) + #FStar.Tactics.Typeclasses.solve ({ 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) + #FStar.Tactics.Typeclasses.solve (Core.Slice.impl__iter #u8 - (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) list + (Core.Ops.Deref.f_deref #(Alloc.Vec.t_Vec u8 Alloc.Alloc.t_Global) + #FStar.Tactics.Typeclasses.solve + list <: t_Slice u8) <: @@ -105,7 +113,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) @@ -113,7 +121,7 @@ class t_Foo (#v_Self: Type0) (#v_T: Type0) = { 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 #FStar.Tactics.Typeclasses.solve x in () ''' "Traits.Implicit_dependencies_issue_667_.Define_type.fst" = ''' @@ -132,7 +140,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 +158,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 @@ -171,15 +179,194 @@ 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 + #FStar.Tactics.Typeclasses.solve x ''' +"Traits.Implicit_explicit_calling_conventions.fst" = ''' +module Traits.Implicit_explicit_calling_conventions +#set-options "--fuel 0 --ifuel 1 --z3rlimit 15" +open Core +open FStar.Mul + +type t_Type (v_TypeArg: Type0) (v_ConstArg: usize) = { f_field:t_Array v_TypeArg v_ConstArg } + +class t_Trait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + f_method_pre: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg + -> bool; + f_method_post: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg -> + Prims.unit + -> bool; + f_method: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + x0: v_Self -> + x1: v_TypeArg -> + x2: t_Type v_TypeArg v_ConstArg + -> Prims.Pure Prims.unit + (f_method_pre #v_MethodTypeArg v_MethodConstArg x0 x1 x2) + (fun result -> f_method_post #v_MethodTypeArg v_MethodConstArg x0 x1 x2 result); + f_associated_function_pre: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg + -> bool; + f_associated_function_post: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + v_Self -> + v_TypeArg -> + t_Type v_TypeArg v_ConstArg -> + Prims.unit + -> bool; + f_associated_function: + #v_MethodTypeArg: Type0 -> + v_MethodConstArg: usize -> + x0: v_Self -> + x1: v_TypeArg -> + x2: t_Type v_TypeArg v_ConstArg + -> Prims.Pure Prims.unit + (f_associated_function_pre #v_MethodTypeArg v_MethodConstArg x0 x1 x2) + (fun result -> f_associated_function_post #v_MethodTypeArg v_MethodConstArg x0 x1 x2 result) +} + +[@@ FStar.Tactics.Typeclasses.tcinstance] +let impl (#v_TypeArg: Type0) (v_ConstArg: usize) : t_Trait Prims.unit v_TypeArg v_ConstArg = + { + f_method_pre + = + (fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + true); + f_method_post + = + (fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + (out: Prims.unit) + -> + true); + f_method + = + (fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + ()); + f_associated_function_pre + = + (fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + true); + f_associated_function_post + = + (fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + (out: Prims.unit) + -> + true); + f_associated_function + = + fun + (#v_MethodTypeArg: Type0) + (v_MethodConstArg: usize) + (v__self: Prims.unit) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + -> + () + } + +class t_SubTrait (v_Self: Type0) (v_TypeArg: Type0) (v_ConstArg: usize) = { + [@@@ FStar.Tactics.Typeclasses.no_method]_super_9139092951006237722:t_Trait v_Self + v_TypeArg + v_ConstArg; + f_AssocType:Type0; + f_AssocType_11967135072657554621:t_Trait f_AssocType v_TypeArg v_ConstArg +} + +let associated_function_caller + (#v_MethodTypeArg #v_TypeArg: Type0) + (v_ConstArg v_MethodConstArg: usize) + (#v_ImplTrait: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: t_Trait v_ImplTrait v_TypeArg v_ConstArg) + (x: v_ImplTrait) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + : Prims.unit = + let _:Prims.unit = + f_associated_function #v_ImplTrait + #v_TypeArg + #v_ConstArg + #FStar.Tactics.Typeclasses.solve + #v_MethodTypeArg + v_MethodConstArg + x + value_TypeArg + value_Type + in + () + +let method_caller + (#v_MethodTypeArg #v_TypeArg: Type0) + (v_ConstArg v_MethodConstArg: usize) + (#v_ImplTrait: Type0) + (#[FStar.Tactics.Typeclasses.tcresolve ()] i3: t_Trait v_ImplTrait v_TypeArg v_ConstArg) + (x: v_ImplTrait) + (value_TypeArg: v_TypeArg) + (value_Type: t_Type v_TypeArg v_ConstArg) + : Prims.unit = + let _:Prims.unit = + f_method #v_ImplTrait + #v_TypeArg + #v_ConstArg + #FStar.Tactics.Typeclasses.solve + #v_MethodTypeArg + v_MethodConstArg + x + value_TypeArg + value_Type + in + () +''' "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) = { +class t_Foo (v_Self: Type0) (v_FooConst: usize) (v_FooType: Type0) = { f_fun_pre: v_FunConst: usize -> #v_FunType: Type0 -> @@ -199,13 +386,12 @@ class t_Foo (#v_Self: Type0) (v_FooConst: usize) (#v_FooType: 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) + (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 = +let impl (v_FooConst: usize) (#v_FooType #v_SelfType: Type0) : t_Foo v_SelfType v_FooConst v_FooType = { f_fun_pre = @@ -246,7 +432,7 @@ module Traits.Type_alias_bounds_issue_707_ open Core open FStar.Mul -type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} = +type t_StructWithGenericBounds (v_T: Type0) (i1: Core.Clone.t_Clone v_T) = | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T ''' "Traits.Unconstrainted_types_issue_677_.fst" = ''' @@ -255,19 +441,19 @@ module Traits.Unconstrainted_types_issue_677_ 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) } let twice (#v_OP: Type0) (#[FStar.Tactics.Typeclasses.tcresolve ()] i1: t_PolyOp v_OP) (x: u32) - : u32 = f_op #v_OP x x + : u32 = f_op #v_OP #FStar.Tactics.Typeclasses.solve x x 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); @@ -277,7 +463,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); @@ -292,14 +478,14 @@ 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) } 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 + : Prims.unit = f_bar #v_T #FStar.Tactics.Typeclasses.solve x type t_Error = | Error_Fail : t_Error @@ -310,7 +496,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; @@ -318,7 +504,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; @@ -329,7 +515,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); @@ -337,7 +523,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; @@ -353,7 +539,9 @@ class t_Foo (#v_Self: Type0) = { f_assoc_type_pre:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> bool; f_assoc_type_post:{| i3: Core.Marker.t_Copy f_AssocType |} -> f_AssocType -> Prims.unit -> bool; f_assoc_type:{| i3: Core.Marker.t_Copy f_AssocType |} -> x0: f_AssocType - -> Prims.Pure Prims.unit (f_assoc_type_pre i3 x0) (fun result -> f_assoc_type_post i3 x0 result) + -> Prims.Pure Prims.unit + (f_assoc_type_pre #i3 x0) + (fun result -> f_assoc_type_post #i3 x0 result) } let closure_impl_expr @@ -362,8 +550,13 @@ let closure_impl_expr (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)) + #FStar.Tactics.Typeclasses.solve #(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_map #v_I + #FStar.Tactics.Typeclasses.solve + #Prims.unit + it + (fun x -> x) <: Core.Iter.Adapters.Map.t_Map v_I (Prims.unit -> Prims.unit)) @@ -375,20 +568,21 @@ let closure_impl_expr_fngen (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) + #FStar.Tactics.Typeclasses.solve #(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.Traits.Iterator.f_map #v_I #FStar.Tactics.Typeclasses.solve #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 _:Prims.unit = f_assoc_f #v_T #FStar.Tactics.Typeclasses.solve () in + f_method_f #v_T #FStar.Tactics.Typeclasses.solve 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 + : u32 = f_function_of_super_trait #i1.f_AssocType #FStar.Tactics.Typeclasses.solve 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; @@ -398,7 +592,9 @@ 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 #FStar.Tactics.Typeclasses.solve ()); f_assoc_type_pre = (fun (_: i32) -> true); f_assoc_type_post = (fun (_: i32) (out: Prims.unit) -> true); f_assoc_type = fun (_: i32) -> () diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 8920f2732..3d48dda4a 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -177,6 +177,77 @@ mod interlaced_consts_types { } } +// Related to issue 719 (after reopen) +mod implicit_explicit_calling_conventions { + struct Type { + field: [TypeArg; ConstArg], + } + + trait Trait { + fn method( + self, + value_TypeArg: TypeArg, + value_Type: Type, + ); + fn associated_function( + _self: Self, + value_TypeArg: TypeArg, + value_Type: Type, + ); + } + + impl Trait for () { + fn method( + self, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + } + fn associated_function( + _self: Self, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + } + } + + trait SubTrait: Trait { + type AssocType: Trait; + } + + fn method_caller< + MethodTypeArg, + TypeArg, + const ConstArg: usize, + const MethodConstArg: usize, + ImplTrait: Trait, + >( + x: ImplTrait, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + x.method::(value_TypeArg, value_Type); + } + + fn associated_function_caller< + MethodTypeArg, + TypeArg, + const ConstArg: usize, + const MethodConstArg: usize, + ImplTrait: Trait, + >( + x: ImplTrait, + value_TypeArg: TypeArg, + value_Type: Type, + ) { + ImplTrait::associated_function::( + x, + value_TypeArg, + value_Type, + ); + } +} + mod type_alias_bounds_issue_707 { struct StructWithGenericBounds(T); type SynonymA = StructWithGenericBounds; From e87b374f51f4a66671c1a678bd72542ab0fd6c0f Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Tue, 9 Jul 2024 10:04:40 +0200 Subject: [PATCH 4/6] fix(proof-libs/f*): `f_deref`: make it a typeclass --- proof-libs/fstar/core/Core.Ops.Deref.fst | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/proof-libs/fstar/core/Core.Ops.Deref.fst b/proof-libs/fstar/core/Core.Ops.Deref.fst index c99ea9e6d..15b5565ca 100644 --- a/proof-libs/fstar/core/Core.Ops.Deref.fst +++ b/proof-libs/fstar/core/Core.Ops.Deref.fst @@ -1,3 +1,12 @@ module Core.Ops.Deref -let f_deref = id +class t_Deref (t_Self: Type0) = { + f_Target: Type0; + f_deref: t_Self -> f_Target; +} + +unfold +instance identity_Deref t_Self: t_Deref t_Self = { + f_Target = t_Self; + f_deref = (fun x -> x); +} From 9f056df8e628ce2e0eabe98608be2adb96b1daea Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 10 Jul 2024 10:05:05 +0200 Subject: [PATCH 5/6] Update tests/traits/src/lib.rs Co-authored-by: Franziskus Kiefer --- tests/traits/src/lib.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/traits/src/lib.rs b/tests/traits/src/lib.rs index 3d48dda4a..4013b9f3d 100644 --- a/tests/traits/src/lib.rs +++ b/tests/traits/src/lib.rs @@ -177,7 +177,7 @@ mod interlaced_consts_types { } } -// Related to issue 719 (after reopen) +// Related to issue #719 (after reopen) mod implicit_explicit_calling_conventions { struct Type { field: [TypeArg; ConstArg], From a17cd49f0dc109063ed7cac7b0b4191213bffffd Mon Sep 17 00:00:00 2001 From: Lucas Franceschino Date: Wed, 10 Jul 2024 11:06:40 +0200 Subject: [PATCH 6/6] fix(engine/f*): `{| ... |}` for trait bounds on types --- engine/backends/fstar/fstar_backend.ml | 10 ++++++---- .../src/snapshots/toolchain__traits into-fstar.snap | 2 +- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index db89c2435..b9d4185b5 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/engine/backends/fstar/fstar_backend.ml @@ -640,7 +640,9 @@ struct type t = { kind : kind; ident : F.Ident.ident; typ : F.AST.term } let make_explicit x = { x with kind = Explicit } - let make_implicit x = { x with kind = Implicit } + + let implicit_to_explicit x = + if [%matches? Tcresolve] x.kind then x else make_explicit x let of_generic_param span (p : generic_param) : t = let ident = plocal_ident p.ident in @@ -1034,7 +1036,7 @@ struct F.AST.TyconRecord ( F.id @@ U.Concrete_ident_view.to_definition_name name, FStarBinder.of_generics e.span generics - |> List.map ~f:FStarBinder.make_explicit + |> List.map ~f:FStarBinder.implicit_to_explicit |> List.map ~f:FStarBinder.to_binder, None, [], @@ -1101,7 +1103,7 @@ struct F.AST.TyconVariant ( F.id @@ U.Concrete_ident_view.to_definition_name name, FStarBinder.of_generics e.span generics - |> List.map ~f:FStarBinder.make_explicit + |> List.map ~f:FStarBinder.implicit_to_explicit |> List.map ~f:FStarBinder.to_binder, None, constructors ); @@ -1299,7 +1301,7 @@ struct List.map ~f: FStarBinder.( - of_generic_param e.span >> make_explicit >> to_binder) + of_generic_param e.span >> implicit_to_explicit >> to_binder) generics.params in F.AST.TyconRecord (name_id, bds, None, [], fields) diff --git a/test-harness/src/snapshots/toolchain__traits into-fstar.snap b/test-harness/src/snapshots/toolchain__traits into-fstar.snap index 13c1c318a..81f7fa2f2 100644 --- a/test-harness/src/snapshots/toolchain__traits into-fstar.snap +++ b/test-harness/src/snapshots/toolchain__traits into-fstar.snap @@ -432,7 +432,7 @@ module Traits.Type_alias_bounds_issue_707_ open Core open FStar.Mul -type t_StructWithGenericBounds (v_T: Type0) (i1: Core.Clone.t_Clone v_T) = +type t_StructWithGenericBounds (v_T: Type0) {| i1: Core.Clone.t_Clone v_T |} = | StructWithGenericBounds : v_T -> t_StructWithGenericBounds v_T ''' "Traits.Unconstrainted_types_issue_677_.fst" = '''