search

jyoo980 / silver

Definition of the Viper intermediate verification language.
Mozilla Public License 2.0
0 stars 0 forks source link

Rewrite functions too #33

Closed ionathanch closed 3 years ago

ionathanch commented 3 years ago

Might as well, right? Gotta change the writeup to include this though, but functions are similar enough to methods that it can probably just be mentioned in passing. The only difference is that the body of a function is an expression, not a statement.

jyoo980 commented 3 years ago

@ionathanch I can change the parts I've written about functions

ionathanch commented 3 years ago

I was thinking the same thing, since they're both Contracted, but yeah it seemed like it would make the code more complex to deduplicate things

jyoo980 commented 3 years ago

I was thinking we'd define a sealed trait where we only declare the things we care about, then have Function and Method implement it and override those values specifically. They'd then have a .toFunction or .toMethod thing we'd call at the end after we do the rewrite but I'm just yak shaving here

Please don't implement this lol update comment

jyoo980 commented 3 years ago

Because the body of Function is an Option[Exp], while the body of Method is an Option[Seqn] (statements)

ionathanch commented 3 years ago

Just realized I haven't written any test examples, gonna do some (or one, at least) and merge after that

jyoo980 commented 3 years ago

🅱️regor spinning in his grave rn