/*  THIS IS A COMPLETE COPY OF Isabelle2016-1 ...

    Title:      Pure/term.scala

    Author:     Makarius

    ... WITH ADDITIONS AFTER "/---..---\"

Lambda terms, types, sorts.

Note: Isabelle/ML is the primary environment for logical operations.

*/

package isac.gui.mawen.syntax.isabelle

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

object XTerm

{

  /* //---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------\\

  type Indexname = (String, Int)

  type Sort = List[String]

  val dummyS: Sort = List("")

  sealed abstract class Typ

  case class Type(name: String, args: List[Typ] = Nil) extends Typ

  case class TFree(name: String, sort: Sort = dummyS) extends Typ

  case class TVar(name: Indexname, sort: Sort = dummyS) extends Typ

  val dummyT = Type("dummy")

  sealed abstract class Term

  case class Const(name: String, typ: Typ = dummyT) extends Term

  case class Free(name: String, typ: Typ = dummyT) extends Term

  case class Var(name: Indexname, typ: Typ = dummyT) extends Term

  case class Bound(index: Int) extends Term

  case class Abs(name: String, typ: Typ = dummyT, body: Term) extends Term

  case class App(fun: Term, arg: Term) extends Term

  \\---------- this would overwrite edu.tum.cs.isabelle.pure._ ----------// */

//----------------- ADDITIONS TO Isabelle2016-1 FOR ISAC -----------------\\

  // see ~~/src/Pure/General/symbol.scala: is digit

  def is_digit(sym: String): Boolean = sym.length == 1 && '0' <= sym(0) && sym(0) <= '9'

  /* display variables */

  def string_of_vname (xi : Indexname): String = 

  { 

    val (x, i) = xi

    val idx = XLibrary.string_of_int(i.intValue)

    val dot = idx.toList match {

      case  _ :: /*?HOW HANDLE THIS CHAR: "⇩" ::*/ _ => false

      //case  c :: _ => XSymbol.is_digit(c)             //unreachable --^^

      case _ => true      

    }

    if (dot) "?" ++ x ++ "." ++ idx

    else {

      if (i != 0) "?" ++ x ++ idx

      else "?" ++ x

    }

  }

  /*maps   f(t1,...,tn)  to  (f, [t1,...,tn]) ; naturally tail-recursive*/

  def strip_comb(u : Term) : (Term, List[Term]) =

  {

    def stripc (u : Term, ts : List[Term]) : (Term, List[Term]) =

    u match {

      case App(f, t) => stripc (f, t::ts)

      case _ => (u, ts)

    }

    stripc(u, List())

  }

}