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

Reorganize anml parser code.

parent 6e05b5cc
package copla.lang
import copla.lang.model.common._
import copla.lang.model.core._
import scala.collection.mutable
......
package copla.lang.model
import copla.lang.model
package object common {
case class Id(scope: Scope, name: String) {
override def toString: String = scope.toScopedString(name)
def toTPId: Timepoint = new Timepoint(this)
}
case class Timepoint(id: Id) {
override def toString: String = id.toString
}
sealed trait Scope {
def +(nestedScope: String): InnerScope = InnerScope(this, nestedScope)
def makeNewId(): Id = Id(this, model.defaultId())
def toScopedString(name: String): String
}
object RootScope extends Scope {
override def toString: String = "root"
def toScopedString(name: String): String = name
}
case class InnerScope(parent: Scope, name: String) extends Scope {
override def toString: String = parent match {
case RootScope => name
case nonScope => s"$nonScope.$name"
}
def toScopedString(name: String): String = s"$this.$name"
}
case class Type(id: Id, parent: Option[Type]) {
def isSubtypeOf(typ: Type): Boolean =
this == typ || parent.exists(t => t == typ || t.isSubtypeOf(typ))
def overlaps(typ: Type): Boolean = this.isSubtypeOf(typ) || typ.isSubtypeOf(this)
def asScope: Scope = id.scope + id.name
override def toString: String = id.toString
}
object Type {
val Integers = Type(Id(RootScope, "integer"), None)
}
sealed trait Term {
def id: Id
def typ: Type
}
object Term {
def unapply(v: Term) = Option((v.id, v.typ))
}
sealed trait Cst extends Term
sealed trait Var extends Term
case class IntLiteral(value: Int) extends Cst {
override def typ: Type = Type.Integers
override def id: Id = Id(RootScope + "_integers_", value.toString)
}
/** Variable declared locally */
case class LocalVar(id: Id, typ: Type) extends Var {
override def toString: String = id.toString
}
/** Instance of a given type, result of the ANML statement "instance Type id;" */
case class Instance(id: Id, typ: Type) extends Cst {
override def toString: String = id.toString
}
/** Denote the argument of the template of state variables and actions. */
case class Arg(id: Id, typ: Type) extends Var {
override def toString: String = id.toString
}
sealed trait FunctionTemplate {
def id: Id
def typ: Type
def params: Seq[Arg]
}
case class FluentTemplate(id: Id, typ: Type, params: Seq[Arg]) extends FunctionTemplate {
override def toString: String = id.toString
}
case class ConstantTemplate(id: Id, typ: Type, params: Seq[Arg]) extends FunctionTemplate {
override def toString: String = id.toString
}
}
......@@ -21,7 +21,7 @@ object Formatter extends LowPriorityFormatter {
def apply[T](implicit fmt: Formatter[T]): Formatter[T] = fmt
implicit def fAction(implicit ev: Formatter[Statement]) = new Formatter[ActionTemplate] {
implicit def fAction(implicit ev: Formatter[InActionBlock]) = new Formatter[ActionTemplate] {
override def format(t: ActionTemplate, indent: Int): String = {
val sb = new StringBuilder()
sb ++= "\n" + " " * indent + t.toString + ":"
......
package copla.lang
import copla.lang.model.core.{InnerScope, RootScope, SimpleTPRef}
import copla.lang.parsing.anml.Parser
package object model {
val reservedPrefix = "__"
......
......@@ -2,10 +2,16 @@ package copla.lang.model.transforms
import copla.lang.model
import copla.lang.model._
import copla.lang.model.full.Scope
import copla.lang.model.common._
object FullToCore {
private object ImplicitConversions {
import scala.language.implicitConversions
implicit def absolute2relativeTimepoint(tp: Timepoint): core.TPRef = core.TPRef(tp)
}
import ImplicitConversions._
case class Context(scope: Scope, config: Config = Config())
/** Monad that represent an expression of type A that is subject to the associated statements to restrict its values. */
......@@ -21,23 +27,23 @@ object FullToCore {
def unit(statements: core.Statement*): CoreM[Unit] = CoreM((), statements)
}
private def f2c(expr: full.StaticExpr)(implicit ctx: Context): CoreM[core.Var] = {
private def f2c(expr: full.StaticExpr)(implicit ctx: Context): CoreM[Term] = {
expr match {
case x: core.Var => CoreM.pure(x)
case x: full.Constant =>
case full.ConstantExpr(cst) => CoreM.pure(cst)
case full.Variable(v) => CoreM.pure(v)
case full.Constant(template, params) =>
for {
params <- f2c(x.params.toList)
cst = core.Constant(x.template, params)
variable = core.LocalVar(ctx.scope.makeNewId(), cst.typ)
params <- f2c(params.toList)
cst = core.Constant(template, params)
variable = LocalVar(ctx.scope.makeNewId(), cst.typ)
_ <- CoreM.unit(core.LocalVarDeclaration(variable))
_ <- CoreM.unit(core.BindAssertion(cst, variable))
} yield variable
}
}
private def f2c(e: full.IntExpr)(implicit ctx: Context): CoreM[core.IntExpr] =
e match {
case x: core.IntExpr => CoreM.pure(x)
private def f2c(expr: full.IntExpr)(implicit ctx: Context): CoreM[core.IntExpr] =
expr match {
case full.GenIntExpr(e) =>
for {
v <- f2c(e)
......@@ -56,15 +62,11 @@ object FullToCore {
}
private def f2c(tp: full.TPRef)(implicit ctx: Context): CoreM[core.TPRef] =
tp match {
case x: core.TPRef => CoreM.pure(x)
case x: full.TPRef =>
for {
de <- f2c(x.delay)
} yield core.TPRef(x.id, de)
}
for {
de <- f2c(tp.delay)
} yield core.TPRef(tp.id, de)
private def f2c(exprs: List[full.StaticExpr])(implicit ctx: Context): CoreM[List[core.Var]] = {
private def f2c(exprs: List[full.StaticExpr])(implicit ctx: Context): CoreM[List[Term]] = {
exprs match {
case Nil => CoreM.pure(Nil)
case head :: tail =>
......@@ -75,7 +77,7 @@ object FullToCore {
}
}
private def f2c(expr: full.TimedSymExpr)(implicit ctx: Context): CoreM[core.Fluent] = {
private def f2c(expr: full.TimedExpr)(implicit ctx: Context): CoreM[core.Fluent] = {
expr match {
case fluent: full.Fluent =>
for {
......@@ -87,26 +89,24 @@ object FullToCore {
private def f2c(act: full.ActionTemplate)(implicit ctx: Context): core.ActionTemplate = {
implicit val actionContext: Context = ctx.copy(scope = act.scope)
val statements = act.store.blocks.flatMap {
case x: core.Statement => Seq(x)
case x: full.Statement => f2c(x)(actionContext).statements
case full.ArgDeclaration(arg) => Seq(core.ArgDeclaration(arg))
case x: full.Statement => f2c(x)(actionContext).statements
}
core.ActionTemplate(act.scope, statements)
}
private def f2c(block: full.Statement)(implicit ctx: Context): CoreM[Unit] = block match {
case x: core.Statement => CoreM.unit(x)
case x: full.StaticAssignmentAssertion =>
(x.left, x.right) match {
case (cst: full.Constant, inst: core.Term)
if cst.params.forall(_.isInstanceOf[core.Term]) =>
val boundCst =
new model.core.BoundConstant(cst.template, cst.params.map(_.asInstanceOf[core.Term]))
CoreM.unit(core.StaticAssignmentAssertion(boundCst, inst))
case _ =>
throw new UnsupportedOperationException(
s"Assignment assertions on constant functions are only supported when all parameters are declared instances: $block")
}
case full.StaticAssignmentAssertion(lhs: full.Constant, full.ConstantExpr(rhs))
if lhs.params.forall(_.isInstanceOf[full.ConstantExpr]) =>
val boundCst =
new model.core.BoundConstant(lhs.template, lhs.params.map {
case full.ConstantExpr(x) => x
case _ => throw new RuntimeException("impossible")
})
CoreM.unit(core.StaticAssignmentAssertion(boundCst, rhs))
case full.StaticAssignmentAssertion(_, _) =>
throw new UnsupportedOperationException(
s"Assignment assertions on constant functions are only supported when all parameters are declared instances: $block")
case x: full.StaticEqualAssertion =>
for {
......@@ -196,13 +196,18 @@ object FullToCore {
core.TBefore(f, t)
)
} yield ()
case full.TimepointDeclaration(tp) => CoreM.unit(core.TimepointDeclaration(tp))
case full.LocalVarDeclaration(v) => CoreM.unit(core.LocalVarDeclaration(v))
}
def trans(model: full.Model, config: Config = Config()): Seq[core.InModuleBlock] = {
model.store.blocks.flatMap {
case x: core.InModuleBlock => Seq(x)
case x: full.Statement => f2c(x)(Context(model.scope, config)).statements
case x: full.ActionTemplate => Seq(f2c(x)(Context(model.scope, config)))
case full.FunctionDeclaration(x) => Seq(core.FunctionDeclaration(x))
case full.InstanceDeclaration(x) => Seq(core.InstanceDeclaration(x))
case full.TypeDeclaration(x) => Seq(core.TypeDeclaration(x))
case x: full.Statement => f2c(x)(Context(model.scope, config)).statements
case x: full.ActionTemplate => Seq(f2c(x)(Context(model.scope, config)))
}
}
......
......@@ -3,6 +3,7 @@ package copla
import java.io.File
import copla.lang.model.core.CoreModel
import copla.lang.model.transforms.FullToCore
import copla.lang.model.{core, full}
import copla.lang.parsing.anml
......@@ -24,10 +25,10 @@ package object lang {
}
def parse(anml: String): Result[core.CoreModel] =
parseToFull(anml).map(_.asCore())
parseToFull(anml).map(FullToCore.trans(_))
def parse(anml: File): Result[CoreModel] =
parseToFull(anml).map(_.asCore())
parseToFull(anml).map(FullToCore.trans(_))
def parseToFull(anmlString: String): Result[full.Model] = {
anml.Parser.parse(anmlString) match {
......
......@@ -7,8 +7,8 @@ import ParserApi.baseApi._
import ParserApi.baseApi.Parsed.Success
import ParserApi.whiteApi._
import ParserApi.extendedApi._
import copla.lang.model.core.SimpleTPRef
import fastparse.core.Parsed.Failure
import copla.lang.model.common._
import copla.lang.model.full._
import scala.util.Try
......@@ -64,15 +64,15 @@ abstract class AnmlParser(val initialContext: Ctx) {
val timepointDeclaration: Parser[TimepointDeclaration] =
timepointKW ~/
freeIdent.map(name => new TimepointDeclaration(SimpleTPRef(ctx.id(name).toTPId))) ~
freeIdent.map(name => TimepointDeclaration(Timepoint(ctx.id(name)))) ~
";"
protected val definedTP: Parser[TPRef] =
protected val definedTP: Parser[Timepoint] =
ident.optGet(ctx.findTimepoint(_), "declared-timepoint")
val timepoint: Parser[TPRef] = {
(int ~ "+").flatMap(d => timepoint.map(tp => tp + d)) |
(definedTP ~ (("+" | "-").! ~ int).?).map {
(definedTP.map(TPRef(_)) ~ (("+" | "-").! ~ int).?).map {
case (tp, Some(("+", delay))) => tp + delay
case (tp, Some(("-", delay))) => tp - delay
case (tp, None) => tp
......@@ -81,7 +81,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
int.flatMap(
i => // integer as a tp defined relatively to the global start, if one exists
ctx.root.findTimepoint("start") match {
case Some(st) => PassWith(st + i)
case Some(st) => PassWith(TPRef(st) + i)
case None => Fail.opaque("fail: no start timepoint in top level scope")
})
}.opaque("timepoint")
......@@ -92,12 +92,12 @@ abstract class AnmlParser(val initialContext: Ctx) {
_ =>
ctx
.findTimepoint("start")
.flatMap(st => ctx.findTimepoint("end").map(ed => (st, ed))) match {
case Some((st, ed)) => PassWith(new Delay(st, ed))
.flatMap(st => ctx.findTimepoint("end").map(ed => (TPRef(st), TPRef(ed)))) match {
case Some((st, ed)) => PassWith(Delay(st, ed))
case None => sys.error("No start/end timepoint")
})
.opaque("duration") |
(timepoint ~ "-" ~ definedTP ~ (("+" | "-").! ~ intExpr).?).map {
(timepoint ~ "-" ~ definedTP.map(TPRef(_)) ~ (("+" | "-").! ~ intExpr).?).map {
case (t1, t2, None) => t1 - t2
case (t1, t2, Some(("+", i))) => (t1 - t2) + i
case (t1, t2, Some(("-", i))) => (t1 - t2) - i
......@@ -125,7 +125,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
}
}
val variable: Parser[Var] =
val variable: Parser[Term] =
ident.optGet(ctx.findVariable(_), "declared-variable")
val fluent: Parser[FluentTemplate] =
......@@ -137,7 +137,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
/** Parses a fluent in the object oriented notation.
* "x.f" where x is a variable of type T and f is a fluent declared in type T or in a supertype of T.
* Returns the fluent T.f and x which is to be the first argument of T.f */
val partiallyAppliedFunction: Parser[(FunctionTemplate, Var)] = {
val partiallyAppliedFunction: Parser[(FunctionTemplate, Term)] = {
/** Retrieves a fluent template declared the the given type or one of its super types.*/
def findInTypeFunction(typ: Type, fluentName: String): Option[FunctionTemplate] =
......@@ -198,7 +198,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
PassWith(Seq()).opaque("no-args") // no args no, parenthesis
}
val timedSymExpr: Parser[TimedSymExpr] = {
val timedSymExpr: Parser[TimedExpr] = {
val partiallyAppliedFluent = partiallyAppliedFunction
.namedFilter(_._1.isInstanceOf[FluentTemplate], "is-fluent")
.map(tup => (tup._1.asInstanceOf[FluentTemplate], tup._2))
......@@ -212,10 +212,11 @@ abstract class AnmlParser(val initialContext: Ctx) {
(partiallyAppliedFluent ~/ Pass).flatMap {
case (f, firstArg) =>
f.params.map(param => param.typ) match {
case Seq(singleParam) => (("(" ~/ ")") | Pass) ~ PassWith(new Fluent(f, Seq(firstArg)))
case Seq(singleParam) =>
(("(" ~/ ")") | Pass) ~ PassWith(new Fluent(f, Seq(CommonTerm(firstArg))))
case paramTypes =>
"(" ~/ varList(paramTypes.tail, ",")
.map(args => new Fluent(f, firstArg +: args)) ~ ")" ~/ Pass
.map(args => new Fluent(f, CommonTerm(firstArg) +: args)) ~ ")" ~/ Pass
}
}
}
......@@ -225,24 +226,24 @@ abstract class AnmlParser(val initialContext: Ctx) {
.namedFilter(_._1.isInstanceOf[ConstantTemplate], "is-constant")
.map(tup => (tup._1.asInstanceOf[ConstantTemplate], tup._2))
variable |
variable.map(CommonTerm(_)) |
(constantFunc ~/ Pass).flatMap(f =>
f.params.map(param => param.typ) match {
case Seq() => (("(" ~/ ")") | Pass) ~ PassWith(new Constant(f, Seq()))
case Seq() => (("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq()))
case paramTypes =>
"(" ~/ varList(paramTypes, ",").map(args => new Constant(f, args)) ~ ")" ~/ Pass
"(" ~/ 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(new Constant(f, Seq(firstArg)))
(("(" ~/ ")") | Pass) ~ PassWith(Constant(f, Seq(CommonTerm(firstArg))))
case paramTypes =>
"(" ~/ varList(paramTypes.tail, ",")
.map(args => new Constant(f, firstArg +: args)) ~ ")" ~/ Pass
.map(args => Constant(f, CommonTerm(firstArg) +: args)) ~ ")" ~/ Pass
}
} |
int.map(i => core.IntLiteral(i))
int.map(i => CommonTerm(IntLiteral(i)))
}
val intExpr: Parser[IntExpr] =
......@@ -259,18 +260,18 @@ abstract class AnmlParser(val initialContext: Ctx) {
} |
P("all").map(_ => {
(ctx.findTimepoint("start"), ctx.findTimepoint("end")) match {
case (Some(st), Some(ed)) => (st, ed)
case (Some(st), Some(ed)) => (TPRef(st), TPRef(ed))
case _ => sys.error("Start and/or end timepoints are not defined.")
}
})) ~
"]").map {
case (tp1, tp2) => new Interval(tp1, tp2)
case (tp1, tp2) => Interval(tp1, tp2)
}
val timedAssertion: Parser[TimedAssertion] = {
// variable that hold the first two parsed token to facilitate type checking logic
var id: String = null
var fluent: TimedSymExpr = null
var fluent: TimedExpr = null
def compatibleTypes(t1: Type, t2: Type): Boolean = t1.isSubtypeOf(t2) || t2.isSubtypeOf(t1)
......@@ -318,10 +319,10 @@ abstract class AnmlParser(val initialContext: Ctx) {
case (expr, None) => expr.typ.id.name == "boolean"
}, "boolean-if-no-right-side")
.map {
case (left, Some(("==", right))) => new StaticEqualAssertion(left, right)
case (left, Some(("!=", right))) => new StaticDifferentAssertion(left, right)
case (left, Some((":=", right))) => new StaticAssignmentAssertion(left, right)
case (expr, None) => new StaticEqualAssertion(expr, ctx.findVariable("true").get)
case (left, Some(("==", right))) => StaticEqualAssertion(left, right)
case (left, Some(("!=", right))) => StaticDifferentAssertion(left, right)
case (left, Some((":=", right))) => StaticAssignmentAssertion(left, right)
case (expr, None) => StaticEqualAssertion(expr, CommonTerm(ctx.findVariable("true").get))
case _ => sys.error("Something is wrong with this parser.")
}
}
......@@ -453,15 +454,15 @@ class AnmlActionParser(superParser: AnmlModuleParser) extends AnmlParser(superPa
}
val emptyAct = new ActionTemplate(actionName, container)
emptyAct +
new TimepointDeclaration(SimpleTPRef(new Id(emptyAct.scope, "start").toTPId)) +
new TimepointDeclaration(SimpleTPRef(new Id(emptyAct.scope, "end").toTPId))
TimepointDeclaration(Timepoint(Id(emptyAct.scope, "start"))) +
TimepointDeclaration(Timepoint(Id(emptyAct.scope, "end")))
}
/** FIXME: this interprets a "constant" as a local variable. This is is compatible with FAPE but not with official ANML. */
val variableDeclaration: Parser[LocalVarDeclaration] = {
(constantKW ~/ declaredType ~/ freeIdent ~/ ";").map {
case (typ, id) =>
new LocalVarDeclaration(new LocalVar(new Id(ctx.scope, id), typ))
LocalVarDeclaration(LocalVar(Id(ctx.scope, id), typ))
}
}
......@@ -476,7 +477,7 @@ class AnmlActionParser(superParser: AnmlModuleParser) extends AnmlParser(superPa
}) ~/
argList // parse arguments and update the current action
.map(_.map {
case (name, typ) => new ArgDeclaration(new Arg(new Id(ctx.scope, name), typ))
case (name, typ) => ArgDeclaration(Arg(Id(ctx.scope, name), typ))
})
.sideEffect(argDeclarations => updateContext(currentAction ++ argDeclarations)) ~
"{" ~/
......
package dahu.planner
import copla.lang.model.common._
import copla.lang.model.core._
import dahu.model.input.{Ident, Input, Tentative}
......
package dahu.planner
import copla.lang.model.core
import copla.lang.model.common
import copla.lang.model.common.{Cst => _, Term => _, _}
import copla.lang.model.core._
import copla.lang.model.core
import dahu.model.functions.WrappedFunction
import dahu.model.input._
import dahu.model.input.dsl._
......@@ -38,7 +40,7 @@ case class ProblemContext(intTag: BoxedInt[Literal],
topTag: TagIsoInt[Literal],
specializedTags: Type => TagIsoInt[Literal]) {
def encode(v: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Literal] =
def encode(v: common.Term)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Literal] =
v match {
case IntLiteral(i) => IntLit(i).asConstant(intTag)
case lv @ LocalVar(_, tpe) => Input[Literal](Ident(lv))(specializedTags(tpe))
......@@ -81,7 +83,8 @@ case class ProblemContext(intTag: BoxedInt[Literal],
def encode(orig: core.Constant)(implicit argRewrite: Arg => Tentative[Literal]): Fluent =
Fluent(orig.template, orig.params.map(p => encode(p)(argRewrite)))
def eqv(lhs: Var, rhs: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
def eqv(lhs: common.Term, rhs: common.Term)(
implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
eqv(encode(lhs), encode(rhs))
private val ObjEquality = WrappedFunction.wrap(int.EQ)(topTag, implicitly[TagIsoInt[Boolean]])
......@@ -110,7 +113,8 @@ case class ProblemContext(intTag: BoxedInt[Literal],
}
}
def neq(lhs: Var, rhs: Var)(implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
def neq(lhs: common.Term, rhs: common.Term)(
implicit argRewrite: Arg => Tentative[Literal]): Tentative[Boolean] =
neq(encode(lhs), encode(rhs))
def neq(lhs: Tentative[Literal], rhs: Tentative[Literal]): Tentative[Boolean] =
not(eqv(lhs, rhs))
......@@ -291,80 +295,81 @@ case class Chronicle(ctx: ProblemContext,
import ctx._
def extended(e: Statement)(implicit argRewrite: Arg => Tentative[Literal]): Chronicle = e match {
case _: TypeDeclaration => this
case _: InstanceDeclaration => this
case _: TimepointDeclaration => this
case _: FunctionDeclaration => this
case _: LocalVarDeclaration => this
case _: ArgDeclaration => this
case BindAssertion(c, v) =>
val cond = ConditionToken(
start = ctx.temporalOrigin,
end = ctx.temporalHorizon,
fluent = encode(c),
value = encode(v)
)
copy(
conditions = cond :: conditions
)
case StaticDifferentAssertion(lhs, rhs) =>
copy(
constraints = ctx.neq(lhs, rhs) :: constraints
)
case StaticEqualAssertion(lhs, rhs) =>
copy(constraints = ctx.eqv(lhs, rhs) :: constraints)
case TBefore(lhs, rhs) =>
copy(constraints = (encode(lhs) <= encode(rhs)) :: constraints)
case TimedAssignmentAssertion(start, end, fluent, value) =>
val changeStart = encode(start)
val changeEnd = encode(end).subjectTo(changeStart <= _)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
val token = EffectToken(
changeStart = changeStart,
changeEnd = changeEnd,
persistenceEnd = persistenceEnd,
fluent = encode(fluent),
value = encode(value)
)
copy(effects = token :: effects)
case TimedEqualAssertion(s, e, f, v) =>
val start = encode(s)
val end = encode(e)
val token = ConditionToken(
start = start,
end = end,
fluent = encode(f),
value = encode(v)
)
copy(conditions = token :: conditions)
case TimedTransitionAssertion(s, e, f, v1, v2) =>
val start = encode(s)
val changeStart = start + 1
val changeEnd = encode(e).subjectTo(changeStart <= _)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
val cond = ConditionToken(start, start, encode(f), encode(v1))
val eff = EffectToken(changeStart, changeEnd, persistenceEnd, encode(f), encode(v2))
copy(
conditions = cond :: conditions,
effects = eff :: effects
)
case StaticAssignmentAssertion(lhs, rhs) =>
val eff = EffectToken(
changeStart = ctx.temporalOrigin,
changeEnd = ctx.temporalOrigin,
persistenceEnd = ctx.temporalHorizon,
fluent = encode(lhs),
value = encode(rhs)
)
copy(
effects = eff :: effects
)
}
def extended(e: InActionBlock)(implicit argRewrite: Arg => Tentative[Literal]): Chronicle =
e match {
case _: TypeDeclaration => this
case _: InstanceDeclaration => this
case _: TimepointDeclaration => this
case _: FunctionDeclaration => this
case _: LocalVarDeclaration => this
case _: ArgDeclaration => this
case BindAssertion(c, v) =>
val cond = ConditionToken(
start = ctx.temporalOrigin,
end = ctx.temporalHorizon,
fluent = encode(c),
value = encode(v)
)
copy(
conditions = cond :: conditions
)
case StaticDifferentAssertion(lhs, rhs) =>
copy(
constraints = ctx.neq(lhs, rhs) :: constraints
)
case StaticEqualAssertion(lhs, rhs) =>
copy(constraints = ctx.eqv(lhs, rhs) :: constraints)
case TBefore(lhs, rhs) =>
copy(constraints = (encode(lhs) <= encode(rhs)) :: constraints)
case TimedAssignmentAssertion(start, end, fluent, value) =>
val changeStart = encode(start)
val changeEnd = encode(end).subjectTo(changeStart <= _)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
val token = EffectToken(
changeStart = changeStart,
changeEnd = changeEnd,
persistenceEnd = persistenceEnd,
fluent = encode(fluent),
value = encode(value)
)
copy(effects = token :: effects)
case TimedEqualAssertion(s, e, f, v) =>
val start = encode(s)
val end = encode(e)
val token = ConditionToken(
start = start,
end = end,
fluent = encode(f),
value = encode(v)
)
copy(conditions = token :: conditions)
case TimedTransitionAssertion(s, e, f, v1, v2) =>
val start = encode(s)
val changeStart = start + 1
val changeEnd = encode(e).subjectTo(changeStart <= _)
val persistenceEnd = anonymousTp().subjectTo(changeEnd <= _)
val cond = ConditionToken(start, start, encode(f), encode(v1))
val eff = EffectToken(changeStart, changeEnd, persistenceEnd, encode(f), encode(v2))
copy(
conditions = cond :: conditions,
effects = eff :: effects
)
case StaticAssignmentAssertion(lhs, rhs) =>
val eff = EffectToken(
changeStart = ctx.temporalOrigin,
changeEnd = ctx.temporalOrigin,
persistenceEnd = ctx.