Type Members

1.  case class CodeGen(inducNames: (Term) => Option[Term] = (_) => None, defns: Map[String, Term] = Map()) extends Product with Serializable
2.  trait CompositeFunctors extends AnyRef

   lower priority Functor and Traverese type classes to be extended in Functors

3.  trait ConeRestriction[X[_], Y[_], G[_]] extends AnyRef

   restriction of cone on functors

4.  trait ContextTranslator[I, O, X[_], Ctx[_, _]] extends (Ctx[I, O]) => (X[I]) => Option[X[O]]

   context dependent version of Translator

5.  trait Domain[E] extends AnyRef
6.  trait Equiv[X[_], Y[_]] extends AnyRef

   Equivalence of Functors (without laws)

7.  class ExprApplnOps[E] extends AnyRef
8.  trait ExprLang[E] extends AnyRef

   Abstraction (as a type class) of a language for mathematical expressions, i.e., of

   Abstraction (as a type class) of a language for mathematical expressions, i.e., of

   * methods for forming expressions, * some basic expressions such as true, false, numbers etc.

   Expression include functions and propositions. However, expressions here need not include sophisticated, and foundation specific, constructions such as inductive types; these should be abstracted separately.

   While the design is based on homotopy type theory, implementations can be with a range of logics or functional languages, for instance HOL or the Wolfram language. All methods are optional, so anything outside a language is just not built.

   This is integrated with and used by many components.

   * As a target for natural language and latex translation. * Bidirectional integration with HoTT implementations: * * terms have such a structure, * * terms can be translated to a language with this structure. * Allows pickling of terms by implementing a formal expression language. * _Goal:_ Bidirectional integration with lean expressions.

9.  trait ExprPatterns[E] extends AnyRef
10.  trait FansiShow[-U] extends AnyRef
11.  trait FoldedTerm[U <: Term with Subs[U]] extends Term
12.  trait FormulaParser[E] extends AnyRef
13.  sealed trait FreeExpr extends AnyRef
14.  case class HoTTParser(ctx: Context = Context.Empty, contextMap: Map[String, Context] = Map()) extends Product with Serializable
15.  trait Inclusion[X[_], Y[_]] extends AnyRef

    inclusion of functors

16.  sealed trait MathExpr extends AnyRef

    Expression in a language to represent terms in HoTT and trees representing them in prose, including partially collapsed trees.

    Expression in a language to represent terms in HoTT and trees representing them in prose, including partially collapsed trees. At the level of structure, we do not make distinctions between words and phrases; the distinction is specific to trees, where a word is a leaf.

    We model expressions that will mostly become Terms in HoTT, mostly following Naproche. At the upper level are sentential phrases. We typically start with a tree that encodes a sentential phrase.

17.  trait MathReader[D, E] extends AnyRef
18.  sealed trait MathText extends AnyRef
19.  trait MathWriter[D, E] extends AnyRef

    Type-class for writing to a document of type D in terms of expressions of type E.

    Type-class for writing to a document of type D in terms of expressions of type E. We can write statements and begin and end blocks. We append to the document, but the document may come with a cursor that allows insertion instead.

20.  trait NestedDoc[T] extends AnyRef
21.  trait OptRestriction[X[_], Y[_]] extends ConeRestriction[X, Y, Option]

    restriction on optional functor

22.  abstract class QuasiInclHList[X, Y, F[_] <: HList] extends QuasiInclusion[X, Y, F]

    inclusion of type Y in F(X) with F(_) an HList

23.  abstract class QuasiInclusion[X, Y, F[_]] extends AnyRef

    inclusion of type Y in F(X)

24.  trait QuasiProjection[X, Y] extends AnyRef

    projection of X onto Y

25.  case class Raw(model: TreeModel) extends MathText with MathExpr with Product with Serializable

    An unparsed tree, the default parse for iterative debugging.

26.  sealed trait Scoped[S] extends AnyRef
27.  sealed trait ShapeTree extends AnyRef
28.  class ShapeTreeFormat extends TermRec[ShapeTree]
29.  trait Statement[E] extends AnyRef

    A statement obtained from source which affects a document.

30.  trait SubType[X[_], Y[_]] extends Inclusion[X, Y] with OptRestriction[X, Y]

    subtype relation between functors, giving inclusion and optional restriction, explicit, not depending on scala type checking

31.  class SubTypePattern[X, Y, F[_]] extends AnyRef

    Pattern and builder for matching whether, for a term x: X, F(x) is in the subtype Y.

    Pattern and builder for matching whether, for a term x: X, F(x) is in the subtype Y. Here Y is not just a scala subtype, but we have inclusions and projections making it a direct summand.

32.  class TermParser extends JavaTokenParsers

33.  trait TermRec[U] extends AnyRef
34.  class TermToExpr[E] extends AnyRef
35.  trait Translator[I, O] extends (I) => Option[O]

    Translator from an input I to an output O, designed to be built recursively.

    Translator from an input I to an output O, designed to be built recursively.

    Translation by Splitting and joining

    The most import class of translators are constructed from

    * a split map I => Option[X], where X is obtained from I by taking Tuples, Lists and sub-types

    * a join map Y => Option[O], where Y is obtained from O structurally, in the same way as X is obtained from I, e.g. X = (I, I) and Y = (O, O).

    However X and Y may involve taking sub-types independently of each other.

    Such a translator splits an input, recursively translates X to Y and combines the result with the join (all steps work optionally).

    Combinations, Basic Translators

    Translators are built by combining others by OrElse, starting with basic translators specified by a function I => Option[O]. One can instead start with an empty translator.

    Note that we can restrict the domain or extend the codomain of a translator by just using it as a function I => Option[O]. However this should be done after making all OrElse combinations, as the wrapped translator does not combine recursively.

    A typical example of usage is as below

    scala> import provingground._
    import provingground._
    
    scala> import translation._, Translator._
    import translation._
    import Translator._
    
    scala> import cats._, cats.implicits._
    import cats._
    import cats.implicits._
    
    scala> class A
    defined class A
    
    scala> case class B(x: A, y: A) extends A
    defined class B
    
    scala> case class C(x: A, y: A) extends A
    defined class C
    
    scala> case object D extends A
    defined object D
    
    scala> import Functors._
    import Functors._
    
    scala> val Bpat = Pattern.partial[A, II]{case B(x, y) => (x, y)}
    
    
    scala> val Dpat = Pattern.partial[A, Un]{case D => ()}
    
    
    scala> case object E extends A
    defined object E
    
    scala> val trans = Translator.Empty[A, A] || Bpat >>> {case (x, y) => C(x,y)} || Dpat >>> {case _ => E}
    trans: provingground.translation.Translator.OrElse[A,A] = <function1>
    
    scala> trans(B(B(D, D), B(B(D, D), D)))
    res0: Option[A] = Some(C(C(E,E),C(C(E,E),E)))
    
    scala> trans(C(D, D))
    res1: Option[A] = None

36.  sealed trait TreeModel extends AnyRef
37.  trait Vocabulary[E, C] extends AnyRef