Commit 3df85aba authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

put built-in theories and modules under the library path "why3"

In this way, we can always distinguish them from local theories and
modules. Both 'use Bool' and 'use why3.Bool' are accepted. No support
for use/clone of built-in modules is done yet, but so far we don't
needed (the only built-in module is why3.Prelude which is used by
default).

As of now, one cannot put a file "why3.why" at the root of loadpath,
since it will be inaccessible. Paths like why3/toto.why are still
admitted, but we will probably ban them too and reserve the whole
"why3.xxx.yyy" hierarchy for the built-in theories and modules.
parent c3357f54
......@@ -101,6 +101,7 @@ let check_qualifier s =
then raise (InvalidQualifier s)
let locate_lib_file env path exts =
if path = [] || path = ["why3"] then raise (LibFileNotFound path);
List.iter check_qualifier path;
let file = List.fold_left Filename.concat "" path in
let add_ext ext = file ^ "." ^ ext in
......@@ -172,7 +173,7 @@ let get_builtin s =
| None -> raise (TheoryNotFound ([],s))
let read_lib_theory lib path th =
if path = [] then get_builtin th else
if path = [] || path = ["why3"] then get_builtin th else
let _,mth = read_lib_file lib path in
try Mstr.find th mth with Not_found ->
raise (TheoryNotFound (path,th))
......
......@@ -766,7 +766,7 @@ let on_meta _meta fn acc theory =
(** Base theories *)
let builtin_theory =
let uc = empty_theory (id_fresh "BuiltIn") [] in
let uc = empty_theory (id_fresh "BuiltIn") ["why3"] in
let uc = add_ty_decl uc ts_int in
let uc = add_ty_decl uc ts_real in
let uc = add_param_decl uc ps_equ in
......@@ -776,12 +776,12 @@ let create_theory ?(path=[]) n =
use_export (empty_theory n path) builtin_theory
let bool_theory =
let uc = empty_theory (id_fresh "Bool") [] in
let uc = empty_theory (id_fresh "Bool") ["why3"] in
let uc = add_data_decl uc [ts_bool, [fs_bool_true,[]; fs_bool_false,[]]] in
close_theory uc
let highord_theory =
let uc = empty_theory (id_fresh "HighOrd") [] in
let uc = empty_theory (id_fresh "HighOrd") ["why3"] in
let uc = add_ty_decl uc ts_func in
let uc = add_ty_decl uc ts_pred in
let uc = add_param_decl uc fs_func_app in
......@@ -791,7 +791,7 @@ let highord_theory =
let tuple_theory = Hint.memo 17 (fun n ->
let ts = ts_tuple n and fs = fs_tuple n in
let pl = List.map (fun _ -> None) ts.ts_args in
let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) [] in
let uc = empty_theory (id_fresh ("Tuple" ^ string_of_int n)) ["why3"] in
let uc = add_data_decl uc [ts, [fs,pl]] in
close_theory uc)
......
......@@ -1913,14 +1913,7 @@ and merge_metas_aux ~keygen ~theories env to_goal _ from_metas =
read_theory ip formats
in
let read_theory ip =
if ip.ip_library = [] then
match ip.ip_theory with
(** Hack?? *)
| "BuiltIn" -> Theory.builtin_theory
| "Bool" -> Theory.bool_theory
(* | "Tuple"??? -> ... *)
(* | "Unit" -> ??? *)
| s -> Mstr.find s theories
if ip.ip_library = [] then Mstr.find ip.ip_theory theories
else read_theory ip ["why";"whyml"] in
let to_idpos_ts = Mts.fold_left (fun idpos_ts from_ts ip ->
......
......@@ -361,7 +361,7 @@ let add_invariant uc its p =
let th_unit =
let ts = create_tysymbol (id_fresh "unit") [] (Some ty_unit) in
let uc = create_theory (id_fresh "Unit") in
let uc = create_theory ~path:["why3"] (id_fresh "Unit") in
let uc = Theory.use_export uc (tuple_theory 0) in
let uc = Theory.add_ty_decl uc ts in
close_theory uc
......@@ -371,7 +371,7 @@ let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit
let mod_prelude env =
let pd_exit = create_exn_decl xs_exit in
let pd_old = create_val_decl (LetV Mlw_wp.pv_old) in
let uc = empty_module env (id_fresh "Prelude") [] in
let uc = empty_module env (id_fresh "Prelude") ["why3"] in
let uc = add_pdecl ~wp:false uc pd_old in
let uc = add_pdecl ~wp:false uc pd_exit in
close_module uc
......
......@@ -1851,7 +1851,7 @@ let find_theory loc lib path s =
in
(* search also in .why files, unless the theory is built-in *)
let th =
if path = [] then None else
if path = [] || path = ["why3"] then None else
try Some (Env.find_theory (Env.env_of_library lib) path s)
with LibFileNotFound _ | TheoryNotFound _ -> None
in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment