Skip to content

New tactic to alias a subexpression of an instruction #647

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

Jump to bottom
Merged
strub merged 1 commit into from
Oct 29, 2024
Merged

New tactic to alias a subexpression of an instruction #647

strub merged 1 commit into from
Oct 29, 2024

Conversation

@strub
Copy link
Member

@strub strub commented Oct 14, 2024

No description provided.

@strub strub force-pushed the alias-subexpr-in-proc branch 2 times, most recently from 6e91947 to 98cb033 Compare October 15, 2024 05:57
@strub strub marked this pull request as ready for review October 15, 2024 05:57
@strub strub changed the title New tactic command to alias a subexpression as a program variable New tactic to alias a subexpression of an instruction Oct 15, 2024
@strub strub requested review from bgregoir and fdupress October 15, 2024 06:03
@fdupress
Copy link
Member

fdupress commented Oct 15, 2024 •
edited
Loading

This looks useful. The implementation seems to use a different meaning to the codepos parameter than the standard alias.

The standard alias takes a line number to insert a new line at. This variant uses the line number to match an expression in.

Perhaps a syntax like alias codepos vname := pattern at codepos would allow both selecting the line where the new variable initialisation is inserted (consistently with alias) and the line in which to match?

@strub
Copy link
Member Author

strub commented Oct 15, 2024 •
edited
Loading

What you propose is harder because you have to verify that there is no modification of the program variables of the aliased expression. Your variant could be done outside of the TCB as alias + move.

@fdupress
Copy link
Member

fdupress commented Oct 15, 2024

Sure, but my comment was more on the inconsistent interpretation of the same tactic prefix between two variants. I'm happy if the new tactic is alias var := pattern at/in codepos.

@strub strub force-pushed the alias-subexpr-in-proc branch from 98cb033 to 37659d1 Compare October 15, 2024 08:56
@strub
Copy link
Member Author

strub commented Oct 15, 2024

I updated the syntax

@strub
Alias sub-expressions in statements
f9a0b7f 
The tactic `alias $name := $pattern @ $pos` alias the $pattern (subject
to matching) in the instruction targetted by $pos using a fresh
program variable $name.

The tactic does not apply to the expression contained in the
condition of a while loop.
@strub strub force-pushed the alias-subexpr-in-proc branch from 37659d1 to f9a0b7f Compare October 29, 2024 12:47
@strub strub enabled auto-merge (rebase) October 29, 2024 12:52
@strub strub merged commit ad2615b into main Oct 29, 2024
15 checks passed
@strub strub deleted the alias-subexpr-in-proc branch October 29, 2024 13:10
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fdupress fdupress fdupress approved these changes

@bgregoir bgregoir Awaiting requested review from bgregoir

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@strub @fdupress