<commit_before>package edu.tum.cs.isabelle

import scala.concurrent.{ExecutionContext, Future}
import scala.math.BigInt

import edu.tum.cs.isabelle.pure._

import acyclic.file

private class ListTypeable[T : Typeable] extends Typeable[List[T]] {
  def typ: Typ = Type("List.list", List(Typeable.typ[T]))
}

trait LowPriorityImplicits {

  implicit def listTypeable[T : Typeable]: Typeable[List[T]] = new ListTypeable[T]

}

package object hol extends LowPriorityImplicits {

  private val MkInt = Operation.implicitly[BigInt, Term]("mk_int")
  private val MkList = Operation.implicitly[(Typ, List[Term]), Term]("mk_list")

  implicit def bigIntTypeable: Embeddable[BigInt] = new Embeddable[BigInt] {
    def typ: Typ = Type("Int.int", Nil)
    def embed(thy: Theory, t: BigInt)(implicit ec: ExecutionContext): Future[Term] =
      thy.system.invoke(MkInt)(t) map {
        case ProverResult.Failure(exn) => throw exn
        case ProverResult.Success(t) => t
      }
  }

  implicit def boolTypeable: Embeddable[Boolean] = new Embeddable[Boolean] {
    def typ: Typ = Type("HOL.bool", Nil)
    def embed(thy: Theory, t: Boolean)(implicit ec: ExecutionContext): Future[Term] = Future.successful {
      t match {
        case true => Const("HOL.True", typ)
        case false => Const("HOL.False", typ)
      }
    }
  }

  implicit def listEmbeddable[T : Embeddable]: Embeddable[List[T]] = new ListTypeable[T] with Embeddable[List[T]] {
    def embed(thy: Theory, ts: List[T])(implicit ec: ExecutionContext): Future[Term] =
      Future.traverse(ts)(Embeddable[T].embed(thy, _)) flatMap { ts =>
        thy.system.invoke(MkList)((Typeable.typ[T], ts))
      } map {
        case ProverResult.Failure(exn) => throw exn
        case ProverResult.Success(t) => t
      }
  }

}
<commit_msg>put auxiliary classes into `hol` package<commit_after>package edu.tum.cs.isabelle

import scala.concurrent.{ExecutionContext, Future}
import scala.math.BigInt

import edu.tum.cs.isabelle.pure._

import acyclic.file

package hol {
  private class ListTypeable[T : Typeable] extends Typeable[List[T]] {
    def typ: Typ = Type("List.list", List(Typeable.typ[T]))
  }

  private[isabelle] trait LowPriorityImplicits {
    implicit def listTypeable[T : Typeable]: Typeable[List[T]] = new ListTypeable[T]
  }
}

package object hol extends LowPriorityImplicits {

  private val MkInt = Operation.implicitly[BigInt, Term]("mk_int")
  private val MkList = Operation.implicitly[(Typ, List[Term]), Term]("mk_list")

  implicit def bigIntTypeable: Embeddable[BigInt] = new Embeddable[BigInt] {
    def typ: Typ = Type("Int.int", Nil)
    def embed(thy: Theory, t: BigInt)(implicit ec: ExecutionContext): Future[Term] =
      thy.system.invoke(MkInt)(t) map {
        case ProverResult.Failure(exn) => throw exn
        case ProverResult.Success(t) => t
      }
  }

  implicit def boolTypeable: Embeddable[Boolean] = new Embeddable[Boolean] {
    def typ: Typ = Type("HOL.bool", Nil)
    def embed(thy: Theory, t: Boolean)(implicit ec: ExecutionContext): Future[Term] = Future.successful {
      t match {
        case true => Const("HOL.True", typ)
        case false => Const("HOL.False", typ)
      }
    }
  }

  implicit def listEmbeddable[T : Embeddable]: Embeddable[List[T]] = new ListTypeable[T] with Embeddable[List[T]] {
    def embed(thy: Theory, ts: List[T])(implicit ec: ExecutionContext): Future[Term] =
      Future.traverse(ts)(Embeddable[T].embed(thy, _)) flatMap { ts =>
        thy.system.invoke(MkList)((Typeable.typ[T], ts))
      } map {
        case ProverResult.Failure(exn) => throw exn
        case ProverResult.Success(t) => t
      }
  }

}

{'fraction_non_alphanumeric': 0.1355281207133059, 'fraction_numerical': 0.0, 'mean_word_length': 3.8163804491413473, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 17, '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': '7049254', 'n_tokens_mistral': 1271, 'n_tokens_neox': 1260, 'n_words': 278}