<commit_before>package provingground

import HoTT._
//import scala.language.existentials

trait RecursiveCaseDefinition[H <: Term with Subs[H], C <: Term with Subs[C]] extends Func[H, C] { self =>
  def caseFn(f: => Func[H, C])(arg: H): Option[C]

  def act(arg: H) = {
    caseFn(self)(arg) getOrElse codom.symbObj(ApplnSym(self, arg))
  }

  def subs(x: Term, y: Term): RecursiveCaseDefinition[H, C]
}

object RecursiveCaseDefinition {
  case class Empty[H <: Term with Subs[H], C <: Term with Subs[C]](
    dom: Typ[H], codom: Typ[C]
  ) extends RecursiveCaseDefinition[H, C] {
    val typ = dom ->: codom

    def subs(x: Term, y: Term) = Empty(dom.replace(x, y), codom.replace(x, y))

    def newobj = Empty(dom.newobj, codom.newobj)

    def caseFn(f: => Func[H, C])(arg: H): Option[C] = None
  }

  case class DataCons[H <: Term with Subs[H], C <: Term with Subs[C], D <: Term with Subs[D]](
    data: D,
    defn: D => Func[H, C] => H => Option[C],
    tail: RecursiveCaseDefinition[H, C]
  ) extends RecursiveCaseDefinition[H, C] {
    val dom = tail.dom

    val codom = tail.codom

    val typ = dom ->: codom

    def newobj = DataCons(data.newobj, defn, tail)

    def subs(x: Term, y: Term) =
      DataCons(data.replace(x, y), defn, tail.subs(x, y))

    def caseFn(f: => Func[H, C])(arg: H): Option[C] =
      defn(data)(f)(arg) orElse (tail.caseFn(f)(arg))
  }

  def sym[C <: Term with Subs[C], H <: Term with Subs[H]](cons: Constructor[C, H]) = Constructor.Sym(cons)

  //for experimentation, should actually chain constructors.
  def constructorFunc[H <: Term with Subs[H], C <: Term with Subs[C]](
    cons: Constructor[C, H], X: Typ[C], tail: RecursiveCaseDefinition[H, C]
  ) =
    {
      val data: cons.pattern.RecDataType = cons.pattern.recDom(cons.W, X).symbObj(sym(cons))
      val defn = (d: cons.pattern.RecDataType) => (f: Func[H, C]) => cons.pattern.recDef(cons.cons, d, f)
      val fn: Func[H, C] = DataCons(data, defn, tail)
      lmbda(data)(fn)
    }

}

trait ConstructorSeq[C <: Term with Subs[C], H <: Term with Subs[H]] {
  val recCaseDefn: RecursiveCaseDefinition[H, C]

  val W: Typ[H]

  val X: Typ[C]

  type RecType <: Term with Subs[RecType]

  val rec : RecType

  def ::(head: Constructor[C, H]) = ConstructorSeq.Cons(head, this)
}

object ConstructorSeq {
  case class Empty[C <: Term with Subs[C], H <: Term with Subs[H]](W: Typ[H], X: Typ[C]) extends ConstructorSeq[C, H] {
    val recCaseDefn = RecursiveCaseDefinition.Empty(W, X)

    type RecType = Func[H, C]

    val rec : Func[H, C] = recCaseDefn
  }

  case class Cons[C <: Term with Subs[C], H <: Term with Subs[H]](
    cons: Constructor[C, H], tail: ConstructorSeq[C, H]
  ) extends ConstructorSeq[C, H] {

    val W = tail.W

    val X = tail.X

    val data: cons.pattern.RecDataType = cons.pattern.recDom(cons.W, X).symbObj(Constructor.Sym(cons))

    val defn = (d: cons.pattern.RecDataType) => (f: Func[H, C]) => cons.pattern.recDef(cons.cons, d, f)

    val recCaseDefn = RecursiveCaseDefinition.DataCons(data, defn, tail.recCaseDefn)

    type RecType = Func[cons.pattern.RecDataType, tail.RecType]

    val rec = lmbda(data)(tail.rec)
  }

  def fold[C<: Term with Subs[C], H<: Term with Subs[H]](
    W: Typ[H], X: Typ[C]): List[Constructor[C, H]] => ConstructorSeq[C, H] = {
      case List() => ConstructorSeq.Empty(W, X)
      case head :: tail => ConstructorSeq.Cons(head, fold(W, X)(tail))
    }

  def recFn[C<: Term with Subs[C], H<: Term with Subs[H]](
    W: Typ[H], X: Typ[C])(cs: List[Constructor[C, H]]) = fold(W, X)(cs).rec

}
<commit_msg>corrections to recursion reworked<commit_after>package provingground

import HoTT._
//import scala.language.existentials

trait RecursiveCaseDefinition[H <: Term with Subs[H], C <: Term with Subs[C]] extends Func[H, C] { self =>
  def caseFn(f: => Func[H, C])(arg: H): Option[C]

  def act(arg: H) = {
    caseFn(self)(arg) getOrElse codom.symbObj(ApplnSym(self, arg))
  }

  def subs(x: Term, y: Term): RecursiveCaseDefinition[H, C]
}

object RecursiveCaseDefinition {
  case class Empty[H <: Term with Subs[H], C <: Term with Subs[C]](
    dom: Typ[H], codom: Typ[C]
  ) extends RecursiveCaseDefinition[H, C] {
    val typ = dom ->: codom

    def subs(x: Term, y: Term) = Empty(dom.replace(x, y), codom.replace(x, y))

    def newobj = Empty(dom.newobj, codom.newobj)

    def caseFn(f: => Func[H, C])(arg: H): Option[C] = None
  }

  case class DataCons[H <: Term with Subs[H], C <: Term with Subs[C], D <: Term with Subs[D]](
    data: D,
    defn: D => Func[H, C] => H => Option[C],
    tail: RecursiveCaseDefinition[H, C]
  ) extends RecursiveCaseDefinition[H, C] {
    val dom = tail.dom

    val codom = tail.codom

    val typ = dom ->: codom

    def newobj = DataCons(data.newobj, defn, tail)

    def subs(x: Term, y: Term) =
      DataCons(data.replace(x, y), defn, tail.subs(x, y))

    def caseFn(f: => Func[H, C])(arg: H): Option[C] =
      defn(data)(f)(arg) orElse (tail.caseFn(f)(arg))
  }

  def sym[C <: Term with Subs[C], H <: Term with Subs[H]](cons: Constructor[C, H]) = Constructor.Sym(cons)

  //for experimentation, should actually chain constructors.
  def constructorFunc[H <: Term with Subs[H], C <: Term with Subs[C]](
    cons: Constructor[C, H], X: Typ[C], tail: RecursiveCaseDefinition[H, C]
  ) =
    {
      val data: cons.pattern.RecDataType = cons.pattern.recDom(cons.W, X).symbObj(sym(cons))
      val defn = (d: cons.pattern.RecDataType) => (f: Func[H, C]) => cons.pattern.recDef(cons.cons, d, f)
      val fn: Func[H, C] = DataCons(data, defn, tail)
      lmbda(data)(fn)
    }

}

trait ConstructorSeq[C <: Term with Subs[C], H <: Term with Subs[H]] {
  val recCaseDefn: RecursiveCaseDefinition[H, C]

  val W: Typ[H]

  val X: Typ[C]

  type RecType <: Term with Subs[RecType]

  def polyLambda : Func[H, C] => RecType

  lazy val rec : RecType = polyLambda(recCaseDefn)

  def ::(head: Constructor[C, H]) = ConstructorSeq.Cons(head, this)
}

object ConstructorSeq {
  case class Empty[C <: Term with Subs[C], H <: Term with Subs[H]](W: Typ[H], X: Typ[C]) extends ConstructorSeq[C, H] {
    val recCaseDefn = RecursiveCaseDefinition.Empty(W, X)

    type RecType = Func[H, C]

    def polyLambda = (f) => f

//    val rec : Func[H, C] = recCaseDefn
  }

  case class Cons[C <: Term with Subs[C], H <: Term with Subs[H]](
    cons: Constructor[C, H], tail: ConstructorSeq[C, H]
  ) extends ConstructorSeq[C, H] {

    val W = tail.W

    val X = tail.X

    val data: cons.pattern.RecDataType = cons.pattern.recDom(cons.W, X).symbObj(Constructor.Sym(cons))

    val defn = (d: cons.pattern.RecDataType) => (f: Func[H, C]) => cons.pattern.recDef(cons.cons, d, f)

    val recCaseDefn = RecursiveCaseDefinition.DataCons(data, defn, tail.recCaseDefn)

    type RecType = Func[cons.pattern.RecDataType, tail.RecType]

    def polyLambda = f => lmbda(data)(tail.polyLambda(f))

//    val rec = lmbda(data)(tail.rec) //FIXME wrong
  }

  def fold[C<: Term with Subs[C], H<: Term with Subs[H]](
    W: Typ[H], X: Typ[C]): List[Constructor[C, H]] => ConstructorSeq[C, H] = {
      case List() => ConstructorSeq.Empty(W, X)
      case head :: tail => ConstructorSeq.Cons(head, fold(W, X)(tail))
    }

  def recFn[C<: Term with Subs[C], H<: Term with Subs[H]](
    cs: List[Constructor[C, H]], W: Typ[H], X: Typ[C]) = fold(W, X)(cs).rec

}

{'fraction_non_alphanumeric': 0.16809582142371035, 'fraction_numerical': 0.0, 'mean_word_length': 3.5724953329184816, 'pattern_counts': {'":': 0, '<': 47, '<?xml version=': 0, '>': 38, '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': '3226920', 'n_tokens_mistral': 2941, 'n_tokens_neox': 2882, 'n_words': 745}