Calling into Agda now works.

Ignore-this: 719d2f36ecfb6d65497635a0ce13b42b

darcs-hash:20110203140858-01858-e3480b3cb12e4d8f622653b52911194741d4e16a.gz

agda-test.el

@@ -4,13 +4,33 @@
 ;; test sevenocity: seven is 7;
 
 (defvar agda2-error-buffer-name "*Agda errors*")
+(defvar agda2-information-buffer-name "*Agda information*")
 (defvar agda2-test-regexp
   "test\\s-*\\(.*?\\)\\s-*:\\s-*\\(.*?\\)\\s-+is\\s-+\\(.*\\);")
 
+(defun agda2-normalise-string (expr)
+  "The authors of agda2-mode, in their infinite mercy and wisdom,
+  implemented agda2-compute-normalised by having GHCi write elisp
+  code to insert the normalised value into a buffer, which
+  agda2-compute-normalised then executes. Hence, the easiest way
+  to get at the normalised value of an Agda expression is to call
+  agda2-compute-normalised and then inspect the *Agda
+  information* buffer. It may look like you need to inspect the
+  *Normal Form* buffer, but your minibuffer is full of
+  lies. Trust me on this."
+  (agda2-compute-normalised-toplevel (substring-no-properties expr))
+  (with-current-buffer agda2-information-buffer-name
+    (buffer-substring-no-properties (point-min) (point-max))))
+
 (defun agda2-run-test (testname lhs rhs)
-  (with-current-buffer agda2-error-buffer-name
-    (insert (format "Testname: %s, LHS: %s, RHS: %s\n" testname lhs rhs))
-    (agda2-go "cmd_compute"))
+  (let ((lhsval (agda2-normalise-string lhs))
+	(rhsval (agda2-normalise-string rhs)))
+    (with-current-buffer agda2-error-buffer-name
+      (insert (format "Testname: %s, LHS: %s, RHS: %s\n" testname lhs rhs))
+      (insert
+       (if (string-equal lhsval rhsval)
+	   (format "Success! LHS=%s, RHS=%s\n" lhsval rhsval)
+	 (format "Failure: LHS=%s, RHS=%s\n" lhsval rhsval))))))
 
 ;; test negativity: -1 is minus one;