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. def contextTermNode(ctx: Context): GeneratorNode[Term]
  2. def domForInduc(defn: ExstInducDefn): AtCoord[::[ExstInducDefn, HNil], Term]
  3. def equationDepends(t: Term)(eq: Equation): Boolean
  4. def equationNodeDepends(t: Term)(eq: EquationNode): Boolean
  5. def expressionMapVars(fn: VariableMap)(exp: Expression): Expression
  6. def expressionSubs(x: Term, y: Term)(exp: Expression): Expression
  7. def funcForCod(cod: Typ[Term]): AtCoord[::[Typ[Term], HNil], Term]
  8. def funcWithDomTermNode(node: GeneratorNode[Term]): GeneratorNodeFamily[::[Typ[Term], HNil], ExstFunc]
  9. 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

  10. 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

  11. def isleNormalize(eq: EquationNode, varWeight: Double = 0.3): EquationNode
  12. def isleNormalizeVarExp[Y](v: Variable[Y], rhs: Expression, vars: Vector[Term]): (Variable[Y], Expression)
  13. def isleNormalizeVars[Y](v: Variable[Y], vars: Vector[Term]): Variable[Y]
  14. def isleSub[c, d](x: Term, y: Term)(isle: Island[c, TermState, d, Term], boat: Term): Island[c, TermState, d, Term]
  15. def jsonToRandomVar(json: Value): RandomVar[_]
  16. 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

  17. val randomVarStrings: Vector[(RandomVar[_], String, String)]
  18. def randomVarSubs[U](x: Term, y: Term)(rv: RandomVar[U]): RandomVar[U]
  19. def randomVarToJson[X](rv: RandomVar[X]): Value
  20. val rvElemMap: Map[RandomVar[Any], String]
  21. val rvStrMap: Map[RandomVar[Any], String]
  22. def sortSubs[U, V](x: Term, y: Term)(sort: Sort[U, V]): Sort[U, V]
  23. val strRvMap: Map[String, RandomVar[Any]]
  24. 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

  25. val typFamilySort: Sort[Term, ExstFunc]
  26. val typFamilyTypes: RandomVar[Term]

    type family types, e.g.

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

  27. val typSort: Sort[Term, Typ[Term]]
  28. def valueSubs[U](x: Term, y: Term)(value: U): U
  29. def varDepends(t: Term)(v: Variable[_]): Boolean
  30. def variableSubs[Y](x: Term, y: Term)(v: Variable[Y]): Variable[Y]
  31. def withTypNode(node: GeneratorNode[Term]): GeneratorNodeFamily[::[Typ[Term], HNil], Term]
  32. def withTypSort(typ: Typ[Term]): Sort[Term, Term]
  33. case object DomFn extends (ExstFunc) => Typ[Term] with Product with Serializable
  34. case object DomForInduc extends SimpleFamily[ExstInducDefn, Term] with Product with Serializable
  35. case object FuncForCod extends SimpleFamily[Typ[Term], Term] with Product with Serializable
  36. case object FuncOpt extends (Term) => Option[ExstFunc] with Product with Serializable
  37. case object Funcs extends RandomVar[ExstFunc] with Product with Serializable

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

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

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

  39. case object FuncsWithDomainFn extends (Typ[Term]) => RandomVar[ExstFunc] with Product with Serializable
  40. case object Goals extends RandomVar[Typ[Term]] with Product with Serializable
  41. case object InducDefns extends RandomVar[ExstInducDefn] with Product with Serializable

    distribution of existential inductive definitions

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

    distribution of existential inductive structures

  43. case object IsleDomains extends RandomVar[Typ[Term]] with Product with Serializable
  44. case object Negate extends (Typ[Term]) => Typ[Term] with Product with Serializable
  45. case object RestrictFuncWithDom extends (Typ[Term]) => Restrict[Term, ExstFunc] with Product with Serializable
  46. 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.

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

    distribution of terms

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

    family of distributions of terms with specified type

  49. 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.

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

    distribution of type families

  52. case object TypFamilyOpt extends (Term) => Option[ExstFunc] with Product with Serializable
  53. case object TypFn extends (Term) => Typ[Term] with Product with Serializable
  54. case object TypOpt extends (Term) => Option[Typ[Term]] with Product with Serializable
  55. case object Typs extends RandomVar[Typ[Term]] with Product with Serializable

    distribution of types

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

    distribution of types and type families

  57. case object WithTypSort extends (Typ[Term]) => Sort[Term, Term] with Product with Serializable