Merge pull request #532 from hacspec/parent-bounds

feat(exporter/traits): parent bounds on impl and associated types

cli/default.nix

@@ -56,7 +56,14 @@
       doInstallCargoArtifacts = true;
     }
   );
-  frontend-docs = craneLib.cargoDoc (commonArgs // {inherit cargoArtifacts pname;});
+  frontend-docs = craneLib.cargoDoc (commonArgs // {
+    preBuildPhases = ["addRustcDocs"];
+    addRustcDocs = ''
+      mkdir -p target/doc
+      cp --no-preserve=mode -rf ${rustc.passthru.availableComponents.rustc-docs}/share/doc/rust/html/rustc/* target/doc/
+    '';
+    inherit cargoArtifacts pname;
+  });
   docs = stdenv.mkDerivation {
     name = "hax-docs";
     unpackPhase = "true";

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -1321,7 +1321,7 @@ struct
 
   let pgeneric_constraints_as_argument span :
       generic_constraint -> SSP.AST.argument list = function
-    | GCType { bound = { trait; args }; _ } ->
+    | GCType { goal = { trait; args }; _ } ->
         [
           SSP.AST.Typeclass
             ( None,
@@ -1738,11 +1738,11 @@ struct
                                     [],
                                     value ) );
                           ]
-                    | TIType trait_refs ->
+                    | TIType impl_idents ->
                         SSP.AST.Named
                           (pconcrete_ident x.ti_ident, SSP.AST.TypeTy)
                         :: List.map
-                             ~f:(fun (tr, _id) ->
+                             ~f:(fun { goal = tr; _ } ->
                                SSP.AST.Coercion
                                  ( pconcrete_ident x.ti_ident ^ "_"
                                    ^ pconcrete_ident tr.trait,
@@ -1752,7 +1752,7 @@ struct
                                          SSP.AST.NameTy
                                            (pconcrete_ident x.ti_ident);
                                        ] ) ))
-                             trait_refs)
+                             impl_idents)
                   items );
           ]
           @ List.concat_map

engine/backends/fstar/fstar_backend.ml

@@ -294,17 +294,17 @@ struct
     let some = Option.some in
     let hax_unstable_impl_exprs = false in
     match ie with
-    | Concrete tr -> c_trait_ref span tr |> some
+    | Concrete tr -> c_trait_goal span tr |> some
     | LocalBound { id } ->
         let local_ident =
           Local_ident.{ name = id; id = Local_ident.mk_id Expr 0 }
         in
         F.term @@ F.AST.Var (F.lid_of_id @@ plocal_ident local_ident) |> some
     | ImplApp { impl; _ } when not hax_unstable_impl_exprs ->
         pimpl_expr span impl
-    | Parent { impl; trait } when hax_unstable_impl_exprs ->
+    | Parent { impl; ident } when hax_unstable_impl_exprs ->
         let* impl = pimpl_expr span impl in
-        let trait = "_super_" ^ name_of_trait_ref span trait in
+        let trait = "_super_" ^ ident.name in
         F.term @@ F.AST.Project (impl, F.lid [ trait ]) |> some
     | ImplApp { impl; args = [] } when hax_unstable_impl_exprs ->
         pimpl_expr span impl
@@ -319,12 +319,9 @@ struct
         F.term_of_lid [ "_Builtin" ] |> some
     | _ -> None
 
-  and name_of_trait_ref _span : trait_ref -> string =
-    [%hash: trait_ref] >> Int.to_string
-
-  and c_trait_ref span trait_ref =
-    let trait = F.term @@ F.AST.Name (pconcrete_ident trait_ref.trait) in
-    List.map ~f:(pgeneric_value span) trait_ref.args |> F.mk_e_app trait
+  and c_trait_goal span trait_goal =
+    let trait = F.term @@ F.AST.Name (pconcrete_ident trait_goal.trait) in
+    List.map ~f:(pgeneric_value span) trait_goal.args |> F.mk_e_app trait
 
   and pgeneric_value span (g : generic_value) =
     match g with
@@ -570,9 +567,9 @@ struct
     let of_generic_constraint span (nth : int) (c : generic_constraint) =
       match c with
       | GCLifetime _ -> .
-      | GCType { bound; id; _ } ->
-          let typ = c_trait_ref span bound in
-          { kind = Tcresolve; ident = F.id id; typ }
+      | GCType { goal; name } ->
+          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
@@ -618,7 +615,7 @@ struct
     match c with
     | GCLifetime _ ->
         Error.assertion_failure span "pgeneric_constraint_bd:LIFETIME"
-    | GCType { bound; _ } -> c_trait_ref span bound
+    | GCType { goal; name = _ } -> c_trait_goal span goal
 
   let get_attr (type a) (name : string) (map : string -> a) (attrs : attrs) :
       a option =
@@ -1033,14 +1030,18 @@ struct
                     (* in *)
                     (F.id name, None, [], t)
                     :: List.map
-                         ~f:(fun ({ trait; args }, id) ->
+                         ~f:
+                           (fun {
+                                  goal = { trait; args };
+                                  name = impl_ident_name;
+                                } ->
                            let base =
                              F.term @@ F.AST.Name (pconcrete_ident trait)
                            in
                            let args =
                              List.map ~f:(pgeneric_value e.span) args
                            in
-                           ( F.id (name ^ "_" ^ id),
+                           ( F.id (name ^ "_" ^ impl_ident_name),
                              None,
                              [],
                              F.mk_e_app base args ))
@@ -1062,10 +1063,10 @@ struct
         let constraints_fields : FStar_Parser_AST.tycon_record =
           generics.constraints
           |> List.map ~f:(fun c ->
-                 let bound =
-                   match c with GCType { bound; _ } -> bound | _ -> .
+                 let bound, id =
+                   match c with GCType { goal; name } -> (goal, name) | _ -> .
                  in
-                 let name = "_super_" ^ name_of_trait_ref e.span bound in
+                 let name = "_super_" ^ id in
                  let typ = pgeneric_constraint_type e.span c in
                  (F.id name, None, [ F.Attrs.no_method ], typ))
         in

engine/lib/ast.ml

@@ -134,22 +134,35 @@ functor
 
     and impl_expr =
       | Self
-      | Concrete of trait_ref
+      | Concrete of trait_goal
       | LocalBound of { id : string }
-      | Parent of { impl : impl_expr; trait : trait_ref }
+      | Parent of { impl : impl_expr; ident : impl_ident }
       | Projection of {
           impl : impl_expr;
-          trait : trait_ref;
           item : concrete_ident;
+          ident : impl_ident;
         }
       | ImplApp of { impl : impl_expr; args : impl_expr list }
-      | Dyn of trait_ref
-      | Builtin of trait_ref
+      | Dyn of trait_goal
+      | Builtin of trait_goal
       | FnPointer of ty
       (* The `IE` suffix is there because visitors conflicts...... *)
       | ClosureIE of todo
 
-    and trait_ref = { trait : concrete_ident; args : generic_value list }
+    and trait_goal = { trait : concrete_ident; args : generic_value list }
+    (** A fully applied trait: [Foo<SomeTy, T0, ..., Tn>] (or
+      `SomeTy: Foo<T0, ..., Tn>`). An `impl_expr` "inhabits" a
+      `trait_goal`. *)
+
+    and impl_ident = { goal : trait_goal; name : string }
+    (** An impl identifier [{goal; name}] can be:
+          {ul
+              {- An in-scope variable [name] that inhabits [goal].}
+              {- A field of some other impl expression [i]: [i.name] inhabits [goal]. This corresponds to parent bounds or associated type bounds.}
+              {- An argument that introduces a variable [name] that inhabits [goal].}
+          }
+      *)
+    (* TODO: ADD SPAN! *)
 
     and pat' =
       | PWild
@@ -309,12 +322,9 @@ functor
 
     and generic_constraint =
       | GCLifetime of todo * F.lifetime
-      | GCType of {
-          bound : trait_ref;
-              (* trait_ref is always applied with the type the trait implements.
-                 For instance, `T: Clone` is actually `Clone<T> *)
-          id : string;
-        }
+      | GCType of impl_ident
+          (** Trait or lifetime constraints. For instance, `A` and `B` in
+    `fn f<T: A + B>()`. *)
     [@@deriving show, yojson, hash, eq]
 
     type param = { pat : pat; typ : ty; typ_span : span option; attrs : attrs }
@@ -388,7 +398,7 @@ functor
       ii_attrs : attrs;
     }
 
-    and trait_item' = TIType of (trait_ref * string) list | TIFn of ty
+    and trait_item' = TIType of impl_ident list | TIFn of ty
 
     and trait_item = {
       (* TODO: why do I need to prefix by `ti_` here? I guess visitors fail or something *)

engine/lib/ast_utils.ml

@@ -180,22 +180,37 @@ module Make (F : Features.T) = struct
           expr e
       end
 
+    (** Rename impl expressions variables. By default, they are big
+      and unique identifiers, after this function, they are renamed
+      into `iN` where `N` is a short local unique identifier. *)
     let rename_generic_constraints =
       object
         inherit [_] Visitors.map as super
 
-        method! visit_generic_constraint (s : (string, string) Hashtbl.t) gc =
+        method! visit_generic_constraint
+            ((enabled, s) : bool * (string, string) Hashtbl.t) gc =
           match gc with
-          | GCType { bound; id } ->
+          | GCType { goal; name } when enabled ->
               let data = "i" ^ Int.to_string (Hashtbl.length s) in
-              let _ = Hashtbl.add s ~key:id ~data in
-              GCType { bound; id = data }
-          | _ -> super#visit_generic_constraint s gc
+              let _ = Hashtbl.add s ~key:name ~data in
+              GCType { goal; name = data }
+          | _ -> super#visit_generic_constraint (enabled, s) gc
+
+        method! visit_trait_item (_, s) = super#visit_trait_item (true, s)
+
+        method! visit_item' (_, s) item =
+          let enabled =
+            (* generic constraints on traits correspond to super
+               traits, those are not local and should NOT be renamed *)
+            [%matches? Trait _] item |> not
+          in
+          super#visit_item' (enabled, s) item
 
         method! visit_impl_expr s ie =
           match ie with
           | LocalBound { id } ->
-              LocalBound { id = Hashtbl.find s id |> Option.value ~default:id }
+              LocalBound
+                { id = Hashtbl.find (snd s) id |> Option.value ~default:id }
           | _ -> super#visit_impl_expr s ie
       end