Assert commands

[MattWindsor91]

(This is fairly pie in the sky.)

I'm wondering if we should have a syntax

assert(x == 1, {| error() |});

which desugars to

if (!(x == 1)) { {| error() |} ; {| error() |} }

to make the intent of things like the error check in the ARC clearer.

[septract]

Is error() a built-in construct? - should we have one?

[septract]

It'd be nicer just to have assert(x==1) as the syntax.

[MattWindsor91]

error() isn't, but thinking about it it would be nice to have it, because then we can create more sugar with it.

For example, something like

{| local(x == 4) |}

could desugar to

{| if x == 4 then error() else emp |}

I'd need to work out the metatheory behind the error view though, because ideally it should be treated specially (e.g. don't put it in the defining view set).

[septract]

As an initial approximation, can we just assume we always have the following?
constraint error() -> false;

[MattWindsor91]

We could do, or at least error if one isn't defined. (Or add it, but that seems a bit magical?)

[septract]

I guess we could just get the parser to treat error as a magic view name, i.e. you're not allowed to define it in a constraint. Then insert into the set of defining views (not sure where in the pipeline?)

[MattWindsor91]

Yeah, that sounds like a good idea—means you can use error in view expressions manually if needed.

[septract]

Okay, I can take a look at the parser end when I'm futzing with #74 / #75.

On 1 November 2016 at 10:56, Matt Windsor notifications@github.com wrote:

Yeah, that sounds like a good idea—means you can use error in view expressions manually if needed.

— You are receiving this because you commented. Reply to this email directly, view it on GitHub https://github.com/septract/starling-tool/issues/76#issuecomment-257538917, or mute the thread https://github.com/notifications/unsubscribe-auth/AANd9isxQDfkj99P6gnC7caiij0ohmVxks5q5xrlgaJpZM4Kl75- .

http://www-users.cs.york.ac.uk/~miked/

[MattWindsor91]

Sure! Apologies in advance for the mess that is Parser.fs.

[septract]

I will come and complain later ;)

[bensimner]

I think magical constructs like an 'error()' view are fine so long as they're treated as keywords, sort of like emp

A really useful one would be some way of keeping track of values of variables through the flow of the program, these are the 2 special views in the arc proof and maybe they can get sugared up in something similar to an assert?

[MattWindsor91]

In general, sure, that's what the {| local(x == 4) |} sugar would be for. But in the ARC case those special views are actually much weaker than local variable assertions: stating that f == free and c == count is not stable!

[MattWindsor91]

The example for this was the ARC, but we can simplify the ARC so it doesn't need this. Thus, this needs an example.