Skip to content

feat(unroll-for): propagate constants after unrolling #909

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
strub merged 1 commit into from
Feb 20, 2026
+20 −14
Merged

feat(unroll-for): propagate constants after unrolling #909

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
7 changes: 5 additions & 2 deletions src/ecParser.mly
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3019,8 +3019,11 @@ interleave_info:
| FUSION s=side? o=codepos NOT i=word AT d1=word COMMA d2=word
{ Pfusion (s, o, (i, (d1, d2))) }

| UNROLL b=boption(FOR) s=side? o=codepos
{ Punroll (s, o, b) }
| UNROLL s=side? o=codepos
{ Punroll (s, o, `While) }

| UNROLL FOR b=boption(STAR) s=side? o=codepos
{ Punroll (s, o, `For (not b)) }

| SPLITWHILE s=side? o=codepos COLON c=expr %prec prec_tactic
{ Psplitwhile (c, s, o) }
Expand Down
2 changes: 1 addition & 1 deletion src/ecParsetree.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -731,7 +731,7 @@ type phltactic =
| Pasyncwhile of async_while_info
| Pfission of (oside * pcodepos * (int * (int * int)))
| Pfusion of (oside * pcodepos * (int * (int * int)))
| Punroll of (oside * pcodepos * bool)
| Punroll of (oside * pcodepos * [`While | `For of bool])
| Psplitwhile of (pexpr * oside * pcodepos)
| Pcall of oside * call_info gppterm
| Pcallconcave of (pformula * call_info gppterm)
Expand Down
21 changes: 12 additions & 9 deletions src/phl/ecPhlLoopTx.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module TTC = EcProofTyping
(* -------------------------------------------------------------------- *)
type fission_t = oside * pcodepos * (int * (int * int))
type fusion_t = oside * pcodepos * (int * (int * int))
type unroll_t = oside * pcodepos * bool
type unroll_t = oside * pcodepos * [`While | `For of bool]
type splitwhile_t = pexpr * oside * pcodepos

(* -------------------------------------------------------------------- *)
Expand Down Expand Up @@ -220,7 +220,7 @@ let process_splitwhile (b, side, cpos) tc =
t_splitwhile b side cpos tc

(* -------------------------------------------------------------------- *)
let process_unroll_for side cpos tc =
let process_unroll_for ~cfold side cpos tc =
let env = FApi.tc1_env tc in
let hyps = FApi.tc1_hyps tc in
let (goal_m, _), c = EcLowPhlGoal.tc1_get_stmt side tc in
Expand Down Expand Up @@ -327,16 +327,19 @@ let process_unroll_for side cpos tc =
let tcenv = t_doit 0 pos zs tc in
let tcenv = FApi.t_onalli doi tcenv in

let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
let clen = blen * (List.length zs - 1) in
if cfold then begin
let cpos = EcMatching.Position.shift ~offset:(-1) cpos in
let clen = blen * (List.length zs - 1) in

FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
FApi.t_last (EcPhlCodeTx.t_cfold side cpos (Some clen)) tcenv
end else tcenv

(* -------------------------------------------------------------------- *)
let process_unroll (side, cpos, for_) tc =
if for_ then
process_unroll_for side cpos tc
else begin
match for_ with
| `While ->
let cpos = EcLowPhlGoal.tc1_process_codepos tc (side, cpos) in
t_unroll side cpos tc
end

| `For cfold ->
process_unroll_for ~cfold side cpos tc
4 changes: 2 additions & 2 deletions src/phl/ecPhlLoopTx.mli
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,10 +13,10 @@ val t_splitwhile : expr -> oside -> codepos -> backward
(* -------------------------------------------------------------------- *)
type fission_t = oside * pcodepos * (int * (int * int))
type fusion_t = oside * pcodepos * (int * (int * int))
type unroll_t = oside * pcodepos * bool
type unroll_t = oside * pcodepos * [`While | `For of bool]
type splitwhile_t = pexpr * oside * pcodepos

val process_unroll_for : oside -> pcodepos -> backward
val process_unroll_for : cfold:bool -> oside -> pcodepos -> backward
val process_fission : fission_t -> backward
val process_fusion : fusion_t -> backward
val process_unroll : unroll_t -> backward
Expand Down