class TermGeneratorNodes[InitState] extends AnyRef
Combining terms and subclasses to get terms, types, functions etc; these are abstract specifications, to be used for generating distributions, obtaining equations etc.
- InitState
the initial state for the dynamics, equations etc
- Alphabetic
- By Inheritance
- TermGeneratorNodes
- AnyRef
- Any
- by any2stringadd
- by StringFormat
- by Ensuring
- by ArrowAssoc
- Hide All
- Show All
- Public
- Protected
Instance Constructors
- new TermGeneratorNodes(appln: (ExstFunc, Term) => Term, unifApplnOpt: (ExstFunc, Term) => Option[Term], addVar: (Typ[Term]) => (InitState) => (Double) => (InitState, Term), getVar: (Typ[Term]) => Term, inIsle: (Term, InitState) => InitState)
- appln
function application, assuming domain and type match
- unifApplnOpt
unified application of functions
- addVar
new state with a variable, of specified type, added
- getVar
a variable of a specified type
Type Members
- case class FoldFuncTargetNode(typ: Typ[Term]) extends (Term) => Option[GeneratorNode[Term]] with Product with Serializable
- case class TargetInducFuncsFolded(target: Typ[Term]) extends (ExstInducDefn) => Option[GeneratorNode[Term]] with Product with Serializable
Value Members
- val applnByArgNode: FiberProductMap[Term, ExstFunc, Typ[Term], Term]
function application to get terms by choosing an argument and then a function with domain containing this.
- val applnNode: FiberProductMap[ExstFunc, Term, Typ[Term], Term]
function application to get terms by choosing a function and then a term in its domain
- val backwardTypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]
nodes combining backward reasoning targeting types that are (dependent) function types, aggregated over all types
- val curryBackwardTypNodeFamily: BasePiOpt[::[Typ[Term], HNil], Term]
nodes combining backward reasoning targeting types that are (dependent) function types, with domain product, sigma-types or co-products aggregated over all types
- def curryForTyp(typ: Typ[Term]): Option[GeneratorNode[Term]]
node for targeting functions on products by currying, and also on sigma-types and co-products
- def foldFuncNode(t: Term, depth: Int): GeneratorNode[Term]
Node for folding a function (or term) with a speficied number of arguments to get terms.
- def foldFuncTargetNode(t: Term, target: Typ[Term], output: RandomVar[Term]): Option[GeneratorNode[Term]]
Node for folding a function (or term) with a speficied target type to optionally get terms with the target type.
- def foldTypFamily(w: Term): GeneratorNode[Typ[Term]]
Node for fully folding a type family to get types
- def foldedTargetFunctionNode(typ: Typ[Term]): FlatMapOpt[Term, Term]
Node for generating terms of a type (if possible) by multiple applications of functions tageting the type.
- def indexedInducIdNode(typF: Typ[Term]): Map[Typ[Term], Typ[Term]]
Start of an indexed introduction rule by fully applying a type family
Start of an indexed introduction rule by fully applying a type family
- typF
the type family for the inductive type
- returns
distribution of types
- def indexedIterFuncIsle(targetTyp: Term)(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
Extending indexed introduction rule by an iterated function ending in the inductive type family fully applied.
Extending indexed introduction rule by an iterated function ending in the inductive type family fully applied.
- typ
the type by which we are extending
- returns
distribution on types.
- def indexedIterFuncNode(targetTyp: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending indexed introduction rule by iterated function type eding in fully applied inductive type family.
Aggregating extending indexed introduction rule by iterated function type eding in fully applied inductive type family.
- returns
distribution on types.
- def indexedIterHeadNode(inductiveTyp: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending introduction types for indexed inductive types by iterated function types
Aggregating extending introduction types for indexed inductive types by iterated function types
- inductiveTyp
the indexed inductive types
- def indexedOtherHeadIsle(typF: Term)(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
Extending an indexed introduction rule by a specific unrelated type
Extending an indexed introduction rule by a specific unrelated type
- typF
the indexed inductive type family
- typ
the type by which to extends
- returns
distribution on types
- def indexedOtherHeadNode(typF: Term): FlatMap[Typ[Term], Typ[Term]]
aggregating extending introduction types for indexed inductive types by unrelated types
aggregating extending introduction types for indexed inductive types by unrelated types
- typF
the indexed type family
- returns
distribution of terms
- def indexedSelfHeadNode(typF: Term): FlatMap[Typ[Term], Typ[Term]]
Aggregating extending indexed introduction rule by fully applied inductive type family.
Aggregating extending indexed introduction rule by fully applied inductive type family.
- typF
the type family
- returns
distribution on types.
- val inducFuncFoldedNode: GeneratorNode[Term]
Node for recursive definitions given an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- val inducFuncs: FlatMap[ExstInducStrucs, ExstFunc]
aggregated induction functions from inductive types
- def inducFuncsFolded(ind: ExstInducDefn): GeneratorNode[Term]
Inductive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
- def inducFuncsFoldedGivenDomNode(ind: ExstInducDefn, dom: Term): GeneratorNode[Term]
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in. Examples of domains are
Nat,Vec(A)andFin - def inducFuncsForStruc(ind: ExstInducStrucs): ZipMapOpt[Typ[Term], Term, ExstFunc]
induction function for a specific structure, picking the type family
induction function for a specific structure, picking the type family
- ind
the inductive structure
- returns
distribution of functions
- def iterFuncIsle(targetTyp: Typ[Term])(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
extending types of iterated functions targeting
Wby the typetypextending types of iterated functions targeting
Wby the typetyp- targetTyp
the target type
- typ
the type by which it is extended
- returns
distribution of types
- def iterFuncNode(targetTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
aggregating extensions of iterated function types
aggregating extensions of iterated function types
- targetTyp
target type
- returns
distribution of types
- def iterHeadNode(inductiveTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
extension of the introduction rule for an inductive type
Wby a type of the form egA -> Wextension of the introduction rule for an inductive type
Wby a type of the form egA -> W- inductiveTyp
the inductive type
W- returns
distribution of types
- def iteratedApply(f: Term): GeneratorNode[Term]
node to generate partial applications of
ffrom partial applications that are functions.node to generate partial applications of
ffrom partial applications that are functions.- f
function to be applied
- returns
distribution of terms
- val lambdaForFuncWithDomFamily: BasePi[::[Typ[Term], HNil], ExstFunc]
nodes combining lambdas with given domain that are (dependent) function types, aggregated over all domains
- def lambdaIsle(typ: Typ[Term]): Island[Term, InitState, Term, Term]
An island to generate lambda terms, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
An island to generate lambda terms, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
- typ
the domain of the lambda
- def lambdaIsleForFuncWithDomain(dom: Typ[Term]): Island[ExstFunc, InitState, Term, Term]
lambda island for generating function with specified domain
lambda island for generating function with specified domain
- dom
the desired domain
- returns
distribution of functions
- val lambdaNode: FlatMap[Typ[Term], Term]
node combining lambda islands aggregated by type
- def lambdaTypFamilyIsle(typ: Typ[Term]): GeneratorNode[ExstFunc]
An island to generate lambda terms that are type families, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in.
An island to generate lambda terms that are type families, i.e., terms are generated withing the island and exported as lambdas; the initial state of the island has a new variable mixed in. Within the island types and type families are generated.
- typ
the domain of the lambda
- val lambdaTypFamilyNode: FlatMap[Typ[Term], ExstFunc]
node combining lambda islands targeting type families aggregated by type
- def nodeForTyp(typ: Typ[Term]): Option[GeneratorNode[Term]]
A node for targeting a (dependent function) type, with variable of the domain generated and the co-domain type (more generally fibre) targeted within the island.
A node for targeting a (dependent function) type, with variable of the domain generated and the co-domain type (more generally fibre) targeted within the island.
- typ
the target type
- returns
optional distribution.
- def otherHeadIsle(inductiveTyp: Typ[Term])(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
extensions of the introduction rule types for an inductive type
Wby an unrelated typeC; we may have a Pi-Type with domainCrather than a FuncTyp there is no assumption on how the head typetypis generated, so this is reusable if only that is changed.extensions of the introduction rule types for an inductive type
Wby an unrelated typeC; we may have a Pi-Type with domainCrather than a FuncTyp there is no assumption on how the head typetypis generated, so this is reusable if only that is changed.- inductiveTyp
the inductive type
W- typ
the type
Cby which we are extending the introduction rule type- returns
distribution of introduction rule types
- def otherHeadNode(inductiveTyp: Typ[Term]): FlatMap[Typ[Term], Typ[Term]]
aggregating extensions of inductive types by unrelated types
aggregating extensions of inductive types by unrelated types
- inductiveTyp
the inductive type being generated
- returns
distribution of introduction rule types.
- def partiallyApply(f: Term): Option[Map[Term, Term]]
single function application to generate partial applications of
f, iffis a functionsingle function application to generate partial applications of
f, iffis a function- f
the function to partially apply
- returns
distribution of terms
- def piIsle(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
island to generate Pi-Types by taking variables with specified domain, similar to lambdaIsle
island to generate Pi-Types by taking variables with specified domain, similar to lambdaIsle
- typ
the domain for
- returns
distribution of types
- val piNode: FlatMap[Typ[Term], Typ[Term]]
aggregate generation of Pi-types from islands
- val recFuncFoldedNode: GeneratorNode[Term]
Node for recursive definitions picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- val recFuncs: FlatMap[ExstInducStrucs, ExstFunc]
aggregate recursion functions from inductive types
- def recFuncsFolded(ind: ExstInducDefn): GeneratorNode[Term]
Recursive definitions from a given inductive definition by generating a domain and invoking the node getting codomain and recursion data
- def recFuncsFoldedGivenDomNode(ind: ExstInducDefn, dom: Term): GeneratorNode[Term]
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in.
Recursive definition given an inductive definition and a domain, i.e., recursion function with data of the right type folded in. Examples of domains are
Nat,Vec(A)andFin - def selfHeadNode(inductiveTyp: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
extend an introduction rule type for an inductive type
WbyW -> ...extend an introduction rule type for an inductive type
WbyW -> ...- inductiveTyp
the inductive type being defined
- returns
distribution of types for introduction rules
- def sigmaIsle(typ: Typ[Term]): Island[Typ[Term], InitState, Typ[Term], Term]
island to generate Sigma-Types by taking variables with specified domain, similar to lambdaIsle
island to generate Sigma-Types by taking variables with specified domain, similar to lambdaIsle
- typ
the domain for
- returns
distribution of types
- val sigmaNode: FlatMap[Typ[Term], Typ[Term]]
aggregate generation of Sigma-types from islands
- def simpleInductiveDefn(inductiveTyp: Typ[Term]): Map[Vector[Typ[Term]], ExstInducDefn]
builds an inductive definition, i.e.
builds an inductive definition, i.e. structure with type, from a bunch of introduction rules for a type
inductiveTyp, we must separately specify how to build an introduction rules, as well as a vector of these.- inductiveTyp
the inductve type being defined
- returns
distribution on existential inductive structures
- def simpleInductiveStructure(inductiveTyp: Typ[Term]): Map[Vector[Typ[Term]], ExstInducStrucs]
builds an inductive structure from a bunch of introduction rules for a type
inductiveTyp, we must separately specify how to build an introduction rules, as well as a vector of these.builds an inductive structure from a bunch of introduction rules for a type
inductiveTyp, we must separately specify how to build an introduction rules, as well as a vector of these.- inductiveTyp
the inductve type being defined
- returns
distribution on existential inductive structures
- def targetInducBackNode(typ: Typ[Term]): MapOpt[ExstInducDefn, Term]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here meant to be used for backward reasoning.
- def targetInducFuncsFolded(ind: ExstInducDefn, target: Typ[Term]): Option[GeneratorNode[Term]]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain and recursion data
- def targetInducNode(typ: Typ[Term]): FlatMapOpt[ExstInducDefn, Term]
Node for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
- val targetInducNodeFamily: BasePi[::[Typ[Term], HNil], Term]
Family of nodes for recursive definitions targeting a specific type picking an inductive definition, generating a domain and invoking the node getting codomain; but not the recursion data here
- val termsByTyps: ZipFlatMap[Typ[Term], Term, Term]
terms generated by first choosing type and then term with the type; a form of backward reasoning
- val typApplnBase: FiberProductMap[ExstFunc, Term, Typ[Term], Term]
function application to get terms by choosing a type family and then a term in its domain, but without conditioning
- val typApplnNode: GeneratorNode[Typ[Term]]
function application to get types by choosing a type family and then a term in its domain, but without conditioning
- val typAsCodNodeFamily: BasePi[::[Typ[Term], HNil], Term]
Node for generating terms of a type (if possible) by multiple applications of functions targeting the type.
- val typFamilyApplnNode: GeneratorNode[ExstFunc]
function application to get type families by choosing a type family and then a term in its domain, but without conditioning
- val typFamilyUnifApplnNode: GeneratorNode[ExstFunc]
function application with unification starting with type families, with output conditioned to be a type family.
- val typFoldNode: FlatMap[ExstFunc, Typ[Term]]
Node family for fully folding type families to get types
- def typFromFamily(typF: Term): MapOpt[Term, Typ[Term]]
types from a type family by filtering partial applications to consider only types.
types from a type family by filtering partial applications to consider only types.
- typF
the type family
- returns
distribution of types.
- val typUnifApplnBase: ZipMapOpt[ExstFunc, Term, Term]
function application with unification starting with type families, but with output not conditioned.
- val typUnifApplnNode: GeneratorNode[Typ[Term]]
function application with unification starting with type families, with output conditioned to be a type.
- val unifApplnNode: ZipMapOpt[ExstFunc, Term, Term]
function application with unification node to get terms
- case object Appln extends (ExstFunc, Term) => Term with Product with Serializable
Wrapper for application to allow equality and
toStringto work. - case object CurryForTyp extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
- case object FlipAppln extends (Term, ExstFunc) => Term with Product with Serializable
Wrapper for flipped application to allow equality and
toStringto work. - case object FoldTypFamily extends (ExstFunc) => GeneratorNode[Typ[Term]] with Product with Serializable
- case object FoldedTargetFunctionNode extends (::[Typ[Term], HNil]) => FlatMapOpt[Term, Term] with Product with Serializable
- case object InducFuncsFolded extends (ExstInducDefn) => GeneratorNode[Term] with Product with Serializable
- case object LambdaIsle extends (Typ[Term]) => Island[Term, InitState, Term, Term] with Product with Serializable
Wrapper for lambda island to allow equality and
toStringto work. - case object LambdaIsleForFuncWithDomain extends (::[Typ[Term], HNil]) => Island[ExstFunc, InitState, Term, Term] with Product with Serializable
- case object LambdaTypFamilyIsle extends (Typ[Term]) => GeneratorNode[ExstFunc] with Product with Serializable
Wrapper for lambda island tageting type families to allow equality and
toStringto work. - case object NodeForTyp extends (::[Typ[Term], HNil]) => Option[GeneratorNode[Term]] with Product with Serializable
- case object PiIsle extends (Typ[Term]) => Island[Typ[Term], InitState, Typ[Term], Term] with Product with Serializable
- case object RecFuncsFolded extends (ExstInducDefn) => GeneratorNode[Term] with Product with Serializable
- case object SigmaIsle extends (Typ[Term]) => Island[Typ[Term], InitState, Typ[Term], Term] with Product with Serializable
- case object TargetInducNode extends (::[Typ[Term], HNil]) => FlatMapOpt[ExstInducDefn, Term] with Product with Serializable
- case object UnifApplnOpt extends (ExstFunc, Term) => Option[Term] with Product with Serializable
Wrapper for unified application to allow equality and
toStringto work.