wneuper/isac: isac-java/src/java/isac/gui/mawen/syntax/isabelle/term.scala@b4e3883d7b66

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

     2     Title:      Pure/term.scala

     3     Author:     Makarius

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

     6 Lambda terms, types, sorts.

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

     9 */

    11 package isac.gui.mawen.syntax.isabelle

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

    15 object XTerm

    16 {

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

    19   type Indexname = (String, Int)

    21   type Sort = List[String]

    22   val dummyS: Sort = List("")

    24   sealed abstract class Typ

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

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

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

    28   val dummyT = Type("dummy")

    30   sealed abstract class Term

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

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

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

    34   case class Bound(index: Int) extends Term

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

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

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

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

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

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

    44   /* display variables */

    45   def string_of_vname (xi : Indexname): String =

    46   {

    47     val (x, i) = xi

    48     val idx = XLibrary.string_of_int(i.intValue)

    49     val dot = idx.toList match {

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

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

    52       case _ => true

    53     }

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

    55     else {

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

    57       else "?" ++ x

    58     }

    59   }

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

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

    62   {

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

    64     u match {

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

    66       case _ => (u, ts)

    67     }

    68     stripc(u, List())

    69   }

    71 }

author	Walther Neuper <walther.neuper@jku.at>
	Fri, 26 Mar 2021 10:45:05 +0100
changeset 5239	b4e3883d7b66
parent 5229	6bf0e95981e3
permissions	-rw-r--r--