From 4d772b1bf1ba4d80a9632d8cbbcc54102f733405 Mon Sep 17 00:00:00 2001
From: Lucas Franceschino <lucas.franceschino@inria.fr>
Date: Thu, 21 Dec 2023 17:15:02 +0100
Subject: [PATCH] fix(engine/fstar): always name binders on `val`s

---
 engine/backends/fstar/fstar_ast.ml     |  8 +++++++-
 engine/backends/fstar/fstar_backend.ml | 18 +++++++++++++++---
 2 files changed, 22 insertions(+), 4 deletions(-)

diff --git a/engine/backends/fstar/fstar_ast.ml b/engine/backends/fstar/fstar_ast.ml
index 969c6733c..18edbce11 100644
--- 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
index 07c0cf100..d2d239612 100644
--- 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