;; This file:
;;   http://angg.twu.net/AGDA/find-agdatype.el.html
;;   http://angg.twu.net/AGDA/find-agdatype.el
;;           (find-angg "AGDA/find-agdatype.el")
;; Author: Eduardo Ochs <eduardoochs@gmail.com>
;; Date: 2022feb04
;; Public domain.
;; Status: not thoroughly tested.
;;
;; See: http://angg.twu.net/eev-agda.html
;; This is a cleaned-up version of:
;;   (find-angg "AGDA/find-agdatype-2021.el")
;;
;; I've tried to make this version independent of eev.
;; If you don't have eev you will probably have to use something like
;; `C-e C-x C-e' to the execute sexps in comments; with eev you can
;; execute them with `M-e'. See:
;;   (find-eev-quick-intro "2. Evaluating Lisp" "When you type `M-e'")
;;   (find-eev-quick-intro "3. Elisp hyperlinks" "eek")
;;   http://angg.twu.net/eev-intros/find-eev-quick-intro.html#2
;;   http://angg.twu.net/eev-intros/find-eev-quick-intro.html#3

(if (not (fboundp 'eek))

(defun eek (str)
  "Execute STR as a keyboard macro. See `edmacro-mode' for the exact format.\n
An example: (eek \"C-x 4 C-h\")"
  (interactive "sKeys: ")
  (execute-kbd-macro (read-kbd-macro str)))

)

(defun eek-at-agda-pg (str)
  "Go to the previous goal, run (eek STR) there, and go back."
  (save-excursion
    (agda2-previous-goal)
    (eek str)))

;; Test: (ee-agda-eekify "  foo  bar  ")
;;   --> "foo SPC bar"
;;
(defun ee-agda-eekify (str)
  "Convert STR - an expression in Agda - to a sequence of keys for `eek'."
  (let* ((str1 (string-trim str))
	 (str2 (replace-regexp-in-string "[ \t]+" " " str1))
         (str3 (replace-regexp-in-string " " " SPC " str2)))
    str3))

(defun find-agdatype (agdaexpr &rest rest)
  "Show the type of AGDAEXPR in the buffer \"*Inferred Type*\".
This function runs `C-c C-d AGDAEXPR RET' at point using `eek'.
This only works in agda2-mode. This is a quick hack!"
  (eek (format "C-c C-d %s RET" (ee-agda-eekify agdaexpr)))
  '(See the buffer "*Inferred Type*"))

(defun find-agdanorm (agdaexpr &rest rest)
  "Show the normalized value of AGDAEXPR in the buffer \"*Normal Form*\".
This function runs `C-c C-n AGDAEXPR RET' at point using `eek'.
This only works in agda2-mode. This is a quick hack!"
  (eek (format "C-c C-n %s RET" (ee-agda-eekify agdaexpr)))
  '(See the buffer "*Normal Form*"))

(defun find-agdatypep (agdaexpr &rest rest)
  "Show the type of AGDAEXPR in the buffer \"*Inferred Type*\".
This function runs `C-c C-d AGDAEXPR RET' at the previous goal using `eek'.
This only works in agda2-mode. This is a quick hack!"
  (eek-at-agda-pg (format "C-c C-d %s RET" (ee-agda-eekify agdaexpr)))
  '(See the buffer "*Inferred Type*"))

(defun find-agdanormp (agdaexpr &rest rest)
  "Show the normalized value of AGDAEXPR in the buffer \"*Normal Form*\".
This function runs `C-c C-n AGDAEXPR RET' at the previous goal using `eek'.
This only works in agda2-mode. This is a quick hack!"
  (eek-at-agda-pg (format "C-c C-n %s RET" (ee-agda-eekify agdaexpr)))
  '(See the buffer "*Normal Form*"))







;;
;; (defun e () (interactive) (find-angg "AGDA/find-agdatype.el"))

;; Local Variables:
;; coding:  utf-8-unix
;; End: