cparser/Env: testing whether two Env.t define the same types

Author: xavierleroy

cparser/Elab.ml

@@ -2580,7 +2580,7 @@ let elab_expr ctx loc env a =
 
 let elab_attrib_expr loc env a =
   let (b, env') = elab_expr ctx_constexp loc env a in
-  if env' != env then
+  if not (Env.same_types env' env) then
     fatal_error loc "cannot define new types within attributes";
   b
 

cparser/Env.ml

@@ -53,6 +53,15 @@ module IdentMap = struct
   let add id data m =
     let l = try StringMap.find id.name m with Not_found -> [] in
     StringMap.add id.name ((id, data) :: l) m
+
+  (* Comparison *)
+  let compare m1 m2 =
+    if m1 == m2 then 0 else StringMap.compare Stdlib.compare m1 m2
+
+  let compare_named m1 m2 =
+    if m1 == m2 then 0 else
+      StringMap.compare Stdlib.compare
+                        (StringMap.remove "" m1) (StringMap.remove "" m2)
 end
 
 let gensym = ref 0
@@ -320,6 +329,18 @@ let set_builtins blt =
 let is_builtin name =
   ident_is_bound !Init.env name
 
+(* Do two environments define the same struct/union/enum types? *)
+
+let same_types env1 env2 =
+  env1 == env2
+  || (IdentMap.compare env1.env_tag env2.env_tag = 0
+      && IdentMap.compare env1.env_enum env2.env_enum = 0)
+
+let same_named_types env1 env2 =
+  env1 == env2
+  || (IdentMap.compare_named env1.env_tag env2.env_tag = 0
+      && IdentMap.compare_named env1.env_enum env2.env_enum = 0)
+
 (* Error reporting *)
 
 open Printf

cparser/Env.mli

@@ -86,3 +86,10 @@ val initial_identifiers: unit -> C.ident list
 val initial_declarations: unit -> C.globdecl list
 val set_builtins: C.builtins -> unit
 val is_builtin : string -> bool
+
+(* Comparing two environments.  One of the environments is assumed
+   to have been obtained from the other environment by a sequence
+   of zero, one or several [add_*] operations. *)
+
+val same_types: t -> t -> bool
+val same_named_types: t -> t -> bool