<commit_before>package leo.datastructures

import Term.{intToBoundVar, intsToBoundVar, mkApp, mkAtom, mkTermAbs, mkTermApp, Λ,Symbol,∙}
import Type.{superKind, typeKind, typeVarToType}
import leo.datastructures.impl.Signature

import scala.language.implicitConversions

/** This type can be mixed-in to supply standard higher-order logic symbol definitions, including
 *
 *  1. Fixed (interpreted) symbols
 *  2. Defined symbols
 *  3. Standard base types
 *
 * These symbols must be inserted into the signature before all other symbols and in the order described below.
 *
 * Details:
 * It defines eight fixed symbols ($true, $false, #box, #diamond, ~, !, |, =),
 * eight defined symbols (?, &, =>, <=, <=>, ~|, ~&, <~>) and three types/kinds ($o, $i, *)
 * @author <NAME>
 * @since 02.05.2014
 * @note Updated 24.June 2014: Added remaining connectives from TPTP: ~|,~&, <~>
  *                            Added trait for binary/unary connectives
 */
trait HOLSignature {
  ////////////////////////////////
  // Hard wired fixed keys
  ////////////////////////////////
  val oKey = 1
  val o = Type.mkType(oKey)

  val iKey = 2
  val i = Type.mkType(iKey)

  val realKey = 3
  val real = Type.mkType(realKey)

  val ratKey = 4
  val rat = Type.mkType(ratKey)

  val intKey = 5
  val int = Type.mkType(intKey)

  val letKey = HOLSignature.letKey
  val iteKey = HOLSignature.iteKey

  // Don't change the order of the elements in this lists.
  // If you do so, you may need to update the Signature implementation.

  // Built-in types
  val types = List(("$tType", superKind), // Key 0
    ("$o", typeKind), // Key 1
    ("$i", typeKind), // Key 2
    ("$real", typeKind), // key 3
    ("$rat", typeKind), // Key 4
    ("$int", typeKind)) // Key 5

  // Fixed symbols
  import Type.{mkPolyType => forall}
  lazy val fixedConsts = List(("$true", o), // Key 6
    ("$false",                        o), // Key 7
    ("#box",                    o ->: o), // Key 8
    ("#diamond",                o ->: o), // Key 9
    ("~",                       o ->: o), // Key 10
    ("!",        forall((1 ->: o) ->: o)), // Key 11
    ("|",                 o ->: o ->: o), // Key 12
    ("=",        forall(1 ->: 1 ->: o)), // Key 13
    ("$$let",    forall(forall(2 ->: 1 ->: 1))), // Key 14
    ("$$ite",    forall(o ->: 1 ->: 1 ->: 1)),  // Key 15
    ("$less",    forall(1 ->: 1 ->: o)), // Key 16
    ("$lesseq",   forall(1 ->: 1 ->: o)), // Key 17
    ("$greater",  forall(1 ->: 1 ->: o)), // Key 18
    ("$greatereq",forall(1 ->: 1 ->: o)), // Key 19
    ("@+",        forall((1 ->: o) ->: 1)), // Key 20
    ("@-",        forall((1 ->: o) ->: 1)), // Key 21
    ("$uminus",   forall(1 ->: 1)), // Key 22
    ("$sum",      forall(1 ->: 1 ->: 1)), // Key 23
    ("$difference",forall(1 ->: 1 ->: 1)), // Key 24
    ("$product",   forall(1 ->: 1 ->: 1)), // Key 25
    ("$quotient",  forall(1 ->: 1 ->: 1)), // Key 26
    ("$quotient_e",forall(1 ->: 1 ->: 1)), // Key 27
    ("$quotient_t",forall(1 ->: 1 ->: 1)), // key 28
    ("$quotient_f",forall(1 ->: 1 ->: 1)), // Key 29
    ("$remainder_e",forall(1 ->: 1 ->: 1)), // Key 30
    ("$remainder_t",forall(1 ->: 1 ->: 1)), // key 31
    ("$remainder_f",forall(1 ->: 1 ->: 1)), // Key 32
    ("$floor",     forall(1 ->: 1)), // Key 33
    ("$ceiling",   forall(1 ->: 1)), // Key 34
    ("$truncate",  forall(1 ->: 1)), // Key 35
    ("$round",     forall(1 ->: 1)), // Key 36
    ("$to_int",      forall(1 ->: int)), // Key 37
    ("$to_rat",      forall(1 ->: rat)), // Key 38
    ("$to_real",      forall(1 ->: real)), // Key 39
      ("$is_rat",      forall(1 ->: o)), // Key 40
      ("$is_int",      forall(1 ->: o)) // Key 41
  )

  // Standard defined symbols
  lazy val definedConsts = List(("?", existsDef, forall((1 ->: o) ->: o)), // Key 42
    ("&",   andDef,  o ->: o ->: o), // Key 43
    ("=>",  implDef, o ->: o ->: o), // Key 44
    ("<=",  ifDef,   o ->: o ->: o), // Key 45
    ("<=>", iffDef,  o ->: o ->: o), // Key 46
    ("~&", nandDef,  o ->: o ->: o), // Key 47
    ("~|",  norDef,  o ->: o ->: o), // Key 48
    ("<~>",niffDef,  o ->: o ->: o), // Key 49
    ("!=",  neqDef, forall(1 ->: 1 ->: o))) // Key 50


  //////////////////////
  // enum end
  //////////////////////

  // Shorthands for later definitions
  private def not = mkAtom(HOLSignature.notKey)
  private def all = mkAtom(HOLSignature.forallKey)
  private def disj = mkAtom(HOLSignature.orKey)
  private def conj = mkAtom(HOLSignature.andKey)
  private def impl = mkAtom(HOLSignature.implKey)
  private def lpmi = mkAtom(HOLSignature.ifKey)
  private def eq = mkAtom(HOLSignature.eqKey)

  // Definitions for default symbols
  protected def existsDef: Term = Λ(
    mkTermAbs(1 ->: o,
      mkTermApp(not,
        mkTermApp(all,
          mkTermAbs(1,
            mkTermApp(not,
              mkTermApp((2, 1 ->: o), (1, 1))))))))

  protected def andDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(disj, mkTermApp(not, (2, o))),
          mkTermApp(not, (1, o))))))

  protected def implDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, mkTermApp(not, (2, o))),
        (1, o))))

  protected def ifDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, (2, o)),
        mkTermApp(not, (1, o)))))

  protected def iffDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(conj, mkTermApp(
          mkTermApp(impl, (2, o)), (1, o))),
        mkTermApp(
          mkTermApp(lpmi, (2, o)), (1, o)))))

  protected def nandDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, mkTermApp(not, (2, o))),
        mkTermApp(not, (1, o)))))

  protected def norDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(disj, (2, o)),
          (1, o)))))

  protected def niffDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(conj, mkTermApp(
            mkTermApp(impl, (2, o)), (1, o))),
          mkTermApp(
            mkTermApp(lpmi, (2, o)), (1, o))))))

  protected def neqDef: Term = Λ(
    mkTermAbs(1,
      mkTermAbs(1,
        mkTermApp(not,
          mkTermApp(
            mkTermApp(eq,
              (2, 1)),
              (1, 1))))))
}

object HOLSignature {
  ////////////////////
  // Systematic enumeration f signature symbols for easier changes later on
  ////////////////////<commit_msg>fixed definition or exists and !=<commit_after>package leo.datastructures

import Term.{intToBoundVar, intsToBoundVar, mkApp, mkAtom, mkTermAbs, mkTermApp, Λ,Symbol,∙}
import Type.{superKind, typeKind, typeVarToType}
import leo.datastructures.impl.Signature

import scala.language.implicitConversions

/** This type can be mixed-in to supply standard higher-order logic symbol definitions, including
 *
 *  1. Fixed (interpreted) symbols
 *  2. Defined symbols
 *  3. Standard base types
 *
 * These symbols must be inserted into the signature before all other symbols and in the order described below.
 *
 * Details:
 * It defines eight fixed symbols ($true, $false, #box, #diamond, ~, !, |, =),
 * eight defined symbols (?, &, =>, <=, <=>, ~|, ~&, <~>) and three types/kinds ($o, $i, *)
 * @author <NAME>
 * @since 02.05.2014
 * @note Updated 24.June 2014: Added remaining connectives from TPTP: ~|,~&, <~>
  *                            Added trait for binary/unary connectives
 */
trait HOLSignature {
  ////////////////////////////////
  // Hard wired fixed keys
  ////////////////////////////////
  val oKey = 1
  val o = Type.mkType(oKey)

  val iKey = 2
  val i = Type.mkType(iKey)

  val realKey = 3
  val real = Type.mkType(realKey)

  val ratKey = 4
  val rat = Type.mkType(ratKey)

  val intKey = 5
  val int = Type.mkType(intKey)

  val letKey = HOLSignature.letKey
  val iteKey = HOLSignature.iteKey

  // Don't change the order of the elements in this lists.
  // If you do so, you may need to update the Signature implementation.

  // Built-in types
  val types = List(("$tType", superKind), // Key 0
    ("$o", typeKind), // Key 1
    ("$i", typeKind), // Key 2
    ("$real", typeKind), // key 3
    ("$rat", typeKind), // Key 4
    ("$int", typeKind)) // Key 5

  // Fixed symbols
  import Type.{mkPolyType => forall}
  lazy val fixedConsts = List(("$true", o), // Key 6
    ("$false",                        o), // Key 7
    ("#box",                    o ->: o), // Key 8
    ("#diamond",                o ->: o), // Key 9
    ("~",                       o ->: o), // Key 10
    ("!",        forall((1 ->: o) ->: o)), // Key 11
    ("|",                 o ->: o ->: o), // Key 12
    ("=",        forall(1 ->: 1 ->: o)), // Key 13
    ("$$let",    forall(forall(2 ->: 1 ->: 1))), // Key 14
    ("$$ite",    forall(o ->: 1 ->: 1 ->: 1)),  // Key 15
    ("$less",    forall(1 ->: 1 ->: o)), // Key 16
    ("$lesseq",   forall(1 ->: 1 ->: o)), // Key 17
    ("$greater",  forall(1 ->: 1 ->: o)), // Key 18
    ("$greatereq",forall(1 ->: 1 ->: o)), // Key 19
    ("@+",        forall((1 ->: o) ->: 1)), // Key 20
    ("@-",        forall((1 ->: o) ->: 1)), // Key 21
    ("$uminus",   forall(1 ->: 1)), // Key 22
    ("$sum",      forall(1 ->: 1 ->: 1)), // Key 23
    ("$difference",forall(1 ->: 1 ->: 1)), // Key 24
    ("$product",   forall(1 ->: 1 ->: 1)), // Key 25
    ("$quotient",  forall(1 ->: 1 ->: 1)), // Key 26
    ("$quotient_e",forall(1 ->: 1 ->: 1)), // Key 27
    ("$quotient_t",forall(1 ->: 1 ->: 1)), // key 28
    ("$quotient_f",forall(1 ->: 1 ->: 1)), // Key 29
    ("$remainder_e",forall(1 ->: 1 ->: 1)), // Key 30
    ("$remainder_t",forall(1 ->: 1 ->: 1)), // key 31
    ("$remainder_f",forall(1 ->: 1 ->: 1)), // Key 32
    ("$floor",     forall(1 ->: 1)), // Key 33
    ("$ceiling",   forall(1 ->: 1)), // Key 34
    ("$truncate",  forall(1 ->: 1)), // Key 35
    ("$round",     forall(1 ->: 1)), // Key 36
    ("$to_int",      forall(1 ->: int)), // Key 37
    ("$to_rat",      forall(1 ->: rat)), // Key 38
    ("$to_real",      forall(1 ->: real)), // Key 39
      ("$is_rat",      forall(1 ->: o)), // Key 40
      ("$is_int",      forall(1 ->: o)) // Key 41
  )

  // Standard defined symbols
  lazy val definedConsts = List(("?", existsDef, forall((1 ->: o) ->: o)), // Key 42
    ("&",   andDef,  o ->: o ->: o), // Key 43
    ("=>",  implDef, o ->: o ->: o), // Key 44
    ("<=",  ifDef,   o ->: o ->: o), // Key 45
    ("<=>", iffDef,  o ->: o ->: o), // Key 46
    ("~&", nandDef,  o ->: o ->: o), // Key 47
    ("~|",  norDef,  o ->: o ->: o), // Key 48
    ("<~>",niffDef,  o ->: o ->: o), // Key 49
    ("!=",  neqDef, forall(1 ->: 1 ->: o))) // Key 50


  //////////////////////
  // enum end
  //////////////////////

  // Shorthands for later definitions
  private def not = mkAtom(HOLSignature.notKey)
  private def all = mkAtom(HOLSignature.forallKey)
  private def disj = mkAtom(HOLSignature.orKey)
  private def conj = mkAtom(HOLSignature.andKey)
  private def impl = mkAtom(HOLSignature.implKey)
  private def lpmi = mkAtom(HOLSignature.ifKey)
  private def eq = mkAtom(HOLSignature.eqKey)

  // Definitions for default symbols
  protected def existsDef: Term = Λ(
    mkTermAbs(1 ->: o,
      mkTermApp(not,
        mkTermApp(Term.mkTypeApp(all, 1),
          mkTermAbs(1,
            mkTermApp(not,
              mkTermApp((2, 1 ->: o), (1, 1))))))))

  protected def andDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(disj, mkTermApp(not, (2, o))),
          mkTermApp(not, (1, o))))))

  protected def implDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, mkTermApp(not, (2, o))),
        (1, o))))

  protected def ifDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, (2, o)),
        mkTermApp(not, (1, o)))))

  protected def iffDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(conj, mkTermApp(
          mkTermApp(impl, (2, o)), (1, o))),
        mkTermApp(
          mkTermApp(lpmi, (2, o)), (1, o)))))

  protected def nandDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(
        mkTermApp(disj, mkTermApp(not, (2, o))),
        mkTermApp(not, (1, o)))))

  protected def norDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(disj, (2, o)),
          (1, o)))))

  protected def niffDef: Term = mkTermAbs(o,
    mkTermAbs(o,
      mkTermApp(not,
        mkTermApp(
          mkTermApp(conj, mkTermApp(
            mkTermApp(impl, (2, o)), (1, o))),
          mkTermApp(
            mkTermApp(lpmi, (2, o)), (1, o))))))

  protected def neqDef: Term = Λ(
    mkTermAbs(1,
      mkTermAbs(1,
        mkTermApp(not,
          mkTermApp(
            mkTermApp(Term.mkTypeApp(eq, 1),
              (2, 1)),
              (1, 1))))))
}

object HOLSignature {
  ////////////////////
  // Systematic enumeration f signature symbols for easier changes later on
  ////////////////////
{'fraction_non_alphanumeric': 0.21667177444069874, 'fraction_numerical': 0.03279190928593319, 'mean_word_length': 1.981498401096391, 'pattern_counts': {'":': 0, '<': 19, '<?xml version=': 0, '>': 173, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '2008698', 'n_tokens_mistral': 5070, 'n_tokens_neox': 4623, 'n_words': 1271}