Rust Engine: refactor names, change tuples representation

CHANGELOG.md

@@ -16,6 +16,7 @@ Changes to the Rust Engine:
  - Update name rendering infrastructure in the Lean backend (#1623, #1624)
  - Printers now emit proper diagnostics (PR #1669)
  - Global identifiers are now interned (#1689)
+ - Global identifiers are encapsulated properly, and provide easy destructuring as tuple identifiers (#1693)
 
 Changes to the frontend:
 - Add an explicit `Self: Trait` clause to trait methods and consts (#1559)

engine/lib/export_ast.ml

@@ -6,49 +6,6 @@ type missing_type = unit
 
 module B = Rust_engine_types
 
-module SpecialNames = struct
-  let rec map_strings (f : string -> string)
-      ({ contents = { id; value } } : Types.def_id) =
-    let id = Int64.neg id in
-    let value =
-      match value with
-      | { index; is_local; kind; krate; parent; path } ->
-          let path =
-            List.map
-              ~f:(fun { data; disambiguator } ->
-                let data =
-                  match data with
-                  | Types.CrateRoot { name } ->
-                      Types.CrateRoot { name = f name }
-                  | Types.TypeNs s -> Types.TypeNs (f s)
-                  | Types.ValueNs s -> Types.ValueNs (f s)
-                  | Types.MacroNs s -> Types.MacroNs (f s)
-                  | Types.LifetimeNs s -> Types.LifetimeNs (f s)
-                  | other -> other
-                in
-                Types.{ data; disambiguator })
-              path
-          in
-          let parent = Option.map ~f:(map_strings f) parent in
-          Types.{ index; is_local; kind; krate; parent; path }
-    in
-    let contents : Types.node_for__def_id_contents = { id; value } in
-    { contents }
-
-  let mk value f =
-    Concrete_ident_generated.def_id_of >> map_strings f
-    >> Concrete_ident.of_def_id ~value
-
-  let f len nth = function
-    | "Tuple2" -> "Tuple" ^ Int.to_string len
-    | "1" -> "Tuple" ^ Int.to_string nth
-    | s -> s
-
-  let tuple_type len = mk false (f len 0) Rust_primitives__hax__Tuple2
-  let tuple_cons len = mk true (f len 0) Rust_primitives__hax__Tuple2__Ctor
-  let tuple_field len nth = mk false (f len nth) Rust_primitives__hax__Tuple2__1
-end
-
 module Make (FA : Features.T) = struct
   open Ast
   module A = Ast.Make (FA)
@@ -114,21 +71,24 @@ module Make (FA : Features.T) = struct
     match fk with F16 -> F16 | F32 -> F32 | F64 -> F64 | F128 -> F128
 
   and dglobal_ident (gi : global_ident) : B.global_id =
-    let concrete c : B.global_id = B.Concrete (Concrete_ident.to_rust_ast c) in
+    let concrete c : B.global_id =
+      Types.Newtypeglobal_id (B.Concrete (Concrete_ident.to_rust_ast c))
+    in
     let of_name n = concrete (Concrete_ident.of_name ~value:true n) in
     match gi with
-    | `Concrete c -> concrete c
-    | `TupleType len -> SpecialNames.tuple_type len |> concrete
-    | `TupleCons len -> SpecialNames.tuple_cons len |> concrete
-    | `TupleField (nth, len) -> SpecialNames.tuple_field len nth |> concrete
+    | `Concrete c | `Projector (`Concrete c) -> concrete c
+    | `TupleType length ->
+        Types.Newtypeglobal_id (Tuple (Type { length = Int.to_string length }))
+    | `TupleCons length ->
+        Types.Newtypeglobal_id
+          (Tuple (Constructor { length = Int.to_string length }))
+    | `Projector (`TupleField (field, length)) | `TupleField (field, length) ->
+        let field, length = (Int.to_string field, Int.to_string length) in
+        Types.Newtypeglobal_id (Tuple (Field { length; field }))
     | `Primitive Deref -> of_name Rust_primitives__hax__deref_op
     | `Primitive Cast -> of_name Rust_primitives__hax__cast_op
     | `Primitive (LogicalOp And) -> of_name Rust_primitives__hax__logical_op_and
     | `Primitive (LogicalOp Or) -> of_name Rust_primitives__hax__logical_op_or
-    | `Projector (`Concrete c) -> Projector (Concrete_ident.to_rust_ast c)
-    | `Projector (`TupleField (nth, len)) ->
-        let c = SpecialNames.tuple_field len nth in
-        Projector (Concrete_ident.to_rust_ast c)
 
   and dlocal_ident (li : local_ident) : B.local_id =
     Newtypelocal_id (Newtypesymbol li.name)

engine/lib/rust_engine_types.ml

@@ -9,7 +9,7 @@ module Renamed = struct
   type binding_mode = Types.binding_mode2
   type borrow_kind = Types.borrow_kind2
   type def_id = Types.def_id_inner
-  type global_id = Types.global_id_inner
+  type global_id = Types.global_id
   type expr_kind = Types.expr_kind2
   type impl_expr = Types.impl_expr2
   type param = Types.param2

rust-engine/src/ast/identifiers.rs

@@ -1,8 +1,8 @@
 //! Identifier types used throughout the AST.
 //!
-//! This module defines:
+//! This module provides two kinds of identifiers:
 //! - `GlobalId`: fully-qualified paths like `std::mem::drop`
-//! - `LocalId`: local variable identifiers
+//! - `LocalId`: local identifiers
 
 use crate::symbol::Symbol;
 use hax_rust_engine_macros::*;