From c559e23692bb561b4a52622c9ba8d3661b15ebe6 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Fri, 11 May 2007 09:23:20 +0000 Subject: Renamed file --- isar/isar-find-theorems.el | 481 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 481 insertions(+) create mode 100644 isar/isar-find-theorems.el (limited to 'isar/isar-find-theorems.el') diff --git a/isar/isar-find-theorems.el b/isar/isar-find-theorems.el new file mode 100644 index 00000000..beeb4905 --- /dev/null +++ b/isar/isar-find-theorems.el @@ -0,0 +1,481 @@ +;; isar-find-theorems.el A search form for Isabelle's find_theorems command. +;; +;; Copyright (C) 2007 Tjark Weber +;; +;; This program is free software; you can redistribute it and/or +;; modify it under the terms of the GNU General Public License +;; as published by the Free Software Foundation; either version 2 +;; of the License, or (at your option) any later version. +;; +;; $Id$ +;; + +;; make the original (minibuffer based) "Find theorems" command (from +;; ../generic/pg-user.el) available as isar-find-theorems-minibuffer; +;; return '(nil) so that isar-find-theorems-minibuffer works as a +;; value for isar-find-theorems-command + +(defun isar-find-theorems-minibuffer () + "Search for items containing given constants (using the minibuffer)." + (interactive) + (let ((isar-find-theorems-command "find_theorems %s")) + (call-interactively 'isar-find-theorems)) + '(nil)) + +;; isar-find-theorems-form (just like isar-find-theorems-minibuffer) can be +;; called interactively, and can be used as a value for +;; isar-find-theorems-command (returning '(nil) means that the actual +;; "find_theorems" command will NOT be issued to Isabelle by +;; isar-find-theorems in this case, but only later on by a handler function +;; for the form's "Find" button) + +(defun isar-find-theorems-form () + "Search for items containing given constants (using a search form)." + (interactive) + (apply 'isar-find-theorems-create-searchform isar-find-theorems-data) + '(nil)) + +;; update the universal key bindings (see ../generic/proof-config.el) +;; +;; C-c C-a C-m is bound to isar-find-theorems-minibuffer +;; C-c C-a C-f is bound to isar-find-theorems-form +;; +;; Note that C-c C-a C-f, although C-c C-a usually invokes the prover +;; assistant specific keymap, is defined as a universal key binding here. +;; This way it will be available in the same buffers as C-c C-f. + +(setq proof-universal-keys + (cons + '([(control c) (control a) (control m)] . isar-find-theorems-minibuffer) + (cons + '([(control c) (control a) (control f)] . isar-find-theorems-form) + proof-universal-keys))) + +;; Documentation, taken from isabelle/NEWS: +;; +;; * Command 'find_theorems' searches for a list of criteria instead of a +;; list of constants. Known criteria are: intro, elim, dest, name:string, +;; simp:term, and any term. Criteria can be preceded by '-' to select +;; theorems that do not match. Intro, elim, dest select theorems that +;; match the current goal, name:s selects theorems whose fully qualified +;; name contain s, and simp:term selects all simplification rules whose +;; lhs match term. Any other term is interpreted as pattern and selects +;; all theorems matching the pattern. Available in ProofGeneral under +;; 'ProofGeneral -> Find Theorems' or C-c C-f. Example: +;; +;; C-c C-f (100) "(_::nat) + _ + _" intro -name: "HOL." +;; +;; prints the last 100 theorems matching the pattern "(_::nat) + _ + _", +;; matching the current goal as introduction rule and not having "HOL." +;; in their name (i.e. not being defined in theory HOL). + +;; search form field values + +(defvar isar-find-theorems-data (list + "" ;; num + "" ;; pattern + "none" ;; intro + "none" ;; elim + "none" ;; dest + "" ;; name + "" ;; simp + ) + "Values of the Find Theorems search form's fields.") + +;; search form widgets (set in isar-find-theorems-create-searchform +;; and accessed in the "Find" handler) + +(defvar isar-find-theorems-widget-number nil + "Search form widget for the number of theorems.") + +(defvar isar-find-theorems-widget-pattern nil + "Search form widget for search patterns.") + +(defvar isar-find-theorems-widget-intro nil + "Search form widget for intro rules.") + +(defvar isar-find-theorems-widget-elim nil + "Search form widget for elim rules.") + +(defvar isar-find-theorems-widget-dest nil + "Search form widget for dest rules.") + +(defvar isar-find-theorems-widget-name nil + "Search form widget for theorem names.") + +(defvar isar-find-theorems-widget-simp nil + "Search form widget for simplification rules.") + +;; creates (or switches to) the search form buffer + +(defun isar-find-theorems-create-searchform + (num pattern intro elim dest name simp &optional errmsg) + "Create (or switch to) the Find Theorems search form buffer." + + (if (get-buffer "*Find Theorems*") + (switch-to-buffer "*Find Theorems*") + + ;; create a new search form + + (switch-to-buffer "*Find Theorems*") + + (widget-insert + (concat "\n " (propertize "Find Theorems" + 'face (list :height 200 :weight 'extra-bold)) + "\n\n")) + + ;; pattern + (widget-insert " Search pattern: ") + (setq isar-find-theorems-widget-pattern (widget-create 'editable-field + :size 50 + :help-echo "A pattern to match in the theorem." + pattern)) + (widget-insert " ") + (widget-create 'push-button + :help-echo "Click for help." + :notify (lambda (&rest ignore) (isar-find-theorems-create-help)) + "?") + + ;; name + (widget-insert "\n\n Theorem name: ") + (setq isar-find-theorems-widget-name (widget-create 'editable-field + :size 50 + :help-echo "Part of the theorem's name." + name)) + (widget-insert " ") + (widget-create 'push-button + :help-echo "Click for help." + :notify (lambda (&rest ignore) (isar-find-theorems-create-help)) + "?") + + ;; intro + (widget-insert "\n\n Rules matching the current goal: ") + (widget-create 'push-button + :help-echo "Click for help." + :notify (lambda (&rest ignore) (isar-find-theorems-create-help)) + "?") + (widget-insert "\n\n INTRO:\n ") + (setq isar-find-theorems-widget-intro (widget-create 'radio-button-choice + :value intro + :indent 6 + :button-args (list :help-echo "Click to select one option.") + '(item "none") '(item "intro") '(item "-intro"))) + + ;; elim + (widget-insert "\n ELIM:\n ") + (setq isar-find-theorems-widget-elim (widget-create 'radio-button-choice + :value elim + :indent 6 + :button-args (list :help-echo "Click to select one option.") + '(item "none") '(item "elim") '(item "-elim"))) + + ;; dest + (widget-insert "\n DEST:\n ") + (setq isar-find-theorems-widget-dest (widget-create 'radio-button-choice + :value dest + :indent 6 + :button-args (list :help-echo "Click to select one option.") + '(item "none") '(item "dest") '(item "-dest"))) + + ;; simp + (widget-insert "\n Simplification pattern: ") + (setq isar-find-theorems-widget-simp (widget-create 'editable-field + :size 42 + :help-echo + "A pattern to match in the left-hand side of a simplification rule." + simp)) + (widget-insert " ") + (widget-create 'push-button + :help-echo "Click for help." + :notify (lambda (&rest ignore) (isar-find-theorems-create-help)) + "?") + + ;; num + (widget-insert "\n\n Number of results: ") + (setq isar-find-theorems-widget-number (widget-create 'editable-field + :size 10 + :help-echo "Maximum number of results to be displayed." + num)) + (widget-insert " ") + (widget-create 'push-button + :help-echo "Click for help." + :notify (lambda (&rest ignore) (isar-find-theorems-create-help)) + "?") + + ;; Find + (widget-insert "\n\n ") + (widget-create 'push-button + :help-echo "Click to submit this form." + :notify (lambda (&rest ignore) + (let ((num (widget-value isar-find-theorems-widget-number)) + (pattern (widget-value isar-find-theorems-widget-pattern)) + (intro (widget-value isar-find-theorems-widget-intro)) + (elim (widget-value isar-find-theorems-widget-elim)) + (dest (widget-value isar-find-theorems-widget-dest)) + (name (widget-value isar-find-theorems-widget-name)) + (simp (widget-value isar-find-theorems-widget-simp))) + (kill-buffer "*Find Theorems*") + (isar-find-theorems-submit-searchform + num pattern intro elim dest name simp))) + "Find") + + ;; Reset form + (widget-insert " ") + (widget-create 'push-button + :help-echo "Click to reset this form." + :notify (lambda (&rest ignore) + (kill-buffer "*Find Theorems*") + (isar-find-theorems-create-searchform + "" "" "none" "none" "none" "" "")) + "Reset Form") + (widget-insert "\n") + + ;; errmsg + (if errmsg + (widget-insert (concat "\n " (propertize + (concat errmsg "\n See help for details.") + 'face (list :foreground "red")) "\n"))) + + (use-local-map widget-keymap) + (widget-setup) + + (goto-char 37)) ;; beginning of the "Search pattern" text field +) + +;; creates the search form help buffer + +(defun isar-find-theorems-create-help () + "Create a help text buffer for the Find Theorems search form." + + (with-output-to-temp-buffer "*Find Theorems - Help*" + (princ (concat + "\n" + "*** Find Theorems - Help ***\n" + "\n" + "Command \"Find Theorems\" (C-c C-f) searches for theorems that satisfy a list of\n" + "user-supplied criteria. Known criteria are:\n" + "\n" + "* Search pattern: a pattern that occurs in the theorem, e.g. \"(_::nat) + _\".\n" + "\n" + "* Theorem name: a substring of the theorem's fully qualified name. (Treats \"*\"\n" + " as a wildcard character.)\n" + "\n" + "* Intro, Elim, Dest: select theorems that match the current goal as\n" + " introduction/elimination/destruction rule.\n" + "\n" + "* Simplification pattern: selects simplification rules whose left-hand side\n" + " matches the given pattern.\n" + "\n" + "* Number of results: an upper bound on the number of theorems that are\n" + " displayed. (Leave empty to use Isabelle's default value.)\n" + "\n" + "Multiple search patterns, theorem names and simplification patterns can be\n" + "given, separated by spaces. (Patterns containing a space must be enclosed in\n" + "double-quotes.) Criteria can be preceded by \"-\" to select theorems that do not.\n" + "match. (Patterns that begin with a \"-\" must be enclosed in double-quotes.)\n" + "\n" + "A minibuffer based \"Find Theorems\" command is available via (C-c C-a C-m). See\n" + "the Isabelle NEWS file for up-to-date documentation. A search form is available\n" + "via (C-c C-a C-f). Variable isar-find-theorems-command (customizable via\n" + "Proof-General > Advanced > Internals > Prover Config) controls the default\n" + "behavior of the \"Find Theorems\" command: set to isar-find-theorems-form or\n" + "isar-find-theorems-minibuffer.\n" + ))) +) + +;; parses the search form's data and calls isar-find-theorems +;; with an appropriate argument string, or displays the search +;; form again, but with an error message + +(defun isar-find-theorems-submit-searchform + (num pattern intro elim dest name simp) + "Parse the Find Theorems search form's data." + + (let (num_ pattern_ intro_ elim_ dest_ name_ simp_ searchstring) + + ;; pattern + (setq pattern_ (isar-find-theorems-parse-criteria "" pattern)) + + (if (not (pop pattern_)) + (isar-find-theorems-create-searchform + num pattern intro elim dest name simp + (concat "Invalid search pattern: " (car pattern_))) + + (setq pattern_ (car pattern_)) + + ;; name + (setq name_ (isar-find-theorems-parse-criteria "name: " name)) + + (if (not (pop name_)) + (isar-find-theorems-create-searchform + num pattern intro elim dest name simp + (concat "Invalid theorem name: " (car name_))) + + (setq name_ (car name_)) + + ;; simp + (setq simp_ (isar-find-theorems-parse-criteria "simp: " simp)) + + (if (not (pop simp_)) + (isar-find-theorems-create-searchform + num pattern intro elim dest name simp + (concat "Invalid simplification pattern: " (car simp_))) + + (setq simp_ (car simp_)) + + ;; num + (setq num_ (isar-find-theorems-parse-number num)) + + (if (not num_) + (isar-find-theorems-create-searchform + num pattern intro elim dest name simp + "Number of results must be a positive integer.") + + ;; intro + (setq intro_ (if (equal intro "none") "" intro)) + + ;; elim + (setq elim_ (if (equal elim "none") "" elim)) + + ;; dest + (setq dest_ (if (equal dest "none") "" dest)) + + ;; success: save data, call isar-find-theorems + (setq isar-find-theorems-data + (list num pattern intro elim dest name simp)) + + (setq searchstring (format "find_theorems %s" + (mapconcat 'identity + (isar-find-theorems-filter-empty + (list num_ pattern_ intro_ elim_ dest_ name_ simp_)) + " "))) + + ;; note that isar-find-theorems with an argument provided + ;; will merely pass this on to Isabelle, and NOT display + ;; the search form again + (isar-find-theorems searchstring)))))) +) + +;; "Multiple search patterns, theorem names and simplification terms can be +;; given, separated by spaces. (Patterns containing a space must be enclosed +;; in double-quotes.) Criteria can be preceded by "-" to select theorems that +;; do not match. (Patterns that begin with a "-" must be enclosed in double- +;; quotes.)" +;; +;; returns (t parsed-string) (where parsed-string may be empty) or +;; (nil errmsg) in case of an error + +(defun isar-find-theorems-parse-criteria (option-string criteria-string) + "Parse search patterns/theorem names/simplification terms, +separated by \" \", possibly preceded by \"-\", and possibly +escaped by double-quotes." + + ;; This code might benefit greatly from the use of regexps. + + (let ((tokens nil) (errmsg nil)) + + ;; turn criteria-string into a list of (string) tokens + (while (and (not (equal criteria-string "")) (not errmsg)) + + ;; ignore space + (if (equal (elt criteria-string 0) ?\ ) + (setq criteria-string (substring criteria-string 1)) + + ;; - is a token + ;; Note: This is still a bit weird, as it treats a - following a - + ;; just like the first -, i.e. not as part of a pattern. Oh + ;; well. + (if (equal (elt criteria-string 0) ?-) + (progn + (setq tokens (cons "-" tokens)) + (setq criteria-string (substring criteria-string 1))) + + ;; " starts a token: search for the next ", regard as one token + ;; Note: This is still a bit weird, as it does not require the + ;; closing double-quotes to be followed by a space. Oh well. + (if (equal (elt criteria-string 0) ?\") + (let ((i 1)) + (while (and (< i (length criteria-string)) + (not (equal (elt criteria-string i) ?\"))) + (setq i (1+ i))) + (if (equal i (length criteria-string)) + (setq errmsg "missing closing double-quotes.") + (setq i (1+ i)) + (setq tokens (cons (substring criteria-string 0 i) tokens)) + (setq criteria-string (substring criteria-string i)))) + + ;; everything else: search for the next space, regard as one token + ;; Note: This is still a bit weird, as it scans over double-quotes. + ;; Oh well. + (let ((i 1)) + (while (and (< i (length criteria-string)) + (not (equal (elt criteria-string i) ?\ ))) + (setq i (1+ i))) + (setq tokens (cons (substring criteria-string 0 i) tokens)) + (setq criteria-string (substring criteria-string i))) + ))) + ) + + (if errmsg + (list nil errmsg) + + (setq tokens (nreverse tokens)) + + ;; convert the tokens into argument strings; make sure every "-" is + ;; followed by a pattern/name (i.e. not by another "-") + (let ((strings nil) (negated nil)) + + (while (and tokens (not errmsg)) + (let ((token (car tokens))) + (if (equal token "-") + (if negated + (setq errmsg "- may not be followed by another -.") + (setq negated t) + (setq tokens (cdr tokens))) + (setq strings (cons + (concat (if negated "-" "") option-string + ;; wrap token in double-quotes if necessary + (if (equal (elt token 0) ?\") token (concat "\"" token "\""))) + strings)) + (setq negated nil) + (setq tokens (cdr tokens)))) + ) + + (if errmsg + (list nil errmsg) + + (if negated + (list nil "- must be followed by a search criterion.") + + (setq strings (nreverse strings)) + + (list t (mapconcat 'identity strings " ")) + ))))) +) + +;; auxiliary functions + +;; returns "" if num is "", "(num)" if num is a string encoding a positive +;; integer, and nil otherwise + +(defun isar-find-theorems-parse-number (num) + "Parse the number of theorems to be displayed." + (if (equal num "") + "" + (let ((numval (string-to-number num))) + (if (and (wholenump numval) (not (equal numval 0))) + (concat "(" (number-to-string numval) ")") + nil))) +) + +(defun isar-find-theorems-filter-empty (strings) + "Build a new list by removing empty strings from a (non-circular) list." + (if (not strings) + nil + (if (equal (car strings) "") + (isar-find-theorems-filter-empty (cdr strings)) + (cons (car strings) + (isar-find-theorems-filter-empty (cdr strings))))) +) + +(provide 'isar-find-theorems) -- cgit v1.2.3