Merge pull request #372 from hacspec/add-self-implsource

Add `Self` implsource

engine/lib/ast.ml

@@ -256,6 +256,7 @@ functor
       | GConst of expr
 
     and impl_expr =
+      | Self
       | Concrete of trait_ref
       | LocalBound of { id : string }
       | Parent of { impl : impl_expr; trait : trait_ref }
@@ -303,6 +304,7 @@ functor
           f : expr;
           args : expr list (* ; f_span: span *);
           generic_args : generic_value list;
+          impl : impl_expr option;
         }
       | Literal of literal
       | Array of expr list

engine/lib/ast_utils.ml

@@ -66,6 +66,7 @@ module Make (F : Features.T) = struct
             f = { e = GlobalVar (`Concrete f'); _ };
             args = [ e ];
             generic_args = _;
+            impl = _;
           (* TODO: see issue #328 *)
           }
         when Concrete_ident.eq_name f f' ->
@@ -165,6 +166,7 @@ module Make (F : Features.T) = struct
                   f = { e = GlobalVar (`Primitive Deref); _ };
                   args = [ { e = Borrow { e = sub; _ }; _ } ];
                   generic_args = _;
+                  impl = _;
                 (* TODO: see issue #328 *)
                 } ->
                 expr sub
@@ -261,9 +263,13 @@ module Make (F : Features.T) = struct
                   f = { e = GlobalVar (`Primitive Cast); _ } as f;
                   args = [ arg ];
                   generic_args;
+                  impl;
                 } ->
                 ascribe
-                  { e with e = App { f; args = [ ascribe arg ]; generic_args } }
+                  {
+                    e with
+                    e = App { f; args = [ ascribe arg ]; generic_args; impl };
+                  }
             | _ ->
                 (* Ascribe the return type of a function application & constructors *)
                 if (ascribe_app && is_app e.e) || [%matches? Construct _] e.e
@@ -582,7 +588,7 @@ module Make (F : Features.T) = struct
 
   let remove_unsize (e : expr) : expr =
     match e.e with
-    | App { f = { e = GlobalVar f; _ }; args = [ e ]; generic_args = _ }
+    | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ }
       when Global_ident.eq_name Rust_primitives__unsize f ->
         e
     | _ -> e
@@ -748,8 +754,9 @@ module Make (F : Features.T) = struct
           {
             f = { e; typ; span };
             args;
-            generic_args =
-              []
+            generic_args = [];
+            impl =
+              None
               (* TODO: see issue #328, and check that for evrey call to `call'` *);
           };
       typ = ret_typ;
@@ -784,7 +791,7 @@ module Make (F : Features.T) = struct
 
   let unbox_expr' (next : expr -> expr) (e : expr) : expr =
     match e.e with
-    | App { f = { e = GlobalVar f; _ }; args = [ e ]; generic_args = _ }
+    | App { f = { e = GlobalVar f; _ }; args = [ e ]; _ }
       when Global_ident.eq_name Alloc__boxed__Impl__new f ->
         next e
     | _ -> e
@@ -796,6 +803,7 @@ module Make (F : Features.T) = struct
           f = { e = GlobalVar (`Primitive Ast.Deref); _ };
           args = [ e ];
           generic_args = _;
+          impl = _;
         } ->
         next e
     | _ -> e
@@ -826,7 +834,12 @@ module Make (F : Features.T) = struct
         {
           e =
             App
-              { f; args = [ e ]; generic_args = [] (* TODO: see issue #328 *) };
+              {
+                f;
+                args = [ e ];
+                generic_args = [];
+                impl = None (* TODO: see issue #328 *);
+              };
           typ;
           span;
         }
@@ -924,6 +937,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 *);
+            impl = None (* TODO: see issue #328 *);
           };
     }
 
@@ -956,6 +970,7 @@ module Make (F : Features.T) = struct
             f = { e = GlobalVar (`Projector _ as projector); _ };
             args = [ place ];
             generic_args = _;
+            impl = _;
           (* TODO: see issue #328 *)
           } ->
           let* place = of_expr place in
@@ -965,6 +980,7 @@ module Make (F : Features.T) = struct
             f = { e = GlobalVar f; _ };
             args = [ place; index ];
             generic_args = _;
+            impl = _;
           (* TODO: see issue #328 *)
           }
         when Global_ident.eq_name Core__ops__index__Index__index f ->
@@ -976,6 +992,7 @@ module Make (F : Features.T) = struct
             f = { e = GlobalVar f; _ };
             args = [ place; index ];
             generic_args = _;
+            impl = _;
           (* TODO: see issue #328 *)
           }
         when Global_ident.eq_name Core__ops__index__IndexMut__index_mut f ->

engine/lib/generic_printer/generic_printer_base.ml

@@ -173,7 +173,9 @@ 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 } -> (
+          | App
+              { f = { e = GlobalVar i; _ } as f; args; generic_args; impl = _ }
+            -> (
               let expect_one_arg where =
                 match args with
                 | [ arg ] -> arg
@@ -189,7 +191,8 @@ module Make (F : Features.T) = struct
               | `Projector (`Concrete i) ->
                   let arg = expect_one_arg "projector concrete" in
                   print#field_projection i arg)
-          | App { f; args; generic_args } -> print#expr_app f args generic_args
+          | App { f; args; generic_args; _ } ->
+              print#expr_app f args generic_args
           | Construct { constructor; fields; base; is_record; is_struct } -> (
               match constructor with
               | `Concrete constructor ->

engine/lib/import_thir.ml

@@ -179,6 +179,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 *);
       }
     when Concrete_ident.eq_name Core__ops__index__IndexMut__index_mut meth ->
       Some (x, index)
@@ -187,6 +188,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 *);
       }
     when Concrete_ident.eq_name Core__ops__index__Index__index meth ->
       Some (x, index)
@@ -321,7 +323,7 @@ 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 = [] }
+      App { f; args = List.map ~f:c_expr args; generic_args = []; impl = None }
     in
     let typ = c_ty e.span e.ty in
     let span = Span.of_thir e.span in
@@ -385,7 +387,13 @@ end) : EXPR = struct
             | _ -> f
           in
           let args = if List.is_empty args then [ unit_expr span ] else args in
-          App { f; args; generic_args }
+          App
+            {
+              f;
+              args;
+              generic_args;
+              impl = Option.map ~f:(c_impl_expr e.span) impl;
+            }
       | Box { value } ->
           (U.call Rust_primitives__hax__box_new [ c_expr value ] span typ).e
       | Deref { arg } ->
@@ -512,6 +520,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 *);
             }
       | TupleField { lhs; field } ->
           (* TODO: refactor *)
@@ -527,6 +536,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 *);
             }
       | GlobalName { id } -> GlobalVar (def_id Value id)
       | UpvarRef { var_hir_id = id; _ } -> LocalVar (local_ident Expr id)
@@ -662,6 +672,7 @@ end) : EXPR = struct
                     };
                   args = [ e ];
                   generic_args = _;
+                  impl = _;
                 (* TODO: see issue #328 *)
                 } ->
                 LhsFieldAccessor
@@ -928,6 +939,7 @@ end) : EXPR = struct
         in
         List.fold ~init ~f path
     | Dyn { trait } -> Dyn (c_trait_ref span trait)
+    | SelfImpl -> Self
     | Builtin { trait } -> Builtin (c_trait_ref span trait)
     | Todo str -> failwith @@ "impl_expr_atom: Todo " ^ str
 

engine/lib/phases/phase_direct_and_mut.ml

@@ -97,8 +97,8 @@ struct
           LhsArbitraryExpr { witness = Features.On.arbitrary_lhs; e }
 
     and translate_app (span : span) (otype : A.ty) (f : A.expr)
-        (raw_args : A.expr list) (generic_args : B.generic_value list) : B.expr
-        =
+        (raw_args : A.expr list) (generic_args : B.generic_value list)
+        (impl : B.impl_expr option) : 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) *)
@@ -135,7 +135,7 @@ 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 }; typ; span }
+          B.{ e = B.App { f; args; generic_args; impl }; typ; span }
       | _ -> (
           (* TODO: when LHS are better (issue #222), compress `p1 = tmp1; ...; pN = tmpN` in `(p1...pN) = ...` *)
           (* we are generating:
@@ -210,7 +210,7 @@ struct
             in
             B.
               {
-                e = App { f; args = unmut_args; generic_args };
+                e = App { f; args = unmut_args; generic_args; impl };
                 typ = pat.typ;
                 span = pat.span;
               }
@@ -260,9 +260,10 @@ struct
     and dexpr_unwrapped (expr : A.expr) : B.expr =
       let span = expr.span in
       match expr.e with
-      | App { f; args; generic_args } ->
+      | App { f; args; generic_args; impl } ->
           let generic_args = List.map ~f:(dgeneric_value span) generic_args in
-          translate_app span expr.typ f args generic_args
+          let impl = Option.map ~f:(dimpl_expr span) impl in
+          translate_app span expr.typ f args generic_args impl
       | _ ->
           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

@@ -110,13 +110,14 @@ struct
               body = dexpr body;
               captures = List.map ~f:dexpr captures;
             }
-      | App { f; args; generic_args } ->
+      | App { f; args; generic_args; impl } ->
           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 }
+          App { f; args; generic_args; impl }
       | _ -> .
       [@@inline_ands bindings_of dexpr - dbinding_mode]
 

engine/lib/print_rust.ml

@@ -211,7 +211,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 } ->
+    | App { f; args; generic_args; impl = _ } ->
         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

@@ -342,7 +342,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 } ->
+          | App { f; args; generic_args; impl } ->
               HoistSeq.many env
                 (List.map ~f:(super#visit_expr env) (f :: args))
                 (fun l effects ->
@@ -351,7 +351,7 @@ struct
                     | f :: args -> (f, args)
                     | _ -> HoistSeq.err_hoist_invariant e.span Stdlib.__LOC__
                   in
-                  ({ e with e = App { f; args; generic_args } }, effects))
+                  ({ e with e = App { f; args; generic_args; impl } }, effects))
           | Literal _ -> (e, m#zero)
           | Block (inner, witness) ->
               HoistSeq.one env (super#visit_expr env inner)

engine/lib/subtype.ml

@@ -53,6 +53,7 @@ struct
 
   and dimpl_expr (span : span) (i : A.impl_expr) : B.impl_expr =
     match i with
+    | Self -> Self
     | Concrete tr -> Concrete (dtrait_ref span tr)
     | LocalBound { id } -> LocalBound { id }
     | Parent { impl; trait } ->
@@ -153,12 +154,13 @@ struct
             then_ = dexpr then_;
             else_ = Option.map ~f:dexpr else_;
           }
-    | App { f; args; generic_args } ->
+    | App { f; args; generic_args; impl } ->
         App
           {
             f = dexpr f;
             args = List.map ~f:dexpr args;
             generic_args = List.map ~f:(dgeneric_value span) generic_args;
+            impl = Option.map ~f:(dimpl_expr span) impl;
           }
     | Literal lit -> Literal lit
     | Array l -> Array (List.map ~f:dexpr l)

engine/utils/phase-debug-webapp/static/script.js

@@ -16,7 +16,7 @@ let mk = (kind, body = [], classes = []) => {
         console.error('wrong type for body', body);
     }
     return e;
-}
+};
 
 function findNode(o, search){
     let h = o => o instanceof Object ? (search(o) ? o : Object.values(o).map(h).find(x => x)) : null;
@@ -49,16 +49,32 @@ function json(json) {
     let o = JSON.parse(JSON.stringify(json));
     let root = mk('div', [], ['json-viewer']);
     let state = {
-        open: new Map()
+        open: new Map(),
+        default_open: false,
     };
     function render_all() {
         root.replaceChildren(render(o, []));
+        let expand_button = mk('button', state.default_open ? '🡒🡐' : '🡘', ['expand-all']);
+        expand_button.style = `
+            position: absolute;
+            top: 1px;
+            right: 1px;
+            padding: 0 3px;
+            margin: 0;
+            line-height: 0;
+            height: 16px;
+        `;
+        expand_button.onclick = () => {
+            state.default_open = !state.default_open;
+            render_all();
+        };
+        root.prepend(expand_button);
     }
     let key_of_path = path => JSON.stringify(path);
     let set_open = (path, v) => state.open.set(key_of_path(path), v);
     let is_open = (path, def = path.length < 6) => {
         let b = state.open.get(key_of_path(path));
-        return b === undefined ? def : b;
+        return b === undefined ? (state.default_open || def) : b;
     };
     let swap = (path, def) => {
         set_open(path, !is_open(path, def), false);
@@ -71,7 +87,7 @@ function json(json) {
                 return true;
             }
         }
-        return false;   
+        return false;
     };
     let is_simple = o => {
         if (o instanceof Object) {

frontend/exporter/src/lib.rs

@@ -8,6 +8,7 @@
 #![feature(let_chains)]
 #![allow(incomplete_features)]
 #![feature(specialization)]
+#![feature(return_position_impl_trait_in_trait)]
 
 extern crate rustc_abi;
 extern crate rustc_ast;