render-tptp.xsltxt

stylesheet "1.0";
include "utils/die.xsl";
include "utils/list.xsl";
output method="text";

//////////////////////////////////////////////////////////////////////
// Templates
//////////////////////////////////////////////////////////////////////

// If we don't handle something explicitly, we don't handle it at all.
tpl [*] {
  $n = `name (.)`;
  $message = `concat ("Error: we have arrived at an unhandled ", $n, " node.")`;
  apply [.] (#message = $message) mode="die";
}

tpl [/] {
  if [tstp] {
    apply [tstp];
  } else {
    msg terminate="yes" "Error: the required tstp document element is missing.";
  }
}

tpl [tstp] {
  for-each [node()] {
    apply [.];
    if [self::text()] {
      // nothing
    } else {
      "\n";
    }
  }
}

tpl [comment] {
  for-each [text()] {
    $s = `.`;
    $c = chomp (#s = $s);
    emit-percents (#s = $c);
  }
}

// if the string starts with a newline, delete it
tpl chomp-front (#s) {
  if [starts-with ($s, "\n")] {
    `substring-after ($s, "\n")`;
  } else {
    $s;
  }
}

tpl chomp-tail (#s) {
  if [contains ($s, "\n")] {
    $before = `substring-before ($s, "\n")`;
    if [contains ($before, "\n")] {
      $chomped = chomp-tail (#s = `substring-after ($before, "\n")`);
      `concat ($before, "\n", $chomped)`;
    } else {
      $before;
    }
  } else {
    $s;
  }
}

tpl chomp (#s) {
  $front = chomp-front (#s = $s);
  chomp-tail (#s = $front);
}

tpl emit-percents (#s) {
  choose {
    when [$s = ""] {
      // nothing
    }
    when [contains ($s, "\n")] {
      $before = `substring-before ($s, "\n")`;
      $after = `substring-after ($s, "\n")`;
      `concat ("%", $before, "\n")`;
      emit-percents (#s = $after);
    }
    otherwise {
      `concat ("%", $s)`;
    }
  }
}

tpl [text()] {
  `.`;
}

tpl [formula[@syntax = "formula" and @status and @name]] {
  "fof(";
    `@name`; ",";
    `@status`; ",";
    apply [*[1]];
    if [source] {
      apply [source];
    }
    if [useful-info] {
      apply [useful-info];
    }
    ")"; ".";
}

tpl [formula[@syntax = "clause" and @status and @name]] {
  "cnf(";
    `@name`; ",";
    `@status`; ",";
    apply [*[1]];
    if [source] {
      apply [source];
    }
    if [useful-info] {
      apply [useful-info];
    }
    ")"; ".";
}

tpl [number[@name]] {
  `@name`;
}

tpl [non-logical-data[@name and (non-logical-data or number)]] {
  `@name`; "("; list (#separ = ",", #elems = `non-logical-data | number`); ")";
}

tpl [non-logical-data[@name and not(non-logical-data or number)]] {
  `@name`;
}

tpl [non-logical-data[not(@name) and (non-logical-data or number)]] {
  "["; list (#separ = ",", #elems = `non-logical-data | number`); "]";
}

tpl [non-logical-data[not(@name) and not(non-logical-data) and not(number)]] {
  "[]";
}

tpl [source] {
  choose {
    when [non-logical-data and number] {
      ","; "["; list (#separ = ",", #elems = `non-logical-data | number`); "]";
    }
    when [non-logical-data[@name]] {
      ","; apply [non-logical-data[@name]];
    }
    when [number] {
      ","; apply [number];
    }
    otherwise {
      "";
    }
  }
}

tpl [useful-info] {
  choose {
    when [non-logical-data[@name]] {
      ","; apply [non-logical-data[@name]];
    }
    when [non-logical-data[not(@name)] or number] {
      ","; "["; list (#separ = ",", #elems = `non-logical-data | number`); "]";
    }
    when [number] {
      ","; apply [number];
    }
    otherwise {
      "";
    }
  }
}

//////////////////////////////////////////////////////////////////////
// Formulas proper
//////////////////////////////////////////////////////////////////////

tpl [disjunction] {
 "("; apply [*[1]]; " | "; apply [*[2]]; ")";
}

tpl [conjunction] {
 "("; apply [*[1]]; " & "; apply [*[2]]; ")";
}

tpl [implication] {
 "("; apply [*[1]]; " => "; apply [*[2]]; ")";
}

tpl [reverse-implication] {
 "("; apply [*[1]]; " <= "; apply [*[2]]; ")";
}

tpl [equivalence] {
 "("; apply [*[1]]; " <=> "; apply [*[2]]; ")";
}

tpl [nonequivalence] {
 "("; apply [*[1]]; " <~> "; apply [*[2]]; ")";
}

tpl [predicate[@name = "="]] {
  "("; apply [*[1]]; " = "; apply [*[2]]; ")";
}

tpl [predicate[@name and not(@name = "=")]] {
  if [*] {
    `@name`; "("; list (#separ = ",", #elems = `*`); ")";
  } else {
    `@name`;
  }
}

tpl [negation] {
  "~ "; apply [*[1]];
}

tpl [quantifier[@type = "universal"]] {
  "(! ";
    "[";list (#separ = ",", #elems = `variable`); "]";
    " : ";
    apply [*[position() = last()]];
  ")";
}

tpl [quantifier[@type = "existential"]] {
  "(? ";
    "[";list (#separ = ",", #elems = `variable`); "]";
    " : "; apply [*[position() = last()]];
  ")";
}

tpl [defined-predicate[@name = "false"]] {
  "$false";
}

tpl [defined-predicate[@name = "true"]] {
  "$true";
}

//////////////////////////////////////////////////////////////////////
// Terms
//////////////////////////////////////////////////////////////////////

tpl [function[@name]] {
  if [*] {
    `@name`; "("; list (#separ = ",", #elems = `*`); ")";
  } else {
    `@name`;
  }
}

tpl [variable[@name]] {
  `@name`;
}

//////////////////////////////////////////////////////////////////////
// Strings
//////////////////////////////////////////////////////////////////////

tpl [string[@name]] {
  $n = `@name`;
  `concat ("'", $n, "'")`;
}