functions for manipulating theorem dependencies

1 files changed, 113 insertions, 0 deletions

diff --git a/generic/proof-depends.el b/generic/proof-depends.el
new file mode 100644
index 00000000..cd495e41
--- /dev/null
+++ b/generic/proof-depends.el
@@ -0,0 +1,113 @@
+;;here is the code to return a list of all the dependencies
+
+;;FIXME: doesn't even slightly work.  First prob is that span-at does not return a span, only nil.  Therefore cannot test the rest of the code as just fails at this point.
+
+(defun make-dependency-list (file)
+  (make-deps-list '() (span-at (point-min file) 'dependencies) (point-max file)))
+(defun make-deps-list (list span end-point)
+  (if (eql (span-end span) end-point)
+      (append list (span-property span 'dependencies))
+   (make-deps-list (append list (span-property span 'dependencies)) (next-span span 'dependencies) end-point)))
+
+(defun mytest ()
+  (save-excursion
+   (set-buffer proof-script-buffer)
+   (span-at (point-min) 'type)))
+
+(defun find-span (buffer)
+  (save-excursion
+    (set-buffer buffer)
+    (span-at (point-min) 'type)))
+
+(span-property (find-span "loading.ML") 'type)
+
+
+
+(find-span "loading.ML")
+
+(defun find-next-span (buffer span)
+  (save-excursion
+    (set-buffer buffer)
+    (next-span span 'type)))
+
+(span-property (find-next-span "loading.ML" (find-span "loading.ML")) 'dependencies)
+
+
+
+
+;; this is code to add dependency info to files not read through the interface.
+
+;;some testing for matching stuff
+
+So ... one idea is: find out where the message starts, move on x nos of steps from there and then return everything between that place and where we find val it = ().
+
+So ... what buffer is this in?   - response buffer
+
+(let ((proof-last-theorem-dependencies 
+(string-match proof-shell-theorem-dependency-list-regexp message)
+
+(setq p-s-t-d-l-r "Proof General, the theorem dependencies are: ")
+
+(goto-char (+ 45 (string-match p-s-t-d-l-r messq)) (get-buffer "empty"))
+;;this returns 60
+(search-forward "val it" nil nil nil (get-buffer "empty"))
+;;this returns 217
+
+;;so we know that all the information we want is contained in the buffer "empty" between lines 61 and 217.
+
+(car (setq lala (read-from-string "blah blah blah Proof General, the theorem dependencies are: (ProtoPure.rev_triv_goal Protopure.triv_goal HOL.TrueI ProtoPure.rev_triv_goal ProtoPure.triv_goal ProtoPure.revcut_rl HOL.subst loading.even_Suc_Suc) 
+val it = () : unit
+
+this is a file with lots of stuff in it so that I can practice
+searching and see what happens 
+
+lots of fun la di la" 60)))
+
+(read-from-string "A short string" 0 10)
+
+(setq noodle (buffer-string (point-min "*isabelle*") (point-max "*isabelle*") (get-buffer "*isabelle*")))
+
+(read-from-string noodle (goto-char (+ 45 (string-match p-s-t-d-l-r noodle)) "*isabelle*"))
+
+(get-buffer "*isabelle*")
+
+
+(save-excursion
+  (set-buffer "*isabelle*")
+  (end-of-buffer)
+  (search-backward p-s-t-d-l-r)
+  (setq beginning (+ 47 (point)))
+  (search-forward "val it")
+  (buffer-string beginning (- (point) 10)))
+
+
+(setq messq "blah blah blah Proof General, the theorem dependencies are: ProtoPure.rev_triv_goal ProtoPure.triv_goal HOL.TrueI ProtoPure.rev_triv_goal ProtoPure.triv_goal ProtoPure.revcut_rl HOL.subst loading.even_Suc_Suc 
+val it = () : unit")
+
+
+
+
+
+
+
+
+
+
+
+
+
+;;sort-deps-list will sort through the list of dependencies and return all those that are not either Protopure or HOL - i.e. will return only those theorems that are written within the file and subject to alteration
+
+;;FIXME: check that ProtoPure and HOL are the only cases that need to be checked for.
+
+(defun sort-deps-list (list1)
+  (if (null list1)
+      nil
+    (if (or (string= '"ProtoPure" (substring (prin1-to-string (car list1)) 0 9))
+	    (string= '"HOL" (substring (prin1-to-string (car list1)) 0 3)))
+	(sort-deps-list (cdr list1))
+      (cons (car list1) (sort-deps-list (cdr list1))))))
+
+(sort-deps-list (car lala))
+
+