Skip to content
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.

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

Just delete a bunch of string_append pattern things #260

Merged
merged 1 commit into from
Oct 27, 2023

Conversation

Alasdair
Copy link
Collaborator

It's so broken, it's not worth even trying to fix. Right now it just generates invalid functions for otherwise functional mappings. Instead, turn any match arm

x ^ ... ^ y => <exp>

into

_ => exit()

String mappings have A) generated a special non-executable effect for a while and B) already don't actually work, so this shouldn't break anything in practice.

On this plus side, generated string append code represented the majority of generated OCaml for RISC-V, so this fixes the compilation time issues.

@Alasdair
Copy link
Collaborator Author

The only realistic (semi) backwards compatible way to make string append patterns work that I can see, without totally breaking existing code is to add type-level regular expressions, so you can have:

hex_bits : forall 'a. (int('n), regex("0x[0-9A-Fa-f]+")) <-> bits('n)

Fundamentally you have to be able to take a string and split it into a string append pattern like x ^ y ^ z without trying to rely on a bunch of broken heuristics and hacks like the previous implementation, which requires having some extra information like a regular expression to let you tokenise and split the string.

@Alasdair Alasdair force-pushed the delete_string_append branch from 292dfe9 to f52188a Compare May 24, 2023 15:54
@github-actions
Copy link

github-actions bot commented May 24, 2023

Test Results

       8 files  ±0       19 suites  ±0   0s ⏱️ ±0s
   550 tests ±0     550 ✔️ ±0  0 💤 ±0  0 ±0 
1 834 runs  ±0  1 833 ✔️ ±0  1 💤 ±0  0 ±0 

Results for commit 91946b0. ± Comparison against base commit e4f9665.

♻️ This comment has been updated with latest results.

It's so broken, it's not worth even trying to fix. Right now it just generates invalid
functions for otherwise functional mappings. Instead, turn any match arm

x ^ ... ^ y => <exp>

into

_ => exit()

String mappings have generated a special non-executable effect for a while, so this shouldn't
break anything in practice.

On this plus side, generated string append code represented the majority of generated OCaml
for RISC-V, so this fixes the compilation time issues
@Alasdair Alasdair force-pushed the delete_string_append branch from f52188a to 91946b0 Compare October 27, 2023 23:01
@Alasdair Alasdair merged commit f9db302 into rems-project:sail2 Oct 27, 2023
3 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant