Skip to content

Eager: match on last statement and use EqTest #900

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

Open
Cameron-Low wants to merge 1 commit into
base: main
Choose a base branch
from
+3 −3
Open

Eager: match on last statement and use EqTest #900

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
6 changes: 3 additions & 3 deletions src/phl/ecPhlEager.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ let destruct_on_op id_op tc =
let env = FApi.tc1_env tc and es = tc1_as_equivS tc in
let s =
try
let s, _ = split_at_cpos1 env (-1, `ByMatch (None, id_op)) es.es_sl
let s, _ = split_at_cpos1 env (-1, `ByMatch (Some (-1), id_op)) es.es_sl
(* ensure the right statement also contains an [id_op]: *)
and _, _ = split_at_cpos1 env (1, `ByMatch (None, id_op)) es.es_sr in
s
Expand Down Expand Up @@ -237,7 +237,7 @@ let t_eager_while_r i tc =
subst_expr (add_memory empty mr ml)
in

if (not (e_equal e (sub_to_left_mem _e))) then
if (not (ER.EqTest.for_expr env e (sub_to_left_mem _e))) then
tc_error !!tc "eager: both while guards must be syntactically equal";

let eqMem1 = eq_on_form_and_stmt env i c' and eqI = eq_on_sided_form env i in
Expand Down Expand Up @@ -317,7 +317,7 @@ let t_eager_fun_def_r tc =
let t_eager_fun_abs_r i tc =
let env, _, _ = FApi.tc1_eflat tc and eg = tc1_as_eagerF tc in

if not (s_equal eg.eg_sl eg.eg_sr) then
if not (ER.EqTest.for_stmt env eg.eg_sl eg.eg_sr) then
tc_error !!tc "eager: both swapping statements must be identical";

if not (ensure_eq_shape tc i.ml i.mr i.inv) then
Expand Down