a-mir-formality
a-mir-formality copied to clipboard
rust-lang
a model of MIR and the Rust type/trait system
Right now, when a function or impl is supposed to get "implied bounds" from a type `Foo`, we add `(well-formed (type Foo))` to the environment. In the "expanded implied bounds"...
Rust prohibits type parameters in a trait impl that don't appear in the trait definition: ```rust impl Iterator for () { type Item = (); } // ERROR ``` and...
Much as we have split out `WhereClause` (Rust surface level) from the logic layer's notion of goals/clauses, we should split out *Rust types* that user's write from the surface layer....
Real MIR carries "user type assertions" that correspond to pattern annotations and the like. We need to add that to a-mir-formality. @lcnr has recently been fixing bugs in those and...
The goal of this spike is to get this program checking completely within a-mir-formality: ```rust static UNIT: &'static &'static () = &&(); fn foo(_: &'a &'b (), v: &'b T)...
Status update: * [x] Skeleton of MIR type checker exists (added by #13, #52) * [ ] Bring function where clauses into scope when creating initial environment * [ ]...
We need to support *unsafe* traits and impls. The `rust:Send` and `rust:Sync` traits should be defined as unsafe.
Currently we have one declaration for all ADTs in the decl grammar: https://github.com/nikomatsakis/a-mir-formality/blob/81ba52b8695db7f87f50b0916940b2bb41fe6d59/src/decl/grammar.rkt#L27-L31 resulting instances like this ``` (; struct Foo { } AdtDecl_Foo (term (Foo (struct () ; no...
We should create a test harness / rustc driver `formalityc` that works as follows: * It parses an input rust crate and compiles it to MIR * It generates MIR...
Currently we have only the cosld solver. We should model the chalk recursive solver. * [x] #33 * [ ] Introduce a recursive solver with canonical goals * [ ]...