Packages

o

gapt.expr

preExpr

object preExpr

Intermediate representation for expressions without explicit types.

The main application is during parsing: the gapt.formats.babel.BabelParser produces pre-expressions.

This representation is intended to be as simple as possible, all higher-level constructs (such as <-> or ∀) are already desugared into simply-typed lambda terms.

It differs from the "real" lambda calculus in gapt.expr in three major ways:

  1. There are type meta-variables.
  2. There are type annotations.
  3. Free variables, bound variables, and constants are not distinguished; they are all stored as "identifiers".
Source
preExpr.scala
Linear Supertypes
AnyRef, Any
Content Hierarchy
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. preExpr
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class Abs(v: Ident, sub: Expr) extends Expr with Product with Serializable
  2. case class App(a: Expr, b: Expr) extends Expr with Product with Serializable
  3. case class ArrType(a: Type, b: Type) extends Type with Product with Serializable
  4. type Assg = Map[MetaTypeIdx, Type]
  5. case class BaseType(name: String, params: List[Type]) extends Type with Product with Serializable
  6. type Elab[X] = IndexedStateT[ElabResult, ElabState, ElabState, X]
  7. case class ElabError(loc: Option[Location], msg: String, expected: Option[Type], actual: Option[Type], assg: ElabState) extends Product with Serializable
  8. type ElabResult[X] = Either[ElabError, X]
  9. type ElabState = Map[MetaTypeIdx, Type]
  10. type Env = Map[String, Type]
  11. sealed trait Expr extends AnyRef
  12. case class FlatOps(children: List[FlatOpsChild]) extends Expr with Product with Serializable
  13. type FlatOpsChild = Either[(String, Location), Expr]
  14. case class Ident(name: String, ty: Type, params: Option[List[Type]]) extends Expr with Product with Serializable
  15. case class LocAnnotation(expr: Expr, loc: Location) extends Expr with Product with Serializable
  16. case class Location(begin: Int, end: Int) extends Product with Serializable
  17. case class MetaType(idx: MetaTypeIdx) extends Type with Product with Serializable
  18. class MetaTypeIdx extends AnyRef
  19. case class Mismatch(t1: Type, t2: Type, assg: Assg) extends UnificationError with Product with Serializable
  20. case class OccursCheck(t1: MetaType, t2: Type, assg: Assg) extends UnificationError with Product with Serializable
  21. case class Quoted(e: expr.Expr, ty: Type, fvs: Map[String, Type]) extends Expr with Product with Serializable
  22. class ReadablePrinter extends AnyRef
  23. sealed trait Type extends AnyRef
  24. case class TypeAnnotation(expr: Expr, ty: Type) extends Expr with Product with Serializable
  25. sealed trait UnificationError extends AnyRef
  26. case class VarType(name: String) extends Type with Product with Serializable

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##: Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def All: (Ident, Expr) => Expr
  5. def And: (Expr, Expr) => Expr
  6. def BinaryConn(c: MonomorphicLogicalC): (Expr, Expr) => Expr
  7. def Bool: BaseType
  8. def Bottom: Quoted
  9. def Eq(a: Expr, b: Expr): App
  10. def Ex: (Ident, Expr) => Expr
  11. def Iff(a: Expr, b: Expr): Expr
  12. def Imp: (Expr, Expr) => Expr
  13. def Neg: (Expr) => Expr
  14. def Or: (Expr, Expr) => Expr
  15. def Quant(name: String): (Ident, Expr) => Expr
  16. def QuoteBlackbox(e: expr.Expr): Quoted
  17. def QuoteWhitebox(e: expr.Expr): Quoted
  18. def Top: Quoted
  19. def UnaryConn(c: MonomorphicLogicalC): (Expr) => Expr
  20. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  21. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @IntrinsicCandidate()
  22. def elabError[T](msg: String)(implicit loc: Option[Location]): Elab[T]
  23. def elabError[T](msg: String, atExpr: Expr)(implicit loc: Option[Location]): Elab[T]
  24. def elabIdent(ch: FlatOpsChild)(implicit loc: Option[Location]): Elab[Ident]
  25. def elabIdent(e: Expr)(implicit loc: Option[Location]): Elab[Ident]
  26. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  28. def freeIdentifers(expr: Expr): Set[String]
  29. def freeMetas(t: Type): Set[MetaTypeIdx]
  30. def freshMetaType(): MetaType
  31. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  32. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @IntrinsicCandidate()
  33. def infer(expr: Expr, env: Env)(implicit loc: Option[Location], sig: BabelSignature): Elab[(Expr, Type)]
  34. def infers(exprs: Seq[Expr], env: Env)(implicit loc: Option[Location], sig: BabelSignature): Elab[List[(Expr, Type)]]
  35. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  36. def liftTypeMono(t: Ty): Type
  37. def liftTypePoly(t: Ty, ps: List[Ty]): (Type, List[Type])
  38. def locOf(expr: Expr): Option[Location]
  39. def locsOf(exprs: Seq[Expr]): Option[Location]
  40. def mkBinOp(c: ConstName, fn: Option[Expr], arg1: Expr, arg2: Expr): Expr
  41. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  42. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  43. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @IntrinsicCandidate()
  44. def parseFlatOpFirst(flatOpsChildren: List[FlatOpsChild], env: Env, minPrec: Int)(implicit loc: Option[Location], sig: BabelSignature): Elab[(Expr, List[FlatOpsChild])]
  45. def parseFlatOpRest(flatOpsChildren: List[FlatOpsChild], lhsExpr: Expr, env: Env, minPrec: Int)(implicit loc: Option[Location], sig: BabelSignature): Elab[(Expr, List[FlatOpsChild])]
  46. def solve(eqs: List[(Type, Type)], assg: Map[MetaTypeIdx, Type]): Either[UnificationError, Assg]
  47. def subst(t: Type, assg: Map[MetaTypeIdx, Type]): Type
  48. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  49. def toRealExpr(expr: Expr, sig: BabelSignature): Either[ElabError, expr.Expr]
  50. def toRealExpr(expr: Expr, assg: Map[MetaTypeIdx, Type], bound: Set[String]): expr.Expr
  51. def toRealExprs(expr: Seq[Expr], sig: BabelSignature): Either[ElabError, Seq[expr.Expr]]
  52. def toRealType(ty: Type, assg: Map[MetaTypeIdx, Type]): Ty
  53. def toString(): String
    Definition Classes
    AnyRef → Any
  54. def typeVars(t: Type): Set[String]
  55. def types(expr: Expr): Set[Type]
  56. def unify(a: Type, b: Type, mkErr: (UnificationError) => ElabError): Elab[Unit]
  57. def unifys(as: List[Type], bs: List[Type], mkErr: (UnificationError) => ElabError): Elab[Unit]
  58. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  59. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  60. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  61. object ElabError extends Serializable

Deprecated Value Members

  1. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.Throwable]) @Deprecated
    Deprecated

Inherited from AnyRef

Inherited from Any

Ungrouped