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

Engine: propagate trait generics arguments #751

Merged
merged 6 commits into from
Jul 10, 2024
Merged

Engine: propagate trait generics arguments #751

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
049d638
feat(engine): propagate trait-specific generics
W95Psp Jul 8, 2024
b1ca060
feat(engine/f*): propagate trait-specific generics
W95Psp Jul 9, 2024
64a1f39
test(engine/f*): propagate trait-specific generics
W95Psp Jul 9, 2024
e87b374
fix(proof-libs/f*): `f_deref`: make it a typeclass
W95Psp Jul 9, 2024
9f056df
Update tests/traits/src/lib.rs
W95Psp Jul 10, 2024
a17cd49
fix(engine/f*): `{| ... |}` for trait bounds on types
W95Psp Jul 10, 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
2 changes: 2 additions & 0 deletions engine/backends/fstar/fstar-surface-ast/FStar_Parser_Const.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) =
Expand Down
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 @@ -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
Expand Down
104 changes: 66 additions & 38 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,17 +407,25 @@ 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)
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
Expand Down Expand Up @@ -449,7 +457,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
Expand All @@ -463,8 +471,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 } ->
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
Expand Down Expand Up @@ -629,12 +639,16 @@ 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 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
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) =
Expand All @@ -644,8 +658,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 =
Expand Down Expand Up @@ -676,17 +690,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
Expand Down Expand Up @@ -1014,7 +1035,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.implicit_to_explicit
|> List.map ~f:FStarBinder.to_binder,
None,
[],
Expand Down Expand Up @@ -1080,7 +1102,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.implicit_to_explicit
|> List.map ~f:FStarBinder.to_binder,
None,
constructors );
Expand Down Expand Up @@ -1157,20 +1180,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
Expand Down Expand Up @@ -1212,14 +1228,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
Expand All @@ -1228,9 +1246,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
Expand Down Expand Up @@ -1277,7 +1295,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 >> implicit_to_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
Expand All @@ -1296,9 +1324,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 =
Expand Down
2 changes: 1 addition & 1 deletion engine/lib/ast.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
27 changes: 14 additions & 13 deletions engine/lib/ast_utils.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -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 *)
}
Expand Down Expand Up @@ -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 *)
} ->
Expand Down Expand Up @@ -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
Expand All @@ -355,7 +356,7 @@ module Make (F : Features.T) = struct
f;
args = [ ascribe arg ];
generic_args;
impl;
trait;
bounds_impls;
};
}
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -924,7 +925,7 @@ module Make (F : Features.T) = struct
args = [ e ];
generic_args = _;
bounds_impls = _;
impl = _;
trait = _;
} ->
next e
| _ -> e
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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 *);
};
}

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