## 2023-07-19

* Have another person on board doing some conversion work (Eric Martin)
* Making pretty good progress overall
*

## 2023-07-05

pub struct Decls {
    pub max_size: usize,
    pub trait_decls: Vec<TraitDecl>,
    pub impl_decls: Vec<ImplDecl>,
    pub neg_impl_decls: Vec<NegImplDecl>,
    pub alias_eq_decls: Vec<AliasEqDecl>,
    pub alias_bound_decls: Vec<AliasBoundDecl>,
    pub local_trait_ids: Set<TraitId>,
    pub local_adt_ids: Set<AdtId>,
}

We would need:

Ty {
    RigidTy(RigidTy),
    AliasTy(AliasTy),
    PredicateTy(PredicateTy),
    Variable(Variable),
}

TraitDecl
  -> TraitId
  -> Ty | Lt
    -> Set(Predicate | Relation | ForAll | Implies)
      -> Predicate -> (IsImplemented | NotImplemented | WellFormedTraitRef | IsLocal) + TraitRef
      -> Relation -> (Equals | Sub | Outlives | WellFormed) + (Parameter(Ty | Lt), Parameter(Ty | Lt))
      -> ForAll(Binder<Wc>)
      -> Implies(Wcs, Wc)

ImplDecl
  -> Binder(Ty|Lt)
  -> TraitRef
  -> Wcs

NegImplDecl
  -> Binder(Ty|Lt)
  -> TraitRef
  -> Wcs

AliasEqDecl
  -> Binder(Ty|Lt)
  -> AliasTy(AliasName, Parameters(Ty|Lt))
  -> Ty
  -> Wcs

AliasBoundDecl
  -> AliasTy
  -> Binder<Wc>
  -> Wcs

To understand the role of each formality declaration, start here:

* [the `Program::to_prove_decls` method](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-rust/src/prove.rs#L19)
* e.g. alias bound decls are [created here](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-rust/src/prove.rs#L223)

Maybe we want to create these [rust-like structure](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-rust/src/grammar.rs#L47-L67)?

doesn't have predicates, has [where clauses](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-rust/src/grammar.rs#L338-L348)

e.g, instead of alias bound decl we have [this](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-rust/src/grammar.rs#L236-L243)

want code that does:

let compiler = Compiler::new(input_source_file)?;

let mut all_crates = vec![];

for crate in compiler.crates() {
    let mut current_crate = vec![];
    for item in crate.items() {
        match item {
            Struct => {
                let formality_struct = StructItem { ... };
                current_crate.push(formality_struct.upcast());
            }
        }
    }
    all_crates.push(Crate { items: current_crate });
}

formality_check::check(Program { crates: all_crates })

what might be helpful for types is [the `Ty` parser impl](https://github.com/nikomatsakis/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-types/src/grammar/ty/parse_impls.rs#L14-L56), which parses rust-like syntax.

## 2023-06-28

* what do we need from SMIR for a-mir-formality?
* [x] types
* [x] MIR
* [ ] predicates
* [ ] generics
* [ ] list all trait declarations of a crate
* do what we do for listing all def ids of all things with bodies
* [ ] list all trait impls of a crate
* [ ] constants

https://github.com/rust-lang/a-mir-formality

https://github.com/rust-lang/a-mir-formality/blob/main/crates/formality-prove/src/decls.rs

https://github.com/rust-lang/a-mir-formality/blob/ca14d9941244eefc472a24895515cc278244534f/crates/formality-prove/src/decls.rs#L13-L22

goal for next meeting:

* go through the decls declaration from a-mir-formality to enumerate exactly what info is needed about each of the kinds of items, along with what items we need
* maybe add some of those items

trait Foo { }
impl Foo for u32 { }

* July 12 -- niko is in seattle
* July 19 -- niko is flying on an airplane to France :snake: :airplane:
*