aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ML4PG/ssreflect/feature_extraction_2.el
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ML4PG/ssreflect/feature_extraction_2.el')
-rw-r--r--contrib/ML4PG/ssreflect/feature_extraction_2.el1282
1 files changed, 0 insertions, 1282 deletions
diff --git a/contrib/ML4PG/ssreflect/feature_extraction_2.el b/contrib/ML4PG/ssreflect/feature_extraction_2.el
deleted file mode 100644
index 36cc53b2..00000000
--- a/contrib/ML4PG/ssreflect/feature_extraction_2.el
+++ /dev/null
@@ -1,1282 +0,0 @@
-;;; This is the feature vector extraction file for SSReflect
-
-;; Different variables which are used to store information about
-;; the numbers associated with tactics, rewrite rules, types, ...
-
-(defvar ml4pg-hypothesis nil)
-
-(defvar ml4pg-saved-theorems nil)
-(defvar ml4pg-goal-level-temp nil)
-(defvar ml4pg-tactic-level nil)
-(defvar ml4pg-proof-tree-level nil)
-
-;; Variables to store the different values associated with the tactics, the
-;; types or the rewrite rules
-
-(defvar ml4pg-tactic_id '(("move" . 1)
- ("case" . 2)
- ("elim" . 3)
- ("apply" . 4)
- ("apply/" . 5)
- ("move/" . -5)
- ("case/" . 6)
- ("rewrite" . 7)
- ("exists" . 8)
- ("[]" . 0)
- ("exact" . 9)))
-
-
-(defvar ml4pg-move nil)
-(defvar ml4pg-case nil)
-(defvar ml4pg-elim nil)
-(defvar ml4pg-apply nil)
-(defvar ml4pg-apply/ nil)
-(defvar ml4pg-move/ nil)
-(defvar ml4pg-case/ nil)
-(defvar ml4pg-rewrite nil)
-(defvar ml4pg-exists nil)
-(defvar ml4pg-done nil)
-(defvar ml4pg-exact nil)
-
-
-(defvar ml4pg-types_id '(("nat" . -2)
- ("Prop" . -4)
- ("bool" . -3)
- ("T" . -1)
- ("seq" . -5)))
-
-(defvar ml4pg-types_id_n -6)
-(defvar ml4pg-views_id nil)
-(defvar ml4pg-theorems_id nil)
-
-(defvar ml4pg-top-symbol-id
- '(("forall" . 5)
- ("@eq" . 6)
- ("and" . 4)
- ("iff" . 8)
- ("or" . 3)
- ("is_true" . 2)
- ("reflect" . 9)
- ))
-
-(defvar ml4pg-top-symbol-n 10)
-
-
-(defvar ml4pg-add_to 0.1)
-(defvar ml4pg-start 100)
-
-(defvar ml4pg-start_view 101)
-(defvar ml4pg-start_thm 101)
-
-
-(defvar ml4pg-init 0)
-
-(defvar ml4pg-current-level 1)
-(defvar ml4pg-dot-level nil)
-
-;;; Proof tree levels
-
-(defvar ml4pg-tdl1 nil)
-(defvar ml4pg-tdl2 nil)
-(defvar ml4pg-tdl3 nil)
-(defvar ml4pg-tdl4 nil)
-(defvar ml4pg-tdl5 nil)
-
-(defun ml4pg-add-info-to-level-aux (info list)
- (if (not list)
- info
- (do ((temp list (cdr temp))
- (temp1 info (cdr temp1))
- (temp2 nil))
- ((endp temp) temp2)
- (cond ((= (car temp) 0) (setf temp2 (append temp2 (list (car temp1)))))
- ((= (car temp1) 0) (setf temp2 (append temp2 (list (car temp)))))
- (t (setf temp2 (append temp2 (list (string-to-number (format "%s%s" (car temp) (car temp1)))))))))))
-
-(defun ml4pg-add-info-to-level (info level)
- (cond ((= level 1) (setf ml4pg-tdl1 (ml4pg-add-info-to-level-aux info ml4pg-tdl1)))
- ((= level 2) (setf ml4pg-tdl2 (ml4pg-add-info-to-level-aux info ml4pg-tdl2)))
- ((= level 3) (setf ml4pg-tdl3 (ml4pg-add-info-to-level-aux info ml4pg-tdl3)))
- ((= level 4) (setf ml4pg-tdl4 (ml4pg-add-info-to-level-aux info ml4pg-tdl4)))
- ((= level 5) (setf ml4pg-tdl5 (ml4pg-add-info-to-level-aux info ml4pg-tdl5)))
- (t nil)
- ))
-
-;;; Main function of this file, it is in charge of extracting the
-;;; information associated with a theorem
-
-
-(defun ml4pg-export-theorem ()
- (interactive)
- (progn (setf ml4pg-tdl1 nil
- ml4pg-tdl2 nil
- ml4pg-tdl3 nil
- ml4pg-tdl4 nil
- ml4pg-tdl5 nil
- ml4pg-move nil
- ml4pg-case nil
- ml4pg-elim nil
- ml4pg-apply nil
- ml4pg-apply/ nil
- ml4pg-move/ nil
- ml4pg-case/ nil
- ml4pg-rewrite nil
- ml4pg-exists nil
- ml4pg-done nil
- ml4pg-exact nil
- ml4pg-current-level 1
- ml4pg-dot-level nil
- ml4pg-hypothesis nil
- ml4pg-goal-level nil)
- (if (equal ml4pg-init 0)
- (progn (ml4pg-read-lemmas)
- (ml4pg-read-views)
- (setq ml4pg-init 1)))
- (ml4pg-export-theorem-aux nil nil)
- (proof-shell-invisible-cmd-get-result (format "Unset Printing All"))
- ))
-
-
-
-;; A function to obtain the type associated with an object
-
-(defun ml4pg-remove-jumps-aux (string res)
- (let ((jump (search "
-" string)))
- (if jump
- (ml4pg-remove-jumps-aux (subseq string (1+ jump)) (concatenate 'string res (subseq string 0 jump)))
- (concatenate 'string res string))))
-
-(defun ml4pg-remove-jumps (string)
- (ml4pg-remove-jumps-aux string ""))
-
-
-(defun ml4pg-get-type-id (object)
- (if (string= "(" (subseq object 0 1))
- -4
- (let* ((a (ml4pg-remove-jumps (proof-shell-invisible-cmd-get-result (concat "Check " object))))
- (pos_jump (search "
-" a :start2 (+ 2 (search " " a))))
- (pos_space (search " " a :start2 (+ 2 (search ": " a))))
- (type (if pos_space
- (cdr (assoc (subseq a (+ 2 (search ": " a)) pos_space) ml4pg-types_id))
- (cdr (assoc (subseq a (+ 2 (search ": " a)) pos_jump) ml4pg-types_id)))))
- (if type type
- (progn (setf ml4pg-types_id
- (append ml4pg-types_id (list (cons (if pos_space
- (subseq a (+ 2 (search ": " a)) pos_space)
- (subseq a (+ 2 (search ": " a)) pos_jump))
- ml4pg-types_id_n))))
-
- (setf ml4pg-types_id_n (1- ml4pg-types_id_n))
- (1+ ml4pg-types_id_n))
- ))))
-
-(defun ml4pg-get-type-id2 (object)
- (let* ((a (proof-shell-invisible-cmd-get-result (concat "Check " object)))
- (pos_jump (search "
-" a :start2 (+ 2 (search " " a))))
- (pos_space (search " " a :start2 (+ 2 (search ": " a))))
- (type (if pos_space
- (cdr (assoc (subseq a (+ 2 (search ": " a)) pos_space) ml4pg-types_id))
- (cdr (assoc (subseq a (+ 2 (search ": " a)) pos_jump) ml4pg-types_id)))))
- (if type type
- (progn (setf ml4pg-types_id
- (append ml4pg-types_id (list (cons (if pos_space
- (subseq a (+ 2 (search ": " a)) pos_space)
- (subseq a (+ 2 (search ": " a)) pos_jump))
- ml4pg-types_id_n))))
-
- (setf ml4pg-types_id_n (1- ml4pg-types_id_n))
- (1+ ml4pg-types_id_n))
- )))
-
-
-;; A function to obtain the value of a top symbol
-
-(defun ml4pg-get-top-symbol ()
- (proof-shell-invisible-cmd-get-result (format "Set Printing All"))
- (let* ((res (proof-shell-invisible-cmd-get-result (format "Focus")))
- (res2 (subseq res (+ 32 (search "============================" res))))
- (fst-symbol (subseq res2 0 (search " " res2))))
- (cond ((search "->" res2) 7)
- (t (let ((is (assoc fst-symbol ml4pg-top-symbol-id)))
- (if is
- (cdr is)
- (progn (setf ml4pg-top-symbol-id
- (append ml4pg-top-symbol-id (list (cons fst-symbol ml4pg-top-symbol-n))))
-
- (setf ml4pg-top-symbol-n (1+ ml4pg-top-symbol-n))
- (1- ml4pg-top-symbol-n))))))))
-
-
-
-
-;; In some cases the intro tactic does not have parameters, the following function
-;; obtain the type of the object introduced with the intro tactic in those cases
-;; Sobra
-(defun ml4pg-get-obj-intro ()
- (let* ((undo (proof-undo-last-successful-command))
- (obj (proof-shell-invisible-cmd-get-result (format "Show Intro")))
- (object (subseq obj 0 (search "
-" obj)))
- (dod (proof-assert-next-command-interactive))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis (list object)))))
-
- (ml4pg-get-type-id object)
- ))
-
-(defun ml4pg-extract-params (seq res)
- (let ((pos_space (search " " seq))
- (pos_jump (search "
-" seq)))
- (if pos_space
- (ml4pg-extract-params (subseq seq (+ 1 pos_space)) (cons (subseq seq 0 pos_space) res))
- (reverse (cons (subseq seq 0 pos_jump) res)))))
-
-(defun ml4pg-extract-params2 (seq res)
- (let ((pos_space (search " " seq))
- (pos_jump (search "." seq)))
- (if pos_space
- (ml4pg-extract-params2 (subseq seq (+ 1 pos_space)) (cons (subseq seq 0 pos_space) res))
- (reverse (cons (subseq seq 0 pos_jump) res)))))
-
-;; Given a list of objects, it obtains the value associated with their types
-
-(defun ml4pg-get-types-list (list res)
- (if (endp list)
- (* -1 res)
- (if (search "_" (car list))
- (ml4pg-get-types-list (cdr list) res)
- (ml4pg-get-types-list (cdr list) (+ (* -1 (ml4pg-get-type-id (car list)) (expt 10 (- (length list) 1))) res)))))
-
-
-(defun ml4pg-get-types-list-exists (list res)
- (if (endp list)
- (* -1 res)
- (ml4pg-get-types-list-exists (cdr list) (+ (* -1 (ml4pg-get-type-id2 (car list)) (expt 10 (- (length list) 1))) res))))
-
-;; To obtain the number of tactics applied
-
-(defun ml4pg-get-number-list (list)
- (if (endp list)
- 0
- (+ (expt 10 (- (length list) 1)) (ml4pg-get-number-list (cdr list)))))
-
-(defun ml4pg-get-number-list2 (list n)
- (if (endp list)
- 0
- (+ (* n (expt 10 (- (length list) 1))) (ml4pg-get-number-list2 (cdr list) n))))
-
-;; To obtain the value associated with top symbol in the case of move
-
-(defun ml4pg-get-top-symbols-list (len res)
- (if (= len 0)
- res
- (let ((gs (ml4pg-get-top-symbol))
- (ps (proof-shell-invisible-cmd-get-result (format "intro"))))
- (+ (ml4pg-get-top-symbols-list (- len 1) (+ (* gs (expt 10 (- len 1))) res))))))
-
-(defun ml4pg-get-top-symbols-seq (seq res)
- (if (endp seq)
- res
- (let ((gs (ml4pg-get-top-symbol))
- (ps (proof-shell-invisible-cmd-get-result (format (concat "intro " (car seq))))))
- (+ (ml4pg-get-top-symbols-seq (cdr seq) (+ (* gs (expt 10 (- (length seq) 1))) res))))))
-
-;; To obtain the value associated with a theorem
-
-(defun ml4pg-search-in-hyp (obj hyp)
- (if (endp hyp)
- nil
- (if (string= obj (car hyp))
- t
- (ml4pg-search-in-hyp obj (cdr hyp)))))
-
-;;; Auxiliary functions
-
-(defun ml4pg-remove=> (string)
- (let ((d (search "=>" string)))
- (if d
- (ml4pg-remove=> (concatenate 'string (subseq string 0 d) (subseq string (+ 2 d))))
- string)))
-
-
-(defun ml4pg-extract-views (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (if (and (string= (subseq (car temp) 0 1) "/") (not (string= (car temp) "//")) (not (string= (car temp) "/=")) (not (string= (car temp) "//=")))
- (if (not (string= (subseq (car temp) 0 2) "/("))
- (setf temp2 (append temp2 (list (subseq (car temp) 1))))
- (setf temp2 (append temp2 (list (subseq (car temp) 2 (search " " (car temp))))))))))
-
-
-(defun ml4pg-extract-real-params (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (if (not (or (string= (subseq (car temp) 0 1) "/") (string= (car temp) "//") (string= (car temp) "_")
- (search "->" (car temp)) (search "<-" (car temp)) (string= (car temp) "/=") (string= (car temp) "//=")))
- (setf temp2 (append temp2 (list (car temp)))))))
-
-(defun ml4pg-extract-rewrites (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (if (or (search "->" (car temp)) (search "<-" (car temp)))
- (setf temp2 (append temp2 (list (car temp)))))))
-
-(defun ml4pg-extract-simplifications (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (if (or (string= (car temp) "//") (string= (car temp) "/=") (string= (car temp) "//="))
- (setf temp2 (append temp2 (list (car temp)))))))
-
-(defun ml4pg-compute-value-simpl (list)
- (list 0 (length list) 0 0))
-
-
-(defun ml4pg-extract-views-id (list)
- (do ((temp list (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (if (assoc (car temp) ml4pg-views_id)
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc (car temp) ml4pg-views_id))) ))
- (progn (setf ml4pg-start_view (+ ml4pg-start_view 1))
- (ml4pg-save-view (car temp) ml4pg-start_view)
- (setf ml4pg-views_id
- (append ml4pg-views_id (list (cons (car temp) ml4pg-start_view))))
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc (car temp) ml4pg-views_id)))))))))
-
-
-
-(defun ml4pg-compute-values-rewrite-tactic (list)
- (do ((temp (ml4pg-extract-real-params list) (cdr temp))
- (temp2 ""))
- ((endp temp) (string-to-number temp2))
- (let* ((obj1 (if (string= "-" (subseq (car temp) 0 1)) (subseq (car temp) 1) (car temp)))
- (obj (if (string= "(" (subseq obj1 0 1)) (subseq obj1 1 (search " " obj1)) obj1)))
- (if (assoc obj ml4pg-theorems_id)
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc obj ml4pg-theorems_id)))) )
- (progn (setf ml4pg-start_thm (+ ml4pg-start_thm 1))
- (ml4pg-save-lemma obj ml4pg-start_thm)
- (setf ml4pg-theorems_id
- (append ml4pg-theorems_id (list (cons obj ml4pg-start_thm))))
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc obj ml4pg-theorems_id))))))))))
-
-
-(defun ml4pg-compute-values-apply-tactic (list)
- (do ((temp list (cdr temp))
- (temp2 ""))
- ((endp temp) (string-to-number temp2))
- (let ((obj (if (string= "(" (subseq (car temp) 0 1)) (subseq (car temp) 1) (car temp))))
- (if (member obj ml4pg-hypothesis)
- (setf temp2 (concatenate 'string temp2 "1"))
- (if (assoc obj ml4pg-theorems_id)
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc obj ml4pg-theorems_id)))) )
- (progn (setf ml4pg-start_thm (+ ml4pg-start_thm 1))
- (setf ml4pg-theorems_id
- (append ml4pg-theorems_id (list (cons obj ml4pg-start_thm))))
- (setf temp2 (concatenate 'string temp2 (format "%s" (cdr (assoc obj ml4pg-theorems_id)))))))))))
-
-
-(defun ml4pg-compute-value-views-move (list)
- (list (* -1 (ml4pg-get-number-list2 list 5)) (length list) (* -1 (ml4pg-get-number-list2 list 4)) (string-to-number (ml4pg-extract-views-id list))))
-
-(defun ml4pg-compute-value-views-apply (list)
- (list (ml4pg-get-number-list2 list 5) (length list) (* -1 (ml4pg-get-number-list2 list 4)) (string-to-number (ml4pg-extract-views-id list))))
-
-(defun ml4pg-compute-value-views-case (list)
- (list (ml4pg-get-number-list2 list 6) (length list) (* -1 (ml4pg-get-number-list2 list 4)) (string-to-number (ml4pg-extract-views-id list))))
-
-(defun ml4pg-compute-value-views-exact (list)
- (list (ml4pg-get-number-list2 list 9) (length list) (* -1 (ml4pg-get-number-list2 list 4)) (string-to-number (ml4pg-extract-views-id list))))
-
-(defun ml4pg-compute-value-rewrites (list)
- (list (ml4pg-get-number-list2 list 7) (length list) (* -1 (ml4pg-get-number-list2 list 4)) (ml4pg-get-number-list list)))
-
-
-
-(defun ml4pg-remove-empties (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (if (not (string= (car temp) ""))
- (setf temp2 (append temp2 (list (car temp)))))))
-
-
-
-(defun ml4pg-occurrences (c string)
- (do ((temp string)
- (n 0))
- ((not (search c temp)) n)
- (progn (setf n (1+ n))
- (setf temp (subseq temp (1+ (search c temp)))))))
-
-
-(defun ml4pg-put-together-parenthesis (list)
- (do ((temp list (cdr temp))
- (n 0)
- (temp2 nil)
- (aux ""))
- ((endp temp) temp2)
- (cond ((search "(" (car temp))
- (progn (setf n (1+ n))
- (setf aux (concatenate 'string aux (car temp) " "))))
- ((and (search ")" (car temp)) (not (= (- n (ml4pg-occurrences ")" (car temp))) 0)))
- (progn (setf n (- n (ml4pg-occurrences ")" (car temp))))
- (setf aux (concatenate 'string aux (car temp) " "))))
- ((search ")" (car temp))
- (progn (setf n (1- n))
- (setf aux (concatenate 'string aux (car temp)))
- (setf temp2 (append temp2 (list aux)))
- (setf aux "")))
- ((not (= n 0))
- (progn (setf aux (concatenate 'string aux (car temp) " "))))
- (t (setf temp2 (append temp2 (list (car temp))))
- ))))
-
-
-(defun ml4pg-remove-squared-parenthesis (string res)
- (let ((pos1 (search "[" string))
- (pos2 (search "{" string)))
- (cond ((and pos1 pos2)
- (if (< pos1 pos2)
- (ml4pg-remove-squared-parenthesis
- (subseq string (1+ (search "]" string :start2 pos1)))
- (concatenate 'string res (subseq string 0 pos1)))
- (ml4pg-remove-squared-parenthesis
- (subseq string (1+ (search "}" string :start2 pos2)))
- (concatenate 'string res (subseq string 0 pos2)))))
- (pos1 (ml4pg-remove-squared-parenthesis
- (subseq string (1+ (search "]" string :start2 pos1)))
- (concatenate 'string res (subseq string 0 pos1))))
- (pos2 (ml4pg-remove-squared-parenthesis
- (subseq string (1+ (search "}" string :start2 pos2)))
- (concatenate 'string res (subseq string 0 pos2))))
- (t (concatenate 'string res string)))))
-
-
-(defun ml4pg-remove-iterations (string)
- (do ((temp string)
- (temp2 ""))
- ((= (length temp) 0) temp2)
- (if (or (string= (subseq temp 0 1) "!") (string= (subseq temp 0 1) "?"))
- (setf temp (subseq temp 1))
- (progn (setf temp2 (concatenate 'string temp2 (subseq temp 0 1)))
- (setf temp (subseq temp 1))
- ))))
-
-
-
-(defun ml4pg-remove-squared-parenthesis2 (string)
- (do ((temp string)
- (temp2 ""))
- ((= (length temp) 0) temp2)
- (if (or (string= (subseq temp 0 1) "[") (string= (subseq temp 0 1) "]") (string= (subseq temp 0 1) "|"))
- (setf temp (subseq temp 1))
- (progn (setf temp2 (concatenate 'string temp2 (subseq temp 0 1)))
- (setf temp (subseq temp 1))
- ))))
-
-
-(defun ml4pg-extract-params3 (cmd)
- (let* ((res (ml4pg-extract-params2 (ml4pg-remove-iterations (ml4pg-remove-squared-parenthesis cmd "") ) nil))
- (res1 (ml4pg-remove-empties res)))
- (ml4pg-put-together-parenthesis res1)))
-
-
-(defun ml4pg-extract-params4 (cmd)
- (let* ((res (ml4pg-extract-params2 (ml4pg-remove-squared-parenthesis2 cmd) nil))
- (res1 (ml4pg-remove-empties res)))
- (ml4pg-put-together-parenthesis res1)))
-
-
-
-;;; The following functions provide the numbers associated with a concrete tactic
-
-
-(defun ml4pg-numbers-move=> (cmd top level)
- (let* ((params (ml4pg-extract-params3 (ml4pg-remove=> (subseq cmd (+ 2 (search "=>" cmd)))) ))
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (rewrites (ml4pg-extract-rewrites params))
- (rewrites-nums (ml4pg-compute-value-rewrites rewrites))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-move views))
- (real-params (ml4pg-extract-real-params params))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis real-params)))
- (types-params (ml4pg-get-types-list real-params 0))
- (foo3 (ml4pg-add-info-to-level (list (ml4pg-get-types-list real-params 0) 0 0 0 0 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-move (append ml4pg-move (list (list (ml4pg-get-types-list (if real-params (list (car real-params)) nil) 0) (ml4pg-get-types-list (cdr real-params) 0)
- (* -1 (ml4pg-get-number-list real-params)) top))))))
- (append (list (list (ml4pg-get-number-list2 real-params (cdr (assoc "move" ml4pg-tactic_id))) (length real-params) types-params (* -1 (ml4pg-get-number-list real-params))))
- (if simpl (list simpl-nums) nil)
- (if views (list views-nums) nil)
- (if rewrites (list rewrites-nums) nil))))
-
-(defun ml4pg-numbers-move/ (cmd top level)
- (let* ((params (ml4pg-extract-params3 (ml4pg-remove=> (subseq cmd 4)) ))
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (rewrites (ml4pg-extract-rewrites params))
- (rewrites-nums (ml4pg-compute-value-rewrites rewrites))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-move views))
- (real-params (ml4pg-extract-real-params params))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis real-params)))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 (nth 2 views-nums) 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-move/ (append ml4pg-move/ (list (list -4 (* -4 (ml4pg-get-number-list real-params)) (nth 3 views-nums) top)))))
- (types-params (ml4pg-get-types-list real-params 0)))
- (append (list views-nums)
- (if real-params (list (list (ml4pg-get-number-list2 real-params (cdr (assoc "move" ml4pg-tactic_id))) (length real-params) types-params (* -1 (ml4pg-get-number-list real-params)))))
- (if simpl (list simpl-nums) nil)
- (if rewrites (list rewrites-nums) nil)))
-)
-
-(defun ml4pg-numbers-move: (cmd top level)
- (let* ((params (ml4pg-extract-params3 (subseq cmd (+ 1 (search ":" cmd)))) )
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (rewrites (ml4pg-extract-rewrites params))
- (rewrites-nums (ml4pg-compute-value-rewrites rewrites))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-move views))
- (real-params (ml4pg-extract-real-params params))
- (types-params (ml4pg-get-types-list real-params 0))
- (foo3 (ml4pg-add-info-to-level (list (ml4pg-get-types-list real-params 0) 0 0 0 0 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-move (append ml4pg-move (list (list (ml4pg-get-types-list (if real-params (list (car real-params)) nil) 0) (ml4pg-get-types-list (cdr real-params) 0)
- (* 1 (ml4pg-get-number-list real-params)) top))))))
- (append (list (list (* -1 (ml4pg-get-number-list2 real-params (cdr (assoc "move" ml4pg-tactic_id)))) (length real-params) types-params (* -1 (ml4pg-get-number-list real-params))))
- (if views (list views-nums) nil)
- (if simpl (list simpl-nums) nil)
- (if rewrites (list rewrites-nums) nil)))
-
-)
-
-(defun ml4pg-numbers-move< (cmd top level)
- (let* ((foo (list (ml4pg-compute-value-rewrites (list 1))))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 top 0 0 0 0 0) level))
- (foo2 (setf ml4pg-rewrite (append ml4pg-rewrite (list (list 4 0 1 top))))))
- foo
- )
-)
-
-(defun ml4pg-numbers-apply: (cmd top level)
- (if (string= cmd "apply")
- (list (list (cdr (assoc "apply" ml4pg-tactic_id)) 1 0 0))
- (let ((moves (search "=>" cmd))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 100 0 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-apply (append ml4pg-apply (list (list -4 0 100 top))))))
- (if (not moves)
- (list (list (cdr (assoc "apply" ml4pg-tactic_id))
- 1
- -4
- (ml4pg-compute-values-apply-tactic (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (if (search ":" cmd) (search ":" cmd) (search " " cmd)))))))))
- (let* ((args0 (ml4pg-extract-params4 (subseq cmd (+ 2 moves))))
- (simpl (ml4pg-extract-simplifications args0))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (args (ml4pg-extract-real-params args0))
- )
- (append (list (list (cdr (assoc "apply" ml4pg-tactic_id))
- 1 -4
- (ml4pg-compute-values-apply-tactic (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (if (search ":" cmd) (search ":" cmd) (search " " cmd))) moves))))
- ))
- (list (list (* -1 (ml4pg-get-number-list2 args (cdr (assoc "move" ml4pg-tactic_id)))) (length args) (ml4pg-get-types-list args 0) (* -1 (ml4pg-get-number-list args))))
- (if simpl (list simpl-nums) nil)))))
-))
-
-(defun ml4pg-numbers-elim (cmd top level)
- (let* ((moves (search "=>" cmd))
- (foo3 (ml4pg-add-info-to-level (list 0 0 (ml4pg-get-types-list (list (car (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (search ":" cmd)) moves))))) 0) 0 0 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-elim (append ml4pg-elim (list (list (ml4pg-get-types-list (list (car (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (search ":" cmd)) moves))))) 0) 0 -1 top))))))
- (if (not moves)
- (list (list (cdr (assoc "elim" ml4pg-tactic_id))
- 1 (ml4pg-get-types-list (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (search ":" cmd))))) 0) -1))
- (let* ((args0 (ml4pg-extract-params4 (subseq cmd (+ 2 moves))))
- (simpl (ml4pg-extract-simplifications args0))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (args (ml4pg-extract-real-params args0)))
- (append (list (list (cdr (assoc "elim" ml4pg-tactic_id))
- 1 (ml4pg-get-types-list (ml4pg-extract-real-params (ml4pg-extract-params3 (subseq cmd (+ 1 (search ":" cmd)) moves))) 0) -1))
- (list (list (* -1 (ml4pg-get-number-list2 args (cdr (assoc "move" ml4pg-tactic_id)))) (length args) (ml4pg-get-types-list args 0) (* -1 (ml4pg-get-number-list args))))
- (if simpl (list simpl-nums) nil))))))
-
-(defun ml4pg-numbers-case (cmd top level)
- (if (string= cmd "case")
- (list (list (cdr (assoc "case" ml4pg-tactic_id)) 1 0 0))
- (let ((moves (search "=>" cmd))
- (foo3 (ml4pg-add-info-to-level (list 0 (if (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd))))))
- (ml4pg-get-types-list (list (car (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd)))))))) 0) 1) 0 0 0 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-case (append ml4pg-case (list (list (if (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd))))))
- (ml4pg-get-types-list (list (car (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd)))))))) 0) 1)
- 0 -1 top))))))
- (if (not moves)
- (list (list (cdr (assoc "case" ml4pg-tactic_id))
- 1 (ml4pg-get-types-list (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd)))))) 0) -1))
- (let* ((args0 (ml4pg-extract-params4 (subseq cmd (+ 2 moves))))
- (simpl (ml4pg-extract-simplifications args0))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (args (ml4pg-extract-real-params args0)))
- (if (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd)))))
- (append (list (list (cdr (assoc "case" ml4pg-tactic_id))
- 1 (ml4pg-get-types-list (ml4pg-extract-real-params (ml4pg-extract-params3 (if (search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))) (subseq cmd (+ 1 (search " " cmd)))))) 0) -1))
- (list (list (* -1 (ml4pg-get-number-list2 args (cdr (assoc "move" ml4pg-tactic_id)))) (length args) (ml4pg-get-types-list args 0) (* -1 (ml4pg-get-number-list args))))
- (if simpl (list simpl-nums) nil))
- (append (list (list (cdr (assoc "case" ml4pg-tactic_id))
- 1 0 0))
- (list (list (* -1 (ml4pg-get-number-list2 args (cdr (assoc "move" ml4pg-tactic_id)))) (length args) (ml4pg-get-types-list args 0) (* -1 (ml4pg-get-number-list args))))
- (if simpl (list simpl-nums) nil))))))))
-
-(defun ml4pg-numbers-case/ (cmd top level)
- (let* ((params (ml4pg-extract-params4 (ml4pg-separate-/ (ml4pg-remove=> (subseq cmd 5)) "")))
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (rewrites (ml4pg-extract-rewrites params))
- (rewrites-nums (ml4pg-compute-value-rewrites rewrites))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-case views))
- (real-params (ml4pg-extract-real-params params))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis real-params)))
- (types-params (ml4pg-get-types-list real-params 0))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 0 (nth 2 views-nums) 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-case/ (append ml4pg-case/ (list (list -4 (/ (nth 2 views-nums) 10) (nth 3 views-nums) top))))))
- (append (list views-nums)
- (if real-params (list (list (ml4pg-get-number-list2 real-params (cdr (assoc "move" ml4pg-tactic_id))) (length real-params) types-params (* -1 (ml4pg-get-number-list real-params)))))
- (if simpl (list simpl-nums) nil)
- (if rewrites (list rewrites-nums) nil)))
-)
-
-(defun ml4pg-separate-/ (string res)
- (let ((pos (search "/" string)))
- (if (not pos)
- (concatenate 'string res string)
- (cond ((= pos 0) (ml4pg-separate-/ (subseq string (1+ pos)) (concatenate 'string "/" res (subseq string 0 pos))))
- ((not (string= " " (subseq string (1- pos) pos)))
- (ml4pg-separate-/ (subseq string (1+ pos)) (concatenate 'string res (subseq string 0 pos) " /")))
- (t (ml4pg-separate-/ (subseq string (1+ pos)) (concatenate 'string res (subseq string 0 pos))))))))
-
-
-(defun ml4pg-numbers-apply/ (cmd top level)
- (let* ((params (ml4pg-extract-params4 (ml4pg-separate-/ (ml4pg-remove=> (subseq cmd 5)) "")))
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (rewrites (ml4pg-extract-rewrites params))
- (rewrites-nums (ml4pg-compute-value-rewrites rewrites))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-apply views))
- (real-params (ml4pg-extract-real-params params))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis real-params)))
- (types-params (ml4pg-get-types-list real-params 0))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 (nth 2 views-nums) 0 0 0 0 0 0 0 0) level))
- (foo2 (setf ml4pg-apply/ (append ml4pg-apply/ (list (list -4 (/ (nth 2 views-nums) 10) (nth 3 views-nums) top))))))
- (append (list views-nums)
- (if real-params (list (list (ml4pg-get-number-list2 real-params (cdr (assoc "move" ml4pg-tactic_id))) (length real-params) types-params (* -1 (ml4pg-get-number-list real-params)))))
- (if simpl (list simpl-nums) nil)
- (if rewrites (list rewrites-nums) nil)))
-)
-
-(defun ml4pg-numbers-exact (cmd top level)
- (if (string= cmd "exact")
- (list (list (cdr (assoc "exact" ml4pg-tactic_id)) 1 0 0))
- (let* ((params (ml4pg-extract-params3 (cond ((search ":" cmd) (subseq cmd (+ 1 (search ":" cmd))))
- ((search "/" cmd) (subseq cmd (search "/" cmd)))
- (t (subseq cmd (+ 1 (search " " cmd)))))))
- (views (ml4pg-extract-views params))
- (views-nums (ml4pg-compute-value-views-exact views))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 0 0 0 100 0 0) level))
- (foo2 (setf ml4pg-exact (append ml4pg-exact (list (list -4 0 100 top))))))
- (if views
- (list views-nums)
- (list (list (cdr (assoc "exact" ml4pg-tactic_id))
- 1
- -4
- (ml4pg-compute-values-apply-tactic (ml4pg-extract-real-params params))))))))
-
-(defun ml4pg-numbers-rewrite (cmd top level)
- (let* ((params (ml4pg-extract-params3 (subseq cmd (+ 1 (search " " cmd)))) )
- (views (ml4pg-extract-views params))
- (simpl (ml4pg-extract-simplifications params))
- (simpl-nums (ml4pg-compute-value-simpl simpl))
- (views-nums (ml4pg-compute-value-views-move views))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 (ml4pg-get-number-list2 (cdr params) 4) 0 0 0 0 0) level))
- (foo2 (setf ml4pg-rewrite (append ml4pg-rewrite (list (list -4 (ml4pg-get-number-list2 (cdr params) 4) (ml4pg-compute-values-rewrite-tactic params) top))))))
- (append (list (list (ml4pg-get-number-list2 params (cdr (assoc "rewrite" ml4pg-tactic_id)))
- (length params)
- (ml4pg-get-number-list2 params 4)
- (ml4pg-compute-values-rewrite-tactic params)))
- (if simpl (list simpl-nums) nil)
- ))
-)
-
-(defun ml4pg-numbers-exists (cmd top level)
- (let ((moves (search "=>" cmd))
- (foo3 (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 0 1 0 0 0 0) level))
- (foo2 (setf ml4pg-exists (append ml4pg-exists (list (list 8 0 1 top))))))
- (if (not moves)
- (let* ((params (ml4pg-extract-params3 (subseq cmd 7)) )
- (types-params (ml4pg-get-types-list-exists params 0))
- )
- (list (list (cdr (assoc "exists" ml4pg-tactic_id)) 1 types-params 0)))
- (let* ((args0 (ml4pg-extract-params4 (subseq cmd (+ 2 moves))))
- (simpl (ml4pg-extract-simplifications args0))
- (simpl-nums (cml4pg-ompute-value-simpl simpl))
- (args (ml4pg-extract-real-params args0)))
- (append (list (list (cdr (assoc "exists" ml4pg-tactic_id))
- 1 (ml4pg-get-types-list-exists (ml4pg-extract-params3 (subseq cmd 7 moves)) 0) -1))
- (list (list (* -1 (ml4pg-get-number-list2 args (cdr (assoc "move" ml4pg-tactic_id)))) (length args) (ml4pg-get-types-list args 0) (* -1 (ml4pg-get-number-list args))))
- (if simpl (list simpl-nums) nil)))))
- )
-
-
-(defun ml4pg-numbers-done (cmd top level)
- (progn
- (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 0 0 top 0 0 0) level)
- (setf ml4pg-done (append ml4pg-done (list (list 0 0 0 top))))
- (list (list (cdr (assoc "[]" ml4pg-tactic_id)) 1 0 0) ) )
-)
-
-
-(defun ml4pg-remove-multiple-spaces (string)
- (let ((d (search " " string)))
- (if d
- (ml4pg-remove-multiple-spaces (concatenate 'string (subseq string 0 d) (subseq string (1+ d))))
- string)))
-
-
-
-(defun ml4pg-compute-numbers-cmd (cmd top level)
- (let* ((cmd1 (ml4pg-remove-multiple-spaces cmd)))
- (cond ((search "symmetry" cmd) nil)
- ((search "last by" cmd) (ml4pg-compute-numbers-cmd (subseq cmd (+ 3 (search "by" cmd))) top level))
- ((search "first by" cmd) (ml4pg-compute-numbers-cmd (subseq cmd (+ 3 (search "by" cmd))) top level))
- ((string= "try" (subseq cmd 0 2)) (ml4pg-compute-numbers-cmd (subseq cmd (+ 4 (search "try" cmd))) top level))
- ((string= "do" (subseq cmd 0 2)) (ml4pg-compute-numbers-cmd (subseq cmd (cond ((search "!" cmd) (1+ (search "!" cmd)))
- ((search "?" cmd) (1+ (search "?" cmd)))
- (t (+ 3 (search "do" cmd))))) top level))
- ((search "have" cmd) nil)
- ((or (search "move=>" cmd1) (search "move =>" cmd1)) (ml4pg-numbers-move=> cmd1 top level))
- ((or (search "move:" cmd1) (search "move :" cmd1)) (ml4pg-numbers-move: cmd1 top level))
- ((or (search "move/" cmd1) (search "move /" cmd1)) (ml4pg-numbers-move/ cmd1 top level))
- ((or (search "move<-" cmd1) (search "move->" cmd1) (search "move ->" cmd1) (search "move <-" cmd1)) (ml4pg-numbers-move< cmd1 top level))
- ((or (search "apply/" cmd1) (search "apply /" cmd1)) (ml4pg-numbers-apply/ cmd1 top level))
- ((or (search "apply:" cmd1) (search "apply :" cmd1) (search "apply" cmd1)) (ml4pg-numbers-apply: cmd1 top level))
- ((or (search "elim:" cmd1) (search "elim :" cmd1)) (ml4pg-numbers-elim cmd1 top level))
- ((or (search "case/" cmd1) (search "case /" cmd1)) (ml4pg-numbers-case/ cmd1 top level))
- ((or (search "case:" cmd1) (search "case" cmd1)) (ml4pg-numbers-case cmd1 top level))
- ((or (search "exact" cmd1) (search "exact :" cmd1)) (ml4pg-numbers-exact cmd1 top level))
- ((search "rewrite" cmd1) (ml4pg-numbers-rewrite cmd1 top level))
- ((search "exists" cmd1) (ml4pg-numbers-exists cmd1 top level))
- ((or (search "[]" cmd1) (search "done" cmd1) (search "constructor" cmd1)) (ml4pg-numbers-done cmd1 top level))
-
- ((string= (subseq cmd1 0 4) "pose") nil)
- ((string= (subseq cmd1 0 3) "set") nil)
- ((string= (subseq cmd1 0 4) "left") nil)
- ((string= (subseq cmd1 0 4) "righ") nil)
- )
- )
- )
-
-
-(defun ml4pg-split-command (cmd result end)
- (if (or (string= " " (subseq cmd 0 1)) (string= "-" (subseq cmd 0 1)))
- (ml4pg-split-command (subseq cmd 1) result end)
- (let ((is_by (string= "by" (subseq cmd 0 2))))
- (if is_by
- (ml4pg-split-command (subseq cmd 3) result 1)
- (let ((comma (search ";" cmd)))
- (if comma
- (ml4pg-split-command (subseq cmd (1+ comma)) (append result (list (subseq cmd 0 comma))) end)
- (list (append result (list (subseq cmd 0 (1- (length cmd))))) end)))))))
-
-
-
-
-(defun ml4pg-add-tactics (tactics end top level)
- (do ((temp tactics (cdr temp))
- (temp2 nil))
- ((endp temp) (if (> end 0) (append temp2 (list (list 0 1 0 0))) temp2))
- (let ((res (ml4pg-compute-numbers-cmd (car temp) top level)))
- (if res (setf temp2 (append temp2 res))))))
-
-
-;The first value is the tactic, the second one is the number of tactics,
-;the third one is the argument type, the fourth one is if the
-;argument is a hypothesis of a theorem, the fifth one is the top-symbol
-;and the last one the number of subgoals
-
-
-(defun ml4pg-get-numbers (cmd top level)
- (let* ((res (ml4pg-split-command cmd nil 0))
- (tactics (car res))
- (end (cadr res))
- (nums (ml4pg-add-tactics tactics end top level)))
- (if nums (do ((temp (cdr nums) (cdr temp))
- (temp2 (list (format "%s" (nth 0 (car nums))) (nth 1 (car nums)) (format "%s" (nth 2 (car nums))) (format "%s" (nth 3 (car nums))))))
- ((endp temp) (list (string-to-number (nth 0 temp2)) (nth 1 temp2) (string-to-number (nth 2 temp2)) (string-to-number (nth 3 temp2))) )
- (setf temp2 (list (if (or (< (string-to-number(nth 0 temp2)) 0) (< (nth 0 (car temp)) 0))
- (concatenate 'string (format "-%s" (abs (string-to-number(nth 0 temp2)))) (format "%s" (abs (nth 0 (car temp)))))
- (concatenate 'string (format "%s" (abs (string-to-number(nth 0 temp2))) ) (format "%s" (abs (nth 0 (car temp))))))
- (+ (nth 1 temp2) (nth 1 (car temp)))
- (if (or (< (abs (string-to-number(nth 2 temp2))) 0) (< (nth 2 (car temp)) 0))
- (concatenate 'string (format "-%s" (abs (abs (string-to-number(nth 2 temp2))))) (format "%s" (abs (nth 2 (car temp)))))
- (concatenate 'string (format "%s" (abs (abs (string-to-number(nth 2 temp2))))) (format "%s" (abs (nth 2 (car temp))))))
- (if (or (< (string-to-number (nth 3 temp2)) 0) (< (nth 3 (car temp)) 0))
- (concatenate 'string (format "-%s" (abs (string-to-number (nth 3 temp2)))) (format "%s" (abs (nth 3 (car temp)))))
- (concatenate 'string (format "%s" (abs (string-to-number (nth 3 temp2)))) (format "%s" (abs (nth 3 (car temp))))))
- ))
- )
- )))
-
-;; Function to obtain the information just about the goals.
-
-(defun ml4pg-count-seq (item seq)
- (let ((is? (search item seq)))
- (if is?
- (+ 1 (ml4pg-count-seq item (subseq seq (+ 1 is?))))
- 0)))
-
-(defun ml4pg-get-number-of-goals ()
- (let ((r (proof-shell-invisible-cmd-get-result (format "Show Proof"))))
- (ml4pg-count-seq "?" r)))
-
-
-(defun ml4pg-flat (ll)
- (if (endp ll)
- nil
- (append (car ll) (ml4pg-flat (cdr ll)))))
-
-
-
-
-;; The following function computes the result of the tactic
-
-
-(defun ml4pg-digits (n)
- (if (= (mod n 10) 0)
- 0
- (1+ (ml4pg-digits (/ n 10)))))
-
-(defun ml4pg-first-digit (n digits)
- (/ n (expt 10 (1- digits))))
-
-(defun ml4pg-rest-of-digits (n digits)
- (- n (* (ml4pg-first-digit n digits) (expt 10 (1- digits)))))
-
-(defun ml4pg-obtain-tactic-result (tactic)
- (do ((temp (cdr tactic) (cdr temp))
- (temp2 (if (endp tactic) (list 0 0 0 0 0)
- (list (ml4pg-first-digit (nth 0 (car tactic)) (ml4pg-digits (nth 0 (car tactic))))
- (* (ml4pg-rest-of-digits (nth 0 (car tactic)) (ml4pg-digits (nth 0 (car tactic)))) (expt 10 (length (cdr tactic))))
- (* (nth 1 (car tactic)) (expt 10 (length (cdr tactic))))
- (nth 2 (car tactic))
- (nth 3 (car tactic))))))
- ((endp temp) temp2)
- (setf temp2 (list (nth 0 temp2)
- (+ (nth 1 temp2) (* (expt 10 (length (cdr temp))) (nth 0 (car temp))))
- (+ (nth 2 temp2) (* (expt 10 (length (cdr temp))) (nth 1 (car temp))))
- (concat (format "%s" (nth 3 temp2)) (format "%s" (nth 2 (car temp))))
- (+ (nth 4 temp2) (nth 3 (car temp))))
- )
- ))
-
-
-
-
-(defvar ml4pg-useless-terms '("Definition" "Defined" "Fixpoint" "Structure" "Section" "Add Ring" "Hypothesis" "Hypotheses" "Include" "Export" "Parameter" "Axiom"
-"End" "Notation" "Hint" "Inductive" "Variable" "Implicit" "Import" "Canonical" "Coercion"
-"Module" "Ltac" "Let" "Opaque" "Bind" "Scope" "Require" "Infix" "Record" "Fact" "Print"))
-
-(defun ml4pg-is-in-search (cmd)
- (do ((temp ml4pg-useless-terms (cdr temp))
- (is nil))
- ((or (endp temp) is) is)
- (if (search (car temp) cmd) (setf is t))))
-
-
-
-(defun ml4pg-compute-tactic-value (list)
- (if (not list) (list 0 0 0 0 0)
- (let ((len (length list))
- (arg0 (car (car list)))
- (arg1 (format "%s" (nth 1 (car list))))
- (hyp (format "%s" (nth 2 (car list))))
- (top (format "%s" (nth 3 (car list)))))
- (do ((temp (cdr list) (cdr temp)))
- ((endp temp) (list arg0 (string-to-number arg1) (string-to-number hyp) (string-to-number top) len))
- (progn (setf arg1 (format "%s%s%s" arg1 (nth 0 (car temp)) (nth 1 (car temp))))
- (setf hyp (format "%s%s" hyp (nth 2 (car temp))))
- (setf top (format "%s%s" top (nth 3 (car temp))))
- )))))
-
-
-
-(defun ml4pg-compute-tactic-result (name)
- (append (list name) (list (append
- (ml4pg-compute-tactic-value ml4pg-move)
- (ml4pg-compute-tactic-value ml4pg-case)
- (ml4pg-compute-tactic-value ml4pg-elim)
- (ml4pg-compute-tactic-value ml4pg-apply/)
- (ml4pg-compute-tactic-value ml4pg-move/)
- (ml4pg-compute-tactic-value ml4pg-case/)
- (ml4pg-compute-tactic-value ml4pg-rewrite)
- (ml4pg-compute-tactic-value ml4pg-exists)
- (ml4pg-compute-tactic-value ml4pg-done)
- (ml4pg-compute-tactic-value ml4pg-exact)))))
-
-(defun ml4pg-compute-proof-tree-result (name)
- (append (list name) (list (append
- (if ml4pg-tdl1 ml4pg-tdl1 (ml4pg-generate-zeros 13))
- (if ml4pg-tdl2 ml4pg-tdl2 (ml4pg-generate-zeros 13))
- (if ml4pg-tdl3 ml4pg-tdl3 (ml4pg-generate-zeros 13))
- (if ml4pg-tdl4 ml4pg-tdl4 (ml4pg-generate-zeros 13))
- (if ml4pg-tdl5 ml4pg-tdl5 (ml4pg-generate-zeros 13))))))
-
-
-
-
-
-(defun ml4pg-export-theorem-aux (result name)
- (let* ((semis (save-excursion
- (skip-chars-backward " \t\n"
- (proof-queue-or-locked-end))
- (proof-segment-up-to-using-cache (point))))
- (comment (caar semis))
- (cmd (cadar semis))
- (pos_dot (search "." cmd))
- (pos_space (search " " cmd))
- (ts nil))
- (if semis
- (cond ((or (string= comment "comment")
- (ml4pg-is-in-search cmd))
- (progn (proof-assert-next-command-interactive)
- (ml4pg-export-theorem-aux result name)))
- ((search "Lemma" cmd)
- (progn (proof-assert-next-command-interactive)
- (ml4pg-export-theorem-aux result
- (subseq cmd (1+ (search " " cmd))
- (search " " cmd :start2 (1+ (search " " cmd))))
- )))
- ((search "Proof" cmd)
- (progn (proof-assert-next-command-interactive)
- (ml4pg-export-theorem-aux result name )))
- ((search "Theorem" cmd)
- (progn (proof-assert-next-command-interactive)
- (ml4pg-export-theorem-aux result
- (subseq cmd (1+ (search " " cmd))
- (search " " cmd :start2 (1+ (search " " cmd))))
- )))
- ((search "Qed." cmd)
- (progn (proof-assert-next-command-interactive)
- ; (insert (format "\n(* %s *)\n" (reverse result)))
- ;(setf proof-tree-level (append proof-tree-level (list (compute-proof-result))))
- ;(setf tactic-level (append tactic-level (list (compute-tactic-result))))
- (setf ml4pg-tactic-level (append ml4pg-tactic-level (list (ml4pg-compute-tactic-result name))))
- (setf ml4pg-proof-tree-level (append ml4pg-proof-tree-level (list (ml4pg-compute-proof-tree-result name))))
- (if name
- ; (split-feature-vector name (flat (reverse result)))
- (setf ml4pg-saved-theorems (append ml4pg-saved-theorems
- (list (list name (ml4pg-flat (reverse result))))))
- )))
- (t (progn (setf ts (ml4pg-get-top-symbol))
- (setf ng (ml4pg-get-number-of-goals))
- (proof-assert-next-command-interactive)
- (setf ng2 (ml4pg-get-number-of-goals))
- (ml4pg-export-theorem-aux (cons (append (ml4pg-get-numbers cmd ts ml4pg-current-level) (list ts) (list ng2)) result)
- name)
- (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 0 0 0 0 ng2 (if (< ng2 ng) 1 0)) ml4pg-current-level)
- (setf ml4pg-current-level (1+ ml4pg-current-level))
-
- ))))))
-
-
-
-
-(defun ml4pg-split-feature-vector (name fv)
- (let ((len (1+ (floor (length fv) 30))))
- (do ((i 0 (+ i 1)))
- ((equal i len) nil)
- (setf ml4pg-saved-theorems (append ml4pg-saved-theorems
- (list (list name (ml4pg-take-30-from fv i))))))
- ))
-
-
-(defun ml4pg-take-30-from (list pos)
- (let ((j (* 30 pos)))
- (do ((i j (1+ i))
- (temp2 nil (if (nth i list) (cons (nth i list) temp2) (cons 0 temp2))))
- ((= i (+ j 30)) (reverse temp2)))))
-
-
-
-
-;;; Functions to save the files
-
-(defun ml4pg-save-file-conventions1 ()
- (interactive)
- (let ((file (read-file-name "Save in file (don't include the extension): ")))
- (progn (with-temp-file (concat file "_goals.csv") (insert (ml4pg-extract-features-1)))
- (with-temp-file (concat file "_tactics.csv") (insert (ml4pg-extract-features-2 tactic-level)))
- (with-temp-file (concat file (format "_summary.txt")) (insert (ml4pg-extract-names))))))
-
-
-(defun ml4pg-extract-names ()
- (do ((temp ml4pg-saved-theorems (cdr temp))
- (temp2 "")
- (i 1 (1+ i)))
- ((endp temp) temp2)
- (setf temp2 (concat temp2 (format "%s %s\n" i (ml4pg-remove_last_colon (caar temp)))) )))
-
-
-
-
-
-(defun ml4pg-print-list (list)
- (do ((temp list (cdr temp))
- (temp2 ""))
- ((endp temp) (subseq temp2 0 (1- (length temp2))))
- (setf temp2 (concat temp2 (format "%s," (car temp))) )))
-
-
-(defun ml4pg-last-part-of-lists (list)
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (setf temp2 (append temp2 (list (cadar temp))))))
-
-
-
-
-(defun ml4pg-extract-features-1 ()
- (let ((fm (ml4pg-find-max-length)))
- (do ((temp (ml4pg-last-part-of-lists ml4pg-saved-theorems) (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (setf temp2 (concat temp2
- (format "%s\n"
- (ml4pg-print-list (ml4pg-take-30 (append (car temp)
- (ml4pg-generate-zeros 30))) ))))
- )
- ))
-
-
-
-
-
-
-(defun ml4pg-extract-features-2 (list)
- (do ((temp (ml4pg-last-part-of-lists (cdr list)) (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (setf temp2 (concat temp2 (format "%s\n" (ml4pg-print-list (car temp)))))))
-
-
-
-(defun ml4pg-generate-zeros (n)
- (do ((i 0 (1+ i))
- (temp nil (cons 0 temp)))
- ((= i n) temp)))
-
-(defun ml4pg-find-max-length ()
- (do ((temp ml4pg-saved-theorems (cdr temp))
- (i 0))
- ((endp temp) i)
- (if (< i (length (cadar temp)))
- (setf i (length (cadar temp)))
- nil)))
-
-(defun ml4pg-take-30 (list)
- (do ((i 0 (1+ i))
- (temp list (cdr temp))
- (temp2 nil (cons (car temp) temp2)))
- ((= i 30) (reverse temp2))))
-
-
-;; Function which extract the info of a theorem up to a concrete point
-
-(defvar ml4pg-tactic-temp nil)
-(defvar ml4pg-proof-tree-temp nil)
-
-(defun ml4pg-extract-info-up-to-here ()
- (interactive)
- (setf ml4pg-move nil
- ml4pg-case nil
- ml4pg-elim nil
- ml4pg-apply nil
- ml4pg-apply/ nil
- ml4pg-move/ nil
- ml4pg-case/ nil
- ml4pg-rewrite nil
- ml4pg-exists nil
- ml4pg-done nil
- ml4pg-exact nil
- ml4pg-tactic-temp nil
- ml4pg-tdl1 nil
- ml4pg-tdl2 nil
- ml4pg-tdl3 nil
- ml4pg-tdl4 nil
- ml4pg-tdl5 nil
- ml4pg-current-level 1
- ml4pg-dot-level nil)
- (let ((final (point))
- (result nil)
- (end nil))
- (search-backward "Proof.")
- (proof-goto-point)
- (while (< (point) final)
- (let* ((semis (save-excursion
- (skip-chars-backward " \t\n"
- (proof-queue-or-locked-end))
- (proof-segment-up-to-using-cache (point))))
- (comment (caar semis))
- (cmd (cadar semis))
- (ts nil))
- (progn (setf ts (ml4pg-get-top-symbol))
- (setf ng (ml4pg-get-number-of-goals))
- (proof-assert-next-command-interactive)
- (setf ng2 (ml4pg-get-number-of-goals))
- (if cmd
- (setf result (cons (append (ml4pg-get-numbers cmd ts ml4pg-current-level) (list ts) (list ng2)) result)))
- (ml4pg-add-info-to-level (list 0 0 0 0 0 0 0 0 0 0 0 ng2 (if (< ng2 ng) 1 0)) ml4pg-current-level)
- (setf ml4pg-current-level (1+ ml4pg-current-level))
- )
-
- )
- )
- (setf ml4pg-tactic-temp (cadr (ml4pg-compute-tactic-result "")))
- (setf ml4pg-proof-tree-temp (cadr (ml4pg-compute-proof-tree-result "")))
- (ml4pg-take-30 (append (ml4pg-flat (reverse result)) (ml4pg-generate-zeros 30) ))
- (proof-shell-invisible-cmd-get-result (format "Unset Printing All"))
- ))
-
-
-
-(defun ml4pg-extract-features-1-bis (thm)
- (let ((fm (ml4pg-find-max-length)))
- (do ((temp (append (ml4pg-last-part-of-lists ml4pg-saved-theorems) (list thm)) (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (setf temp2 (concat temp2
- (format "%s\n"
- (ml4pg-print-list (ml4pg-take-30 (append (car temp)
- (ml4pg-generate-zeros 30))) ))))
- )
- ))
-
-
-(defun ml4pg-extract-features-2-bis (thm list)
- (let ((fm (find-max-length)))
- (do ((temp (append (ml4pg-last-part-of-lists (cdr list)) (list thm)) (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (setf temp2 (concat temp2
- (format "%s\n"
- (ml4pg-print-list (car temp)))))
- )
- ))
-
-
-
-
-
-
-;; Function which extract the information from all the theorems up to a point
-
-(defun ml4pg-extract-feature-theorems ()
- (interactive)
- (let ((final (point))
- (current-level 1)
- (last-point -1))
- (ml4pg-export-theorem)
- (while (and (< (point) final) (not (= (point) last-point)))
- (progn (setq last-point (point))
- (ml4pg-export-theorem)))))
-
-
-
-
-
-(defun ml4pg-extract-theorems-library ()
- (interactive)
- (search-backward "Qed.")
- (forward-char)
- (forward-char)
- (forward-char)
- (forward-char)
- (let ((final (point))
- (last-point -1))
- (beginning-of-buffer)
- (proof-goto-point)
- (ml4pg-export-theorem)
- (while (and (< (point) final) (not (= (point) last-point)))
- (progn (setq last-point (point))
- (ml4pg-export-theorem)))
- )
-
- )
-
-
-
-;;; Function to normalize the results
-
-(defun ml4pg-max-two-lists (list1 list2)
- (do ((temp1 (ml4pg-take-30 (append list1 (ml4pg-generate-zeros 24))) (cdr temp1))
- (temp2 (ml4pg-take-30 (append list2 (ml4pg-generate-zeros 24))) (cdr temp2))
- (temp nil))
- ((endp temp1) temp)
- (if (< (car temp1) (car temp2))
- (setf temp (append temp (list (car temp2))))
- (setf temp (append temp (list (car temp1))))
- )))
-
-(defun ml4pg-min-two-lists (list1 list2)
- (do ((temp1 (ml4pg-take-30 (append list1 (ml4pg-generate-zeros 24))) (cdr temp1))
- (temp2 (ml4pg-take-30 (append list2 (ml4pg-generate-zeros 24))) (cdr temp2))
- (temp nil))
- ((endp temp1) temp)
- (if (> (car temp1) (car temp2))
- (setf temp (append temp (list (car temp2))))
- (setf temp (append temp (list (car temp1))))
- )))
-
-(defun ml4pg-max-position (list )
- (do ((temp list (cdr temp))
- (max (ml4pg-generate-zeros (length (car list)))))
- ((endp temp) max)
- (setf max (ml4pg-max-two-lists max (car temp)))))
-
-(defun ml4pg-min-position (list )
- (do ((temp list (cdr temp))
- (min (ml4pg-generate-zeros (length (car list)))))
- ((endp temp) min)
- (setf min (ml4pg-min-two-lists min (car temp)))))
-
-
-(defun ml4pg-normalize-list (list max min)
- (do ((temp (ml4pg-take-30 (append list (ml4pg-generate-zeros 24))) (cdr temp))
- (temp-max max (cdr temp-max))
- (temp-min min (cdr temp-min))
- (temp2 nil))
- ((endp temp) temp2)
- (cond ((< 0 (car temp)) (setf temp2 (append temp2 (list (/ (+ (car temp) .0) (car temp-max))))))
- ((= 0 (car temp)) (setf temp2 (append temp2 (list 0))))
- (t (setf temp2 (append temp2 (list (- (/ (+ (car temp) .0) (car temp-min))))))))))
-
-(defun ml4pg-normalize (list)
-
- (let ((max (ml4pg-max-position list))
- (min (ml4pg-min-position list)))
- (do ((temp list (cdr temp))
- (temp2 nil))
- ((endp temp) temp2)
- (setf temp2 (append temp2 (list (ml4pg-normalize-list (car temp) max min)))))))
-
-
-
-
-
-
-
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 18:21:50 +0000