proofgeneral (3.7-4) minlog/minlog-abbrev.el

--- proofgeneral-3.7.orig/minlog/minlog-abbrev.el
+++ proofgeneral-3.7/minlog/minlog-abbrev.el
@@ -0,0 +1,261 @@
+;; minlog.el Proof General instance for Minlog
+;;
+;; Copyright (C) 2004 Stefan Schimanski, Freiric Barral
+;;
+;; Author: Stefan Schimanski <schimans@math.lmu.de>
+;;         Freiric Barral <barral@math.lmu.de>
+;;
+;;;;; default abbrev table
+
+(defun insert-exp (exp)
+  (let* ((pos (point))			
+			(c (count-re-in-string empty-hole-regexp exp)))
+	 (insert exp)
+	 (replace-string-by-holes-backward-move-point c empty-hole-regexp)
+	 (if (> c 1) (goto-char pos)
+		(goto-char pos)
+		(set-point-next-hole-destroy) ; if only one hole, go to it.
+		)
+	 (if (> c 1) (message "Hit M-ret to jump to active hole. M-x holes-short-doc to see holes doc.")
+		)	 
+	 )
+  )
+
+
+(defun minlog-defined-types ()
+  (let ((algebras (read (progn (proof-shell-invisible-command "(map car ALGEBRAS)" "#t")proof-shell-last-output)))
+	(tconst (read(progn (proof-shell-invisible-command "(map car TYPE-CONSTANTS)" "#t")proof-shell-last-output)))
+	(tvar (read(progn (proof-shell-invisible-command "(map car TYPE-VARIABLES)" "#t")proof-shell-last-output))))
+    (append algebras tconst tvar)    
+    )
+  )
+; (minlog-defined-types)
+
+(defconst algebra-kinds-table 
+  '(("Algebra" 1) ("Simultaneous Algebras" 2) ("Algebra with parameters" 3)("Simultaneous Algebras with parameters" 4))
+  "Enumerates the different kinds of Algebras.")
+
+(defconst commands (list "add-alg" "add-algs" "add-param-alg" "add-param-algs" "remove-algebra-name")
+  "Enumerate the commands of the Minlog system")
+
+(defconst minlog-kind-typ-op (list "postfix-typeop" "prefix-typeop" "prod-typeop"
+			    "tensor-typeop" "sum-typeop" "alg" "alg-typeop")
+  "list of kind of type operator (for display purposes)")
+
+
+(defun alist-from (list)
+  (let (alist)
+    (dotimes (i (length list) alist)
+      (setq alist (append alist (list(list (nth i list) (+ 1 i )))))
+   )))
+
+(defun minlog-alist-defined-types () 
+  (alist-from (minlog-defined-types)))
+
+
+(defconst minlog-alist-kind-typ-op (alist-from minlog-kind-typ-op)
+  "association list of kind of type operator (for display purposes)")
+
+
+;; for later development
+(defconst minlog-add-algs
+(progn
+  (setq l nil)
+  (dotimes (i 4 l)
+    (setq l (append l (list (cons (car (nth i algebra-kinds-table))
+				  (nth i commands)))))))
+  "Association list between the different kind of algebra and the corresponding minlog command")
+
+;; minlog-add-algs
+
+;; arity of a constructor to be used in inductive definition
+;;; todo: better display, prohibit non strictly positive type position in operator
+
+(defun arite-op (n aliste-def-types alg)
+  (progn 
+    (format "arity for constructor number %d:" n)
+    (progn 
+      (setq temp "")
+      (setq operator 1)
+      (while (progn	       
+	       (setq type-in-op 1)
+	       (setq temp2 "")
+	       (setq simple-op t)
+	       (while  (progn  (setq ss (completing-read  
+					   (format "type %d of operator %d  for constructor number %d: (enter to exit, tab to see list)" 
+						   type-in-op operator n)
+					   aliste-def-types))
+				 (not (string-equal  ss "")))
+		  (if (string-equal temp2 "") 
+		      (progn (setq type-in-op (+ 1 type-in-op))
+			     (setq temp2 ss))
+		    (progn (setq temp2 (concat temp2  "=>" ss ))
+			   (setq simple-op nil)
+			   (setq type-in-op (+ 1 type-in-op)))))
+	       (not (string-equal  temp2 "")))
+	(if (string-equal temp "") 
+	    (setq temp temp2)
+	  (if simple-op 
+	      (setq temp (concat temp  "=>" temp2 ))
+	    (setq temp (concat temp  "=>" "(" temp2 ")" ))))
+	  (setq operator (+ 1 operator)))
+      temp)))
+
+;; (arite-op 1 (alist-from commands))
+
+(defun minlog-insert-algebra ()
+  "todo: implement kind-type-op, and kind-constr-op, syntax enjolivement, 
+         implemented ! arity with memory of the already defined types 
+         next step: prohibition of not strictly positive inductive type"
+  (interactive)
+  (let* ((algk (completing-read "kind of algebra (tab to see list): " algebra-kinds-table))
+         (command-algs (cdr (assoc algk minlog-add-algs)))
+	 (single-alg (or (string-equal algk "Algebra")
+			 (string-equal algk "Algebra with parameters")))
+	 (param-alg (or (string-equal algk "Algebra with parameters")
+			(string-equal algk "Simultaneous Algebras with parameters")))	 
+
+	 (liste-algebra 
+	  (progn 
+	    (setq temp nil)
+	    (setq ty-arity 1)
+	    (while (progn (setq ss (read-string (if single-alg "algebra: " 
+						  (format "algebra %d:" 
+							  ty-arity
+							  ))))
+			  (not (or (and single-alg (progn (setq temp (list ss )) t))
+				   (string-equal  ss ""))))
+	      (setq temp (append temp  (list  ss )))
+	      (setq ty-arity (+ 1 ty-arity)))
+	    temp))
+	 (aliste-def-types (alist-from (append (minlog-defined-types) liste-algebra)))
+	 (aliste-algebra (alist-from liste-algebra))
+;	 (algs (if single-alg
+;		   (format "\"%s\"" (caar aliste-algebra))
+;		 (format "(list \"%s\")" (mapconcat (car) (aliste-algebra) "\" \""))
+;		 ))
+	 (algs (format "\"%s\"" (append liste-algebra))
+		)
+	 (kind-type-op (format " '%s" (completing-read 
+				       "kind of algebra type ? (TAB to see list) " 
+			minlog-alist-kind-typ-op)))
+	 (nb-constr (read-minibuffer "number of constructor: "))
+	 (constructeur
+	  (lambda (n)(format "\"%s\"" (read-string (format "constructor number %d: " n)))))
+	 (arite 
+	  (lambda (n) 
+	      (interactive)
+	      (format "\"%s\"" 
+		      (let ((alg (if (or single-alg 
+					 (equal 1 (length aliste-algebra)))
+				     (caar aliste-algebra)
+				   (completing-read 
+				    "constructor for algebra (tab to see list): " 
+				    aliste-algebra)				   
+				 )))
+			(concat (if (string-equal 
+				     (setq ss (arite-op n aliste-def-types alg))
+				     "")
+				    ""
+				  (concat ss "=>"))
+				alg)))))
+	 (kind-constr-op "")
+	 ; trace of the implementation in coq, maybe to be use...
+	 ; when the user don't want to write all the details
+	 (p (point))) 
+    (progn
+      (insert "\(" command-algs " ")
+      (insert algs kind-type-op)
+        (dotimes (i nb-constr)
+	  (insert "\n  '\(" (funcall constructeur (+ 1 i)) 
+		  " " 
+		  (funcall arite (+ 1 i)) kind-constr-op"\)"))
+      (insert ")\n"))))
+
+(define-key minlog-keymap [(control ?a)] 'minlog-insert-algebra)
+
+(defun minlog-remove-algebra ()
+  (interactive)
+  (insert "("
+	  (nth 4 commands)
+	  (format " \"%s\"" (read-string "Name of the algebra to be removed" ""))
+	  ")\n"))
+
+
+(define-key minlog-keymap [(control ?r)] 'minlog-remove-algebra)
+
+(define-key global-map [(control backspace)] 'expand-abbrev)
+
+;#s are replaced by holes by holes-abbrev-complete
+(if (boundp 'holes-abbrev-complete)
+    ()
+  (define-abbrev-table 'minlog-mode-abbrev-table
+	 '(
+	   ("alg" "(add-alg \"#\" '(\"#\") '(\"#\") )" holes-abbrev-complete 3)
+;	   ("a"    "(auto)" holes-abbrev-complete 0)
+	   ("av"    "(av \"#\")" holes-abbrev-complete 0)
+	   ("as"     "(assume \"#\")" holes-abbrev-complete 0)
+	   ("aa" "(add-alg \"#\" '(\"#\") '(\"#\") )" 
+	    holes-abbrev-complete 0
+	    )
+	   ("ac" "(add-computation-rule (pt \"#\") (pt \"#\"))" holes-abbrev-complete 0)
+	   ("ap" "(add-program-constant (pt \"@{name}\") @{type} @{t-deg} @{token-type} @{arity})" holes-abbrev-complete 0)
+	   ("i"     "(ind)"   holes-abbrev-complete 0)		
+	   ("ar" "(add-rewrite-rule (pt \"#\") (pt \"#\"))" holes-abbrev-complete 0)
+	   ("s"    "(search)" holes-abbrev-complete 0)
+	   ("set"   "(set-goal (pf \"#\"))" holes-abbrev-complete 0)
+	   ("si"   "(simp \"#\")" holes-abbrev-complete 0)
+	   ("sp"   "(split)" holes-abbrev-complete 0)
+	   ("st"   "(strip @{number})" holes-abbrev-complete 0)	   
+
+	 )
+  )
+;TODO: build the command submenu automatically from abbrev table
+  (defpgdefault menu-entries
+    '(
+      ("Insert Command" 
+       "COMMAND               ABBREVIATION"
+       ["Add an algebra (interactive)...    " minlog-insert-algebra t]
+       ["Remove an algebra (interactive)... " minlog-remove-algebra t]
+       ["Add an algebra            alg<C-BS>" (insert-and-expand "alg") t]
+       ["Add a computation rule    ac<C-BS>" (insert-and-expand "ac") t]
+       ["Add a rewrite rule        ar<C-BS>"  (insert-and-expand "ar") t]
+       ["Add a variable            av <C-BS>"  (insert-and-expand "av") t]
+       ["Add a program constant    ap <C-BS>"  (insert-and-expand "ap") t]
+       ["Set goal                  set<C-BS>"  (insert-and-expand "set") t]
+       )
+       ("Insert tactic"
+	["ind                      i<C-BS>" (insert-and-expand "i") t]
+	["assume                   as<C-BS>" (insert-and-expand "as") t]
+	["strip                    st<C-BS>" (insert-and-expand "st") t]
+	["auto                     a<C-BS>" (insert-and-expand "a") t]	
+	["search                   s<C-BS>" (insert-and-expand "s") t]	
+	["split                    sp<C-BS>" (insert-and-expand "sp") t]	
+	["simp                     si<C-BS>" (insert-and-expand "si") t]	
+	)
+
+       ["What are those highlighted chars??" (holes-short-doc) t]
+       ("holes" 
+	"make a hole active   click on it"
+	"disable a hole   click on it (button 2)"
+	"destroy a hole   click on it (button 3)"
+	"make a hole with mouse  C-M-select"
+	["make a hole at point   C-M-h"  (set-make-active-hole) t]
+	["make selection a hole  C-M-h"  (set-make-active-hole) t]
+	["replace active hole by selection C-M-y"  (replace-update-active-hole) t]
+	"replace active hole with mouse  C-M-Shift select"
+	["jump to active hole M-return"  (set-point-next-hole-destroy) t]
+	["forget all holes in this buffer"  (clear-all-buffer-holes) t]
+	["What are those holes?" (holes-short-doc) t]
+	)
+       ("Insert examples schemata"
+	["Add an algebra            alg<C-BS>" (insert-and-expand "alg") t]
+	)
+       ["expand abbrev at point" expand-abbrev t]
+       ["list abbrevs" list-abbrevs t]
+       )
+  )
+)
+ 
+(provide 'minlog-abbrev)
+