From 4fe4a30c1ae5853f7bfcd91dc6ea1dfb603139d5 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 19 Feb 2004 14:09:14 +0000 Subject: added submenus for command insertion for coq. menu uses abbrev expansion to build holes. --- coq/coq-abbrev.el | 242 ++++++++++++++++++++++++++++-------------------------- coq/coq.el | 84 +++++++++++++++++-- generic/holes.el | 10 ++- 3 files changed, 209 insertions(+), 127 deletions(-) diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index baad752c..dbcaac92 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -7,170 +7,176 @@ (if (boundp 'holes-abbrev-complete) (define-abbrev-table 'coq-mode-abbrev-table '( - ("u" "unfold" nil 0) - ("si" "simpl" nil 0) - ("t" "trivial" nil 0) - ("dec" "decompose []" nil 0) + ("a" "auto" nil 0) ("ab" "absurd" nil 0) + ("abs" "absurd" nil 0) ("ao" "abstract omega" nil 0) - ("s" "simpl" nil 0) - ("r<" "rewrite <-" nil 0) - ("r" "rewrite" nil 0) - ("di" "discriminate" nil 0) - ("p" "Print" nil 0) - ("indv" "Inductive" nil 0) - ("o" "abstract omega" nil 0) - ("l" "Lemma :" nil 0) + ("ap" "apply" nil 0) + ("as" "assumption" nil 0) + ("au" "auto" nil 0) + ("aw" "auto with" nil 0) ("awa" "auto with arith" nil 0) - ("i" "intro" nil 0) - ("h" "Hints : ." nil 0) - ("g" "generalize" nil 0) ("con" "constructor" nil 0) + ("dec" "decompose []" nil 0) + ("def" "Definition : :=." nil 0) + ("di" "discriminate" nil 0) + ("dis" "discriminate" nil 0) ("e" "elim" nil 0) - ("ge" "generalize" nil 0) - ("sym" "symmetry" nil 0) - ("a" "auto" nil 0) - ("re" "rewrite" nil 0) - ("eawa" "eauto with arith" nil 0) - ("un" "unfold" nil 0) + ("ea" "eauto" nil 0) + ("eap" "eapply" nil 0) ("eaw" "eauto with" nil 0) + ("eawa" "eauto with arith" nil 0) + ("el" "elim" nil 0) + ("ex" "exists" nil 0) ("f" "forall #:#,#" nil 0) + ("f" "fun (:) => " nil 0) ("fi" "functional induction" nil 0) + ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0) ("fs" "Functional Scheme xxx := Induction for yyy (opt:with ...)." nil 0) - ("sc" "Scheme := Induction for Sort ." nil 0) - ("f" "fun (:) => " nil 0) - ("eap" "eapply" nil 0) - ("ex" "exists" nil 0) - ("inv" "inversion" nil 0) - ("is" "intros" nil 0) - ("abs" "absurd" nil 0) - ("tr" "trivial" nil 0) - ("in" "intro" nil 0) - ("dis" "discriminate" nil 0) - ("aw" "auto with" nil 0) - ("pr" "Print" nil 0) - ("au" "auto" nil 0) - ("as" "assumption" nil 0) - ("sy" "symmetry" nil 0) - ("el" "elim" nil 0) - ("ap" "apply" nil 0) + ("g" "generalize" nil 0) + ("ge" "generalize" nil 0) ("gen" "generalize" nil 0) + ("h" "Hints : ." nil 0) ("hr" "Hint Resolve :." nil 0) + ("i" "intro" nil 0) + ("in" "intro" nil 0) ("ind" "induction" nil 0) - ("fix" "Fixpoint X (X : X) {struct X} : X := X." nil 0) + ("indv" "Inductive" nil 0) + ("inv" "inversion" nil 0) + ("is" "intros" nil 0) + ("l" "Lemma :" nil 0) + ("o" "abstract omega" nil 0) + ("p" "Print" nil 0) + ("pr" "Print" nil 0) + ("r" "rewrite" nil 0) + ("r<" "rewrite <-" nil 0) + ("re" "rewrite" nil 0) ("re<" "rewrite <-" nil 0) - ("ea" "eauto" nil 0) - ("def" "Definition : :=." nil 0) + ("s" "simpl" nil 0) + ("sc" "Scheme := Induction for Sort ." nil 0) + ("si" "simpl" nil 0) + ("sy" "symmetry" nil 0) + ("sym" "symmetry" nil 0) + ("t" "trivial" nil 0) + ("tr" "trivial" nil 0) + ("u" "unfold" nil 0) + ("un" "unfold" nil 0) )) (define-abbrev-table 'coq-mode-abbrev-table '( + ("a" "auto" holes-abbrev-complete 4) + ("ab" "absurd #" holes-abbrev-complete 0) + ("abs" "absurd #" holes-abbrev-complete 0) + ("ap" "apply #" holes-abbrev-complete 16) + ("as" "assumption" 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) + ("con" "constructor" holes-abbrev-complete 3) + ("dec" "decompose [#] #" holes-abbrev-complete 3) + ("def" "Definition #:# := #." holes-abbrev-complete 5) + ("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5) + ("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) + ("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) + ("di" "discriminate" holes-abbrev-complete 0) + ("dis" "discriminate" holes-abbrev-complete 0) + ("e" "elim #" holes-abbrev-complete 1) + ("ea" "eauto" holes-abbrev-complete 0) + ("eap" "eapply #" holes-abbrev-complete 0) + ("eaw" "eauto with #" holes-abbrev-complete 0) + ("eawa" "eauto with arith" holes-abbrev-complete 0) + ("el" "elim #" holes-abbrev-complete 0) + ("elu" "elim # using #" holes-abbrev-complete 0) + ("ex" "exists #" holes-abbrev-complete 0) + ("f" "fun # => #" holes-abbrev-complete 0) + ("f1" "fun #:# => #" holes-abbrev-complete 0) + ("f2" "fun (#:#) (#:#) => #" holes-abbrev-complete 0) + ("f3" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) + ("f4" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) + ("fi" "functional induction #" holes-abbrev-complete 0) + ("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3) + ("fo" "forall #,#" holes-abbrev-complete 0) + ("fo1" "forall #:#,#" holes-abbrev-complete 0) + ("fo2" "forall (#:#) (#:#), #" holes-abbrev-complete 0) + ("fo3" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) + ("fo4" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) + ("fs" "Functional Scheme # := Induction for #." holes-abbrev-complete 0) + ("fsw" "Functional Scheme # := Induction for # with #." holes-abbrev-complete 0) + ("g" "generalize #" holes-abbrev-complete 0) + ("ge" "generalize #" holes-abbrev-complete 0) + ("gen" "generalize #" holes-abbrev-complete 0) + ("he" "Hint # : # := Extern # # #." holes-abbrev-complete 0) + ("hi" "Hint Immediate #: #." holes-abbrev-complete 0) + ("hr" "Hint Resolve #: #." holes-abbrev-complete 0) + ("hs" "Hints # : #." holes-abbrev-complete 0) + ("hu" "Hint Unfold #: #." holes-abbrev-complete 0) + ("i" "intro #" holes-abbrev-complete 10) + ("if" "if # then # else #" holes-abbrev-complete 1) + ("in" "intro" holes-abbrev-complete 1) + ("ind" "induction #" holes-abbrev-complete 2) + ("indv" "Inductive # : # := # : #." holes-abbrev-complete 0) + ("inv" "inversion #" holes-abbrev-complete 9) + ("is" "intros #" holes-abbrev-complete 11) + ("ite" "if # then # else #" holes-abbrev-complete 1) + ("l" "Lemma # : #." holes-abbrev-complete 4) + ("li" "let # := # in #" holes-abbrev-complete 1) + ("o" "omega" holes-abbrev-complete 0) + ("om" "Omega" holes-abbrev-complete 0) + ("p" "Print #" holes-abbrev-complete 3) + ("pr" "print #" holes-abbrev-complete 2) + ("r" "rewrite #" holes-abbrev-complete 19) + ("r<" "rewrite <- #" holes-abbrev-complete 0) + ("re" "rewrite #" holes-abbrev-complete 0) + ("re<" "rewrite <- #" holes-abbrev-complete 0) + ("s" "simpl" holes-abbrev-complete 23) + ("sc" "Scheme # := Induction for # Sort #." nil 0) + ("si" "simpl" holes-abbrev-complete 0) + ("sp" "Split" holes-abbrev-complete 1) + ("sy" "symmetry" holes-abbrev-complete 0) + ("sym" "symmetry" holes-abbrev-complete 0) + ("t" "trivial" holes-abbrev-complete 1) + ("tr" "trivial" holes-abbrev-complete 7) + ("u" "unfold #" holes-abbrev-complete 1) + ("un" "unfold #" holes-abbrev-complete 7) ("m" "match # with # => #" holes-abbrev-complete 1) - ("m|" "match # with + ("m2" "match # with # => # | # => #" holes-abbrev-complete 1) - ("m||" "match # with + ("m3" "match # with # => # | # => # | # => #" holes-abbrev-complete 1) - ("m|||" "match # with + ("m4" "match # with # => # | # => # | # => # | # => #" holes-abbrev-complete 1) - ("m||||" "match # with + ("m5" "match # with # => # | # => # | # => # | # => # | # => #" holes-abbrev-complete 1) - ("c" "cases #" holes-abbrev-complete 1) - ("u" "unfold #" holes-abbrev-complete 1) - ("si" "simpl" holes-abbrev-complete 0) - ("t" "trivial" holes-abbrev-complete 1) - ("dec" "decompose [#] #" holes-abbrev-complete 3) - ("ab" "absurd #" holes-abbrev-complete 0) - ("om" "abstract Omega" holes-abbrev-complete 0) - ("s" "simpl" holes-abbrev-complete 23) - ("r<" "rewrite <- #" holes-abbrev-complete 0) - ("r" "rewrite #" holes-abbrev-complete 19) - ("di" "discriminate" holes-abbrev-complete 0) - ("p" "Print #" holes-abbrev-complete 3) - ("indv" "Inductive # : # := #." holes-abbrev-complete 0) - ("indv|" "Inductive # : # := + ("indv2" "Inductive # : # := # : # | # : #." holes-abbrev-complete 0) - ("indv||" "Inductive # : # := + ("indv3" "Inductive # : # := # : # | # : # | # : #." holes-abbrev-complete 0) - ("indv|||" "Inductive # : # := + ("indv4" "Inductive # : # := # : # | # : # | # : # | # : #." holes-abbrev-complete 0) - ("indv||||" "Inductive # : # := + ("indv5" "Inductive # : # := # : # | # : # | # : # | # : # | # : #." holes-abbrev-complete 0) - ("o" "abstract omega" holes-abbrev-complete 0) - ("l" "Lemma # : #." holes-abbrev-complete 4) - ("awa" "auto with arith" holes-abbrev-complete 4) - ("i" "intro #" holes-abbrev-complete 10) - ("h" "Hints # : #." holes-abbrev-complete 0) - ("g" "generalize #" holes-abbrev-complete 0) - ("fo" "forall #,#" holes-abbrev-complete 0) - ("fo:" "forall #:#,#" holes-abbrev-complete 0) - ("fo::" "forall (#:#) (#:#), #" holes-abbrev-complete 0) - ("fo:::" "forall (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) - ("fo::::" "forall (#:#) (#:#) (#:#) (#:#), #" holes-abbrev-complete 0) - ("f" "fun # => #" holes-abbrev-complete 0) - ("f:" "fun #:# => #" holes-abbrev-complete 0) - ("f::" "fun (#:#) (#:#) => #" holes-abbrev-complete 0) - ("f:::" "fun (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) - ("f::::" "fun (#:#) (#:#) (#:#) (#:#) => #" holes-abbrev-complete 0) - ("e" "elim #" holes-abbrev-complete 1) - ("con" "constructor" holes-abbrev-complete 3) - ("ge" "generalize #" holes-abbrev-complete 0) - ("sym" "symmetry" holes-abbrev-complete 0) - ("a" "auto" holes-abbrev-complete 4) - ("re" "rewrite #" holes-abbrev-complete 0) - ("eawa" "eauto with arith" holes-abbrev-complete 0) - ("un" "unfold #" holes-abbrev-complete 7) - ("eaw" "eauto with #" holes-abbrev-complete 0) - ("fi" "functional induction #" holes-abbrev-complete 0) - ("fs" "Functional Scheme # := Induction for #." - holes-abbrev-complete 0) - ("fsw" "Functional Scheme # := Induction for # with #." - holes-abbrev-complete 0) - ("sc" "Scheme # := Induction for # Sort #." nil 0) - ("eap" "eapply #" holes-abbrev-complete 0) - ("ex" "exists #" holes-abbrev-complete 0) - ("inv" "inversion #" holes-abbrev-complete 9) - ("is" "intros #" holes-abbrev-complete 11) - ("abs" "absurd #" holes-abbrev-complete 0) - ("tr" "trivial" holes-abbrev-complete 7) - ("in" "intro" holes-abbrev-complete 1) - ("dis" "discriminate" holes-abbrev-complete 0) - ("aw" "auto with #" holes-abbrev-complete 1) - ("pr" "print #" holes-abbrev-complete 2) - ("au" "auto" holes-abbrev-complete 1) - ("as" "assumption" holes-abbrev-complete 4) - ("sy" "symmetry" holes-abbrev-complete 0) - ("el" "elim #" holes-abbrev-complete 0) - ("ap" "apply #" holes-abbrev-complete 16) - ("gen" "generalize #" holes-abbrev-complete 0) - ("hr" "Hint Resolve : #." holes-abbrev-complete 0) - ("ind" "induction #" holes-abbrev-complete 2) - ("fix" "Fixpoint # (#:#) {struct #} : # :=" holes-abbrev-complete 3) - ("re<" "rewrite <- #" holes-abbrev-complete 0) - ("ea" "eauto" holes-abbrev-complete 0) - ("def" "Definition #:# := #." holes-abbrev-complete 5) - ("def2" "Definition # (# : #) (# : #):# := #." holes-abbrev-complete 5) - ("def3" "Definition # (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) - ("def4" "Definition # (# : #) (# : #) (# : #) (# : #):# := #." holes-abbrev-complete 5) ) ) ) diff --git a/coq/coq.el b/coq/coq.el index 804db615..b36f1dc0 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -86,22 +86,92 @@ ;; ----- coq specific menu (defpgdefault menu-entries - '(["Print..." coq-Print t] + '( + ("Insert Command" + "COMMAND ABBREVIATION" + ["Definition def" (insert-and-expand "def") t] + ["Fixpoint fix" (insert-and-expand "fix") t] + ["Functional Scheme fs" (insert-and-expand "fs") t] + ["Functional Scheme w fs" (insert-and-expand "fs") t] + ["Inductive indv" (insert-and-expand "indv") t] + ["Inductive1 indv1" (insert-and-expand "indv1") t] + ["Inductive2 indv2" (insert-and-expand "indv2") t] + ["Inductive3 indv3" (insert-and-expand "indv3") t] + ["Inductive4 indv4" (insert-and-expand "indv4") t] + ["Lemma l" (insert-and-expand "l") t] + ["Scheme sc" (insert-and-expand "sc") t] + ["hint Immediate hi" (insert-and-expand "hi") t] + ["hint Resolve hr" (insert-and-expand "hr") t] + ["hint extern he" (insert-and-expand "he") t] + ["hints hs" (insert-and-expand "hs") t] + ) + + ("Insert term" + "FORM ABBREVIATION" + ["forall fo" (insert-and-expand "fo") t] + ["forall1 fo1" (insert-and-expand "fo1") t] + ["forall2 fo2" (insert-and-expand "fo2") t] + ["forall3 fo3" (insert-and-expand "fo3") t] + ["forall4 fo4" (insert-and-expand "fo4") t] + ["fun f" (insert-and-expand "f") t] + ["fun1 f1" (insert-and-expand "f1") t] + ["fun2 f2" (insert-and-expand "f2") t] + ["fun3 f3" (insert-and-expand "f3") t] + ["fun4 f4" (insert-and-expand "f4") t] + ["if then else if" (insert-and-expand "li") t] + ["let in li" (insert-and-expand "li") t] + ["match m" (insert-and-expand "m") t] + ["match2 m2" (insert-and-expand "m2") t] + ["match3 m3" (insert-and-expand "m3") t] + ["match4 m4" (insert-and-expand "m4") t] + ["match5 m5" (insert-and-expand "m5") t] + ) + + ("Insert tactic" + "TACTIC ABBREVIATION" + ["absurd ab" (insert-and-expand "ab") t] + ["absurd abs" (insert-and-expand "abs") t] + ["assumption as" (insert-and-expand "as") t] + ["auto a" (insert-and-expand "a") t] + ["auto with aw" (insert-and-expand "aw") t] + ["auto with arith awa" (insert-and-expand "awa") t] + ["cases c" (insert-and-expand "c") t] + ["decompose dec" (insert-and-expand "dec") t] + ["discriminate di" (insert-and-expand "di") t] + ["eauto ea" (insert-and-expand "ea") t] + ["eauto with eaw" (insert-and-expand "dec") t] + ["elim e" (insert-and-expand "e") t] + ["elim using elu" (insert-and-expand "elu") t] + ["exists ex" (insert-and-expand "ex") t] + ["functional induction fi" (insert-and-expand "fi") t] + ["generalize g" (insert-and-expand "g") t] + ["induction ind" (insert-and-expand "ind") t] + ["intro i" (insert-and-expand "i") t] + ["intros is" (insert-and-expand "is") t] + ["inversion inv" (insert-and-expand "inv") t] + ["omega om" (insert-and-expand "om") t] + ["rewrite r" (insert-and-expand "r") t] + ["simpl s" (insert-and-expand "s") t] + ["simpl si" (insert-and-expand "si") t] + ["split sp" (insert-and-expand "sp") t] + ["symmetry sym" (insert-and-expand "sym") t] + ["trivial t" (insert-and-expand "t") t] + ["trivial tr" (insert-and-expand "tr") t] + ["unfold u" (insert-and-expand "u") t] + ) + + ["Print..." coq-Print t] ["Check..." coq-Check t] ["Hints" coq-PrintHint t] - ["Intros..." coq-Intros t] ["Show ith goal..." coq-Show t] - ["Apply" coq-Apply t] ["Search isos/pattern..." coq-SearchIsos t] ["expand abbrev at point" expand-abbrev t] - ["list abbrevs" list-abbrevs t] ["What are those #??" (holes-short-doc) t] - ["insert Fixpoint" (insert-and-expand "fix") t] - ["insert Definition" (insert-and-expand "def") t] + ["list abbrevs" list-abbrevs t] ["3 buffers view" coq-three-b t] ["Begin Section..." coq-begin-Section t] ["End Section" coq-end-Section t] - ["Compile" coq-Compile t])) + ["Compile" coq-Compile t] )) diff --git a/generic/holes.el b/generic/holes.el index ab68925f..aefa519c 100644 --- a/generic/holes.el +++ b/generic/holes.el @@ -841,10 +841,16 @@ created" (count-holes-in-last-expand) empty-hole-string) ) +; insert the expansion of abbrev s, and replace #s by holes. It was +; possible to implement it with a simple ((insert s) (expand-abbrev)) +; but undo would show the 2 steps, which is bad. (defun insert-and-expand (s) - (insert s) - (expand-abbrev) + (let* ((exp (abbrev-expansion s)) + (c (count-char-in-string empty-hole-string exp))) + (insert exp) + (replace-string-by-holes-backward-move-point c empty-hole-string) + ) ) (provide 'holes) -- cgit v1.2.3