Towards polymorphic sorts

[ranjitjhala]

Allow polymorphic sorts, see rset.rs, rmap.rs and rmapk.rs and clients.

[ranjitjhala]

The rset00.rs tests work as expected. I'll probably add some more tests, and perhaps some WF/error message tests too, but I think you can take a look at this PR.

[ranjitjhala]

Currently, we have to explicitly write the generic <Tiger> { elems : Set<Tiger>} in the refined_by clause.

Should we require this? (Without it, you get a weird crash later.) But OTOH we could plausibly automatically just "scrape" them from the actual sorts appearing in the refined_by ? e.g. Set<Tiger> I suppose the trouble is how do you know which one is supposed to be a generic and which one is just some other rust type?

#[flux::refined_by(<Tiger> { elems: Set<Tiger> })]
// #[flux::refined_by( elems: Set<Tiger> )] //~ ERROR unbound generic `Tiger`
pub struct RSet<Tiger> {
    pub inner: std::collections::HashSet<Tiger>,
}

[ranjitjhala]

Maybe for now, better to be explicit and throw a WF error if there is an unbound generic.

[ranjitjhala]

I decided to go the other way -- I removed the explicit params and instead just gather them from the sorts themselves.
The principle here -- perhaps inspired by the excessive bureaucracy at banks in India -- is we shouldn't be asking users to write down stuff that we can extract from other stuff they've already written down!

[ranjitjhala]

@nilehmann - I think I'm done with this, ready for review.

[nilehmann]

I'm going to take a look at this now

[nilehmann]

First batch of comments.

I've only looked until desugaring. Most comments are related to how we use the SortResolver. I think we could reuse it instead of creating a new one every time.

Also as a general comment about SortResolver. I think we never have a case where both generics and sort_vars are Some so we could expose that as two construction methods (not sure about the names)

impl<'a> SortResolver<'a> {
    fn with_sort_vars(sess: &'a FluxSession, sort_decls: &'a SortDecls, sort_vars: &[surface::Ident]) -> Self {
        ... 
    }
    
    // we grab `sort_decls` from `genv` and fetch generics of `owner_id` inside 
    fn with_generics(genv: &'a GlobalEnv<'a, '_>, owner_id: DefId) -> Self {
        ...
    }
}

edit: Just noticed that for qualifiers both generics and sort_vars are None, but the SortResolver for qualifier should morally be a SortResolver::with_sort_vars(sess, sort_decls, &[]).

[nilehmann]

@ranjitjhala Another batch of comments. Looking better!

I still haven't gone through the changes in flux-fhir-analysis and wf.

[nilehmann]

Comments about fhir_analysis and wf

[ranjitjhala]

Ok I think I addressed the various comments; including representing the T inside refined_by with Var.
One unpleasant thing is that to do so, I'm now requiring an explicit list of sort_params i.e.

#[flux::refined_by(<K,V>{keys: Set<K>, vals: Map<K, V>})]

instead of automatically finding the K,V from the generics (its a bit tedious as you have to first "gather"
the relevant Vec<Ident> using the generics -- still, not impossible by any means...)

Not clear if we want to write this explicitly -- more the user has to write, the more opportunity for error!

Any thoughts?

[nilehmann]

Ok, this looks good. There are still many details I'm not happy with, but I'm ok with merging so we can move forward.

About the syntax, as always, I'm not too worried about it, we can always change it later. I'm more concerned about having enough pieces of the puzzle in place.

That being said, I do think is a bit redundant to annotate the parameters. It also makes it that you need to check more things. For example, this line will crash if you don't use the same names.