text: package org.kframework.kdoc
  
  import org.kframework.attributes.Att
  import org.kframework.definition.{Module, NonTerminal, RegexTerminal, Terminal}
  import org.kframework.frontend.K
  import org.kframework.frontend.Unapply._
  
  /**
    * Takes a K term with the grammar described by Module module, and unparses it to its latex representation.
    * For each term:
    *  - when its production has latex attribute, it uses that attribute for unparsing
    *  - otherwise, it unparses by concatenating the Production's items with the separator parameter as a separator
    * @param module
    * @param separator
    */
  class KtoLatex(module: Module, separator: String = " ") extends ((K) => String) {
    var x = 0
    def apply(k: K): String = k match {
      case KApply(l, children) =>
        val latexAtts = module.productionsFor(l).flatMap(_.att.get[String](Att.latex))
        val latex = latexAtts.size match {
          case 0 => // no latex annotation
            val possibleLatexes = module.productionsFor(l).map(_.items.foldLeft((Seq[String](), 1)) {
              case ((r, i), t: Terminal) => (r :+ t.value, i)
              case ((r, i), t: RegexTerminal) => (r :+ t.regex, i) //TODO: we probably want something better here
              case ((r, i), nt: NonTerminal) => (r :+ "#" + i, i + 1)
            }).map(_._1.mkString(separator))
            possibleLatexes.size match {
              case 0 => throw new AssertionError("Could not find a label for " + l)
              case 1 => possibleLatexes.head
              case _ => throw new AssertionError("Too productions for klabel " + l)
            }
          case 1 => // exactly one latex annotation
            latexAtts.head
          case _ => // multiple latex attributes
            throw new AssertionError("Too many latex attributes for klabel " + l)
        }
        children.zipWithIndex.foldRight(latex) { case ((value, i), res) => res.replace("#" + (i + 1), apply(value)) }
      case KToken(s, _) => s
      case KRewrite(l, r) => apply(l) + "\\Rightarrow" + apply(r) //TODO: use kast.k latex annotation
      case KSequence(s) => s map apply mkString "~>"              //TODO: use kast.k latex annotation
    }
  }
  