cryspen/hax

Support `let` without initialization

Aperta

#156 aperta il 23 giu 2023

Vedi su GitHubGuida contributor
 (0 commenti) (1 reazione) (0 assegnatari)OCaml (61 fork)auto 404
enginehelp wantedkeep-openmarked-unimplementedunsupported-rust

Metriche repository

Star
 (456 stelle)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

Hax doesn't support the following:

fn main() {
    let (x, y);
    x = 0;
    y = 0;
}

Draft plan to support let <PAT>; BODY:

  • translate the pattern PAT into our AST, extract bindings
  • for each binding, generate a let binding wrapped with in an option type
  • replace any occurrence of each binder b in BODY with b.unwrap() (or make everything a monad, but that's quite heavy)

Guida contributor

Direzione di ricerca
Comprendere l'AST di Hax e implementare la traduzione di let pattern senza inizializzazione, estraendo i binding e generando let binding con tipo Option, quindi sostituendo le occorrenze dei binder con unwrap().
Tech stack
rust
Dominio
backend
Tipo issue
Funzionalità
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
3
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
1-2 giorni
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Nuova
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
RustOCaml
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
40