Commit c072e4c5 authored by Andrei Paskevich's avatar Andrei Paskevich

Mlw: do not include Bool in HighOrd

also, we believe that VCgen does not introduce new dependencies
on built-in theories, so no need to reapply add_use.
parent 8c8bb218
...@@ -822,7 +822,6 @@ let bool_theory = ...@@ -822,7 +822,6 @@ let bool_theory =
let highord_theory = let highord_theory =
let uc = empty_theory (id_fresh "HighOrd") ["why3";"HighOrd"] in let uc = empty_theory (id_fresh "HighOrd") ["why3";"HighOrd"] in
let uc = use_export uc bool_theory in
let uc = add_ty_decl uc ts_func in let uc = add_ty_decl uc ts_func in
let uc = add_param_decl uc fs_func_app in let uc = add_param_decl uc fs_func_app in
close_theory uc close_theory uc
...@@ -880,7 +879,7 @@ let () = Exn_printer.register ...@@ -880,7 +879,7 @@ let () = Exn_printer.register
| ClashSymbol s -> | ClashSymbol s ->
Format.fprintf fmt "Symbol %s is already defined in the current scope" s Format.fprintf fmt "Symbol %s is already defined in the current scope" s
| UnknownMeta s -> | UnknownMeta s ->
Format.fprintf fmt "Unknown metaproperty %s" s Format.fprintf fmt "Unknown meta-property %s" s
| KnownMeta m -> | KnownMeta m ->
Format.fprintf fmt "Metaproperty %s is already registered with \ Format.fprintf fmt "Metaproperty %s is already registered with \
a conflicting signature" m.meta_name a conflicting signature" m.meta_name
......
...@@ -480,7 +480,7 @@ let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with ...@@ -480,7 +480,7 @@ let pd_int, pd_real, pd_equ = match builtin_theory.th_decls with
| _ -> assert false | _ -> assert false
let pd_func, pd_func_app = match highord_theory.th_decls with let pd_func, pd_func_app = match highord_theory.th_decls with
| [{td_node = Use _bo}; {td_node = Decl df}; {td_node = Decl da}] -> | [{td_node = Decl df}; {td_node = Decl da}] ->
mk_decl (PDtype [mk_itd its_func [] [] []]) [df], mk_decl (PDtype [mk_itd its_func [] [] []]) [df],
mk_decl (PDlet ld_func_app) [da] mk_decl (PDlet ld_func_app) [da]
| _ -> assert false | _ -> assert false
......
...@@ -298,7 +298,6 @@ let bool_module = ...@@ -298,7 +298,6 @@ let bool_module =
let highord_module = let highord_module =
let uc = empty_module dummy_env (id_fresh "HighOrd") ["why3";"HighOrd"] in let uc = empty_module dummy_env (id_fresh "HighOrd") ["why3";"HighOrd"] in
let uc = use_export uc bool_module in
let uc = add_pdecl_no_logic uc pd_func in let uc = add_pdecl_no_logic uc pd_func in
let uc = add_pdecl_no_logic uc pd_func_app in let uc = add_pdecl_no_logic uc pd_func_app in
let m = close_module uc in let m = close_module uc in
...@@ -334,13 +333,11 @@ let add_use uc d = Sid.fold (fun id uc -> ...@@ -334,13 +333,11 @@ let add_use uc d = Sid.fold (fun id uc ->
let add_pdecl ~vc uc d = let add_pdecl ~vc uc d =
let uc = add_use uc d in let uc = add_use uc d in
let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in let dl = if vc then Vc.vc uc.muc_env uc.muc_known d else [] in
(* verification conditions might contain built-in symbols which (* verification conditions must not add additional dependencies
do not occur in the original declaration, so we call add_use. on built-in theories like TupleN or HighOrd. Also, we expect
However, we expect int.Int or any other library theory to int.Int or any other library theory to be in the context:
be in the context: importing them automatically seems to be importing them automatically seems to be too invasive. *)
too invasive for the namespace. *) add_pdecl (List.fold_left add_pdecl uc dl) d
let uc = List.fold_left (fun uc d -> add_pdecl (add_use uc d) d) uc dl in
add_pdecl uc d
(** {2 Cloning} *) (** {2 Cloning} *)
......
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