<commit_before>package leo
package datastructures

import leo.datastructures.impl.Signature

import Term.{:::>, TypeLambda,∙,Symbol, Bound}

import scala.annotation.tailrec

/**
 * Collection of Ordering relations of terms, clauses, etc.
 *
 * @author <NAME>
 * @since 20.08.14
 */
/////////////////////
// Ordering related library functions
/////////////////////

object Orderings {
  import scala.language.implicitConversions

  def isComparable(x: CompareResult): Boolean = (x & ~(CMP_EQ | CMP_UK)) != 0
  def isGE(x: CompareResult): Boolean = (x & (CMP_EQ | CMP_GT)) != 0
  def isLE(x: CompareResult): Boolean = (x & (CMP_EQ | CMP_LT)) != 0

  /** Return a (simple) ordering that is induced by a weighting. */
  def simple[A](weighting: Weight[A]) = new Ordering[A] {
    def compare(a: A, b: A) = weighting.weightOf(a) - weighting.weightOf(b)
  }

  val intOrd = new Ordering[Int] {
    def compare(a: Int, b: Int) = a-b
  }

  def lift[A](f: A => A => Int): Ordering[A] = new Ordering[A] {
    def compare(x: A, y: A) = f(x)(y)
  }
  def lift[A](f:  (A,A) => Option[Int]): QuasiOrdering[A] = new QuasiOrdering[A] {
    def compare(x: A, y: A) = f(x,y)
  }

  def productOrd[A,B](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B]): QuasiOrdering[(A,B)] = new QuasiOrdering[(A, B)] {
    def compare(x: (A, B), y: (A, B)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2)
      case res => res
    }
  }
  def productOrd[A,B,C](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B], ordC: QuasiOrdering[C]): QuasiOrdering[(A,B,C)] = new QuasiOrdering[(A, B, C)] {
    def compare(x: (A, B, C), y: (A, B, C)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2) match {
        case Some(0) => ordC.compare(x._3, y._3)
        case res => res
      }
      case res => res
    }
  }
  def productOrd[A,B,C,D](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B], ordC: QuasiOrdering[C], ordD: QuasiOrdering[D]): QuasiOrdering[(A,B,C,D)] = new QuasiOrdering[(A, B, C,D)] {
    def compare(x: (A, B, C,D), y: (A, B, C,D)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2) match {
        case Some(0) => ordC.compare(x._3, y._3) match {
          case Some(0) => ordD.compare(x._4, y._4)
          case res => res
        }
        case res => res
      }
      case res => res
    }
  }

  def lexOrd[A](ord: QuasiOrdering[A]): QuasiOrdering[Seq[A]] = new QuasiOrdering[Seq[A]] {
    def compare(x: Seq[A], y: Seq[A]) = (x.length - y.length) match {
      case 0 => (x,y) match {
        case (Seq(), Seq()) => Some(0)
        case (Seq(xHead, xTail@_*), Seq(yHead, yTail@_*)) => ord.compare(xHead, yHead) match {
          case Some(0) => compare(xTail, yTail)
          case res => res
        }
      }
      case res => Some(res)
    }
  }

  implicit def toQuasiOrdering[A](ord: Ordering[A]): QuasiOrdering[A] = new QuasiOrdering[A] {
    def compare(x: A, y: A) = Some(ord.compare(x,y))
  }
}


/////////////////////
// Precedences
/////////////////////

trait Precedence {
  type Const = Signature#Key
  def compare(x: Const, y: Const): CMP_Result
  def gt(x: Const, y: Const): Boolean = compare(x,y) == CMP_GT
  def ge(x: Const, y: Const): Boolean = compare(x,y) == CMP_GT || compare(x,y) == CMP_EQ
  def lt(x: Const, y: Const): Boolean = compare(x,y) == CMP_LT
  def le(x: Const, y: Const): Boolean = compare(x,y) == CMP_LT || compare(x,y) == CMP_EQ

  protected final def intToCMPRes(x: Int, y: Int): CMP_Result = {
    if (x > y) CMP_GT
    else if (x < y) CMP_LT
    else CMP_EQ
  }
}

object Precedence {
  import leo.datastructures.impl.precedences._
  final val sigInduced: Precedence = Prec_SigInduced
  final val arity: Precedence = Prec_Arity
  final val arity_UnaryFirst: Precedence = Prec_Arity_UnaryFirst
  final val arityOrder: Precedence = Prec_ArityOrder
  final val arityOrder_UnaryFirst: Precedence = Prec_ArityOrder_UnaryFirst
}

///////////////////////
/// Term Orderings
///////////////////////

object TermOrdering {
  import leo.datastructures.impl.orderings._
  final val senseless: TermOrdering = TO_SenselessOrdering
  final val sizeBased: TermOrdering = TO_SizedBased
}

/////////////////////
// Clause Orderings
/////////////////////

object ClauseOrdering {
  import leo.datastructures.impl.orderings._
  /** Lexicographic clause ordering on the 3-tuple (clause weight, clause age, clause origin) */
  final val lex_WeightAgeOrigin: ClauseOrdering = CLO_Lex_WeightAgeOrigin
}

///////////////////////
/// Type Orderings
///////////////////////

<commit_msg>added new precedence to access object<commit_after>package leo
package datastructures

import leo.datastructures.impl.Signature

import Term.{:::>, TypeLambda,∙,Symbol, Bound}

import scala.annotation.tailrec

/**
 * Collection of Ordering relations of terms, clauses, etc.
 *
 * @author <NAME>
 * @since 20.08.14
 */
/////////////////////
// Ordering related library functions
/////////////////////

object Orderings {
  import scala.language.implicitConversions

  def isComparable(x: CompareResult): Boolean = (x & ~(CMP_EQ | CMP_UK)) != 0
  def isGE(x: CompareResult): Boolean = (x & (CMP_EQ | CMP_GT)) != 0
  def isLE(x: CompareResult): Boolean = (x & (CMP_EQ | CMP_LT)) != 0

  /** Return a (simple) ordering that is induced by a weighting. */
  def simple[A](weighting: Weight[A]) = new Ordering[A] {
    def compare(a: A, b: A) = weighting.weightOf(a) - weighting.weightOf(b)
  }

  val intOrd = new Ordering[Int] {
    def compare(a: Int, b: Int) = a-b
  }

  def lift[A](f: A => A => Int): Ordering[A] = new Ordering[A] {
    def compare(x: A, y: A) = f(x)(y)
  }
  def lift[A](f:  (A,A) => Option[Int]): QuasiOrdering[A] = new QuasiOrdering[A] {
    def compare(x: A, y: A) = f(x,y)
  }

  def productOrd[A,B](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B]): QuasiOrdering[(A,B)] = new QuasiOrdering[(A, B)] {
    def compare(x: (A, B), y: (A, B)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2)
      case res => res
    }
  }
  def productOrd[A,B,C](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B], ordC: QuasiOrdering[C]): QuasiOrdering[(A,B,C)] = new QuasiOrdering[(A, B, C)] {
    def compare(x: (A, B, C), y: (A, B, C)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2) match {
        case Some(0) => ordC.compare(x._3, y._3)
        case res => res
      }
      case res => res
    }
  }
  def productOrd[A,B,C,D](ordA: QuasiOrdering[A], ordB: QuasiOrdering[B], ordC: QuasiOrdering[C], ordD: QuasiOrdering[D]): QuasiOrdering[(A,B,C,D)] = new QuasiOrdering[(A, B, C,D)] {
    def compare(x: (A, B, C,D), y: (A, B, C,D)) = ordA.compare(x._1, y._1) match {
      case Some(0) => ordB.compare(x._2, y._2) match {
        case Some(0) => ordC.compare(x._3, y._3) match {
          case Some(0) => ordD.compare(x._4, y._4)
          case res => res
        }
        case res => res
      }
      case res => res
    }
  }

  def lexOrd[A](ord: QuasiOrdering[A]): QuasiOrdering[Seq[A]] = new QuasiOrdering[Seq[A]] {
    def compare(x: Seq[A], y: Seq[A]) = (x.length - y.length) match {
      case 0 => (x,y) match {
        case (Seq(), Seq()) => Some(0)
        case (Seq(xHead, xTail@_*), Seq(yHead, yTail@_*)) => ord.compare(xHead, yHead) match {
          case Some(0) => compare(xTail, yTail)
          case res => res
        }
      }
      case res => Some(res)
    }
  }

  implicit def toQuasiOrdering[A](ord: Ordering[A]): QuasiOrdering[A] = new QuasiOrdering[A] {
    def compare(x: A, y: A) = Some(ord.compare(x,y))
  }
}


/////////////////////
// Precedences
/////////////////////

trait Precedence {
  type Const = Signature#Key
  def compare(x: Const, y: Const): CMP_Result
  def gt(x: Const, y: Const): Boolean = compare(x,y) == CMP_GT
  def ge(x: Const, y: Const): Boolean = compare(x,y) == CMP_GT || compare(x,y) == CMP_EQ
  def lt(x: Const, y: Const): Boolean = compare(x,y) == CMP_LT
  def le(x: Const, y: Const): Boolean = compare(x,y) == CMP_LT || compare(x,y) == CMP_EQ

  protected final def intToCMPRes(x: Int, y: Int): CMP_Result = {
    if (x > y) CMP_GT
    else if (x < y) CMP_LT
    else CMP_EQ
  }
}

object Precedence {
  import leo.datastructures.impl.precedences._
  final val sigInduced: Precedence = Prec_SigInduced
  final val arity: Precedence = Prec_Arity
  final val arity_UnaryFirst: Precedence = Prec_Arity_UnaryFirst
  final val arityOrder: Precedence = Prec_ArityOrder
  final val arityOrder_UnaryFirst: Precedence = Prec_ArityOrder_UnaryFirst
  final val arityInvOrder_UnaryFirst: Precedence = Prec_ArityInvOrder_UnaryFirst
}

///////////////////////
/// Term Orderings
///////////////////////

object TermOrdering {
  import leo.datastructures.impl.orderings._
  final val senseless: TermOrdering = TO_SenselessOrdering
  final val sizeBased: TermOrdering = TO_SizedBased
}

/////////////////////
// Clause Orderings
/////////////////////

object ClauseOrdering {
  import leo.datastructures.impl.orderings._
  /** Lexicographic clause ordering on the 3-tuple (clause weight, clause age, clause origin) */
  final val lex_WeightAgeOrigin: ClauseOrdering = CLO_Lex_WeightAgeOrigin
}

///////////////////////
/// Type Orderings
///////////////////////


{'fraction_non_alphanumeric': 0.19522213814722733, 'fraction_numerical': 0.007999135228623933, 'mean_word_length': 2.785597381342062, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 51, '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': '5929894', 'n_tokens_mistral': 3530, 'n_tokens_neox': 3437, 'n_words': 848}