motoko-san: use id in AdtI, ConT

serokell · May 20, 2024 · 3a2261a · 3a2261a
1 parent ae88ee0
commit 3a2261a
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 15 deletions.
diff --git a/src/viper/pretty.ml b/src/viper/pretty.ml
@@ -27,9 +27,9 @@ let rec pp_prog ppf p =
 
 and pp_item ppf i =
   match i.it with
-  | AdtI (name, params, cons) ->
+  | AdtI (id, params, cons) ->
     fprintf ppf "@[<2>adt %s@;%a@;%a@]"
-      name
+      id.it
       pp_adt_params params
       pp_adt_cons cons
   | FieldI (id, typ) ->
@@ -54,20 +54,20 @@ and pp_adt_params ppf = function
       fprintf ppf "[%a]"
         (pp_print_list pp_adt_param ~pp_sep:comma) params
 
-and pp_adt_param ppf param = fprintf ppf "%s" param
+and pp_adt_param ppf param = fprintf ppf "%s" param.it
 
 and pp_adt_cons ppf cons =
   fprintf ppf "@[<v 2>{ %a }@]"
     (pp_print_list pp_adt_con) cons
 
 and pp_adt_con ppf con =
   fprintf ppf "%s@[(%a)@]"
-    con.con_name
+    con.con_name.it
     (pp_print_list ~pp_sep:comma pp_adt_con_field) (List.mapi (fun i fld -> con, i, fld) con.con_fields)
 
 and pp_adt_con_field ppf (con, i, con_field) =
   fprintf ppf "%s$%s : %a"
-    con.con_name
+    con.con_name.it
     (string_of_int i)
     pp_typ con_field
 
@@ -123,10 +123,10 @@ and pp_typ ppf t =
   | RefT -> pr ppf "Ref"
   | ArrayT -> pr ppf "Array"
   | TupleT -> pr ppf "Tuple"
-  | ConT(name, []) -> fprintf ppf "%s" name
-  | ConT(name, ts) ->
+  | ConT(con, []) -> fprintf ppf "%s" con.it
+  | ConT(con, ts) ->
       fprintf ppf "@[%s[%a]@]"
-        name
+        con.it
         (pp_print_list ~pp_sep:comma pp_typ) ts
 
 and pp_exp ppf exp =

diff --git a/src/viper/syntax.ml b/src/viper/syntax.ml
@@ -11,12 +11,12 @@ type prog = (item list, info) Source.annotated_phrase
 and item = (item', info) Source.annotated_phrase
 and item' =
   (* | import path *)
-  | AdtI of string * string list * adt_con list
+  | AdtI of id * id list * adt_con list
   | FieldI of id * typ
   | MethodI of id * par list * par list * exp list * exp list * seqn option
   | InvariantI of string * exp
 
-and adt_con = { con_name : string; con_fields : typ list }
+and adt_con = { con_name : id; con_fields : typ list }
 
 and par = id * typ
 
@@ -101,5 +101,5 @@ and typ' =
   | RefT
   | ArrayT
   | TupleT
-  | ConT of string * typ list
+  | ConT of id * typ list
 
diff --git a/src/viper/trans.ml b/src/viper/trans.ml
@@ -268,15 +268,15 @@ and dec_field' ctxt d =
   (* type declarations*)
   | M.(TypD (typ_id, typ_binds, {note = T.Variant cons;_})) ->
     ctxt, None, None, fun _ ->
-      let adt_param tb = tb.it.M.var.it in
+      let adt_param tb = id tb.it.M.var in
       let adt_con con = begin
-        { con_name = con.T.lab;
+        { con_name = !!! Source.no_region con.T.lab;
           con_fields = match con.T.typ with
             | T.Tup ts -> List.map tr_typ ts
             | t -> [tr_typ t]
         }
       end in
-      AdtI (typ_id.it,
+      AdtI ({ typ_id with note = NoInfo },
             List.map adt_param typ_binds,
             List.map adt_con cons),
       NoInfo
@@ -733,7 +733,7 @@ and tr_typ' typ =
   | _, T.Prim T.Bool -> BoolT
   | _, T.Array _ -> ArrayT     (* Viper arrays are not parameterised by element type *)
   | _, T.Tup   _ -> TupleT     (* Viper tuples are not parameterised by element type *)
-  | T.Con (con, ts), _ -> ConT (Mo_types.Cons.name con, List.map tr_typ ts)
+  | T.Con (con, ts), _ -> ConT (!!! Source.no_region (Mo_types.Cons.name con), List.map tr_typ ts)
   | _, t -> unsupported Source.no_region (Mo_types.Arrange_type.typ t)
 
 and is_mut t =