diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index bf5c0054260a2191d2c4347ab095a4bff4c634dc..40f7cf42aeb0cd3a2aecd03c5dfeb61326bb5327 100644
--- a/src/plugins/wp/Lang.ml
+++ b/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
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 96c978a24930266759ef828cf87daa3cb0ff5bf8..3a469eb93f6d2ae03392de145c08447b2b00a873 100644
--- a/src/plugins/wp/Lang.mli
+++ b/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
diff --git a/src/plugins/wp/LogicBuiltins.ml b/src/plugins/wp/LogicBuiltins.ml
index 23138d3e16679e8a7f7572beab592b6d09d78b4b..ebf416fae4f8b7285d672c25a4a8aba21d011837 100644
--- a/src/plugins/wp/LogicBuiltins.ml
+++ b/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
diff --git a/src/plugins/wp/LogicBuiltins.mli b/src/plugins/wp/LogicBuiltins.mli
index c4e8968dd46e252dcefd9fbb82527e60dd4f15fc..eb0c6d9045dd42be3f14bf07e440d8c4b3e1da23 100644
--- a/src/plugins/wp/LogicBuiltins.mli
+++ b/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 ->
diff --git a/src/plugins/wp/Vlist.ml b/src/plugins/wp/Vlist.ml
index 338ce8992abfb449129aa056505c2f8234dd4d50..40238be85bde3c5c429b26cdc1cad0fe961e7e26 100644
--- a/src/plugins/wp/Vlist.ml
+++ b/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"