Skip to content

Make old apply to the whole subexpression. #579

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
gebner merged 1 commit into from
Mar 2, 2026
+26 −20
Merged

Make old apply to the whole subexpression. #579

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
44 changes: 25 additions & 19 deletions src/checker/Pulse.Checker.ImpureSpec.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -92,7 +92,15 @@ let symb_eval_stateful_app (g: env) (ctxt: slprop) (t: term) : T.Tac R.term =
let rwr = RU.deep_compress rwr in // TODO: maybe this fails on uvars...
rwr

let rec symb_eval_subterms (g:env) (ctxt: ctxt) (t:R.term) : T.Tac (bool & R.term) =
noeq type ctxt' = {
ctxt: ctxt;
in_old: in_old:bool { in_old ==> Some? ctxt.ctxt_old };
}

let cur_ctxt c =
if c.in_old then Some?.v c.ctxt.ctxt_old else c.ctxt.ctxt_now

let rec symb_eval_subterms (g:env) (ctxt: ctxt') (t:R.term) : T.Tac (bool & R.term) =
match R.inspect_ln t with
| R.Tv_Abs b body ->
debug g (fun _ -> [text "symb eval subterms abs 0"; pp t]);
Expand Down Expand Up @@ -145,7 +153,7 @@ let rec symb_eval_subterms (g:env) (ctxt: ctxt) (t:R.term) : T.Tac (bool & R.ter
match is_stateful_application g t with
| Some _ ->
let t = RU.mk_app_flat head args (T.range_of_term t) in
let t' = symb_eval_stateful_app g ctxt.ctxt_now t in
let t' = symb_eval_stateful_app g (cur_ctxt ctxt) t in
true, t'
| None ->
if changed then
Expand All @@ -159,28 +167,23 @@ let rec symb_eval_subterms (g:env) (ctxt: ctxt) (t:R.term) : T.Tac (bool & R.ter
| R.Tv_FVar fv, [t, _] ->
if R.inspect_fv fv = old_lid then
// let t = RU.mk_app_flat head args (T.range_of_term t) in
match is_stateful_application g t, ctxt.ctxt_old with
| _, None ->
if not (Some? ctxt.ctxt.ctxt_old) then
T.fail_doc_at [
text "'old' can only be used in postconditions";
] r
| None, _ ->
T.fail_doc_at [
text "'old' needs to be applied to a stateful computation, not:";
pp t;
] r
| Some _, Some ctxt_old ->
let head, args = T.collect_app_ln t in
let g, changed, args = symb_eval_subterms_args g ctxt args in
let t = RU.mk_app_flat head args (T.range_of_term t) in
let t' = symb_eval_stateful_app g ctxt_old t in
true, t'
else (
(if ctxt.in_old then
warn_doc g r [
text "'old' only needs to be specified once";
]);
symb_eval_subterms g { ctxt with in_old = true } t
)
else
fallback ()
| _ ->
fallback ()

and symb_eval_subterms_args (g:env) (ctxt: ctxt) (args:list T.argv)
and symb_eval_subterms_args (g:env) (ctxt: ctxt') (args:list T.argv)
: T.Tac (env & bool & list T.argv)
= T.fold_right
(fun (arg, q) (g, changed, args) ->
Expand Down Expand Up @@ -219,7 +222,8 @@ let run_elim (g: env) (ctxt: slprop) : T.Tac (env & list nvar & slprop) =
g', xs, list_as_slprop ctxt

(* Adds add to the ctxt in a way that the prover will prefer it when ambiguous. *)
let push_ctxt ctxt add = { ctxt with ctxt_now = tm_star add ctxt.ctxt_now }
let push_ctxt (ctxt: ctxt') add =
{ ctxt with ctxt = { ctxt.ctxt with ctxt_now = tm_star add ctxt.ctxt.ctxt_now } }

let un_uinst (t: term) : R.term_view =
match R.inspect_ln t with
Expand Down Expand Up @@ -282,7 +286,7 @@ let tc_term_phase1_with_type_twice g t ty =
let or_emp (t: option slprop) : slprop =
match t with Some t -> t | None -> tm_emp

let rec purify_spec_core (g: env) (ctxt: ctxt) (ts: list slprop) : T.Tac (option slprop) =
let rec purify_spec_core (g: env) (ctxt: ctxt') (ts: list slprop) : T.Tac (option slprop) =
match ts with
| [] -> None
| t::ts ->
Expand Down Expand Up @@ -336,7 +340,7 @@ let rec purify_spec_core (g: env) (ctxt: ctxt) (ts: list slprop) : T.Tac (option
let t = T.norm_term_env (elab_env g) steps t in
extrude g ctxt [t] ts

and extrude (g: env) (ctxt: ctxt) (todo: list slprop) (ts: list slprop) : T.Tac (option slprop) =
and extrude (g: env) (ctxt: ctxt') (todo: list slprop) (ts: list slprop) : T.Tac (option slprop) =
match todo with
| [] -> purify_spec_core g ctxt ts
| t::todo ->
Expand Down Expand Up @@ -386,12 +390,14 @@ let run_elim_ctxt (g: env) (ctxt: ctxt) =

let purify_term (g: env) (ctxt: ctxt) (t: term) : T.Tac term =
let g', xs, ctxt = run_elim_ctxt g ctxt in
let ctxt = { ctxt; in_old = false } in
let _, t = symb_eval_subterms g ctxt t in
t

let purify_spec (g: env) (ctxt: ctxt) (t0: slprop) : T.Tac slprop =
let t = t0 in
let g', xs, ctxt = run_elim_ctxt g ctxt in
let ctxt = { ctxt; in_old = false } in
let t = purify_spec_core g' ctxt [t] |> or_emp in
// TODO: check that xs is not free in t
// If we call phase1 TC only once, then the universe instantiation in
Expand Down
2 changes: 1 addition & 1 deletion test/ImpureSpec.fst
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -102,7 +102,7 @@ fn test10 (x: bool)
fn test11 (x:ref (ref int))
preserves nested_live x
returns w:_
ensures pure (w == old(!(old(!x))))
ensures pure (w == old(! !x))
{
!(!x);
}
Expand Down
Loading