<commit_before>package provingground
import HoTT._
//import ScalaUniverses._
import math._
import scala.language.existentials

/**
 * @author gadgil
 */
object Families {

  /**
   * A pattern for families, e.g. of inductive types to be defined
   * for instance A -> B -> W, where W is the type to be defined;
   * ends with the type with members.
   * the pattern is a function of the type W.
   *
   */
  sealed trait FmlyPtn[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F]] {
    /**
     * the universe containing the type
     */
    val univLevel: Int

    type Cod = C

    /**
     * scala type (upper bound) for a member of the family, i.e., sections
     */
    type Family = F

    /**
      *  type of the total space, i.e., of W, sections to a universe
      **/
    type FamilyType <: Term with Subs[FamilyType]

    type Total <: Term with Subs[Total]

    /**
      *  Type of Curried function to X.
      **/
    type IterFunc <: Term with Subs[IterFunc]

    /**
      *  Type of curried function to typ[X]
      **/
    type IterTypFunc <: Term with Subs[IterTypFunc]

    type IterDepFunc <: Term with Subs[IterDepFunc]

    def iterFuncTyp(w: FamilyType, x: Typ[Cod]): Typ[IterFunc]

    def iterDepFuncTyp(w: FamilyType, xs: IterTypFunc): Typ[IterDepFunc]

    def domTotal(w: FamilyType) : Typ[Total]

//    def contract(f: Family)(arg: ArgType): O

    def fill(g: IterFunc)(arg: ArgType): Func[O, C]

    def depFill(g: IterDepFunc)(arg: ArgType) : FuncLike[O, C]

    def curry(f: Func[Total, Cod]): IterFunc

    def totalDomain(g: IterFunc) : Typ[Total]

    def uncurry(g: IterFunc) : Func[Total, Cod]

    def depCurry(f: FuncLike[Total, Cod]): IterDepFunc

    def depTotalDomain(g: IterDepFunc) : Typ[Total]

    def depUncurry(g: IterDepFunc) : FuncLike[Total, Cod]

    def contractType(w: FamilyType)(arg: ArgType): Typ[O]

//    def collapse(mem: PairObj[Family, ArgType]) = contract(mem.first)(mem.second)

    /**
      *  type of total index
      **/
    type ArgType <: Term with Subs[ArgType]

    /**
     * scala type of target for induced functions, i.e., with O = Term
     */
    type TargetType <: Term with Subs[TargetType]

    /**
      * Note that the target may be a type family, not a type,
      *  so this is the actual type of objects.
      */
    type DepTargetType <: Term with Subs[DepTargetType]

    /**
     * returns the type corresponding to the pattern, such as A -> W, given the (inductive) type W,
      *  this is used mainly for constructor patterns, with the W being fixed, not for genuine families.
     */
    def apply(tp: Typ[O]): Typ[Family]

    def target(x: Typ[Cod]): Typ[TargetType]

    def depTarget(xs: Func[O, Typ[Cod]]): Family => Typ[DepTargetType]


    def withCod[CC <: Term with Subs[CC]]: FmlyPtn[O, CC, Family]

    /**
     * function induced by f: W -> X of type (A -> W) -> (A -> X) etc
     *
     * @param f function from which to induce
     *
     * @param W the inductive type
     *
     * @param X codomain of the given function
     */
    def induced(f: Func[O, Cod]): Family => TargetType

    /**
     * dependent function induced by dependent f: W -> X(s) of type (A -> W) -> ((a : A) ~> Xs(a)) etc
     *
     * @param f dependent function from which to induce
     *
     * @param W the inductive type
     *
     * @param Xs family of codomains of the given dependent function
     */
    def inducedDep(f: FuncLike[O, Cod]): Family => DepTargetType
  }

  object FmlyPtn{
    def get[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F]](typ: Typ[O])(fmlyTyp: Typ[F]) : FmlyPtn[O, C, F]  =
      fmlyTyp match {
        case `typ` => IdFmlyPtn[O, C].asInstanceOf[FmlyPtn[O, C, F]]
        case FuncTyp(dom : Typ[u], codom : Typ[v]) =>
          val head = get[O, C, v](typ)(codom)
          val tail = dom
          val headCast: FmlyPtn[O,C,v]{
            type FamilyType = head.FamilyType;
            type IterFunc = head.IterFunc;
            type IterTypFunc = head.IterTypFunc;
            type IterDepFunc = head.IterDepFunc;
            type ArgType = head.ArgType; type TargetType = head.TargetType;
            type DepTargetType = head.DepTargetType;
            type Total = head.Total} = head
          val funcFmlyPtn = FuncFmlyPtn(tail, headCast)
          funcFmlyPtn.asInstanceOf[FmlyPtn[O, C, F]]
/*        case tp: PiTyp[u, v] =>
          val fibre = tp.fibers
          val tail = fibre.dom
          val a = tail.Var
          val headfibre = fibre(a)
          val newHead = headfibre(tail.symbObj(Star))
          type VV = newHead.Family
          type FVV = newHead.FamilyType
          type SS = newHead.ArgType
          type TTT = newHead.TargetType
          type DD = newHead.DepTargetType
          val newHeadFibre = (t: Term) =>
            (
              headfibre(t).withCod[CC].asInstanceOf[FmlyPtn[O, CC, VV] {
                type FamilyType = FVV;
                type IterFunc = I;
                type IterTypFunc = IT;
                type IterDepFunc = DI;
                type ArgType = SS;
                type TargetType = TTT; type DepTargetType = DD;
                type Total = HTot
              }]
            )
          DepFuncFmlyPtn[u, VV, FVV, I, IT, DI, SS, TTT, DD, O, CC, HTot](tail, newHeadFibre)
            ???
            */
      }
  }

  /**
   * The identity family
   */
  case class IdFmlyPtn[O <: Term with Subs[O], C <: Term with Subs[C]]() extends FmlyPtn[O, C, O] {
    def apply(W: Typ[O]) = W

    //    type Family =  O

    type FamilyType = Typ[O]

    type Total = O

    type IterFunc = Func[O, C]

    type IterTypFunc = Func[O, Typ[C]]

    type IterDepFunc = FuncLike[O, C]
<commit_msg>Reading families from types; should try to clean up FuncFmlyPtn (make type parameters internal)<commit_after>package provingground
import HoTT._
//import ScalaUniverses._
import math._
import scala.language.existentials

/**
 * @author gadgil
 */
object Families {

  /**
   * A pattern for families, e.g. of inductive types to be defined
   * for instance A -> B -> W, where W is the type to be defined;
   * ends with the type with members.
   * the pattern is a function of the type W.
   *
   */
  sealed trait FmlyPtn[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F]] {
    /**
     * the universe containing the type
     */
    val univLevel: Int

    type Cod = C

    /**
     * scala type (upper bound) for a member of the family, i.e., sections
     */
    type Family = F

    /**
      *  type of the total space, i.e., of W, sections to a universe
      **/
    type FamilyType <: Term with Subs[FamilyType]

    type Total <: Term with Subs[Total]

    /**
      *  Type of Curried function to X.
      **/
    type IterFunc <: Term with Subs[IterFunc]

    /**
      *  Type of curried function to typ[X]
      **/
    type IterTypFunc <: Term with Subs[IterTypFunc]

    type IterDepFunc <: Term with Subs[IterDepFunc]

    def iterFuncTyp(w: FamilyType, x: Typ[Cod]): Typ[IterFunc]

    def iterDepFuncTyp(w: FamilyType, xs: IterTypFunc): Typ[IterDepFunc]

    def domTotal(w: FamilyType) : Typ[Total]

//    def contract(f: Family)(arg: ArgType): O

    def fill(g: IterFunc)(arg: ArgType): Func[O, C]

    def depFill(g: IterDepFunc)(arg: ArgType) : FuncLike[O, C]

    def curry(f: Func[Total, Cod]): IterFunc

    def totalDomain(g: IterFunc) : Typ[Total]

    def uncurry(g: IterFunc) : Func[Total, Cod]

    def depCurry(f: FuncLike[Total, Cod]): IterDepFunc

    def depTotalDomain(g: IterDepFunc) : Typ[Total]

    def depUncurry(g: IterDepFunc) : FuncLike[Total, Cod]

    def contractType(w: FamilyType)(arg: ArgType): Typ[O]

//    def collapse(mem: PairObj[Family, ArgType]) = contract(mem.first)(mem.second)

    /**
      *  type of total index
      **/
    type ArgType <: Term with Subs[ArgType]

    /**
     * scala type of target for induced functions, i.e., with O = Term
     */
    type TargetType <: Term with Subs[TargetType]

    /**
      * Note that the target may be a type family, not a type,
      *  so this is the actual type of objects.
      */
    type DepTargetType <: Term with Subs[DepTargetType]

    /**
     * returns the type corresponding to the pattern, such as A -> W, given the (inductive) type W,
      *  this is used mainly for constructor patterns, with the W being fixed, not for genuine families.
     */
    def apply(tp: Typ[O]): Typ[Family]

    def target(x: Typ[Cod]): Typ[TargetType]

    def depTarget(xs: Func[O, Typ[Cod]]): Family => Typ[DepTargetType]


    def withCod[CC <: Term with Subs[CC]]: FmlyPtn[O, CC, Family]

    /**
     * function induced by f: W -> X of type (A -> W) -> (A -> X) etc
     *
     * @param f function from which to induce
     *
     * @param W the inductive type
     *
     * @param X codomain of the given function
     */
    def induced(f: Func[O, Cod]): Family => TargetType

    /**
     * dependent function induced by dependent f: W -> X(s) of type (A -> W) -> ((a : A) ~> Xs(a)) etc
     *
     * @param f dependent function from which to induce
     *
     * @param W the inductive type
     *
     * @param Xs family of codomains of the given dependent function
     */
    def inducedDep(f: FuncLike[O, Cod]): Family => DepTargetType
  }

  object FmlyPtn{
    def get[O <: Term with Subs[O], C <: Term with Subs[C], F <: Term with Subs[F]](typ: Typ[O])(fmlyTyp: Typ[F]) : FmlyPtn[O, C, F]  =
      fmlyTyp match {
        case `typ` => IdFmlyPtn[O, C].asInstanceOf[FmlyPtn[O, C, F]]
        case FuncTyp(dom : Typ[u], codom : Typ[v]) =>
          val head = get[O, C, v](typ)(codom)
          val tail = dom
          val headCast: FmlyPtn[O,C,v]{
            type FamilyType = head.FamilyType;
            type IterFunc = head.IterFunc;
            type IterTypFunc = head.IterTypFunc;
            type IterDepFunc = head.IterDepFunc;
            type ArgType = head.ArgType; type TargetType = head.TargetType;
            type DepTargetType = head.DepTargetType;
            type Total = head.Total} = head
          val funcFmlyPtn = FuncFmlyPtn(tail, headCast)
          funcFmlyPtn.asInstanceOf[FmlyPtn[O, C, F]]
        case tp: PiTyp[u, v] =>
          val fibre = tp.fibers
          val tail = fibre.dom
          val a = tail.Var
          val headfibre = (x: u) =>
            get[O, C, v](typ)(fibre(x))
          val newHead = headfibre(tail.symbObj(Star))
          type VV = newHead.Family
          type I = newHead.IterFunc
          type IT = newHead.IterTypFunc
          type DI = newHead.IterDepFunc
          type FVV = newHead.FamilyType
          type SS = newHead.ArgType
          type TTT = newHead.TargetType
          type DD = newHead.DepTargetType
          type HTot = newHead.Total
          val newHeadFibre = (t: u) =>
            (
              headfibre(t).asInstanceOf[FmlyPtn[O, C, VV] {
                type FamilyType = FVV;
                type IterFunc = I;
                type IterTypFunc = IT;
                type IterDepFunc = DI;
                type ArgType = SS;
                type TargetType = TTT; type DepTargetType = DD;
                type Total = HTot
              }]
            )
          DepFuncFmlyPtn(tail, newHeadFibre).asInstanceOf[FmlyPtn[O, C, F]]
      }
  }

  /**
   * The identity family
   */
  case class IdFmlyPtn[O <: Term with Subs[O], C <: Term with Subs[C]]() extends FmlyPtn[O, C, O] {
    def apply(W: Typ[O]) = W

    //    type Family =  O

    type FamilyType = Typ[O]

    type Total = O

    type IterFunc = Func[O, C]

    type IterTypFunc = Func[O, Typ[C]]

    type IterDepFunc = FuncLike[O, C]

{'fraction_non_alphanumeric': 0.11678957297204597, 'fraction_numerical': 0.0, 'mean_word_length': 2.17619825708061, 'pattern_counts': {'":': 0, '<': 37, '<?xml version=': 0, '>': 40, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '4433792', 'n_tokens_mistral': 4029, 'n_tokens_neox': 3857, 'n_words': 1212}