1.1 --- a/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Wed Mar 22 15:09:45 2017 +0100
1.2 +++ b/isac-java/src/java/isac/gui/mawen/scalaterm/Util.scala Thu Mar 23 10:31:04 2017 +0100
1.3 @@ -1,5 +1,6 @@
1.4 package isac.gui.mawen.scalaterm
1.5
1.6 +import isac.gui.mawen.syntax.XSyntax
1.7 import isac.gui.mawen.termtree.TreeNodeContent
1.8 import javax.swing.tree.DefaultMutableTreeNode
1.9
1.10 @@ -10,47 +11,7 @@
1.11 object Util {
1.12
1.13 def int(s: String): Integer = new Integer(s)
1.14 -
1.15 - /* Data for presentation of Const which are not contained in (Scala-) Term:
1.16 - * _1: string as shown by Isabelle's pretty printing
1.17 - * _2: string in LaTeX format with place-holders "#d", where d is a digit:
1.18 - * number of place-holders determine arity;
1.19 - * pre/post/mix-fix is read out from here also for _1
1.20 - * _3: infixl | infixr | prefix | postfix: the latter two are redundant with _2
1.21 - * _4: priority, which determines parentheses to be set
1.22 - * TODO: reconsider data representation: record, ...
1.23 - */
1.24 - val present = Map (
1.25 - "HOL.eq" -> (" = ", "#1=#2", "infixl", 50), //see ~~/src/HOL/HOL.thy
1.26 - "Groups.plus_class.plus" -> (" + ", "#1+#2", "infixl", 65), //see ~~/src/HOL/Groups.thy
1.27 - "Groups.minus_class.minus" -> (" - ", "#1-#2", "infixl", 65), //see ~~/src/HOL/Groups.thy
1.28 - "Groups.plus_class.uminus" -> (" -", "#1-#2", "prefix", 80), //see ~~/src/HOL/Groups.thy
1.29 - "Groups.times_class.times" -> (" * ", "#1.#2", "infixl", 70), //see ~~/src/HOL/Groups.thy
1.30 - //"Groups.plus_class.times"->("*", "#1\cdot#2", "infixl", 70),
1.31 - //...ERROR: implicit conversion found: Groups.plus_class.times => ...
1.32 - "Fields.inverse_class.divide" -> (" / ", "\frac{#1}{#2}", "infixl", 70), //see ~~/src/HOL/Fields.thy
1.33 - "Atools.pow" -> (" ^ ", "#1^{#2}", "infixr", 80) //see ~~/src/HOL/Transcendental.thy
1.34 - //"Transcendental.sin" -> ("sin ", "\sin{#1}", "infixl", 70)
1.35 - //...ERROR: implicit conversion found: ...
1.36 - )
1.37 - /* so not every constant needs to be in Util.present */
1.38 - def ST_isa(str: String): String = {
1.39 - present.get(str) match {
1.40 - case Some((isa, _, _, _)) => isa
1.41 - case None => str.substring(str.lastIndexOf(".") + 1) + " "}}
1.42 - def ST_latex(str: String): String = {
1.43 - present.get(str) match {
1.44 - case Some((_, latex, _, _)) => latex
1.45 - case None => str.substring(str.lastIndexOf(".") + 1) + " "}}
1.46 - def ST_fix(str: String): String = {
1.47 - present.get(str) match {
1.48 - case Some((_, _, fix, _)) => fix
1.49 - case None => "prefix"}}
1.50 - def ST_prior(str: String): Int = {
1.51 - present.get(str) match {
1.52 - case Some((_, _, _, prior)) => prior
1.53 - case None => 99}}
1.54 -
1.55 +
1.56 /* transform a Term into a String, which corresponds to Isabelle's
1.57 * pretty_printing within Isac's Knowledge.
1.58 * mawen uses this for string representation of Terms.
1.59 @@ -59,31 +20,31 @@
1.60 case App(App(Const("Product_Type.Pair", _), t1), t2)
1.61 => str_of(t1, prior, "none") + ", " + str_of(t2, prior, "none")
1.62 case App(App(Const(str, _), t1), t2)
1.63 - => { val pri = ST_prior(str)
1.64 + => { val pri = XSyntax.prior(str)
1.65 if (prior > pri) {
1.66 - ST_fix(str) match {
1.67 - case "infixl" => "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"
1.68 - case "infixr" => "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"
1.69 - case "prefix" => "(" + ST_isa(str) + str_of(t1, pri, "left") + " (2" + str_of(t2, pri, "right") + "2)" + ")"}
1.70 + XSyntax.fix(str) match {
1.71 + case "infixl" => "(" + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right") + ")"
1.72 + case "infixr" => "(" + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right") + ")"
1.73 + case "prefix" => "(" + XSyntax.isa(str) + str_of(t1, pri, "left") + " (2" + str_of(t2, pri, "right") + "2)" + ")"}
1.74 }else{
1.75 - ST_fix(str) match {
1.76 + XSyntax.fix(str) match {
1.77 case "infixl" => {
1.78 if (prior == pri & l_r == "right") {
1.79 - "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"
1.80 + "(" + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right") + ")"
1.81 }else{
1.82 - str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right")
1.83 + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right")
1.84 }
1.85 }
1.86 case "infixr" => {
1.87 if (prior == pri & l_r == "left") {
1.88 - "(" + str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right") + ")"
1.89 + "(" + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right") + ")"
1.90 }else{
1.91 - str_of(t1, pri, "left") + ST_isa(str) + str_of(t2, pri, "right")
1.92 + str_of(t1, pri, "left") + XSyntax.isa(str) + str_of(t2, pri, "right")
1.93 }
1.94 }
1.95 - case "prefix" => ST_isa(str) + str_of(t1, pri, "none") + " " + str_of(t2, pri, "none")}
1.96 + case "prefix" => XSyntax.isa(str) + str_of(t1, pri, "none") + " " + str_of(t2, pri, "none")}
1.97 }}
1.98 - case App(Const(str, _), t1) => ST_isa(str) + "(" + str_of(t1, prior, "none") + ")"
1.99 + case App(Const(str, _), t1) => XSyntax.isa(str) + "(" + str_of(t1, prior, "none") + ")"
1.100 case Free(str, _) => str
1.101 case Const(str, _) => str
1.102 case _ => throw new IllegalArgumentException("str_of WRONG arg: " + t)
1.103 @@ -138,7 +99,7 @@
1.104 => n //TODO
1.105 case App(App(Const(str, typ), t1), t2)
1.106 => { val tmp1 = n.clone().asInstanceOf[DefaultMutableTreeNode]
1.107 - n.setUserObject(new TreeNodeContent(ST_isa(str), Util.string_of(App(App(Const(str, typ), t1), t2))))
1.108 + n.setUserObject(new TreeNodeContent(XSyntax.isa(str), Util.string_of(App(App(Const(str, typ), t1), t2))))
1.109 n.add(insert_nodes(t1, tmp1))
1.110 val tmp2 = n.clone().asInstanceOf[DefaultMutableTreeNode]
1.111 n.add(insert_nodes(t2, tmp2))
1.112 @@ -146,7 +107,7 @@
1.113 }
1.114 case App(Const(str, typ), t1)
1.115 => { val tmp = n.clone().asInstanceOf[DefaultMutableTreeNode]
1.116 - n.setUserObject(new TreeNodeContent(ST_isa(str), Util.string_of(App(Const(str, typ), t1))))
1.117 + n.setUserObject(new TreeNodeContent(XSyntax.isa(str), Util.string_of(App(Const(str, typ), t1))))
1.118 n.add(insert_nodes(t1, tmp))
1.119 n
1.120 }
1.121 @@ -194,31 +155,31 @@
1.122 case App(App(Const("Fields.inverse_class.divide", _), t1), t2)
1.123 => {
1.124 val str = "Fields.inverse_class.divide"
1.125 - val pri = ST_prior(str)
1.126 + val pri = XSyntax.prior(str)
1.127 "<mfrac><mrow>" + matml_of(t1, pri, "left") + "</mrow><mrow>" + matml_of(t2, pri, "right") + "</mrow></mfrac>"
1.128 }
1.129 case App(App(Const(str, _), t1), t2)
1.130 - => { val pri = ST_prior(str)
1.131 + => { val pri = XSyntax.prior(str)
1.132 if (prior > pri) {
1.133 - ST_fix(str) match {
1.134 - case "prefix" => "<mfenced separators=\'\'>" + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t1, pri, "left") +
1.135 + XSyntax.fix(str) match {
1.136 + case "prefix" => "<mfenced separators=\'\'>" + "<mo>" + XSyntax.isa(str) + "</mo>" + matml_of(t1, pri, "left") +
1.137 "<mfenced separators=\'\'>" + matml_of(t2, pri, "right") + "</mfenced>" + "</mfenced>"
1.138 case _ => "<mfenced separators=\'\'>" + matml_of(t1, pri, "left") + "<mo>" +
1.139 - ST_isa(str) + "</mo>" + matml_of(t2, pri, "right") + "</mfenced>"
1.140 + XSyntax.isa(str) + "</mo>" + matml_of(t2, pri, "right") + "</mfenced>"
1.141 }
1.142 }else{
1.143 - ST_fix(str) match {
1.144 - case "prefix" => "<mo>" + ST_isa(str) + "</mo>" + matml_of(t1, pri, "none") + " " + matml_of(t2, pri, "none")
1.145 + XSyntax.fix(str) match {
1.146 + case "prefix" => "<mo>" + XSyntax.isa(str) + "</mo>" + matml_of(t1, pri, "none") + " " + matml_of(t2, pri, "none")
1.147 case _ => {
1.148 if (prior == pri & l_r == "right") {
1.149 - matml_of(t1, pri, "left") + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t2, pri, "right")
1.150 + matml_of(t1, pri, "left") + "<mo>" + XSyntax.isa(str) + "</mo>" + matml_of(t2, pri, "right")
1.151 }else{
1.152 - matml_of(t1, pri, "left") + "<mo>" + ST_isa(str) + "</mo>" + matml_of(t2, pri, "right")
1.153 + matml_of(t1, pri, "left") + "<mo>" + XSyntax.isa(str) + "</mo>" + matml_of(t2, pri, "right")
1.154 }
1.155 }}
1.156 }
1.157 }
1.158 - case App(Const(str, _), t1) => "<mo>" + ST_isa(str) + "</mo>" + "<mfenced separators=\'\'>" + matml_of(t1, prior, "none") + "</mfenced>"
1.159 + case App(Const(str, _), t1) => "<mo>" + XSyntax.isa(str) + "</mo>" + "<mfenced separators=\'\'>" + matml_of(t1, prior, "none") + "</mfenced>"
1.160 case Free(str, _) => if (is_numeral(str)) "<mn>" + str + "</mn>" else "<mi>" + str + "</mi>"
1.161 case Const(str, _) => str
1.162 case _ => throw new IllegalArgumentException("matml_of WRONG arg: " + t)