[wp] builtin types are now registered in LogicBuiltins

src/plugins/wp/Lang.ml

@@ -197,17 +197,18 @@ let rec varpoly k x = function
   | y::ys -> if x = y then k else varpoly (succ k) x ys
 
 type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
+let builtin_types = Context.create "Wp.Lang.builtin_types"
 
-let builtins = Hashtbl.create 131
+let find_builtin name = Context.get builtin_types name
 
 let adt lt =
-  try match Hashtbl.find builtins lt.lt_name with
+  try match find_builtin lt.lt_name with
     | E_mdt m -> Mtype m
     | E_poly _ -> assert false
   with Not_found -> Atype lt
 
 let atype lt ts =
-  try match Hashtbl.find builtins lt.lt_name with
+  try match find_builtin lt.lt_name with
     | E_mdt m -> Logic.Data(Mtype m,ts)
     | E_poly ftau -> ftau ts
   with Not_found -> Logic.Data(Atype lt,ts)
@@ -279,30 +280,21 @@ end
 (* --- Datatypes                                                          --- *)
 (* -------------------------------------------------------------------------- *)
 
-let get_builtin_type ~name ~link ~library =
-  try match Hashtbl.find builtins name with
-    | E_mdt m -> Mtype m
-    | E_poly _ -> assert false
-  with Not_found ->
-    let m = new_extern ~link ~library ~debug:name in
-    Hashtbl.add builtins name (E_mdt m) ; Mtype m
-
-let set_builtin_type ~name ~link ~library =
-  let m = new_extern ~link ~library ~debug:name in
-  Hashtbl.add builtins name (E_mdt m)
-
-let set_builtin_poly ~name f =
-  Hashtbl.add builtins name (E_poly f)
+let get_builtin_type ~name =
+  match find_builtin name with
+  | E_mdt m -> Mtype m
+  | E_poly _ -> assert false
 
 let mem_builtin_type ~name =
-  Hashtbl.mem builtins name
+  try ignore (find_builtin name) ; true
+  with Not_found -> false
 
-let is_builtin lt = Hashtbl.mem builtins lt.lt_name
+let is_builtin lt = mem_builtin_type lt.lt_name
 
 let is_builtin_type ~name = function
   | Data(Mtype m,_) ->
       begin
-        try match Hashtbl.find builtins name with
+        try match find_builtin name with
           | E_mdt m0 -> m == m0
           | _ -> false
         with Not_found -> false
@@ -527,6 +519,9 @@ let generated_p ?context name =
     m_source = generated ?context name
   }
 
+let extern_t name ~link ~library =
+  new_extern ~link ~library ~debug:name
+
 module Fun =
 struct
 

src/plugins/wp/Lang.mli

@@ -73,6 +73,7 @@ and field =
   | Cfield of fieldinfo
 and tau = (field,adt) Logic.datatype
 
+type t_builtin = E_mdt of mdt | E_poly of (tau list -> tau)
 
 type lfun =
   | ACSL of Cil_types.logic_info (** Registered in Definition.t,
@@ -94,11 +95,9 @@ and source =
   | Extern of Engine.link extern
 
 val mem_builtin_type : name:string -> bool
-val set_builtin_poly : name:string -> (tau list -> tau) -> unit
-val set_builtin_type : name:string -> link:string infoprover -> library:string -> unit
-val get_builtin_type : name:string -> link:string infoprover -> library:string -> adt
 val is_builtin : logic_type_info -> bool
 val is_builtin_type : name:string -> tau -> bool
+val get_builtin_type : name:string -> adt
 val datatype : library:string -> string -> adt
 val record :
   link:string infoprover -> library:string -> (string * tau) list -> adt
@@ -151,6 +150,9 @@ val generated_f : ?context:bool -> ?category:lfun category ->
 
 val generated_p : ?context:bool -> string -> lfun
 
+val extern_t:
+  string -> link:string infoprover -> library:library -> mdt
+
 (** {2 Sorting and Typing} *)
 
 val tau_of_comp : compinfo -> tau
@@ -174,6 +176,7 @@ val t_datatype : adt -> tau list -> tau
 val pointer : (typ -> tau) Context.value (** type of pointers *)
 val floats : (c_float -> tau) Context.value (** type of floats *)
 val poly : string list Context.value (** polymorphism *)
+val builtin_types: (string -> t_builtin) Context.value (* builtin types *)
 val parameters : (lfun -> sort list) -> unit (** definitions *)
 
 val name_of_lfun : lfun -> string

src/plugins/wp/LogicBuiltins.ml

@@ -106,6 +106,7 @@ type driver = {
   description : string;
   includes : string list;
   hlogic : (string , sigfun list) Hashtbl.t;
+  htypes : (string , t_builtin) Hashtbl.t;
   hdeps : (string, string list) Hashtbl.t;
   hoptions :
     (string (* library *) * string (* group *) * string (* name *), string list)
@@ -168,6 +169,12 @@ let register ?source name kinds link =
   let entry = (kinds,link) in
   Hashtbl.add driver.hlogic name (entry::sigs)
 
+let register_type ?source name builtin =
+  let driver = cdriver_rw () in
+  if Hashtbl.mem driver.htypes name then
+    Wp_parameters.warning ?source "Redifinition of type %s" name ;
+  Hashtbl.add driver.htypes name builtin
+
 let iter_table f =
   let items = ref [] in
   Hashtbl.iter
@@ -239,12 +246,12 @@ let add_ctor ~source name kinds ~library ~link () =
   let lfun = Lang.extern_s ~library ~category ~params ~link name in
   register ~source name kinds (LFUN lfun)
 
-let add_type ~source name ~library ?(link=Lang.infoprover name) () =
-  if Lang.mem_builtin_type ~name then
-    Wp_parameters.warning ~source "Redefinition of type '%s'" name ;
-  Lang.set_builtin_type ~name ~library ~link
+let add_type ?source name ~library ?(link=Lang.infoprover name) () =
+  let mdt = Lang.extern_t name ~link ~library in
+  register_type ?source name (E_mdt mdt)
 
-let hack_type name poly = Lang.set_builtin_poly ~name poly
+let hack_type name poly =
+  register_type name (E_poly poly)
 
 type sanitizer = driver_dir:string -> string -> string
 let sanitizers : ( string * string , sanitizer ) Hashtbl.t = Hashtbl.create 10
@@ -298,6 +305,7 @@ let builtin_driver = {
   description = "builtin driver";
   includes = [];
   hlogic = Hashtbl.create 131;
+  htypes = Hashtbl.create 131;
   hdeps  = Hashtbl.create 31;
   hoptions = Hashtbl.create 131;
   locked = false
@@ -310,6 +318,25 @@ let add_builtin name kinds lfun =
   else
     Context.bind driver builtin_driver (register name kinds) phi
 
+let add_type ?source name ~library ?link () =
+  if Context.defined driver then
+    add_type ?source name ~library ?link ()
+  else
+    Context.bind driver builtin_driver
+      (add_type ?source name ~library ?link) ()
+
+let hack_type name poly =
+  if Context.defined driver then hack_type name poly
+  else Context.bind driver builtin_driver hack_type name poly
+
+let find_type name =
+  Hashtbl.find (cdriver_ro ()).htypes name
+let find_type name =
+  if Context.defined driver then find_type name
+  else Context.bind driver builtin_driver find_type name
+
+let () = Context.set Lang.builtin_types find_type
+
 let new_driver ~id ?(base=builtin_driver)
     ?(descr=id) ?(includes=[]) ?(configure=fun () -> ()) () =
   lock base ;
@@ -318,6 +345,7 @@ let new_driver ~id ?(base=builtin_driver)
     description = descr ;
     includes = includes @ base.includes ;
     hlogic = Hashtbl.copy base.hlogic ;
+    htypes = Hashtbl.copy base.htypes ;
     hdeps  = Hashtbl.copy base.hdeps ;
     hoptions = Hashtbl.copy base.hoptions ;
     locked = false

src/plugins/wp/LogicBuiltins.mli

@@ -77,7 +77,7 @@ val add_library : string -> string list -> unit
 
 val add_alias : source:Filepath.position -> string -> kind list -> alias:string -> unit -> unit
 
-val add_type : source:Filepath.position -> string -> library:string ->
+val add_type : ?source:Filepath.position -> string -> library:string ->
   ?link:string infoprover -> unit -> unit
 
 val add_ctor : source:Filepath.position -> string -> kind list ->

src/plugins/wp/Vlist.ml

@@ -53,7 +53,8 @@ let l_repeat = Lang.(E.({
 
 (*--- Typechecking ---*)
 
-let a_list = Lang.get_builtin_type ~library ~name:t_list ~link:l_list
+let () = LogicBuiltins.add_type t_list ~library ~link:l_list ()
+let a_list = Lang.get_builtin_type t_list
 
 let vlist_get_tau = function
   | None -> invalid_arg "a list operator without result type"