Commit 6563fac9 authored by Guillaume Melquiond's avatar Guillaume Melquiond

Rename Stdlib into Wstdlib (fix issue #105).

OCaml 4.07 introduces a new standard module named Stdlib, which clashes
with the one from Why3 (during the compilation of Why3).
parent 4d07e5a8
......@@ -165,7 +165,7 @@ LIBGENERATED = src/util/config.ml \
LIB_UTIL = config bigInt util opt lists strings \
extmap extset exthtbl weakhtbl \
hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
hashcons wstdlib exn_printer pp json debug loc lexlib print_tree \
cmdline warning sysutil rc plugin bigInt number pqueue
LIB_CORE = ident ty term pattern decl theory \
......@@ -1759,7 +1759,7 @@ endif
MODULESTODOC = \
util/util util/opt util/lists util/strings \
util/extmap util/extset util/exthtbl \
util/weakhtbl util/stdlib util/rc util/debug \
util/weakhtbl util/wstdlib util/rc util/debug \
core/ident core/ty core/term core/decl core/theory \
core/env core/task \
driver/whyconf driver/call_provers driver/driver \
......
......@@ -20,7 +20,7 @@
open Format
open Why3
open Stdlib
open Wstdlib
open Whyconf
open Theory
open Task
......
......@@ -34,7 +34,7 @@
{
open Why3
open Stdlib
open Wstdlib
type vars = Term.term array
let get_indice i =
......
......@@ -45,7 +45,7 @@ open Why3
open Theory
open Term
open Stdlib
open Wstdlib
open Ident
......
......@@ -13,7 +13,7 @@ open Why3
open Mlw_module
open Py_ast
open Ptree
open Stdlib
open Wstdlib
let debug = Debug.register_flag "python"
~desc:"mini-python plugin debug flag"
......
......@@ -13,7 +13,7 @@ open Format
open Tptp_ast
open Why3
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -10,5 +10,5 @@
(********************************************************************)
val typecheck : Why3.Env.env -> Why3.Env.pathname ->
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Stdlib.Mstr.t
Tptp_ast.tptp_file -> Why3.Theory.theory Why3.Wstdlib.Mstr.t
......@@ -837,11 +837,11 @@ and decompose_definition dep env evd c =
| Some b ->
let tvs = List.fold_left Ty.ty_freevars Stv.empty
(Ty.oty_cons ls.ls_args ls.ls_value) in
let add tv tvm = Stdlib.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Stdlib.Mstr.empty in
let add tv tvm = Wstdlib.Mstr.add tv.tv_name.Ident.id_string tv tvm in
let tvm = Stv.fold add tvs Wstdlib.Mstr.empty in
let ty = type_of_global env r in
let (_, vars), env, _ = decomp_type_quantifiers env evd ty in
let conv tv = Stdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
let conv tv = Wstdlib.Mstr.find tv.tv_name.Ident.id_string tvm in
let vars = List.map conv vars in
let tvm, env, b = decomp_type_lambdas Idmap.empty env evd vars (of_constr b) in
let (bv, vsl), env, b =
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Library environment *)
......
......@@ -11,7 +11,7 @@
(** {1 Environments} *)
open Stdlib
open Wstdlib
(** Local type aliases *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Labels *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Format
open Term
open Ident
......@@ -79,22 +79,22 @@ let array_add_element ~array ~index ~value =
let convert_float_value f =
match f with
| Plus_infinity ->
let m = Mstr.add "cons" (Json.String "Plus_infinity") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Plus_infinity") Wstdlib.Mstr.empty in
Json.Record m
| Minus_infinity ->
let m = Mstr.add "cons" (Json.String "Minus_infinity") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Minus_infinity") Wstdlib.Mstr.empty in
Json.Record m
| Plus_zero ->
let m = Mstr.add "cons" (Json.String "Plus_zero") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Plus_zero") Wstdlib.Mstr.empty in
Json.Record m
| Minus_zero ->
let m = Mstr.add "cons" (Json.String "Minus_zero") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Minus_zero") Wstdlib.Mstr.empty in
Json.Record m
| Not_a_number ->
let m = Mstr.add "cons" (Json.String "Not_a_number") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Not_a_number") Wstdlib.Mstr.empty in
Json.Record m
| Float_value (b, eb, sb) ->
let m = Mstr.add "cons" (Json.String "Float_value") Stdlib.Mstr.empty in
let m = Mstr.add "cons" (Json.String "Float_value") Wstdlib.Mstr.empty in
let m = Mstr.add "sign" (Json.String b) m in
let m = Mstr.add "exponent" (Json.String eb) m in
let m = Mstr.add "significand" (Json.String sb) m in
......@@ -103,32 +103,32 @@ let convert_float_value f =
let rec convert_model_value value : Json.json =
match value with
| Integer s ->
let m = Mstr.add "type" (Json.String "Integer") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Integer") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String s) m in
Json.Record m
| Float f ->
let m = Mstr.add "type" (Json.String "Float") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Float") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (convert_float_value f) m in
Json.Record m
| Decimal (int_part, fract_part) ->
let m = Mstr.add "type" (Json.String "Decimal") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Decimal") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String (int_part^"."^fract_part)) m in
Json.Record m
| Unparsed s ->
let m = Mstr.add "type" (Json.String "Unparsed") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Unparsed") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String s) m in
Json.Record m
| Bitvector v ->
let m = Mstr.add "type" (Json.String "Bv") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Bv") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.String v) m in
Json.Record m
| Boolean b ->
let m = Mstr.add "type" (Json.String "Boolean") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Boolean") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.Bool b) m in
Json.Record m
| Array a ->
let l = convert_array a in
let m = Mstr.add "type" (Json.String "Array") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Array") Wstdlib.Mstr.empty in
let m = Mstr.add "val" (Json.List l) m in
Json.Record m
| Record r ->
......@@ -136,22 +136,22 @@ let rec convert_model_value value : Json.json =
and convert_array a =
let m_others =
Mstr.add "others" (convert_model_value a.arr_others) Stdlib.Mstr.empty in
Mstr.add "others" (convert_model_value a.arr_others) Wstdlib.Mstr.empty in
convert_indices a.arr_indices @ [Json.Record m_others]
and convert_indices indices =
match indices with
| [] -> []
| index :: tail ->
let m = Mstr.add "indice" (Json.String index.arr_index_key) Stdlib.Mstr.empty in
let m = Mstr.add "indice" (Json.String index.arr_index_key) Wstdlib.Mstr.empty in
let m = Mstr.add "value" (convert_model_value index.arr_index_value) m in
Json.Record m :: convert_indices tail
and convert_record r =
let m = Mstr.add "type" (Json.String "Record") Stdlib.Mstr.empty in
let m = Mstr.add "type" (Json.String "Record") Wstdlib.Mstr.empty in
let fields = convert_fields r.fields in
let discrs = convert_discrs r.discrs in
let m_field_discr = Mstr.add "Field" fields Stdlib.Mstr.empty in
let m_field_discr = Mstr.add "Field" fields Wstdlib.Mstr.empty in
let m_field_discr = Mstr.add "Discr" discrs m_field_discr in
let m = Mstr.add "val" (Json.Record m_field_discr) m in
Json.Record m
......@@ -237,8 +237,8 @@ let print_location fmt m_element =
** Model definitions
***************************************************************
*)
module IntMap = Stdlib.Mint
module StringMap = Stdlib.Mstr
module IntMap = Wstdlib.Mint
module StringMap = Wstdlib.Mstr
type model_file = model_element list IntMap.t
type model_files = model_file StringMap.t
......
......@@ -11,7 +11,7 @@
open Format
open Pp
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -12,7 +12,7 @@
open Format
open Pp
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......@@ -31,7 +31,7 @@ type 'a pp = Pp.formatter -> 'a -> unit
type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
queried_terms : Term.term Stdlib.Mstr.t;
queried_terms : Term.term Wstdlib.Mstr.t;
}
type printer_args = {
......@@ -54,7 +54,7 @@ exception UnknownPrinter of string
let get_default_printer_mapping = {
lsymbol_m = (function _ -> raise Not_found);
vc_term_loc = None;
queried_terms = Stdlib.Mstr.empty;
queried_terms = Wstdlib.Mstr.empty;
}
let register_printer ~desc s p =
......@@ -224,9 +224,9 @@ let get_type_arguments t = match t.t_node with
let m = oty_match Mtv.empty ls.ls_value t.t_ty in
let m = List.fold_left2
(fun m ty t -> oty_match m (Some ty) t.t_ty) m ls.ls_args tl in
let name tv = Stdlib.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Stdlib.Mstr.empty in
Array.of_list (Stdlib.Mstr.values m)
let name tv = Wstdlib.Mstr.add tv.tv_name.id_string in
let m = Mtv.fold name m Wstdlib.Mstr.empty in
Array.of_list (Wstdlib.Mstr.values m)
| _ ->
[||]
......
......@@ -30,7 +30,7 @@ type printer_mapping = {
lsymbol_m : string -> Term.lsymbol;
vc_term_loc : Loc.position option;
(* The position of the term that triggers the VC *)
queried_terms : Term.term Stdlib.Mstr.t;
queried_terms : Term.term Wstdlib.Mstr.t;
(* The list of terms that were queried for the counter-example
by the printer *)
}
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
......
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
(** Theories and Namespaces *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ty
open Term
open Decl
......
......@@ -14,7 +14,7 @@ open Term
open Decl
open Theory
open Task
open Stdlib
open Wstdlib
(** Task transformation *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
(** Types *)
......@@ -18,7 +18,7 @@ type tvsymbol = {
tv_name : ident;
}
module Tvar = Stdlib.MakeMSHW (struct
module Tvar = Wstdlib.MakeMSHW (struct
type t = tvsymbol
let tag tv = tv.tv_name.id_tag
end)
......@@ -63,7 +63,7 @@ and ty_node =
| Tyvar of tvsymbol
| Tyapp of tysymbol * ty list
module Tsym = Stdlib.MakeMSHW (struct
module Tsym = Wstdlib.MakeMSHW (struct
type t = tysymbol
let tag ts = ts.ts_name.id_tag
end)
......
......@@ -40,7 +40,7 @@ The regexp must start with ^.
*)
open Format
open Stdlib
open Wstdlib
open Whyconf
module Wc = Whyconf
open Rc
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Smt2_model_defs
open Strings
......
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Stdlib
open Wstdlib
open Ident
open Term
open Decl
......
......@@ -40,12 +40,12 @@ let do_parsing model =
Warning.emit
~loc:(get_position lexbuf)
"Error@ during@ lexing@ of@ smtlib@ model:@ unexpected character";
Stdlib.Mstr.empty
Wstdlib.Mstr.empty
| Parse_smtv2_model_parser.Error ->
begin
let loc = get_position lexbuf in
Warning.emit ~loc:loc "Error@ during@ parsing@ of@ smtlib@ model";
Stdlib.Mstr.empty
Wstdlib.Mstr.empty
end
let do_parsing model =
......
......@@ -52,11 +52,11 @@
output:
| EOF { Stdlib.Mstr.empty }
| EOF { Wstdlib.Mstr.empty }
| LPAREN ps MODEL ps list_decls RPAREN { $5 }
list_decls:
| LPAREN decl RPAREN ps { Smt2_model_defs.add_element $2 Stdlib.Mstr.empty false}
| LPAREN decl RPAREN ps { Smt2_model_defs.add_element $2 Wstdlib.Mstr.empty false}
| LPAREN decl RPAREN ps list_decls { Smt2_model_defs.add_element $2 $5 false }
| COMMENT ps list_decls { $3 } (* Lines beginning with ';' are ignored *)
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
type variable = string
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
type variable = string
......
......@@ -10,7 +10,7 @@
(********************************************************************)
open Format
open Stdlib
open Wstdlib
open Rc
(* magicnumber for the configuration :
......
......@@ -11,7 +11,7 @@
(** Managing the configuration of Why3 *)
open Stdlib
open Wstdlib
(** {2 General configuration} *)
......
......@@ -15,7 +15,7 @@ open Format
open Why3
open Whyconf
open Gconfig
open Stdlib
open Wstdlib
open Debug
module C = Whyconf
......
......@@ -138,7 +138,7 @@ let ref_modules, ref_theories =
Self.fatal "Exception raised while loading ref module:@ %a"
Exn_printer.exn_printer e
let ref_module : Mlw_module.modul = Stdlib.Mstr.find "Ref" ref_modules
let ref_module : Mlw_module.modul = Wstdlib.Mstr.find "Ref" ref_modules
*)
let ref_module : Mlw_module.modul =
Mlw_module.read_module env ["ref"] "Ref"
......@@ -169,7 +169,7 @@ let mach_int_modules, _mach_int_theories =
let int32_module : Mlw_module.modul =
try
Self.result "Looking up module mach.int.Int32";
Stdlib.Mstr.find "Int32" mach_int_modules
Wstdlib.Mstr.find "Int32" mach_int_modules
with Not_found ->
Self.fatal "Module mach.int.Int32 not found"
*)
......@@ -215,7 +215,7 @@ let uint32ofint_fun : Mlw_expr.psymbol = find_ps uint32_module "int_check"
let int64_module : Mlw_module.modul =
try
Self.result "Looking up module mach.int.Int64";
Stdlib.Mstr.find "Int64" mach_int_modules
Wstdlib.Mstr.find "Int64" mach_int_modules
with Not_found ->
Self.fatal "Module mach.int.Int64 not found"
*)
......@@ -245,7 +245,7 @@ let int64ofint_fun : Mlw_expr.psymbol = find_ps int64_module "of_int"
let array_modules, array_theories =
Env.read_lib_file (Mlw_main.library_of_env env) ["array"]
let array_module : Mlw_module.modul = Stdlib.Mstr.find "Array" array_modules
let array_module : Mlw_module.modul = Wstdlib.Mstr.find "Array" array_modules
*)
(*
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Term
open Ity
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ty
open Term
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Theory
open Ity
......
......@@ -9,7 +9,7 @@
(* *)
(********************************************************************)
open Stdlib
open Wstdlib
open Ident
open Ptree
open Ty
......
......@@ -11,7 +11,7 @@
(** Typing environments *)
open Stdlib
open Wstdlib
open Term
open Theory
......
......@@ -388,9 +388,9 @@ let print_info_model cntexample info =
S.fold (fun f acc ->
fprintf str_formatter "%a" (print_fmla info) f;