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 =