Packages

object TermGeneratorNodes

Combining terms and subclasses to get terms, types, functions etc; these are abstract specifications, to be used for generating distributions, obtaining equations etc. The object contains helpers and other static objects.

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

Type Members

  1. case class AddVar(typ: Typ[Term]) extends (TermState) => (Double) => (TermState, Term) with Product with Serializable

    Wrapper for adding variable to allow equality and toString to work.

  2. case class ApplyFunc[U <: Term with Subs[U], V <: Term with Subs[V]](fn: Func[U, V]) extends (Term) => Term with Product with Serializable

    Wrapper for function application to allow equality and toString to work.

  3. case class ConstRandVar[O](randomVar: RandomVar[O]) extends (Term) => RandomVar[O] with Product with Serializable

    Constant random variable, for fibers for islands

    Constant random variable, for fibers for islands

    O

    scala type of the random variable

    randomVar

    the random variable

  4. case class Incl1[U <: Term with Subs[U], V <: Term with Subs[V]](pt: PlusTyp[U, V]) extends (Term) => Term with Product with Serializable

    Wrapper for first inclusion to allow equality and toString to work.

  5. case class Incl2[U <: Term with Subs[U], V <: Term with Subs[V]](pt: PlusTyp[U, V]) extends (Term) => Term with Product with Serializable

    Wrapper for second to allow equality and toString to work.

  6. case class PTTerm[U <: Term with Subs[U], V <: Term with Subs[V]](pt: ProdTyp[U, V]) extends (Term, Term) => Term with Product with Serializable

    Wrapper for pair terms to allow equality and toString to work.

  7. case class STFibVar[U <: Term with Subs[U], V <: Term with Subs[V]](pt: SigmaTyp[U, V]) extends (Term) => RandomVar[Term] with Product with Serializable

    Wrapper for fiber for sigma types to allow equality and toString to work.

  8. case class STTerm[U <: Term with Subs[U], V <: Term with Subs[V]](pt: SigmaTyp[U, V]) extends (Term, Term) => Term with Product with Serializable

    Wrapper for dependent pair term to allow equality and toString to work.

  9. case class SolverNode(solver: TypSolver) extends Product with Serializable
  10. case class SolverTyp(solver: TypSolver) extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  11. case class TargetCodomain(typ: Typ[Term]) extends (ExstFunc) => Option[Term] with Product with Serializable
  12. case class TargetInducFuncs(target: Typ[Term]) extends (ExstInducDefn) => Option[Term] 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 codomainNode(typ: Typ[Term]): GeneratorNode[Term]

    Node for generating functions that target a codomain; they are not applied yet, instead form terms of a customised random variable.

  7. val codomainNodeFamily: BasePi[::[Typ[Term], HNil], Term]

    Node family for generating functions that target a codomain; they are not applied yet, instead form terms of a customised random variable.

  8. def domainForDefn(ind: ExstInducDefn): Option[GeneratorNode[Term]]

    Generating domains for a given inductive structure, with an inductive definition also given.

    Generating domains for a given inductive structure, with an inductive definition also given. Examples of domains are Nat, Vec(A) and Fin.

  9. val domainForDefnNodeFamily: GeneratorNodeFamily[::[ExstInducDefn, HNil], Term]

    Node family for generating domains for a given inductive structure, with an inductive definition also given.

    Node family for generating domains for a given inductive structure, with an inductive definition also given. Examples of domains are Nat, Vec(A) and Fin.

  10. def domainForStruct(ind: ExstInducStrucs, fmly: Term, defn: ExstInducDefn): Option[GeneratorNode[Term]]

    Generating domains for a given inductive structure, with an inductive definition also given.

    Generating domains for a given inductive structure, with an inductive definition also given. Examples of domains are Nat, Vec(A) and Fin. The structure is specified separately as it may have some parameters applied, so be different from the one corresponding to the definition; similarly we start with the full type family of the definition, e.g. Vec, but fill in parameters to get e.g. Vec(Nat). Note that if there are no parameters the type family is returned

  11. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  12. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  13. val funcSort: Sort[Term, ExstFunc]

    conditioning on being a function

  14. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  15. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  16. def incl1Node(typ: Typ[Term]): Option[GeneratorNode[Term]]

    Node for the first inclusion targeting a plus type.

  17. val incl1TypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]

    node family to target products using inclusions

  18. def incl2Node(typ: Typ[Term]): Option[GeneratorNode[Term]]

    Node for second inclusion targeting a plus type.

  19. val incl2TypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]

    node family to target products using inclusions

  20. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  21. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  22. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  23. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  24. def recFuncsForStrucNode(ind: ExstInducStrucs): ZipMapOpt[Typ[Term], Typ[Term], ExstFunc]

    recursive functions from a specific inductive structure, picking the codomain, this is the simplest form, where the domain is not selected and so is usually wrong; further just the function is returned, not with data applied

    recursive functions from a specific inductive structure, picking the codomain, this is the simplest form, where the domain is not selected and so is usually wrong; further just the function is returned, not with data applied

    ind

    the inductive structure

    returns

    distribution of functions

  25. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  26. def targetInducFuncs(ind: ExstInducDefn, target: Typ[Term]): Option[Term]

    Node for recursive definitions targeting a specific type given an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here

  27. def toString(): String
    Definition Classes
    AnyRef → Any
  28. val typAsTermSort: Sort[Typ[Term], Term]
  29. val typViaZeroFamily: BasePiOpt[::[Typ[Term], HNil], Term]

    node family to target (dependent) function types by mapping domain to zero (i.e.

    node family to target (dependent) function types by mapping domain to zero (i.e. contradict hypothesis)

  30. def typViaZeroNodeOpt(typ: Typ[Term]): Option[Map[Term, Term]]

    node to target (dependent) function types by mapping domain to zero (i.e.

    node to target (dependent) function types by mapping domain to zero (i.e. contradict hypothesis)

  31. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  32. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  33. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  34. case object Base extends TermGeneratorNodes[TermState] with Product with Serializable

    The default term generators; essentially the only one used, except the choice of variable weight, 0.3 here, may vary.

  35. case object CodomainNode extends (::[Typ[Term], HNil]) => GeneratorNode[Term] with Product with Serializable
  36. case object DomainForDefn extends (::[ExstInducDefn, HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  37. case object EnterIsle extends (Term, TermState) => TermState with Product with Serializable

    Wrapper for entering an isle to allow equality and toString to work.

  38. case object GetVar extends (Typ[Term]) => Term with Product with Serializable

    Wrapper for getting variables to allow equality and toString to work.

  39. case object Incl1Node extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  40. case object Incl2Node extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  41. case object LamApply extends (Term, Term) => Term with Product with Serializable

    Wrapper for lambda to allow equality and toString to work.

  42. case object LamFunc extends (Term, Term) => ExstFunc with Product with Serializable

    Wrapper for lambda giving functions to allow equality and toString to work.

  43. case object PiApply extends (Term, Typ[Term]) => Typ[Term] with Product with Serializable

    Wrapper for Pi to allow equality and toString to work.

  44. case object Proj2 extends (Typ[Term], Term) => Term with Product with Serializable

    Wrapper for a specific projection to allow equality and toString to work.

  45. case object SigmaApply extends (Term, Typ[Term]) => Typ[Term] with Product with Serializable

    Wrapper for Sigma to allow equality and toString to work.

  46. case object TypViaZeroNode extends (::[Typ[Term], HNil]) => Option[GeneratorNode[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