;;; ob-acl2.el --- org-babel functions for ACL2

;; Copyright (C) Masaya Tojo <masaya@tojo.tokyo>

;; Author: Masaya Tojo
;; Keywords: literate programming
;; Homepage: https://git.tojo.tokyo/ob-acl2.git
;; Version: 0.1.0

;;; License:

;; This program is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 3, or (at your option)
;; any later version.
;;
;; This program is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.
;;
;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs.  If not, see <https://www.gnu.org/licenses/>.

;;; Commentary:

;; This is implemented by pouring expressions into a *shell* buffer,
;; which is a standard ACL2 execution environment.
;; Must run acl2 with *shell* before using it.

;;; Code:
(require 'ob)

(defun org-babel-acl2-clean-prompt (string)
  (string-join (butlast (split-string string "\n")) "\n"))

(defun org-babel-execute:acl2 (body params)
  (let ((full-body (org-babel-expand-body:generic body params))
        ;;; XXX: Using *shell* for now.
        (session (get-buffer "*shell*"))
        (pt (lambda ()
              (marker-position
               (process-mark (get-buffer-process (current-buffer))))))
        (ob-babel-p (lambda ()
                      (goto-char (point-max))
                      (forward-line -1)
                      (beginning-of-line)
                      (let ((line (thing-at-point 'line t)))
                        (goto-char (point-max))
                        (and (< 9 (length line))
                             (equal (substring line -9 -1) "OB-BABEL"))))))
    (org-babel-acl2-clean-prompt
     (org-babel-comint-in-buffer session
       (let ((start (funcall pt)))
         (with-temp-buffer
           (insert full-body)
           (comint-send-region session (point-min) (point-max))
           (comint-send-string session "\n")
           (comint-send-string session "'ob-babel\n"))
         (while (or (equal start (funcall pt))
                    (not (funcall ob-babel-p)))
           (sleep-for 0.1))
         (goto-char (point-max))
         (forward-line -1)
         (beginning-of-line)
         (let ((end (point)))
           (goto-char (point-max))
           (buffer-substring start end)))))))

(provide 'ob-acl2)

;;; ob-acl2.el ends here