Better support for projections in flux refinements

[vrindisbacher]

Right now, it seems like it's not possible to use projections in a few scenarios. Say I have the following structs:

#[refined_by(x: int)]
pub struct S2 {
   #[field(u32[x])]
    x: u32
}

#[refined_by(s: S2)]
pub struct S1 {
   #[field(S2[s])]
    s: S2
}

This does not work:

#[sig(fn (&S1[@s]) -> u32[s.s.x])] //~ERROR here - s.s is ok but s.s.x results in an unexpected token
fn get_inner(s1: &S1) -> u32 {
    s1.s.x
}

And neither does this:

defs! {
  fn new_s2() -> S2 {
        S2 { x: 0 }
  }
  
  fn index_new_s2() ->  int {
       new_s2().x //~ERROR unexpected token when using `.` on `new_s2()`
  }
}

It would be helpful from an ergonomic standpoint if we could support this sort of thing.

[ranjitjhala]

Is this mostly a parsing issue? i.e. are these things supported "internally" ?

[vrindisbacher]

I'd need to look at the code again to be 100% sure but I don't think this is currently supported - the left side of "dot" expressions are parsed as an expr path and this is propagated through surface -> fhir. We would need to parse the left side as an expression and change the representation through surface and fhir. I don't think this is too bad though - I can take a stab at it.

[nilehmann]

This is supported in rty and the encoding into fixpoint should handle it as well (modulo bugs arising because we've never tested it). We need to change the surface syntax and fhir, and consequently sort checking/elaboration.

[vrindisbacher]

I think the parsing may be a pain here... 🙃

[nilehmann]

Something like this may work

Level10<AllowStruct>: surface::Expr = {
    <lo:@L> "if" <p:Level1<"false">> "{" <e1:Level1<AllowStruct>> "}" <e2:ElseIf> <hi:@R> => {
        surface::Expr {
            kind: surface::ExprKind::IfThenElse(Box::new([p, e1, e2])),
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
    <base:Atom<AllowStruct>> "." <fld:Ident> => {
        todo!()
    },
    <lo:@L> <f:Ident> "(" <args:Comma<Level1<AllowStruct>>> ")" <hi:@R> => {
        surface::Expr {
            kind: surface::ExprKind::App(f, args),
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
    <lo:@L> "<" <qself:Ty> "as" <path:Path> ">" "::" <name:Ident> "(" <fun_args:Comma<Expr>> ")" <hi:@R> => {
        let alias = surface::AliasReft { qself: Box::new(qself), path, name };
        surface::Expr {
            kind: surface::ExprKind::Alias(alias, fun_args),
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
    Atom<AllowStruct>,
    "(" <Level1<AllowStruct>> ")"
}
Atom<AllowStruct>: surface::Expr = {
    <lo:@L> <lit:Lit> <hi:@R> => {
        surface::Expr {
            kind: surface::ExprKind::Literal(lit),
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
    <lo:@L> <path:ExprPath> <hi:@R> => surface::Expr {
        kind: surface::ExprKind::Path(path),
        node_id: cx.next_node_id(),
        span: cx.map_span(lo, hi),
    },
    <lo:@L> <name:ExprPath> "{" <args:Comma<ConstructorArg>> "}" <hi:@L> if AllowStruct == "true" => {
    	surface::Expr {
            kind: surface::ExprKind::Constructor(Some(name), args) ,
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
    <lo:@L> "{" <args:Comma<ConstructorArg>> "}" <hi:@L> if AllowStruct == "true" => {
    	surface::Expr {
            kind: surface::ExprKind::Constructor(None, args) ,
            node_id: cx.next_node_id(),
            span: cx.map_span(lo, hi),
        }
    },
}

I'm taking inspiration from syn https://docs.rs/syn/latest/src/syn/expr.rs.html#1581

edit:
hmm this doesn't consider multiple chained projections, but I think is on the right track