aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/ML4PG/coq/feature_extraction.el
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/ML4PG/coq/feature_extraction.el')
-rw-r--r--contrib/ML4PG/coq/feature_extraction.el862
1 files changed, 0 insertions, 862 deletions
diff --git a/contrib/ML4PG/coq/feature_extraction.el b/contrib/ML4PG/coq/feature_extraction.el
deleted file mode 100644
index 4d934143..00000000
--- a/contrib/ML4PG/coq/feature_extraction.el
+++ /dev/null
@@ -1,862 +0,0 @@
-;; Variables to store the tree depth levels
-
-(defvar ml4pg-tdl1 nil)
-(defvar ml4pg-tdl2 nil)
-(defvar ml4pg-tdl3 nil)
-(defvar ml4pg-tdl4 nil)
-(defvar ml4pg-tdl5 nil)
-
-;; Variables to store the information about the tactic level
-
-(defvar ml4pg-intro nil)
-(defvar ml4pg-case nil)
-(defvar ml4pg-simpltrivial nil)
-(defvar ml4pg-induction nil)
-(defvar ml4pg-simpl nil)
-(defvar ml4pg-rewrite nil)
-(defvar ml4pg-trivial nil)
-
-(defvar ml4pg-hypothesis nil)
-
-(defvar ml4pg-init 0)
-
-(defun ml4pg-export-theorem ()
- (interactive)
- (progn (setf ml4pg-tdl1 nil
- ml4pg-tdl2 nil
- ml4pg-tdl3 nil
- ml4pg-tdl4 nil
- ml4pg-tdl5 nil
- ml4pg-intro nil
- ml4pg-case nil
- ml4pg-simpltrivial nil
- ml4pg-induction nil
- ml4pg-simpl nil
- ml4pg-rewrite nil
- ml4pg-trivial nil
- ml4pg-hypothesis nil
- ml4pg-goal-level nil)
- (if (equal ml4pg-init 0)
- (progn (ml4pg-read-lemmas)
- (setq ml4pg-init 1)))
- (ml4pg-export-theorem-aux nil nil 1 nil)
- (proof-shell-invisible-cmd-get-result (format "Unset Printing All"))
- ))
-
-(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 '(("intro" . 1)
- ("case" . 2)
- ("simpl" . 3)
- ("trivial" . 4)
- ("induction" . 5)
- ("rewrite" . 6)
- ("simpl; trivial" . 34)))
-
-
-(defvar ml4pg-types_id '(("nat" . -2)
- ("Prop" . -4)
- ("bool" . -3)
- ("A" . -1)
- ("list" . -5)))
-
-(defvar ml4pg-theorems_id nil)
-
-;; A function to obtain the type associated with an object
-
-(defun ml4pg-get-type-id (object)
- (let* ((a (proof-shell-invisible-cmd-get-result (format (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 -4)))
-
-
-;; 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 ((string= fst-symbol "forall") 5)
- ((search "->" res2) 7)
- ((string= "@eq" fst-symbol) 6)
- ((string= "and" fst-symbol) 4) ; I have included this
- ((string= "iff" fst-symbol) 8) ; I have included this
- ((string= "or" fst-symbol) 3) ; I have included this
- (t 0))))
-
-;; 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
-
-(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)
- (ml4pg-get-types-list (cdr list) (+ (* -1 (ml4pg-get-type-id (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)))))
-
-;; To obtain the value associated with top symbol in the case of intros
-
-(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 values associated with intros both for the case when parameters are
-;; given and the case intros.
-
-(defun ml4pg-get-obj-intros ()
- (let* ((undo (proof-undo-last-successful-command))
- (obj (proof-shell-invisible-cmd-get-result (format "Show Intros")))
- (dod (proof-assert-next-command-interactive))
- (params (ml4pg-extract-params obj nil))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis params)))
- (types (ml4pg-get-types-list params 0))
- (num (ml4pg-get-number-list params))
- (undo2 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (gts (ml4pg-get-top-symbols-list (length params) 0)))
- (list num types (length params) gts)
- ))
-
-(defun ml4pg-get-obj-intros2 (objects)
- (let* ((params (ml4pg-extract-params2 objects nil))
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis params)))
- (types (ml4pg-get-types-list params 0))
- (num (ml4pg-get-number-list params))
- (undo2 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (gts (ml4pg-get-top-symbols-seq params 0)))
- (list num types (length params) gts)
- ))
-
-;; 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)))))
-
-
-(defvar ml4pg-add_to 0.1)
-(defvar ml4pg-start 100)
-
-(defun ml4pg-extract-theorem-id (cmd)
- (let ((s<- (search "<-" cmd)))
- (if s<-
- (if (assoc (subseq cmd (+ 3 s<-) (search "." cmd)) ml4pg-theorems_id)
- (cdr (assoc (subseq cmd (+ 3 s<-) (search "." cmd)) ml4pg-theorems_id))
- (if (ml4pg-search-in-hyp (subseq cmd (+ 3 s<-) (search "." cmd)) ml4pg-hypothesis)
- 1
- (progn (setf ml4pg-start (+ ml4pg-start ml4pg-add_to))
- (setf ml4pg-theorems_id
- (append ml4pg-theorems_id (list (cons (subseq cmd (+ 3 s<-)
- (search "." cmd))
- ml4pg-start))))
- (ml4pg-save-lemma (subseq cmd (+ 3 s<-)
- (search "." cmd)) ml4pg-start)
- (setf ml4pg-add_to (/ ml4pg-add_to 2))
- ml4pg-start
- )))
- (if (assoc (subseq cmd (+ 1 (search " " cmd)) (search "." cmd)) ml4pg-theorems_id)
- (cdr (assoc (subseq cmd (+ 1 (search " " cmd)) (search "." cmd)) ml4pg-theorems_id))
- (if (ml4pg-search-in-hyp (subseq cmd (+ 1 (search " " cmd)) (search "." cmd)) ml4pg-hypothesis)
- 1
- (progn (setf ml4pg-start (+ ml4pg-start ml4pg-add_to))
- (ml4pg-save-lemma (subseq cmd (+ 1 (search " " cmd)) (search "." cmd)) ml4pg-start)
- (setf ml4pg-theorems_id
- (append ml4pg-theorems_id (list (cons (subseq cmd (+ 1 (search " " cmd)) (search "." cmd))
- ml4pg-start))))
- (setf ml4pg-add_to (/ ml4pg-add_to 2))
- ml4pg-start
- ))))))
-
-
-(defun ml4pg-arg-induction (object)
- (let* ((ps0 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (res (proof-shell-invisible-cmd-get-result (concat "Check " object)))
- (ps3 (proof-shell-invisible-cmd-get-result (concat "induction " object)))
- (err (search "Error" res)))
- (if err -1 1)))
-
-(defun ml4pg-get-type-id-induction (object arg-ind)
- (if (equal arg-ind 1)
- (let ((ps0 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (gt (ml4pg-get-type-id object))
- (ps3 (proof-shell-invisible-cmd-get-result (concat "induction " object))))
- gt)
- (let ((ps0 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (ps (proof-shell-invisible-cmd-get-result (concat "intro " object)))
- (gt (ml4pg-get-type-id object))
- (ps2 (proof-shell-invisible-cmd-get-result (format "Undo")))
- (ps3 (proof-shell-invisible-cmd-get-result (concat "induction " object))))
- gt)))
-
-;; Function to add the information to the corresponding tree depth level
-
-(defun ml4pg-add-info-to-tree (info level)
- (cond ((= ml4pg-level 1) (setf ml4pg-tdl1 (append ml4pg-tdl1 (list info))))
- ((= ml4pg-level 2) (setf ml4pg-tdl2 (append ml4pg-tdl2 (list info))))
- ((= ml4pg-level 3) (setf ml4pg-tdl3 (append ml4pg-tdl3 (list info))))
- ((= ml4pg-level 4) (setf ml4pg-tdl4 (append ml4pg-tdl4 (list info))))
- ((= ml4pg-level 5) (setf ml4pg-tdl5 (append ml4pg-tdl5 (list info))))
- (t nil)))
-
-;; Function to add the information to the corresponding tactic
-
-(defun ml4pg-add-info-to-tactic (info tactic)
- (cond ((string= ml4pg-tactic "intro") (setf ml4pg-intro (append ml4pg-intro (list info))))
- ((string= ml4pg-tactic "case") (setf ml4pg-case (append ml4pg-case (list info))))
- ((string= ml4pg-tactic "simpltrivial") (setf ml4pg-simpltrivial (append ml4pg-simpltrivial (list info))))
- ((string= ml4pg-tactic "induction") (setf ml4pg-induction (append ml4pg-induction (list info))))
- ((string= ml4pg-tactic "simpl") (setf ml4pg-simpl (append ml4pg-simpl (list info))))
- ((string= ml4pg-tactic "rewrite") (setf ml4pg-rewrite (append ml4pg-rewrite (list info))))
- ((string= ml4pg-tactic "trivial") (setf ml4pg-trivial (append ml4pg-trivial (list info))))
- (t nil)))
-
-
-
-;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 tactic ngs ts current-level bot)
- (cond ((and (string= tactic "intro") (not (string= cmd "intro.")))
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (type (ml4pg-get-type-id object))
-
-
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis (list object))))
- (res (list (cdr (assoc "intro" ml4pg-tactic_id))
- 1
- type
- -1
- ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "intro")
- (let* ((type (ml4pg-get-obj-intro))
-
-
- (res (list (cdr (assoc "intro" ml4pg-tactic_id))
- 1
- (ml4pg-get-obj-intro)
- -1
- ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((and (string= tactic "intros") (not (string= cmd "intros.")))
- (let* ((params (ml4pg-get-obj-intros2 (subseq cmd (1+ (search " " cmd)))))
- (nparams (car params))
- (types-params (cadr params))
- (len (caddr params))
- (gts (cadddr params))
-
-
- (res (list nparams
- len
- types-params
- -1
- gts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "intros")
- (let* ((params (ml4pg-get-obj-intros))
- (nparams (car params))
- (types-params (cadr params))
- (len (caddr params))
- (gts (cadddr params))
-
-
- (res (list nparams
- len
- types-params
- -1
- gts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "case")
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (type (ml4pg-get-type-id object))
-
-
- (res (list (cdr (assoc "case" ml4pg-tactic_id))
- 1
- type
- 1 ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "simpl")
- (progn
-
- (setf ml4pg-goal-level-temp (cons (list (cdr (assoc "simpl" ml4pg-tactic_id)) 1 0 0 ts ngs) ml4pg-goal-level-temp))
- (list (cdr (assoc "simpl" ml4pg-tactic_id)) 1 0 0 ts ngs)))
- ((string= tactic "trivial")
- (progn
-
- (setf ml4pg-goal-level-temp (cons (list (cdr (assoc "trivial" ml4pg-tactic_id)) 1 0 0 ts ngs) ml4pg-goal-level-temp))
- (list (cdr (assoc "trivial" ml4pg-tactic_id)) 1 0 0 ts ngs)))
- ((string= tactic "induction")
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (arg-ind (ml4pg-arg-induction object))
- (type (ml4pg-get-type-id-induction object arg-ind))
-
-
- (ih (setf ml4pg-theorems_id (append ml4pg-theorems_id (list (cons (concat "IH" object) 10)))))
- (res (list (cdr (assoc "induction" ml4pg-tactic_id))
- 1 type arg-ind ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "rewrite")
- (progn
-
- (setf ml4pg-goal-level-temp (cons (list (cdr (assoc "rewrite" ml4pg-tactic_id)) 1 -4
- (ml4pg-extract-theorem-id cmd) ts ngs) ml4pg-goal-level-temp))
- (list (cdr (assoc "rewrite" ml4pg-tactic_id)) 1 -4
- (ml4pg-extract-theorem-id cmd) ts ngs))
- )
- ((string= cmd "simpl; trivial.")
- (progn
-
- (setf goal-level-temp (cons (list (cdr (assoc "simpl; trivial" ml4pg-tactic_id)) 2 0 0 ts ngs) ml4pg-goal-level-temp))
- (list (cdr (assoc "simpl; trivial" ml4pg-tactic_id)) 2 0 0 ts ngs))
- )))
-
-;; Function to obtain the information just about the goals.
-
-(defun ml4pg-get-numbers2 (cmd tactic ngs ts current-level bot)
- (cond ((and (string= tactic "intro") (not (string= cmd "intro.")))
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (type (ml4pg-get-type-id object))
-
-
- (foo (setf ml4pg-hypothesis (append ml4pg-hypothesis (list object))))
- (res (list (cdr (assoc "intro" ml4pg-tactic_id))
- 1
- type
- -1
- ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "intro")
- (let* ((type (ml4pg-get-obj-intro))
-
-
- (res (list (cdr (assoc "intro" ml4pg-tactic_id))
- 1
- (get-obj-intro)
- -1
- ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((and (string= tactic "intros") (not (string= cmd "intros.")))
- (let* ((params (ml4pg-get-obj-intros2 (subseq cmd (1+ (search " " cmd)))))
- (nparams (car params))
- (types-params (cadr params))
- (len (caddr params))
- (gts (cadddr params))
-
-
- (res (list nparams
- len
- types-params
- -1
- gts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "intros")
- (let* ((params (ml4pg-get-obj-intros))
- (nparams (car params))
- (types-params (cadr params))
- (len (caddr params))
- (gts (cadddr params))
-
-
- (res (list nparams
- len
- types-params
- -1
- gts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "case")
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (type (ml4pg-get-type-id object))
-
-
- (res (list (cdr (assoc "case" ml4pg-tactic_id))
- 1
- type
- 1 ts ngs))
- (foo2 (setf ml4pg-goal-level-temp (cons res ml4pg-goal-level-temp))))
- res))
- ((string= tactic "simpl")
- (progn
-
- (list (cdr (assoc "simpl" ml4pg-tactic_id)) 1 0 0 ts ngs)))
- ((string= tactic "trivial")
- (progn
-
- (list (cdr (assoc "trivial" ml4pg-tactic_id)) 1 0 0 ts ngs)))
- ((string= tactic "induction")
- (let* ((object (subseq cmd (1+ (search " " cmd)) (search "." cmd)))
- (arg-ind (ml4pg-arg-induction object))
- (type (ml4pg-get-type-id-induction object arg-ind))
-
-
- (ih (setf ml4pg-theorems_id (append ml4pg-theorems_id (list (cons (concat "IH" object) 10)))))
- (res (list (cdr (assoc "induction" ml4pg-tactic_id))
- 1 type arg-ind ts ngs))
- (foo2 (setf goal-level-temp (cons res goal-level-temp))))
- res))
- ((string= tactic "rewrite")
- (progn
-
- (list (cdr (assoc "rewrite" ml4pg-tactic_id)) 1 -4
- (ml4pg-extract-theorem-id cmd) ts ngs))
- )
- ((string= cmd "simpl; trivial.")
- (progn
-
- (list (cdr (assoc "simpl; trivial" ml4pg-tactic_id)) 2 0 0 ts ngs))
- )))
-
-(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 proof tree level
-
-(defun ml4pg-remove-zeros (n)
- (do ((temp n (/ temp 10)))
- ((or (= temp 0) (not (= (mod temp 10) 0))) temp)))
-
-(defun ml4pg-obtain-level (level n)
- (do ((temp (cdr level) (cdr temp))
- (temp2 (if (endp level) (list 0 0 0 0 0 0 0 0 0)
- (list (* (nth 0 (car level)) (expt 10 (length (cdr level))))
- (* (nth 1 (car level)) (expt 10 (length (cdr level))))
- (* (nth 2 (car level)) (expt 10 (length (cdr level))))
- (* (nth 3 (car level)) (expt 10 (length (cdr level))))
- (* (nth 4 (car level)) (expt 10 (length (cdr level))))
- (* (nth 5 (car level)) (expt 10 (length (cdr level))))
- (* (nth 6 (car level)) (expt 10 (length (cdr level))))
- (* (nth 7 (car level)) (expt 10 (length (cdr level))))
- (nth 8 (car level))))))
- ((endp temp) (list (ml4pg-remove-zeros (nth 0 temp2))
- (ml4pg-remove-zeros (nth 1 temp2))
- (ml4pg-remove-zeros (nth 2 temp2))
- (ml4pg-remove-zeros (nth 3 temp2))
- (ml4pg-remove-zeros (nth 4 temp2))
- (nth 5 temp2)
- (ml4pg-remove-zeros (nth 6 temp2))
- (if (= (nth 7 temp2) 0) (nth 7 temp2) (+ (* n (expt 10 (length level))) (ml4pg-remove-zeros (nth 7 temp2))))
- (nth 8 temp2)))
- (setf temp2 (list (+ (nth 0 temp2) (* (expt 10 (length (cdr temp))) (nth 0 (car temp))))
- (+ (nth 1 temp2) (* (expt 10 (length (cdr temp))) (nth 1 (car temp))))
- (+ (nth 2 temp2) (* (expt 10 (length (cdr temp))) (nth 2 (car temp))))
- (+ (nth 3 temp2) (* (expt 10 (length (cdr temp))) (nth 3 (car temp))))
- (+ (nth 4 temp2) (* (expt 10 (length (cdr temp))) (nth 4 (car temp))))
- (+ (nth 5 temp2) (* (expt 10 (length (cdr temp))) (nth 5 (car temp))))
- (+ (nth 6 temp2) (* (expt 10 (length (cdr temp))) (nth 6 (car temp))))
- (+ (nth 7 temp2) (* (expt 10 (length (cdr temp))) (nth 7 (car temp))))
- (+ (nth 8 temp2) (nth 8 (car temp))))
- )
- ))
-
-
-(defun ml4pg-compute-proof-result ()
- (append (ml4pg-obtain-level ml4pg-tdl1 1)
- (ml4pg-obtain-level ml4pg-tdl2 2)
- (ml4pg-obtain-level ml4pg-tdl3 3)
- (ml4pg-obtain-level ml4pg-tdl4 4)
- (ml4pg-obtain-level ml4pg-tdl5 5)))
-
-;; 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))))
- )
- ))
-
-
-(defun ml4pg-compute-tactic-result ()
- (append (ml4pg-obtain-tactic-result ml4pg-intro)
- (ml4pg-obtain-tactic-result ml4pg-case)
- (ml4pg-obtain-tactic-result ml4pg-simpltrivial)
- (ml4pg-obtain-tactic-result ml4pg-induction)
- (ml4pg-obtain-tactic-result ml4pg-simpl)
- (ml4pg-obtain-tactic-result ml4pg-rewrite)
- (ml4pg-obtain-tactic-result ml4pg-trivial)))
-
-
-(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"))
-
-(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-export-theorem-aux (result name current-level dot-level)
- (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 current-level dot-level)))
- ((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))))
- current-level dot-level)))
- ((search "Proof" cmd)
- (progn (proof-assert-next-command-interactive)
- (ml4pg-export-theorem-aux result name current-level dot-level)))
- ((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))))
- current-level dot-level)))
- ((search "Qed." cmd)
- (progn (proof-assert-next-command-interactive)
- ; (insert (format "\n(* %s *)\n" (reverse result)))
- (setf ml4pg-proof-tree-level (append ml4pg-proof-tree-level (list (ml4pg-compute-proof-result))))
- (setf ml4pg-tactic-level (append ml4pg-tactic-level (list (ml4pg-compute-tactic-result))))
- (setf ml4pg-saved-theorems (append ml4pg-saved-theorems
- (list (list name (ml4pg-flat (reverse result))))))))
- (pos_space
- (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))
- (cond ((< ng ng2) (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 1) result)
- name
- (1+ current-level)
- (1+ current-level)))
- ((< ng2 ng) (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 0) result)
- name
- dot-level
- nil))
- (t (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 0) result)
- name
- (1+ current-level)
- dot-level)))))
- (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))
- (cond ((< ng ng2) (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 1) result)
- name
- (1+ current-level)
- (1+ current-level)))
- ((< ng2 ng) (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 0) result)
- name
- dot-level
- nil))
- (t (ml4pg-export-theorem-aux
- (cons (ml4pg-get-numbers cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 0) result)
- name
- (1+ current-level)
- dot-level))
- )
- ))))))
-
-
-
-
-
-;;; 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 "_proof_tree.csv") (insert (ml4pg-extract-features-2 proof-tree-level)))
- (with-temp-file (concat file "_tactic.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 (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-extract-features-1 ()
- (let ((fm (ml4pg-find-max-length)))
- (do ((temp ml4pg-saved-theorems (cdr temp))
- (temp2 ""))
- ((endp temp) temp2)
- (if (< (length (cadar temp)) fm)
- (setf temp2 (concat temp2
- (format "%s\n"
- (ml4pg-print-list (ml4pg-take-30 (append (cadar temp)
- (ml4pg-generate-zeros (- fm (length (cadar temp)))))) ))))
- (setf temp2 (concat temp2 (format "%s\n" (ml4pg-print-list (ml4pg-take-30 (cadar temp))) )))))
- ))
-
-
-
-(defun ml4pg-extract-features-2 (list)
- (do ((temp 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
-
-(defun ml4pg-extract-info-up-to-here ()
- (interactive)
- (setf ml4pg-tdl1 nil
- ml4pg-tdl2 nil
- ml4pg-tdl3 nil
- ml4pg-tdl4 nil
- ml4pg-tdl5 nil
- ml4pg-intro nil
- ml4pg-case nil
- ml4pg-simpltrivial nil
- ml4pg-induction nil
- ml4pg-simpl nil
- ml4pg-rewrite nil
- ml4pg-trivial nil)
- (let ((final (point))
- (result nil)
- (current-level 1))
- (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))
- (pos_dot (search "." cmd))
- (pos_space (search " " cmd))
- (ts nil))
- (cond (pos_space
- (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))
- (cond ((< ng ng2) (progn (setf result (cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 1) result))
- (setf current-level (1+ current-level))))
- ((< ng2 ng) (progn (setf result (cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 0) result))
- (setf current-level (1+ current-level))))
- (t (progn (setf result (cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_space) (ml4pg-get-number-of-goals) ts current-level 0) result))
- (setf current-level (1+ current-level)))))))
- (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))
- (cond ((< ng ng2) (progn (setf result (cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 1) result))
- (setf current-level (1+ current-level))))
- ((< ng2 ng) (progn (setf result (cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 0) result))
- (setf current-level (1+ current-level))))
- (t (progn (setf result(cons (ml4pg-get-numbers2 cmd (subseq cmd 0 pos_dot) (ml4pg-get-number-of-goals) ts current-level 0) result) )
- (setf current-level (1+ current-level))))
- )
- ))))
- )
-
-
- (ml4pg-take-30 (append (ml4pg-flat (reverse result)) (ml4pg-generate-zeros 20) ))
- ))
-
-
-
-(defun ml4pg-extract-features-1-bis (thm)
- (let ((fm (ml4pg-find-max-length)))
- (do ((temp ml4pg-saved-theorems (cdr temp))
- (temp2 ""))
- ((endp temp) (concat temp2 (format "%s\n" (ml4pg-print-list thm))))
- (if (< (length (cadar temp)) fm)
- (setf temp2 (concat temp2
- (format "%s\n"
- (ml4pg-print-list (ml4pg-take-30 (append (cadar temp)
- (ml4pg-generate-zeros (- fm (length (cadar temp)))))) ))))
- (setf temp2 (concat temp2 (format "%s\n" (ml4pg-print-list (ml4pg-take-30 (cadar 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)))
- )
-
- )
-
-
-
- \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 08:48:41 +0000