cryspen/hax

`while let .. = .. {}`

Offen

#113 geöffnet am 02.06.2023

 (1 Kommentar) (0 Reaktionen) (0 zugewiesene Personen)OCaml (61 Forks)auto 404
enginegood first issuehelp wantedkeep-openunsupported-rust

Repository-Metriken

Stars
 (456 Sterne)
PR-Merge-Metriken
 (Durchschn. Merge 4T 22h) (42 gemergte PRs in 30 T)

Beschreibung

Early in the pipeline, the Rust compiler expands every kind of loops (while, while let, for) as plain loops. Thus, what we see in the engine are only loops.

Loops in the AST of hax are designed to be flexible: either we deal with plain loops, or with specific loop kinds. ASTs can allow or disable (by type) any loop kind.

For for loops, we have two different possible special handlings. Loops that look like for loops can be reshaped into proper iterator-based fors or into range-based fors.

  • reconstruct while let loops.

(see https://github.com/hacspec/hax/issues/522 for simple whiles)

Contributor Guide