Merge pull request #1184 from hacspec/fix-1070

Skip generated impls using `Erased` attribute.
hacspec · Dec 12, 2024 · 62f7bfa · 62f7bfa
2 parents 08beb2d + 9360aeb
commit 62f7bfa
Show file tree

Hide file tree

Showing 7 changed files with 431 additions and 409 deletions.
diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml
@@ -407,14 +407,19 @@ struct
       method item'_Impl ~super ~generics ~self_ty ~of_trait ~items
           ~parent_bounds:_ ~safety:_ =
         let name, args = of_trait#v in
-        CoqNotation.instance
-          (name#p ^^ string "_" ^^ string (Int.to_string ([%hash: item] super)))
-          generics#p []
-          (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
-          (braces
-             (nest 2
-                (concat_map (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p) items)
-             ^^ break 1))
+        if Attrs.is_erased super.attrs then empty
+        else
+          CoqNotation.instance
+            (name#p ^^ string "_"
+            ^^ string (Int.to_string ([%hash: item] super)))
+            generics#p []
+            (name#p ^^ concat_map (fun x -> space ^^ parens x#p) args)
+            (braces
+               (nest 2
+                  (concat_map
+                     (fun x -> break 1 ^^ name#p ^^ !^"_" ^^ x#p)
+                     items)
+               ^^ break 1))
 
       method item'_NotImplementedYet = string "(* NotImplementedYet *)"
 

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -875,11 +875,7 @@ struct
       | `VerbatimIntf of string * [ `NoNewline | `Newline ]
       | `Comment of string ]
       list =
-    let is_erased =
-      Attrs.find_unique_attr e.attrs
-        ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
-      |> Option.is_some
-    in
+    let is_erased = Attrs.is_erased e.attrs in
     let erased_impl name ty attrs binders =
       let name' = F.id_prime name in
       let pat = F.AST.PatVar (name, None, []) in

diff --git a/engine/lib/attr_payloads.ml b/engine/lib/attr_payloads.ml
@@ -108,6 +108,11 @@ module MakeBase (Error : Phase_utils.ERROR) = struct
   let late_skip : attrs -> bool =
     status >> [%matches? Types.Included { late_skip = true }]
 
+  let is_erased : attrs -> bool =
+    find_unique_attr
+      ~f:([%eq: Types.ha_payload] Erased >> Fn.flip Option.some_if ())
+    >> Option.is_some
+
   let uid : attrs -> UId.t option =
     let f = function Types.Uid uid -> Some (UId.of_raw uid) | _ -> None in
     find_unique_attr ~f