;; This file:
;;   http://angg.twu.net/AGDA/find-agdatype-2021.el.html
;;   http://angg.twu.net/AGDA/find-agdatype-2021.el
;;           (find-angg "AGDA/find-agdatype-2021.el")
;; Author: Eduardo Ochs <eduardoochs@gmail.com>
;; Version: 2022feb01
;; Public domain.
;;
;; This is obsolete. The new version is here:
;;   http://angg.twu.net/AGDA/find-agdatype.el.html
;;   http://angg.twu.net/AGDA/find-agdatype.el
;;           (find-angg "AGDA/find-agdatype.el")
;;
;; See:     http://angg.twu.net/eev-agda.html
;; Used by: (find-angg "AGDA/Postulate1.agda")
;;          (find-angg "AGDA/TestStrings.agda")
;;          (find-angg "AGDA/TestPublic.agda")
;; and lots of other files.
;;
;; A quirk: sometimes we need to open modules with "open ... public"
;; to make find-agdatype and find-agdanorm see certain symbols.
;; See: https://lists.chalmers.se/pipermail/agda/2022/012862.html
;;      https://lists.chalmers.se/pipermail/agda/2022/012863.html
;;      http://angg.twu.net/AGDA/TestPublic.agda.html
;;      http://angg.twu.net/AGDA/TestPublic.agda
;;              (find-angg "AGDA/TestPublic.agda")



;; «.video-0»		(to "video-0")
;; «.find-agdatype»	(to "find-agdatype")
;; «.find-agdatype2»	(to "find-agdatype2")


;; «video-0»  (to ".video-0")
;; "On find-agdatype and find-agdatype2 - PRELIMINARY VERSION!" (2021dec29)
;; http://angg.twu.net/eev-videos/2021-find-agdatype.mp4
;; https://www.youtube.com/watch?v=mqW_rmQPZ_w
;;  (find-ssr-links     "2021findagdatype" "2021-find-agdatype" "mqW_rmQPZ_w")
;;  (code-eevvideo      "2021findagdatype" "2021-find-agdatype" "mqW_rmQPZ_w")
;;  (code-eevlinksvideo "2021findagdatype" "2021-find-agdatype" "mqW_rmQPZ_w")
;; (find-2021findagdatypevideo "0:00")




;;;   __ _           _                       _       _                    
;;;  / _(_)_ __   __| |       __ _  __ _  __| | __ _| |_ _   _ _ __   ___ 
;;; | |_| | '_ \ / _` |_____ / _` |/ _` |/ _` |/ _` | __| | | | '_ \ / _ \
;;; |  _| | | | | (_| |_____| (_| | (_| | (_| | (_| | |_| |_| | |_) |  __/
;;; |_| |_|_| |_|\__,_|      \__,_|\__, |\__,_|\__,_|\__|\__, | .__/ \___|
;;;                                |___/                 |___/|_|         
;;
;; «find-agdatype»  (to ".find-agdatype")
;; Tests:
;;
;;       (ee-agda-eekify "  foo  bar  ")
;;  (eek (ee-agda-eekify "  foo  bar  "))
;;
;;  foo -- bar -- plic
;;  (eek "<up> <<ee-agda-boc>>")
;;  (eek "<up> <<ee-agda-boc>>")

(defun ee-agda-eekify (str)
  "Convert STR - an expression in Agda - to a sequence of keys."
  (let* ((str1 (string-trim str))
	 (str2 (replace-regexp-in-string "[ \t]+" " " str1))
         (str3 (replace-regexp-in-string " " " SPC " str2)))
    str3))

(defun ee-agda-boc ()
  "Go to the beginning of the Agda comment in the current line."
  (interactive)
  (goto-char (ee-bol))			; to beginning of line
  (search-forward "--" (ee-eol))	; to end of "--"
  (backward-char 2))			; to beginning of "--"

(defun find-agdatype (agdaexpr &rest rest)
  "Show the type of AGDAEXPR in the buffer \"*Inferred Type*\".
This function goes to the beginning of the Agda comment in the
current line, i.e., to the first occurrence of \"--\" in the
current line, and the runs `C-c C-d AGDAEXPR RET' there.
This only works in agda2-mode. This is a quick hack!"
  (ee-agda-boc)
  (apply 'find-eek (format "C-c C-d %s RET" (ee-agda-eekify agdaexpr)) rest)
  '(See the buffer "*Inferred Type*"))

(defun find-agdanorm (agdaexpr &rest rest)
  "Show the normalized value  of AGDAEXPR in the buffer \"*Normal Form*\".
This function goes to the beginning of the Agda comment in the
current line, i.e., to the first occurrence of \"--\" in the
current line, and the runs `C-c C-n AGDAEXPR RET' there.
This only works in agda2-mode. This is a quick hack!"
  (ee-agda-boc)
  (apply 'find-eek (format "C-c C-n %s RET" (ee-agda-eekify agdaexpr)) rest)
  '(See the buffer "*Normal Form*"))

;; 2022feb04:
(defun ee-at-agda-pg (sexp)
  "Go to the previous goal, eval SEXP, and go back."
  (save-excursion
    (agda2-previous-goal)
    (eval sexp)))

(defun find-agdatypep (agdaexpr &rest rest)
  "Like `find-agdatype', but runs inside the previous goal."
  (ee-at-agda-pg
   '(apply 'find-eek (format "C-c C-d %s RET" (ee-agda-eekify agdaexpr)) rest))
  '(See the buffer "*Inferred Type*"))

(defun find-agdanormp (agdaexpr &rest rest)
  "Like `find-agdanorm', but runs inside the previous goal."
  (ee-at-agda-pg
   '(apply 'find-eek (format "C-c C-n %s RET" (ee-agda-eekify agdaexpr)) rest))
  '(See the buffer "*Normal Form*"))




;;;   __ _           _                       _       _                    ____  
;;;  / _(_)_ __   __| |       __ _  __ _  __| | __ _| |_ _   _ _ __   ___|___ \ 
;;; | |_| | '_ \ / _` |_____ / _` |/ _` |/ _` |/ _` | __| | | | '_ \ / _ \ __) |
;;; |  _| | | | | (_| |_____| (_| | (_| | (_| | (_| | |_| |_| | |_) |  __// __/ 
;;; |_| |_|_| |_|\__,_|      \__,_|\__, |\__,_|\__,_|\__|\__, | .__/ \___|_____|
;;;                                |___/                 |___/|_|               
;;
;; «find-agdatype2»  (to ".find-agdatype2")

;; The hash table trick was based on this code:
;; (find-angg "emacs-lua/emlua.el" "emlua-quote")

(defun ee-agda-symbols-with-prefix (prefix &optional bigstr)
  (setq bigstr (or bigstr (buffer-substring-no-properties (point-min) (point-max))))
  (let* ((regexp (format "%s[0-9]+" prefix))
         (hash-table (make-hash-table :test 'equal))
         (l (length bigstr))
	 (start 0)
         mb me ms)
    (save-match-data
      (while (and (< start l) (string-match regexp bigstr start))
	(setq mb (match-beginning 0)
	      me (match-end 0)
	      ms (match-string 0 bigstr))
        (puthash ms t hash-table)
	(setq start me))
      hash-table)))

(defun ee-agda-new-symbol-with-prefix (prefix &optional hash-table)
  (setq hash-table (or hash-table (ee-agda-symbols-with-prefix prefix)))
  (cl-loop for k from 0
           do (let ((agdasymbol (format "%s%d" prefix k)))
		(if (not (gethash agdasymbol hash-table))
		  (cl-return agdasymbol)))))

;; Tests:
;;
;; (ee-agda-symbols-with-prefix "ee")
;; (ee-agda-new-symbol-with-prefix "ee")
;; (ee-agda-new-symbol-test ";;" "ee")
;;      (ee-agda-spaces-before-comment)
;;   -- (ee-agda-spaces-before-comment)
;;   -- (ee-agda-new-symbol-query "ee" "anexpr")
;;   -- (find-agdatype2-0 "anotherexpr")
;;
;; ee0 ee1 ee4
;;
(defun ee-agda-new-symbol-test (commentprefix agdaprefix)
  (let ((agdasymbol (ee-agda-new-symbol-with-prefix agdaprefix)))
    (eek "C-a")
    (insert (format "%s %s\n" commentprefix agdasymbol))))

(defun ee-agda-spaces-before-comment ()
  "Return the string between the BOL and the \"--\" in the current line."
  (interactive)
  (save-excursion
    (goto-char (ee-bol))
    (search-forward "--" (ee-eol))
    (buffer-substring-no-properties (ee-bol) (- (point) 2))))

(defun ee-agda-new-symbol-query (agdaprefix agdaexpr)
  (let ((spaces (ee-agda-spaces-before-comment))
	(agdasymbol (ee-agda-new-symbol-with-prefix "ee")))
    (format "%s%s : ?\n%s%s = %s\n"
	    spaces agdasymbol
	    spaces agdasymbol agdaexpr)))

(defun find-agdatype2-0 (agdaexpr)
  (eek "C-a")
  (insert (ee-agda-new-symbol-query "ee" agdaexpr))
  (eek "C-e"))

(defun find-agdatype2 (agdaexpr)
  "Check the type of AGDAEXPR using a trick that inserts two lines."
  (find-agdatype2-0 agdaexpr)
  (eek "C-c C-l"))






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