Packages

object HoTTBot

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

Type Members

  1. type HoTTBot = PostResponse[HoTTPostWeb, ID]
  2. type HoTTCallBack[P, Q] = Callback[P, HoTTPostWeb, Q, ID]
  3. type ID = (Int, Int)
  4. type MicroHoTTBoTT[P, Q, V] = MicroBot[P, Q, HoTTPostWeb, V, ID]
  5. type SimpleBot[P, Q] = MicroBot[P, Q, HoTTPostWeb, Unit, ID]

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. lazy val addInductive: MicroBot[ConsiderInductiveTypes, LocalProver, HoTTPostWeb, QueryProver, ID]
  5. def appEquations(cutoff: Double): MicroHoTTBoTT[TangentBaseState, GeneratedEquationNodes, TangentLemmas]
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def avoidLemmas(decay: Double = 0.5, cutoff: Double = 0.04)(v: Vector[UsedLemmas]): ParSet[Typ[Term]]
  8. lazy val backwardFunction: MiniBot[SeekGoal, WithWeight[FunctionForGoal], HoTTPostWeb, QueryProver, ID]
  9. def baseMixinLemmas(power: Double = 1.0, pfWeight: Double = 0.0): SimpleBot[Lemmas, BaseMixinLemmas]
  10. def baseState(initialState: TermState, equationNodes: Set[EquationNode], tg: TermGenParams, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, smooth: Option[Double] = None, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None): (TermState, ExpressionEquationSolver)
  11. def baseStateFromLp(lemmaMix: Double, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None): MicroHoTTBoTT[BaseMixinLemmas, TangentBaseState, ::[QueryProver, ::[QueryEquations, HNil]]]
  12. def baseStateFromSpecialInit(verbose: Boolean = true): DualMiniBot[BaseMixinLemmas, TangentBaseState, HoTTPostWeb, ::[PreviousPosts[SpecialInitState], ::[QueryProver, ::[Set[EquationNode], HNil]]], ID]
  13. def baseStateFromSpecialInitTask(verbose: Boolean = true): DualMiniBotTask[BaseMixinLemmas, TangentBaseState, HoTTPostWeb, ::[PreviousPosts[SpecialInitState], ::[QueryProver, ::[Set[EquationNode], HNil]]], ID]
  14. def baseStateTask(initialState: TermState, equationNodes: Set[EquationNode], tg: TermGenParams, maxRatio: Double = 1.01, resolution: Double = 0.0, scale: Double = 1.0, smooth: Option[Double] = None, exponent: Double = 0.5, decay: Double = 1, maxTime: Option[Long] = None): Task[(TermState, ExpressionEquationSolver)]
  15. def cappedBaseState(lemmaMix: Double, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None, verbose: Boolean = true): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  16. lazy val cappedForkedTangentEquations: ReducedResponse[TangentBaseCompleted.type, GeneratedEquationNodes, GeneratedEquationNodes, HoTTPostWeb, ID]
  17. def cappedSpecialBaseState(verbose: Boolean = true): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  18. lazy val chompEqnUpdate: TypedPostResponse[ChompResult, HoTTPostWeb, ID]
  19. def chompReport(haltIfComplete: Boolean = true, numFailures: Int = 10): HoTTCallBack[ChompResult, FinalState]
  20. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.CloneNotSupportedException]) @native() @HotSpotIntrinsicCandidate()
  21. lazy val coproductBackward: SimpleBot[SeekGoal, Option[FromAny]]
  22. def decided(web: HoTTPostWeb): Future[Set[Decided]]
  23. lazy val deducedResults: MiniBot[Proved, Either[Contradicted, Proved], HoTTPostWeb, ::[GatherMapPost[PropagateProof], ::[GatherMapPost[Decided], ::[Set[Term], HNil]]], ID]
  24. def elemVals(elems: Vector[Expression], ts: TermState): Vector[(FinalVal[Any], Double)]
  25. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  26. lazy val eqnSimpleUpdate: Callback[GeneratedEquationNodes, HoTTPostWeb, Unit, ID]
  27. lazy val eqnUpdate: Callback[GeneratedEquationNodes, HoTTPostWeb, Unit, ID]
  28. def eqnsToExpEv(cvOpt: Option[(Coeff[_]) => Option[Double]] = None): MicroHoTTBoTT[GeneratedEquationNodes, ExpressionEquationSolver, ::[Set[EquationNode], ::[QueryProver, HNil]]]
  29. def equals(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef → Any
  30. lazy val expEvToEqns: SimpleBot[ExpressionEquationSolver, GeneratedEquationNodes]
  31. lazy val expEvToFinalState: SimpleBot[ExpressionEquationSolver, FinalState]
  32. lazy val expnEqnUpdate: TypedPostResponse[ExpressionEquationSolver, HoTTPostWeb, ID]
  33. val exportProof: MicroHoTTBoTT[Proved, Option[Proved], GatherPost[ProofLambda]]
  34. def failedAfterChomp(power: Double = 1.0): MiniBot[ChompResult, WithWeight[FailedToProve], HoTTPostWeb, ::[QueryInitState, ::[FinalState, HNil]], ID]
  35. def finalStateFilteredLemmas(tg: TermGenParams = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1), maxRatio: Double = 1.5, maxTime: Option[Long] = Some(60000L)): MicroHoTTBoTT[FinalState, Lemmas, ::[PreviousPosts[FinalState], ::[PreviousPosts[TautologyInitState], ::[Set[Equation], ::[QueryBaseState, HNil]]]]]
  36. def finalStateToChomp(solverWeight: Double = 0.05): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  37. def finalStateToConcurrentChomp(solverWeight: Double = 0.05, concurrency: Int = Utils.threadNum): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  38. val finalStateToLemma: SimpleBot[FinalState, Lemmas]
  39. def finalStateToLiberalChomp(solverWeight: Double = 0.05): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  40. val finalStateToNewLemmas: MicroHoTTBoTT[FinalState, Lemmas, QueryBaseState]
  41. def finalStateToParallelChomp(solverWeight: Double = 0.05, cutoffScales: List[Double] = List(1)): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  42. lazy val forkedTangentEquations: DualMiniBot[TangentBaseState, GeneratedEquationNodes, HoTTPostWeb, ::[TangentLemmas, ::[LocalProver, ::[Set[EquationNode], HNil]]], ID]
  43. val fullGoalInContext: SimpleBot[SeekGoal, Option[SeekGoal]]
  44. lazy val funcToFromAll: SimpleBot[FunctionForGoal, Option[FromAll]]
  45. final def getClass(): Class[_ <: AnyRef]
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  46. def goalAttempt(varWeight: Double): MicroBot[SeekGoal, Option[Either[FailedToProve, Proved]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  47. def goalAttemptEqs(varWeight: Double): MicroBot[SeekGoal, Option[::[GeneratedEquationNodes, ::[Either[FailedToProve, Proved], HNil]]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  48. val goalInContext: SimpleBot[SeekGoal, Option[::[ProofLambda, ::[SeekGoal, HNil]]]]
  49. lazy val goalLookup: MicroHoTTBoTT[SeekGoal, Either[FailedToProve, Proved], Set[Term]]
  50. def goalToProver(varWeight: Double, goalWeight: Double): MicroBot[SeekGoal, Option[LocalProver], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]

    prover with variables for the context of the goal (if compatible) and with goal mixed in.

    prover with variables for the context of the goal (if compatible) and with goal mixed in.

    varWeight

    weight of variables added based on context

    goalWeight

    weight of the goal

    returns

    optionally a local prover

  51. val goalsAfterChomp: MiniBot[ChompResult, WithWeight[SeekGoal], HoTTPostWeb, ::[QueryInitState, ::[FinalState, HNil]], ID]
  52. val goalsAfterTRChomp: MiniBot[ChompResult, WithWeight[SeekGoal], HoTTPostWeb, ::[QueryInitState, ::[TermResult, HNil]], ID]
  53. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  54. def inductionBackward(maxDepth: Option[Int] = None): MicroHoTTBoTT[SeekGoal, Option[FromAll], GatherPost[ExstInducDefn]]
  55. lazy val inductionWeightedBackward: MiniBot[SeekGoal, WithWeight[FunctionForGoal], HoTTPostWeb, QueryProver, ID]
  56. lazy val instanceToGoal: MicroBot[Instance, Option[::[Consequence, ::[SeekGoal, HNil]]], HoTTPostWeb, SeekInstances, ID]

    given an instance, which is just a term of specified types, looks for instances sought and in case of match returns the corresponding new goal and how the old is a consequence of the new.

  57. lazy val instancesFromLP: MiniBot[SeekInstances, WithWeight[Instance], HoTTPostWeb, QueryProver, ID]

    generate instances with weights from a local prover alternatively we can just use a final state and given goal, with the final state generated from the local prover if desired, but this way we target the type

  58. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  59. def lemmaDistributions(sizes: Map[Int, Double]): MiniBot[Lemmas, UseLemmaDistribution, HoTTPostWeb, Unit, ID]
  60. val lemmaGoal: MicroBot[UseLemma, SeekGoal, HoTTPostWeb, SeekGoal, ID]
  61. def lemmaMixin(weight: Double = 0.3): MicroBot[UseLemma, LocalProver, HoTTPostWeb, QueryProver, ID]
  62. def lemmaTangents(tangentScale: Double = 1.0): MicroBot[UseLemma, LocalTangentProver, HoTTPostWeb, QueryProver, ID]
  63. def lemmasBigTangentEquations(scale: Double = 1.0, power: Double = 1.0, lemmaMix: Double = 0, decay: Double = 0.5, cutoff: Double = 0.04): MicroHoTTBoTT[Lemmas, ::[UsedLemmas, ::[GeneratedEquationNodes, HNil]], ::[QueryProver, ::[Set[EquationNode], ::[FinalState, ::[PreviousPosts[UsedLemmas], HNil]]]]]
  64. def lemmasTangentEquations(scale: Double = 1.0, power: Double = 1.0): MicroHoTTBoTT[Lemmas, GeneratedEquationNodes, QueryProver]
  65. lazy val lpLemmas: MicroBot[LocalProver, Lemmas, HoTTPostWeb, Unit, ID]
  66. def lpOptimalInit(decay: Double): MicroBot[LocalProver, OptimalInitial, HoTTPostWeb, Unit, ID]
  67. lazy val lpToBigExpEv: MicroHoTTBoTT[LocalProver, ExpressionEquationSolver, Set[Equation]]
  68. lazy val lpToEnhancedExpEv: SimpleBot[LocalProver, ExpressionEquationSolver]
  69. lazy val lpToExpEv: SimpleBot[LocalProver, ExpressionEquationSolver]
  70. val lpToFinalState: SimpleBot[LocalProver, FinalState]
  71. lazy val lpToTermResult: SimpleBot[LocalProver, TermResult]
  72. def lpUnAppEquations(cutoff: Double, maxTime: FiniteDuration): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  73. lazy val lptLemmas: MicroBot[LocalTangentProver, Lemmas, HoTTPostWeb, Unit, ID]
  74. lazy val lptToEnhancedExpEv: SimpleBot[LocalTangentProver, ExpressionEquationSolver]
  75. lazy val lptToExpEv: SimpleBot[LocalTangentProver, ExpressionEquationSolver]
  76. val lptToFinalState: SimpleBot[LocalTangentProver, FinalState]
  77. lazy val lptToTermResult: SimpleBot[LocalTangentProver, TermResult]
  78. lazy val narrowOptimalInit: MicroBot[NarrowOptimizeGenerators, OptimalInitial, HoTTPostWeb, QueryProver, ID]
  79. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  80. lazy val negateGoal: MicroBot[SeekGoal, Option[::[Contradicts, ::[SeekGoal, HNil]]], HoTTPostWeb, GatherPost[SeekGoal], ID]
  81. def newLemmas(previous: Vector[FinalState], fs: FinalState): Vector[(Typ[Term], Option[Term], Double)]
  82. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  83. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native() @HotSpotIntrinsicCandidate()
  84. def parGenUnAppEquations(cutoff: Double, maxTime: FiniteDuration): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  85. def parGoalAttemptEqs(varWeight: Double): MicroBot[SeekGoal, Option[::[GeneratedEquationNodes, ::[Either[FailedToProve, Proved], HNil]]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  86. lazy val parLpEqns: SimpleBot[LocalProver, GeneratedEquationNodes]
  87. lazy val postProofs: MiniBot[FinalState, Proved, HoTTPostWeb, Unit, ID]
  88. lazy val postProofsSimple: SimpleBot[FinalState, Option[Set[Proved]]]
  89. lazy val productBackward: SimpleBot[SeekGoal, Option[FromAll]]
  90. def proofEquationLHS(eqns: Set[EquationNode], tp: Typ[Term]): Set[Expression]
  91. def proofTrace(eqns: Set[EquationNode], tp: Typ[Term], depth: Int): (Vector[EquationNode], Vector[Expression])
  92. def reportBaseTangentPairs(results: Vector[Typ[Term]], steps: Vector[Typ[Term]]): Callback[TangentBaseState, HoTTPostWeb, TangentLemmas, ID]
  93. def reportBaseTangentsCalc(results: Vector[Typ[Term]], steps: Vector[Typ[Term]], inferTriples: Vector[(Typ[Term], Typ[Term], Typ[Term])], depth: Int = 4, verbose: Boolean = true): Callback[TangentBaseCompleted.type, HoTTPostWeb, ::[Collated[TangentBaseState], ::[TangentLemmas, HNil]], ID]
  94. lazy val reportContradicted: Callback[Contradicted, HoTTPostWeb, Unit, ID]
  95. def reportMixinLemmas(results: Vector[Typ[Term]]): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  96. def reportProofs(results: Vector[Typ[Term]], text: String = "Results", goalOpt: Option[Typ[Term]] = None): Callback[FinalState, HoTTPostWeb, QueryEquations, ID]
  97. def reportProofsSimple(results: Vector[Typ[Term]], text: String = "Results", goalOpt: Option[Typ[Term]] = None): Callback[FinalState, HoTTPostWeb, Unit, ID]
  98. lazy val reportProved: Callback[Proved, HoTTPostWeb, Unit, ID]
  99. lazy val reportSuccesses: TypedPostResponse[FinalState, HoTTPostWeb, ID]
  100. def reportTangentBaseTerms(steps: Vector[Typ[Term]]): TypedPostResponse[TangentBaseState, HoTTPostWeb, ID]
  101. def reportTangentLemmas(results: Vector[Typ[Term]]): TypedPostResponse[TangentLemmas, HoTTPostWeb, ID]
  102. def repost[P](implicit arg0: scala.reflect.api.JavaUniverse.TypeTag[P], pw: Postable[P, HoTTPostWeb, ID]): MicroHoTTBoTT[Cap.type, P, P]
  103. def repostGoals(lp: LocalProver, context: Context = Context.Empty): MicroBot[Cap.type, ::[LocalProver, ::[FinalState, ::[ChompResult, HNil]]], HoTTPostWeb, ::[ChompResult, ::[GatherPost[Proved], ::[GatherPost[FinalState], HNil]]], ID]
  104. lazy val resolveFromAll: MiniBot[FromAll, SeekGoal, HoTTPostWeb, Unit, ID]
  105. lazy val resolveFromAny: MiniBot[FromAny, SeekGoal, HoTTPostWeb, Unit, ID]
  106. def scaleSplitLemmas(scale: Double = 1.0): MiniBot[Lemmas, WithWeight[UseLemma], HoTTPostWeb, Unit, ID]
  107. def scribeLog(post: PostData[_, HoTTPostWeb, ID]): Future[Unit]
  108. lazy val sigmaBackward: SimpleBot[SeekGoal, Option[SeekInstances]]
  109. lazy val skolemBot: MicroBot[SeekGoal, Option[::[Consequence, ::[SeekGoal, HNil]]], HoTTPostWeb, Unit, ID]
  110. lazy val splitLemmas: MiniBot[Lemmas, WithWeight[UseLemma], HoTTPostWeb, Unit, ID]
  111. final def synchronized[T0](arg0: => T0): T0
    Definition Classes
    AnyRef
  112. def tangentEquations(results: Vector[Typ[Term]], steps: Vector[Typ[Term]]): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[QueryProver, ::[Set[EquationNode], HNil]]]]]
  113. def tangentLemmas(scale: Double = 1.0, decay: Double = 0.5, cutoff: Double = 0.04, power: Double = 1, pfScale: Double = 0.0): MicroHoTTBoTT[Lemmas, ::[UsedLemmas, ::[TangentLemmas, HNil]], PreviousPosts[UsedLemmas]]
  114. def tautologyTerms(tautGen: TermState, eqs: Set[Equation], tg: TermGenParams = TermGenParams.zero.copy(appW = 0.1, unAppW = 0.1), maxRatio: Double = 1.5, maxTime: Option[Long] = Some(60000L)): Set[Term]
  115. lazy val termResultToChomp: MicroBot[TermResult, ChompResult, HoTTPostWeb, ::[Set[Term], ::[LocalProver, HNil]], ID]
  116. lazy val termResultToEquations: SimpleBot[TermResult, GeneratedEquationNodes]
  117. lazy val termResultToFinalState: SimpleBot[TermResult, FinalState]
  118. lazy val termsFromProofs: Callback[Proved, HoTTPostWeb, Unit, ID]
  119. def timedUnAppEquations(cutoff: Double, maxTime: FiniteDuration, cutoffScale: Double = 2, minCutoff: Option[Double] = None): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  120. def toString(): String
    Definition Classes
    AnyRef → Any
  121. def topLevelGoals(web: HoTTPostWeb, context: Context): Future[Set[SeekGoal]]
  122. def topLevelRelevantGoals(web: HoTTPostWeb, context: Context): Future[Set[SeekGoal]]
  123. def topLevelRelevantGoalsBot[P](haltIfEmpty: Boolean = false, context: Context = Context.Empty)(implicit pp: Postable[P, HoTTPostWeb, ID]): Callback[P, HoTTPostWeb, Unit, ID]
  124. def unAppEquations(cutoff: Double): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, HNil]]]
  125. lazy val updateTerms: Callback[FinalState, HoTTPostWeb, Unit, ID]
  126. lazy val viaZeroBot: MicroBot[SeekGoal, Option[::[Consequence, ::[SeekGoal, HNil]]], HoTTPostWeb, Unit, ID]
  127. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])
  128. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException]) @native()
  129. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws(classOf[java.lang.InterruptedException])

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