Merge pull request #403 from hacspec/fix-fstar-interfaces

fix(engine/fstar): always name binders on `val`s
cryspen · Jan 5, 2024 · 8ecf9c6 · 8ecf9c6
2 parents 9d54718 + 4d772b1
commit 8ecf9c6
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 4 deletions.
diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
@@ -59,7 +59,13 @@ let mk_binder ?(aqual : FStar_Parser_AST.arg_qualifier option = Some Implicit) b
 
 let mk_e_binder b = mk_binder ~aqual:None b
 let term_of_lid path = term @@ AST.Name (lid path)
-let binder_of_term (t : AST.term) : AST.binder = mk_e_binder @@ AST.NoName t
+
+let binder_of_term ?name (t : AST.term) : AST.binder =
+  let b =
+    match name with None -> AST.NoName t | Some n -> AST.Annotated (n, t)
+  in
+  mk_e_binder b
+
 let unit = term AST.(Const Const_unit)
 
 let mk_e_arrow inputs output =

diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml
@@ -791,10 +791,22 @@ struct
           F.term
           @@ F.AST.Product
                ( List.map ~f:FStarBinder.to_binder generics
-                 @ List.map
-                     ~f:(fun { pat = _; typ_span; typ } ->
+                 @ List.mapi
+                     ~f:(fun i { pat; typ_span; typ } ->
+                       let name =
+                         match pat.p with
+                         | PBinding { var; _ } ->
+                             Some (U.Concrete_ident_view.local_ident var)
+                         | _ ->
+                             (* TODO: this might generate bad code,
+                                see
+                                https://github.com/hacspec/hax/issues/402
+                             *)
+                             None
+                       in
+                       let name = Option.map ~f:F.id name in
                        let span = Option.value ~default:e.span typ_span in
-                       pty span typ |> F.binder_of_term)
+                       pty span typ |> F.binder_of_term ?name)
                      params,
                  ty )
         in