Merge pull request #1199 from cryspen/rework-name-repr

Engine: rework global name representation

Author: W95Psp

engine/backends/coq/coq/coq_backend.ml

@@ -68,7 +68,8 @@ module AST = Ast.Make (InputLanguage)
 module BackendOptions = Backend.UnitBackendOptions
 open Ast
 module CoqNamePolicy = Concrete_ident.DefaultNamePolicy
-module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy)
+module U = Ast_utils.Make (InputLanguage)
+module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy)
 open AST
 
 let hardcoded_coq_headers =
@@ -492,7 +493,7 @@ struct
           let crate =
             String.capitalize
               (Option.value ~default:"(TODO CRATE)"
-                 (Option.map ~f:fst current_namespace))
+                 (Option.bind ~f:List.hd current_namespace))
           in
           let concat_capitalize l =
             String.concat ~sep:"_" (List.map ~f:String.capitalize l)
@@ -509,7 +510,7 @@ struct
                   (crate
                    :: List.drop_last_exn
                         (Option.value ~default:[]
-                           (Option.map ~f:snd current_namespace))
+                           (Option.bind ~f:List.tl current_namespace))
                   @ xs)
             | [ a ] -> a
             | xs -> concat_capitalize_include xs
@@ -729,7 +730,7 @@ struct
 
       method concrete_ident ~local:_ id : document =
         string
-          (match id.definition with
+          (match id.name with
           | "not" -> "negb"
           | "eq" -> "t_PartialEq_f_eq"
           | "lt" -> "t_PartialOrd_f_lt"
@@ -765,12 +766,13 @@ let translate m _ ~bundles:_ (items : AST.item list) : Types.file list =
   let my_printer = make m in
   U.group_items_by_namespace items
   |> Map.to_alist
+  |> List.filter_map ~f:(fun (_, items) ->
+         let* first_item = List.hd items in
+         Some ((RenderId.render first_item.ident).path, items))
   |> List.map ~f:(fun (ns, items) ->
          let mod_name =
            String.concat ~sep:"_"
-             (List.map
-                ~f:(map_first_letter String.uppercase)
-                (fst ns :: snd ns))
+             (List.map ~f:(map_first_letter String.uppercase) ns)
          in
          let sourcemap, contents =
            let annotated = my_printer#entrypoint_modul items in

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -74,7 +74,8 @@ module AST = Ast.Make (InputLanguage)
 module BackendOptions = Backend.UnitBackendOptions
 open Ast
 module CoqNamePolicy = Concrete_ident.DefaultNamePolicy
-module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (CoqNamePolicy)
+module U = Ast_utils.Make (InputLanguage)
+module RenderId = Concrete_ident.MakeRenderAPI (CoqNamePolicy)
 open AST
 
 module SSProveLibrary : Library = struct
@@ -553,7 +554,7 @@ end
 
 module Context = struct
   type t = {
-    current_namespace : string * string list;
+    current_namespace : string list;
     analysis_data : StaticAnalysis.analysis_data;
   }
 end
@@ -618,10 +619,10 @@ module TransformToInputLanguage (* : PHASE *) =
 (*   | None -> Error.unimplemented ~details:err span *)
 
 let pconcrete_ident (id : Ast.concrete_ident) : string =
-  U.Concrete_ident_view.to_definition_name id
+  (RenderId.render id).name
 
 let plocal_ident (e : Local_ident.t) : string =
-  U.Concrete_ident_view.local_ident
+  RenderId.local_ident
     (match String.chop_prefix ~prefix:"impl " e.name with
     | Some name ->
         let name = "impl_" ^ Int.to_string ([%hash: string] name) in
@@ -690,7 +691,7 @@ struct
     | Bool b -> SSP.AST.Const_bool b
 
   let operators =
-    let c = Ast.Global_ident.of_name Value in
+    let c = Ast.Global_ident.of_name ~value:true in
     [
       (c Rust_primitives__hax__array_of_list, (3, [ ""; ".a["; "]<-"; "" ]));
       (c Core__ops__index__Index__index, (2, [ ""; ".a["; "]" ]));
@@ -1556,8 +1557,8 @@ struct
             let id = [%show: concrete_ident] macro in
             Error.raise { kind = UnsupportedMacro { id }; span = e.span }
           in
-          match U.Concrete_ident_view.to_view macro with
-          | { crate = "hacspec_lib"; path = _; definition = name } -> (
+          match RenderId.render macro with
+          | { path = "hacspec_lib" :: _; name } -> (
               match name with
               | "public_nat_mod" ->
                   let open Hacspeclib_macro_parser in
@@ -1713,7 +1714,7 @@ struct
               | _ -> unsupported ())
           | _ -> unsupported ())
       | Use { path; is_external; rename } ->
-          let _ns_crate, _ns_path = ctx.current_namespace in
+          let _ns_path = ctx.current_namespace in
           if is_external then []
           else
             [ SSP.AST.Require (None, (* ns_crate:: ns_path @ *) path, rename) ]
@@ -1989,10 +1990,7 @@ let print_item (analysis_data : StaticAnalysis.analysis_data) (item : AST.item)
     : SSP.AST.decl list =
   let (module Print) =
     make
-      {
-        current_namespace = U.Concrete_ident_view.to_namespace item.ident;
-        analysis_data;
-      }
+      { current_namespace = (RenderId.render item.ident).path; analysis_data }
   in
   Print.pitem item
 
@@ -2422,12 +2420,14 @@ let translate _ (_bo : BackendOptions.t) ~(bundles : AST.item list list)
   let analysis_data = StaticAnalysis.analyse items in
   U.group_items_by_namespace items
   |> Map.to_alist
+  |> List.filter_map
+       ~f:
+         (snd >> List.hd
+         >> Option.map ~f:(fun i -> ((RenderId.render i.ident).path, items)))
   |> List.map ~f:(fun (ns, items) ->
          let mod_name =
            String.concat ~sep:"_"
-             (List.map
-                ~f:(map_first_letter String.uppercase)
-                (fst ns :: snd ns))
+             (List.map ~f:(map_first_letter String.uppercase) ns)
          in
          let file_content =
            hardcoded_coq_headers ^ "\n"

engine/backends/easycrypt/easycrypt_backend.ml

@@ -22,7 +22,8 @@ include
 module BackendOptions = Backend.UnitBackendOptions
 module AST = Ast.Make (InputLanguage)
 module ECNamePolicy = Concrete_ident.DefaultNamePolicy
-module U = Ast_utils.MakeWithNamePolicy (InputLanguage) (ECNamePolicy)
+module U = Ast_utils.Make (InputLanguage)
+module RenderId = Concrete_ident.MakeRenderAPI (ECNamePolicy)
 open AST
 
 module RejectNotEC (FA : Features.T) = struct
@@ -88,14 +89,11 @@ module NM = struct
 
         { the with subnms = Map.Poly.update ~f:update the.subnms name }
 
-  let push_using_namespace (the : nmtree) (nm : string * string list)
-      (item : AST.item) =
-    push_using_longname the (List.rev (fst nm :: snd nm)) item
+  let push_using_namespace (the : nmtree) (nm : string list) (item : AST.item) =
+    push_using_longname the (List.rev nm) item
 
   let push (the : nmtree) (item : AST.item) =
-    push_using_namespace the
-      (U.Concrete_ident_view.to_namespace item.ident)
-      item
+    push_using_namespace the (RenderId.render item.ident).path item
 end
 
 let suffix_of_size (size : Ast.size) =
@@ -132,7 +130,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
              match item.v with
              | Fn { name; generics; body; params }
                when List.is_empty generics.params ->
-                 let name = U.Concrete_ident_view.to_definition_name name in
+                 let name = (RenderId.render name).name in
 
                  doit_fn fmt (name, params, body)
              | Fn _ -> assert false
@@ -166,7 +164,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
          pp_param)
       params doit_stmt body
   and doit_concrete_ident (fmt : Formatter.t) (p : Concrete_ident.t) =
-    Stdlib.Format.fprintf fmt "%s" (U.Concrete_ident_view.to_definition_name p)
+    Stdlib.Format.fprintf fmt "%s" (RenderId.render p).name
   and doit_type (fmt : Formatter.t) (typ : ty) =
     match typ with
     | TBool -> assert false
@@ -281,7 +279,7 @@ let translate' (_bo : BackendOptions.t) (items : AST.item list) :
              || eq_name Core__cmp__PartialEq__ne op
              || eq_name Core__cmp__PartialEq__eq op) ->
         Stdlib.Format.fprintf fmt "(%a) %s (%a)" doit_expr e1
-          (match U.Concrete_ident_view.to_definition_name op with
+          (match (RenderId.render op).name with
           | "bitxor" -> "^"
           | "bitand" -> "&"
           | "bitor" -> "|"