Added entries in coq menu, rearranged coq menu.

Also added semi-automated setting of local file variables (*** Local
Variables ***) coq-prog-name and coq-prog-args.

2 files changed, 245 insertions, 45 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 3c09968b..ae21a1fb 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -15,15 +15,20 @@
 		("ab" "absurd " holes-abbrev-complete 0)
 		("abs" "absurd " holes-abbrev-complete 0)
 		("ap" "apply " holes-abbrev-complete 16)
+		("argsc" "Arguments Scope @{id} [ @{_} ]" holes-abbrev-complete 4)
 		("as" "assumption" holes-abbrev-complete 4)
 		("ass" "assert ( # : # )" holes-abbrev-complete 4)
 		("au" "auto" holes-abbrev-complete 1)
 		("aw" "auto with " holes-abbrev-complete 1)
 		("awa" "auto with arith" holes-abbrev-complete 4)
 		("c" "cases " holes-abbrev-complete 1)
+		("bndsc" "Bind Scope @{scope} with @{type}" holes-abbrev-complete 1)
 		("ch" "change " holes-abbrev-complete 1)
 		("chi" "change # in #" holes-abbrev-complete 1)
 		("chwi" "change # with # in #" holes-abbrev-complete 1)
+		("cllsc" "Close Local Scope #" holes-abbrev-complete 0)
+		("clsc" "Close Scope #" holes-abbrev-complete 0)
+		("coerc" "Coercion @{id} : @{typ1} >-> @{typ2}." holes-abbrev-complete 3)
 		("con" "constructor" holes-abbrev-complete 3)
 		("cong" "congruence" holes-abbrev-complete 3)
 		("dec" "decompose [#] @{hyp}" holes-abbrev-complete 3)
@@ -32,6 +37,7 @@
 		("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5)
 		("deg" "decide equality" holes-abbrev-complete 3)
+		("delsc" "Delimit Scope @{scope} with @{id}" holes-abbrev-complete 3) 
 		("des" "destruct " holes-abbrev-complete 0)
 		("desu" "destruct # using #" holes-abbrev-complete 0)
 		("desa" "destruct # as #" holes-abbrev-complete 0)
@@ -102,7 +108,9 @@
 		("moi" "Module # : #.\n#\nEnd #." holes-abbrev-complete 0)
 		("moi2" "Module # <: #.\n#\nEnd #." holes-abbrev-complete 0)
 		("nots" "Notation # := #." holes-abbrev-complete 0)
+		("notsp" "Notation # := # (only parsing)." holes-abbrev-complete 0)
 		("notsl" "Notation Local # := #." holes-abbrev-complete 0)
+		("notslp" "Notation Local # := # (only parsing)." holes-abbrev-complete 0)
 		("not" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0)
 		("nota" "Notation \"#\" := # (at level #, # at level #)." holes-abbrev-complete 0)
 		("notas" "Notation \"#\" := # (at level #, # associativity)." holes-abbrev-complete 0)
@@ -110,6 +118,8 @@
 		("notassc" "Notation \"#\" := # (at level #, # associativity) : @{scope}." holes-abbrev-complete 0)
 		("o" "omega" holes-abbrev-complete 0)
 		("om" "omega" holes-abbrev-complete 0)
+		("oplsc" "Open Local Scope #" holes-abbrev-complete 0)
+		("opsc" "Open Scope #" holes-abbrev-complete 0)
 		("p" "Print #" holes-abbrev-complete 3)
 		("po" "pose ( # := # )" nil 0)
 		("pr" "print #" holes-abbrev-complete 2)
@@ -135,6 +145,10 @@
 		("sp" "Split" holes-abbrev-complete 1)
 		("sy" "symmetry" holes-abbrev-complete 0)
 		("sym" "symmetry" holes-abbrev-complete 0)
+		("sprall" "Set Printing All" holes-abbrev-complete 1)
+		("unsprall" "Unset Printing All" holes-abbrev-complete 1)
+		("sprn" "Set Printing Notations" holes-abbrev-complete 1)
+		("unsprn" "Unset Printing Notations" holes-abbrev-complete 1)
 		("t" "trivial" holes-abbrev-complete 1)
 		("tr" "trivial" holes-abbrev-complete 1)
 		("trans" "transitivity #" holes-abbrev-complete 1)
@@ -150,7 +164,30 @@
 ;TODO: build the command submenu automatically from abbrev table
 (defpgdefault menu-entries
   '(
-    ("Insert Command" 
+    ["Print..." coq-Print t]
+    ["Check..." coq-Check t]
+    ["About..." coq-About t]
+    ("OTHER QUERIES"
+     ["Print Hint" coq-PrintHint t]
+     ["Show ith goal..." coq-Show t]
+     ["Show Tree" coq-show-tree t]
+     ["Show Proof" coq-show-proof t]
+     ["Show Conjectures" coq-show-conjectures t] ;; maybe not so useful with editing in PG?
+     ""
+     ["Print..." coq-Print t]
+     ["Check..." coq-Check t]
+     ["About..." coq-About t]
+     ["Search isos/pattern..." coq-SearchIsos t]
+     ["Locate constant..." coq-LocateConstant t]
+     ["Locate Library..." coq-LocateLibrary t]
+     ""
+     ["Locate notation..." coq-LocateNotation t]
+     ["Print Implicit..." coq-Print t]
+     ["Print Scope/Visibility..." coq-PrintScope t]
+     )
+    ["Smart intros" coq-intros t]
+    ["Require/Export/Import" coq-insert-requires t]
+    ("INSERT COMMAND" 
       "COMMAND               ABBREVIATION"
      ["Definition            def<C-BS>" (holes-insert-and-expand "def") t]
      ["Fixpoint              fix<C-BS>" (holes-insert-and-expand "fix") t]
@@ -163,6 +200,7 @@
      ["Inductive4            indv4<C-BS>" (holes-insert-and-expand "indv4") t]
      ""
      ["Section/Module (interactive)..." coq-insert-section-or-module t]
+     ["Require/Export/Import" coq-insert-requires t]
      ""
      ("Modules"
       "COMMAND               ABBREVIATION"
@@ -189,25 +227,46 @@
      )
      ("Schemes"
       "COMMAND               ABBREVIATION"
-      ["Scheme                sc<C-BS>" (holes-insert-and-expand "sc") t]
-      ["Functional Scheme     fs<C-BS>" (holes-insert-and-expand "fs") t]
-      ["Functional Scheme with    fsw<C-BS>" (holes-insert-and-expand "fsw") t]
+      ["Scheme                 sc<C-BS>" (holes-insert-and-expand "sc") t]
+      ["Functional Scheme      fs<C-BS>" (holes-insert-and-expand "fs") t]
+      ["Functional Scheme with fsw<C-BS>" (holes-insert-and-expand "fsw") t]
       )
      ("Notations"
       "COMMAND               ABBREVIATION"
+      ""
+      ["Open Scope                opsc<C-BS>" (holes-insert-and-expand "opsc") t]     
+      ["Open Local Scope          oplsc<C-BS>" (holes-insert-and-expand "oplsc") t]     
+      ["Close Scope               clsc<C-BS>" (holes-insert-and-expand "clsc") t]     
+      ["Open Local Scope          cllsc<C-BS>" (holes-insert-and-expand "cllsc") t]     
+      ""
+      ["Set Printing Notations     sprn<C-BS>" (holes-insert-and-expand "sprn") t]
+      ["Unset Printing Notations   unsprn<C-BS>" (holes-insert-and-expand "unsprn") t]
+      ["Set Printing All           sprall<C-BS>" (holes-insert-and-expand "sprall") t]
+      ["Unset Printing All         unsprall<C-BS>" (holes-insert-and-expand "unsprall") t]
+      ""
+      ["Print Scope/Visibility..." coq-PrintScope t]
+      ["Locate..." coq-LocateNotation t]
+
+      ""
       ["Infix                      inf<C-BS>" (holes-insert-and-expand "inf") t]     
+      ["Notation (simple)          nots<C-BS>" (holes-insert-and-expand "nots") t]     
+      ["Notation (simple,only parsing) notsp<C-BS>" (holes-insert-and-expand "notsp") t]
+      ["Notation (simple,local)    notsl<C-BS>" (holes-insert-and-expand "notsl") t]     
+      ["Notation (simple,local,only parsing) notslp<C-BS>" (holes-insert-and-expand "notslp") t]
+      ""
       ["Notation (no assoc)        nota<C-BS>" (holes-insert-and-expand "nota") t]     
       ["Notation (assoc)           notas<C-BS>" (holes-insert-and-expand "notas") t] 
       ["Notation (no assoc, scope) notasc<C-BS>" (holes-insert-and-expand "notasc") t] 
       ["Notation (assoc, scope)    notassc<C-BS>" (holes-insert-and-expand "notassc") t]
-      ""
-      ["Notation (simple)          nots<C-BS>" (holes-insert-and-expand "nots") t]     
-      ["Notation (simple,local)    notsl<C-BS>" (holes-insert-and-expand "nots") t]     
-
+      ["Delimit Scope              delsc<C-BS>" (holes-insert-and-expand "delsc") t]
+      ["Arguments Scope            argsc<C-BS>" (holes-insert-and-expand "argsc") t]
+      ["Bind Scope                 bndsc<C-BS>" (holes-insert-and-expand "bndsc") t]
       )
+     ""
+     ["Coercion          coerc<C-BS>" (holes-insert-and-expand "coerc") t]
      )
 
-    ("Insert Term" 
+    ("INSERT TERM" 
      "FORM           ABBREVIATION"
      ["forall        fo<C-BS>"  (holes-insert-and-expand "fo") t]
      ["forall1       fo1<C-BS>"  (holes-insert-and-expand "fo1") t]
@@ -231,7 +290,7 @@
      ["match4        m4<C-BS>"  (holes-insert-and-expand "m4") t]
      )
 
-    ("Insert Tactic (a-f)" 
+    ("INSERT TACTIC (a-f)" 
      "TACTIC           ABBREVIATION"
      ["absurd                 abs<C-BS>"  (holes-insert-and-expand "abs") t]
      ["assumption              as<C-BS>"  (holes-insert-and-expand "as") t]
@@ -263,7 +322,7 @@
      ["functional induction    fi<C-BS>"  (holes-insert-and-expand "fi") t]
      )
 
-    ("Insert Tactic (g-z)" 
+    ("INSERT TACTIC (g-z)" 
      "TACTIC           ABBREVIATION"
      ["generalize             g<C-BS>"  (holes-insert-and-expand "g") t]
      ["induction              ind<C-BS>"  (holes-insert-and-expand "ind") t]
@@ -298,12 +357,6 @@
     ;; da: I added Show sub menu, not sure if it's helpful, but why not.
     ;; FIXME: submenus should be split off here.  Also, these commands
     ;; should only be available when a proof is open.
-    ("Show"
-     ["ith goal..." coq-Show t]
-     ["Tree" coq-show-tree t]
-     ["Proof" coq-show-proof t]
-     ["Conjectures" coq-show-conjectures t] ;; maybe not so useful with editing in PG?
-     ["Hints" coq-PrintHint t])
 
     ("Holes" 
      ;; da: I tidied this menu a bit.  I personally think this "trick"
@@ -336,14 +389,9 @@
       :selected (and (boundp 'abbrev-mode) abbrev-mode)])
     ;; With all these submenus you have to wonder if these things belong
     ;; on the main menu.  Are they the most often used?
-    ["Smart intros" coq-intros t]
-    ["Print..." coq-Print t]
-    ["Print Implicit..." coq-Print t]
-    ["About..." coq-About t]
-    ["Check..." coq-Check t]
-    ["Hints" coq-PrintHint t]
-    ["Search isos/pattern..." coq-SearchIsos t]
-    ["Compile" coq-Compile t] ))
+    ["Compile" coq-Compile t]
+    ["Set coq prog name for this file persistently" coq-ask-insert-coq-prog-name t]
+    ))
 
 ;; da: Moved this from the main menu to the Help submenu.  
 ;; It also appears under Holes, anyway.
diff --git a/coq/coq.el b/coq/coq.el
index 3817f3aa..3e4f9660 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -58,7 +58,7 @@ To disable coqc being called (and use only make), set this to nil."
   :group 'coq)
 
 (defconst coq-shell-init-cmd 
-  (format "Set Undo %s. " coq-default-undo-limit))
+  (format "Set Undo %s . " coq-default-undo-limit))
 
 ;; da 15/02/03: moved setting of coq-version-is-vX to coq-syntax to
 ;; fix compilation
@@ -159,6 +159,98 @@ To disable coqc being called (and use only make), set this to nil."
     )
   )
 
+(defconst reqkinds-kinds-table
+  '(("Require" 1) ("Require Export" 2) ("Import" 3))
+  "Enumerates the different kinds of requiring a module.")
+
+
+(defun coq-insert-requires ()
+  "Insert requires to modules, iteratively."
+  (interactive)
+  (let* ((s) 
+         (reqkind 
+          (completing-read "Command (tab to see list, default Require Export) : " 
+                           reqkinds-kinds-table nil nil nil nil "Require Export"))
+         )
+    (setq s (read-string  "Name (empty to stop) : "))
+    (while (not (string-equal s ""))
+      (insert (format "%s %s.\n" reqkind s))
+      (setq s (read-string  "Name (empty to stop) : ")))
+    )
+  )
+
+
+
+
+
+(defun coq-insert-coq-prog-name (progname progargs)
+  "Insert the local variables coq-prog-name and coq-prog-args.
+These variables describe the coqtop command to be launched on this file."
+  (save-excursion
+    (goto-char (point-max))
+    (insert 
+     (format
+      "
+(* 
+   *** Local Variables: ***
+   *** coq-prog-name: %s ***
+   *** coq-prog-args: %s ***
+   *** End: ***
+*)"
+      progname progargs))))
+
+
+(defun coq-ask-build-addpath-option ()
+  "Ask for and return a directory name."
+  (let* 
+      ;; read-file-name here because it is convenient to see .v files when selecting
+      ;; directories to add to the path
+      ((path (read-file-name "library path to add (empty to stop) : "
+                             "" "" t)))
+    (if (and (string-match " " path)
+             (not (y-or-n-p "The path contains spaces, are you sure? (y or n) :")))
+        (coq-ask-build-addpath-option) ; retry
+      path)))
+
+(defun coq-ask-prog-args ()
+  "Ask for and return the information to put into variables coq-prog-args.
+These variable describes the coqtop arguments to be launched on this file."  
+  (let ((progargs '("-emacs"))
+        (option (coq-ask-build-addpath-option)))
+    (message "progargs = %s" progargs)
+    (while (not (string-equal option ""))
+      (setq progargs (cons option (cons "-I" progargs))) ;reversed
+      (message "progargs = %s" progargs)
+      (setq option (coq-ask-build-addpath-option)))
+    (message "progargs = %s" progargs)
+    (reverse progargs)))
+
+(defun coq-ask-prog-name ()
+  "Ask for and return the local variables coq-prog-name.
+These variable describes the coqtop command to be launched on this file."  
+  (let ((cmd (read-string "coq program name (default coqtop) : " "coqtop")))
+    (if (and 
+         (string-match " " cmd)
+         (not (y-or-n-p "The prog name contains spaces, are you sure? (y or n) :")))
+        (coq-ask-prog-name) ; retry
+      cmd)
+    ))
+
+
+(defun coq-ask-insert-coq-prog-name ()
+  "Ask for and insert the local variables coq-prog-name and coq-prog-args.
+These variables describe the coqtop command to be launched on this file."  
+  (interactive)
+  (let ((progname (coq-ask-prog-name))
+         (progargs (coq-ask-prog-args)))
+    (coq-insert-coq-prog-name 
+     (concat "\"" progname "\"") 
+     (concat "(\"" (proof-splice-separator "\" \"" progargs) "\")"))
+    (setq coq-prog-name progname)
+    (setq coq-prog-args progargs)))
+
+
+
 ;; ----- outline
 
 (defvar coq-outline-regexp
@@ -175,8 +267,8 @@ To disable coqc being called (and use only make), set this to nil."
 ;; all these are to be remove when coq > 8.0
 
 (defconst coq-kill-goal-command "Abort. ")
-(defconst coq-forget-id-command "Reset %s. ")
-(defconst coq-back-n-command "Back %s. ")
+(defconst coq-forget-id-command "Reset %s . ")
+(defconst coq-back-n-command "Back %s . ")
 
 
 (defconst coq-state-preserving-tactics-regexp 
@@ -228,7 +320,7 @@ To disable coqc being called (and use only make), set this to nil."
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
 (defun coq-set-undo-limit (undos)
-  (proof-shell-invisible-command (format "Set Undo %s. " undos)))
+  (proof-shell-invisible-command (format "Set Undo %s . " undos)))
 
 ;; da: have now combined count-undos and find-and-forget, they're the
 ;; same now we deal with nested proofs and send general sequence
@@ -479,7 +571,7 @@ If locked span already has a state number, thne do nothing. Also updates
             (naborts (count-not-intersection coq-last-but-one-proofstack proofstack))
             )
     (setq ans
-          (format "Backtrack %s %s %s. " 
+          (format "Backtrack %s %s %s . " 
                   (int-to-string span-staten)
                   (int-to-string proofdepth)
                   naborts)
@@ -631,28 +723,63 @@ This is specific to `coq-mode'."
   (interactive)
   (let (cmd)
     (proof-shell-ready-prover) 
-    (setq cmd (read-string "SearchPattern ex: (?X1 + _ = _ + ?X1) : " "(" 'proof-minibuffer-history))
-    (proof-shell-invisible-command (format "SearchPattern %s. " cmd))))
+    (setq cmd (read-string "SearchPattern (parenthesis mandatory), ex: (?X1 + _ = _ + ?X1) : " "" 'proof-minibuffer-history))
+    (proof-shell-invisible-command (format "SearchPattern %s . " cmd))))
 
 
-(defun coq-guess-or-ask-for-string (s)
+;
+;(defun coq-LocateNotation ()
+;  "Search a a notation.
+;This is specific to `coq-mode'."
+;  (interactive)
+;  (let (cmd)
+;    (proof-shell-ready-prover) 
+;    (setq cmd (read-string "Locate ex: \'exists\' _ , _) : " "" 'proof-minibuffer-history))
+;    (proof-shell-invisible-command (format "Locate %s%s%s . " "\"" cmd "\""))))
+;
+
+
+(defconst notation-print-kinds-table 
+  '(("Print Scope(s)" 0) ("Print Visibility" 1))
+  "Enumerates the different kinds of notation information one can ask to coq.")
+
+(defun coq-PrintScope ()
+  "Show information on notations. Coq specific."
+  (interactive)
+  (let* 
+      ((mods 
+        (completing-read "Infos on notation (tab to see list): " 
+                         notation-print-kinds-table))
+       (s (read-string  "Name (empty for all): "))
+       (all (string-equal s "")))
+    (cond 
+     ((and (string-equal mods "Print Scope(s)") (string-equal s "")) 
+      (proof-shell-invisible-command (format "Print Scopes.")))
+     (t 
+      (proof-shell-invisible-command (format "%s %s ." mods s)))
+     )
+    )
+  )
+
+(defun coq-guess-or-ask-for-string (s &optional dontguess)
   (let ((guess
+         (and (not dontguess)
          (if (region-exists-p) 
              (buffer-substring-no-properties (region-beginning) (region-end))
-           (symbol-near-point))))
+           (symbol-near-point)))))
     (read-string 
-     (if guess (concat s " (" guess "):")(concat s ":"))
+     (if guess (concat s " (" guess "):") (concat s ":"))
      nil 'proof-minibuffer-history guess))
   )
 
-(defun coq-ask-do (ask do)
+(defun coq-ask-do (ask do &optional dontguess postformatcmd)
   "Ask for an ident and print the corresponding term."
-  (let (cmd)
+  (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
     (proof-shell-ready-prover) 
-    (setq cmd (coq-guess-or-ask-for-string ask))
+    (setq cmd (coq-guess-or-ask-for-string ask dontguess))
     (proof-shell-invisible-command
-     (format (concat do " %s. ") cmd)))  
-  ) 
+     (format (concat do " %s . ") (funcall postform cmd))))  
+  )
 
 (defun coq-Print () "Ask for an ident and print the corresponding term."
   (interactive)
@@ -662,6 +789,27 @@ This is specific to `coq-mode'."
   (interactive)
   (coq-ask-do "About: " "About"))
 
+(defun coq-LocateConstant ()
+  "Locate a constant.
+This is specific to `coq-mode'."
+  (interactive)
+  (coq-ask-do "Locate : " "Locate"))
+
+(defun coq-LocateLibrary ()
+  "Locate a constant.
+This is specific to `coq-mode'."
+  (interactive)
+  (coq-ask-do "Locate Library : " "Locate Library"))
+
+(defun coq-addquotes (s) (concat "\"" s "\""))
+
+(defun coq-LocateNotation ()
+  "Locate a notation.
+This is specific to `coq-mode'."
+  (interactive)
+  (coq-ask-do "Locate (ex: \'exists\' _ , _)" "Locate" 
+              'coq-addquotes))
+
 (defun coq-Print-implicit ()
   "Ask for an ident and print the corresponding term."
   (interactive)
@@ -768,6 +916,7 @@ positions."
 ;(proof-defshortcut coq-begin-Section "Section " [(control ?s)])
 (define-key coq-keymap [(control ?i)] 'coq-intros)
 (define-key coq-keymap [(control ?s)] 'coq-insert-section-or-module)
+(define-key coq-keymap [(control ?r)] 'coq-insert-requires)
 (define-key coq-keymap [(control ?m)] 'coq-match)
 (define-key coq-keymap [(control ?e)] 'coq-end-Section)
 (define-key coq-keymap [(control ?o)] 'coq-SearchIsos)
@@ -775,6 +924,9 @@ positions."
 (define-key coq-keymap [(control ?b)] 'coq-About)
 (define-key coq-keymap [(control ?c)] 'coq-Check)
 (define-key coq-keymap [(control ?h)] 'coq-PrintHint)
+(define-key coq-keymap [(control ?l)] 'coq-LocateConstant)
+(define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
+(define-key coq-keymap [(control ?g)] 'coq-Show)
 ;; da: I've moved this three buffer layout into the main code now,
 ;; making it default for three bufer mode.  The function 
 ;; `proof-layout-windows' lays out according to current display
@@ -845,9 +997,9 @@ positions."
   ;; Commands sent to proof engine
   (setq proof-showproof-command "Show. "
 	proof-context-command "Print All. "
-	proof-goal-command "Goal %s. "
-	proof-save-command "Save %s. "
-	proof-find-theorems-command "Search %s. ")
+	proof-goal-command "Goal %s . "
+	proof-save-command "Save %s . "
+	proof-find-theorems-command "Search %s . ")
 ;; FIXME da: Does Coq have a help or about command?
 ;;	proof-info-command "Help"
 
@@ -967,7 +1119,7 @@ positions."
   (proof-shell-config-done))
 
 (defun coq-goals-mode-config ()
-  (setq pg-goals-change-goal "Show %s. ")
+  (setq pg-goals-change-goal "Show %s . ")
   (setq pg-goals-error-regexp coq-error-regexp)
   (coq-init-syntax-table)
   (setq font-lock-keywords coq-font-lock-keywords-1)
@@ -1151,7 +1303,7 @@ Group number 1 matches the name of the library which is required.")
 (defpacustom printing-depth 50
   "*Depth of pretty printer formatting, beyond which dots are displayed."
   :type 'integer
-  :setting "Set Printing Depth %i. ")
+  :setting "Set Printing Depth %i . ")
 
 (defpacustom time-commands nil
   "*Whether to display timing information for each command."