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. lazy val addInductive: MicroBot[ConsiderInductiveTypes, LocalProver, HoTTPostWeb, QueryProver, ID]
  2. def appEquations(cutoff: Double): MicroHoTTBoTT[TangentBaseState, GeneratedEquationNodes, TangentLemmas]
  3. def avoidLemmas(decay: Double = 0.5, cutoff: Double = 0.04)(v: Vector[UsedLemmas]): ParSet[Typ[Term]]
  4. lazy val backwardFunction: MiniBot[SeekGoal, WithWeight[FunctionForGoal], HoTTPostWeb, QueryProver, ID]
  5. def baseMixinLemmas(power: Double = 1.0, pfWeight: Double = 0.0): SimpleBot[Lemmas, BaseMixinLemmas]
  6. 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)
  7. def baseStateFromLp(lemmaMix: Double, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None): MicroHoTTBoTT[BaseMixinLemmas, TangentBaseState, ::[QueryProver, ::[QueryEquations, HNil]]]
  8. def baseStateFromSpecialInit(verbose: Boolean = true): DualMiniBot[BaseMixinLemmas, TangentBaseState, HoTTPostWeb, ::[PreviousPosts[SpecialInitState], ::[QueryProver, ::[Set[EquationNode], HNil]]], ID]
  9. def baseStateFromSpecialInitTask(verbose: Boolean = true): DualMiniBotTask[BaseMixinLemmas, TangentBaseState, HoTTPostWeb, ::[PreviousPosts[SpecialInitState], ::[QueryProver, ::[Set[EquationNode], HNil]]], ID]
  10. 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)]
  11. def cappedBaseState(lemmaMix: Double, cutoffScale: Double = 1.0, tgOpt: Option[TermGenParams] = None, depthOpt: Option[Int] = None, verbose: Boolean = true): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  12. lazy val cappedForkedTangentEquations: ReducedResponse[TangentBaseCompleted.type, GeneratedEquationNodes, GeneratedEquationNodes, HoTTPostWeb, ID]
  13. def cappedSpecialBaseState(verbose: Boolean = true): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  14. lazy val chompEqnUpdate: TypedPostResponse[ChompResult, HoTTPostWeb, ID]
  15. def chompReport(haltIfComplete: Boolean = true, numFailures: Int = 10): HoTTCallBack[ChompResult, FinalState]
  16. lazy val coproductBackward: SimpleBot[SeekGoal, Option[FromAny]]
  17. def decided(web: HoTTPostWeb): Future[Set[Decided]]
  18. lazy val deducedResults: MiniBot[Proved, Either[Contradicted, Proved], HoTTPostWeb, ::[GatherMapPost[PropagateProof], ::[GatherMapPost[Decided], ::[Set[Term], HNil]]], ID]
  19. def elemVals(elems: Vector[Expression], ts: TermState): Vector[(FinalVal[Any], Double)]
  20. lazy val eqnSimpleUpdate: Callback[GeneratedEquationNodes, HoTTPostWeb, Unit, ID]
  21. lazy val eqnUpdate: Callback[GeneratedEquationNodes, HoTTPostWeb, Unit, ID]
  22. def eqnsToExpEv(cvOpt: Option[(Coeff[_]) => Option[Double]] = None): MicroHoTTBoTT[GeneratedEquationNodes, ExpressionEquationSolver, ::[Set[EquationNode], ::[QueryProver, HNil]]]
  23. lazy val expEvToEqns: SimpleBot[ExpressionEquationSolver, GeneratedEquationNodes]
  24. lazy val expEvToFinalState: SimpleBot[ExpressionEquationSolver, FinalState]
  25. lazy val expnEqnUpdate: TypedPostResponse[ExpressionEquationSolver, HoTTPostWeb, ID]
  26. val exportProof: MicroHoTTBoTT[Proved, Option[Proved], GatherPost[ProofLambda]]
  27. def failedAfterChomp(power: Double = 1.0): MiniBot[ChompResult, WithWeight[FailedToProve], HoTTPostWeb, ::[QueryInitState, ::[FinalState, HNil]], ID]
  28. 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]]]]]
  29. def finalStateToChomp(solverWeight: Double = 0.05): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  30. def finalStateToConcurrentChomp(solverWeight: Double = 0.05, concurrency: Int = Utils.threadNum): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  31. val finalStateToLemma: SimpleBot[FinalState, Lemmas]
  32. def finalStateToLiberalChomp(solverWeight: Double = 0.05): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  33. val finalStateToNewLemmas: MicroHoTTBoTT[FinalState, Lemmas, QueryBaseState]
  34. def finalStateToParallelChomp(solverWeight: Double = 0.05, cutoffScales: List[Double] = List(1)): MicroBot[FinalState, ChompResult, HoTTPostWeb, ::[Set[Term], ::[QueryProver, HNil]], ID]
  35. lazy val forkedTangentEquations: DualMiniBot[TangentBaseState, GeneratedEquationNodes, HoTTPostWeb, ::[TangentLemmas, ::[LocalProver, ::[Set[EquationNode], HNil]]], ID]
  36. val fullGoalInContext: SimpleBot[SeekGoal, Option[SeekGoal]]
  37. lazy val funcToFromAll: SimpleBot[FunctionForGoal, Option[FromAll]]
  38. def goalAttempt(varWeight: Double): MicroBot[SeekGoal, Option[Either[FailedToProve, Proved]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  39. def goalAttemptEqs(varWeight: Double): MicroBot[SeekGoal, Option[::[GeneratedEquationNodes, ::[Either[FailedToProve, Proved], HNil]]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  40. val goalInContext: SimpleBot[SeekGoal, Option[::[ProofLambda, ::[SeekGoal, HNil]]]]
  41. lazy val goalLookup: MicroHoTTBoTT[SeekGoal, Either[FailedToProve, Proved], Set[Term]]
  42. 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

  43. val goalsAfterChomp: MiniBot[ChompResult, WithWeight[SeekGoal], HoTTPostWeb, ::[QueryInitState, ::[FinalState, HNil]], ID]
  44. val goalsAfterTRChomp: MiniBot[ChompResult, WithWeight[SeekGoal], HoTTPostWeb, ::[QueryInitState, ::[TermResult, HNil]], ID]
  45. def inductionBackward(maxDepth: Option[Int] = None): MicroHoTTBoTT[SeekGoal, Option[FromAll], GatherPost[ExstInducDefn]]
  46. lazy val inductionWeightedBackward: MiniBot[SeekGoal, WithWeight[FunctionForGoal], HoTTPostWeb, QueryProver, ID]
  47. 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.

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

  49. def lemmaDistributions(sizes: Map[Int, Double]): MiniBot[Lemmas, UseLemmaDistribution, HoTTPostWeb, Unit, ID]
  50. val lemmaGoal: MicroBot[UseLemma, SeekGoal, HoTTPostWeb, SeekGoal, ID]
  51. def lemmaMixin(weight: Double = 0.3): MicroBot[UseLemma, LocalProver, HoTTPostWeb, QueryProver, ID]
  52. def lemmaTangents(tangentScale: Double = 1.0): MicroBot[UseLemma, LocalTangentProver, HoTTPostWeb, QueryProver, ID]
  53. 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]]]]]
  54. def lemmasTangentEquations(scale: Double = 1.0, power: Double = 1.0): MicroHoTTBoTT[Lemmas, GeneratedEquationNodes, QueryProver]
  55. lazy val lpLemmas: MicroBot[LocalProver, Lemmas, HoTTPostWeb, Unit, ID]
  56. def lpOptimalInit(decay: Double): MicroBot[LocalProver, OptimalInitial, HoTTPostWeb, Unit, ID]
  57. lazy val lpToBigExpEv: MicroHoTTBoTT[LocalProver, ExpressionEquationSolver, Set[Equation]]
  58. lazy val lpToEnhancedExpEv: SimpleBot[LocalProver, ExpressionEquationSolver]
  59. lazy val lpToExpEv: SimpleBot[LocalProver, ExpressionEquationSolver]
  60. val lpToFinalState: SimpleBot[LocalProver, FinalState]
  61. lazy val lpToTermResult: SimpleBot[LocalProver, TermResult]
  62. def lpUnAppEquations(cutoff: Double, maxTime: FiniteDuration): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  63. lazy val lptLemmas: MicroBot[LocalTangentProver, Lemmas, HoTTPostWeb, Unit, ID]
  64. lazy val lptToEnhancedExpEv: SimpleBot[LocalTangentProver, ExpressionEquationSolver]
  65. lazy val lptToExpEv: SimpleBot[LocalTangentProver, ExpressionEquationSolver]
  66. val lptToFinalState: SimpleBot[LocalTangentProver, FinalState]
  67. lazy val lptToTermResult: SimpleBot[LocalTangentProver, TermResult]
  68. lazy val narrowOptimalInit: MicroBot[NarrowOptimizeGenerators, OptimalInitial, HoTTPostWeb, QueryProver, ID]
  69. lazy val negateGoal: MicroBot[SeekGoal, Option[::[Contradicts, ::[SeekGoal, HNil]]], HoTTPostWeb, GatherPost[SeekGoal], ID]
  70. def newLemmas(previous: Vector[FinalState], fs: FinalState): Vector[(Typ[Term], Option[Term], Double)]
  71. def parGenUnAppEquations(cutoff: Double, maxTime: FiniteDuration): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  72. def parGoalAttemptEqs(varWeight: Double): MicroBot[SeekGoal, Option[::[GeneratedEquationNodes, ::[Either[FailedToProve, Proved], HNil]]], HoTTPostWeb, ::[QueryProver, ::[Set[Term], ::[GatherMapPost[Decided], HNil]]], ID]
  73. lazy val parLpEqns: SimpleBot[LocalProver, GeneratedEquationNodes]
  74. lazy val postProofs: MiniBot[FinalState, Proved, HoTTPostWeb, Unit, ID]
  75. lazy val postProofsSimple: SimpleBot[FinalState, Option[Set[Proved]]]
  76. lazy val productBackward: SimpleBot[SeekGoal, Option[FromAll]]
  77. def proofEquationLHS(eqns: Set[EquationNode], tp: Typ[Term]): Set[Expression]
  78. def proofTrace(eqns: Set[EquationNode], tp: Typ[Term], depth: Int): (Vector[EquationNode], Vector[Expression])
  79. def reportBaseTangentPairs(results: Vector[Typ[Term]], steps: Vector[Typ[Term]]): Callback[TangentBaseState, HoTTPostWeb, TangentLemmas, ID]
  80. 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]
  81. lazy val reportContradicted: Callback[Contradicted, HoTTPostWeb, Unit, ID]
  82. def reportMixinLemmas(results: Vector[Typ[Term]]): TypedPostResponse[BaseMixinLemmas, HoTTPostWeb, ID]
  83. def reportProofs(results: Vector[Typ[Term]], text: String = "Results", goalOpt: Option[Typ[Term]] = None): Callback[FinalState, HoTTPostWeb, QueryEquations, ID]
  84. def reportProofsSimple(results: Vector[Typ[Term]], text: String = "Results", goalOpt: Option[Typ[Term]] = None): Callback[FinalState, HoTTPostWeb, Unit, ID]
  85. lazy val reportProved: Callback[Proved, HoTTPostWeb, Unit, ID]
  86. lazy val reportSuccesses: TypedPostResponse[FinalState, HoTTPostWeb, ID]
  87. def reportTangentBaseTerms(steps: Vector[Typ[Term]]): TypedPostResponse[TangentBaseState, HoTTPostWeb, ID]
  88. def reportTangentLemmas(results: Vector[Typ[Term]]): TypedPostResponse[TangentLemmas, HoTTPostWeb, ID]
  89. def repost[P](implicit arg0: scala.reflect.api.JavaUniverse.TypeTag[P], pw: Postable[P, HoTTPostWeb, ID]): MicroHoTTBoTT[Cap.type, P, P]
  90. def repostGoals(lp: LocalProver, context: Context = Context.Empty): MicroBot[Cap.type, ::[LocalProver, ::[FinalState, ::[ChompResult, HNil]]], HoTTPostWeb, ::[ChompResult, ::[GatherPost[Proved], ::[GatherPost[FinalState], HNil]]], ID]
  91. lazy val resolveFromAll: MiniBot[FromAll, SeekGoal, HoTTPostWeb, Unit, ID]
  92. lazy val resolveFromAny: MiniBot[FromAny, SeekGoal, HoTTPostWeb, Unit, ID]
  93. def scaleSplitLemmas(scale: Double = 1.0): MiniBot[Lemmas, WithWeight[UseLemma], HoTTPostWeb, Unit, ID]
  94. def scribeLog(post: PostData[_, HoTTPostWeb, ID]): Future[Unit]
  95. lazy val sigmaBackward: SimpleBot[SeekGoal, Option[SeekInstances]]
  96. lazy val skolemBot: MicroBot[SeekGoal, Option[::[Consequence, ::[SeekGoal, HNil]]], HoTTPostWeb, Unit, ID]
  97. lazy val splitLemmas: MiniBot[Lemmas, WithWeight[UseLemma], HoTTPostWeb, Unit, ID]
  98. def tangentEquations(results: Vector[Typ[Term]], steps: Vector[Typ[Term]]): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[QueryProver, ::[Set[EquationNode], HNil]]]]]
  99. 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]]
  100. 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]
  101. lazy val termResultToChomp: MicroBot[TermResult, ChompResult, HoTTPostWeb, ::[Set[Term], ::[LocalProver, HNil]], ID]
  102. lazy val termResultToEquations: SimpleBot[TermResult, GeneratedEquationNodes]
  103. lazy val termResultToFinalState: SimpleBot[TermResult, FinalState]
  104. lazy val termsFromProofs: Callback[Proved, HoTTPostWeb, Unit, ID]
  105. def timedUnAppEquations(cutoff: Double, maxTime: FiniteDuration, cutoffScale: Double = 2, minCutoff: Option[Double] = None): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, ::[Set[Term], HNil]]]]
  106. def topLevelGoals(web: HoTTPostWeb, context: Context): Future[Set[SeekGoal]]
  107. def topLevelRelevantGoals(web: HoTTPostWeb, context: Context): Future[Set[SeekGoal]]
  108. def topLevelRelevantGoalsBot[P](haltIfEmpty: Boolean = false, context: Context = Context.Empty)(implicit pp: Postable[P, HoTTPostWeb, ID]): Callback[P, HoTTPostWeb, Unit, ID]
  109. def unAppEquations(cutoff: Double): MicroHoTTBoTT[TangentBaseCompleted.type, GeneratedEquationNodes, ::[Collated[TangentBaseState], ::[TangentLemmas, HNil]]]
  110. lazy val updateTerms: Callback[FinalState, HoTTPostWeb, Unit, ID]
  111. lazy val viaZeroBot: MicroBot[SeekGoal, Option[::[Consequence, ::[SeekGoal, HNil]]], HoTTPostWeb, Unit, ID]