Commit a70f61e9 authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

[anml] Translation to core.

parent 2bc3a6e4
......@@ -105,12 +105,15 @@ package object common {
case Right(t) => t
case Left(err) => sys.error(err)
}
override def toString: String = s"(${op.op} $lhs $rhs)"
}
case class Op1(op: UnaryOperator, lhs: Expr) extends Expr {
override def typ: Type = op.tpe(lhs.typ) match {
case Right(t) => t
case Left(err) => sys.error(err)
}
override def toString: String = s"(${op.op} $lhs)"
}
......
......@@ -60,19 +60,19 @@ package object core {
sealed trait Function {
def template: FunctionTemplate
def params: Seq[Term]
def params: Seq[Expr]
def typ: Type = template.typ
}
case class Constant(override val template: ConstantTemplate, override val params: Seq[Term])
case class Constant(override val template: ConstantTemplate, override val params: Seq[Expr])
extends Function {
require(template.params.size == params.size)
override def toString: String = super.toString
override def toString: String = s"$template(${params.mkString(", ")})"
}
class BoundConstant(override val template: ConstantTemplate, override val params: Seq[Cst])
extends Constant(template, params)
final case class Fluent(override val template: FluentTemplate, override val params: Seq[Term])
final case class Fluent(override val template: FluentTemplate, override val params: Seq[Expr])
extends Function {
require(template.params.size == params.size)
template.params.zip(params).foreach {
......@@ -115,29 +115,29 @@ package object core {
/** Denotes an assertion that changes a fluent */
sealed trait ProvidesChange { self: TimedAssertion =>
def valueAfterChange: Term
def valueAfterChange: Expr
}
final case class TimedEqualAssertion(start: Expr, end: Expr, fluent: Fluent, value: Term)
final case class TimedEqualAssertion(start: Expr, end: Expr, fluent: Fluent, value: Expr)
extends TimedAssertion
with RequiresSupport {
override def toString: String = s"[$start, $end] $fluent == $value"
}
final case class TimedAssignmentAssertion(start: Expr, end: Expr, fluent: Fluent, value: Term)
final case class TimedAssignmentAssertion(start: Expr, end: Expr, fluent: Fluent, value: Expr)
extends TimedAssertion
with ProvidesChange {
override def valueAfterChange: Term = value
override def valueAfterChange: Expr = value
override def toString: String = s"[$start,$end] $fluent := $value"
}
final case class TimedTransitionAssertion(start: Expr,
end: Expr,
fluent: Fluent,
from: Term,
to: Term)
from: Expr,
to: Expr)
extends TimedAssertion
with RequiresSupport
with ProvidesChange {
override def valueAfterChange: Term = to
override def valueAfterChange: Expr = to
override def toString: String = s"[$start, $end] $fluent == $from :-> $to"
}
......
......@@ -172,18 +172,10 @@ package object full {
trait StaticAssertion extends Statement
case class BooleanAssertion(expr: StaticExpr) extends StaticAssertion {
require(expr.typ.isSubtypeOf(Type.Boolean))
override def toString: String = expr.toString
}
@deprecated
case class StaticEqualAssertion(left: StaticExpr, right: StaticExpr) extends StaticAssertion {
override def toString: String = s"$left == $right"
}
@deprecated
case class StaticDifferentAssertion(left: StaticExpr, right: StaticExpr) extends StaticAssertion {
override def toString: String = s"$left != $right"
}
case class StaticAssignmentAssertion(left: StaticExpr, right: StaticExpr)
case class StaticAssignmentAssertion(left: Constant, right: StaticExpr)
extends StaticAssertion {
override def toString: String = s"$left := $right"
}
......
......@@ -34,7 +34,7 @@ object FullToCore {
def unit(statements: core.Statement*): CoreM[Unit] = CoreM((), statements)
}
private def f2c(expr: full.StaticExpr)(implicit ctx: Context): CoreM[Term] = {
private def f2c(expr: full.StaticExpr)(implicit ctx: Context): CoreM[Expr] = {
expr match {
case full.ConstantExpr(cst) => CoreM.pure(cst)
case full.Variable(v) => CoreM.pure(v)
......@@ -46,10 +46,20 @@ object FullToCore {
_ <- CoreM.unit(core.LocalVarDeclaration(variable))
_ <- CoreM.unit(core.BindAssertion(cst, variable))
} yield variable
case full.BinaryExprTree(op, lhs, rhs) =>
for {
l <- f2c(lhs)
r <- f2c(rhs)
} yield Op2(op, l, r)
case full.UnaryExprTree(op, e) =>
for {
ec <- f2c(e)
} yield Op1(op, ec)
}
}
private def f2c(exprs: List[full.StaticExpr])(implicit ctx: Context): CoreM[List[Term]] = {
private def f2c(exprs: List[full.StaticExpr])(implicit ctx: Context): CoreM[List[Expr]] = {
exprs match {
case Nil => CoreM.pure(Nil)
case head :: tail =>
......@@ -79,6 +89,12 @@ object FullToCore {
}
private def f2c(block: full.Statement)(implicit ctx: Context): CoreM[Unit] = block match {
case full.BooleanAssertion(e) =>
for {
ec <- f2c(e)
_ <- CoreM.unit(core.StaticBooleanAssertion(ec))
} yield ()
case full.StaticAssignmentAssertion(lhs: full.Constant, full.ConstantExpr(rhs))
if lhs.params.forall(_.isInstanceOf[full.ConstantExpr]) =>
val boundCst =
......@@ -91,22 +107,9 @@ object FullToCore {
throw new UnsupportedOperationException(
s"Assignment assertions on constant functions are only supported when all parameters are declared instances: $block")
case x: full.StaticEqualAssertion =>
for {
lVar <- f2c(x.left)
rVar <- f2c(x.right)
_ <- CoreM.unit(core.StaticEqualAssertion(lVar, rVar))
} yield ()
case x: full.StaticDifferentAssertion =>
for {
lVar <- f2c(x.left)
rVar <- f2c(x.right)
_ <- CoreM.unit(core.StaticDifferentAssertion(lVar, rVar))
} yield ()
case full.TemporallyQualifiedAssertion(qualifier, assertion) =>
val startEnd: CoreM[(Term, Term)] =
val startEnd: CoreM[(Expr, Expr)] =
qualifier match {
case full.Equals(interval)
if ctx.config.mergeTimepoints && assertion.name.startsWith(reservedPrefix) =>
......
......@@ -230,11 +230,30 @@ abstract class AnmlParser(val initialContext: Ctx) {
}
}
val staticTerm: Parser[StaticExpr] = {
val constantFuncTerm: Parser[Constant] = P {
val partiallyAppliedConstant = partiallyAppliedFunction
.namedFilter(_._1.isInstanceOf[ConstantTemplate], "is-constant")
.map(tup => (tup._1.asInstanceOf[ConstantTemplate], tup._2))
(constantFunc ~/ Pass).flatMap(f =>
f.params.map(param => param.typ) match {
case Seq() => (("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq()))
case paramTypes =>
"(" ~/ varList(paramTypes, ",").map(args => Constant(f, args)) ~ ")" ~/ Pass
}) |
(partiallyAppliedConstant ~/ Pass).flatMap {
case (f, firstArg) =>
f.params.map(param => param.typ) match {
case Seq(singleParam) =>
(("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq(CommonTerm(firstArg))))
case paramTypes =>
"(" ~/ varList(paramTypes.tail, ",")
.map(args => Constant(f, CommonTerm(firstArg) +: args)) ~ ")" ~/ Pass
}
}
}
val staticTerm: Parser[StaticExpr] = {
(durationKW ~/ Pass)
.flatMap(_ =>
(for {
......@@ -247,22 +266,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
.opaque("duration") |
int.map(i => CommonTerm(IntLiteral(i))) |
variable.map(CommonTerm(_)) |
(constantFunc ~/ Pass).flatMap(f =>
f.params.map(param => param.typ) match {
case Seq() => (("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq()))
case paramTypes =>
"(" ~/ varList(paramTypes, ",").map(args => Constant(f, args)) ~ ")" ~/ Pass
}) |
(partiallyAppliedConstant ~/ Pass).flatMap {
case (f, firstArg) =>
f.params.map(param => param.typ) match {
case Seq(singleParam) =>
(("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq(CommonTerm(firstArg))))
case paramTypes =>
"(" ~/ varList(paramTypes.tail, ",")
.map(args => Constant(f, CommonTerm(firstArg) +: args)) ~ ")" ~/ Pass
}
}
constantFuncTerm
}
val staticExpr: P[StaticExpr] = Tmp.expr
......@@ -409,12 +413,17 @@ abstract class AnmlParser(val initialContext: Ctx) {
(staticExpr.sideEffect(leftExpr = _) ~/
(":=".! ~/ staticExpr.namedFilter(_.typ.overlaps(leftExpr.typ), "has-compatible-type")).? ~
";")
.namedFilter({
case (_: Constant, Some(_)) => true
case (_, Some(_)) => false
case (_, None) => true
}, "assignment-to-const-func-only")
.namedFilter({
case (_, Some(_)) => true
case (expr, None) => expr.typ.isSubtypeOf(Type.Boolean)
}, "boolean-if-no-right-side")
}, "boolean-if-not-assignment")
.map {
case (left, Some((":=", right))) => StaticAssignmentAssertion(left, right)
case (left: Constant, Some((":=", right))) => StaticAssignmentAssertion(left, right)
case (expr, None) => BooleanAssertion(expr)
case _ => sys.error("Something is wrong with this parser.")
}
......
......@@ -13,7 +13,7 @@ class ActionInstantiationTest extends FunSuite {
lang.parse("""
|fluent boolean sv;
|action Template(boolean x, boolean y) {
| duration := 10;
| duration == 10;
| [all] sv == true;
| [all] contains id: sv == x :-> y;
|};
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment