Remove the cparser/Builtins module

Move its definitions to modules C (the type `builtins`) and Env
(the operations that deal with the initial environment).

Reasons for the refactoring:
1- The name "Builtins" will soon be reused for a Coq module
2- `Env.initial()` makes more sense than `Builtins.environment()`.

12 files changed, 62 insertions, 87 deletions

diff --git a/cparser/Builtins.ml b/cparser/Builtins.ml
deleted file mode 100644
index 8eb1abfd..00000000
--- a/cparser/Builtins.ml
+++ /dev/null
@@ -1,54 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-(* Compiler built-ins *)
-
-open C
-open Cutil
-
-let env = ref Env.empty
-let idents = ref []
-let decls = ref []
-
-let environment () = !env
-let identifiers () = !idents
-let declarations () = List.rev !decls
-
-let add_typedef (s, ty) =
-  let (id, env') = Env.enter_typedef !env s ty in
-  env := env';
-  idents := id :: !idents;
-  decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
-
-let add_function (s, (res, args, va)) =
-  let ty =
-    TFun(res,
-         Some (List.map (fun ty -> (Env.fresh_ident "", ty)) args),
-         va, []) in
-  let (id, env') = Env.enter_ident !env s Storage_extern ty in
-  env := env';
-  idents := id :: !idents;
-  decls := {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
-
-type t = {
-  typedefs: (string * C.typ) list;
-  functions: (string * (C.typ * C.typ list * bool)) list
-}
-
-let set blt =
-  env := Env.empty;
-  idents := [];
-  List.iter add_typedef blt.typedefs;
-  List.iter add_function blt.functions
diff --git a/cparser/Builtins.mli b/cparser/Builtins.mli
deleted file mode 100644
index 7f9d78a9..00000000
--- a/cparser/Builtins.mli
+++ /dev/null
@@ -1,25 +0,0 @@
-(* *********************************************************************)
-(*                                                                     *)
-(*              The Compcert verified compiler                         *)
-(*                                                                     *)
-(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
-(*                                                                     *)
-(*  Copyright Institut National de Recherche en Informatique et en     *)
-(*  Automatique.  All rights reserved.  This file is distributed       *)
-(*  under the terms of the GNU General Public License as published by  *)
-(*  the Free Software Foundation, either version 2 of the License, or  *)
-(*  (at your option) any later version.  This file is also distributed *)
-(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
-(*                                                                     *)
-(* *********************************************************************)
-
-val environment: unit -> Env.t
-val identifiers: unit -> C.ident list
-val declarations: unit -> C.globdecl list
-
-type t = {
-  typedefs: (string * C.typ) list;
-  functions: (string * (C.typ * C.typ list * bool)) list
-}
-
-val set: t -> unit
diff --git a/cparser/C.mli b/cparser/C.mli
index cc8d4065..15717565 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -264,3 +264,10 @@ and globdecl_desc =
   | Gpragma of string                   (* #pragma directive *)
 
 type program = globdecl list
+
+(** Builtin types and functions *)
+
+type builtins = {
+  builtin_typedefs: (string * typ) list;
+  builtin_functions: (string * (typ * typ list * bool)) list
+}
diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index ef62edd6..17caf19a 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -117,7 +117,7 @@ let traverse_program
           pragma env g.gloc s;
           env in
       traverse env gl in
-  traverse (Builtins.environment ()) p
+  traverse (Env.initial ()) p
 
 (* Unknown attributes warning *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b2934c67..eea60127 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -3089,7 +3089,7 @@ let _ = elab_funbody_f := elab_funbody
 
 let elab_file prog =
   reset();
-  let env = Builtins.environment () in
+  let env = Env.initial () in
   let elab_def env d = snd (elab_definition false false false env d) in
   ignore (List.fold_left elab_def env prog);
   let p = elaborated_program () in
diff --git a/cparser/Env.ml b/cparser/Env.ml
index 5fa4571a..4723a725 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -276,6 +276,46 @@ let add_enum env id info =
 let add_types env_old env_new =
   { env_new with env_ident = env_old.env_ident;env_scope = env_old.env_scope;}
 
+(* Initial environment describing the built-in types and functions *)
+
+module Init = struct
+
+let env = ref empty
+let idents = ref []
+let decls = ref []
+
+let no_loc = ("", -1)
+
+let add_typedef (s, ty) =
+  let (id, env') = enter_typedef !env s ty in
+  env := env';
+  idents := id :: !idents;
+  decls := {gdesc = Gtypedef(id, ty); gloc = no_loc} :: !decls
+
+let add_function (s, (res, args, va)) =
+  let ty =
+    TFun(res,
+         Some (List.map (fun ty -> (fresh_ident "", ty)) args),
+         va, []) in
+  let (id, env') = enter_ident !env s Storage_extern ty in
+  env := env';
+  idents := id :: !idents;
+  decls :=
+    {gdesc = Gdecl(Storage_extern, id, ty, None); gloc = no_loc} :: !decls
+
+end
+
+let initial () = !Init.env
+let initial_identifiers () = !Init.idents
+let initial_declarations () = List.rev !Init.decls
+
+let set_builtins blt =
+  Init.env := empty;
+  Init.idents := [];
+  Init.decls := [];
+  List.iter Init.add_typedef blt.builtin_typedefs;
+  List.iter Init.add_function blt.builtin_functions
+
 (* Error reporting *)
 
 open Printf
diff --git a/cparser/Env.mli b/cparser/Env.mli
index 7ea2c514..1baab68f 100644
--- a/cparser/Env.mli
+++ b/cparser/Env.mli
@@ -77,3 +77,10 @@ val add_typedef : t -> C.ident -> typedef_info -> t
 val add_enum : t -> C.ident -> enum_info -> t
 
 val add_types : t -> t -> t
+
+(* Initial environment describing the builtin types and functions *)
+
+val initial: unit -> t
+val initial_identifiers: unit -> C.ident list
+val initial_declarations: unit -> C.globdecl list
+val set_builtins: C.builtins -> unit
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 010d12f3..458e51d3 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -38,10 +38,10 @@ let intPtrType = TPtr(TInt(IInt, []), [])
 let sizeType() = TInt(size_t_ikind(), [])
 
 let builtins = {
-  Builtins.typedefs = [
+  builtin_typedefs = [
   "__builtin_va_list", voidPtrType
 ];
-  Builtins.functions = [
+  builtin_functions = [
   "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
   "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
   "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 3c27f3a9..4c70c7ae 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -418,4 +418,4 @@ let program p =
     | _ -> false
     end;
   Hashtbl.clear byteswapped_fields;
-  transf_globdecls (Builtins.environment()) [] p
+  transf_globdecls (Env.initial()) [] p
diff --git a/cparser/Rename.ml b/cparser/Rename.ml
index eb31eaf0..64412194 100644
--- a/cparser/Rename.ml
+++ b/cparser/Rename.ml
@@ -246,7 +246,7 @@ let rec globdecls env accu = function
 (* Reserve names of builtins *)
 
 let reserve_builtins () =
-  List.fold_left enter_public empty_env (Builtins.identifiers())
+  List.fold_left enter_public empty_env (Env.initial_identifiers())
 
 (* Reserve global declarations with public visibility *)
 
diff --git a/cparser/Transform.ml b/cparser/Transform.ml
index 0a2ce3bb..349a3155 100644
--- a/cparser/Transform.ml
+++ b/cparser/Transform.ml
@@ -227,4 +227,4 @@ let program
       in
         transf_globdecls env' ({g with gdesc = desc'} :: accu) gl
 
-  in transf_globdecls (Builtins.environment()) [] p
+  in transf_globdecls (Env.initial()) [] p
diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 66b497cc..d25f70c6 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -399,4 +399,4 @@ let rec unblock_glob env accu = function
 let program p =
   next_scope_id := 0;
   {gloc = no_loc; gdesc = Gdecl(Storage_extern, debug_id, debug_ty, None)} ::
-  unblock_glob (Builtins.environment()) [] p
+  unblock_glob (Env.initial()) [] p