Fix merge conflict.

TODO

-# vim: set fileencoding=utf-8 :
-
- - Fix BisonSyntaxError location tracking.
-
- - Sort polynom by its exponents?
-
- - Fix division by zero caused by "0/0": Catch exception in front-end
-
-smvv@multivac ~/work/trs $ printf "a/0\n??" | ./main.py
-Traceback (most recent call last):
-  File "./main.py", line 75, in <module>
-    main()
-  File "./main.py", line 64, in main
-    node = p.run(debug=args.debug)
-  File "/home/smvv/work/trs/external/pybison/src/python/bison.py", line 258, in run
-    self.report_last_error(filename, e)
-  File "/home/smvv/work/trs/external/pybison/src/python/bison.py", line 251, in run
-    self.engine.runEngine(debug)
-  File "bison_.pyx", line 592, in bison_.ParserEngine.runEngine (build/external/pybison/bison_.c:592)
-  File "/home/smvv/work/trs/src/parser.py", line 195, in hook_handler
-    possibilities = handler(retval)
-  File "/home/smvv/work/trs/src/rules/fractions.py", line 23, in match_constant_division
-    raise ZeroDivisionError('Division by zero: %s.' % node)
-ZeroDivisionError: Division by zero: a / 0.
-
-smvv@multivac ~/work/trs $ printf "0/0\n??" | ./main.py
-Traceback (most recent call last):
-  File "./main.py", line 75, in <module>
-    main()
-  File "./main.py", line 64, in main
-    node = p.run(debug=args.debug)
-  File "/home/smvv/work/trs/external/pybison/src/python/bison.py", line 258, in run
-    self.report_last_error(filename, e)
-  File "/home/smvv/work/trs/external/pybison/src/python/bison.py", line 251, in run
-    self.engine.runEngine(debug)
-  File "bison_.pyx", line 592, in bison_.ParserEngine.runEngine (build/external/pybison/bison_.c:592)
-  File "/home/smvv/work/trs/src/parser.py", line 195, in hook_handler
-    possibilities = handler(retval)
-  File "/home/smvv/work/trs/src/rules/numerics.py", line 73, in match_divide_numerics
-    divide = not divmod(n.value, dv)[1]
-ZeroDivisionError: integer division or modulo by zero
-
- - Last possibilities reduce to a similar result.
-
-smvv@multivac ~/work/trs $ printf "0/1\n??" | ./main.py
-<Possibility root="0 / 1" handler=divide_numerics args=(0, 1)>
-Division of 0 by 1 reduces to 0.
-Division of 0 by 1 reduces to 0.
-
- - ExpressionNode.equals() werkend maken voor alle cases (negatie).
-
- - validation: preorder traversal implementatie vergelijken met andere
-               implementaties.
-
- - No matches for sin(pi), sin(2pi), sin(4pi), etc...
-
- - Create unit tests for node inequivalence operator.
-
- - Line printer: 1 / (n + n)x  ->  1 / (n + n) * x
-
- - Parser: 'apia' -> 'aa'
-
- - Unit tests for strategy.
-
- - MESSAGES needs to be expanded.
-
- - Use pretty-print for expressions in hint messages.
-
- - Parser: add unit tests for operator associativity (derivatives/integrals).
-
- - Modules:
-   + Equations with substitution
-   + Sort
-   + Gonio
-
- - Add parentheses to integral bounds where needed:
-   int_(-1)^2 ... dx
-   or, fix parser error using the following notation:
-   int_-1^2 ... dx
-
- - Frontend: implicit rules are applied after expicit ones, but are still
-   printed separately. This yields multiple successive occurences of the same
-   expression.
-
- - Base hint selection on the desired final expression.
-   To generate a hint for expression list A, ..., B:
-   1. Create a possibility tree for A.
-   2. Validate all expressions up to B:
-      set ROOT = A
-
-      for each expression C in <A, B] do:
-          if final answer of C is not equal to final answer of A:
-              validation failes at c
-
-          find C in the possibility tree, traversing from ROOT
-
-          if not found:
-              validation continues, but generate an efficiency warning at C
-              # FIXME: validation fails at C?
-
-          set ROOT = C
-    3. Generate a hint:
-      # ROOT should now be equal to B, so lookup of B is unnecessary
-      set N = empty dictionary
-
-      for each possibility of ROOT P node do:
-          evaluate P(B) until the final expression of A is reached
-          set N[P] = the number of explicit possibilities that have been applied in the evaluation
-
-      the hint is that P for which the value of N[P] the smallest
-
- - Optimization: put possibility tree in hashmap: {'expression': [(handler, args, 'applied_expression')], ...}
-   This hashmap can be used to speedup the calculation of possbility trees.

src/backend/backend.py

+import web
+import json
+
+from src.parser import Parser
+from tests.parser import ParserWrapper
+from src.validation import validate as validate_expression
+
+urls = (
+    '/math\.py/validate', 'validate',
+    '/math\.py/hint', 'hint',
+    '/math\.py/step', 'Step',
+    '/math\.py/answer', 'Answer',
+)
+
+app = web.application(urls, globals())
+
+
+def get_last_line():
+    data = web.input(data='').data
+    lines = map(str, data.split('\n'))
+
+    # Get the last none empty line.
+    for i in range(len(lines))[::-1]:
+        last_line = lines[i].strip()
+
+        if last_line:
+            return last_line
+
+
+class Step(object):
+    def POST(self):
+        web.header('Content-Type', 'application/json')
+
+        try:
+            last_line = get_last_line()
+
+            if last_line:
+                parser = ParserWrapper(Parser)
+                response = parser.run([last_line])
+
+                if response:
+                    response = response.rewrite(include_step=True,
+                            check_implicit=True)
+
+                    if response:
+                        return json.dumps({'step': str(response)})
+
+            return json.dumps({'hint': 'No further reduction is possible.'})
+        except Exception as e:
+            return json.dumps({'error': str(e)})
+
+
+class Answer(object):
+    def POST(self):
+        web.header('Content-Type', 'application/json')
+
+        try:
+            last_line = get_last_line()
+
+            if last_line:
+                parser = ParserWrapper(Parser)
+                response = parser.run([last_line])
+
+                if response:
+                    steps = response.rewrite_all(include_step=True)
+
+                    if steps:
+                        hints, steps = zip(*steps)
+                        return json.dumps({'hints': map(str, hints),
+                                           'steps': map(str, steps)})
+
+            return json.dumps({'hint': 'No further reduction is possible.'})
+        except Exception as e:
+            return json.dumps({'error': str(e)})
+
+
+class hint(object):
+    def POST(self):
+        web.header('Content-Type', 'application/json')
+
+        try:
+            last_line = get_last_line()
+
+            if last_line:
+                parser = ParserWrapper(Parser)
+                response = parser.run([last_line])
+                response = parser.parser.give_hint()
+
+                if response:
+                    return json.dumps({'hint': str(response)})
+
+            return json.dumps({'hint': 'No further reduction is possible.'})
+        except Exception as e:
+            return json.dumps({'error': str(e)})
+
+
+class validate(object):
+    def POST(self):
+        web.header('Content-Type', 'application/json')
+
+        data = web.input(data='').data
+        lines = map(str, data.split('\n'))
+
+        i = 0
+        skipped = 0
+
+        try:
+            # Get the first none empty line.
+            for i in range(0, len(lines)):
+                last_line = lines[i].strip()
+
+                if not last_line:  # or last_line in ['?']:
+                    skipped += 1
+                    continue
+
+                break
+
+            # Validate each none empty line with the following none empty line.
+            for i in range(i + 1, len(lines)):
+                line = lines[i].strip()
+
+                if not line:  # or line in ['?']:
+                    skipped += 1
+                    continue
+
+                if not validate_expression(last_line, line):
+                    i -= 1
+                    break
+
+                last_line = line
+
+            return json.dumps({'validated': i - skipped})
+        except Exception as e:
+            i -= 1
+            return json.dumps({'error': str(e), 'validated': i - skipped})
+
+
+if __name__ == "__main__":
+    app.run()

src/frontend/css/editor.css

 html {
-    background-color: #ccc;
+    background-color: #ccddef;
     margin: 0;
     padding: 0;
 }
@@ -10,15 +10,29 @@ body {
     font: 16px/24px Verdana, Arial, sans;
 }
 
+#loader {
+    background: url(/static/img/load.gif) no-repeat scroll 0 0 transparent;
+    height: 31px;
+    width: 31px;
+    display: none;
+    position: absolute;
+    margin-top: -5px;
+    margin-left: 16px;
+}
+
 .panel {
-    border: 3px solid #bbb;
     background-color: #fff;
-    width: 47%;
+    border: 3px solid #bbb;
+    cursor: text;
+    min-height: 400px;
+    padding-bottom: 10px;
     position: absolute;
+    top: 58px;
+    width: 47%;
 }
 
 #input {
-    float:left;
+    float: left;
     left: 2%;
 }
 
@@ -27,22 +41,79 @@ body {
     border: 0;
     margin: 0;
     padding: 0;
-    height: 100%;
+    height: 388px;
     overflow-y: visible;
     font: 16px/24px Verdana, Arial, sans;
 }
 
+.box {
+    padding: 10px 15px 0 15px;
+}
+
 #math {
     float:right;
     right: 2%;
 }
 
-.box {
-    height: 380px;
-    padding: 10px;
+#math .box {
+    padding: 10px 15px 0 40px;
+    background: no-repeat scroll 15px 13px transparent;
 }
 
-#math .box {
-    height: 380px;
-    padding: 10px;
+#math .box.correct {
+    background-image: url(/static/img/tick.png);
+}
+
+#math .box.wrong {
+    background-image: url(/static/img/cross.png);
+}
+
+#math .hint {
+    padding: 10px 15px 0 40px;
+    background: url(/static/img/info.png) no-repeat scroll 15px 13px transparent;
+    color: #666;
+    font-size: 14px;
+    line-height: 20px;
+}
+
+#control-buttons {
+    height: 21px;
+    left: 2%;
+    line-height: 0;
+    margin-bottom: 16px;
+    position: absolute;
+    vertical-align: top;
+}
+
+.separator {
+    border-right: 1px solid #999;
+    display: inline-block;
+    width: 0;
+    height: 21px;
+    margin: 1px 5px;
+    vertical-align: top;
+}
+
+.panel .label {
+    background-color: #fff;
+    border: 1px solid #ccc;
+    clear: both;
+    float: left;
+    font-size: 10px;
+    line-height: 14px;
+    margin-left: 4px;
+    margin-top: -12px;
+    padding: 2px;
+}
+
+/* Codemirror should not resize the input area. */
+/*
+.CodeMirror-scroll {
+    height: auto;
+    overflow: visible;
+}
+
+.CodeMirror-lines {
+    padding: 0 !important;
 }
+*/

src/frontend/js/editor.js

@@ -3,42 +3,199 @@
     var math = null; // the element jax for the math output
 
     // Hide and show the box (so it doesn't flicker as much)
-    var hide_box = function () {box.style.visibility = "hidden"}
-    var show_box = function () {box.style.visibility = "visible"}
+    //var hide_box = function () {box.style.visibility = 'hidden'}
+    //var show_box = function () {box.style.visibility = 'visible'}
     var trigger_update = true;
 
-    // Initialise codemirror environment
-    var input_textarea = document.getElementById("MathInput"),
-        input_box = CodeMirror.fromTextArea(input_textarea, {
-            value: '',
-            mode:  'r',
-            matchBrackets: true,
-            onChange: function(f) { trigger_update = true; }
+    //// Initialise codemirror environment
+    //var input_textarea = document.getElementById('MathInput'),
+    //    input_box = CodeMirror.fromTextArea(input_textarea, {
+    //        value: '',
+    //        mode:  'r',
+    //        matchBrackets: true,
+    //        onChange: function(f) { trigger_update = true; }
+    //    });
+
+    var input_textarea = $('#MathInput');
+
+    input_textarea.change(function(){ trigger_update = true; })
+        .keyup(function(){ trigger_update = true; });
+
+    $('#input').click(function(){
+        //input_box.focus();
+        input_textarea.focus();
     });
 
     // Get the element jax when MathJax has produced it.
-    QUEUE.Push(function () {
-        math = MathJax.Hub.getAllJax("MathOutput")[0];
-        box = document.getElementById("box");
-        show_box();
+    QUEUE.Push(function() {
+        //math = MathJax.Hub.getAllJax('MathOutput')[0];
+        //box = document.getElementById('box');
+        //show_box();
 
         // The onchange event handler that typesets the math entered
         // by the user.  Hide the box, then typeset, then show it again
         // so we don't see a flash as the math is cleared and replaced.
-        var update_math = function (tex) {
-            //var start = '\\begin{equation}\\begin{split}';
-            //var end = '\\end{split}\\end{equation}';
-            //tex = start + tex.replace(/\n/g, end + start) + end;
-            //tex = '\\displaystyle{' + tex.replace(/\n/g, '\\\\') + '}';
-            //tex = '`' + tex.replace(/\n/g, '\\\\') + '`';
-            QUEUE.Push(hide_box, ["Text", math, tex], show_box);
+        var update_math = function(tex) {
+            var parts = tex.split('\n');
+
+            var math_container = $('#math'),
+                math_lines = math_container.find('div.box script'),
+                mathjax_instances = MathJax.Hub.getAllJax('math');
+
+            var real_lines = 0,
+                updated_line = -1;
+
+            for (var p = 0; p < parts.length; p++) {
+                if (!parts[p])
+                    continue;
+
+                // TODO: Mark updated line as "pending" (e.g. remove "wrong"
+                // and "good" class names from element).
+
+                if (real_lines < math_lines.length) {
+                    var elem = mathjax_instances[real_lines];
+
+                    // Update the line when the input is modified.
+                    if (elem.originalText != parts[p]) {
+                        updated_line = real_lines;
+                        QUEUE.Push(['Text', elem, parts[p]]);
+                    }
+
+                    if (updated_line > -1) {
+                        // Remove the out-of-date status information. This will
+                        // be done from now on for all remaining lines, whether
+                        // they are up-to-date or not.
+                        $(math_lines[real_lines]).parent()
+                            .removeClass('wrong').removeClass('correct');
+                    }
+                } else {
+                    var line = '`' + parts[p] + '`',
+                        elem = $('<div class="box"/>').text(line);
+
+                    math_container.append(elem);
+
+                    QUEUE.Push(['Typeset', MathJax.Hub, elem[0]]);
+                }
+
+                real_lines++;
+            }
+
+            // Remove old hints, given that at least one line is updated.
+            // Iterate over the DOM nodes until the updated line is found,
+            // and remove all following hint nodes.
+            var line_count = 0, i = 0, elems = $('#math div');
+
+            if(updated_line == -1)
+                updated_line = real_lines + 1;
+
+            for(; i < elems.length; i++) {
+                var elem = $(elems[i]);
+
+                if (line_count == updated_line) {
+                    if (elem.hasClass('hint'))
+                        elem.remove();
+                } else if (elem.hasClass('box')) {
+                    line_count++;
+                }
+            }
+
+            QUEUE.Push((function(math_lines, real_lines) {
+                return function() {
+                    for (var p = real_lines; p < math_lines.length; p++) {
+                        $(math_lines[p].parentNode).remove();
+                    }
+                };
+            })(math_lines, real_lines));
         }
 
         setInterval(function() {
             if (trigger_update) {
                 trigger_update = false;
-                update_math(input_box.getValue());
+                //update_math(input_box.getValue());
+                update_math(input_textarea.val());
             }
-        }, 50);
+        }, 100);
     });
+
+    var loader = $('#loader');
+
+    window.show_loader = function() {
+        loader.show().css('display', 'inline-block');
+    };
+
+    window.hide_loader = function() {
+        loader.hide();
+    };
+
+    window.hint_input = function() {
+        show_loader();
+
+        // TODO: disable input box and enable it when this ajax request is done
+        // (on failure and success).
+        //$.post('/hint', {data: input_box.getValue()}, function(response) {
+        $.post('/hint', {data: input_textarea.val()}, function(response) {
+            if (!response)
+                return;
+
+            console.log(response);
+
+            $('#math div').last().filter('.hint').remove();
+
+            var elem = $('<div class=hint/>');
+            elem.text(response.hint);
+            $('#math').append(elem);
+
+            hide_loader();
+        }, 'json').error(function(e) {
+            console.log('error:', e);
+
+            hide_loader();
+        });
+    };
+
+    window.validate_input = function() {
+        show_loader();
+
+        // TODO: disable input box and enable it when this ajax request is done
+        // (on failure and success).
+        //$.post('/validate', {data: input_box.getValue()}, function(response) {
+        $.post('/validate', {data: input_textarea.val()}, function(response) {
+            if (!response)
+                return;
+
+            var math_container = $('#math'),
+                math_lines = math_container.find('div.box');
+
+            console.log(response.validated);
+
+            var i = 0;
+
+            // Mark every line as correct (and remove previous class names).
+            for(; i < math_lines.length && i <= response.validated; i++)
+                $(math_lines[i]).removeClass('wrong').addClass('correct');
+
+            if (i < math_lines.length) {
+                // Mark the current line as wrong.
+                $(math_lines[i]).removeClass('correct').addClass('wrong');
+
+                // Remove the status indicator from the remaining lines.
+                for(i += 1; i < math_lines.length; i++)
+                    $(math_lines[i]).removeClass('correct')
+                        .removeClass('wrong');
+            }
+
+            hide_loader();
+        }, 'json').error(function(e) {
+            console.log('error:', e);
+
+            hide_loader();
+        });
+    };
+
+    window.clear_input = function() {
+        input_textarea.val('');
+        $('#math .box,#math .hint').remove();
+        trigger_update = true;
+        hide_loader();
+    };
 })(jQuery);

src/frontend/tpl/editor.html

@@ -3,27 +3,28 @@
     <head>
         <meta http-equiv="content-type" content="text/html; charset=utf-8">
         <title>Mathematical term rewriting frontend</title>
-        <script type="text/javascript" src="../../../build/external/jquery/jquery.min.js"></script>
+        <script type="text/javascript" src="/static/build/external/jquery/jquery.min.js"></script>
         <script type="text/javascript"
-            src="../../../external/mathjax/MathJax.js?config=AM_HTMLorMML-full"></script>
-        <link rel="stylesheet" href="../../../external/codemirror2/lib/codemirror.css">
-        <link rel="stylesheet" href="../../../src/frontend/css/editor.css">
-        <script src="../../../external/codemirror2/lib/codemirror.js"></script>
-        <script src="../../../external/codemirror2/mode/r/r.js"></script>
+            src="/static/external/mathjax/MathJax.js?config=AM_HTMLorMML-full"></script>
+        <link rel="stylesheet" href="/static/external/codemirror2/lib/codemirror.css">
+        <link rel="stylesheet" href="/static/frontend/css/editor.css">
+        <script src="/static/external/codemirror2/lib/codemirror.js"></script>
+        <script src="/static/external/codemirror2/mode/r/r.js"></script>
     </head>
     <body>
+        <div id="control-buttons"><button onclick=window.clear_input()>clear</button><div class="separator"></div><button onclick=window.hint_input()>hint</button><button onclick=window.validate_input()>validate</button><div id="loader"></div></div>
+
         <div id="input" class="panel">
+            <div class="label">Input view</div>
             <div class="box">
                 <textarea id="MathInput"></textarea>
             </div>
         </div>
 
         <div id="math" class="panel">
-            <div class="box" id="box" style="visibility:hidden">
-                <div id="MathOutput">``</div>
-            </div>
+            <div class="label">Math view</div>
         </div>
 
-        <script type="text/javascript" src="../../../src/frontend/js/editor.js"></script>
+        <script type="text/javascript" src="/static/frontend/js/editor.js"></script>
     </body>
 </html>

src/parser.py

@@ -28,6 +28,10 @@ import Queue
 import re
 
 
+# Rewriting an expression is stopped after this number of steps is passed.
+MAXIMUM_REWRITE_STEPS = 100
+
+
 # Check for n-ary operator in child nodes
 def combine(op, op_type, *nodes):
     # At least return the operator.
@@ -255,21 +259,27 @@ class Parser(BisonParser):
         self.possibilities = find_possibilities(self.root_node)
 
     def display_hint(self):
-        self.find_possibilities()
+        hint = self.give_hint()
 
-        if self.interactive:
-            if self.possibilities:
-                print self.possibilities[0]
+        if hint:
+            print hint
         else:
             print 'No further reduction is possible.'
 
+    def give_hint(self):
+        self.find_possibilities()
+
+        if self.possibilities:
+            return self.possibilities[0]
+
     def display_possibilities(self):
         self.find_possibilities()
 
         for i, p in enumerate(self.possibilities):
             print '%d %s' % (i, p)
 
-    def rewrite(self, index=0, verbose=False, check_implicit=True):
+    def rewrite(self, index=0, include_step=False, verbose=False,
+            check_implicit=True):
         self.find_possibilities()
 
         if not self.possibilities:
@@ -326,19 +336,32 @@ class Parser(BisonParser):
         if verbose and not self.verbose:
             print self.root_node
 
+        if include_step:
+            return suggestion, self.root_node
+
         return self.root_node
 
-    def rewrite_all(self, verbose=False):
-        i = 0
+    def rewrite_all(self, include_steps=False, check_implicit=True,
+            verbose=False):
+        steps = []
 
-        while self.rewrite(verbose=verbose):
-            i += 1
+        for i in range(MAXIMUM_REWRITE_STEPS):
+            obj = self.rewrite(verbose=verbose, check_implicit=check_implicit,
+                include_step=include_steps)
 
-            if i > 100:
-                print 'Too many rewrite steps, aborting...'
+            if not obj:
                 break
 
+            if include_steps:
+                steps.append(obj)
+
+        if i > MAXIMUM_REWRITE_STEPS:
+            print 'Too many rewrite steps, aborting...'
+
         if not verbose or not i:
+            if include_steps:
+                return steps
+
             return self.root_node
 
     #def hook_run(self, filename, retval):

src/validation.py

@@ -9,9 +9,22 @@ def validate(exp, result):
     Validate that exp =>* result.
     """
     parser = ParserWrapper(Parser)
+
     exp = parser.run([exp])
     result = parser.run([result])
 
+    # Compare the simplified expressions first, in order to avoid the
+    # computational intensive traversal of the possibilities tree.
+    parser.set_root_node(exp)
+    a = parser.rewrite_all()
+
+    parser.set_root_node(result)
+    b = parser.rewrite_all()
+
+    if not a or not a.equals(b):
+        return False
+
+    # TODO: make sure cycles are avoided / eliminated using cycle detection.
     def traverse_preorder(node, result):
         if node.equals(result):
             return True

static/build/external/jquery

+../../../build/external/jquery
\ No newline at end of file

static/external/codemirror2

+../../external/codemirror2
\ No newline at end of file

static/external/mathjax

+../../external/mathjax
\ No newline at end of file

static/frontend/css

+../../src/frontend/css
\ No newline at end of file

static/frontend/js

+../../src/frontend/js
\ No newline at end of file

tests/parser.py

@@ -21,6 +21,12 @@ class ParserWrapper(object):
 
         self.parser = base_class(file=self, read=self.read, **kwargs)
 
+    def __getattr__(self, name):
+        if name in self.__dict__:
+            return getattr(self, name)
+
+        return getattr(self.parser, name)
+
     def readline(self, nbytes=False):
         return self.read(nbytes)