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

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

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

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

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

  6. val funcSort: Sort[Term, ExstFunc]

    conditioning on being a function

  7. def incl1Node(typ: Typ[Term]): Option[GeneratorNode[Term]]

    Node for the first inclusion targeting a plus type.

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

    node family to target products using inclusions

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

    Node for second inclusion targeting a plus type.

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

    node family to target products using inclusions

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

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

  13. val typAsTermSort: Sort[Typ[Term], Term]
  14. 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)

  15. 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)

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

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

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

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

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

  21. case object Incl1Node extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  22. case object Incl2Node extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
  23. case object LamApply extends (Term, Term) => Term with Product with Serializable

    Wrapper for lambda to allow equality and toString to work.

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

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

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

    Wrapper for Pi to allow equality and toString to work.

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

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

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

    Wrapper for Sigma to allow equality and toString to work.

  28. case object TypViaZeroNode extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable