diff --git a/engine/lib/ast.ml b/engine/lib/ast.ml index 10cc44808..1fdcb5b93 100644 --- a/engine/lib/ast.ml +++ b/engine/lib/ast.ml @@ -194,6 +194,7 @@ functor f : expr; args : expr list (* ; f_span: span *); generic_args : generic_value list; + bounds_impls : impl_expr list; impl : impl_expr option; } | Literal of literal diff --git a/engine/lib/ast_utils.ml b/engine/lib/ast_utils.ml index fed3bebf4..5f688e280 100644 --- a/engine/lib/ast_utils.ml +++ b/engine/lib/ast_utils.ml @@ -72,9 +72,15 @@ module Make (F : Features.T) = struct | _ -> None let app (e : expr) : - (expr * expr list * generic_value list * impl_expr option) option = + (expr + * expr list + * generic_value list + * impl_expr option + * impl_expr list) + option = match e.e with - | App { f; args; generic_args; impl } -> Some (f, args, generic_args, impl) + | App { f; args; generic_args; impl; bounds_impls } -> + Some (f, args, generic_args, impl, bounds_impls) | _ -> None let pbinding_simple (p : pat) : (local_ident * ty) option = @@ -91,7 +97,8 @@ module Make (F : Features.T) = struct args = [ e ]; generic_args = _; impl = _; - (* TODO: see issue #328 *) + _; + (* TODO: see issue #328 *) } when Concrete_ident.eq_name f f' -> Some e @@ -195,7 +202,8 @@ module Make (F : Features.T) = struct args = [ { e = Borrow { e = sub; _ }; _ } ]; generic_args = _; impl = _; - (* TODO: see issue #328 *) + _; + (* TODO: see issue #328 *) } -> expr sub | _ -> super#visit_expr () e @@ -336,11 +344,20 @@ module Make (F : Features.T) = struct args = [ arg ]; generic_args; impl; + bounds_impls; } -> ascribe { e with - e = App { f; args = [ ascribe arg ]; generic_args; impl }; + e = + App + { + f; + args = [ ascribe arg ]; + generic_args; + impl; + bounds_impls; + }; } | _ -> (* Ascribe the return type of a function application & constructors *) @@ -685,7 +702,7 @@ module Make (F : Features.T) = struct (** See [beta_reduce_closure]'s documentation. *) let beta_reduce_closure_opt (e : expr) : expr option = - let* f, args, _, _ = Expect.app e in + let* f, args, _, _, _ = Expect.app e in let* pats, body = Expect.closure f in let* vars = List.map ~f:Expect.pbinding_simple pats |> sequence in let vars = List.map ~f:fst vars in @@ -851,7 +868,15 @@ module Make (F : Features.T) = struct let typ = TArrow (List.map ~f:(fun arg -> arg.typ) args, ret_typ) in let e = GlobalVar f in { - e = App { f = { e; typ; span }; args; generic_args = []; impl }; + e = + App + { + f = { e; typ; span }; + args; + generic_args = []; + bounds_impls = []; + impl; + }; typ = ret_typ; span; } @@ -898,6 +923,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar (`Primitive Ast.Deref); _ }; args = [ e ]; generic_args = _; + bounds_impls = _; impl = _; } -> next e @@ -933,6 +959,7 @@ module Make (F : Features.T) = struct f; args = [ e ]; generic_args = []; + bounds_impls = []; impl = None (* TODO: see issue #328 *); }; typ; @@ -1032,6 +1059,7 @@ module Make (F : Features.T) = struct f = tuple_projector tuple.span tuple.typ len nth type_at_nth; args = [ tuple ]; generic_args = [] (* TODO: see issue #328 *); + bounds_impls = []; impl = None (* TODO: see issue #328 *); }; } @@ -1075,6 +1103,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar (`Projector _ as projector); _ }; args = [ place ]; generic_args = _; + bounds_impls = _; impl = _; (* TODO: see issue #328 *) } -> @@ -1085,6 +1114,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar f; _ }; args = [ place; index ]; generic_args = _; + bounds_impls = _; impl = _; (* TODO: see issue #328 *) } @@ -1097,6 +1127,7 @@ module Make (F : Features.T) = struct f = { e = GlobalVar f; _ }; args = [ place; index ]; generic_args = _; + bounds_impls = _; impl = _; (* TODO: see issue #328 *) } diff --git a/engine/lib/ast_visitors.ml b/engine/lib/ast_visitors.ml index 1f9ce20f7..518c0011c 100644 --- a/engine/lib/ast_visitors.ml +++ b/engine/lib/ast_visitors.ml @@ -270,10 +270,14 @@ functor self#visit_list self#visit_generic_value env record_payload.generic_args in + let bounds_impls = + self#visit_list self#visit_impl_expr env + record_payload.bounds_impls + in let impl = self#visit_option self#visit_impl_expr env record_payload.impl in - App { f; args; generic_args; impl } + App { f; args; generic_args; impl; bounds_impls } | Literal x0 -> let x0 = self#visit_literal env x0 in Literal x0 @@ -1242,11 +1246,16 @@ functor record_payload.generic_args in let reduce_acc = self#plus reduce_acc reduce_acc' in + let bounds_impls, reduce_acc' = + self#visit_list self#visit_impl_expr env + record_payload.bounds_impls + in + let reduce_acc = self#plus reduce_acc reduce_acc' in let impl, reduce_acc' = self#visit_option self#visit_impl_expr env record_payload.impl in let reduce_acc = self#plus reduce_acc reduce_acc' in - (App { f; args; generic_args; impl }, reduce_acc) + (App { f; args; generic_args; impl; bounds_impls }, reduce_acc) | Literal x0 -> let x0, reduce_acc = self#visit_literal env x0 in (Literal x0, reduce_acc) @@ -2403,6 +2412,11 @@ functor record_payload.generic_args in let reduce_acc = self#plus reduce_acc reduce_acc' in + let reduce_acc' = + self#visit_list self#visit_impl_expr env + record_payload.bounds_impls + in + let reduce_acc = self#plus reduce_acc reduce_acc' in let reduce_acc' = self#visit_option self#visit_impl_expr env record_payload.impl in diff --git a/engine/lib/generic_printer/generic_printer_base.ml b/engine/lib/generic_printer/generic_printer_base.ml index 3c55d9430..3e61a44fd 100644 --- a/engine/lib/generic_printer/generic_printer_base.ml +++ b/engine/lib/generic_printer/generic_printer_base.ml @@ -181,9 +181,7 @@ module Make (F : Features.T) = struct method expr' : par_state -> expr' fn = fun _ctx e -> match e with - | App - { f = { e = GlobalVar i; _ } as f; args; generic_args; impl = _ } - -> ( + | App { f = { e = GlobalVar i; _ } as f; args; generic_args; _ } -> ( let expect_one_arg where = match args with | [ arg ] -> arg diff --git a/engine/lib/import_thir.ml b/engine/lib/import_thir.ml index 77bb64069..90fa21d13 100644 --- a/engine/lib/import_thir.ml +++ b/engine/lib/import_thir.ml @@ -198,6 +198,7 @@ let resugar_index_mut (e : expr) : (expr * expr) option = args = [ { e = Borrow { e = x; _ }; _ }; index ]; generic_args = _ (* TODO: see issue #328 *); impl = _ (* TODO: see issue #328 *); + bounds_impls = _; } when Concrete_ident.eq_name Core__ops__index__IndexMut__index_mut meth -> Some (x, index) @@ -207,6 +208,7 @@ let resugar_index_mut (e : expr) : (expr * expr) option = args = [ x; index ]; generic_args = _ (* TODO: see issue #328 *); impl = _ (* TODO: see issue #328 *); + bounds_impls = _; } when Concrete_ident.eq_name Core__ops__index__Index__index meth -> Some (x, index) @@ -357,7 +359,14 @@ end) : EXPR = struct and c_expr_unwrapped (e : Thir.decorated_for__expr_kind) : expr = (* TODO: eliminate that `call`, use the one from `ast_utils` *) let call f args = - App { f; args = List.map ~f:c_expr args; generic_args = []; impl = None } + App + { + f; + args = List.map ~f:c_expr args; + generic_args = []; + impl = None; + bounds_impls = []; + } in let typ = c_ty e.span e.ty in let span = Span.of_thir e.span in @@ -408,8 +417,10 @@ end) : EXPR = struct fun'; ty = _; generic_args; + bounds_impls; } -> let args = List.map ~f:c_expr args in + let bounds_impls = List.map ~f:(c_impl_expr e.span) bounds_impls in let generic_args = List.map ~f:(c_generic_value e.span) generic_args in @@ -426,6 +437,7 @@ end) : EXPR = struct f; args; generic_args; + bounds_impls; impl = Option.map ~f:(c_impl_expr e.span) impl; } | Box { value } -> @@ -564,6 +576,7 @@ end) : EXPR = struct args = [ lhs ]; generic_args = [] (* TODO: see issue #328 *); impl = None (* TODO: see issue #328 *); + bounds_impls = []; } | TupleField { lhs; field } -> (* TODO: refactor *) @@ -580,6 +593,7 @@ end) : EXPR = struct args = [ lhs ]; generic_args = [] (* TODO: see issue #328 *); impl = None (* TODO: see issue #328 *); + bounds_impls = []; } | GlobalName { id } -> GlobalVar (def_id Value id) | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id) @@ -715,6 +729,7 @@ end) : EXPR = struct args = [ e ]; generic_args = _; impl = _; + bounds_impls = _; (* TODO: see issue #328 *) } -> LhsFieldAccessor diff --git a/engine/lib/phases/phase_direct_and_mut.ml b/engine/lib/phases/phase_direct_and_mut.ml index 5bcab80b3..1348c711a 100644 --- a/engine/lib/phases/phase_direct_and_mut.ml +++ b/engine/lib/phases/phase_direct_and_mut.ml @@ -101,7 +101,7 @@ 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) : B.expr = + (impl : B.impl_expr 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) *) @@ -138,7 +138,12 @@ struct (* there is no mutation, we can reconstruct the expression right away *) let f, typ = (dexpr f, dty span otype) in let args = List.map ~f:dexpr raw_args in - B.{ e = B.App { f; args; generic_args; impl }; typ; span } + B. + { + e = B.App { f; args; generic_args; impl; bounds_impls }; + typ; + span; + } | _ -> ( (* TODO: when LHS are better (issue #222), compress `p1 = tmp1; ...; pN = tmpN` in `(p1...pN) = ...` *) (* we are generating: @@ -213,7 +218,8 @@ struct in B. { - e = App { f; args = unmut_args; generic_args; impl }; + e = + App { f; args = unmut_args; generic_args; impl; bounds_impls }; typ = pat.typ; span = pat.span; } @@ -263,10 +269,11 @@ struct and dexpr_unwrapped (expr : A.expr) : B.expr = let span = expr.span in match expr.e with - | App { f; args; generic_args; impl } -> + | 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 - translate_app span expr.typ f args generic_args impl + let bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls in + translate_app span expr.typ f args generic_args impl 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 c576d99ee..8bdd29ff2 100644 --- a/engine/lib/phases/phase_drop_references.ml +++ b/engine/lib/phases/phase_drop_references.ml @@ -111,14 +111,15 @@ struct body = dexpr body; captures = List.map ~f:dexpr captures; } - | App { f; args; generic_args; impl } -> + | App { f; args; generic_args; impl; 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 - App { f; args; generic_args; impl } + let bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls in + App { f; args; generic_args; impl; bounds_impls } | _ -> . [@@inline_ands bindings_of dexpr - dbinding_mode] diff --git a/engine/lib/phases/phase_specialize.ml b/engine/lib/phases/phase_specialize.ml index f87dc9b39..dd89b956e 100644 --- a/engine/lib/phases/phase_specialize.ml +++ b/engine/lib/phases/phase_specialize.ml @@ -129,7 +129,15 @@ module Make (F : Features.T) = let f = { f' with e = GlobalVar f } in { e with - e = App { f; args = l; impl = None; generic_args = [] }; + e = + App + { + f; + args = l; + impl = None; + generic_args = []; + bounds_impls = []; + }; } | [] -> super#visit_expr () e | _ -> diff --git a/engine/lib/print_rust.ml b/engine/lib/print_rust.ml index 68ed18b3e..653e67475 100644 --- a/engine/lib/print_rust.ml +++ b/engine/lib/print_rust.ml @@ -236,7 +236,7 @@ module Raw = struct match else_ with Some e -> !" else {" & pexpr e & !"}" | None -> !"" in !"(" & !"if " & pexpr cond & !"{" & pexpr then_ & !"}" & else_ & !")" - | App { f; args; generic_args; impl = _ } -> + | App { f; args; generic_args; _ } -> let args = concat ~sep:!"," @@ List.map ~f:pexpr args in let generic_args = let f = pgeneric_value e.span in diff --git a/engine/lib/side_effect_utils.ml b/engine/lib/side_effect_utils.ml index ec5533df4..44799d3e0 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 } -> + | App { f; args; generic_args; impl; bounds_impls } -> HoistSeq.many env (List.map ~f:(self#visit_expr env) (f :: args)) (fun l effects -> @@ -356,7 +356,11 @@ struct | f :: args -> (f, args) | _ -> HoistSeq.err_hoist_invariant e.span Stdlib.__LOC__ in - ({ e with e = App { f; args; generic_args; impl } }, effects)) + ( { + e with + e = App { f; args; generic_args; impl; bounds_impls }; + }, + effects )) | Literal _ -> (e, m#zero) | Block (inner, witness) -> HoistSeq.one env (self#visit_expr env inner) (fun inner effects -> diff --git a/engine/lib/subtype.ml b/engine/lib/subtype.ml index 76c2db4b9..f58487482 100644 --- a/engine/lib/subtype.ml +++ b/engine/lib/subtype.ml @@ -157,12 +157,13 @@ struct then_ = dexpr then_; else_ = Option.map ~f:dexpr else_; } - | App { f; args; generic_args; impl } -> + | App { f; args; generic_args; bounds_impls; impl } -> App { f = dexpr f; args = List.map ~f:dexpr args; generic_args = List.map ~f:(dgeneric_value span) generic_args; + bounds_impls = List.map ~f:(dimpl_expr span) bounds_impls; impl = Option.map ~f:(dimpl_expr span) impl; } | Literal lit -> Literal lit