Skip to content

Commit

Permalink
Change FieldMap.Elem to Binding
Browse files Browse the repository at this point in the history
  • Loading branch information
jhnaldo committed Sep 12, 2024
1 parent 5220264 commit b9080fa
Show file tree
Hide file tree
Showing 11 changed files with 240 additions and 250 deletions.
2 changes: 1 addition & 1 deletion src/main/resources/manuals/types
Original file line number Diff line number Diff line change
Expand Up @@ -736,7 +736,7 @@ type SharedArrayBuffer extends Object {

// https://tc39.es/ecma262/#sec-properties-of-dataview-instances
type DataView extends OrdinaryObject {
DataView: Bot;
DataView: Undefined;
ViewedArrayBuffer: ESValue;
ByteLength: NonNegInt | Enum[~auto~];
ByteOffset: NonNegInt;
Expand Down
5 changes: 2 additions & 3 deletions src/main/scala/esmeta/analyzer/TypeAnalyzer.scala
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@ import esmeta.es.*
import esmeta.ir.{Func => IRFunc, *}
import esmeta.ty.*
import esmeta.ty.util.{Stringifier => TyStringifier}
import esmeta.ty.FieldMap.{Elem => FMElem}
import esmeta.util.*
import esmeta.util.Appender.*
import esmeta.state.*
Expand Down Expand Up @@ -601,7 +600,7 @@ class TypeAnalyzer(
rv <- transfer(expr)
lty = lv.ty
rty = rv.ty
relem = FMElem(rty)
relem = Binding(rty)
elem = if (positive) relem else lty.record(field) -- relem
refinedTy = ValueTy(
ast = lty.ast,
Expand All @@ -622,7 +621,7 @@ class TypeAnalyzer(
record = ty.record
refinedTy = ValueTy(
ast = ty.ast,
record = if (positive) record.update(field, FMElem.Exist) else record,
record = if (positive) record.update(field, Binding.Exist) else record,
)
_ <- modify(_.update(l, AbsValue(refinedTy)))
} yield ()
Expand Down
79 changes: 79 additions & 0 deletions src/main/scala/esmeta/ty/Binding.scala
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
package esmeta.ty

import esmeta.state.*
import esmeta.ty.util.Parser
import esmeta.util.*

/** field binding types */
case class Binding(
value: ValueTy,
uninit: Boolean = false,
absent: Boolean = false,
) extends TyElem
with Lattice[Binding] {

/** top check */
def isTop: Boolean = value.isTop && uninit.isTop && absent.isTop

/** bottom check */
def isBottom: Boolean = value.isBottom && uninit.isBottom && absent.isBottom

/** Absent check */
def isAbsent: Boolean = value.isBottom && !uninit && absent

/** partial order/subset operator */
def <=(that: => Binding): Boolean = (this eq that) || {
this.value <= that.value &&
this.uninit <= that.uninit &&
this.absent <= that.absent
}

/** union type */
def ||(that: => Binding): Binding =
if (this eq that) this
else
Binding(
this.value || that.value,
this.uninit || that.uninit,
this.absent || that.absent,
)

/** intersection type */
def &&(that: => Binding): Binding =
if (this eq that) this
else
Binding(
this.value && that.value,
this.uninit && that.uninit,
this.absent && that.absent,
)

/** prune type */
def --(that: => Binding): Binding =
if (that.isBottom) this
else
Binding(
this.value -- that.value,
this.uninit -- that.uninit,
this.absent -- that.absent,
)

/** existence check */
def exists: Set[Boolean] =
(if (!value.isBottom || uninit) Set(true) else Set()) ++
(if (absent) Set(false) else Set())

/** containment check */
def contains(v: Option[Value | Uninit], heap: Heap): Boolean = v match
case Some(value: Value) => this.value.contains(value, heap)
case Some(Uninit) => this.uninit
case None => this.absent
}
object Binding extends Parser.From(Parser.binding) {
lazy val Top: Binding = Binding(AnyT, true, true)
lazy val Exist: Binding = Binding(AnyT, true, false)
lazy val Init: Binding = Binding(AnyT, false, false)
lazy val Uninit: Binding = Binding(BotT, true, false)
lazy val Absent: Binding = Binding(BotT, false, true)
lazy val Bot: Binding = Binding(BotT, false, false)
}
99 changes: 12 additions & 87 deletions src/main/scala/esmeta/ty/FieldMap.scala
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ import esmeta.state.*
import esmeta.ty.util.Parser
import esmeta.util.*

/** field type map */
case class FieldMap(map: Map[String, FieldMap.Elem])
/** field refinement map */
case class FieldMap(map: Map[String, Binding])
extends TyElem
with Lattice[FieldMap] {

Expand All @@ -30,9 +30,9 @@ case class FieldMap(map: Map[String, FieldMap.Elem])
FieldMap(
(for {
field <- (this.fields ++ that.fields)
elem = this(field) || that(field)
if !elem.isTop
} yield field -> elem).toMap,
binding = this(field) || that(field)
if !binding.isTop
} yield field -> binding).toMap,
)

/** intersection type */
Expand All @@ -44,20 +44,20 @@ case class FieldMap(map: Map[String, FieldMap.Elem])
FieldMap(
(for {
field <- (this.fields ++ that.fields)
elem = this(field) && that(field)
if !elem.isTop
} yield field -> elem).toMap,
binding = this(field) && that(field)
if !binding.isTop
} yield field -> binding).toMap,
)

/** TODO prune type */
def --(that: => FieldMap): FieldMap = this

/** field accessor */
def apply(field: String): Elem = map.getOrElse(field, Elem.Top)
def apply(field: String): Binding = map.getOrElse(field, Binding.Top)

/** field update */
def update(field: String, elem: Elem): FieldMap =
FieldMap(map + (field -> elem))
def update(field: String, binding: Binding): FieldMap =
FieldMap(map + (field -> binding))

/** fields */
def fields: Set[String] = map.keySet
Expand All @@ -70,80 +70,5 @@ case class FieldMap(map: Map[String, FieldMap.Elem])

object FieldMap extends Parser.From(Parser.fieldMap) {
lazy val Top: FieldMap = FieldMap()

def apply(fields: (String, Elem)*): FieldMap = FieldMap(fields.toMap)

/** optinoal value types */
case class Elem(
value: ValueTy,
uninit: Boolean = false,
absent: Boolean = false,
) extends TyElem
with Lattice[Elem] {

/** top check */
def isTop: Boolean = value.isTop && uninit.isTop && absent.isTop

/** bottom check */
def isBottom: Boolean = value.isBottom && uninit.isBottom && absent.isBottom

/** Absent check */
def isAbsent: Boolean = value.isBottom && !uninit && absent

/** partial order/subset operator */
def <=(that: => Elem): Boolean = (this eq that) || {
this.value <= that.value &&
this.uninit <= that.uninit &&
this.absent <= that.absent
}

/** union type */
def ||(that: => Elem): Elem =
if (this eq that) this
else
Elem(
this.value || that.value,
this.uninit || that.uninit,
this.absent || that.absent,
)

/** intersection type */
def &&(that: => Elem): Elem =
if (this eq that) this
else
Elem(
this.value && that.value,
this.uninit && that.uninit,
this.absent && that.absent,
)

/** prune type */
def --(that: => Elem): Elem =
if (that.isBottom) this
else
Elem(
this.value -- that.value,
this.uninit -- that.uninit,
this.absent -- that.absent,
)

/** existence check */
def exists: Set[Boolean] =
(if (!value.isBottom || uninit) Set(true) else Set()) ++
(if (absent) Set(false) else Set())

/** containment check */
def contains(v: Option[Value | Uninit], heap: Heap): Boolean = v match
case Some(value: Value) => this.value.contains(value, heap)
case Some(Uninit) => this.uninit
case None => this.absent
}
object Elem extends Parser.From(Parser.fieldMapElem) {
lazy val Top: Elem = Elem(AnyT, true, true)
lazy val Exist: Elem = Elem(AnyT, true, false)
lazy val Init: Elem = Elem(AnyT, false, false)
lazy val Uninit: Elem = Elem(BotT, true, false)
lazy val Absent: Elem = Elem(BotT, false, true)
lazy val Bot: Elem = Elem(BotT, false, false)
}
def apply(fields: (String, Binding)*): FieldMap = FieldMap(fields.toMap)
}
51 changes: 19 additions & 32 deletions src/main/scala/esmeta/ty/RecordTy.scala
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ package esmeta.ty
import esmeta.util.*
import esmeta.state.{Value, RecordObj, Heap}
import esmeta.ty.util.Parser
import FieldMap.{Elem => FMElem}

/** record types */
enum RecordTy extends TyElem with Lattice[RecordTy] {
Expand Down Expand Up @@ -53,17 +52,14 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
val rs = rmap.keySet
Elem(
(for {
t <-
ls.filter(isSubTy(_, rs)) ++
rs.filter(isSubTy(_, ls))
fm =
lmap.getOrElse(t, FieldMap.Top) &&
rmap.getOrElse(t, FieldMap.Top)
t <- ls.filter(isSubTy(_, rs)) ++ rs.filter(isSubTy(_, ls))
lfm = lmap.getOrElse(t, FieldMap.Top)
rfm = rmap.getOrElse(t, FieldMap.Top)
fm = lfm && rfm
pair <- update(t, fm)
} yield pair)
.groupBy(_._1)
.view
.mapValues(_.map(_._2).reduce(_ || _))
.map { case (t, pairs) => t -> pairs.map(_._2).reduce(_ && _) }
.toMap,
)

Expand All @@ -84,14 +80,9 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
case Elem(map) =>
StrT((for {
(name, fm) <- map.toList
f <- fm.map.keySet ++ fieldMapOf(name).map.keySet
f <- fm.map.keySet ++ fieldsOf(name).keySet
} yield f).toSet)

/** field type map */
def fieldMap: Option[FieldMap] = this match
case Top => Some(FieldMap.Top)
case Elem(map) => map.map(fieldMapOf(_) && _).reduceOption(_ || _)

/** base type names */
def bases: BSet[String] = this match
case Top => Inf
Expand All @@ -103,22 +94,22 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
case Elem(map) => Fin(map.keySet)

/** field accessor */
def apply(f: String): FMElem = this match
case Top => FMElem.Top
def apply(f: String): Binding = this match
case Top => Binding.Top
case Elem(map) =>
map.map(getField(_, f) && _(f)).foldLeft(FMElem.Bot)(_ || _)
map.map(getField(_, f) && _(f)).foldLeft(Binding.Bot)(_ || _)

/** field accessor for specific record type */
def apply(name: String, f: String): FMElem = this match
case Top => FMElem.Top
def apply(name: String, f: String): Binding = this match
case Top => Binding.Top
case Elem(map) =>
map.get(name).fold(FMElem.Bot)(getField(name, f) && _(f))
map.get(name).fold(Binding.Bot)(getField(name, f) && _(f))

/** field update */
def update(field: String, ty: ValueTy): RecordTy = update(field, FMElem(ty))
def update(field: String, ty: ValueTy): RecordTy = update(field, Binding(ty))

/** field update */
def update(field: String, elem: FMElem): RecordTy = this match
def update(field: String, elem: Binding): RecordTy = this match
case Top => Top
case Elem(map) =>
Elem(map.foldLeft(Map[String, FieldMap]()) {
Expand All @@ -139,15 +130,15 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
private def update(
pair: (String, FieldMap),
field: String,
elem: FMElem,
elem: Binding,
): Option[(String, FieldMap)] =
val (t, fm) = pair
val x = (for {
map <- refinerOf(t).get(field)
(_, u) <- map.find { case (e, _) => elem <= e }
} yield u).getOrElse(t)
val xfm = fieldMapOf(x)
if (!xfm.map.contains(field) || (elem && xfm(field)).isBottom) None
val xfm = fieldsOf(x)
if (!xfm.contains(field) || (elem && xfm(field)).isBottom) None
else Some(normalize(x -> fm.update(field, elem)))

/** record containment check */
Expand All @@ -172,11 +163,7 @@ enum RecordTy extends TyElem with Lattice[RecordTy] {
/** normalized type */
private def normalize(pair: (String, FieldMap)): (String, FieldMap) =
val (t, fm) = pair
t -> FieldMap(fm.map.filter { (f, elem) => isValidField(t, f, elem) })

/** normalized type */
private def isValidField(t: String, field: String, elem: FMElem): Boolean =
!(getField(t, field) <= elem)
t -> FieldMap(fm.map.filter { (f, elem) => !(getField(t, f) <= elem) })
}

object RecordTy extends Parser.From(Parser.recordTy) {
Expand All @@ -193,7 +180,7 @@ object RecordTy extends Parser.From(Parser.recordTy) {
name -> FieldMap(
(for {
(field, ty) <- fields
elem = FMElem(ty, false, false)
elem = Binding(ty, false, false)
} yield field -> elem).toMap,
),
),
Expand Down
Loading

0 comments on commit b9080fa

Please sign in to comment.