Skip to content

Commit

Permalink
Fix added block syntax for interactions in compiler plugin
Browse files Browse the repository at this point in the history
  • Loading branch information
robflop committed Aug 14, 2024
1 parent d24407b commit 2db69ba
Show file tree
Hide file tree
Showing 2 changed files with 15 additions and 11 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -26,24 +26,24 @@ object interactionExamplesObject:
val integerInteraction1 = Interaction[Int, Int]

val integerInteraction2 = Interaction[Int, Int]
.requires((a: Int, b: Int) => a > b)
.requires { (a: Int, b: Int) => a > b }

val integerInteraction3 = Interaction[Int, Int]
.requires((a: Int, b: Int) => a > b)
.executes((a: Int, b: Int) => a)
.requires { (a: Int, b: Int) => a > b }
.executes { (a: Int, b: Int) => a }

val integerInteraction4 = Interaction[Int, Int]
.requires((a: Int, b: Int) => a > b)
.executes((a: Int, b: Int) => a)
.ensures((a: Int, b: Int) => a > b)
.requires { (a: Int, b: Int) => a > b }
.executes { (a: Int, b: Int) => a }
.ensures { (a: Int, b: Int) => a > b }

val integerSource: Source[Int] = Source(1)
val integerDerived: Derived[Int] = Derived { integerSource.value + integerSource.value }

val integerInteraction5 = Interaction[Int, Int]
.requires((curr: Int, _) => curr < 3)
.modifies(integerSource)
.executes((curr: Int, _) => curr + 1)
.ensures((curr: Int, _) => curr < 3)
.requires { (curr: Int, _) => curr < 3 }
.modifies { integerSource }
.executes { (curr: Int, _) => curr + 1 }
.ensures { (curr: Int, _) => curr < 3 }
end interactionExamplesFunction
end interactionExamplesObject
Original file line number Diff line number Diff line change
Expand Up @@ -242,7 +242,7 @@ class LoRePhase extends PluginPhase:
rawInteractionTree.sourcePos
)
TVar("<error>")
case modifiesTree @ Apply(Apply(TypeApply(Select(_, methodName), _), List(innerNode)), List(Ident(modVar)))
case modifiesTree @ Apply(Apply(TypeApply(Select(_, methodName), _), List(innerNode)), List(Block(_, Ident(modVar))))
if methodName.toString == "modifies" =>
// Interaction modifies is different from the other methods as it doesn't take an arrow function as input
var innerTerm = buildLoreRhsTerm(innerNode, indentLevel + 1, operandSide)
Expand Down Expand Up @@ -321,6 +321,10 @@ class LoRePhase extends PluginPhase:
arrowTree.sourcePos
)
TVar("<error>")
case arrowBodyTree @ Block(_, arrowBody) => // Arrow functions part 2
// When the body of the arrow function is in the second parameter as opposed to the first, for some reason
// This happens for example when you call requires/ensures/executes/modifies on Interactions, "{ (..) => (..) }"
buildLoreRhsTerm(arrowBody, indentLevel, operandSide)
case _ => // Unsupported RHS forms
// No access to sourcePos here due to LazyTree
report.error(
Expand Down

0 comments on commit 2db69ba

Please sign in to comment.