[CN] Proposal: better support for chains of spec-level conditionals

[septract]

CN supports specification-level conditionals (if (..) {..} else {..}) but the syntax is restricted in a way that makes it ugly to write chains of conditionals. I suggest we make the syntax a bit more permissive so these are nicer to write.

Since this idiom can already be encoded into the CN spec language, I'd guess this modification would require only minor parser changes. I'm happy to work on a PR for this if people think it would valuable (looking for feedback from @cp526 and @dc-mak mainly).

Problem

In C, we can write chains of conditionals as so:

// C code-level conditional chain: 
if (c1) { 
  fn1(); 
} else if (c2) { 
  fn2(); 
} else if (c3) { 
  fn3(); 
  ... 
} else { 
  fnN(); 
} 

In CN, we can nearly do this, but it's uglier because we can't drop the LBRACE {...} surrounding the else case. So we end up having to write the following:

// CN spec-level conditional chain: 
if (c1) { 
  fn1(); 
} else { if (c2) { 
  fn2(); 
} else { if (c3) { 
  fn3(); 
  ... 
} else { 
 fnN() 
}}}}}}}}}}} // <-- what is this, Lisp? 

We have several motivating example of this pattern in the OpenSUT MKM proofs - see here. As well as being a little ugly, the nesting of brackets was kind of annoying to get right. So I think this is a (small) UX issue as well.

(Aside: an interesting thing to note in the MKM example is that the spec-level conditional is pretty much just lifting the C-level code conditional structure, in this case a switch statement. I'd expect we'll often have CN specs that reflect the C-level structure in this way, which motivates keeping parity of expressiveness between C and CN control constructs.)

Proposal

I suggest we follow the C convention and allow conditional chains without brackets. We could either allow 'bare' else-expressions without {...}, or (probably easier) just special-case the situation where an else is followed immediately by an if.

[dc-mak]

Lgtm but I'm off until March so won't be able to say much more than that.

[septract]

@dc-mak Thanks for working on this, but I don't think your fix actually addresses my use-case. Looks like we can now write predicate-level if-else chains, but we can't write if-else chains in contracts (which is where I want them). For example, this example doesn't parse:

void ifelsechain(int x) 
/*@ 
requires 
  if (true) { 
    true 
  } else if (true) { 
   true 
  } else {
   true
  }; 
@*/
{ 
  return; 
}

[dc-mak]

Yeah so very annoyingly, two issues with the grammar for predicates and specifications being slightly different:

1. return is a statement in the former, and an expression in the latter (CN: Make assert optional #922)
2. The CN internal OCaml data-structures for specifications do not support ifs on specifications. @cp526 can comment on the difficulty of implementing this.