case class TorsoForm(torso: Term, apps: List[Appendage]) extends HashEquality[TorsoForm] with Product with Serializable
The torso form of a term is named akin to the head normal forms.
For example, OMA(h1, OMA(h2, tr, ext2), ext1) is in torso form with tr as the torso and (h1,ext1) and (h2,ext2) as Appendages that are attached to the torso.
Its torso normal form is TorsoNormalForm(c, Appendage(h1, ext1) :: Appendage(h2, ext2) :: Nil)
The point of the torso normal form is understood by considering a type theory, whose constructor are paired into introduction and elimination operators. Then the torso form is a useful representation for a series h1, h2, ... of eliminators applied to a term (the torso). The torso is either atomic or a sequence of introductors. In the latter case, a reduction rule (e.g., beta) can be applied, which eventually yields an atomic torso.
For example, OMA(@,OMA(pi1,c),a) arises from the constant c (of product type) by first projection out a component (a function) and then applying it to a.
- Source
- TorsoForm.scala
- Alphabetic
- By Inheritance
- TorsoForm
- Serializable
- Serializable
- Product
- Equals
- HashEquality
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val apps: List[Appendage]
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
lazy val
hash: Int
the hash code
the hash code
- Definition Classes
- HashEquality
-
def
hasheq(that: HashEquality[TorsoForm]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
-
def
hashneq(that: HashEquality[TorsoForm]): Boolean
this hasheq that is the same as this == that, but fails immediately if false
this hasheq that is the same as this == that, but fails immediately if false
- Definition Classes
- HashEquality
-
def
heads: List[GlobalName]
only the heads
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
toHeadForm: Term
transforms a TorsoForm into the usual form
- val torso: Term
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()