diff options
Diffstat (limited to 'contrib/ML4PG/coq/matlab_interaction.el')
| -rw-r--r-- | contrib/ML4PG/coq/matlab_interaction.el | 627 |
1 files changed, 0 insertions, 627 deletions
diff --git a/contrib/ML4PG/coq/matlab_interaction.el b/contrib/ML4PG/coq/matlab_interaction.el deleted file mode 100644 index bab2a30f..00000000 --- a/contrib/ML4PG/coq/matlab_interaction.el +++ /dev/null @@ -1,627 +0,0 @@ -;; This function starts Matlab - -(defun ml4pg-init-clusters () - (interactive) - (ml4pg-my-config-display) - (require 'comint) - (apply 'make-comint "matlab" *matlab-program* nil - (list "-nodesktop -r 0"))) - ;(apply 'make-comint "matlab" *matlab-program* nil (list "-nodesktop -r"))) - ; (shell-command "/home/jonathan/Matlab/bin/matlab -nodesktop -r - ; \"load /home/jonathan/Desktop/Research/Matlab/expt1_complete_goals.csv; kmeans_clusters_and_frequencies(expt1_complete_goals,3,1000)\"") - -(defvar ml4pg-my-buffer "") - -(defun ml4pg-my-config-display () - (delete-other-windows) - (switch-to-buffer-other-window "*display*") - (erase-buffer) - (other-window -1)) - -;; This function is in charge of processing the output produced by Matlab -;; The variable signal is used to indicate the function which has called to matlab and to process the result - -(defvar ml4pg-signal 0) - -(defun ml4pg-my-output-filter (output) - (setq ml4pg-my-buffer (concat ml4pg-my-buffer output)) - (when (and output (get-buffer "*display*")) - (with-current-buffer "*display*" - (progn (erase-buffer) - (cond ((equal ml4pg-signal 0) nil) - ;((equal signal 1) (print-similarities (search-cluster (split-clusters-aux (remove-jumps my-buffer) nil) (1+(length saved-theorems))))) - ;((equal signal 2) (print-clusters (split-clusters-aux (remove-jumps my-buffer) nil) (split-frequencies my-buffer nil))) - ((equal ml4pg-signal 1) (ml4pg-print-similarities (ml4pg-split-clusters-aux2 ml4pg-my-buffer nil))) - ;((equal signal 2) (print-clusters (split-clusters-aux my-buffer nil) (split-frequencies my-buffer nil))) - ((equal ml4pg-signal 4) (ml4pg-print-clusters-bis (ml4pg-split-clusters-aux ml4pg-my-buffer nil) (ml4pg-split-frequencies ml4pg-my-buffer nil))) - ((equal ml4pg-signal 3) (ml4pg-compute-clusters-and-values (ml4pg-split-clusters-aux (ml4pg-remove-jumps (subseq ml4pg-my-buffer (search "load" ml4pg-my-buffer :from-end t))) nil) - (ml4pg-split-frequencies (ml4pg-remove-jumps (subseq ml4pg-my-buffer (search "load" ml4pg-my-buffer :from-end t))) nil))) - (t nil))))) - output) - -(add-hook 'comint-preoutput-filter-functions 'ml4pg-my-output-filter) - -;(defun ml4pg-split-clusters-aux (str res) - ;(let ((init (search "'" str))) - ;(if init -; (let ((end (search "'" str :start2 (1+ init)))) -; (split-clusters-aux (subseq str (1+ end)) -; (cons (cluster-string-to-list (subseq str (1+ init) end)) res))) - ; res))) - -;(defun ml4pg-split-frequencies (str res) - ;(let ((init (search "[" str))) - ;(if init -; (let ((end (search "]" str :start2 (1+ init)))) -; (if (not (search "char" (subseq str init end))) -; (split-frequencies (subseq str (1+ end)) -; (cons (string-to-number (subseq str (1+ init) end)) res)) -; (split-frequencies (subseq str (1+ (search "[" str :start2 (1+ end)))) res) -; )) - ; res))) - - -(defun ml4pg-split-clusters-aux2 (str res) - (let ((init (search "ans =" str))) - (if init - (list (ml4pg-cluster-string-to-list (ml4pg-remove-jumps (subseq str (+ 5 init) (search ">>" str :from-end t))))) - nil))) - -(defun ml4pg-split-clusters-aux (str res) - (let ((init (search "ans =" str))) - (if init - (let ((end (search "[" str :start2 (1+ init)))) - (ml4pg-split-clusters-aux (subseq str (1+ end)) - (cons (ml4pg-cluster-string-to-list (ml4pg-remove-jumps (subseq str (+ 5 init) end))) res))) - res))) - - -(defun ml4pg-split-frequencies (str res) -(let ((init (search "[" str))) - (if init - (let ((end (search "]" str :start2 (1+ init)))) - (if (not (search "char" (subseq str init end))) - (ml4pg-split-frequencies (subseq str (1+ end)) - (cons (string-to-number (ml4pg-remove-jumps (subseq str (1+ init) end))) res)) - (ml4pg-split-frequencies (subseq str (1+ (search "[" str :start2 (1+ end)))) res) - )) - res))) - - - - -(defun ml4pg-search-cluster (res n) - (do ((temp res (cdr temp)) - (temp2 nil)) - ((endp temp) temp2) - (if (member (format "%s" n) (car temp)) - (append temp2 (list (car temp)))))) - - - -(defun ml4pg-cluster-string-to-list (cluster) - (do ((temp cluster) - (temp2 nil)) - ((not (search "," temp)) (append temp2 (list temp))) - (progn (setf temp2 (append temp2 (list (subseq temp 0 (search "," temp))))) - (setf temp (subseq temp (1+ (search "," temp))))))) - - - - - -(defun ml4pg-remove-occurrence (list n) - (do ((temp list (cdr temp)) - (temp2 nil)) - ((endp temp) temp2) - (if (not (equal (format "%s" n) (car temp))) - (setf temp2 (append temp2 (list (car temp))))))) - - -(defvar ml4pg-granularity-level-temp 1) - -(defun ml4pg-print-similarities (res) - (interactive) - (cond ((not (caar res)) (insert (format "Searching similarities...\n"))) - ((search "None" (caar res)) - (if (not ml4pg-iterative) - (insert (format "Sorry, but we have not found any similarity using granularity %s\n" ml4pg-granularity-level)) - (if (eq ml4pg-granularity-level-temp 5) - (format "Sorry, but we have not found any similarity at any ganularity level\n") - (progn (setf ml4pg-granularity-level-temp (1+ ml4pg-granularity-level-temp)) - (ml4pg-show-clusters-of-theorem-iterative))))) - (t (progn (insert (format "Similarities:\n")) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (insert (format "This lemma is similar to the lemmas:\n")) - (do ((temp2 (ml4pg-remove-occurrence (car res) (1+ (length ml4pg-saved-theorems))) (cdr temp2))) - ((endp temp2) ) - (if (<= (string-to-number (car temp2)) (length ml4pg-saved-theorems)) - (progn (insert (format "- ")) - (ml4pg-insert-button-lemma (ml4pg-remove_last_colon(car (nth (- (string-to-number (car temp2)) 1) ml4pg-saved-theorems))))) - (progn (shell-command (concat "cat "(expand-file-name "names_temp.txt") " | sed -n '" - (format "%s" (- (string-to-number (car temp2)) (length ml4pg-saved-theorems))) - "p'")) - (with-current-buffer "*Shell Command Output*" - (beginning-of-buffer) - (read (current-buffer)) - (setf temp-res (ml4pg-remove_last_colon (format "%s" (read (current-buffer)))))) - (insert (format "- ")) - (ml4pg-insert-button-lemma temp-res))))) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (if ml4pg-iterative (insert (format "Similarities found using granularity level %s\n" ml4pg-granularity-level-temp))) - ))) - - - - -(defun ml4pg-print-similarities-matlab () - (with-current-buffer "*display*" - (while (string= "0" (car (read-lines (expand-file-name "available.txt")))) - - (progn (erase-buffer) - (insert (format "Searching clusters...\n")) - (sleep-for 1)) - ) - (erase-buffer) - (let* ((clu (car (ml4pg-read-lines (expand-file-name "matlab_res.txt"))))) - (cond - ((search "None" clu) - (if (not ml4pg-iterative) - (insert (format "Sorry, but we have not found any similarity using granularity %s\n" ml4pg-granularity-level)) - (if (eq ml4pg-granularity-level-temp 5) - (format "Sorry, but we have not found any similarity at any ganularity level\n") - (progn (setf ml4pg-granularity-level-temp (1+ ml4pg-granularity-level-temp)) - (ml4pg-show-clusters-of-theorem-iterative))))) - (t (progn (insert (format "Similarities:\n")) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (insert (format "This lemma is similar to the lemmas:\n ")) - (do ((temp2 (ml4pg-remove-occurrence (ml4pg-cluster-string-to-list clu) (1+ (length ml4pg-saved-theorems))) (cdr temp2))) - ((endp temp2) ) - (if (<= (string-to-number (car temp2)) (length ml4pg-saved-theorems)) - (progn (insert (format "- ")) - (ml4pg-insert-button-lemma (ml4pg-remove_last_colon(car (nth (- (string-to-number (car temp2)) 1) ml4pg-saved-theorems))))) - (progn (shell-command (concat "cat "(expand-file-name "names_temp.txt") " | sed -n '" - (format "%s" (- (string-to-number (car temp2)) (length ml4pg-saved-theorems))) - "p'")) - (with-current-buffer "*Shell Command Output*" - (beginning-of-buffer) - (read (current-buffer)) - (setf temp-res (ml4pg-remove_last_colon (format "%s" (read (current-buffer)))))) - (insert (format "- ")) - (ml4pg-insert-button-lemma temp-res))))) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (if ml4pg-iterative (insert (format "Similarities found using granularity level %s\n" ml4pg-granularity-level-temp))) - )) -))) - - - - - -(defun ml4pg-print-similarities-weka (n) - (let ((clusters (ml4pg-extract-clusters-from-file n))) - (with-current-buffer "*display*" - (erase-buffer) - (insert (format "Similarities:\n")) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (insert (format "This lemma is similar to the lemmas:\n ")) - (do ((temp2 (ml4pg-remove-occurrence (ml4pg-clusters-of-n clusters (nth (1- (length ml4pg-saved-theorems)) clusters)) (1+ (length ml4pg-saved-theorems))) (cdr temp2))) - ((endp temp2) ) - (if (<= (car temp2) (length ml4pg-saved-theorems)) - (progn (insert (format "- ")) - (ml4pg-insert-button-lemma (ml4pg-remove_last_colon(car (nth (- (car temp2) 1) ml4pg-saved-theorems))))) - (progn (shell-command (concat "cat "(expand-file-name "names_temp.txt") " | sed -n '" - (format "%s" (- (car temp2) (length ml4pg-saved-theorems))) - "p'")) - (with-current-buffer "*Shell Command Output*" - (beginning-of-buffer) - (read (current-buffer)) - (setf temp-res (ml4pg-remove_last_colon (format "%s" (read (current-buffer)))))) - (insert (format "- ")) - (ml4pg-insert-button-lemma temp-res)))) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - ) - )) - - - -(defun ml4pg-insert-button-lemma (lemma) - (progn (insert-button lemma 'action (ml4pg-insert-button-lemma-macro lemma) - 'face (list 'link) - 'follow-link t) - (insert (format "\n")))) - - - -(defun ml4pg-insert-button-lemma-macro (test) - (list 'lambda '(x) - (list 'progn - (list 'proof-shell-invisible-cmd-get-result (list 'format '"Unset Printing All.")) - (list 'if (list 'get-buffer '"*display2*") (list 'with-current-buffer '"*display2*" (list 'delete-window))) - (list 'with-current-buffer '"*display*" (list 'split-window-vertically)) - (list 'switch-to-buffer-other-window '"*display2*") - (list 'with-current-buffer '"*display2*" (list 'erase-buffer)) - (list 'with-current-buffer '"*display2*" - (list 'insert (list 'proof-shell-invisible-cmd-get-result - (list 'format '"Print %s." test)))) - ))) - - - - - - -(defvar ml4pg-times 0) - -(defun ml4pg-print-clusters (res freq) - (interactive) - (setf times (1+ times)) - (if (not (caar res)) - (insert (format "Searching clusters...\n")) - (let* ((temp0 (ml4pg-unzip (ml4pg-quicksort-pair (ml4pg-zip res freq)))) - (res1 (car temp0)) - (freq1 (cadr temp0))) - (insert (format "We have found the following clusters:\n" )) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (do ((temp res1 (cdr temp)) - (temp-freq freq1 (cdr temp-freq)) - (i 1 (1+ i))) - ((endp temp) (insert (format "------------------------------------------------------------------------------------------------------------\n")) ) - (progn (insert (format "Cluster %s with frequency %s%%\n" i (car temp-freq))) - (do ((temp2 (car temp) (cdr temp2))) - ((endp temp2) (insert (format "\n"))) - (progn (insert (format "Lemma ")) - (ml4pg-insert-button-lemma - (ml4pg-remove_last_colon - (car (nth (string-to-number (car temp2)) ml4pg-saved-theorems))))))))))) - - -(defun ml4pg-print-clusters-bis (res freq) - (interactive) - (setf times (1+ times)) - (if (not (caar res)) - (insert (format "Searching clusters...\n")) - (let* ((temp0 (ml4pg-unzip (ml4pg-quicksort-pair (ml4pg-zip res freq)))) - (res1 (car temp0)) - (freq1 (cadr temp0))) - (insert (format "We have found the following clusters:\n" )) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (do ((temp res1 (cdr temp)) - (temp-freq freq1 (cdr temp-freq)) - (i 1 (1+ i))) - ((endp temp) (insert (format "------------------------------------------------------------------------------------------------------------\n")) ) - (progn (insert (format "Cluster %s with frequency %s%%\n" i (car temp-freq))) - (do ((temp2 (car temp) (cdr temp2))) - ((endp temp2) (insert (format "\n"))) - (if (< (string-to-number (car temp2)) (length ml4pg-saved-theorems)) - (progn (insert (format "Lemma ")) - (ml4pg-insert-button-lemma (ml4pg-remove_last_colon - (car (nth (string-to-number (car temp2)) ml4pg-saved-theorems))))) - (progn (shell-command (concat "cat "(expand-file-name "names_temp.txt") " | sed -n '" - (format "%s" (- (string-to-number (car temp2)) (length ml4pg-saved-theorems))) - "p'")) - (with-current-buffer "*Shell Command Output*" - (beginning-of-buffer) - (read (current-buffer)) - (setf temp-res (format "%s" (read (current-buffer))))) - (insert (format "Lemma " )) - (ml4pg-insert-button-lemma temp-res)) - ))))))) - - -(defun ml4pg-extract_clusters_freq (list) - (do ((temp list (cdr temp)) - (clusters nil) - (freq nil)) - ((endp temp) (list clusters freq)) - (if (not (string= (subseq (car temp) 0 1) "[")) - (setf clusters (append clusters (list (car temp)))) - (setf freq (append freq (list (string-to-number (subseq (car temp) 1 (search "]" (car temp)))))))))) - - - - - - - - - - - -(defun ml4pg-print-clusters-weka (gra) - (let* ((clusters (ml4pg-extract-clusters-from-file gra)) - (res1 (ml4pg-remove-alone (cdr (ml4pg-form-clusters clusters gra))))) - (with-current-buffer "*display*" - (erase-buffer) - (insert (format "We have found the following clusters:\n" )) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - - (do ((temp res1 (cdr temp)) - (i 1 (1+ i))) - ((endp temp) (insert (format "------------------------------------------------------------------------------------------------------------\n")) ) - (progn (insert (format "Cluster %s\n" i )) - (do ((temp2 (car temp) (cdr temp2))) - ((endp temp2) (insert (format "\n"))) - (if (< (car temp2) (length ml4pg-saved-theorems)) - (progn (insert (format "Lemma ")) - (ml4pg-insert-button-lemma (ml4pg-remove_last_colon - (car (nth (car temp2) ml4pg-saved-theorems))))) - (progn (shell-command (concat "cat "(expand-file-name "names_temp.txt") " | sed -n '" - (format "%s" (- (car temp2) (length ml4pg-saved-theorems))) - "p'")) - (with-current-buffer "*Shell Command Output*" - (beginning-of-buffer) - (read (current-buffer)) - (setf temp-res (format "%s" (read (current-buffer))))) - (insert (format "Lemma " )) - (if (not (search "home" temp-res) )(ml4pg-insert-button-lemma temp-res))) - )))) - - - ))) - - - - - - - -(defun ml4pg-remove_last_colon (str) - (if (string= (subseq str (1- (length str))) ":") - (subseq str 0 (1- (length str))) - str)) - - -;; This functions shows the cluster of a theorem - - -(defun ml4pg-show-clusters-of-theorem-iterative () - (interactive) - (let* ((alg (cond ((string= "g" ml4pg-algorithm) "find_cluster_with_gaussian") (t "find_cluster_with_kmeans"))) - (gra (if (not ml4pg-iterative) - (cond ((eq 2 ml4pg-granularity-level) 5) - ((eq 3 ml4pg-granularity-level) 10) - ((eq 4 ml4pg-granularity-level) 15) - ((eq 5 ml4pg-granularity-level) 20) - (t 3)) - (cond ((eq 2 ml4pg-granularity-level-temp) 5) - ((eq 3 ml4pg-granularity-level-temp) 10) - ((eq 4 ml4pg-granularity-level-temp) 15) - ((eq 5 ml4pg-granularity-level-temp) 20) - (t 3))))) - (progn (setf ml4pg-signal 1) - (shell-command (concat "echo 0 > " (expand-file-name "available.txt"))) - (require 'comint) - (comint-send-string (get-buffer-process "*matlab*") - (concat "load " (expand-file-name "temp.csv") - (format "; %s(temp,%s,%s,'%s'); csvwrite('%s',1)\n" alg gra (1+ (length ml4pg-saved-theorems)) - (expand-file-name "matlab_res.txt") (expand-file-name "available.txt")))) - (ml4pg-print-similarities-matlab) - ))) - -(defun ml4pg-show-clusters-of-theorem () - (interactive) - (let* ((alg (cond ((string= "g" ml4pg-algorithm) "find_cluster_with_gaussian") (t "find_cluster_with_kmeans"))) - (gra (if (not ml4pg-iterative) - (cond ((eq 2 ml4pg-granularity-level) 8) - ((eq 3 ml4pg-granularity-level) 15) - ((eq 4 ml4pg-granularity-level) 25) - ((eq 5 ml4pg-granularity-level) 50) - (t 5)) - (cond ((eq 2 ml4pg-granularity-level-temp) 8) - ((eq 3 ml4pg-granularity-level-temp) 15) - ((eq 4 ml4pg-granularity-level-temp) 25) - ((eq 5 ml4pg-granularity-level-temp) 50) - (t 5))))) - (progn - (setq ml4pg-my-buffer "") - (setf res (ml4pg-extract-info-up-to-here)) - (with-temp-file (expand-file-name "temp.csv") (cond ((string= ml4pg-level "g") (insert (ml4pg-extract-features-1-bis res))) - ((string= ml4pg-level "t") (insert (ml4pg-extract-features-2-bis tactic-temp tactic-level))) - ((string= ml4pg-level "p") (insert (ml4pg-extract-features-2-bis proof-tree-temp proof-tree-level))))) - (if ml4pg-libs-menus - (progn (ml4pg-add-libraries-temp) - (ml4pg-add-names))) - (switch-to-buffer-other-window "*display*") - (cond ((string= ml4pg-ml-system "m") - (progn (setf ml4pg-signal 1) - (shell-command (concat "echo 0 > " (expand-file-name "available.txt"))) - (require 'comint) - (comint-send-string (get-buffer-process "*matlab*") - (concat "load " (expand-file-name "temp.csv") - (format "; %s(temp,%s,%s,'%s'); csvwrite('%s',1)\n" alg gra (1+ (length ml4pg-saved-theorems)) - (expand-file-name "matlab_res.txt") (expand-file-name "available.txt")))) - (ml4pg-print-similarities-matlab) - )) - - ((string= ml4pg-ml-system "w") - (progn (setf ml4pg-signal 5) - (ml4pg-weka gra) - (sleep-for 1) - (ml4pg-print-similarities-weka gra)) - ) - ))) - (proof-shell-invisible-cmd-get-result (format "Unset Printing All"))) - -;; The following function shows all the clusters which have been obtained from all the theorems exported up to now - -(defun ml4pg-show-clusters () - (interactive) - (let* ((alg (cond ((string= "g" ml4pg-algorithm) "gaussian_clusters") (t "kmeans_clusters_and_frequencies"))) - (gra (cond ((eq 2 ml4pg-granularity-level) 5) - ((eq 3 ml4pg-granularity-level) 10) - ((eq 4 ml4pg-granularity-level) 15) - ((eq 5 ml4pg-granularity-level) 20) - (t 3))) - (freq (cond ((eq 2 ml4pg-frequency-precision) 500) - ((eq 3 ml4pg-frequency-precision) 1000) - (t 100)))) - - (progn - (setf ml4pg-signal 2) - (setf ml4pg-my-buffer "") - (progn (with-temp-file (expand-file-name "temp1.csv") (insert (ml4pg-extract-features-1))) - (switch-to-buffer-other-window "*display*") - (require 'comint) - (comint-send-string (get-buffer-process "*matlab*") - (concat "load " (expand-file-name "temp1.csv") (format "; %s(temp1,%s,%s)\n" alg gra freq)))) - ))) - - - -(defun ml4pg-show-clusters-bis () - (interactive) - (let* ((alg (cond ((string= "g" ml4pg-algorithm) "gaussian_clusters") (t "kmeans_clusters_and_frequencies"))) - (gra (cond ((eq 2 ml4pg-granularity-level) 5) - ((eq 3 ml4pg-granularity-level) 10) - ((eq 4 ml4pg-granularity-level) 15) - ((eq 5 ml4pg-granularity-level) 20) - (t 3))) - (freq (cond ((eq 2 ml4pg-frequency-precision) 500) - ((eq 3 ml4pg-frequency-precision) 1000) - (t 100)))) - - (progn - (setf ml4pg-signal 4) - (setf ml4pg-my-buffer "") - (if ml4pg-libs-menus - (progn (with-temp-file (expand-file-name "temp.csv") (cond ((string= ml4pg-level "g") (insert (ml4pg-extract-features-1))) - ((string= ml4pg-level "t") (insert (ml4pg-extract-features-2 tactic-level))) - ((string= ml4pg-level "p") (insert (ml4pg-extract-features-2 proof-tree-level))))) - (ml4pg-add-libraries-temp) - (ml4pg-add-names)) - (with-temp-file (expand-file-name "temp.csv") (insert (ml4pg-extract-features-1)))) - (switch-to-buffer-other-window "*display*") - (cond ((string= ml4pg-ml-system "m") - (progn - (shell-command (concat "echo 0 > " (expand-file-name "available.txt"))) - (require 'comint) - (comint-send-string (get-buffer-process "*matlab*") - (concat "load " (expand-file-name "temp.csv") (format "; %s(temp,%s,%s,'%s'); csvwrite('%s',1)\n" alg gra freq - (expand-file-name "matlab_res.txt") (expand-file-name "available.txt")))) - (ml4pg-print-clusters-matlab))) - ((string= ml4pg-ml-system "w") - (progn (setf ml4pg-signal 5) - (ml4pg-weka gra) - (sleep-for 1) - (ml4pg-print-clusters-weka gra)) - ) - - ))) - (proof-shell-invisible-cmd-get-result (format "Unset Printing All")) -) - - - - -(defun ml4pg-add-libraries () - (do ((temp ml4pg-libs-menus (cdr temp))) - ((endp temp) nil) - (cond ((string= ml4pg-level "g") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) ".csv >> " (expand-file-name "temp1.csv")))) - ((string= ml4pg-level "t") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) "_tactics.csv >> " (expand-file-name "temp1.csv")))) - ((string= ml4pg-level "p") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) "_tree.csv >> " (expand-file-name "temp1.csv"))))))) - -(defun ml4pg-add-libraries-temp () - (do ((temp ml4pg-libs-menus (cdr temp))) - ((endp temp) nil) - (cond ((string= ml4pg-level "g") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) ".csv >> " (expand-file-name "temp.csv")))) - ((string= ml4pg-level "t") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) "_tactics.csv >> " (expand-file-name "temp.csv")))) - ((string= ml4pg-level "p") (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) "_tree.csv >> " (expand-file-name "temp.csv"))))))) - -(defun ml4pg-add-names () - (shell-command (concat "rm " (expand-file-name "names_temp.txt"))) - (shell-command (concat "touch " (expand-file-name "names_temp.txt"))) - (do ((temp ml4pg-libs-menus (cdr temp))) - ((endp temp) nil) - (shell-command (concat "cat " ml4pg-home-dir "libs/coq/" (car temp) "_names >> " (expand-file-name "names_temp.txt"))))) - - - - - - - -(defvar ml4pg-names-values nil) - -(defun ml4pg-print-clusters2 (res freq) - (interactive) - (let* ((temp0 (ml4pg-unzip (ml4pg-quicksort-pair (ml4pg-zip res freq)))) - (res1 (car temp0)) - (freq1 (cadr temp0))) - (insert (format "We have found the following clusters:\n")) - (insert (format "------------------------------------------------------------------------------------------------------------\n")) - (do ((temp res1 (cdr temp)) - (temp-freq freq1 (cdr temp-freq)) - (i 1 (1+ i))) - ((endp temp) (insert (format "------------------------------------------------------------------------------------------------------------\n"))) - (progn (insert (format "Cluster %s with frequency %s%%\n" i (car temp-freq))) - (do ((temp2 (car temp) (cdr temp2))) - ((endp temp2) (insert (format "\n"))) - (insert (format "Lemma %s\n" - (ml4pg-remove_last_colon - (car (nth (- (string-to-number (car temp2)) 1) ml4pg-saved-theorems2)))))))))) - - -(defun ml4pg-compute-clusters-and-values (list fr) - (if (not (ml4pg-left-strings ml4pg-saved-theorems2)) - (ml4pg-print-clusters2 list fr) - (progn (setf ml4pg-names-values (ml4pg-extract-names-dynamic)) - (do ((temp list (cdr temp)) - (n 200 (+ n 5))) - ((endp temp) (progn (setf ml4pg-names-values (ml4pg-complete-names-values ml4pg-names-values n)) - (setf ml4pg-saved-theorems2 (ml4pg-recompute-saved-theorems ml4pg-saved-theorems2)) - (setf ml4pg-my-buffer "") - (ml4pg-show-clusters-dynamic-b) - ) -nil -) - (ml4pg-assign-values (car temp) n)) - ))) - -(defvar ml4pg-granularity-dynamic 0) - -(defun ml4pg-show-clusters-dynamic () - (interactive) - (setf ml4pg-granularity-dynamic (read-string "Introduce the granularity level (values from 1 to 5): ")) - (progn - (setf ml4pg-signal 3) - (setf ml4pg-my-buffer "") - (with-temp-file (expand-file-name "temp.csv") (insert (ml4pg-extract-features-dynamic))) - (switch-to-buffer-other-window "*display*") - (require 'comint) - (cond ((string= "1" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,3,100)\n"))) - ((string= "2" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,5,100)\n"))) - ((string= "3" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,10,100)\n"))) - ((string= "4" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,15,100)\n"))) - ((string= "5" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,20,100)\n"))) - (t (ml4pg-show-clusters-dynamic))) - - )) - -(defun ml4pg-show-clusters-dynamic-b () - (interactive) - (progn - (setf ml4pg-signal 3) - (setf ml4pg-my-buffer "") - (with-temp-file (expand-file-name "temp.csv") (insert (ml4pg-extract-features-dynamic))) - (require 'comint) - (cond ((string= "1" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,3,100)\n"))) - ((string= "2" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,5,100)\n"))) - ((string= "3" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,10,100)\n"))) - ((string= "4" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,15,100)\n"))) - ((string= "5" ml4pg-granularity-dynamic) - (comint-send-string (get-buffer-process "*matlab*") (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp,20,100)\n"))) - (t (ml4pg-show-clusters-dynamic))) - ;(comint-send-string (get-buffer-process "*matlab*") -; (concat "load " (expand-file-name "temp.csv") "; kmeans_clusters_and_frequencies(temp," -; (format "%s" (floor (length (extract-list-without-strings saved-theorems2)) 5) ) ",100)\n")) - ))
\ No newline at end of file |