Fix implicit shadowing by an auto-generated "pointer-name" for a struct

src/3d/Ast.fst

@@ -530,7 +530,7 @@ noeq
 type typedef_names = {
   typedef_name: ident;
   typedef_abbrev: ident;
-  typedef_ptr_abbrev: ident;
+  typedef_ptr_abbrev: option ident;
   typedef_attributes: list attribute
 }
 
@@ -1174,6 +1174,11 @@ and print_switch_case (s:switch_case) : ML string =
                  (print_expr head)
                  (String.concat "\n" (List.map print_case cases))
 
+let option_to_string (f:'a -> ML string) (x:option 'a) : ML string =
+  match x with
+  | Some x -> f x
+  | _ -> ""
+
 let print_decl' (d:decl') : ML string =
   match d with
   | ModuleAbbrev i m -> Printf.sprintf "module %s = %s" (print_ident i) (print_ident m)
@@ -1205,7 +1210,7 @@ let print_decl' (d:decl') : ML string =
                     (match wopt with | None -> "" | Some e -> " where " ^ print_expr e)
                     (String.concat "\n" (List.map print_field fields))
                     (ident_to_string td.typedef_abbrev)
-                    (ident_to_string td.typedef_ptr_abbrev)
+                    (option_to_string ident_to_string td.typedef_ptr_abbrev)
   | CaseType td params switch_case ->
     Printf.sprintf "casetype %s%s {\n\
                         %s \n\
@@ -1214,7 +1219,7 @@ let print_decl' (d:decl') : ML string =
                     (print_params params)
                     (print_switch_case switch_case)
                     (ident_to_string td.typedef_abbrev)
-                    (ident_to_string td.typedef_ptr_abbrev)
+                    (option_to_string ident_to_string td.typedef_ptr_abbrev)
   | OutputType out_t -> "Printing for output types is TBD"
   | ExternType _ -> "Printing for extern types is TBD"
   | ExternFn _ _ _

src/3d/Binding.fst

@@ -1892,7 +1892,7 @@ let initial_global_env () =
   in
   let nullary_decl i =
     let td_name =
-      { typedef_name = i; typedef_abbrev = i; typedef_ptr_abbrev = i; typedef_attributes = [] }
+      { typedef_name = i; typedef_abbrev = i; typedef_ptr_abbrev = None; typedef_attributes = [] }
     in
     mk_decl (Record td_name [] None []) dummy_range [] true
   in
@@ -2059,7 +2059,7 @@ let initial_global_env () =
             ({
                 typedef_name = void_ident;
                 typedef_abbrev = void_ident;
-                typedef_ptr_abbrev = void_ident;
+                typedef_ptr_abbrev = None;
                 typedef_attributes = []
               }))
           dummy_range

src/3d/Desugar.fst

@@ -391,7 +391,7 @@ let resolve_typedef_names (env:qenv) (td_names:typedef_names) : ML typedef_names
   {
     typedef_name = resolve_ident env td_names.typedef_name;
     typedef_abbrev = resolve_ident env td_names.typedef_abbrev;
-    typedef_ptr_abbrev = resolve_ident env td_names.typedef_ptr_abbrev;
+    typedef_ptr_abbrev = map_opt (resolve_ident env) td_names.typedef_ptr_abbrev;
     typedef_attributes = List.map (resolve_typedef_attribute env) td_names.typedef_attributes;
   }
 

src/3d/TranslateForInterpreter.fst

@@ -950,7 +950,7 @@ let make_tdn (i:A.ident) =
   {
     typedef_name = i;
     typedef_abbrev = with_dummy_range (to_ident' "");
-    typedef_ptr_abbrev = with_dummy_range (to_ident' "");
+    typedef_ptr_abbrev = None;
     typedef_attributes = []
   }
 

src/3d/TypeSizes.fst

@@ -87,7 +87,9 @@ let extend_with_size_of_typedef_names (env:env_t) (names:typedef_names) (size:si
   : ML unit
   = extend_with_size_of_ident env names.typedef_name size a;
     extend_with_size_of_ident env names.typedef_abbrev size a;
-    extend_with_size_of_ident env names.typedef_ptr_abbrev Variable a
+    (match names.typedef_ptr_abbrev with
+     | None -> ()
+     | Some nm -> extend_with_size_of_ident env nm Variable a)
 
 let size_and_alignment_of_typ (env:env_t) (t:typ)
   : ML (size & alignment)

src/3d/ocaml/parser.mly

@@ -20,11 +20,6 @@
   let with_range (x:'a) (l:Lexing.position) : 'a with_meta_t =
       Ast.with_range x (mk_pos l, mk_pos l)
 
-  let pointer_name j p =
-      match p with
-      | None -> {j with v={j.v with name="P"^j.v.name}}
-      | Some k -> k
-
   let parse_int_and_type r (s:string) : Z.t * string * integer_type =
       let r = mk_pos r, mk_pos r in
       let s', t = parse_int_suffix s in
@@ -509,30 +504,29 @@ decl_no_range:
   | b=attributes TYPEDEF STRUCT i=IDENT ps=parameters w=where_opt
     LBRACE fields=fields
     RBRACE j=IDENT p=typedef_pointer_name_opt SEMICOLON
-    {  let k = pointer_name j p in
-       Record(mk_td b i j k, ps, w, fields)
+    {  
+        Record(mk_td b i j p, ps, w, fields)
     }
   | b=attributes CASETYPE i=IDENT ps=parameters
     LBRACE SWITCH LPAREN e=IDENT RPAREN
            LBRACE cs=cases
            RBRACE
     RBRACE j=IDENT p=typedef_pointer_name_opt SEMICOLON
     {
-        let k = pointer_name j p in
-        let td = mk_td b i j k in
+        let td = mk_td b i j p in
         CaseType(td, ps, (with_range (Identifier e) ($startpos(i)), cs))
     }
 
   | OUTPUT TYPEDEF STRUCT i=IDENT
     LBRACE out_flds=right_flexible_nonempty_list(SEMICOLON, out_field) RBRACE
     j=IDENT p=typedef_pointer_name_opt SEMICOLON
-    {  let k = pointer_name j p in
-       let td = mk_td [] i j k in       
-       OutputType ({out_typ_names=td; out_typ_fields=out_flds; out_typ_is_union=false}) }
+    {
+       let td = mk_td [] i j p in
+       OutputType ({out_typ_names=td; out_typ_fields=out_flds; out_typ_is_union=false})
+    }
 
   | EXTERN TYPEDEF STRUCT i=IDENT j=IDENT
-    {  let k = pointer_name j None in
-       let td = mk_td [] i j k in
+    {  let td = mk_td [] i j None in
        ExternType td
     }
 

src/3d/tests/Align.3d

@@ -54,6 +54,30 @@ typedef struct _F
    E(false) f2; //4 byte aligned; needs 3 bytes of padding
 } F;
 
+
+typedef UINT64 PCASE_T;
+
+#define KK 1000 
+
+casetype _CASE_T
+{
+    switch (KK)
+    {
+        case 1:
+            UINT64 f;
+        case 2:
+            UINT16 g;
+    }
+} CASE_T;
+
+entrypoint
+aligned
+typedef struct _USE_T
+{
+    PCASE_T pt;
+    UINT16   other;
+} USE_T;
+
 refining "AlignC.h" {
- A, B, C, D, E, F
+ A, B, C, D, E, F, USE_T
 }

src/3d/tests/AlignC.h

@@ -43,3 +43,9 @@ typedef struct _F
   uint8_t f1;
   E f2;
 } F;
+
+typedef struct _USE_T
+{
+   uint64_t pt;
+   uint16_t other;
+} USE_T;