Merge pull request #669 from hacspec/bounds_impls

Add bounds impls on calls in expressions

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

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 *)
           }

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

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

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

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 }

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]
 

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
                 | _ ->

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

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 ->