Rust Engine: add interning table, intern GlobalIds

CHANGELOG.md

@@ -14,7 +14,9 @@ Changes to the Rust Engine:
  - Add support for enums and structs to the Lean backend (type definitions,
    expressions, pattern-matching) (#1623)
  - Update name rendering infrastructure in the Lean backend (#1623, #1624)
-- Printers now emit proper diagnostics (PR #1669)
+ - 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)
@@ -29,7 +31,7 @@ Changes to the frontend:
 - Fix a regression affecting projection predicates (#1678)
 
 Changes to hax-lib:
-- New behavior for`hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag (#1685)
+- New behavior for `hax_lib::include`: it now forces inclusion when in contradiction with `-i` flag.
 
 Miscellaneous:
  - A lean tutorial has been added to the hax website (#1626)

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

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

justfile

@@ -52,7 +52,7 @@ expand *FLAGS:
 # Regenerate names in the Rust engine. Writes to `rust-engine/src/names/generated.rs`.
 regenerate-names:
   #!/usr/bin/env bash
-  OUTPUT_FILE=rust-engine/src/names/generated.rs
+  OUTPUT_FILE=rust-engine/src/ast/identifiers/global_id/generated.rs
   cargo hax -C --manifest-path engine/names/Cargo.toml \; into --output-dir $(dirname -- $OUTPUT_FILE) generate-rust-engine-names
   rustfmt "$OUTPUT_FILE"
 

rust-engine/src/ast.rs

@@ -973,7 +973,7 @@ pub enum ExprKind {
         /// The body of the loop.
         body: Expr,
         /// The kind of loop (e.g. `while`, `loop`, `for`...).
-        kind: LoopKind,
+        kind: Box<LoopKind>,
         /// An optional loop state, that makes explicit the state mutated by the
         /// loop.
         state: Option<LoopState>,

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::*;