cryspen/hax

Support `let` without initialization

Open

#156 opened on Jun 23, 2023

View on GitHubContributor guide
 (0 comments) (1 reaction) (0 assignees)OCaml (61 forks)auto 404
enginehelp wantedkeep-openmarked-unimplementedunsupported-rust

Repository metrics

Stars
 (456 stars)
PR merge metrics
 (PR metrics pending)

Description

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)

Contributor guide

Research direction
Understand the Hax AST and implement translation of let patterns without initialization, extracting bindings and generating let bindings with Option type, then replacing binder occurrences with unwrap().
Tech stack
rust
Domain
backend
Issue type
Feature
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
3
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
1-2 days
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Fresh
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
RustOCaml
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
40