1.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Sun Apr 23 11:14:37 2017 +0200
1.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/ScalaAstFromString.scala Thu Apr 27 12:51:54 2017 +0200
1.3 @@ -115,6 +115,23 @@
1.4 //println(Ast.raw_string_of(ast))
1.5 assertEquals(ast, Ast.Variable("123"))
1.6
1.7 + //create <code>TestDATA.box_07_with_cursor</code>
1.8 + term_str = "[aaa, bbb, ccc]"
1.9 + tree = sys_.invoke(isac.bridge.IsacOperations.SCALATERM_OF_STRING, term_str)
1.10 + form = DataTypes.xml_to_Formula_NEW(tree)
1.11 + ast = form.getTerm
1.12 + println(Ast.raw_string_of(ast))
1.13 + assertEquals(ast,
1.14 + Ast.Appl(List(
1.15 + Ast.Constant("List.list.Cons"),
1.16 + Ast.Variable("aaa"), Ast.Appl(List(
1.17 + Ast.Constant("List.list.Cons"),
1.18 + Ast.Variable("bbb"),
1.19 + Ast.Appl(List(
1.20 + Ast.Constant("List.list.Cons"),
1.21 + Ast.Variable("ccc"),
1.22 + Ast.Constant("List.list.Nil"))))))) )
1.23 +
1.24 println("\\--END isac.gui.mawen.syntax.ScalaAstFromString#test_etc");
1.25 }
1.26
2.1 --- a/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Sun Apr 23 11:14:37 2017 +0200
2.2 +++ b/isac-java/src/java-tests/isac/gui/mawen/syntax/TestAst.scala Thu Apr 27 12:51:54 2017 +0200
2.3 @@ -10,113 +10,178 @@
2.4
2.5 class TestAst extends TestCase {
2.6
2.7 - // x / y
2.8 - def a1 = Appl(List(Constant("Fields.inverse_class.divide"), Variable ("x"), Variable ("y")))
2.9 -
2.10 - // a * b / c
2.11 - def a2 = Appl(List(Constant("Groups.times_class.times"), Variable ("a"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("b"), Variable("c")))))
2.12 -
2.13 - // sin(a + b) / c
2.14 - def a3 = Appl(List
2.15 - (Constant("Fields.inverse_class.divide"),
2.16 - Appl(List(Constant("sin"),
2.17 - Appl(List(Constant("Groups.plus_class.plus"),
2.18 - Variable("a"),
2.19 - Variable("b")
2.20 - ))
2.21 - ))
2.22 - ,Variable ("c")
2.23 - ))
2.24 - def a4 = Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Variable("b"))), Variable("c")))
2.25 - def a5 = Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Appl(List(Constant("Groups.plus_class.plus"), Variable("b"), Variable("c")))))
2.26 -
2.27 - def test_prefix_string_of() {
2.28 - println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");
2.29 -
2.30 - assertEquals(Ast.prefix_string_of(a1), "/ x y")
2.31 - assertEquals(Ast.prefix_string_of(a2), "* a / b c")
2.32 - assertEquals(Ast.prefix_string_of(a3), "/ sin + a b c")
2.33 -
2.34 - println("\\--END isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");
2.35 - }
2.36 -
2.37 - def test_math_string_of() {
2.38 - println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_math_string_of");
2.39 -
2.40 - assertEquals(Ast.math_string_of(a1), "x / y")
2.41 - assertEquals(Ast.math_string_of(a2), "a * (b / c)")
2.42 - assertEquals(Ast.math_string_of(a3), "sin (a + b) / c")
2.43 -
2.44 - assertEquals(Ast.math_string_of(a4), "a + b + c")
2.45 - assertEquals(Ast.math_string_of(a5), "a + (b + c)")
2.46 -
2.47 - println("\\--END isac.gui.mawen.asttrans.TestAst#test_math_string_of");
2.48 - }
2.49 -
2.50 - /*
2.51 - * The examples for reference of Natalie Karl initially took terms,
2.52 - * @see isac.gui.mawen.scalaterm.TestUtil.
2.53 - * Here we check, whether term_to_ast + Ast.string_of give the same result.
2.54 - */
2.55 - def test_examples_for_NK() {
2.56 - println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");
2.57 -
2.58 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t1)),
2.59 - "aaa + bbb = processed_by_Isabelle_Isac ")
2.60 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t2)),
2.61 - "a + 2 * b + 3 * (c + d)")
2.62 -
2.63 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t31)),
2.64 - "aaa + bbb + ccc")
2.65 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t32)),
2.66 - "aaa + (bbb + ccc)")
2.67 -
2.68 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t41)),
2.69 - "Diff (x + sin (x ^ 2), x)")
2.70 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t42)),
2.71 - "d_d x (x + sin (x ^ 2))")
2.72 -
2.73 - // MAWEN example for reference No.1
2.74 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt1())),
2.75 - "Simplify (1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5)")
2.76 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt3())),
2.77 - "1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5")
2.78 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt4())),
2.79 - "1 + 2 * x / (4 * z) + 5")
2.80 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt5())),
2.81 - "1 + x / (2 * z) + 5")
2.82 - assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt6())),
2.83 - "6 + x / (2 * z)")
2.84 -
2.85 - println("\\--END isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");
2.86 - }
2.87 +// // x / y
2.88 +// def a1 = Appl(List(Constant("Fields.inverse_class.divide"), Variable ("x"), Variable ("y")))
2.89 +//
2.90 +// // a * b / c
2.91 +// def a2 = Appl(List(Constant("Groups.times_class.times"), Variable ("a"), Appl(List(Constant("Fields.inverse_class.divide"), Variable("b"), Variable("c")))))
2.92 +//
2.93 +// // sin(a + b) / c
2.94 +// def a3 = Appl(List
2.95 +// (Constant("Fields.inverse_class.divide"),
2.96 +// Appl(List(Constant("sin"),
2.97 +// Appl(List(Constant("Groups.plus_class.plus"),
2.98 +// Variable("a"),
2.99 +// Variable("b")
2.100 +// ))
2.101 +// ))
2.102 +// ,Variable ("c")
2.103 +// ))
2.104 +// def a4 = Appl(List(Constant("Groups.plus_class.plus"), Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Variable("b"))), Variable("c")))
2.105 +// def a5 = Appl(List(Constant("Groups.plus_class.plus"), Variable("a"), Appl(List(Constant("Groups.plus_class.plus"), Variable("b"), Variable("c")))))
2.106 +//
2.107 +// def test_prefix_string_of() {
2.108 +// println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");
2.109 +//
2.110 +// assertEquals(Ast.prefix_string_of(a1), "/ x y")
2.111 +// assertEquals(Ast.prefix_string_of(a2), "* a / b c")
2.112 +// assertEquals(Ast.prefix_string_of(a3), "/ sin + a b c")
2.113 +//
2.114 +// println("\\--END isac.gui.mawen.asttrans.TestAst#test_prefix_string_of");
2.115 +// }
2.116 +//
2.117 +// def test_math_string_of() {
2.118 +// println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_math_string_of");
2.119 +//
2.120 +// assertEquals(Ast.math_string_of(a1), "x / y")
2.121 +// assertEquals(Ast.math_string_of(a2), "a * (b / c)")
2.122 +// assertEquals(Ast.math_string_of(a3), "sin (a + b) / c")
2.123 +//
2.124 +// assertEquals(Ast.math_string_of(a4), "a + b + c")
2.125 +// assertEquals(Ast.math_string_of(a5), "a + (b + c)")
2.126 +//
2.127 +// println("\\--END isac.gui.mawen.asttrans.TestAst#test_math_string_of");
2.128 +// }
2.129 +//
2.130 +// /*
2.131 +// * The examples for reference of Natalie Karl initially took terms,
2.132 +// * @see isac.gui.mawen.scalaterm.TestUtil.
2.133 +// * Here we check, whether term_to_ast + Ast.string_of give the same result.
2.134 +// */
2.135 +// def test_examples_for_NK() {
2.136 +// println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");
2.137 +//
2.138 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t1)),
2.139 +// "aaa + bbb = processed_by_Isabelle_Isac ")
2.140 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t2)),
2.141 +// "a + 2 * b + 3 * (c + d)")
2.142 +//
2.143 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t31)),
2.144 +// "aaa + bbb + ccc")
2.145 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t32)),
2.146 +// "aaa + (bbb + ccc)")
2.147 +//
2.148 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t41)),
2.149 +// "Diff (x + sin (x ^ 2), x)")
2.150 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.t42)),
2.151 +// "d_d x (x + sin (x ^ 2))")
2.152 +//
2.153 +// // MAWEN example for reference No.1
2.154 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt1())),
2.155 +// "Simplify (1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5)")
2.156 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt3())),
2.157 +// "1 + 2 * x * (y + 3) / (4 * z * (y + 3)) + 5")
2.158 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt4())),
2.159 +// "1 + 2 * x / (4 * z) + 5")
2.160 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt5())),
2.161 +// "1 + x / (2 * z) + 5")
2.162 +// assertEquals(Ast.math_string_of(Syntax_Phases.term_to_ast(TestsDATA.tt6())),
2.163 +// "6 + x / (2 * z)")
2.164 +//
2.165 +// println("\\--END isac.gui.mawen.asttrans.TestAst#test_examples_for_NK");
2.166 +// }
2.167 +//
2.168 +// //test additional examples with BOX, CURSOR, GAP
2.169 +// def test_BOX_CURSOR_GAP() {
2.170 +// println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");
2.171 +//
2.172 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1))
2.173 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_2))
2.174 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_3))
2.175 +//
2.176 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR))
2.177 +// assertEquals( "# + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR_GAP))
2.178 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR_b))
2.179 +//
2.180 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_CURSOR_BOX_3A))
2.181 +// assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_CURSOR_BOX_3B))
2.182 +//
2.183 +//
2.184 +// assertEquals("d_d x x + d_d x (sin (x ^ 2))", Ast.math_string_of(TestDATA.box_05))
2.185 +// assertEquals("d_d bdv (sin (u)) = cos (u) * d_d bdv u", Ast.math_string_of(TestDATA.box_06))
2.186 +// assertEquals("d_d x x + cos (x ^ 2) * d_d x #", Ast.math_string_of(TestDATA.box_07_with_cursor))
2.187 +// assertEquals("a + (# + c)", Ast.math_string_of(TestDATA.box_gap_cursor))
2.188 +// assertEquals("#", Ast.math_string_of(TestDATA.box_with_cursor_on_gap))
2.189 +// assertEquals("# + #", Ast.math_string_of(TestDATA.in_1a))
2.190 +// assertEquals("a + # / #", Ast.math_string_of(TestDATA.in_1b))
2.191 +// assertEquals("a + b / #", Ast.math_string_of(TestDATA.in_1c))
2.192 +//
2.193 +// println("\\--END isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");
2.194 +// }
2.195 +//
2.196
2.197 //test additional examples with BOX, CURSOR, GAP
2.198 - def test_BOX_CURSOR_GAP() {
2.199 - println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");
2.200 + def test_list_match() {
2.201 + println("/--BEGIN isac.gui.mawen.asttrans.TestAst#test_list_match");
2.202
2.203 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1))
2.204 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_2))
2.205 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_3))
2.206 + val ast =
2.207 + Ast.Appl(List(
2.208 + Ast.Constant("\\<^const>List.list.Cons"),
2.209 + Ast.Variable("aaa"),
2.210 + Ast.Appl(List(
2.211 + Ast.Constant("\\<^const>List.list.Cons"),
2.212 + Ast.Variable("bbb"),
2.213 + Ast.Appl(List(
2.214 + Ast.Constant("List.list.Cons"),
2.215 + Ast.Variable("ccc"),
2.216 + Ast.Constant("\\<^const>List.list.Nil")))))))
2.217 + /*from ast.ML: fun try_rules ((lhs, rhs) :: pats) ast = (*WN*)
2.218 + ###try_rules Appl(List(Constant("\<^const>List.list.Cons"), Variable("x"), Constant("\<^const>List.list.Nil")))
2.219 + ###try_rules=> Appl(List(Constant("_list"), Variable("x")))
2.220 + */
2.221 + var lhs =
2.222 + Appl(List(
2.223 + Constant("\\<^const>List.list.Cons"),
2.224 + Variable("x"),
2.225 + Constant("\\<^const>List.list.Nil")))
2.226 + var rhs =
2.227 + Appl(List(
2.228 + Constant("_list"),
2.229 + Variable("x")))
2.230
2.231 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR))
2.232 - assertEquals( "# + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR_GAP))
2.233 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_BOX_1_CURSOR_b))
2.234 + println("------------------------- 1 ---")
2.235 + println(Ast.matches(ast, lhs))
2.236 + println("------------------------- 2 ---")
2.237
2.238 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_CURSOR_BOX_3A))
2.239 - assertEquals("aaa + bbb", Ast.math_string_of(TestDATA.nest_CURSOR_BOX_3B))
2.240 + /*from ast.ML: fun try_rules ((lhs, rhs) :: pats) ast = (*WN*)
2.241 + ###try_rules Appl(List(Constant("\<^const>List.list.Cons"), Variable("x"), Appl(List(Constant("_list"), Variable("xs")))))
2.242 + ###try_rules=> Appl(List(Constant("_list"), Appl(List(Constant("_args"), Variable("x"), Variable("xs")))))
2.243 + */
2.244 + lhs =
2.245 + Ast.Appl(List(
2.246 + Ast.Constant("\\<^const>List.list.Cons"),
2.247 + Ast.Variable("x"),
2.248 + Ast.Appl(List(
2.249 + Ast.Constant("_list"),
2.250 + Ast.Variable("xs")))))
2.251 + rhs =
2.252 + Ast.Appl(List(
2.253 + Ast.Constant("_list"),
2.254 + Ast.Appl(List(
2.255 + Ast.Constant("_args"),
2.256 + Ast.Variable("x"),
2.257 + Ast.Variable("xs")))))
2.258
2.259 + println("------------------------- 3 ---")
2.260 + println(Ast.matches(ast, lhs))
2.261 + println("------------------------- 4 ---")
2.262 +
2.263 + println(Ast.matches(Ast.Constant("a"), Ast.Constant("a")))
2.264 + println(Ast.matches(Ast.Variable("b"), Ast.Variable("b")))
2.265 + println(Ast.matches(Ast.Appl(List(Ast.Constant("c"))), Appl(List(Ast.Constant("c")))))
2.266 + //println(Ast.matches(Ast.Appl(List(Ast.Variable("c"))), Appl(List(Ast.Variable("c")))))
2.267
2.268 - assertEquals("d_d x x + d_d x (sin (x ^ 2))", Ast.math_string_of(TestDATA.box_05))
2.269 - assertEquals("d_d bdv (sin (u)) = cos (u) * d_d bdv u", Ast.math_string_of(TestDATA.box_06))
2.270 - assertEquals("d_d x x + cos (x ^ 2) * d_d x #", Ast.math_string_of(TestDATA.box_07_with_cursor))
2.271 - assertEquals("a + (# + c)", Ast.math_string_of(TestDATA.box_gap_cursor))
2.272 - assertEquals("#", Ast.math_string_of(TestDATA.box_with_cursor_on_gap))
2.273 - assertEquals("# + #", Ast.math_string_of(TestDATA.in_1a))
2.274 - assertEquals("a + # / #", Ast.math_string_of(TestDATA.in_1b))
2.275 - assertEquals("a + b / #", Ast.math_string_of(TestDATA.in_1c))
2.276 -
2.277 - println("\\--END isac.gui.mawen.asttrans.TestAst#test_BOX_CURSOR_GAP");
2.278 + println("\\--END isac.gui.mawen.asttrans.TestAst#test_list_match");
2.279 }
2.280 -
2.281 -}
2.282 \ No newline at end of file
2.283 +
2.284 + }
2.285 \ No newline at end of file
3.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/ast.scala Sun Apr 23 11:14:37 2017 +0200
3.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/ast.scala Thu Apr 27 12:51:54 2017 +0200
3.3 @@ -9,6 +9,8 @@
3.4 import isac.gui.mawen.scalaterm.Util
3.5 import isac.gui.mawen.syntax.isabelle.XLibrary
3.6
3.7 +import scala.collection.immutable.TreeMap
3.8 +
3.9 object Ast {
3.10
3.11 sealed abstract class Ast
3.12 @@ -48,47 +50,45 @@
3.13 /* transform an Ast into a String, which corresponds to Isabelle's
3.14 * pretty_printing within Isac's Knowledge.
3.15 */
3.16 - def to_str (t: Ast, prior: Int, l_r: String): String = t match {
3.17 - case Appl(List(Constant("Product_Type.Pair"), t1, t2))
3.18 - => to_str(t1, prior, "none") + ", " + to_str(t2, prior, "none")
3.19 - case Appl(Constant("BOX") :: Constant(_) :: List(t))
3.20 - => to_str(t, prior, "none")
3.21 - case Appl(Constant("CURSOR") :: List(t))
3.22 - => to_str(t, prior, "none")
3.23 - case Appl(List(Constant(str), t1, t2))
3.24 + def to_str (ast: Ast, prior: Int, l_r: String): String = ast match {
3.25 + case Constant("GAP") => "#"
3.26 + case Constant(str) => XSyntax.isa_math(str)
3.27 + case Variable(str) => str
3.28 + case Appl(List(Constant("CURSOR"), a)) => to_str(a, prior, "none")
3.29 + case Appl(List(Constant(str), a)) => {
3.30 + if (prior == 99 & XSyntax.isa_prior(str) == 99) //FIXME: handles "d_d x (! sin(_) !)" as special case
3.31 + "(" + XSyntax.isa_math(str) + "(" + to_str(a, 0, "none") + ")" + ")"
3.32 + else
3.33 + XSyntax.isa_math(str) + "(" + to_str(a, 0, "none") + ")"
3.34 + }
3.35 + case Appl(List(Constant("BOX"), Constant(_), a)) => to_str(a, prior, "none")
3.36 + case Appl(List(Constant("Product_Type.Pair"), a1, a2))
3.37 + => to_str(a1, prior, "none") + ", " + to_str(a2, prior, "none")
3.38 + case Appl(List(Constant(str), a1, a2))
3.39 => { val pri = XSyntax.isa_prior(str)
3.40 if (prior > pri) {
3.41 XSyntax.isa_fix(str) match {
3.42 - case "infixl" => "(" + to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right") + ")"
3.43 - case "infixr" => "(" + to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right") + ")"
3.44 - case "prefix" => "(" + XSyntax.isa_math(str) + to_str(t1, pri, "left") + to_str(t2, pri, "right") + ")"}
3.45 + case "infixl" => "(" + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right") + ")"
3.46 + case "infixr" => "(" + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right") + ")"
3.47 + case "prefix" => "(" + XSyntax.isa_math(str) + to_str(a1, pri, "left") + to_str(a2, pri, "right") + ")"}
3.48 }else{
3.49 XSyntax.isa_fix(str) match {
3.50 case "infixl" => {
3.51 if (prior == pri & l_r == "right") {
3.52 - "(" + to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right") + ")"
3.53 + "(" + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right") + ")"
3.54 }else{
3.55 - to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right")
3.56 + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right")
3.57 }
3.58 }
3.59 case "infixr" => {
3.60 if (prior == pri & l_r == "left") {
3.61 - "(" + to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right") + ")"
3.62 + "(" + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right") + ")"
3.63 }else{
3.64 - to_str(t1, pri, "left") + XSyntax.isa_math(str) + to_str(t2, pri, "right")
3.65 + to_str(a1, pri, "left") + XSyntax.isa_math(str) + to_str(a2, pri, "right")
3.66 }
3.67 }
3.68 - case "prefix" => XSyntax.isa_math(str) + to_str(t1, pri, "none") + " " + to_str(t2, pri, "none")}
3.69 + case "prefix" => XSyntax.isa_math(str) + to_str(a1, pri, "none") + " " + to_str(a2, pri, "none")}
3.70 }}
3.71 - case Appl(List(Constant(str), t)) => {
3.72 - if (prior == 99 & XSyntax.isa_prior(str) == 99) //FIXME: handles "d_d x (! sin(_) !)" as special case
3.73 - "(" + XSyntax.isa_math(str) + "(" + to_str(t, 0, "none") + ")" + ")"
3.74 - else
3.75 - XSyntax.isa_math(str) + "(" + to_str(t, 0, "none") + ")"
3.76 - }
3.77 - case Constant("GAP") => "#"
3.78 - case Constant(str) => XSyntax.isa_math(str)
3.79 - case Variable(str) => str
3.80 case _ => throw new AstException("Ast.math_string_of: uncovered match")
3.81 }
3.82 // infix: "left" or "right" argument ---------vvvv
3.83 @@ -106,6 +106,77 @@
3.84 "Appl" + XLibrary.enclose("(List(", "))", XLibrary.commas(asts.map ( x => raw_string_of(x) )))
3.85 }
3.86
3.87 + /*
3.88 + translation from Isabelle2016-1 ~~/src/Pure/Syntax/ast.ML
3.89 + (* match = fn: ast -> ast -> (ast Symtab.table * ast list) option*)
3.90 + fun match ast pat =
3.91 + let
3.92 + exception NO_MATCH;
3.93 + (* mtch = fn: ast -> ast -> ast Symtab.table -> ast Symtab.table *)
3.94 + fun mtch (Constant a) (Constant b) env =
3.95 + if a = b then env else raise NO_MATCH
3.96 + | mtch (Variable a) (Constant b) env =
3.97 + if a = b then env else raise NO_MATCH
3.98 + | mtch ast (Variable x) env = Symtab.update (x, ast) env
3.99 + (*update: key * 'a -> 'a table -> 'a table*)
3.100 + | mtch (Appl asts) (Appl pats) env = mtch_lst asts pats env
3.101 + | mtch _ _ _ = raise NO_MATCH
3.102 + (* mtch_lst = fn: ast list -> ast list -> ast Symtab.table -> ast Symtab.table *)
3.103 + and mtch_lst (ast :: asts) (pat :: pats) env =
3.104 + mtch_lst asts pats (mtch ast pat env)
3.105 + | mtch_lst [] [] env = env
3.106 + | mtch_lst _ _ _ = raise NO_MATCH;
3.107 + (* ast * (ast list) *)
3.108 + val (head, args) =
3.109 + (case (ast, pat) of
3.110 + (Appl asts, Appl pats) =>
3.111 + let val a = length asts and p = length pats in
3.112 + if a > p then (Appl (take p asts), drop p asts)
3.113 + else (ast, [])
3.114 + end
3.115 + | _ => (ast, []));
3.116 + in
3.117 + (* (ast Symtab.table * ast list) *)
3.118 + SOME (mtch head pat Symtab.empty, args ) handle NO_MATCH => NONE
3.119 + end;
3.120 + */
3.121 + def matches (ast_pat: Tuple2[Ast, Ast]) : Option[(TreeMap[String, Ast], List[Ast])] = {
3.122 +
3.123 + case class NO_MATCH() extends Exception()
3.124 +
3.125 + def mtch (ast_pat: Tuple2[Ast, Ast], env: TreeMap[String, Ast])
3.126 + : TreeMap[String, Ast] = ast_pat match {
3.127 + case ((Ast.Constant(a), Ast.Constant(b))) =>
3.128 + if (a == b) env else throw new NO_MATCH
3.129 + case ((Ast.Variable(a), Ast.Constant(b))) =>
3.130 + if (a == b) env else throw new NO_MATCH
3.131 + case ((ast, Ast.Variable(x))) => env + ((x, ast))
3.132 + case ((Appl(asts), Appl(pats))) => mtch_lst ((asts, pats), env)
3.133 + case (_) => throw new NO_MATCH
3.134 + }
3.135 + def mtch_lst (asts_pats: Tuple2[List[Ast], List[Ast]], env: TreeMap[String, Ast])
3.136 + : TreeMap[String, Ast] = asts_pats match {
3.137 + case ((ast :: asts, pat :: pats)) =>
3.138 + mtch_lst ((asts, pats), mtch ((ast, pat), env))
3.139 + case ((List(), List())) => env
3.140 + case (_) => throw new NO_MATCH
3.141 + }
3.142 + val (head, args) = ast_pat match {
3.143 + case ((Appl(asts), Appl(pats))) => {
3.144 + val a = asts.length
3.145 + val p = pats.length
3.146 + if (a > p) {(Ast.Appl(asts.take(p)), asts.drop(p))}
3.147 + else (ast_pat._1, List())
3.148 + }
3.149 + case ((_,_)) => (ast_pat._1, List())
3.150 + }
3.151 + try {
3.152 + Some (mtch ((head, ast_pat._2), new TreeMap()), args)
3.153 + } catch {
3.154 + case c: NO_MATCH => None
3.155 + }
3.156 + }
3.157 +
3.158 }
3.159
3.160
4.1 --- a/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Sun Apr 23 11:14:37 2017 +0200
4.2 +++ b/isac-java/src/java/isac/gui/mawen/syntax/syntax_phases.scala Thu Apr 27 12:51:54 2017 +0200
4.3 @@ -15,7 +15,8 @@
4.4
4.5 object Syntax_Phases {
4.6
4.7 - /* CODE OMITTED IN THE TRANSLATION IS INDICATED BY (**) IN ORIGINAL ML:
4.8 + /* translation from Isabelle2016-1 ~~/src/Pure/Syntax/syntax_phases.ML
4.9 + CODE OMITTED IN THE TRANSLATION IS INDICATED BY (**) IN ORIGINAL ML:
4.10 (* simple_ast_of *)
4.11
4.12 (* = fn: Proof.context -> term -> Ast.ast*)