sdthompson1 / babylon

An experimental new programming language with verification features.
https://www.solarflare.org.uk/babylon
Other
1 stars 0 forks source link

Allow return f(x); where x is a ref parameter #9

Open sdthompson1 opened 1 month ago

sdthompson1 commented 1 month ago

Currently the use of 'ref' parameters is very restricted. E.g. if f and g take ref parameters, then you cannot write a = f(x) + g(x); you have to do something like f0 = f(x); g0 = g(x); a = f0 + g0; instead.

The rationale for this is to simplify the semantics (e.g. the order of evaluation of subexpressions does not matter) but it can be annoying.

Perhaps in general we should define e.g. subexpressions to evaluate left to right, then e.g. the expression f(x) + g(x) would have meaning.

But that might be too much work for now (perhaps it could be split off into a separate issue) so for now I suggest focusing on easier cases e.g. I think return f(x); is currently disallowed (if x is a ref parameter) but I don't see any real reason why it couldn't be allowed.