Commit 5fe2e452 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Do not keep the declaration for "%old".

This removes the need for exporting the theory about marks and thus the
resulting noise in the produced tasks. The patch is large due to the
dependencies between files.
parent 218e736a
......@@ -39,10 +39,17 @@ and pdecl_node =
let pd_equal : pdecl -> pdecl -> bool = (==)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let ity_mark = ity_pur ts_mark []
let pv_old = create_pvsymbol ~ghost:true (id_fresh "%old") ity_mark
let mk_decl =
let r = ref 0 in
fun node syms news ->
incr r;
let syms = Sid.remove pv_old.pv_vs.vs_name syms in
{ pd_node = node; pd_syms = syms; pd_news = news; pd_tag = !r; }
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s
......
......@@ -41,6 +41,13 @@ and pdecl_node = private
| PDrec of fun_defn list
| PDexn of xsymbol
(** {2 Marks} *)
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val ity_mark : ity
val pv_old : pvsymbol
(** {2 Declaration constructors} *)
type pre_field = preid option * field
......
......@@ -937,7 +937,7 @@ let check_user_effect ?ps e spec args dsp =
Loc.errorm ?loc:(e_find_loc (fun e -> has_write reg e.e_effect) e)
"this@ expression@ produces@ an@ unlisted@ write@ effect" in
if dsp.ds_checkrw then begin
let reads = Spv.remove Mlw_wp.pv_old e.e_syms.syms_pv in
let reads = Spv.remove Mlw_decl.pv_old e.e_syms.syms_pv in
let reads = Spv.diff reads (spec_pvset Spv.empty spec) in
Spv.iter check_read (Spv.diff reads args);
Sreg.iter check_write eeff.eff_writes;
......
......@@ -1346,7 +1346,7 @@ let eval_global_expr env mkm tkm _writes e =
let add_glob _ d ((venv,renv) as acc) =
match d.Mlw_decl.pd_node with
| Mlw_decl.PDval (Mlw_expr.LetV pvs)
when not (pv_equal pvs Mlw_wp.pv_old) ->
when not (pv_equal pvs Mlw_decl.pv_old) ->
let ity = pvs.pv_ity in
let v = any_value_of_type env (ty_of_ity ity) in
let renv,v = to_program_value env renv (VTvalue ity) v in
......
......@@ -400,10 +400,7 @@ let xs_exit = create_xsymbol (id_fresh "%Exit") ity_unit
let mod_prelude =
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 None (id_fresh "Prelude") ["why3";"Prelude"] in
let uc = use_export_theory uc Mlw_wp.mark_theory in
let uc = add_pdecl ~wp:false uc pd_old in
let uc = add_pdecl ~wp:false uc pd_exit in
close_module uc
......@@ -536,7 +533,7 @@ let clone_export uc m minst inst =
| VTarrow a -> VTarrow (conv_aty mv a)
| VTvalue v -> VTvalue (conv_ity v) in
vty_arrow args ~spec vty in
let mvs = ref (Mvs.singleton Mlw_wp.pv_old.pv_vs Mlw_wp.pv_old.pv_vs) in
let mvs = ref (Mvs.singleton pv_old.pv_vs pv_old.pv_vs) in
let add_pdecl uc d = { uc with
muc_decls = d :: uc.muc_decls;
muc_known = known_add_decl (Theory.get_known nth) uc.muc_known d;
......
......@@ -447,8 +447,6 @@ module Translate = struct
| None -> ML.Tapp (ts.ts_name, List.map (ity info) tl)
end
let ity_mark = ity_pur Mlw_wp.ts_mark []
let is_underscore pv =
pv.pv_vs.vs_name.id_string = "_" && ity_equal pv.pv_ity ity_unit
......@@ -631,7 +629,7 @@ module Translate = struct
let pdecl info pd =
match pd.pd_node with
| PDval (LetV pv) when pv_equal pv Mlw_wp.pv_old ->
| PDval (LetV pv) when pv_equal pv Mlw_decl.pv_old ->
[]
| PDval _ ->
[]
......
......@@ -18,6 +18,7 @@ open Theory
open Mlw_ty
open Mlw_ty.T
open Mlw_expr
open Mlw_decl
let debug = Debug.register_info_flag "whyml_wp"
~desc:"Print@ details@ of@ verification@ conditions@ generation."
......@@ -32,11 +33,6 @@ let lemma_label = Ident.create_label "why3:lemma"
(** Marks *)
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let ity_mark = ity_pur ts_mark []
let fresh_mark () = create_vsymbol (id_fresh "'mark") ty_mark
let fs_at =
......@@ -70,7 +66,6 @@ let e_now = e_ghost (e_lapp fs_now [] (ity_pur ts_mark []))
(* [vs_old] appears in the postconditions given to the core API,
which expects every vsymbol to be a pure part of a pvsymbol *)
let pv_old = create_pvsymbol ~ghost:true (id_fresh "%old") ity_mark
let vs_old = pv_old.pv_vs
let t_old = t_var vs_old
......
......@@ -12,7 +12,6 @@
(** {1 Weakest preconditions} *)
open Theory
open Mlw_ty
open Mlw_ty.T
open Mlw_decl
open Mlw_expr
......@@ -21,9 +20,6 @@ open Mlw_expr
val lemma_label : Ident.label
val ts_mark : Ty.tysymbol
val ty_mark : Ty.ty
val fs_at : Term.lsymbol
val fs_old : Term.lsymbol
......@@ -36,7 +32,6 @@ val th_mark_old : Theory.theory
val fs_now : Term.lsymbol
val e_now : expr
val pv_old : pvsymbol
val remove_old : Term.term -> Term.term
val full_invariant :
......
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