Packages

o

provingground.learning

TermRandomVars

object TermRandomVars

Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. TermRandomVars
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. Protected

Type Members

  1. case class AtomVar[U](atom: U) extends RandomVar[U] with Product with Serializable
  2. case class ContextTerms(ctx: Context) extends RandomVar[Term] with Product with Serializable
  3. case class ContextTyps(ctx: Context) extends RandomVar[Typ[Term]] with Product with Serializable
  4. case class FuncFoldVar(func: Term, depth: Int) extends RandomVar[Term] with Product with Serializable
  5. case class FuncWithDom(dom: Typ[Term]) extends (Term) => Option[ExstFunc] with Product with Serializable
  6. case class FuncWithDomFilter(dom: Typ[Term]) extends (ExstFunc) => Boolean with Product with Serializable
  7. case class IndexedIntroRuleTyps(typF: Term) extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of introduction rules for an indexed inductive type

    distribution of introduction rules for an indexed inductive type

    typF

    the type family

  8. case class IndexedIterFuncTypTo(typF: Term) extends RandomVar[Typ[Term]] with Product with Serializable

    iterated function type targetting a fully applied type family

    iterated function type targetting a fully applied type family

    typF

    the type family

  9. case class IntroRuleTypes(inductiveTyp: Typ[Term]) extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of introduction rules for an inductive type

    distribution of introduction rules for an inductive type

    inductiveTyp

    the inductive type being defined

  10. case class IterFuncTypTo(typ: Typ[Term]) extends RandomVar[Typ[Term]] with Product with Serializable

    iterated function types targeting a given type, typically used in introduction rules

    iterated function types targeting a given type, typically used in introduction rules

    typ

    the final type

  11. case class PartiallyApplied(func: Term) extends RandomVar[Term] with Product with Serializable

    distribution of f, f(x), f(x)(y) etc

    distribution of f, f(x), f(x)(y) etc

    func

    the function to apply

  12. case class PiOutput[U <: Term with Subs[U], V <: Term with Subs[V]](pd: PiDefn[U, V]) extends (Term) => RandomVar[Term] with Product with Serializable
  13. case class TypsFromFamily(typF: Term) extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of types obtained by full application in a type family

    distribution of types obtained by full application in a type family

    typF

    the type family

  14. case class WithTyp(typ: Typ[Term]) extends (Term) => Boolean 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. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  5. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  6. def contextTermNode(ctx: Context): GeneratorNode[Term]
  7. def domForInduc(defn: ExstInducDefn): AtCoord[::[ExstInducDefn, HNil], Term]
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  10. def equationDepends(t: Term)(eq: Equation): Boolean
  11. def equationNodeDepends(t: Term)(eq: EquationNode): Boolean
  12. def expressionMapVars(fn: VariableMap)(exp: Expression): Expression
  13. def expressionSubs(x: Term, y: Term)(exp: Expression): Expression
  14. def funcForCod(cod: Typ[Term]): AtCoord[::[Typ[Term], HNil], Term]
  15. def funcWithDomTermNode(node: GeneratorNode[Term]): GeneratorNodeFamily[::[Typ[Term], HNil], ExstFunc]
  16. def funcsWithDomain(typ: Typ[Term]): RandomVar[ExstFunc]

    distribution of functions with a specified domain

    distribution of functions with a specified domain

    typ

    the domain

    returns

    distribution at domain

  17. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  18. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  19. def inducHeadNode(inductiveTyp: Typ[Term]): Atom[Typ[Term]]

    the introduction with just the target type

    the introduction with just the target type

    inductiveTyp

    the inductive type being defined

    returns

    node for inclusion

  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. def isleNormalize(eq: EquationNode, varWeight: Double = 0.3): EquationNode
  22. def isleNormalizeVarExp[Y](v: Variable[Y], rhs: Expression, vars: Vector[Term]): (Variable[Y], Expression)
  23. def isleNormalizeVars[Y](v: Variable[Y], vars: Vector[Term]): Variable[Y]
  24. def isleSub[c, d](x: Term, y: Term)(isle: Island[c, TermState, d, Term], boat: Term): Island[c, TermState, d, Term]
  25. def jsonToRandomVar(json: Value): RandomVar[_]
  26. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  27. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  28. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  29. def partiallyApplySelf(f: Term): Atom[Term]

    atomic distribution f for partial application

    atomic distribution f for partial application

    f

    the function

    returns

    node to include

  30. val randomVarStrings: Vector[(RandomVar[_], String, String)]
  31. def randomVarSubs[U](x: Term, y: Term)(rv: RandomVar[U]): RandomVar[U]
  32. def randomVarToJson[X](rv: RandomVar[X]): Value
  33. val rvElemMap: Map[RandomVar[Any], String]
  34. val rvStrMap: Map[RandomVar[Any], String]
  35. def sortSubs[U, V](x: Term, y: Term)(sort: Sort[U, V]): Sort[U, V]
  36. val strRvMap: Map[String, RandomVar[Any]]
  37. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  38. def termsWithTyp(typ: Typ[Term]): RandomVar[Term]

    distribution of terms with a specific type

    distribution of terms with a specific type

    typ

    the type

    returns

    distribution at type

  39. def toString(): String
    Definition Classes
    AnyRef → Any
  40. val typFamilySort: Sort[Term, ExstFunc]
  41. val typFamilyTypes: RandomVar[Term]

    type family types, e.g.

    type family types, e.g. A -> Type, for indexed induction

  42. val typSort: Sort[Term, Typ[Term]]
  43. def valueSubs[U](x: Term, y: Term)(value: U): U
  44. def varDepends(t: Term)(v: Variable[_]): Boolean
  45. def variableSubs[Y](x: Term, y: Term)(v: Variable[Y]): Variable[Y]
  46. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  47. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  48. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  49. def withTypNode(node: GeneratorNode[Term]): GeneratorNodeFamily[::[Typ[Term], HNil], Term]
  50. def withTypSort(typ: Typ[Term]): Sort[Term, Term]
  51. case object DomFn extends (ExstFunc) => Typ[Term] with Product with Serializable
  52. case object DomForInduc extends SimpleFamily[ExstInducDefn, Term] with Product with Serializable
  53. case object FuncForCod extends SimpleFamily[Typ[Term], Term] with Product with Serializable
  54. case object FuncOpt extends (Term) => Option[ExstFunc] with Product with Serializable
  55. case object Funcs extends RandomVar[ExstFunc] with Product with Serializable

    distribution of functions : as existentials (wrapping terms), not as terms

  56. case object FuncsWithDomain extends SimpleFamily[Typ[Term], ExstFunc] with Product with Serializable

    family of distribution of (existential) functions with specifed domain.

  57. case object FuncsWithDomainFn extends (Typ[Term]) => RandomVar[ExstFunc] with Product with Serializable
  58. case object Goals extends RandomVar[Typ[Term]] with Product with Serializable
  59. case object InducDefns extends RandomVar[ExstInducDefn] with Product with Serializable

    distribution of existential inductive definitions

  60. case object InducStrucs extends RandomVar[ExstInducStrucs] with Product with Serializable

    distribution of existential inductive structures

  61. case object IsleDomains extends RandomVar[Typ[Term]] with Product with Serializable
  62. case object Negate extends (Typ[Term]) => Typ[Term] with Product with Serializable
  63. case object RestrictFuncWithDom extends (Typ[Term]) => Restrict[Term, ExstFunc] with Product with Serializable
  64. case object TargetTyps extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of types to target for generating terms; either a generated type or a goal.

  65. case object Terms extends RandomVar[Term] with Product with Serializable

    distribution of terms

  66. case object TermsWithTyp extends SimpleFamily[Typ[Term], Term] with Product with Serializable

    family of distributions of terms with specified type

  67. case object TermsWithTypFn extends (Typ[Term]) => RandomVar[Term] with Product with Serializable

    Wrapper for terms with type family to allow equality and toString to work.

  68. case object TypAsTermOpt extends (Typ[Term]) => Option[Term] with Product with Serializable
  69. case object TypFamilies extends RandomVar[ExstFunc] with Product with Serializable

    distribution of type families

  70. case object TypFamilyOpt extends (Term) => Option[ExstFunc] with Product with Serializable
  71. case object TypFn extends (Term) => Typ[Term] with Product with Serializable
  72. case object TypOpt extends (Term) => Option[Typ[Term]] with Product with Serializable
  73. case object Typs extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of types

  74. case object TypsAndFamilies extends RandomVar[Term] with Product with Serializable

    distribution of types and type families

  75. case object WithTypSort extends (Typ[Term]) => Sort[Term, Term] with Product with 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