aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ML4PG/ssreflect/menus.el
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ML4PG/ssreflect/menus.el')
-rw-r--r--contrib/ML4PG/ssreflect/menus.el308
1 files changed, 0 insertions, 308 deletions
diff --git a/contrib/ML4PG/ssreflect/menus.el b/contrib/ML4PG/ssreflect/menus.el
deleted file mode 100644
index 226c1212..00000000
--- a/contrib/ML4PG/ssreflect/menus.el
+++ /dev/null
@@ -1,308 +0,0 @@
-;;; The menu interaction
-
-(easy-menu-define ml4pg-menu global-map "Statistics"
- '("Statistics"
- ("Configuration"
- ("Algorithm"
- ["K-means" (ml4pg-change-algorithm "k")
- :selected (string= ml4pg-algorithm "k")
- :style toggle
- :help "Use k-means algorithm"]
- ["Gaussian" (ml4pg-change-algorithm "g")
- :selected (string= ml4pg-algorithm "g")
- :style toggle
- :active (string= ml4pg-ml-system "m")
- :help "Use Gaussian algorithm"]
- ["EM" (ml4pg-change-algorithm "e")
- :selected (string= ml4pg-algorithm "e")
- :style toggle
- :active (string= ml4pg-ml-system "w")
- :help "Use Simple EM algorithm"]
- ["FarthestFirst" (ml4pg-change-algorithm "f")
- :selected (string= ml4pg-algorithm "f")
- :style toggle
- :active (string= ml4pg-ml-system "w")
- :help "Use FarhestFirst algorithm"])
- ("Granularity"
- ["1" (ml4pg-change-granularity 1)
- :selected (eq ml4pg-granularity-level 1)
- :style toggle
- :help "We will use 3 clusters"]
- ["2" (ml4pg-change-granularity 2)
- :selected (eq ml4pg-granularity-level 2)
- :style toggle
- :help "We will use 5 clusters"]
- ["3" (ml4pg-change-granularity 3)
- :selected (eq ml4pg-granularity-level 3)
- :style toggle
- :help "We will use 10 clusters"]
- ["4" (ml4pg-change-granularity 4)
- :selected (eq ml4pg-granularity-level 4)
- :style toggle
- :help "We will use 15 clusters"]
- ["5" (ml4pg-change-granularity 5)
- :selected (eq ml4pg-granularity-level 5)
- :style toggle
- :help "We will use 20 clusters"])
- ("Frequencies"
- ["1" (ml4pg-change-frequency 1)
- :selected (eq ml4pg-frequency-precision 1)
- :style toggle
- :help "The experiments will be run 100 times"]
- ["2" (ml4pg-change-frequency 2)
- :selected (eq ml4pg-frequency-precision 2)
- :style toggle
- :help "The experiments will be run 500 times"]
- ["3" (ml4pg-change-frequency 3)
- :selected (eq ml4pg-frequency-precision 3)
- :style toggle
- :help "The experiments will be run 1000 times"]))
- ["Extract info up to point" (ml4pg-extract-feature-theorems)
- :keys "C-c SPC"]
- ["Show clusters" (ml4pg-show-clusters-bis)
- :keys "C-c c"]
- ["Show similar theorems" (ml4pg-show-clusters-of-theorem)
- :keys "C-c m"]
- ["Export library" (ml4pg-save-numbers)
- :keys "C-c n"]
- ["Show cluster libraries" (ml4pg-exported-libraries)]
- ["Activate Icons" (ml4pg-activate-icons)]
-))
-
-(easy-menu-remove-item global-map '("menu-bar") "Statistics")
-
-(easy-menu-add-item nil nil ml4pg-menu "help-menu")
-
-(defun ml4pg-activate-icons ()
- (interactive)
- (progn
- (easy-menu-remove-item nil '("Statistics") "Activate Icons")
- (define-key coq-mode-map [tool-bar statistical-hint]
- (list 'menu-item "Statistical Hint" 'ml4pg-show-clusters-of-theorem
- :help "Statistical Hint"
- :image (list 'image :type 'xpm
- :file (concat ml4pg-home-dir "icons/sh-hint.xpm"))))
- (define-key coq-mode-map [tool-bar clustering]
- (list 'menu-item "Clustering" 'ml4pg-show-clusters-bis
- :help "Clustering"
- :image (list 'image :type 'xpm
- :file (concat ml4pg-home-dir "icons/clustering.xpm"))))))
-
-
-(defvar ml4pg-ml-system "w")
-(defvar ml4pg-algorithm "k")
-(defvar ml4pg-granularity-level 3)
-(defvar ml4pg-frequency-precision 1)
-(defvar ml4pg-iterative nil)
-(defvar ml4pg-save-automatically nil)
-(defvar ml4pg-level "g")
-
-
-(defun ml4pg-change-level (n)
- (setq ml4pg-level n))
-
-(defun ml4pg-change-algorithm (s)
- (setq ml4pg-algorithm s))
-
-(defun ml4pg-change-ml-system (s)
- (setq ml4pg-ml-system s)
- (setq ml4pg-algorithm "k")
- (cond ((string= s "w")
- (setq ml4pg-iterative nil)
- ))
- )
-
-(defun ml4pg-change-granularity (n)
- (setq ml4pg-granularity-level n))
-
-(defun ml4pg-change-frequency (n)
- (setq ml4pg-frequency-precision n))
-
-(defun ml4pg-change-iterative-search ()
- (setq ml4pg-iterative (not ml4pg-iterative)))
-
-(defun ml4pg-change-save ()
- (setq ml4pg-save-automatically (not ml4pg-save-automatically)))
-
-
-;(easy-menu-add-item nil '("Statistics") statistics-menu "help-menu")
-
-(defun ml4pg-change-algorithm-interactive ()
- (interactive)
- (let ((alg (read-string
- "What algorithm do you want to use (k-means -> k, Gaussian -> g): ")))
- (setf ml4pg-algorithm (cond ((string= "g" alg) "g")
- ((string= "k" alg) "k")
- (t ml4pg-algorithm)))))
-
-(defun ml4pg-change-granularity-interactive ()
- (interactive)
- (let ((alg (read-string
- "Introduce the granularity level (values from 1 to 5): ")))
- (setf ml4pg-granularity-level (cond ((string= "1" alg) 1)
- ((string= "2" alg) 2)
- ((string= "3" alg) 3)
- ((string= "4" alg) 4)
- ((string= "5" alg) 5)
- (t granularity-level)))))
-
-(defun ml4pg-change-frequency-interactive ()
- (interactive)
- (let ((alg (read-string
- "Introduce the precision of the frequencies that you want to obtain (values from 1 to 3): ")))
- (setf ml4pg-frequency-precision (cond ((string= "1" alg) 1)
- ((string= "2" alg) 2)
- ((string= "3" alg) 3)
- (t ml4pg-frequency-precision)))))
-
-(defun change-iterative-interactive ()
- (interactive)
- (let ((alg (read-string
- "Do you want to perform iterative search? (yes -> y, no -> n): ")))
- (setf ml4pg-iterative (cond ((string= "y" alg) 1)
- ((string= "n" alg) 2)
- (t ml4pg-iterative)))))
-
-
-
-(defun ml4pg-exported-libraries ()
- (interactive)
- (easy-menu-remove-item nil '("Statistics") "Show cluster libraries")
- (easy-menu-add-item nil '("Statistics")
- (cons "Available libraries for clustering:"
- (cons ["Current" nil
- :selected t
- :style toggle
- :help "Use the current library for clustering"]
- (ml4pg-select-libraries)))))
-
-
-(defun ml4pg-select-libraries ()
- (ml4pg-available-libraries)
- (ml4pg-available-dirs)
- (append (ml4pg-select-libraries-aux ml4pg-libs nil) (ml4pg-libraries-dirs)))
-
-
-(defun ml4pg-select-libraries-aux (temp temp2)
- (if (endp temp)
- temp2
- (ml4pg-select-libraries-aux (cdr temp) (append temp2 (list (ml4pg-menu-library (car temp)))))))
-
-
-
-
-(defvar ml4pg-libs nil)
-
-(defun ml4pg-available-libraries ()
- (shell-command (concat "ls " ml4pg-home-dir "libs/ssreflect | grep .csv | wc -l"))
- (let ((n nil)
- (i 0))
- (with-current-buffer "*Shell Command Output*"
- (beginning-of-buffer)
- (setq n (string-to-number (format "%s" (read (current-buffer))))))
- (shell-command (concat "ls " ml4pg-home-dir "libs/ssreflect | grep .csv"))
- (with-current-buffer "*Shell Command Output*"
- (progn (beginning-of-buffer)
- (while (< i n)
- (let ((r (format "%s" (read (current-buffer)))))
- (progn (setq i (1+ i))
- (setq ml4pg-libs (append ml4pg-libs (list (subseq r 0 (search "." r))))))))))))
-
-
-
-(defvar ml4pg-dirs nil)
-
-(defun ml4pg-available-dirs ()
- (shell-command (concat "ls -d " ml4pg-home-dir "libs/ssreflect/*/ | wc -l"))
- (let ((n nil)
- (i 0))
- (with-current-buffer "*Shell Command Output*"
- (beginning-of-buffer)
- (setq n (string-to-number (format "%s" (read (current-buffer))))))
- (shell-command (concat "ls -d " ml4pg-home-dir "libs/ssreflect/*/"))
- (with-current-buffer "*Shell Command Output*"
- (progn (beginning-of-buffer)
- (while (< i n)
- (let ((r (format "%s" (read (current-buffer)))))
- (progn (setq i (1+ i))
- (setq ml4pg-dirs (append ml4pg-dirs (list (subseq r (length (concat ml4pg-home-dir "libs/ssreflect/")) (1- (length r)))))))))))
- ))
-
-
-
-
-(defun ml4pg-libraries-dirs ()
- (do ((temp ml4pg-dirs (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (setf temp2 (append temp2 (list (append (list (car temp)) (ml4pg-libraries-dir (car temp))))))))
-
-
-
-(defun ml4pg-libraries-dir (dir)
- (shell-command (concat "ls " ml4pg-home-dir "libs/ssreflect/" dir "/ | grep _names | wc -l"))
- (let ((n nil)
- (i 0)
- (temp nil))
- (with-current-buffer "*Shell Command Output*"
- (beginning-of-buffer)
- (setq n (string-to-number (format "%s" (read (current-buffer))))))
- (shell-command (concat "ls " ml4pg-home-dir "libs/ssreflect/" dir "/ | grep _names"))
- (with-current-buffer "*Shell Command Output*"
- (progn (beginning-of-buffer)
- (while (< i n)
- (let* ((r1 (format "%s" (read (current-buffer))))
- (r (subseq r1 0 (search "_names" r1))))
- (progn (setq i (1+ i))
- (setq temp (append temp (list (ml4pg-menu-library-dir (subseq r 0 (search "." r)) dir)))))))
-))
- temp))
-
-
-
-(defun ml4pg-menu-library-dir (item dir)
- (vector item (list 'ml4pg-change-library (concat dir "/" item))
- :selected (list 'ml4pg-string-member (concat dir "/" item) 'ml4pg-libs-menus)
- :style 'toggle
- :help (format "Use the %s library for clustering" item)))
-
-(defun ml4pg-menu-library (item)
- (vector item (list 'change-library item)
- :selected (list 'ml4pg-string-member item 'ml4pg-libs-menus)
- :style 'toggle
- :help (format "Use the %s library for clustering" item)))
-
-
-
-(defvar ml4pg-libs-menus nil)
-
-(defun ml4pg-string-member (string list)
- (do ((temp list (cdr temp))
- (is nil))
- ((or (endp temp) is) is)
- (if (string= string (car temp))
- (setf is t))))
-
-
-(defun ml4pg-change-library (string)
- (if (ml4pg-string-member string ml4pg-libs-menus)
- (ml4pg-remove-from-menus string)
- (setq ml4pg-libs-menus (append ml4pg-libs-menus (list string)))))
-
-
-(defun ml4pg-remove-from-menus (string)
- (do ((temp ml4pg-libs-menus (cdr temp))
- (temp2 nil))
- ((endp temp) (setf ml4pg-libs-menus temp2))
- (if (not (string= string (car temp)))
- (setf temp2 (append temp2 (list (car temp)))))))
-
-
-
-
-
-
-
-
-
-