Commit 4fa7559b authored by Arthur Bit-Monnot's avatar Arthur Bit-Monnot

[planning] Allow the definition of custom predefined symbols.

parent 490d1a2a
......@@ -39,7 +39,7 @@ case class ObjLit(value: Instance) extends Literal {
case class ProblemContext(intTag: BoxedInt[Literal],
topTag: TagIsoInt[Literal],
specializedTags: Type => TagIsoInt[Literal]) {
specializedTags: Type => TagIsoInt[Literal])(implicit predef: Predef) {
def intBox(tpe: TagIsoInt[Literal], i: Tentative[Int]): Tentative[Literal] =
Computation(tpe.box, i)
......@@ -49,19 +49,19 @@ case class ProblemContext(intTag: BoxedInt[Literal],
case _ => unexpected
}
}
private val booleanTag = specializedTags(Type.Boolean)
private val booleanTag = specializedTags(predef.Boolean)
val boolBoxing = new Reversible[Boolean, Literal]()(Tag[Boolean], booleanTag) { self =>
override def reverse: Reversible[Literal, Boolean] =
new Reversible[Literal, Boolean]()(booleanTag, Tag[Boolean]) {
override def reverse: Reversible[Boolean, Literal] = self
override def of(in: Literal): Boolean = in match {
case ObjLit(Type.True) => true
case ObjLit(Type.False) => false
case _ => unexpected
case ObjLit(predef.True) => true
case ObjLit(predef.False) => false
case _ => unexpected
}
override def name: String = "unbox"
}
override def of(in: Boolean): Literal = if(in) ObjLit(Type.True) else ObjLit(Type.False)
override def of(in: Boolean): Literal = if(in) ObjLit(predef.True) else ObjLit(predef.False)
override def name: String = "box"
}
def boolUnbox(i: Tentative[Literal]): Tentative[Boolean] = Computation(boolBoxing.reverse, i)
......@@ -70,11 +70,11 @@ case class ProblemContext(intTag: BoxedInt[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(id, tpe) if tpe.isSubtypeOf(Type.Time) =>
assert(tpe == Type.Time)
val e: Tentative[Int] = id match {
case Type.Start => temporalOrigin
case Type.End => temporalHorizon
case lv @ LocalVar(id, tpe) if tpe.isSubtypeOf(predef.Time) =>
assert(tpe == predef.Time)
val e: Tentative[Int] = lv match {
case predef.Start => temporalOrigin
case predef.End => temporalHorizon
case _ =>
Input[Int](Ident(lv)).subjectTo(tp => temporalOrigin <= tp && tp <= temporalHorizon)
}
......
......@@ -2,13 +2,17 @@ package dahu
import java.io.File
import dahu.planning.model.common.Predef
import dahu.planning.model.core.CoreModel
import dahu.planning.model.transforms.FullToCore
import dahu.planning.model.{core, full}
import dahu.planning.parsing.anml
import dahu.planning.parsing.anml.AnmlPredef
package object planning {
implicit val predef = AnmlPredef
sealed trait Result[+T] {
def map[B](f: T => B): Result[B]
}
......
package dahu.planning.parsing.anml
import dahu.planning.model.common._
import dahu.planning.model.common.Type._
import dahu.planning.model.full
import dahu.planning.model.full._
object AnmlPredef extends dahu.planning.model.common.Predef {
override val Time: IRealType = IntSubType(Id(RootScope, "time"), Integers)
override val Boolean: BooleanType = BooleanType(Id(RootScope, "boolean"))
override val True: Instance = Instance(Id(RootScope, "true"), Boolean)
override val False: Instance = Instance(Id(RootScope, "false"), Boolean)
override val Start = LocalVar(Id(RootScope, "start"), Time)
override val End = LocalVar(Id(RootScope, "end"), Time)
override def baseModel: full.Model =
(Model() ++ Seq(
TypeDeclaration(ObjectTop),
TypeDeclaration(Boolean),
TypeDeclaration(Reals),
TypeDeclaration(Integers),
InstanceDeclaration(True),
InstanceDeclaration(False),
LocalVarDeclaration(Start),
LocalVarDeclaration(End),
)).getOrElse(sys.error("Could not instantiate base model"))
}
......@@ -22,7 +22,7 @@ import dahu.planning.model.full._
import scala.annotation.tailrec
import scala.util.Try
abstract class AnmlParser(val initialContext: Ctx) {
abstract class AnmlParser(val initialContext: Ctx)(implicit predef: Predef) {
/** Denotes the current context of this AnmlParser.
* It is used by many suparsers to find the variable/fluent/type associated to an identifier.
......@@ -73,7 +73,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
val timepointDeclaration: Parser[LocalVarDeclaration] =
timepointKW ~/
freeIdent.map(name => TimepointDeclaration(ctx.id(name))) ~
freeIdent.map(name => LocalVarDeclaration(Timepoint(ctx.id(name)))) ~
";"
protected val definedTP: Parser[LocalVar] =
......@@ -421,7 +421,7 @@ abstract class AnmlParser(val initialContext: Ctx) {
}, "assignment-to-const-func-only")
.namedFilter({
case (_, Some(_)) => true
case (expr, None) => expr.typ.isSubtypeOf(Type.Boolean)
case (expr, None) => expr.typ.isSubtypeOf(predef.Boolean)
}, "boolean-if-not-assignment")
.map {
case (left: Constant, Some((":=", right))) => StaticAssignmentAssertion(left, right)
......@@ -501,7 +501,7 @@ class AnmlModuleParser(val initialModel: Model) extends AnmlParser(initialModel)
case (_, _, None) => Seq()
case (t, _, Some(funcDecl)) =>
funcDecl.map(fd => {
val id = new Id(t.asScope, fd.id.name)
val id = Id(t.asScope, fd.id.name)
val functionScope = t.asScope + id.name
val selfArg = new Arg(new Id(functionScope, "self"), t)
val params = selfArg +: fd.func.params.map(arg =>
......@@ -541,7 +541,8 @@ class AnmlModuleParser(val initialModel: Model) extends AnmlParser(initialModel)
}
}
class AnmlActionParser(superParser: AnmlModuleParser) extends AnmlParser(superParser.currentModel) {
class AnmlActionParser(superParser: AnmlModuleParser)(implicit predef: Predef)
extends AnmlParser(superParser.currentModel) {
private def currentAction: ActionTemplate = ctx match {
case a: ActionTemplate => a
......@@ -556,8 +557,8 @@ class AnmlActionParser(superParser: AnmlModuleParser) extends AnmlParser(superPa
}
val emptyAct = new ActionTemplate(actionName, container)
emptyAct +
TimepointDeclaration(Id(emptyAct.scope, "start")) +
TimepointDeclaration(Id(emptyAct.scope, "end"))
LocalVarDeclaration(Timepoint(Id(emptyAct.scope, "start"))) +
LocalVarDeclaration(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. */
......@@ -594,7 +595,8 @@ class AnmlActionParser(superParser: AnmlModuleParser) extends AnmlParser(superPa
}
/** First phase parser used to extract all type declarations from a given ANML string. */
class AnmlTypeParser(val initialModel: Model) extends AnmlParser(initialModel) {
class AnmlTypeParser(val initialModel: Model)(implicit predef: Predef)
extends AnmlParser(initialModel) {
val nonTypeToken: Parser[String] =
(word | int | CharIn("{}[]();=:<>-+.,!/*")).!.namedFilter(_ != "type", "non-type-token")
......@@ -625,17 +627,7 @@ class AnmlTypeParser(val initialModel: Model) extends AnmlParser(initialModel) {
object Parser {
/** ANML model with default definitions already added */
val baseAnmlModel: Model =
(Model() ++ Seq(
TypeDeclaration(Type.ObjectTop),
TypeDeclaration(Type.Boolean),
TypeDeclaration(Type.Reals),
TypeDeclaration(Type.Integers),
InstanceDeclaration(Type.True),
InstanceDeclaration(Type.False),
TimepointDeclaration(Type.Start),
TimepointDeclaration(Type.End),
)).getOrElse(sys.error("Could not instantiate base model"))
def baseAnmlModel(implicit predef: Predef): Model = predef.baseModel
/** Parses an ANML string. If the previous model parameter is Some(m), then the result
* of parsing will be appended to m.
......
......@@ -29,22 +29,23 @@ object operators {
val precedence: Int,
val associativity: Associativity)
extends Operator {
def tpe(lhs: Type, rhs: Type): TypingResult
def tpe(lhs: Type, rhs: Type)(implicit predef: Predef): TypingResult
}
sealed abstract class BooleanBinaryOperator(op: String,
precedence: Int,
associativity: Associativity)
extends BinaryOperator(op, precedence, associativity) {
override def tpe(lhs: Type, rhs: Type): TypingResult = (lhs, rhs) match {
case (Type.Boolean, Type.Boolean) => Right(Type.Boolean)
case _ => Left("On of the subexpression does not have the boolean type.")
}
override def tpe(lhs: Type, rhs: Type)(implicit predef: Predef): TypingResult =
(lhs, rhs) match {
case (predef.Boolean, predef.Boolean) => Right(predef.Boolean)
case _ => Left("On of the subexpression does not have the boolean type.")
}
}
sealed abstract class NumericBinaryOperator(op: String, precedence: Int)
extends BinaryOperator(op, precedence, Associativity.Left) {
override def tpe(lhs: Type, rhs: Type): TypingResult = {
override def tpe(lhs: Type, rhs: Type)(implicit predef: Predef): TypingResult = {
lhs.lowestCommonAncestor(rhs) match {
case None if !lhs.isNum => Left(s"Left hand side is not a numeric type but: $lhs")
case None if !rhs.isNum => Left(s"Right hand side is not a numeric type but: $rhs")
......@@ -58,11 +59,11 @@ object operators {
sealed abstract class NumericComparison(op: String, precedence: Int)
extends BinaryOperator(op, precedence, Associativity.Non) {
override def tpe(lhs: Type, rhs: Type): TypingResult = {
override def tpe(lhs: Type, rhs: Type)(implicit predef: Predef): TypingResult = {
lhs.lowestCommonAncestor(rhs) match {
case None if !lhs.isNum => Left(s"Left hand side is not a numeric type but: $lhs")
case None if !rhs.isNum => Left(s"Right hand side is not a numeric type but: $rhs")
case Some(tpe) if tpe.isNum => Right(Type.Boolean)
case Some(tpe) if tpe.isNum => Right(predef.Boolean)
case x => sys.error(s"Unhandled case: $x")
}
}
......@@ -70,11 +71,11 @@ object operators {
sealed abstract class EqualityOperator(op: String, precedence: Int)
extends BinaryOperator(op, precedence, Associativity.Non) {
override def tpe(lhs: Type, rhs: Type): TypingResult = {
override def tpe(lhs: Type, rhs: Type)(implicit predef: Predef): TypingResult = {
if(!lhs.overlaps(rhs))
Left(s"Comparing unrelated types: $lhs $rhs")
else
Right(Type.Boolean)
Right(predef.Boolean)
}
}
......
......@@ -2,6 +2,7 @@ package dahu.planning.model
import dahu.planning.model
import dahu.planning.model.common.operators.{BinaryOperator, UnaryOperator}
import dahu.planning.model.full.Model
import spire.math.Real
import spire.implicits._
......@@ -9,17 +10,16 @@ package object common {
final case class Id(scope: Scope, name: String) {
override def toString: String = scope.toScopedString(name)
def toTPId = Timepoint(this)
}
object Timepoint {
def apply(id: Id): LocalVar = LocalVar(id, Type.Time)
def apply(id: Id)(implicit predef: Predef): LocalVar = LocalVar(id, predef.Time)
}
sealed trait Scope {
def +(nestedScope: String): InnerScope = InnerScope(this, nestedScope)
def /(name: String): Id = Id(this, name)
def makeNewId(): Id = Id(this, model.defaultId())
def toScopedString(name: String): String
......@@ -44,6 +44,8 @@ package object common {
def isSubtypeOf(typ: Type): Boolean =
this == typ || parent.exists(t => t == typ || t.isSubtypeOf(typ))
def isBoolean: Boolean = this.isInstanceOf[Type.BooleanType]
def overlaps(typ: Type): Boolean =
this.isSubtypeOf(typ) || typ.isSubtypeOf(this)
......@@ -77,6 +79,9 @@ package object common {
final case class ObjSubType(id: Id, father: ObjType) extends ObjType {
def parent: Some[ObjType] = Some(father)
}
final case class BooleanType(id: Id) extends ObjType {
override def parent: Option[ObjType] = Some(ObjectTop)
}
sealed trait IRealType extends Type {
def min: Option[Real]
......@@ -126,22 +131,23 @@ package object common {
override def parent: Some[IIntType] = Some(father)
}
val Time = IntSubType(Id(RootScope, "time"), Integers)
}
trait Predef {
import Type._
val Time: IRealType
val Boolean = ObjSubType(Id(RootScope, "boolean"), ObjectTop)
val Boolean: BooleanType
// 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)
val True: Instance
val False: Instance
val True = Instance(Id(RootScope, "true"), Boolean)
val False = Instance(Id(RootScope, "false"), Boolean)
val Start: Var
val End: Var
val Start = Id(RootScope, "start")
val End = Id(RootScope, "end")
def baseModel: Model
}
sealed trait Expr {
def typ: Type
}
......@@ -176,7 +182,7 @@ package object common {
override def toString: String = id.toString
}
case class Op2(op: BinaryOperator, lhs: Expr, rhs: Expr) extends Expr {
case class Op2(op: BinaryOperator, lhs: Expr, rhs: Expr)(implicit predef: Predef) extends Expr {
override def typ: Type = op.tpe(lhs.typ, rhs.typ) match {
case Right(t) => t
case Left(err) => sys.error(err)
......
......@@ -84,7 +84,7 @@ package object core {
sealed trait StaticAssertion extends Statement
final case class StaticBooleanAssertion(e: Expr) extends StaticAssertion {
require(e.typ.isSubtypeOf(Type.Boolean))
require(e.typ.isBoolean)
override def toString: String = s"assert($e)"
}
final case class StaticAssignmentAssertion(left: BoundConstant, right: Cst)
......@@ -133,7 +133,8 @@ package object core {
override def toString: String = s"[$start, $end] $fluent == $from :-> $to"
}
final case class ActionTemplate(scope: InnerScope, content: Seq[InActionBlock])
final case class ActionTemplate(scope: InnerScope, content: Seq[InActionBlock])(
implicit predef: Predef)
extends InModuleBlock {
def name: String = scope.name
lazy val args: Seq[Arg] = content.collect { case ArgDeclaration(a) => a }
......@@ -143,34 +144,33 @@ package object core {
lazy val start: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), Type.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), predef.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), Type.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), predef.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
}
/** Instance of an action template */
final case class Action(scope: InnerScope,
content: Seq[InActionBlock],
template: ActionTemplate) {
final case class Action(scope: InnerScope, content: Seq[InActionBlock], template: ActionTemplate)(
implicit predef: Predef) {
def name: String = scope.name
val args: Seq[Arg] = content.collect { case ArgDeclaration(a) => a }
lazy val start: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), Type.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "start"), predef.Time)) => tp
}
.getOrElse(sys.error("No start timepoint in this action"))
lazy val end: LocalVar = content
.collectFirst {
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), Type.Time)) => tp
case LocalVarDeclaration(tp @ LocalVar(Id(`scope`, "end"), predef.Time)) => tp
}
.getOrElse(sys.error("No end timepoint in this action"))
}
......
package dahu.planning.model
import dahu.planning.model.common.Type.BooleanType
import dahu.planning.model.common._
import dahu.planning.model.common.operators.{BinaryOperator, UnaryOperator}
......@@ -14,11 +15,6 @@ package object full {
def id: Id
}
object TimepointDeclaration {
def apply(id: Id): LocalVarDeclaration =
LocalVarDeclaration(LocalVar(id, Type.Time))
}
case class TypeDeclaration(typ: Type) extends Declaration[Type] with InModuleBlock {
override def id: Id = typ.id
override def toString: String = s"type $id" + {
......@@ -64,7 +60,9 @@ package object full {
sealed trait TimedExpr extends Expr
sealed trait ExprTree extends StaticExpr
case class BinaryExprTree(op: BinaryOperator, lhs: StaticExpr, rhs: StaticExpr) extends ExprTree {
case class BinaryExprTree(op: BinaryOperator, lhs: StaticExpr, rhs: StaticExpr)(
implicit predef: Predef)
extends ExprTree {
override val typ: Type = op.tpe(lhs.typ, rhs.typ) match {
case Right(tpe) => tpe
case Left(err) =>
......@@ -110,7 +108,9 @@ package object full {
def wrapped: Seq[Block]
}
abstract class TimedAssertion(parent: Option[Ctx], name: String) extends Ctx with Block {
abstract class TimedAssertion(parent: Option[Ctx], name: String)(implicit predef: Predef)
extends Ctx
with Block {
override val scope: InnerScope = parent.map(_.scope).getOrElse(RootScope) + name
val start: LocalVar = Timepoint(this.id("start"))
......@@ -123,7 +123,7 @@ package object full {
case class TimedEqualAssertion(left: TimedExpr, // TODO: should not restrict this to be symbolic
right: StaticExpr,
parent: Option[Ctx],
name: String)
name: String)(implicit predef: Predef)
extends TimedAssertion(parent, name) {
if(name == "__296")
println(name)
......@@ -136,7 +136,7 @@ package object full {
from: StaticExpr,
to: StaticExpr,
parent: Option[Ctx],
name: String)
name: String)(implicit predef: Predef)
extends TimedAssertion(parent, name) {
override def toString: String =
if(name.startsWith(reservedPrefix)) s"$fluent == $from :-> $to"
......@@ -146,7 +146,7 @@ package object full {
case class TimedAssignmentAssertion(fluent: TimedExpr,
to: StaticExpr,
parent: Option[Ctx],
name: String)
name: String)(implicit predef: Predef)
extends TimedAssertion(parent, name) {
override def toString: String =
if(name.startsWith(reservedPrefix)) s"$fluent := $to"
......@@ -171,7 +171,7 @@ package object full {
trait StaticAssertion extends Statement
case class BooleanAssertion(expr: StaticExpr) extends StaticAssertion {
require(expr.typ.isSubtypeOf(Type.Boolean))
require(expr.typ.isInstanceOf[BooleanType])
override def toString: String = expr.toString
}
......@@ -302,10 +302,10 @@ package object full {
case _ => None
}
def findTimepoint(name: String): Option[LocalVar] =
def findTimepoint(name: String)(implicit predef: Predef): Option[LocalVar] =
findDeclaration(name).flatMap {
case LocalVarDeclaration(v @ LocalVar(_, tpe)) if tpe.isSubtypeOf(Type.Time) => Some(v)
case _ => None
case LocalVarDeclaration(v @ LocalVar(_, tpe)) if tpe.isSubtypeOf(predef.Time) => Some(v)
case _ => None
}
def findType(name: String): Option[Type] =
......
......@@ -10,22 +10,22 @@ object ActionInstantiation {
trait IdRewrite[T] {
/** Transforms a type T, recursively replacing any id: Id in it with f(id) */
def map(a: T, f: Id => Id): T
def map(a: T, f: Id => Id)(implicit predef: Predef): T
}
// provides syntax for boilerplate
implicit class Rewrite[T](private val lhs: T) extends AnyVal {
def rw(f: Id => Id)(implicit rewrite: IdRewrite[T]): T = rewrite.map(lhs, f)
def rw(f: Id => Id)(implicit rewrite: IdRewrite[T], predef: Predef): T = rewrite.map(lhs, f)
}
implicit object ofCst extends IdRewrite[Cst] {
override def map(a: Cst, f: Id => Id): Cst = a match {
override def map(a: Cst, f: Id => Id)(implicit predef: Predef): Cst = a match {
case i: IntLiteral => i
case Instance(id, tpe) => Instance(f(id), tpe)
}
}
implicit object ofExpr extends IdRewrite[Expr] {
override def map(a: Expr, f: Id => Id): Expr = a match {
override def map(a: Expr, f: Id => Id)(implicit predef: Predef): Expr = a match {
case x: Cst => x.rw(f)
case Arg(id, tpe) => Arg(f(id), tpe)
case LocalVar(id, tpe) => LocalVar(f(id), tpe)
......@@ -35,44 +35,48 @@ object ActionInstantiation {
}
implicit object ofConstantTemplate extends IdRewrite[ConstantTemplate] {
override def map(a: ConstantTemplate, f: Id => Id): ConstantTemplate = a match {
override def map(a: ConstantTemplate, f: Id => Id)(
implicit predef: Predef): ConstantTemplate = a match {
case ConstantTemplate(id, tpe, params) =>
ConstantTemplate(f(id), tpe, params.map { case Arg(id, tpe) => Arg(f(id), tpe) })
}
}
implicit object ofFluentTemplate extends IdRewrite[FluentTemplate] {
override def map(a: FluentTemplate, f: Id => Id): FluentTemplate = a match {
case FluentTemplate(id, tpe, params) =>
FluentTemplate(f(id), tpe, params.map { case Arg(id, tpe) => Arg(f(id), tpe) })
}
override def map(a: FluentTemplate, f: Id => Id)(implicit predef: Predef): FluentTemplate =
a match {
case FluentTemplate(id, tpe, params) =>
FluentTemplate(f(id), tpe, params.map { case Arg(id, tpe) => Arg(f(id), tpe) })
}
}
implicit object ofFluent extends IdRewrite[Fluent] {
override def map(a: Fluent, f: Id => Id): Fluent = a match {
override def map(a: Fluent, f: Id => Id)(implicit predef: Predef): Fluent = a match {
case Fluent(template, params) => Fluent(template.rw(f), params.map(_.rw(f)))
}
}
implicit object ofBlock extends IdRewrite[InActionBlock] {
override def map(a: InActionBlock, f: Id => Id): InActionBlock = a match {
case StaticBooleanAssertion(e) => StaticBooleanAssertion(e.rw(f))
case ArgDeclaration(Arg(id, tpe)) => ArgDeclaration(Arg(f(id), tpe))
case LocalVarDeclaration(LocalVar(id, tpe)) => LocalVarDeclaration(LocalVar(f(id), tpe))
case StaticAssignmentAssertion(x: BoundConstant, cst) =>
StaticAssignmentAssertion(new BoundConstant(x.template, x.params.map(_.rw(f))), cst.rw(f))
case TimedAssignmentAssertion(st, ed, fl, value) =>
TimedAssignmentAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedEqualAssertion(st, ed, fl, value) =>
TimedEqualAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedTransitionAssertion(st, ed, fl, from, to) =>
TimedTransitionAssertion(st.rw(f), ed.rw(f), fl.rw(f), from.rw(f), to.rw(f))
case BindAssertion(Constant(template, params), LocalVar(id, tpe)) =>
BindAssertion(Constant(template.rw(f), params.map(_.rw(f))), LocalVar(f(id), tpe))
}
override def map(a: InActionBlock, f: Id => Id)(implicit predef: Predef): InActionBlock =
a match {
case StaticBooleanAssertion(e) => StaticBooleanAssertion(e.rw(f))
case ArgDeclaration(Arg(id, tpe)) => ArgDeclaration(Arg(f(id), tpe))
case LocalVarDeclaration(LocalVar(id, tpe)) => LocalVarDeclaration(LocalVar(f(id), tpe))
case StaticAssignmentAssertion(x: BoundConstant, cst) =>
StaticAssignmentAssertion(new BoundConstant(x.template, x.params.map(_.rw(f))),
cst.rw(f))
case TimedAssignmentAssertion(st, ed, fl, value) =>
TimedAssignmentAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedEqualAssertion(st, ed, fl, value) =>
TimedEqualAssertion(st.rw(f), ed.rw(f), fl.rw(f), value.rw(f))
case TimedTransitionAssertion(st, ed, fl, from, to) =>
TimedTransitionAssertion(st.rw(f), ed.rw(f), fl.rw(f), from.rw(f), to.rw(f))
case BindAssertion(Constant(template, params), LocalVar(id, tpe)) =>
BindAssertion(Constant(template.rw(f), params.map(_.rw(f))), LocalVar(f(id), tpe))
}
}
}
/** Builds a new action instance with the given name*/
def instance(template: ActionTemplate, instanceName: String): Action = {
def instance(template: ActionTemplate, instanceName: String)(implicit predef: Predef): Action = {
val instanceScope: InnerScope = template.scope.parent + instanceName
val trans: Id => Id = x => {
......
......@@ -9,17 +9,19 @@ object FullToCore {
private object ImplicitConversions {
import scala.language.implicitConversions
implicit def extractPredef(implicit ctx: Context): Predef = ctx.predef
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 ===(rhs: Expr)(implicit predef: Predef): Expr = Op2(operators.Eq, lhs, rhs)
def <=(rhs: Expr)(implicit predef: Predef): Expr = Op2(operators.LEQ, lhs, rhs)
def <(rhs: Expr)(implicit predef: Predef): Expr = Op2(operators.LT, lhs, rhs)
def toStatement: core.Statement = core.StaticBooleanAssertion(lhs)
}
}
import ImplicitConversions._
case class Context(scope: Scope, config: Config = Config())
case class Context(predef: Predef, scope: Scope, config: Config = Config())
/** Monad that represent an expression of type A that is subject to the associated statements to restrict its values. */
private case class CoreM[+A](value: A, statements: Seq[core.Statement]) {
......@@ -85,7 +87,7 @@ object FullToCore {
case full.ArgDeclaration(arg) => Seq(core.ArgDeclaration(arg))
case x: full.Statement => f2c(x)(actionContext).statements
}
core.ActionTemplate(act.scope, statements)
core.ActionTemplate(act.scope, statements)(actionContext.predef)
}
private def f2c(block: full.Statement)(implicit ctx: Context): CoreM[Unit] = block match {
......@@ -176,13 +178,14 @@ object FullToCore {
case full.LocalVarDeclaration(v) => CoreM.unit(core.LocalVarDeclaration(v))
}
def trans(model: full.Model, config: Config = Config()): Seq[core.InModuleBlock] = {
def trans(model: full.Model, config: Config = Config())(
implicit predef: Predef): Seq[core.InModuleBlock] = {
model.store.blocks.flatMap {
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)))
case x: full.Statement => f2c(x)(Context(predef, model.scope, config)).statements
case x: full.ActionTemplate => Seq(f2c(x)(Context(predef, model.scope, config)))
}
}
......
......@@ -8,6 +8,7 @@ import dahu.utils.errors._
import scala.collection.JavaConverters._
import scala.collection.mutable
import scala.language.implicitConversions
object Main extends App {
......@@ -28,16 +29,37 @@ object Main extends App {
println(dom)
// println(pb)
object PddlPredef extends Predef {
import common.Type._
private val scope = RootScope + "_predef_"
override val Time: IRealType = IntSubType(scope / "time", Integers)
override val Boolean: BooleanType = BooleanType(scope / "boolean")
override val True: Instance = Instance(scope / "true", Boolean)
override val False: Instance = Instance(scope / "false", Boolean)