Commit 2bc3a6e4 authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

[anml] Parsing to full model with generalized expressions.

parent dd322384
package copla.lang.model
import copla.lang.model
import copla.lang.model.common.operators.{BinaryOperator, UnaryOperator}
import scala.annotation.tailrec
......@@ -9,11 +10,11 @@ package object common {
case class Id(scope: Scope, name: String) {
override def toString: String = scope.toScopedString(name)
def toTPId: Timepoint = new Timepoint(this)
def toTPId = Timepoint(this)
}
case class Timepoint(id: Id) {
override def toString: String = id.toString
object Timepoint {
def apply(id: Id): LocalVar = LocalVar(id, Type.Time)
}
sealed trait Scope {
......@@ -61,14 +62,16 @@ package object common {
object Type {
val Numeric = Type(Id(RootScope, "__numeric__"), None)
val Integer = Type(Id(RootScope, "integer"), Some(Numeric))
val Time = Integer //Type(Id(RootScope, "time"), Some(Integer))
val Float = Type(Id(RootScope, "float"), Some(Numeric))
val Boolean = Type(Id(RootScope, "boolean"), None)
}
sealed trait Term {
def id: Id
sealed trait Expr {
def typ: Type
}
sealed trait Term extends Expr {
def id: Id
}
object Term {
def unapply(v: Term) = Option((v.id, v.typ))
}
......@@ -97,6 +100,22 @@ package object common {
override def toString: String = id.toString
}
case class Op2(op: BinaryOperator, lhs: Expr, rhs: Expr) extends Expr {
override def typ: Type = op.tpe(lhs.typ, rhs.typ) match {
case Right(t) => t
case Left(err) => sys.error(err)
}
}
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)
}
}
sealed trait FunctionTemplate {
def id: Id
def typ: Type
......
......@@ -14,12 +14,6 @@ package object core {
sealed trait Declaration[T] {
def id: Id
}
final case class TimepointDeclaration(tp: Timepoint)
extends Declaration[Timepoint]
with Statement {
override def id: Id = tp.id
override def toString: String = s"timepoint $id"
}
final case class TypeDeclaration(typ: Type) extends Declaration[Type] with InModuleBlock {
override def id: Id = typ.id
......@@ -89,9 +83,15 @@ package object core {
}
sealed trait StaticAssertion extends Statement
final case class StaticBooleanAssertion(e: Expr) extends StaticAssertion {
require(e.typ.isSubtypeOf(Type.Boolean))
override def toString: String = s"assert($e)"
}
@deprecated
final case class StaticEqualAssertion(left: Term, right: Term) extends StaticAssertion {
override def toString: String = s"$left == $right"
}
@deprecated
final case class StaticDifferentAssertion(left: Term, right: Term) extends StaticAssertion {
override def toString: String = s"$left != $right"
}
......@@ -104,8 +104,8 @@ package object core {
}
sealed trait TimedAssertion extends Statement {
def start: TPRef
def end: TPRef
def start: Expr
def end: Expr
def fluent: Fluent
}
......@@ -118,19 +118,19 @@ package object core {
def valueAfterChange: Term
}
final case class TimedEqualAssertion(start: TPRef, end: TPRef, fluent: Fluent, value: Term)
final case class TimedEqualAssertion(start: Expr, end: Expr, fluent: Fluent, value: Term)
extends TimedAssertion
with RequiresSupport {
override def toString: String = s"[$start, $end] $fluent == $value"
}
final case class TimedAssignmentAssertion(start: TPRef, end: TPRef, fluent: Fluent, value: Term)
final case class TimedAssignmentAssertion(start: Expr, end: Expr, fluent: Fluent, value: Term)
extends TimedAssertion
with ProvidesChange {
override def valueAfterChange: Term = value
override def toString: String = s"[$start,$end] $fluent := $value"
}
final case class TimedTransitionAssertion(start: TPRef,
end: TPRef,
final case class TimedTransitionAssertion(start: Expr,
end: Expr,
fluent: Fluent,
from: Term,
to: Term)
......@@ -141,48 +141,6 @@ package object core {
override def toString: String = s"[$start, $end] $fluent == $from :-> $to"
}
sealed trait IntExpr
object IntExpr {
def apply(lit: Int): IntExpr = IntTerm(IntLiteral(lit))
}
final case class IntTerm(e: Term) extends IntExpr {
require(e.typ.isSubtypeOf(Type.Integer))
override def toString: String = e.toString
}
final case class Minus(e: IntExpr) extends IntExpr
final case class Add(lhs: IntExpr, rhs: IntExpr) extends IntExpr
final case class Mul(lhs: IntExpr, rhs: IntExpr) extends IntExpr
final case class Div(lhs: IntExpr, rhs: IntExpr) extends IntExpr
/** A timepoint, declared when appearing in the root of a context.*/
final case class TPRef(id: Timepoint, delay: IntExpr = IntExpr(0)) {
override def toString: String =
id.toString + (delay match {
case IntTerm(IntLiteral(d)) =>
if(d == 0) ""
else if(d > 0) s"+$d"
else s"-${-d}"
case x => s"+$x"
})
def +(d: IntExpr): TPRef = TPRef(id, Add(delay, d))
def +(d: Int): TPRef = this + IntExpr(d)
def -(d: IntExpr): TPRef = TPRef(id, Add(delay, Minus(d)))
def -(d: Int): TPRef = this - IntExpr(d)
def <=(other: TPRef): TBefore = TBefore(this, other)
def <(other: TPRef): TBefore = TBefore(this, other - 1)
def >=(other: TPRef): TBefore = other <= this
def >(other: TPRef): TBefore = other < this
def ===(other: TPRef): Seq[TBefore] = Seq(this <= other, this >= other)
}
case class TBefore(from: TPRef, to: TPRef) extends Statement {
override def toString: String = s"$from <= $to"
}
final case class ActionTemplate(scope: InnerScope, content: Seq[InActionBlock])
extends InModuleBlock {
def name: String = scope.name
......@@ -191,15 +149,15 @@ package object core {
override def toString: String =
s"action $name(${args.map(a => s"${a.typ} ${a.id.name}").mkString(", ")})"
lazy val start: TPRef = content
lazy val start: LocalVar = content
.collectFirst {
case TimepointDeclaration(tp) if tp.id == Id(scope, "start") => TPRef(tp)
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), Type.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: TPRef = content
lazy val end: LocalVar = content
.collectFirst {
case TimepointDeclaration(tp) if tp.id == Id(scope, "end") => TPRef(tp)
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), Type.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
......@@ -212,15 +170,15 @@ package object core {
def name: String = scope.name
val args: Seq[Arg] = content.collect { case ArgDeclaration(a) => a }
lazy val start: TPRef = content
lazy val start: LocalVar = content
.collectFirst {
case TimepointDeclaration(tp) if tp.id == Id(scope, "start") => TPRef(tp)
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), Type.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: TPRef = content
lazy val end: LocalVar = content
.collectFirst {
case TimepointDeclaration(tp) if tp.id == Id(scope, "end") => TPRef(tp)
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), Type.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
}
......
......@@ -13,9 +13,10 @@ package object full {
sealed trait Declaration[T] {
def id: Id
}
case class TimepointDeclaration(tp: Timepoint) extends Declaration[Timepoint] with Statement {
override def id: Id = tp.id
override def toString: String = s"timepoint $id"
object TimepointDeclaration {
def apply(id: Id): LocalVarDeclaration =
LocalVarDeclaration(LocalVar(id, Type.Time))
}
case class TypeDeclaration(typ: Type) extends Declaration[Type] with InModuleBlock {
......@@ -75,7 +76,7 @@ package object full {
case class UnaryExprTree(op: UnaryOperator, lhs: StaticExpr) extends ExprTree {
override val typ: Type = op.tpe(lhs.typ) match {
case Right(tpe) => tpe
case Left(err) => sys.error(err)
case Left(err) => sys.error(err)
}
override def toString: String = s"(${op.op} $lhs)"
......@@ -98,65 +99,12 @@ package object full {
override def toString: String = term.toString
}
sealed trait IntExpr
object IntExpr {
def apply(lit: Int): IntExpr = GenIntExpr(ConstantExpr(IntLiteral(lit)))
}
/** A timepoint, declared when appearing in the root of a context.*/
case class TPRef(id: Timepoint, delay: IntExpr = IntExpr(0)) {
override def toString: String =
id.toString + (delay match {
case GenIntExpr(ConstantExpr(IntLiteral(d))) =>
if(d == 0) ""
else if(d > 0) s"+$d"
else s"-${-d}"
case x => s"+$x"
})
def +(d: IntExpr): TPRef = TPRef(id, Add(delay, d))
def +(d: Int): TPRef = this + IntExpr(d)
def -(d: IntExpr): TPRef = TPRef(id, Add(delay, Minus(d)))
def -(d: Int): TPRef = this - IntExpr(d)
def <=(other: TPRef): TBefore = TBefore(this, other)
def <(other: TPRef): TBefore = TBefore(this, other - 1)
def >=(other: TPRef): TBefore = other <= this
def >(other: TPRef): TBefore = other < this
def ===(other: TPRef): Seq[TBefore] = Seq(this <= other, this >= other)
def -(other: TPRef) = Delay(other, this)
}
case class GenIntExpr(e: StaticExpr) extends IntExpr {
require(e.typ.id.name == "integer")
override def toString: String = e.toString
}
case class Minus(e: IntExpr) extends IntExpr
case class Add(lhs: IntExpr, rhs: IntExpr) extends IntExpr
case class Mul(lhs: IntExpr, rhs: IntExpr) extends IntExpr
case class Div(lhs: IntExpr, rhs: IntExpr) extends IntExpr
case class Interval(start: TPRef, end: TPRef) {
case class Interval(start: StaticExpr, end: StaticExpr) {
require(start.typ.isSubtypeOf(Type.Time))
require(end.typ.isSubtypeOf(Type.Time))
override def toString: String = s"[$start, $end]"
}
case class TBefore(from: TPRef, to: TPRef) extends Statement {
override def toString: String = s"$from <= $to"
}
/*** Time ***/
case class Delay(from: TPRef, to: TPRef) {
def <=(dur: IntExpr): TBefore = to <= from + dur
def <(dur: IntExpr): TBefore = to < from + dur
def >=(dur: IntExpr): TBefore = to >= from + dur
def >(dur: IntExpr): TBefore = to > from + dur
def +(time: IntExpr): Delay = Delay(from, to + time)
def -(time: IntExpr): Delay = Delay(from, to - time)
def ===(dur: IntExpr): Seq[TBefore] = Seq(this <= dur, this >= dur)
}
/** A block wrapping other blocks pertaining to the same scope. */
sealed trait Wrapper extends Block {
def wrapped: Seq[Block]
......@@ -165,12 +113,12 @@ package object full {
abstract class TimedAssertion(parent: Option[Ctx], name: String) extends Ctx with Block {
override val scope: InnerScope = parent.map(_.scope).getOrElse(RootScope) + name
val start: Timepoint = Timepoint(this.id("start"))
val end: Timepoint = Timepoint(this.id("end"))
val start: LocalVar = Timepoint(this.id("start"))
val end: LocalVar = Timepoint(this.id("end"))
override val store: BlockStore[Statement] = new BlockStore[Statement]() +
TimepointDeclaration(start) +
TimepointDeclaration(end)
LocalVarDeclaration(start) +
LocalVarDeclaration(end)
}
case class TimedEqualAssertion(left: TimedExpr, // TODO: should not restrict this to be symbolic
right: StaticExpr,
......@@ -366,10 +314,10 @@ package object full {
case _ => None
}
def findTimepoint(name: String): Option[Timepoint] =
def findTimepoint(name: String): Option[LocalVar] =
findDeclaration(name).flatMap {
case decl: TimepointDeclaration => Some(decl.tp)
case _ => None
case LocalVarDeclaration(v @ LocalVar(_, tpe)) if tpe.isSubtypeOf(Type.Time) => Some(v)
case _ => None
}
def findType(name: String): Option[Type] =
......
......@@ -10,32 +10,32 @@ object ActionInstantiation {
type Up[T] = Trans.Aux[Id, Id, T, T]
def instance[T](implicit ev: Up[T]): Up[T] = ev
// landscaper has problem with the new ADT, provide some help
implicit val x3 = instance[IntExpr]
implicit val x4 = instance[TPRef]
implicit val x5 = instance[TBefore] // ok
implicit val x6 = instance[StaticAssertion] //ok
implicit val x7 = instance[ArgDeclaration] //ok
implicit val x8 = instance[TimedAssignmentAssertion] //ok
implicit val x9 = instance[TimedEqualAssertion] //ok
implicit val x10 = instance[TimedTransitionAssertion] //ok
implicit val x11 = instance[TimedAssertion] //ok
implicit val x12 = instance[LocalVarDeclaration] //ok
implicit val x13 = instance[TimepointDeclaration] //ok
// derivation of Trans[Id,Id,InActionBlock] never ends for an obscure reason, dispatch manually
implicit val main: Up[InActionBlock] = new Trans[Id, Id, InActionBlock] {
override type Result = InActionBlock
override def rewrite(f: Id => Id, in: InActionBlock): Result = in match {
case x: TimedAssertion => x11.rewrite(f, x)
case x: StaticAssertion => x6.rewrite(f, x)
case x: TBefore => x5.rewrite(f, x)
case x: ArgDeclaration => x7.rewrite(f, x)
case x: LocalVarDeclaration => x12.rewrite(f, x)
case x: TimepointDeclaration => x13.rewrite(f, x)
}
}
// // landscaper has problem with the new ADT, provide some help
// implicit val x3 = instance[IntExpr]
// implicit val x4 = instance[TPRef]
// implicit val x5 = instance[TBefore] // ok
// implicit val x6 = instance[StaticAssertion] //ok
// implicit val x7 = instance[ArgDeclaration] //ok
// implicit val x8 = instance[TimedAssignmentAssertion] //ok
// implicit val x9 = instance[TimedEqualAssertion] //ok
// implicit val x10 = instance[TimedTransitionAssertion] //ok
// implicit val x11 = instance[TimedAssertion] //ok
// implicit val x12 = instance[LocalVarDeclaration] //ok
// implicit val x13 = instance[TimepointDeclaration] //ok
//
// // derivation of Trans[Id,Id,InActionBlock] never ends for an obscure reason, dispatch manually
// implicit val main: Up[InActionBlock] = new Trans[Id, Id, InActionBlock] {
// override type Result = InActionBlock
//
// override def rewrite(f: Id => Id, in: InActionBlock): Result = in match {
// case x: TimedAssertion => x11.rewrite(f, x)
// case x: StaticAssertion => x6.rewrite(f, x)
// case x: TBefore => x5.rewrite(f, x)
// case x: ArgDeclaration => x7.rewrite(f, x)
// case x: LocalVarDeclaration => x12.rewrite(f, x)
// case x: TimepointDeclaration => x13.rewrite(f, x)
// }
// }
}
/** Builds a new action instance with the given name*/
......@@ -53,8 +53,8 @@ object ActionInstantiation {
}
//
val instanceContent = template.content.map(s => implicits.main.rewrite(trans, s))
Action(instanceScope, instanceContent, template)
???
// val instanceContent = template.content.map(s => implicits.main.rewrite(trans, s))
// Action(instanceScope, instanceContent, template)
}
}
......@@ -8,7 +8,14 @@ object FullToCore {
private object ImplicitConversions {
import scala.language.implicitConversions
implicit def absolute2relativeTimepoint(tp: Timepoint): core.TPRef = core.TPRef(tp)
implicit class ExprOps(private val lhs: Expr) extends AnyVal {
def ===(rhs: Expr): Expr = Op2(operators.Eq, lhs, rhs)
def <=(rhs: Expr): Expr = Op2(operators.LEQ, lhs, rhs)
def <(rhs: Expr): Expr = Op2(operators.LT, lhs, rhs)
def toStatement: core.Statement = core.StaticBooleanAssertion(lhs)
}
}
import ImplicitConversions._
......@@ -42,42 +49,6 @@ object FullToCore {
}
}
private def f2c(expr: full.IntExpr)(implicit ctx: Context): CoreM[core.IntExpr] =
expr match {
case full.GenIntExpr(e) =>
for {
v <- f2c(e)
} yield core.IntTerm(v)
case full.Minus(e) =>
for {
ce <- f2c(e)
} yield core.Minus(ce)
case full.Add(lhs, rhs) =>
for {
el <- f2c(lhs)
er <- f2c(rhs)
} yield core.Add(el, er)
case full.Mul(lhs, rhs) =>
for {
el <- f2c(lhs)
er <- f2c(rhs)
} yield core.Mul(el, er)
case full.Div(lhs, rhs) =>
for {
el <- f2c(lhs)
er <- f2c(rhs)
} yield core.Div(el, er)
}
private def f2c(tp: full.TPRef)(implicit ctx: Context): CoreM[core.TPRef] =
for {
de <- f2c(tp.delay)
} yield core.TPRef(tp.id, de)
private def f2c(exprs: List[full.StaticExpr])(implicit ctx: Context): CoreM[List[Term]] = {
exprs match {
case Nil => CoreM.pure(Nil)
......@@ -135,7 +106,7 @@ object FullToCore {
} yield ()
case full.TemporallyQualifiedAssertion(qualifier, assertion) =>
val startEnd: CoreM[(core.TPRef, core.TPRef)] =
val startEnd: CoreM[(Term, Term)] =
qualifier match {
case full.Equals(interval)
if ctx.config.mergeTimepoints && assertion.name.startsWith(reservedPrefix) =>
......@@ -149,10 +120,10 @@ object FullToCore {
for {
itvStart <- f2c(interval.start)
itvEnd <- f2c(interval.end)
_ <- CoreM.unit(core.TimepointDeclaration(assertion.start),
core.TimepointDeclaration(assertion.end))
_ <- CoreM.unit(itvStart === assertion.start: _*)
_ <- CoreM.unit(assertion.end === itvEnd: _*)
_ <- CoreM.unit(core.LocalVarDeclaration(assertion.start),
core.LocalVarDeclaration(assertion.end))
_ <- CoreM.unit(core.StaticBooleanAssertion(itvStart === assertion.start))
_ <- CoreM.unit(core.StaticBooleanAssertion(assertion.end === itvEnd))
} yield (assertion.start, assertion.end)
case full.Contains(interval) =>
......@@ -160,10 +131,10 @@ object FullToCore {
itvStart <- f2c(interval.start)
itvEnd <- f2c(interval.end)
_ <- CoreM.unit(
core.TimepointDeclaration(assertion.start),
core.TimepointDeclaration(assertion.end),
itvStart <= assertion.start,
assertion.end <= itvEnd
core.LocalVarDeclaration(assertion.start),
core.LocalVarDeclaration(assertion.end),
core.StaticBooleanAssertion(itvStart <= assertion.start),
core.StaticBooleanAssertion(assertion.end <= itvEnd)
)
} yield (assertion.start, assertion.end)
}
......@@ -175,7 +146,7 @@ object FullToCore {
coreFluent <- f2c(fluent)
coreValue <- f2c(value)
_ <- CoreM.unit(core.TimedEqualAssertion(start, end, coreFluent, coreValue),
start <= end)
core.StaticBooleanAssertion(start <= end))
} yield ()
case full.TimedAssignmentAssertion(fluent, value, _, _) =>
......@@ -185,7 +156,7 @@ object FullToCore {
coreFluent <- f2c(fluent)
coreValue <- f2c(value)
_ <- CoreM.unit(core.TimedAssignmentAssertion(start, end, coreFluent, coreValue),
start <= end)
core.StaticBooleanAssertion(start <= end))
} yield ()
case full.TimedTransitionAssertion(fluent, fromValue, toValue, _, _) =>
......@@ -196,20 +167,10 @@ object FullToCore {
coreFrom <- f2c(fromValue)
coreTo <- f2c(toValue)
_ <- CoreM.unit(core.TimedTransitionAssertion(start, end, coreFluent, coreFrom, coreTo),
start < end)
core.StaticBooleanAssertion(start < end))
} yield ()
}
case full.TBefore(from, to) =>
for {
f <- f2c(from)
t <- f2c(to)
_ <- CoreM.unit(
core.TBefore(f, t)
)
} yield ()
case full.TimepointDeclaration(tp) => CoreM.unit(core.TimepointDeclaration(tp))
case full.LocalVarDeclaration(v) => CoreM.unit(core.LocalVarDeclaration(v))
}
......
......@@ -75,6 +75,7 @@ object InputAnmlModels {
"constant boolean isTrue(integer x); isTrue(1) := false;",
"duration == 10 * 4 + 2;",
"constant integer i; duration == 10 * i + 2;",
"constant boolean x; x implies 10 > 4;"
)
val invalid = Seq(
......@@ -99,7 +100,6 @@ object InputAnmlModels {
"type T; constant boolean f; constant T g; f == g;",
"type T; constant boolean f(T t); f(true) == true;",
"start < x;",
"timepoint t; start - end < t;",
"type A; type B; fluent A f(A a); instance A a1; instance B b1; [start,end] f(a1) == b1;",
"type A; type B; fluent A f(B b); instance A a1; instance B b1; [start,end] id: f(b1) == a2;",
"type A; type B; fluent A f(B b); instance A a1; instance B b1; [start,end] id: f(b1) == a1 :-> b1;",
......
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