Commit ed3ae39a authored by Andrei Paskevich's avatar Andrei Paskevich

optimize old_mark and erase_mark

parent 2a47e428
......@@ -170,7 +170,7 @@ let ts_unit = create_tysymbol (id_fresh "unit") [] (Some ty_unit)
(* logic ignore 'a : () *)
let ts_mark = create_tysymbol (id_fresh "mark") [] None
let ts_mark = create_tysymbol (id_fresh "'mark") [] None
let ty_mark = ty_app ts_mark []
let fs_at =
......@@ -181,6 +181,9 @@ let fs_old =
let ty = ty_var (create_tvsymbol (id_fresh "a")) in
create_lsymbol (id_fresh "old") [ty] (Some ty)
let vs_old = create_vsymbol (id_fresh "'old") ty_mark
let vs_now = create_vsymbol (id_fresh "'now") ty_mark
let th_prelude =
let uc = create_theory (id_fresh "Prelude") in
let uc = use_export uc (tuple_theory 0) in
......
......@@ -95,6 +95,9 @@ val ty_unit : ty
val fs_old : lsymbol
val fs_at : lsymbol
val vs_old : vsymbol
val vs_now : vsymbol
val th_prelude : theory
(** exceptions *)
......
......@@ -420,6 +420,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
with Not_found ->
errorm ~loc "unbound symbol %a" print_qualid p
in
(*if ls_equal ls fs_at then errorm ~loc "at not allowed in programs";*)
if ls_equal ls fs_old then errorm ~loc "old not allowed in programs";
let ps = get_psymbol ls in
begin match ps.ps_kind with
......@@ -913,7 +914,9 @@ let post env ((ty, f), ql) =
let iterm env l =
let t = dterm (pure_uc env.i_uc) env.i_denv l in
Denv.term env.i_pures t
let t = Denv.term env.i_pures t in
check_at_fmla l.pp_loc t;
t
(* FIXME: ensure that symbol comes from theory int.Int *)
let find_int_ls ~loc env s =
......@@ -940,12 +943,18 @@ let ivariant env (t, ps) =
| _ ->
assert false
let ifmla ?old env l =
let loc = l.pp_loc in
(* replace every occurrence of [old(t)] with [at(t,'old)] *)
let rec remove_old f = match f.t_node with
| Term.Tapp (ls, [t]) when ls_equal ls fs_old ->
t_app fs_at [remove_old t; t_var vs_old] f.t_ty
| _ ->
t_map remove_old f
let ifmla ?(old=false) env l =
let f = dfmla (pure_uc env.i_uc) env.i_denv l in
let f = Denv.fmla env.i_pures f in
check_at_fmla ?old loc f;
f
check_at_fmla ~old l.pp_loc f;
if (old = true) then remove_old f else f
let id_result loc = id_user id_result loc
......
......@@ -117,30 +117,27 @@ let add_binder x rm =
let add_binders = List.fold_right add_binder
(* replace old(t) with at(t,lab) everywhere in formula f *)
let rec old_mark lab t = match t.t_node with
| Tapp (ls, [t]) when ls_equal ls fs_old ->
let t = old_mark lab t in (* NECESSARY? *)
t_app fs_at [t; t_var lab] t.t_ty
| _ ->
t_map (old_mark lab) t
(* replace [at(t,'old)] with [at(t,lab)] everywhere in formula [f] *)
let old_mark lab t = t_subst_single vs_old (t_var lab) t
(* replace at(t,lab) with t everywhere in formula f *)
let rec erase_mark lab t = match t.t_node with
| Tapp (ls, [t; {t_node = Tvar l}])
when ls_equal ls fs_at && vs_equal l lab ->
erase_mark lab t
| _ ->
t_map (erase_mark lab) t
(* replace [at(t,lab)] with [at(t,'now)] everywhere in formula [f] *)
let erase_mark lab t = t_subst_single lab (t_var vs_now) t
let rec unref s t = match t.t_node with
| Tvar vs ->
begin try t_var (Mvs.find vs s) with Not_found -> t end
| Tapp (ls, _) when ls_equal ls fs_old ->
assert false
| Tapp (ls, _) when ls_equal ls fs_at ->
| Tapp (ls, [e;{t_node = Tvar lab}]) when ls_equal ls fs_at ->
if vs_equal lab vs_old then assert false else
if vs_equal lab vs_now then unref s e else
(* do not recurse in at(...) *)
t
| Tlet _ | Tcase _ | Teps _ | Tquant _ ->
(* do not open unless necessary *)
let s = Mvs.set_inter s t.t_vars in
if Mvs.is_empty s then t else
t_map (unref s) t
| _ ->
t_map (unref s) t
......@@ -683,12 +680,20 @@ let bool_to_prop env f =
in
f_btop f
(* replace every occurrence of [at(t,'now)] with [t] *)
let rec remove_at f = match f.t_node with
| Tapp (ls, [t;{t_node = Tvar lab}])
when ls_equal ls fs_at && vs_equal lab vs_now ->
remove_at t
| _ ->
t_map remove_at f
let add_wp_decl ps f uc =
let name = ps.ps_pure.ls_name in
let s = "WP_" ^ name.id_string in
let label = ["expl:" ^ name.id_string] in
let id = id_fresh ~label ?loc:name.id_loc s in
let f = bool_to_prop uc f in
let f = bool_to_prop uc (remove_at f) in
let km = get_known (pure_uc uc) in
let f = eval_match ~inline:inline_nonrec_linear km f in
(* printf "wp: f=%a@." print_term f; *)
......
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